parse_core panics on SAW core terms with types not supported by Cryptol

[eddywestbrook]

The following leads to a panic:

parse_core "returnM Bool True"

Interestingly enough, the following does not, and successfully prints out the corresponding SAW core term when this is inputted into the prompt:

parse_core "\\ (x:Bool) -> returnM Bool x"

But, if you try to perform a computation on the Cryptol type of the resulting term, you then get the panic again. E.g., this again leads to a panic:

type (parse_core "\\ (x:Bool) -> returnM Bool x")

[eddywestbrook]

One really straightforward solution is to wrap the call to the simulator in scCryptolType in a catch block, like this:

scCryptolType :: SharedContext -> Term -> IO (Maybe (Either C.Kind C.Type))
scCryptolType sc t =
  do modmap <- scGetModuleMap sc
     catch
       (case SC.evalSharedTerm modmap Map.empty Map.empty t of
           SC.TValue tv -> return (asCryptolTypeValue tv)
           _ -> return Nothing)
       (\ (_::SomeException) -> return Nothing)

[eddywestbrook]

Ok, scratch that: wrapping the call to the simulator in scCryptolType in a catch only makes the first example work. That is, it makes this not panic: parse_core "returnM Bool True". The other example still panics.

[eddywestbrook]

Aha, this is because the above function definition does not evaluate asCryptolTypeValue. The following seems to fix the problem:

scCryptolType :: SharedContext -> Term -> IO (Maybe (Either C.Kind C.Type))
scCryptolType sc t =
  do modmap <- scGetModuleMap sc
     catch
       (case SC.evalSharedTerm modmap Map.empty Map.empty t of
           SC.TValue tv
             | Just !ret <- asCryptolTypeValue tv -> return $ Just ret
           _ -> return Nothing)
       (\ (_::SomeException) -> return Nothing)

[eddywestbrook]

Of course, it would probably be better if the simulator itself could handle unknown type constructors like CompM without panicking...

[brianhuffman]

This should be fixable because the saw-script Term type now includes values that don't have an actual cryptol type. The scCryptolType function needs to have better error handling.

[robdockins]

The immediate problem here is that the simulator doesn't have a representation for the CompM type constructor. We can add that to the TValue type directly, which would solve the immediate problem. Or, we could try to solve the problem in generality and allow the simulator to handle "abstract" type constructors. I don't know offhand how difficult that would be.

[eddywestbrook]

Well, unless we can guarantee that the simulator won't panic on any well-typed SAW core terms, however arbitrarily complex they are, then it is always possible that this call to the simulator could panic, because it is passed an arbitrary SAW core term. If the simulator panics here, it just means that the input SAW core term is outside the scope of what it can handle, which IMHO means that the function should return Nothing. At least, that's how I am interpreting the semantics of this function. To me, the difficulty here was that laziness meant that the panic was being carried around as a subterm of the returned value, which is why I put that bang pattern there. But maybe you guys see it differently?

[sauclovian-g]

I think this is the same as #780.

[RyanGlScott]

Note that #1552 added the exception-catching hack proposed in #1479 (comment), so the example above no longer panics. There is still work to be done to figure out how to improve the error-handling story so that we do not need to resort to such a hack.