Incorporate crucible fancy assumptions

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -599,6 +599,8 @@ instance TransInfo info =>
       return $ error "translate: RealValRepr"
     [nuMP| ComplexRealRepr |] ->
       return $ error "translate: ComplexRealRepr"
+    [nuMP| SequenceRepr{} |] ->
+      return $ error "translate: SequenceRepr"
     [nuMP| BVRepr w |] ->
       returnType1 =<< bitvectorTransM (translate w)
 

heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs

@@ -331,6 +331,7 @@ tcExpr WordMapRepr       {} e = tcError (pos e) "Expected wordmap"
 tcExpr StringMapRepr     {} e = tcError (pos e) "Expected stringmap"
 tcExpr SymbolicArrayRepr {} e = tcError (pos e) "Expected symbolicarray"
 tcExpr SymbolicStructRepr{} e = tcError (pos e) "Expected symbolicstruct"
+tcExpr SequenceRepr      {} e = tcError (pos e) "Expected sequencerepr"
 
 -- | Check for a unit literal
 tcUnit :: AstExpr -> Tc (PermExpr UnitType)

src/SAWScript/Crucible/Common.hs

@@ -58,7 +58,7 @@ sawCoreState sym = pure (onlineUserState (W4.sbUserState sym))
 ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann)
                 -> AbortedResult Sym ext
                 -> PP.Doc ann
-ppAbortedResult _ (AbortedExec InfeasibleBranch _) =
+ppAbortedResult _ (AbortedExec InfeasibleBranch{} _) =
   PP.pretty "Infeasible branch"
 ppAbortedResult ppGP (AbortedExec abt gp) = do
   PP.vcat

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -59,7 +59,6 @@ import qualified Data.Map as Map
 import           Data.Maybe (fromMaybe, isNothing)
 import           Data.Set (Set)
 import qualified Data.Set as Set
-import qualified Data.Sequence as Seq
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.Time.Clock (getCurrentTime, diffUTCTime)
@@ -132,6 +131,7 @@ import SAWScript.Crucible.JVM.Override
 import SAWScript.Crucible.JVM.ResolveSetupValue
 import SAWScript.Crucible.JVM.BuiltinsJVM ()
 
+type AssumptionReason = (W4.ProgramLoc, String)
 type SetupValue = MS.SetupValue CJ.JVM
 type Lemma = MS.ProvedSpec CJ.JVM
 type MethodSpec = MS.CrucibleMethodSpecIR CJ.JVM
@@ -276,7 +276,7 @@ verifyObligations ::
   JVMCrucibleContext ->
   MethodSpec ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   [(String, W4.ProgramLoc, Term)] ->
   TopLevel (SolverStats, Set TheoremNonce)
 verifyObligations cc mspec tactic assumes asserts =
@@ -333,7 +333,7 @@ verifyPrestate ::
   MethodSpec ->
   Crucible.SymGlobalState Sym ->
   IO ([(J.Type, JVMVal)],
-      [Crucible.LabeledPred Term Crucible.AssumptionReason],
+      [Crucible.LabeledPred Term AssumptionReason],
       Map AllocIndex JVMRefVal,
       Crucible.SymGlobalState Sym)
 verifyPrestate cc mspec globals0 =
@@ -511,7 +511,7 @@ setupPrestateConditions ::
   JVMCrucibleContext ->
   Map AllocIndex JVMRefVal ->
   [SetupCondition] ->
-  IO [Crucible.LabeledPred Term Crucible.AssumptionReason]
+  IO [Crucible.LabeledPred Term AssumptionReason]
 setupPrestateConditions mspec cc env = aux []
   where
     tyenv   = MS.csAllocations mspec
@@ -523,11 +523,11 @@ setupPrestateConditions mspec cc env = aux []
       do val1' <- resolveSetupVal cc env tyenv nameEnv val1
          val2' <- resolveSetupVal cc env tyenv nameEnv val2
          t     <- assertEqualVals cc val1' val2'
-         let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition")
+         let lp = Crucible.LabeledPred t (loc, "equality precondition")
          aux (lp:acc) xs
 
     aux acc (MS.SetupCond_Pred loc tm : xs) =
-      let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in
+      let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in
       aux (lp:acc) xs
 
     aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_
