Better printing of Cryptol errors in saw-remote-api

[RyanGlScott]

This is a first stab at improving the state of affairs observed in #1128. Before, we had:

Running: cabal new-exec --verbose=0 saw-remote-api socket
⚠️  Failed to verify: lemma_FPointsToContract (defined at bug.py:34):
error: Cryptol error: RenamerErrors (FromModule (ModName "<interactive>")) [UnboundExpr (Located {srcRange = Range {from = Position {line = 1, col = 1}, to = Position {line = 1, col = 2}, source = ""}, thing = UnQual (Ident False "x")}) <NameDisp>,UnboundExpr (Located {srcRange = Range {from = Position {line = 1, col = 5}, to = Position {line = 1, col = 6}, source = ""}, thing = UnQual (Ident False "x")}) <NameDisp>]
CallStack (from HasCallStack):
  error, called at src/SAWServer/LLVMCrucibleSetup.hs:175:24 in saw-remote-api-0.1.0.0-inplace:SAWServer.LLVMCrucibleSetup
Traceback (most recent call last):
  File "bug.py", line 34, in <module>
    result = llvm_verify(mod, "f", FPointsToContract())
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/__init__.py", line 396, in llvm_verify
    raise result.exception from None
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/__init__.py", line 361, in llvm_verify
    conn.llvm_assume(module.server_name,
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/virtenv/lib/python3.8/site-packages/argo_client/interaction.py", line 163, in result
    return self.process_result(self._result_and_state_and_out_err()[0])
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/virtenv/lib/python3.8/site-packages/argo_client/interaction.py", line 148, in _result_and_state_and_out_err
    raise self.process_error(exception)
saw.exceptions.VerificationError: error: Cryptol error: RenamerErrors (FromModule (ModName "<interactive>")) [UnboundExpr (Located {srcRange = Range {from = Position {line = 1, col = 1}, to = Position {line = 1, col = 2}, source = ""}, thing = UnQual (Ident False "x")}) <NameDisp>,UnboundExpr (Located {srcRange = Range {from = Position {line = 1, col = 5}, to = Position {line = 1, col = 6}, source = ""}, thing = UnQual (Ident False "x")}) <NameDisp>]
CallStack (from HasCallStack):
  error, called at src/SAWServer/LLVMCrucibleSetup.hs:175:24 in saw-remote-api-0.1.0.0-inplace:SAWServer.LLVMCrucibleSetup
🛑  The goal failed to verify.

Now, we have:

Running: cabal new-exec --verbose=0 saw-remote-api socket
Traceback (most recent call last):
  File "bug.py", line 34, in <module>
    result = llvm_verify(mod, "f", FPointsToContract())
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/__init__.py", line 381, in llvm_verify
    raise err from None
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/__init__.py", line 346, in llvm_verify
    stdout = res.stdout()
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/virtenv/lib/python3.8/site-packages/argo_client/interaction.py", line 167, in stdout
    return self._result_and_state_and_out_err()[2]
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/virtenv/lib/python3.8/site-packages/argo_client/interaction.py", line 148, in _result_and_state_and_out_err
    raise self.process_error(exception)
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/commands.py", line 8, in process_error
    return exceptions.make_saw_exception(ae)
  File "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/galois-py-toolkit/saw/exceptions.py", line 42, in make_saw_exception
    raise ae
argo_client.interaction.ArgoException: [error] at :1:1--1:2 Value not in scope: x
[error] at :1:5--1:6 Value not in scope: x {'warnings': [], 'source': 'module name <interactive>', 'errors': ['[error] at :1:1--1:2 Value not in scope: x', '[error] at :1:5--1:6 Value not in scope: x']}
🔶 No goal results logged.

There's obviously some room for improvement still (it still prints a {'warnings': ... } dictionary, and the errors lack filenames), but I wanted to submit this now to get @pnwamk's feedback.

[pnwamk]

Looks strictly better to me =)

[RyanGlScott]

Upon further inspection, the room for improvement might strictly be a cryptol-remote-api problem, as I am able to observe similar problems without bringing in SAW at all:

# crypt.py
import os
from pathlib import Path
import cryptol

server = os.environ.get('CRYPTOL_SERVER')
if not server:
    server = "cabal new-exec --verbose=0 cryptol-remote-api socket"
print("Running: " + server)
c = cryptol.connect(server)

c.load_module('Cryptol')
print(c.evaluate_expression("1 + True").result())

Running: cabal new-exec --verbose=0 cryptol-remote-api socket
Traceback (most recent call last):
  File "crypt.py", line 13, in <module>
    print(c.evaluate_expression("1 + True").result())
  File "/home/rscott/.cache/pypoetry/virtualenvs/signal-verification-E-XE2rfq-py3.8/lib/python3.8/site-packages/argo_client/interaction.py", line 215, in result
    return self.process_result(self._result_and_out_err()[0])
  File "/home/rscott/.cache/pypoetry/virtualenvs/signal-verification-E-XE2rfq-py3.8/lib/python3.8/site-packages/argo_client/interaction.py", line 205, in _result_and_out_err
    raise self.process_error(exception)
argo_client.interaction.ArgoException: [error] at :1:1--1:9:
  • Type `Bit` does not support ring operations.
      arising from
      use of expression (Cryptol::+)
      at :1:1--1:9 {'warnings': [], 'source': 'module name <interactive>', 'errors': ['(Range {from = Position {line = 1, col = 1}, to = Position {line = 1, col = 9}, source = ""},UnsolvableGoals [Goal {goalSource = CtInst (EVar (Name {nUnique = 4143, nInfo = Declared (ModName "Cryptol") UserName, nIdent = Ident True "+", nFixity = Just (Fixity {fAssoc = LeftAssoc, fLevel = 80}), nLoc = Range {from = Position {line = 289, col = 12}, to = Position {line = 289, col = 13}, source = "Cryptol"}})), goalRange = Range {from = Position {line = 1, col = 1}, to = Position {line = 1, col = 9}, source = ""}, goal = TCon (PC PRing) [TCon (TC TCBit) []]}])']}

It looks like cryptol-remote-api formats all of its error messages this way, and since saw-remote-api is piggybacking on top of cryptol-remote-api's error message infrastructure, it inherits the same formatting. Perhaps we should just merge this as-is and open an issue in the cryptol repo to track improving how it formats error messages?

[RyanGlScott]

I've opened GaloisInc/cryptol#1106 to track improving the Cryptol side of the error message.