Separate backend

cabal.project

@@ -21,7 +21,6 @@ packages:
     deps/crucible/crucible-concurrency
     deps/crucible/crucible-jvm
     deps/crucible/crucible-llvm
-    deps/crucible/crucible-saw
     deps/crucible/crucible-symio
     deps/crucible/crucible-syntax
     deps/crucible/crux

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

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

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

@@ -190,9 +190,10 @@ builderNew :: forall sym p t st fs rtp.
     DefId ->
     OverrideSim (p sym) sym MIR rtp
         EmptyCtx MethodSpecBuilderType (MethodSpecBuilder sym t)
-builderNew cs defId = do
-    sym <- getSymInterface
-    snapFrame <- liftIO $ pushAssumptionFrame sym
+builderNew cs defId =
+  ovrWithBackend $ \bak -> do
+    let sym = backendGetSym bak
+    snapFrame <- liftIO $ pushAssumptionFrame bak
 
     let tyArg = cs ^? collection . M.intrinsics . ix defId .
             M.intrInst . M.inSubsts . _Wrapped . ix 0
@@ -227,8 +228,10 @@ addArg :: forall sym p t st fs rtp args ret tp.
     (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
-    sym <- lift $ getSymInterface
+addArg tpr argRef msb =
+  ovrWithBackend $ \bak ->
+  execBuilderT msb $ do
+    let sym = backendGetSym bak
     loc <- liftIO $ W4.getCurrentProgramLoc sym
 
     let idx = Map.size $ msb ^. msbSpec . MS.csArgBindings
@@ -238,7 +241,7 @@ addArg tpr argRef msb = execBuilderT msb $ do
     let shp = tyToShapeEq col ty tpr
 
     rv <- lift $ readMirRefSim tpr argRef
-    sv <- regToSetup sym Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
+    sv <- regToSetup bak Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
 
     void $ forNewRefs Pre $ \fr -> do
         let len = fr ^. frAllocSpec . maLen
@@ -248,15 +251,15 @@ addArg tpr argRef msb = execBuilderT msb $ do
             ref' <- lift $ mirRef_offsetSim (fr ^. frType) (fr ^. frRef) iSym
             rv <- lift $ readMirRefSim (fr ^. frType) ref'
             let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
-            sv <- regToSetup sym Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
+            sv <- regToSetup bak Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
 
             -- Clobber the current value
             rv' <- case fr ^. frAllocSpec . maMutbl of
                 M.Mut -> lift $ clobberSymbolic sym loc "clobberArg" shp rv
                 M.Immut -> lift $ clobberImmutSymbolic sym loc "clobberArg" shp rv
             lift $ writeMirRefSim (fr ^. frType) ref' rv'
             -- Gather fresh vars created by the clobber operation
-            sv' <- regToSetup sym Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv'
+            sv' <- regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv'
 
             return (sv, sv')
 
@@ -277,16 +280,17 @@ setReturn :: forall sym t st fs p rtp args ret tp.
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     TypeRepr tp -> MirReferenceMux sym tp -> MethodSpecBuilder sym t ->
     OverrideSim p sym MIR rtp args ret (MethodSpecBuilder sym t)
-setReturn tpr argRef msb = execBuilderT msb $ do
-    sym <- lift $ getSymInterface
-
+setReturn tpr argRef msb =
+  ovrWithBackend $ \bak ->
+  execBuilderT msb $ do
+    let sym = backendGetSym bak
     let ty = case msb ^. msbSpec . MS.csRet of
             Just x -> x
             Nothing -> M.TyTuple []
     let shp = tyToShapeEq col ty tpr
 
     rv <- lift $ readMirRefSim tpr argRef
-    sv <- regToSetup sym Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
+    sv <- regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
 
     void $ forNewRefs Post $ \fr -> do
         let len = fr ^. frAllocSpec . maLen
@@ -296,7 +300,7 @@ setReturn tpr argRef msb = execBuilderT msb $ do
             ref' <- lift $ mirRef_offsetSim (fr ^. frType) (fr ^. frRef) iSym
             rv <- lift $ readMirRefSim (fr ^. frType) ref'
             let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
-            regToSetup sym Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
+            regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
 
         msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo (fr ^. frAlloc) svs :)
 
@@ -315,14 +319,15 @@ gatherAssumes :: forall sym t st fs p rtp args ret.
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     MethodSpecBuilder sym t ->
     OverrideSim p sym MIR rtp args ret (MethodSpecBuilder sym t)
-gatherAssumes msb = do
-    sym <- getSymInterface
+gatherAssumes msb =
+  ovrWithBackend $ \bak -> do
+    let sym = backendGetSym bak
 
     -- Find all vars that are mentioned in the arguments.
     let vars = msb ^. msbPre . seVars
 
     -- Find all assumptions that mention a relevant variable.
-    assumes <- liftIO $ collectAssumptions sym
+    assumes <- liftIO $ collectAssumptions bak
     flatAssumes <- liftIO $ flattenAssumptions sym assumes
     optAssumes' <- liftIO $ relevantPreds sym vars $
         map (\a -> (assumptionPred a, show $ ppAssumption PP.viaShow a)) $ flatAssumes
@@ -355,14 +360,15 @@ gatherAsserts :: forall sym t st fs p rtp args ret.
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     MethodSpecBuilder sym t ->
     OverrideSim p sym MIR rtp args ret (MethodSpecBuilder sym t)
-gatherAsserts msb = do
-    sym <- getSymInterface
+gatherAsserts msb =
+  ovrWithBackend $ \bak -> do
+    let sym = backendGetSym bak
 
     -- Find all vars that are mentioned in the arguments or return value.
     let vars = (msb ^. msbPre . seVars) `Set.union` (msb ^. msbPost . seVars)
 
     -- Find all assertions that mention a relevant variable.
-    goals <- liftIO $ maybe [] goalsToList <$> getProofObligations sym
+    goals <- liftIO $ maybe [] goalsToList <$> getProofObligations bak
     let asserts = map proofGoal goals
     optAsserts' <- liftIO $ relevantPreds sym vars $
         map (\a -> (a ^. W4.labeledPred, a ^. W4.labeledPredMsg)) asserts
@@ -464,7 +470,7 @@ gatherVars sym vals = do
 -- `pred` that mentions at least one variable in `vars` along with some
 -- `badVar` not in `vars`.
 relevantPreds :: forall sym t st fs a.
-    (IsSymInterface sym, IsBoolSolver sym, sym ~ W4.ExprBuilder t st fs) =>
+    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     sym ->
     Set (Some (W4.ExprBoundVar t)) ->
     [(W4.Pred sym, a)] ->
@@ -502,14 +508,15 @@ finish :: forall sym t st fs p rtp args ret.
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     MethodSpecBuilder sym t ->
     OverrideSim p sym MIR rtp args ret (M.MethodSpec sym)
-finish msb = do
-    sym <- getSymInterface
-    let ng = W4.exprCounter sym
+finish msb =
+  ovrWithBackend $ \bak -> do
+    let sym = backendGetSym bak
+    let ng  = sym ^. W4.exprCounter
 
     -- TODO: also undo any changes to Crucible global variables / refcells
     -- (correct spec functions shouldn't make such changes, but it would be
     -- nice to warn the user if they accidentally do)
-    _ <- liftIO $ popAssumptionFrameAndObligations sym (msb ^. msbSnapshotFrame)
+    _ <- liftIO $ popAssumptionFrameAndObligations bak (msb ^. msbSnapshotFrame)
 
     let preVars = msb ^. msbPre . seVars
     let postVars = msb ^. msbPost . seVars
@@ -628,14 +635,16 @@ substMethodSpec sc sm ms = do
 -- RegValue will be converted into fresh variables in the MethodSpec (in either
 -- the pre or post state, depending on the pre/post flag `p`), and any
 -- MirReferences will be converted into MethodSpec allocations/pointers.
-regToSetup :: forall sym t st fs tp p rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
-    sym -> PrePost ->
+regToSetup :: forall sym bak t st fs tp p rtp args ret.
+    (IsSymBackend sym bak, sym ~ W4.ExprBuilder t st fs, HasCallStack) =>
+    bak -> PrePost ->
     (forall tp'. BaseTypeRepr tp' -> W4.Expr t tp' -> IO SAW.TypedTerm) ->
     TypeShape tp -> RegValue sym tp ->
     BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
-regToSetup sym p eval shp rv = go shp rv
+regToSetup bak p eval shp rv = go shp rv
   where
+    sym = backendGetSym bak
+
     go :: forall tp. TypeShape tp -> RegValue sym tp ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
     go (UnitShape _) () = return $ MS.SetupStruct () False []
@@ -686,7 +695,7 @@ regToSetup sym p eval shp rv = go shp rv
         let mutbl = case refTy of
                 M.TyRef _ M.Immut -> M.Immut
                 _ -> M.Mut
-        alloc <- refToAlloc sym p mutbl ty' tpr startRef len
+        alloc <- refToAlloc bak p mutbl ty' tpr startRef len
         let offsetSv idx sv = if idx == 0 then sv else MS.SetupElem () sv idx
         return $ offsetSv idx $ MS.SetupVar alloc
 
@@ -704,11 +713,11 @@ regToSetup sym p eval shp rv = go shp rv
                 OptField shp -> liftIO (readMaybeType sym "field" (shapeType shp) rv) >>= go shp
             loop flds rvs (sv : svs)
 
-refToAlloc :: forall sym t st fs tp p rtp args ret.
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
-    sym -> PrePost -> M.Mutability -> M.Ty -> TypeRepr tp -> MirReferenceMux sym tp -> Int ->
+refToAlloc :: forall sym bak t st fs tp p rtp args ret.
+    (IsSymBackend sym bak, sym ~ W4.ExprBuilder t st fs) =>
+    bak -> PrePost -> M.Mutability -> M.Ty -> TypeRepr tp -> MirReferenceMux sym tp -> Int ->
     BuilderT sym t (OverrideSim p sym MIR rtp args ret) MS.AllocIndex
-refToAlloc sym p mutbl ty tpr ref len = do
+refToAlloc bak p mutbl ty tpr ref len = do
     refs <- use $ msbPrePost p . seRefs
     mAlloc <- liftIO $ lookupAlloc ref (toList refs)
     case mAlloc of
@@ -734,7 +743,7 @@ refToAlloc sym p mutbl ty tpr ref len = do
     lookupAlloc _ref [] = return Nothing
     lookupAlloc ref (Some fr : frs) = case testEquality tpr (fr ^. frType) of
         Just Refl -> do
-            eq <- mirRef_eqIO sym ref (fr ^. frRef)
+            eq <- mirRef_eqIO bak ref (fr ^. frRef)
             case W4.asConstantPred eq of
                 Just True -> return $ Just $ fr ^. frAlloc
                 Just False -> lookupAlloc ref frs

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

@@ -127,7 +127,8 @@ freshSymbolic sym loc nameStr shp = go shp
         let nameSymbol = W4.safeSymbol nameStr
         expr <- liftIO $ W4.freshConstant sym nameSymbol btpr
         let ev = CreateVariableEvent loc nameStr btpr expr
-        liftIO $ addAssumptions sym (singleEvent ev)
+        ovrWithBackend $ \bak ->
+          liftIO $ addAssumptions bak (singleEvent ev)
         return expr
     go (ArrayShape (M.TyArray _ len) _ shp) =
         MirVector_Vector <$> V.replicateM len (go shp)

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

@@ -127,8 +127,8 @@ runSpec :: forall sym p t st fs args ret rtp.
     (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
-    let col = cs ^. collection
+runSpec cs mh ms = ovrWithBackend $ \bak ->
+ do let col = cs ^. collection
     sym <- getSymInterface
     RegMap argVals <- getOverrideArgs
     let argVals' = Map.fromList $ zip [0..] $ MS.assignmentToList argVals
@@ -168,7 +168,7 @@ runSpec cs mh ms = do
         Some btpr <- liftIO $ termToType sym sc (SAW.ecType ec)
         expr <- liftIO $ W4.freshConstant sym nameSymbol btpr
         let ev = CreateVariableEvent loc nameStr btpr expr
-        liftIO $ addAssumptions sym (singleEvent ev)
+        liftIO $ addAssumptions bak (singleEvent ev)
         term <- liftIO $ eval expr
         return (SAW.ecVarIndex ec, term)
 
@@ -239,7 +239,7 @@ runSpec cs mh ms = do
                     show alloc ++ " (info: " ++ show info ++ ")"
 
         -- All references in `allocSub` must point to disjoint memory regions.
-        liftIO $ checkDisjoint sym (Map.toList allocSub)
+        liftIO $ checkDisjoint bak (Map.toList allocSub)
 
         -- TODO: see if we need any other assertions from LLVM OverrideMatcher
 
@@ -266,10 +266,9 @@ runSpec cs mh ms = do
         Right x -> return x
 
     forM_ (os ^. MS.osAsserts) $ \lp ->
-        liftIO $ addAssertion sym lp
-
+      liftIO $ addAssertion bak lp
     forM_ (os ^. MS.osAssumes) $ \p ->
-        liftIO $ addAssumption sym (GenericAssumption loc "methodspec postcondition" p)
+      liftIO $ addAssumption bak (GenericAssumption loc "methodspec postcondition" p)
 
     let preAllocMap = os ^. MS.setupValueSub
 
@@ -465,7 +464,8 @@ matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv
             Nothing -> return ()
             Just (Some ptr)
               | Just Refl <- testEquality tpr (ptr ^. mpType) -> do
-                eq <- liftIO $ mirRef_eqIO sym ref' (ptr ^. mpRef)
+                eq <- lift $ ovrWithBackend $ \bak ->
+                        liftIO $ mirRef_eqIO bak ref' (ptr ^. mpRef)
                 let loc = mkProgramLoc "matchArg" InternalPos
                 MS.addAssert eq $
                     SimError loc (AssertFailureSimError ("mismatch on " ++ show alloc) "")
@@ -555,16 +555,18 @@ condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do
 
 
 checkDisjoint ::
-    (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
-    sym ->
+    (sym ~ W4.ExprBuilder t st fs, IsSymBackend sym bak) =>
+    bak ->
     [(MS.AllocIndex, Some (MirPointer sym))] ->
     IO ()
-checkDisjoint sym refs = go refs
+checkDisjoint bak refs = go refs
   where
+    sym = backendGetSym bak
+
     go [] = return ()
     go ((alloc, Some ptr) : rest) = do
         forM_ rest $ \(alloc', Some ptr') -> do
-            disjoint <- W4.notPred sym =<< mirRef_overlapsIO sym (ptr ^. mpRef) (ptr' ^. mpRef)
-            assert sym disjoint $ GenericSimError $
+            disjoint <- W4.notPred sym =<< mirRef_overlapsIO bak (ptr ^. mpRef) (ptr' ^. mpRef)
+            assert bak disjoint $ GenericSimError $
                 "references " ++ show alloc ++ " and " ++ show alloc' ++ " must not overlap"
         go rest

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

@@ -63,9 +63,9 @@ import Mir.Compositional.Convert
 
 
 cryptolOverrides ::
-    forall sym p t st fs args ret blocks rtp a r .
+    forall sym bak p t st fs args ret blocks rtp a r .
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
-    Maybe (SomeOnlineSolver sym) ->
+    Maybe (SomeOnlineSolver sym bak) ->
     CollectionState ->
     Text ->
     CFG MIR blocks args ret ->