@@ -593,7 +593,7 @@ verifySimulate ::
   [Crucible.GenericExecutionFeature Sym] ->
   MethodSpec ->
   [(a, JVMVal)] ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   W4.ProgramLoc ->
   [Lemma] ->
   Crucible.SymGlobalState Sym ->
@@ -630,9 +630,10 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat =
                    mapM_ (registerOverride opts cc simctx top_loc)
                            (groupOn (view csMethodName) (map (view MS.psSpec) lemmas))
                    liftIO $ putStrLn "registering assumptions"
-                   liftIO $ do
-                     preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes
-                     Crucible.addAssumptions sym (Seq.fromList preds)
+                   liftIO $
+                     for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) ->
+                       do expr <- resolveSAWPred cc p
+                          Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr)
                    liftIO $ putStrLn "simulating function"
                    fnCall
           Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats)
@@ -731,14 +732,14 @@ verifyPoststate cc mspec env0 globals ret =
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
-     io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations)
+     io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations)
 
   where
     sym = cc^.jccBackend
 
     verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) =
       do st         <- sawCoreState sym
-         hypTerm    <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps)
+         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
          conclTerm  <- toSC sym st concl
          obligation <- scImplies sc hypTerm conclTerm
          return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, loc, obligation)

src/SAWScript/Crucible/JVM/Override.hs

@@ -243,13 +243,15 @@ methodSpecHandler opts sc cc top_loc css h = do
                 case res of
                   Left (OF loc rsn)  ->
                     -- TODO, better pretty printing for reasons
-                    liftIO $ Crucible.abortExecBecause
-                      (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn)))
+                    liftIO
+                      $ Crucible.abortExecBecause
+                      $ Crucible.AssertionFailure
+                      $ Crucible.SimError loc
+                      $ Crucible.AssertFailureSimError "assumed false" (show rsn)
                   Right (ret,st') ->
                     do liftIO $ forM_ (st'^.osAssumes) $ \asum ->
                          Crucible.addAssumption (cc ^. jccBackend)
-                            (Crucible.LabeledPred asum
-                              (Crucible.AssumptionReason (st^.osLocation) "override postcondition"))
+                          $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
                        Crucible.writeGlobals (st'^.overrideGlobals)
                        Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
            , Just (W4.plSourceLoc (cs ^. MS.csLoc))

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -198,6 +198,8 @@ import SAWScript.Crucible.LLVM.Override
 import SAWScript.Crucible.LLVM.ResolveSetupValue
 import SAWScript.Crucible.LLVM.MethodSpecIR
 
+type AssumptionReason = (W4.ProgramLoc, String)
+
 type MemImpl = Crucible.MemImpl Sym
 
 data LLVMVerificationException
@@ -603,7 +605,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
 verifyObligations :: LLVMCrucibleContext arch
                   -> MS.CrucibleMethodSpecIR (LLVM arch)
                   -> ProofScript ()
-                  -> [Crucible.LabeledPred Term Crucible.AssumptionReason]
+                  -> [Crucible.LabeledPred Term AssumptionReason]
                   -> [(String, W4.ProgramLoc, Term)]
                   -> TopLevel (SolverStats, Set TheoremNonce)
 verifyObligations cc mspec tactic assumes asserts =
@@ -738,7 +740,7 @@ verifyPrestate ::
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   Crucible.SymGlobalState Sym ->
   IO ([(Crucible.MemType, LLVMVal)],
-      [Crucible.LabeledPred Term Crucible.AssumptionReason],
+      [Crucible.LabeledPred Term AssumptionReason],
       Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)),
       Crucible.SymGlobalState Sym)
 verifyPrestate opts cc mspec globals =
@@ -772,7 +774,7 @@ assumptionsContainContradiction ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel Bool
 assumptionsContainContradiction cc tactic assumptions =
   do
@@ -803,7 +805,7 @@ computeMinimalContradictingCore ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel ()
 computeMinimalContradictingCore cc tactic assumes =
   do
@@ -814,8 +816,9 @@ computeMinimalContradictingCore cc tactic assumes =
      findM (assumptionsContainContradiction cc tactic) cores >>= \case
       Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
       Just core ->
-        forM_ core $ \ assumption ->
-          printOutLnTop Warn (show . Crucible.ppAssumptionReason $ assumption ^. Crucible.labeledPredMsg)
+        forM_ core $ \assume ->
+          case assume^.Crucible.labeledPredMsg of
+            (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
      printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."
 
 -- | Checks whether the given list of assumptions contains a contradiction, and
@@ -824,7 +827,7 @@ checkAssumptionsForContradictions ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
   LLVMCrucibleContext arch ->
   ProofScript () ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   TopLevel ()
 checkAssumptionsForContradictions cc tactic assumes =
   whenM
@@ -953,7 +956,7 @@ setupPrestateConditions ::
   Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) ->
   Crucible.SymGlobalState Sym ->
   [MS.SetupCondition (LLVM arch)]            ->
-  IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term Crucible.AssumptionReason])
+  IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason])
 setupPrestateConditions mspec cc mem env = aux []
   where
     tyenv   = MS.csAllocations mspec
