Fancy assumptions

crucible-concurrency/crucibles/Main.hs

@@ -9,10 +9,6 @@
 {-# LANGUAGE ImplicitParams #-}
 module Main where
 
-import qualified Data.Text.IO as T
-import qualified Options.Applicative.Simple as Opts
-import           System.IO
-
 import qualified Crux
 import Cruces.CrucesMain
 import Paths_crucible_concurrency (version)

crucible-concurrency/src/Cruces/CrucesMain.hs

@@ -153,7 +153,5 @@ run (cruxOpts, opts) =
 
             return ()
 
-printCounterexamples :: Crux.Logs
-                     => ProvedGoals (Either AssumptionReason SimError)
-                     -> IO ()
+printCounterexamples :: Crux.Logs => ProvedGoals -> IO ()
 printCounterexamples = Crux.logGoal

crucible-concurrency/src/Cruces/ExploreCrux.hs

@@ -29,7 +29,6 @@ import           Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import           Lang.Crucible.Backend
 
 import qualified Crux
-import           Crux.Model
 
 import           Crucibles.SchedulingAlgorithm hiding (_exec, exec)
 import           Crucibles.Execution
@@ -73,7 +72,6 @@ emptyExploration :: SchedulingAlgorithm alg => Exploration alg ext C.UnitType sy
 emptyExploration = Exploration { _exec      = initialExecutions
                                , _scheduler = s0
                                , _schedAlg  = initialAlgState
-                               , _model     = emptyModel
                                , _num       = 0
                                , _gVars     = mempty
                                }

crucible-concurrency/src/Crucibles/Explore.hs

@@ -129,16 +129,10 @@ schedule prims globs = \case
   -- we might have conservatively added this thread to a backtracking list even
   -- though it wasn't actually runnable. In any case, restart the computation
   -- using the mainCont continuation.
-  ResultState (AbortedResult ctx (AbortedExec rsn gps))
-    | InfeasibleBranch <- rsn ->
-      return $ ExecutionFeatureNewState s0
-    | AssumedFalse _   <- rsn ->
-      return $ ExecutionFeatureNewState s0
-    | otherwise               -> return ExecutionFeatureNoChange
+  ResultState (AbortedResult ctx (AbortedExec _rsn _gps)) -> return (ExecutionFeatureNewState s0)
     where
       k  = ctx ^. cruciblePersonality.scheduler.to mainCont
       t  = ctx ^. cruciblePersonality.scheduler.retRepr
-      globVars = gps ^. gpGlobals
       s0 = InitialState ctx emptyGlobals defaultAbortHandler t $ runOverrideSim t k
 
   -- TODO: I don't think this is reachable anymore, but this needs to be
@@ -521,7 +515,7 @@ restoreBranchingThread tID dir branchPred stk tframe fframe =
                             then (tframe, return branchPred)
                             else (fframe, notPred sym branchPred)
      assmPred <- liftIO assm
-     liftIO $ addAssumption sym (LabeledPred assmPred (ExploringAPath loc (pausedLoc frame)))
+     liftIO $ addAssumption sym (BranchCondition loc (pausedLoc frame) assmPred)
      s <- get
      case frame of
        PausedFrame frm cont l ->
@@ -536,7 +530,9 @@ abortInfeasible ::
   ThreadExecM alg sym ext ret rtp f a (ExecState (ThreadExec alg sym ext ret) sym ext rtp)
 abortInfeasible =
   do s <- get
-     liftIO $ runReaderT (abortExec InfeasibleBranch) s
+     sym <- use (stateContext.ctxSymInterface)
+     loc <- liftIO $ getCurrentProgramLoc sym
+     liftIO $ runReaderT (abortExec (InfeasibleBranch loc)) s
 
 returnFinishedResult ::
   ( SchedulerConstraints sym ext alg
@@ -559,7 +555,7 @@ returnFinishedResult mres =
             s <- get
             liftIO $
               do putStrLn "<deadlock>"
-                 runReaderT (abortExec (AssumedFalse $ AssumingNoError simerr)) s
+                 runReaderT (abortExec (AssertionFailure simerr)) s
 
 -- | ThreadState helpers
 

crucible-concurrency/src/Crucibles/ExploreTypes.hs

@@ -15,7 +15,6 @@ import Data.Map.Strict
 import Data.Parameterized (Some(..))
 
 import Lang.Crucible.Simulator
-import Crux.Types (Model, HasModel(..))
 
 import Crucibles.Scheduler
 import Crucibles.Execution
@@ -45,18 +44,13 @@ data Exploration alg ext ret sym = Exploration
     -- ^ State of each thread
   , _schedAlg  :: !alg
     -- ^ State required by the scheduling algorithm
-  , _model     :: !(Model sym)
-    -- ^ For use by Crux
   , _num       :: !Int
     -- ^ Number of executions explored
   , _gVars     :: !(Map Text (Some GlobalVar))
     -- ^ Map from name to GlobalVars that the exploration has invented. Typically these are locks.
   }
 makeLenses ''Exploration
 
-instance HasModel (Exploration alg ext ret) where
-  personalityModel = model
-
 stateExpl :: Simple Lens (SimState (ThreadExec alg sym ext ret) sym ext r f a) (ThreadExec alg sym ext ret)
 stateExpl = stateContext.cruciblePersonality
 

crucible-go/src/Lang/Crucible/Go/Overrides.hs

@@ -99,8 +99,7 @@ do_assume = do
   sym <- C.getSymInterface
   RegMap (Empty :> mgs :> file :> b) <- C.getOverrideArgs
   loc <- liftIO $ W4.getCurrentProgramLoc sym
-  liftIO $ addAssumption sym (LabeledPred (regValue b) $
-                              AssumptionReason loc "assume")
+  liftIO $ addAssumption sym (GenericAssumption loc "assume" (regValue b))
   return Ctx.empty
 
 do_assert :: IsSymInterface sym

crucible-jvm/tool/Main.hs

@@ -92,7 +92,7 @@ import           Paths_crucible_jvm (version)
 import System.Console.GetOpt
 
 -- | A simulator context
-type SimCtxt sym = SimContext (Crux.Model sym) sym JVM
+type SimCtxt sym = SimContext (Crux.Crux sym) sym JVM
 
 data JVMOptions = JVMOptions
   { classPath        :: [FilePath]
@@ -193,7 +193,7 @@ simulateJVM copts opts = Crux.SimulatorCallback $ \sym _maybeOnline -> do
    let nullstr = RegEntry refRepr W4.Unassigned
    let regmap = RegMap (Ctx.Empty `Ctx.extend` nullstr)
 
-   initSt <- setupCrucibleJVMCrux @UnitType cb verbosity sym Crux.emptyModel
+   initSt <- setupCrucibleJVMCrux @UnitType cb verbosity sym Crux.CruxPersonality
      cname mname regmap
 
    return (Crux.RunnableState initSt, \_ _ -> return mempty) -- TODO add failure explanations

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -441,7 +441,7 @@ evalStmt sym = eval
                 loc <- getCurrentProgramLoc sym
                 let err = SimError loc (AssertFailureSimError "Failed to load function handle" (show doc))
                 addProofObligation sym (LabeledPred p err)
-                abortExecBecause $ AssumedFalse $ AssumingNoError err
+                abortExecBecause (AssertionFailure err)
 
            Right (VarargsFnHandle h) ->
              let err = failedAssert "Failed to load function handle"
@@ -1195,15 +1195,13 @@ mergeWriteOperations sym mem cond true_write_op false_write_op = do
   loc <- getCurrentProgramLoc sym
 
   true_frame_id <- pushAssumptionFrame sym
-  addAssumption sym $ LabeledPred cond $
-    AssumptionReason loc "conditional memory write predicate"
+  addAssumption sym (GenericAssumption loc "conditional memory write predicate" cond)
   true_mutated_heap <- memImplHeap <$> true_write_op branched_mem
   _ <- popAssumptionFrame sym true_frame_id
 
   false_frame_id <- pushAssumptionFrame sym
   not_cond <- notPred sym cond
-  addAssumption sym $ LabeledPred not_cond $
-    AssumptionReason loc "conditional memory write predicate"
+  addAssumption sym (GenericAssumption loc "conditional memory write predicate" not_cond)
   false_mutated_heap <- memImplHeap <$> false_write_op branched_mem
   _ <- popAssumptionFrame sym false_frame_id
 

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -332,7 +332,7 @@ assertSafe sym (Err p) = do
      loc <- getCurrentProgramLoc sym
      let err = SimError loc rsn
      addProofObligation sym (LabeledPred p err)
-     abortExecBecause $ AssumedFalse $ AssumingNoError err
+     abortExecBecause (AssertionFailure err)
 
 
 ------------------------------------------------------------------------

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs

@@ -68,7 +68,6 @@ import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.Translation.Types
 import           Lang.Crucible.LLVM.TypeContext
 
-import           Lang.Crucible.FunctionHandle
 import           Lang.Crucible.Types
 
 ------------------------------------------------------------------------

crucible-llvm/test/TestMemory.hs

@@ -73,8 +73,7 @@ userSymbol' s = case What4.userSymbol s of
 assume :: CB.IsSymInterface sym => sym -> What4.Pred sym -> IO ()
 assume sym p = do
   loc <- What4.getCurrentProgramLoc sym
-  CB.addAssumption sym $
-    CB.LabeledPred p $ CB.AssumptionReason loc ""
+  CB.addAssumption sym (CB.GenericAssumption loc "assume" p)
 
 checkSat ::
   W4O.OnlineSolver solver =>

crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs

@@ -12,7 +12,6 @@ module Lang.Crucible.Syntax.Overrides
 import Control.Lens hiding ((:>), Empty)
 import Control.Monad (forM_)
 import Control.Monad.IO.Class
-import Data.Foldable(toList)
 import System.IO
 
 import Data.Parameterized.Context hiding (view)
@@ -48,15 +47,15 @@ proveObligations =
      liftIO $ do
        hPutStrLn h "Attempting to prove all outstanding obligations!\n"
 
-       obls <- proofGoalsToList <$> getProofObligations sym
+       obls <- maybe [] goalsToList <$> getProofObligations sym
        clearProofObligations sym
 
        forM_ obls $ \o ->
-         do let asms = map (view labeledPred) $ toList $ proofAssumptions o
-            gl <- notPred sym ((proofGoal o)^.labeledPred)
+         do asms <- assumptionsPred sym (proofAssumptions o)
+            gl <- notPred sym (o ^. to proofGoal.labeledPred)
             let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
                                          , logReason = "assertion proof" }
-            runZ3InOverride sym logData (asms ++ [gl]) $ \case
+            runZ3InOverride sym logData [asms,gl] $ \case
               Unsat{}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
               Sat _mdl -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
               Unknown  -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]

crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs

@@ -8,11 +8,9 @@ module Lang.Crucible.Syntax.Prog where
 import Control.Lens (view)
 import Control.Monad
 
-import Data.Foldable (toList)
 import Data.List (find)
 import Data.Text (Text)
 import Data.String (IsString(..))
---import qualified Data.Text as T
 import qualified Data.Text.IO as T
 import System.IO
 import System.Exit
@@ -33,7 +31,6 @@ import Lang.Crucible.Syntax.Atoms
 
 import Lang.Crucible.Analysis.Postdom
 import Lang.Crucible.Backend
-import Lang.Crucible.Backend.ProofGoals
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
@@ -136,9 +133,10 @@ simulateProgram fn theInput outh profh opts setup =
                          Just gs ->
                            do hPutStrLn outh "==== Proof obligations ===="
                               forM_ (goalsToList gs) (\g ->
-                                do hPrint outh (ppProofObligation sym g)
+                                do hPrint outh =<< ppProofObligation sym g
                                    neggoal <- notPred sym (view labeledPred (proofGoal g))
-                                   let bs = neggoal : map (view labeledPred) (toList (proofAssumptions g))
+                                   asms <- assumptionsPred sym (proofAssumptions g)
+                                   let bs = [neggoal, asms]
                                    runZ3InOverride sym defaultLogData bs (\case
                                      Sat _   -> hPutStrLn outh "COUNTEREXAMPLE"
                                      Unsat _ -> hPutStrLn outh "PROVED"

crucible-syntax/test-data/simulator-tests/override-test2.out.good

@@ -16,9 +16,9 @@ Prove:
 COUNTEREXAMPLE
 Assuming:
 * The branch in symbolicBranchesTest from after branch 1 to third branch
-    let -- default branch
-        v26 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i))
-     in not v26
+    let -- test-data/simulator-tests/override-test2.cbl:7:5
+        v30 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i))
+     in not v30
 Prove:
   test-data/simulator-tests/override-test2.cbl:6:5: error: in main
   bogus!

