Bad error message for "prove_print rme ..."

[ramsdell]

In saw version 0.5 (d2d48ee9), prove_print rme thm produces the following error message:

[17:37:32.785] bvStreamGetOp CallStack (from HasCallStack): error, called at src/Verifier/SAW/Simulator/RME.hs:338:3 in saw-core-0.12HglGxrwc5M9tSYlrEJLAX:Verifier.SAW.Simulator.RME

I doubt this is what you want users to see. To duplicate, run saw with the aes.saw script while ensuring that the contents of cryptol-spec is on saw's path.

AES.cry.txt aes.saw.txt

[brianhuffman]

Apparently we have an unimplemented primitive in the rme proof backend (specifically, symbolic indexing into an infinite stream), and there is a call to the Haskell error function as a placeholder. We should never call error to indicate user errors, so we should definitely consider this a bug.

We could fix this particular case by simply implementing the primitive. But I can see other calls to error in the rme backend for other unimplemented primitives, and not all of them are implementable in the rme backend; for example, we'll never be able to handle symbolic integer operations because rme only handles boolean formulas.

To fix this properly, we really need to start using a proper exception handling mechanism in the rme backend. Currently the rme backend runs in the Identity monad, which doesn't provide any options for error handling, so we should probably switch this code to the IO monad, and use the IO exceptions for unimplemented/unsupported primitives that we recently added for this purpose.

[robdockins]

FYI, this coincidentally overlaps with work I'm doing in the split-arith branches. One of the tasks is to remove the bvStreamGet operation and fold it into streamGet.

As to the error handling, I think we'd get most of the same bang for the buck by using throw on an appropriate exception type.

[brianhuffman]

I strongly prefer to use throwIO instead of throw. The problem with throw is that it doesn't provide any sequencing guarantees w.r.t. the IO monad, so in the presence of laziness exceptions might be thrown at delayed times when a computation is forced, and it's hard to ensure that these latent exceptions can't slip past your exception handlers.

We should really just switch all the saw-core backends to use the IO monad. We don't really get any benefit from having some backends run in Identity. And making the evaluation code work for arbitrary monads has drawbacks: It's harder to understand, it requires lots of SPECIALIZE pragmas to compile efficiently, it requires different implementations of thunks for each monad, different implementations of stream datatype for each monad, etc.

[robdockins]

Fair enough. I'll just note that it was pretty useful in the recent Cryptol refactor I did to have the monad be selectable per backend so I could fold in handling for safety predicates. Not sure if that's an argument here against just going to IO, but something to think about. Otherwise, I basically agree there's no reason we shouldn't at least have a MonadIO constraint and use throwIO.