@@ -965,11 +968,11 @@ setupPrestateConditions mspec cc mem env = aux []
       do val1' <- resolveSetupVal cc mem env tyenv nameEnv val1
          val2' <- resolveSetupVal cc mem env tyenv nameEnv val2
          t     <- assertEqualVals cc val1' val2'
-         let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition")
+         let lp = Crucible.LabeledPred t (loc, "equality precondition")
          aux (lp:acc) globals xs
 
     aux acc globals (MS.SetupCond_Pred loc tm : xs) =
-      let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in
+      let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in
       aux (lp:acc) globals xs
 
     aux acc globals (MS.SetupCond_Ghost () _loc var val : xs) =
@@ -1155,7 +1158,7 @@ verifySimulate ::
   [Crucible.GenericExecutionFeature Sym] ->
   MS.CrucibleMethodSpecIR (LLVM arch) ->
   [(Crucible.MemType, LLVMVal)] ->
-  [Crucible.LabeledPred Term Crucible.AssumptionReason] ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
   W4.ProgramLoc ->
   [MS.ProvedSpec (LLVM arch)] ->
   Crucible.SymGlobalState Sym ->
@@ -1209,8 +1212,9 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as
            do mapM_ (registerOverride opts cc simCtx top_loc)
                     (groupOn (view csName) funcLemmas)
               liftIO $
-                do preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes
-                   Crucible.addAssumptions sym (Seq.fromList preds)
+                for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) ->
+                  do expr <- resolveSAWPred cc p
+                     Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr)
               Crucible.regValue <$> (Crucible.callBlock cfg entryId args')
      res <- Crucible.executeCrucible execFeatures initExecState
      case res of
@@ -1302,15 +1306,15 @@ verifyPoststate cc mspec env0 globals ret =
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
-     sc_obligations <- io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations)
+     sc_obligations <- io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations)
      return (sc_obligations, st)
 
   where
     sym = cc^.ccBackend
 
     verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) =
       do st <- Common.sawCoreState sym
-         hypTerm <- toSC sym st =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps
+         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
          conclTerm  <- toSC sym st concl
          obligation <- scImplies sc hypTerm conclTerm
          return (unlines ["safety assertion:", show err], loc, obligation)

src/SAWScript/Crucible/LLVM/Override.hs

@@ -475,13 +475,15 @@ methodSpecHandler opts sc cc top_loc css h = do
                 case res of
                   Left (OF loc rsn)  ->
                     -- TODO, better pretty printing for reasons
