Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Invoking Cryptol's error function discards the error string #1326

Open
RyanGlScott opened this issue Jun 9, 2021 · 1 comment · May be fixed by #1344
Open

Invoking Cryptol's error function discards the error string #1326

RyanGlScott opened this issue Jun 9, 2021 · 1 comment · May be fixed by #1344
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core topics: error-messages Issues involving the messages SAW produces on error

Comments

@RyanGlScott
Copy link
Contributor

Any invocation of Cryptol's error function will result in the same message:

sawscript> prove abc {{ error "Descriptive error message" : Bit }}

Run-time error: encountered call to the Cryptol 'error' function

This makes it difficult to track down what function is causing a Cryptol-related failure in SAW proofs. The culprit is this line of code:

ecError a len msg = error a "encountered call to the Cryptol 'error' function"; -- FIXME: don't throw away message

@RyanGlScott RyanGlScott added topics: error-messages Issues involving the messages SAW produces on error subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core labels Jun 9, 2021
@RyanGlScott
Copy link
Contributor Author

It looks like ecError did pass the error string along at one point, but this was changed in 2e68cd0 for reasons that are unclear to me.

RyanGlScott added a commit that referenced this issue Jun 17, 2021
This patch adds two new SAWCore primitives:

* `appendString : String -> String -> String`, which appends the underlying
  `Text` values in a `String`, and
* `bytesToString : (n : Nat) -> Vec n (Vec 8 Bool) -> String`, which converts a
  Cryptol string (a sequence of 8-bit ASCII characters) to a SAWCore `String`.

Moreover, this reimplements `ecError` in terms of
`appendString`/`bytesToString` such that invoking the Cryptol `error` function
from SAW will preserve the string passed to `error`. Previously, if you invoked
the following in SAW:

```
sawscript> prove abc {{ error "Descriptive error message" : Bit }}
```

You would get:

```
Run-time error: encountered call to the Cryptol 'error' function
```

Now, you get:

```
Run-time error: encountered call to the Cryptol 'error' function: Descriptive error message
```

Fixes #1326.
@RyanGlScott RyanGlScott linked a pull request Jun 17, 2021 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core topics: error-messages Issues involving the messages SAW produces on error
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant