Merge pull request #1952 from GaloisInc/mrsolver-specM-fixes

MRSolver SpecM bugfixes

cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs

@@ -92,7 +92,7 @@ import Verifier.SAW.SharedTerm
 import Verifier.SAW.OpenTerm
 import Verifier.SAW.TypedTerm
 import Verifier.SAW.Cryptol (Env)
--- import Verifier.SAW.SCTypeCheck
+import Verifier.SAW.SCTypeCheck
 import Verifier.SAW.Recognizer
 -- import Verifier.SAW.Position
 import Verifier.SAW.Cryptol.PreludeM
@@ -608,7 +608,9 @@ fromCompTerm mtp t = ArgMonTerm $ fromArgTerm mtp t
 
 -- | Take a function of type @A1 -> ... -> An -> SpecM E emptyFunStack B@ and
 -- lift the stack of the output type to an arbitrary @stack@ parameter using
--- @liftStackS@
+-- @liftStackS@. Note that @liftStackS@ is only added if the stack of the
+-- output type is non-empty, i.e. not @emptyFunStack@. Otherwise, this operation
+-- leaves the function unchanged.
 class LiftCompStack a where
   liftCompStack :: HasSpecMParams => a -> a
 
@@ -623,10 +625,14 @@ instance LiftCompStack ArgMonTerm where
 
 instance LiftCompStack MonTerm where
   liftCompStack (ArgMonTerm amtrm) = ArgMonTerm $ liftCompStack amtrm
-  liftCompStack (CompMonTerm mtp trm) =
-    CompMonTerm mtp $
-    applyGlobalOpenTerm "Prelude.liftStackS"
-    [specMEvType ?specMParams, specMStack ?specMParams, toArgType mtp, trm]
+  liftCompStack (CompMonTerm mtp trm) = CompMonTerm mtp $ OpenTerm $ do
+    -- Only add @liftStackS@ when the stack is not @emptyFunStack@
+    empty_stk <- typedVal <$> unOpenTerm emptyStackOpenTerm
+    curr_stk  <- typedVal <$> unOpenTerm (specMStack ?specMParams)
+    curr_stk_empty <- liftTCM scConvertible False empty_stk curr_stk
+    unOpenTerm $ if curr_stk_empty then trm else
+      applyGlobalOpenTerm "Prelude.liftStackS"
+      [specMEvType ?specMParams, specMStack ?specMParams, toArgType mtp, trm]
 
 -- | Test if a monadification type @tp@ is pure, meaning @MT(tp)=tp@
 monTypeIsPure :: MonType -> Bool
@@ -708,8 +714,8 @@ applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] ->
 applyMonTermMulti = foldl applyMonTerm
 
 -- | Build a 'MonTerm' from a global of a given argument type, applying it to
--- the current 'SpecMParams' if the 'Bool' flag is 'True' and lifting it using
--- @liftStackS@ if it is 'False'
+-- the current 'SpecMParams' if the 'Bool' flag is 'True' or lifting it using
+-- @liftStackS@ if it is 'False' and the stack is non-empty
 mkGlobalArgMonTerm :: HasSpecMParams => MonType -> Ident -> Bool -> ArgMonTerm
 mkGlobalArgMonTerm tp ident params_p =
   (if params_p then id else liftCompStack) $
@@ -747,9 +753,11 @@ data MonMacro = MonMacro {
   macroNumArgs :: Int,
   macroApply :: GlobalDef -> [Term] -> MonadifyM MonTerm }
 
--- | Make a simple 'MonMacro' that inspects 0 arguments and just returns a term
+-- | Make a simple 'MonMacro' that inspects 0 arguments and just returns a term,
+-- lifted with @liftStackS@ if the outer stack is non-empty
 monMacro0 :: MonTerm -> MonMacro
-monMacro0 mtrm = MonMacro 0 (\_ _ -> return mtrm)
+monMacro0 mtrm = MonMacro 0 $ \_ _ -> usingSpecMParams $
+  return $ liftCompStack mtrm
 
 -- | Make a 'MonMacro' that maps a named global to a global of semi-pure type.
 -- (See 'fromSemiPureTermFun'.) Because we can't get access to the type of the
@@ -773,7 +781,7 @@ semiPureGlobalMacro from to params_p =
 -- indicates whether the "to" global is polymorphic in the event type and
 -- function stack; if so, the current 'SpecMParams' are passed as its first two
 -- arguments, and otherwise the returned computation is lifted with
--- @liftStackS@.
+-- @liftStackS@ if the outer stack is non-empty.
 argGlobalMacro :: NameInfo -> Ident -> Bool -> MonMacro
 argGlobalMacro from to params_p =
   MonMacro 0 $ \glob args -> usingSpecMParams $

heapster-saw/examples/Makefile

@@ -41,7 +41,7 @@ endif
 	$(SAW) $<
 
 # Lists all the Mr Solver tests, without their ".saw" suffix
-MR_SOLVER_TESTS = exp_explosion_mr_solver # arrays_mr_solver linked_list_mr_solver sha512_mr_solver
+MR_SOLVER_TESTS = exp_explosion_mr_solver linked_list_mr_solver arrays_mr_solver sha512_mr_solver
 
 .PHONY: mr-solver-tests $(MR_SOLVER_TESTS)
 mr-solver-tests: $(MR_SOLVER_TESTS)

heapster-saw/examples/SpecPrims.cry

@@ -2,25 +2,25 @@ module SpecPrims where
 
 /* Specification primitives */
 
-// The specification that holds for f x for some input x
-exists : {a, b} (a -> b) -> b
-exists f = error "Cannot run exists"
+// The specification that holds for some element of type a
+exists : {a} a
+exists = error "Cannot run exists"
 
-// The specification that holds for f x for all inputs x
-forall : {a, b} (a -> b) -> b
-forall f = error "Cannot run forall"
+// The specification that holds for all elements of type a
+forall : {a} a
+forall = error "Cannot run forall"
 
-// The specification that a computation returns some value with no errors
-returnsSpec : {a} a
-returnsSpec = exists (\x -> x)
+// The specification that a computation has no errors
+noErrors : {a} a
+noErrors = exists
 
 // The specification that matches any computation. This calls exists at the
-// function type () -> a, which is monadified to () -> CompM a. This means that
+// function type () -> a, which is monadified to () -> SpecM a. This means that
 // the exists does not just quantify over all values of type a like noErrors,
 // but it quantifies over all computations of type a, including those that
 // contain errors.
 anySpec : {a} a
-anySpec = exists (\f -> f ())
+anySpec = exists ()
 
 // The specification which asserts that the first argument is True and then
 // returns the second argument

heapster-saw/examples/arrays.sawcore

@@ -3,39 +3,41 @@ module arrays where
 
 import Prelude;
 
+-- The LetRecType of noErrorsContains0
+noErrorsContains0LRT : LetRecType;
+noErrorsContains0LRT =
+  LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
+  LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
+  LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
+  LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))));
+
 -- The helper function for noErrorsContains0
 --
 -- noErrorsContains0H len i v =
---   orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
+--   orS (existsS x. x) (noErrorsContains0H len (i+1) v)
 noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                     CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
-noErrorsContains0H len_top i_top v_top =
-  letRecM
-    (LRT_Cons
-     (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
-      LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
-      LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
-      LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
-     LRT_Nil)
-    (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
-    (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
-       ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
-           invariantHint
-             (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
-             (and (bvsle 64 0x0000000000000000 i)
-                  (bvsle 64 i 0x0fffffffffffffff))
-             (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                  (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
-                           (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
-                  (f len (bvAdd 64 i 0x0000000000000001) v))), ()))
+                     SpecM VoidEv emptyFunStack
+                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+noErrorsContains0H =
+  multiArgFixS VoidEv emptyFunStack noErrorsContains0LRT
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
-       f len_top i_top v_top);
+            SpecM VoidEv (pushFunStack (singletonFrame noErrorsContains0LRT) emptyFunStack)
+                         (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+       (\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
+          invariantHint
+            (SpecM VoidEv (pushFunStack (singletonFrame noErrorsContains0LRT) emptyFunStack)
+                          (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
+            (and (bvsle 64 0x0000000000000000 i)
+                 (bvsle 64 i 0x0fffffffffffffff))
+            (orS VoidEv (pushFunStack (singletonFrame noErrorsContains0LRT) emptyFunStack)
+                 (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                 (existsS VoidEv (pushFunStack (singletonFrame noErrorsContains0LRT) emptyFunStack)
+                          (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
+                 (f len (bvAdd 64 i 0x0000000000000001) v))));
 
 -- The specification that contains0 has no errors
 noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
-                    CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+                    SpecM VoidEv emptyFunStack
+                          (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
 noErrorsContains0 len v =
   noErrorsContains0H len 0x0000000000000000 v;

heapster-saw/examples/arrays_mr_solver.saw

@@ -11,6 +11,9 @@ prove_extcore mrsolver (refines [] contains0 noErrorsContains0);
 include "specPrims.saw";
 import "arrays.cry";
 
-zero_array <- parse_core_mod "arrays" "zero_array";
-prove_extcore mrsolver (refines [] zero_array {{ zero_array_loop_spec }});
-prove_extcore mrsolver (refines [] zero_array {{ zero_array_spec }});
+monadify_term {{ zero_array_spec }};
+
+// FIXME: Uncomment once FunStacks are removed
+// zero_array <- parse_core_mod "arrays" "zero_array";
+// prove_extcore mrsolver (refines [] zero_array {{ zero_array_loop_spec }});
+// prove_extcore mrsolver (refines [] zero_array {{ zero_array_spec }});

heapster-saw/examples/specPrims.saw

@@ -2,9 +2,8 @@
 
 import "SpecPrims.cry";
 
-set_monadification "exists" "Prelude.existsM";
-set_monadification "forall" "Prelude.forallM";
-set_monadification "anySpec" "Prelude.anySpec";
-set_monadification "asserting" "Prelude.asserting";
-set_monadification "assuming" "Prelude.assuming";
-set_monadification "invariantHint" "Prelude.invariantHint";
+set_monadification "exists" "Prelude.existsS" true;
+set_monadification "forall" "Prelude.forallS" true;
+set_monadification "asserting" "Prelude.asserting" true;
+set_monadification "assuming" "Prelude.assuming" true;
+set_monadification "invariantHint" "Prelude.invariantHint" true;

src/SAWScript/Prover/MRSolver/Monad.hs

@@ -546,10 +546,6 @@ liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e)
 -- * Functions for Building Terms
 ----------------------------------------------------------------------
 
--- | Create a term representing the type @IsFinite n@
-mrIsFinite :: Term -> MRM t Term
-mrIsFinite n = liftSC2 scGlobalApply "CryptolM.isFinite" [n]
-
 -- | Create a term representing an application of @Prelude.error@
 mrErrorTerm :: Term -> T.Text -> MRM t Term
 mrErrorTerm a str =
@@ -1094,7 +1090,8 @@ mrGetFunAssump nm = lookupFunAssump nm <$> mrRefnset
 withFunAssump :: FunName -> [Term] -> Term -> MRM t a -> MRM t a
 withFunAssump fname args rhs m =
   do k <- mkCompFunReturn <$> mrFunOutType fname args
-     mrDebugPPPrefixSep 1 "withFunAssump" (FunBind fname args k) "|=" rhs
+     mrDebugPPPrefixSep 1 "withFunAssump" (FunBind fname args Unlifted k)
+                                     "|=" rhs
      ctx <- mrUVars
      rs <- mrRefnset
      let assump = FunAssump ctx fname args (RewriteFunAssump rhs) Nothing