-                    liftIO $ Crucible.abortExecBecause
-                      (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn)))
+                    liftIO
+                      $ Crucible.abortExecBecause
+                      $ Crucible.AssertionFailure
+                      $ Crucible.SimError loc
+                      $ Crucible.AssertFailureSimError "assumed false" (show rsn)
                   Right (ret,st') ->
                     do liftIO $ forM_ (st'^.osAssumes) $ \asum ->
                          Crucible.addAssumption (cc^.ccBackend)
-                            (Crucible.LabeledPred asum
-                              (Crucible.AssumptionReason (st^.osLocation) "override postcondition"))
+                          $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum
                        Crucible.writeGlobals (st'^.overrideGlobals)
                        Crucible.overrideReturn' (Crucible.RegEntry retTy ret)
            , Just (W4.plSourceLoc (cs ^. MS.csLoc))

src/SAWScript/Crucible/LLVM/X86.hs

@@ -914,8 +914,8 @@ assertPost globals env premem preregs = do
   st <- case result of
     Left err -> throwX86 $ show err
     Right (_, st) -> pure st
-  liftIO . forM_ (view O.osAssumes st) $ \p ->
-    C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition"
+  liftIO . forM_ (view O.osAssumes st) $
+    C.addAssumption sym . C.GenericAssumption (st ^. O.osLocation) "precondition"
   liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) ->
     C.addAssertion sym $ C.LabeledPred p r
 

src/SAWScript/X86.hs

@@ -27,7 +27,7 @@ module SAWScript.X86
   ) where
 
 
-import Control.Lens (toListOf, folded, (^.))
+import Control.Lens ((^.))
 import Control.Exception(Exception(..),throwIO)
 import Control.Monad.IO.Class(liftIO)
 
@@ -72,7 +72,8 @@ import Lang.Crucible.Simulator.ExecutionTree
           )
 import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason)
 import Lang.Crucible.Backend
-          (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,proofGoalsToList)
+          (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,goalsToList
+          ,assumptionsPred)
 import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHandleMap,emptyHandleMap)
 
 
@@ -564,15 +565,15 @@ gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g)
 
 getGoals :: Sym -> IO [Goal]
 getGoals sym =
-  do obls <- proofGoalsToList <$> getProofObligations sym
+  do obls <- maybe [] goalsToList <$> getProofObligations sym
      st <- sawCoreState sym
      mapM (toGoal st) obls
   where
   toGoal st (ProofGoal asmps g) =
-    do as <- mapM (toSC sym st) (toListOf (folded . labeledPred) asmps)
+    do a1 <- toSC sym st =<< assumptionsPred sym asmps
        p  <- toSC sym st (g ^. labeledPred)
        let SimError loc msg = g^.labeledPredMsg
-       return Goal { gAssumes = as
+       return Goal { gAssumes = [a1]
                    , gShows   = p
                    , gLoc     = loc
                    , gMessage = msg

src/SAWScript/X86Spec.hs

@@ -103,8 +103,8 @@ import qualified Lang.Crucible.LLVM.MemModel as Crucible
 
 import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError))
 import Lang.Crucible.Backend
-          (addAssumption, getProofObligations, proofGoalsToList
-          ,assert, AssumptionReason(..)
+          (addAssumption, getProofObligations, goalsToList
+          ,assert, CrucibleAssumption(..)
           ,LabeledPred(..), ProofGoal(..), labeledPredMsg)
 
 import Lang.Crucible.Simulator.ExecutionTree
@@ -826,7 +826,8 @@ makeEquiv opts s (Pair (Rep t _) (Equiv xs ys)) =
      let same a =
            do p <- evalSame sym t v a
               let loc = mkProgramLoc "<makeEquiv>" InternalPos
-              addAssumption sym (LabeledPred p (AssumptionReason loc "equivalance class assumption"))
+              addAssumption sym
+                $ GenericAssumption loc "equivalance class assumption" p
 
      mapM_ same rest
 
@@ -847,7 +848,7 @@ addAsmp opts s (msg,p) =
 
     _ -> do p' <- evalProp opts p s
             let loc = mkProgramLoc "<addAssmp>" InternalPos -- FIXME
-            addAssumption (optsSym opts) (LabeledPred p' (AssumptionReason loc msg))
+            addAssumption (optsSym opts) (GenericAssumption loc msg p')
 
 setCryPost :: forall p. (Eval p, Crucible.HasLLVMAnn Sym) => Opts -> S p -> (String,Prop p) -> IO (S p)
 setCryPost opts s (_nm,p) =
@@ -1132,7 +1133,7 @@ debugPPReg r s =
 
 _debugDumpGoals :: Sym -> IO ()
 _debugDumpGoals sym =
-  do obls <- proofGoalsToList <$> getProofObligations sym
+  do obls <- maybe [] goalsToList <$> getProofObligations sym
      mapM_ sh (toList obls)
   where
   sh (ProofGoal _hyps g) = print (view labeledPredMsg g)