Fix crux-mir-comp build and add to CI

.github/ci.sh

@@ -58,9 +58,9 @@ build() {
   cabal v2-configure -j --enable-tests
   git status --porcelain
   if $IS_WIN; then
-    pkgs=(saw)
+    pkgs=(saw crux-mir-comp)
   else
-    pkgs=(saw saw-remote-api)
+    pkgs=(saw crux-mir-comp saw-remote-api)
   fi
   tee -a cabal.project.local > /dev/null < cabal.project.ci
   if ! retry cabal v2-build "$@" "${pkgs[@]}"; then

crux-mir-comp/crux-mir-comp.cabal

@@ -81,7 +81,7 @@ executable crux-mir-comp
                 crux-mir,
                 template-haskell
 
-  ghc-options: -Wall
+  ghc-options: -Wall -threaded
   ghc-prof-options: -O2 -fprof-auto-top
   default-language: Haskell2010
 
@@ -90,7 +90,7 @@ test-suite test
   type: exitcode-stdio-1.0
   hs-source-dirs: test
 
-  ghc-options: -Wall
+  ghc-options: -Wall -threaded
   ghc-prof-options: -fprof-auto -O2
 
   main-is: Test.hs

crux-mir-comp/src/Mir/Compositional.hs

@@ -31,7 +31,7 @@ import Mir.Compositional.Clobber (clobberGlobalsOverride)
 
 compositionalOverrides ::
     forall sym p t st fs args ret blocks rtp a r .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     Maybe (SomeOnlineSolver sym) ->
     CollectionState ->
     Text ->

crux-mir-comp/src/Mir/Compositional/Builder.hs

@@ -31,6 +31,7 @@ import qualified Data.Sequence as Seq
 import Data.Set (Set)
 import qualified Data.Set as Set
 import GHC.Stack (HasCallStack)
+import qualified Prettyprinter as PP
 
 import qualified What4.Expr.Builder as W4
 import What4.FunctionName (functionNameFromText)
@@ -50,8 +51,6 @@ import qualified Verifier.SAW.TypedTerm as SAW
 
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 
-import Crux.Types (HasModel)
-
 import Mir.DefId
 import Mir.Generator (CollectionState, collection)
 import Mir.Intrinsics hiding (MethodSpec, MethodSpecBuilder)
@@ -183,7 +182,7 @@ instance (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
 -- Rust invokes `msb.add_arg(...)` or similar.
 
 builderNew :: forall sym p t st fs rtp.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     CollectionState ->
     -- | `DefId` of the `builder_new` monomorphization.  Its `Instance` should
     -- have one type argument, which is the `TyFnDef` of the function that the
@@ -225,7 +224,7 @@ builderNew cs defId = do
 -- argument.  For example, if `argRef` points to an `&mut i32`, the `i32` will
 -- be overwritten with a fresh symbolic variable.
 addArg :: forall sym p t st fs rtp args ret tp.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     TypeRepr tp -> MirReferenceMux sym tp -> MethodSpecBuilder sym t ->
     OverrideSim (p sym) sym MIR rtp args ret (MethodSpecBuilder sym t)
 addArg tpr argRef msb = execBuilderT msb $ do
@@ -324,8 +323,9 @@ gatherAssumes msb = do
 
     -- Find all assumptions that mention a relevant variable.
     assumes <- liftIO $ collectAssumptions sym
+    flatAssumes <- liftIO $ flattenAssumptions sym assumes
     optAssumes' <- liftIO $ relevantPreds sym vars $
-        map (\a -> (a ^. W4.labeledPred, a ^. W4.labeledPredMsg)) $ toList assumes
+        map (\a -> (assumptionPred a, show $ ppAssumption PP.viaShow a)) $ flatAssumes
     let assumes' = case optAssumes' of
             Left (pred, msg, Some v) ->
                 error $ "assumption `" ++ show pred ++ "` (" ++ show msg ++
@@ -362,7 +362,7 @@ gatherAsserts msb = do
     let vars = (msb ^. msbPre . seVars) `Set.union` (msb ^. msbPost . seVars)
 
     -- Find all assertions that mention a relevant variable.
-    goals <- liftIO $ proofGoalsToList <$> getProofObligations sym
+    goals <- liftIO $ maybe [] goalsToList <$> getProofObligations sym
     let asserts = map proofGoal goals
     optAsserts' <- liftIO $ relevantPreds sym vars $
         map (\a -> (a ^. W4.labeledPred, a ^. W4.labeledPredMsg)) asserts

crux-mir-comp/src/Mir/Compositional/Clobber.hs

@@ -6,7 +6,7 @@
 module Mir.Compositional.Clobber
 where
 
-import Control.Lens ((^.), (^?), (%=), ix)
+import Control.Lens ((^.), (^?), ix)
 import Control.Monad.Except
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
@@ -23,9 +23,6 @@ import Lang.Crucible.Backend
 import Lang.Crucible.Simulator
 import Lang.Crucible.Types
 
-import qualified Crux.Model as Crux
-import Crux.Types (HasModel(..))
-
 import Mir.Generator (CollectionState, collection, staticMap, StaticVar(..))
 import Mir.Intrinsics hiding (MethodSpec, MethodSpecBuilder)
 import qualified Mir.Mir as M
@@ -39,7 +36,7 @@ import Mir.Compositional.Convert
 
 -- | Replace each primitive value within `rv` with a fresh symbolic variable.
 clobberSymbolic :: forall sym p t st fs tp rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
     sym -> ProgramLoc -> String -> TypeShape tp -> RegValue sym tp ->
     OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp)
 clobberSymbolic sym loc nameStr shp rv = go shp rv
@@ -76,7 +73,7 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv
 -- immutable (`&`) access.  So this function modifies only the portions of `rv`
 -- that lie within an `UnsafeCell` and leaves the rest unchanged.
 clobberImmutSymbolic :: forall sym p t st fs tp rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
     sym -> ProgramLoc -> String -> TypeShape tp -> RegValue sym tp ->
     OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp)
 clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