crucible-syntax/test-data/simulator-tests/seq-test3.out.good

@@ -2,49 +2,49 @@
 
 ==== Finish Simulation ====
 ==== Proof obligations ====
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!
   eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!
   eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:56:5: error: in main
   head 1 eq check
   eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:57:5: error: in main
   head 1 check
   eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!
   eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!
   eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!
   eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i)
 PROVED
-Assuming:
+
 Prove:
   test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq
   value mismatch!

crucible-wasm/tool/Main.hs

@@ -14,8 +14,6 @@ import Lang.Crucible.Simulator
 import Lang.Crucible.FunctionHandle
 
 import qualified Crux
-import qualified Crux.Model as Crux
-import qualified Crux.Types as Crux
 
 import qualified Language.Wasm as Wasm
 
@@ -35,13 +33,13 @@ cruxWasmConfig = Crux.Config
   }
 
 setupWasmState :: IsSymInterface sym =>
-  sym -> Wasm.Script -> IO (ExecState (Crux.Model sym) sym WasmExt (RegEntry sym UnitType))
+  sym -> Wasm.Script -> IO (ExecState (Crux.Crux sym) sym WasmExt (RegEntry sym UnitType))
 setupWasmState sym s =
   do halloc <- newHandleAllocator
 
      let globals = emptyGlobals
      let bindings = emptyHandleMap
-     let simctx = initSimContext sym wasmIntrinsicTypes halloc stdout (FnBindings bindings) extImpl Crux.emptyModel
+     let simctx = initSimContext sym wasmIntrinsicTypes halloc stdout (FnBindings bindings) extImpl Crux.CruxPersonality
      let m = execScript s emptyScriptState >> pure ()
 
      pure (InitialState simctx globals defaultAbortHandler knownRepr (runOverrideSim knownRepr m))

crucible/crucible.cabal

@@ -106,6 +106,7 @@ library
     Lang.Crucible.Simulator.OverrideSim
     Lang.Crucible.Simulator.PathSatisfiability
     Lang.Crucible.Simulator.PathSplitting
+    Lang.Crucible.Simulator.PositionTracking
     Lang.Crucible.Simulator.Profiling
     Lang.Crucible.Simulator.RegMap
     Lang.Crucible.Simulator.RegValue