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.

Sign up for GitHub

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

Jump to bottom

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 type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone
2024T3

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:

saw-script/cryptol-saw-core/saw/Cryptol.sawcore

Line 1410 in 1a6dd61

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
@RyanGlScott
Propagate Cryptol error strings
b9c7784 
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
Draft
@sauclovian-g sauclovian-g mentioned this issue Oct 16, 2024
Closed
@sauclovian-g sauclovian-g added this to the 2024T3 milestone Nov 1, 2024
@sauclovian-g sauclovian-g added the type: bug Issues reporting bugs or unexpected/unwanted behavior label Nov 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
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 type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Milestone
2024T3
Development

Successfully merging a pull request may close this issue.

WIP: Propagate Cryptol error strings GaloisInc/saw-script
2 participants
@RyanGlScott @sauclovian-g