@@ -118,7 +115,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
 
 -- | Construct a fresh symbolic `RegValue` of type `tp`.
 freshSymbolic :: forall sym p t st fs tp rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
     sym -> ProgramLoc -> String -> TypeShape tp ->
     OverrideSim (p sym) sym MIR rtp args ret (RegValue sym tp)
 freshSymbolic sym loc nameStr shp = go shp
@@ -129,7 +126,8 @@ freshSymbolic sym loc nameStr shp = go shp
     go (PrimShape _ btpr) = do
         let nameSymbol = W4.safeSymbol nameStr
         expr <- liftIO $ W4.freshConstant sym nameSymbol btpr
-        stateContext . cruciblePersonality . personalityModel %= Crux.addVar loc nameStr btpr expr
+        let ev = CreateVariableEvent loc nameStr btpr expr
+        liftIO $ addAssumptions sym (singleEvent ev)
         return expr
     go (ArrayShape (M.TyArray _ len) _ shp) =
         MirVector_Vector <$> V.replicateM len (go shp)
@@ -155,7 +153,7 @@ freshSymbolic sym loc nameStr shp = go shp
 -- might write through the old ref before replacing it with a new one.
 
 clobberGlobals :: forall sym p t st fs rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
     sym -> ProgramLoc -> String -> CollectionState ->
     OverrideSim (p sym) sym MIR rtp args ret ()
 clobberGlobals sym loc nameStr cs = do
@@ -173,7 +171,7 @@ clobberGlobals sym loc nameStr cs = do
         writeGlobal gv rv'
 
 clobberGlobalsOverride :: forall sym p t st fs rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p, HasCallStack) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
     CollectionState ->
     OverrideSim (p sym) sym MIR rtp args ret ()
 clobberGlobalsOverride cs = do

crux-mir-comp/src/Mir/Compositional/Override.hs

@@ -37,7 +37,6 @@ import GHC.Stack (HasCallStack)
 
 import qualified What4.Expr.Builder as W4
 import qualified What4.Interface as W4
-import qualified What4.LabeledPred as W4
 import qualified What4.Partial as W4
 import What4.ProgramLoc
 
@@ -55,9 +54,6 @@ import qualified Verifier.SAW.TypedTerm as SAW
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import qualified SAWScript.Crucible.Common.Override as MS
 
-import qualified Crux.Model as Crux
-import Crux.Types (HasModel(..))
-
 import Mir.Generator
 import Mir.Intrinsics hiding (MethodSpec)
 import qualified Mir.Mir as M
@@ -68,7 +64,6 @@ import Mir.Compositional.MethodSpec
 
 
 type MirOverrideMatcher sym a = forall p rorw rtp args ret.
-    HasModel p =>
     MS.OverrideMatcher' sym MIR rorw (OverrideSim (p sym) sym MIR rtp args ret) a
 
 data MethodSpec = MethodSpec 
@@ -86,7 +81,7 @@ instance (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) => MethodSpecImpl sy
 -- | Pretty-print a MethodSpec.  This wraps `ppMethodSpec` and returns the
 -- result as a Rust string.
 printSpec ::
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     MethodSpec ->
     OverrideSim (p sym) sym MIR rtp args ret (RegValue sym (MirSlice (BVType 8)))
 printSpec ms = do
@@ -109,7 +104,7 @@ printSpec ms = do
 -- the current test, calls to the subject function will be replaced with
 -- `runSpec`.
 enable ::
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     MethodSpec ->
     OverrideSim (p sym) sym MIR rtp args ret ()
 enable ms = do
