MR Solver SMT fixes for testing on Heapster models

heapster-saw/examples/arrays_mr_solver.saw

@@ -0,0 +1,3 @@
+include "arrays.saw";
+contains0 <- parse_core_mod "arrays" "contains0";
+mr_solver_debug 1 contains0 contains0;

saw-core/src/Verifier/SAW/OpenTerm.hs

@@ -27,13 +27,14 @@ module Verifier.SAW.OpenTerm (
   unitOpenTerm, unitTypeOpenTerm,
   stringLitOpenTerm, stringTypeOpenTerm,
   trueOpenTerm, falseOpenTerm, boolOpenTerm, boolTypeOpenTerm,
-  arrayValueOpenTerm, bvLitOpenTerm, bvTypeOpenTerm,
+  arrayValueOpenTerm, vectorTypeOpenTerm, bvLitOpenTerm, bvTypeOpenTerm,
   pairOpenTerm, pairTypeOpenTerm, pairLeftOpenTerm, pairRightOpenTerm,
   tupleOpenTerm, tupleTypeOpenTerm, projTupleOpenTerm,
   tupleOpenTerm', tupleTypeOpenTerm',
   recordOpenTerm, recordTypeOpenTerm, projRecordOpenTerm,
   ctorOpenTerm, dataTypeOpenTerm, globalOpenTerm, extCnsOpenTerm,
-  applyOpenTerm, applyOpenTermMulti, applyPiOpenTerm, piArgOpenTerm,
+  applyOpenTerm, applyOpenTermMulti, applyGlobalOpenTerm,
+  applyPiOpenTerm, piArgOpenTerm,
   lambdaOpenTerm, lambdaOpenTermMulti, piOpenTerm, piOpenTermMulti,
   arrowOpenTerm, letOpenTerm, sawLetOpenTerm,
   -- * Monadic operations for building terms with binders
@@ -179,6 +180,10 @@ bvLitOpenTerm :: [Bool] -> OpenTerm
 bvLitOpenTerm bits =
   arrayValueOpenTerm boolTypeOpenTerm $ map boolOpenTerm bits
 
+-- | Create a SAW core term for a vector type
+vectorTypeOpenTerm :: OpenTerm -> OpenTerm -> OpenTerm
+vectorTypeOpenTerm n a = applyGlobalOpenTerm "Prelude.Vec" [n,a]
+
 -- | Create a SAW core term for the type of a bitvector
 bvTypeOpenTerm :: Integral a => a -> OpenTerm
 bvTypeOpenTerm n =
@@ -287,6 +292,10 @@ applyOpenTerm (OpenTerm f) (OpenTerm arg) =
 applyOpenTermMulti :: OpenTerm -> [OpenTerm] -> OpenTerm
 applyOpenTermMulti = foldl applyOpenTerm
 
+-- | Apply a named global to 0 or more arguments
+applyGlobalOpenTerm :: Ident -> [OpenTerm] -> OpenTerm
+applyGlobalOpenTerm ident = applyOpenTermMulti (globalOpenTerm ident)
+
 -- | Compute the output type of applying a function of a given type to an
 -- argument. That is, given @tp@ and @arg@, compute the type of applying any @f@
 -- of type @tp@ to @arg@.

src/SAWScript/Builtins.hs

@@ -1385,8 +1385,8 @@ tailPrim :: [a] -> TopLevel [a]
 tailPrim [] = fail "tail: empty list"
 tailPrim (_ : xs) = return xs
 
-parseCore :: String -> TopLevel Term
-parseCore input =
+parseCoreMod :: String -> String -> TopLevel Term
+parseCoreMod mnm_str input =
   do sc <- getSharedContext
      let base = "<interactive>"
          path = "<interactive>"
@@ -1397,18 +1397,29 @@ parseCore input =
            do let msg = show err
               printOutLnTop Opts.Error msg
               fail msg
-     let mnm = Just $ mkModuleName ["Cryptol"]
-     err_or_t <- io $ runTCM (typeInferComplete uterm) sc mnm []
+     let mnm =
+           mkModuleName $ Text.splitOn (Text.pack ".") $ Text.pack mnm_str
+     _ <- io $ scFindModule sc mnm -- Check that mnm exists
+     err_or_t <- io $ runTCM (typeInferComplete uterm) sc (Just mnm) []
      case err_or_t of
        Left err -> fail (show err)
        Right (TC.TypedTerm x _) -> return x
 
+parseCore :: String -> TopLevel Term
+parseCore = parseCoreMod "Cryptol"
+
 parse_core :: String -> TopLevel TypedTerm
 parse_core input = do
   t <- parseCore input
   sc <- getSharedContext
   io $ mkTypedTerm sc t
 
+parse_core_mod :: String -> String -> TopLevel TypedTerm
+parse_core_mod mnm input = do
+  t <- parseCoreMod mnm input
+  sc <- getSharedContext
+  io $ mkTypedTerm sc t
+
 prove_core :: ProofScript () -> String -> TopLevel Theorem
 prove_core script input =
   do sc <- getSharedContext
@@ -1540,16 +1551,18 @@ monadifyTypedTerm sc t =
 
 -- | Ensure that a 'TypedTerm' has been monadified
 ensureMonadicTerm :: SharedContext -> TypedTerm -> TopLevel TypedTerm
-ensureMonadicTerm _ t
-  | TypedTermOther tp <- ttType t
-  , Prover.isCompFunType tp = return t
+ensureMonadicTerm sc t
+  | TypedTermOther tp <- ttType t =
+    io (Prover.isCompFunType sc tp) >>= \case
+      True -> return t
+      False -> monadifyTypedTerm sc t
 ensureMonadicTerm sc t = monadifyTypedTerm sc t
 
 mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool
 mrSolver sc dlvl t1 t2 =
   do m1 <- ttTerm <$> ensureMonadicTerm sc t1
      m2 <- ttTerm <$> ensureMonadicTerm sc t2
-     res <- liftIO $ Prover.askMRSolver sc dlvl SBV.z3 Nothing m1 m2
+     res <- liftIO $ Prover.askMRSolver sc dlvl Nothing m1 m2
      case res of
        Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False
        Nothing -> return True

src/SAWScript/Interpreter.hs

@@ -2225,6 +2225,13 @@ primitives = Map.fromList
     [ "Parse a Term from a String in SAWCore syntax."
     ]
 
+  , prim "parse_core_mod"      "String -> String -> Term"
+    (funVal2 parse_core_mod)
+    Current
+    [ "Parse a Term from the second supplied String in SAWCore syntax,"
+    , "relative to the module specified by the first String"
+    ]
+
   , prim "prove_core"         "ProofScript () -> String -> TopLevel Theorem"
     (pureVal prove_core)
     Current