@@ -129,7 +124,7 @@ enable ms = do
 -- | "Run" a MethodSpec: assert its preconditions, create fresh symbolic
 -- variables for its outputs, and assert its postconditions.
 runSpec :: forall sym p t st fs args ret rtp.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     CollectionState -> FnHandle args ret -> MIRMethodSpec ->
     OverrideSim (p sym) sym MIR rtp args ret (RegValue sym ret)
 runSpec cs mh ms = do
@@ -172,7 +167,8 @@ runSpec cs mh ms = do
         let nameSymbol = W4.safeSymbol nameStr
         Some btpr <- liftIO $ termToType sym sc (SAW.ecType ec)
         expr <- liftIO $ W4.freshConstant sym nameSymbol btpr
-        stateContext . cruciblePersonality . personalityModel %= Crux.addVar loc nameStr btpr expr
+        let ev = CreateVariableEvent loc nameStr btpr expr
+        liftIO $ addAssumptions sym (singleEvent ev)
         term <- liftIO $ eval expr
         return (SAW.ecVarIndex ec, term)
 
@@ -273,8 +269,7 @@ runSpec cs mh ms = do
         liftIO $ addAssertion sym lp
 
     forM_ (os ^. MS.osAssumes) $ \p ->
-        liftIO $ addAssumption sym $ W4.LabeledPred p $
-            AssumptionReason loc "methodspec postcondition"
+        liftIO $ addAssumption sym (GenericAssumption loc "methodspec postcondition" p)
 
     let preAllocMap = os ^. MS.setupValueSub
 

crux-mir-comp/src/Mir/Cryptol.hs

@@ -64,7 +64,7 @@ import Mir.Compositional.Convert
 
 cryptolOverrides ::
     forall sym p t st fs args ret blocks rtp a r .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     Maybe (SomeOnlineSolver sym) ->
     CollectionState ->
     Text ->
@@ -133,7 +133,7 @@ cryptolOverrides _symOnline cs name cfg
 
 cryptolLoad ::
     forall sym p t st fs rtp a r tp .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     M.Collection ->
     M.FnSig ->
     TypeRepr tp ->
@@ -163,7 +163,7 @@ cryptolLoad col sig (FunctionHandleRepr argsCtx retTpr) modulePathStr nameStr =
 cryptolLoad _ _ tpr _ _ = fail $ "cryptol::load: bad function type " ++ show tpr
 
 loadString ::
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     RegValue sym (MirSlice (BVType 8)) ->
     String ->
     OverrideSim (p sym) sym MIR rtp a r Text
@@ -174,7 +174,7 @@ loadString str desc = getString str >>= \x -> case x of
 
 cryptolOverride ::
     forall sym p t st fs rtp a r .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     M.Collection ->
     MirHandle ->
     RegValue sym (MirSlice (BVType 8)) ->
@@ -202,14 +202,14 @@ data LoadedCryptolFunc sym = forall args ret . LoadedCryptolFunc
     { _lcfArgs :: Assignment TypeShape args
     , _lcfRet :: TypeShape ret
     , _lcfRun :: forall p rtp r.
-        HasModel p => OverrideSim (p sym) sym MIR rtp args r (RegValue sym ret)
+        OverrideSim (p sym) sym MIR rtp args r (RegValue sym ret)
     }
 
 -- | Load a Cryptol function, returning an `OverrideSim` action that can be
 -- used to run the function.
 loadCryptolFunc ::
     forall sym p t st fs rtp a r .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     M.Collection ->
     M.FnSig ->
     Text ->
@@ -259,7 +259,7 @@ loadCryptolFunc col sig modulePath name = do
 
 cryptolRun ::
     forall sym p t st fs rtp r args ret .
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasModel p) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     SAW.SharedContext ->
     String ->
     Assignment TypeShape args ->

crux-mir-comp/test/Test.hs

@@ -72,7 +72,7 @@ data RunCruxMode = RcmConcrete | RcmSymbolic | RcmCoverage
   deriving (Show, Eq)
 
 runCrux :: FilePath -> Handle -> RunCruxMode -> IO ()
-runCrux rustFile outHandle mode = do
+runCrux rustFile outHandle mode = Mir.withMirLogging $ do
     -- goalTimeout is bumped from 60 to 180 because scalar.rs symbolic
     -- verification runs close to the timeout, causing flaky results
     -- (especially in CI).
@@ -90,8 +90,8 @@ runCrux rustFile outHandle mode = do
                                         Crux.branchCoverage = (mode == RcmCoverage) } ,
                    Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete),
                                            Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" })
-    let ?outputConfig = Crux.mkOutputConfig False outHandle outHandle $
-                        Just (fst options)
+    let ?outputConfig = Crux.mkOutputConfig (outHandle, False) (outHandle, False)
+            Mir.mirLoggingToSayWhat (Just $ fst options)
     setEnv "CRYPTOLPATH" "."
     _exitCode <- Mir.runTestsWithExtraOverrides overrides options
     return ()