Merge pull request #257 from GaloisInc/separate-backend

Update with changes flowing from GaloicInc/crucible#945.
GaloisInc · Jan 25, 2022 · d1d71fd · d1d71fd
2 parents 63a65c3 + c572e37
commit d1d71fd
Show file tree

Hide file tree

Showing 27 changed files with 542 additions and 466 deletions.
diff --git a/deps/asl-translator b/deps/asl-translator
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/semmc b/deps/semmc
diff --git a/deps/what4 b/deps/what4
diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 module Data.Macaw.AArch32.Symbolic.Functions (
   SymFuns
@@ -82,33 +83,33 @@ funcSemantics :: (CB.IsSymInterface sym, MS.ToCrucibleType mt ~ t)
               -> IO (CS.RegValue sym t, S sym rtp bs r ctx)
 funcSemantics sfns fn st0 =
    case fn of
-    MAA.SDiv _rep lhs rhs -> withSym st0 $ \sym -> do
-      lhs' <- toValBV sym lhs
-      rhs' <- toValBV sym rhs
+    MAA.SDiv _rep lhs rhs -> withBackend st0 $ \sym bak -> do
+      lhs' <- toValBV bak lhs
+      rhs' <- toValBV bak rhs
       -- NOTE: We are applying division directly here without checking the divisor for zero.
       --
       -- The ARM semantics explicitly check this and have different behaviors
       -- depending on what CPU flags are set; this operation is never called
       -- with a divisor of zero.  We could add an assertion to that effect here,
       -- but it might be difficult to prove.
       LL.llvmPointer_bv sym =<< WI.bvSdiv sym lhs' rhs'
-    MAA.UDiv _rep lhs rhs -> withSym st0 $ \sym -> do
-      lhs' <- toValBV sym lhs
-      rhs' <- toValBV sym rhs
+    MAA.UDiv _rep lhs rhs -> withBackend st0 $ \sym bak -> do
+      lhs' <- toValBV bak lhs
+      rhs' <- toValBV bak rhs
       -- NOTE: See the note in SDiv
       LL.llvmPointer_bv sym =<< WI.bvUdiv sym lhs' rhs'
-    MAA.URem _rep lhs rhs -> withSym st0 $ \sym -> do
-      lhs' <- toValBV sym lhs
-      rhs' <- toValBV sym rhs
+    MAA.URem _rep lhs rhs -> withBackend st0 $ \sym bak -> do
+      lhs' <- toValBV bak lhs
+      rhs' <- toValBV bak rhs
       -- NOTE: See the note in SDiv
       LL.llvmPointer_bv sym =<< WI.bvUrem sym lhs' rhs'
-    MAA.SRem _rep lhs rhs -> withSym st0 $ \sym -> do
-      lhs' <- toValBV sym lhs
-      rhs' <- toValBV sym rhs
+    MAA.SRem _rep lhs rhs -> withBackend st0 $ \sym bak -> do
+      lhs' <- toValBV bak lhs
+      rhs' <- toValBV bak rhs
       -- NOTE: See the note in SDiv
       LL.llvmPointer_bv sym =<< WI.bvSrem sym lhs' rhs'
-    MAA.UnsignedRSqrtEstimate _rep v -> withSym st0 $ \sym -> do
-      v' <- toValBV sym v
+    MAA.UnsignedRSqrtEstimate _rep v -> withBackend st0 $ \sym bak -> do
+      v' <- toValBV bak v
       let args = Ctx.empty Ctx.:> v'
       res <- lookupApplySymFun sym sfns "unsignedRSqrtEstimate" CT.knownRepr args CT.knownRepr
       LL.llvmPointer_bv sym res
@@ -139,22 +140,21 @@ funcSemantics sfns fn st0 =
     MAA.ARMSyscall {} ->
       AP.panic AP.AArch32 "funcSemantics" ["The ARM syscall primitive should be eliminated and replaced by a handle lookup"]
 
-withSym :: (CB.IsSymInterface sym)
-        => S sym rtp bs r ctx
-        -> (sym -> IO a)
-        -> IO (a, S sym rtp bs r ctx)
-withSym s action = do
-  let sym = s ^. CSET.stateSymInterface
-  val <- action sym
-  return (val, s)
-
+withBackend ::
+  S sym rtp bs r ctx ->
+  (forall bak. CB.IsSymBackend sym bak => sym -> bak -> IO a) ->
+  IO (a, S sym rtp bs r ctx)
+withBackend s action = do
+  CSET.withBackend (s^.CSET.stateContext) $ \bak ->
+    do val <- action (CB.backendGetSym bak) bak
+       return (val, s)
 
 -- | Assert that the wrapped value is a bitvector
-toValBV :: (CB.IsSymInterface sym)
-        => sym
+toValBV :: (CB.IsSymBackend sym bak)
+        => bak
         -> AA.AtomWrapper (CS.RegEntry sym) (MT.BVType w)
         -> IO (CS.RegValue sym (CT.BVType w))
-toValBV sym (AA.AtomWrapper x) = LL.projectLLVM_bv sym (CS.regValue x)
+toValBV bak (AA.AtomWrapper x) = LL.projectLLVM_bv bak (CS.regValue x)
 
 -- | Apply an uninterpreted function to the provided arguments
 --

diff --git a/macaw-aarch32-symbolic/tests/Main.hs b/macaw-aarch32-symbolic/tests/Main.hs
@@ -37,6 +37,7 @@ import qualified Data.Macaw.Discovery as M
 import qualified Data.Macaw.Symbolic as MS
 import qualified Data.Macaw.Symbolic.Testing as MST
 import qualified What4.Config as WC
+import qualified What4.Expr.Builder as WEB
 import qualified What4.Interface as WI
 import qualified What4.ProblemFeatures as WPF
 import qualified What4.Solver as WS
@@ -113,6 +114,8 @@ mkSymExTest expected exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOpti
           symExTestSized expected exePath saveSMT saveMacaw step ehi MA.arm_linux_info
         Elf.ELFCLASS64 -> TTH.assertFailure "64 bit ARM is not supported"
 
+data MacawAarch32TestData t = MacawAarch32TestData
+
 symExTestSized :: MST.SimulationResult
                -> FilePath
                -> SaveSMT
@@ -128,19 +131,20 @@ symExTestSized expected exePath saveSMT saveMacaw step ehi archInfo = do
      step ("Testing " ++ BS8.unpack name ++ " at " ++ show (M.discoveredFunAddr dfi))
      writeMacawIR saveMacaw (BS8.unpack name) dfi
      Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator
-     CBO.withYicesOnlineBackend CBO.FloatRealRepr gen CBO.NoUnsatFeatures WPF.noFeatures $ \sym -> do
+     sym <- WEB.newExprBuilder WEB.FloatRealRepr MacawAarch32TestData gen
+     CBO.withYicesOnlineBackend sym CBO.NoUnsatFeatures WPF.noFeatures $ \bak -> do
        -- We are using the z3 backend to discharge proof obligations, so
        -- we need to add its options to the backend configuration
        let solver = WS.z3Adapter
        let backendConf = WI.getConfiguration sym
        WC.extendConfig (WS.solver_adapter_config_options solver) backendConf
 
-       execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend sym)
+       execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend bak)
        let Just archVals = MS.archVals (Proxy @MA.ARM) Nothing
        let extract = armResultExtractor archVals
        logger <- makeGoalLogger saveSMT solver name exePath
        let ?memOpts = LLVM.defaultMemOptions
-       simRes <- MST.simulateAndVerify solver logger sym execFeatures archInfo archVals mem extract dfi
+       simRes <- MST.simulateAndVerify solver logger bak execFeatures archInfo archVals mem extract dfi
        TTH.assertEqual "AssertionResult" expected simRes
 
 writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
@@ -19,15 +19,15 @@ import           Data.Macaw.ARM.Arch ( a32InstructionMatcher )
 import           Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics, armTranslateType )
 import qualified Data.Macaw.CFG as MC
 import           Data.Macaw.SemMC.Generator ( Generator )
-import           Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction )
+import           Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction, MacawSemMC(..) )
 import qualified Data.Macaw.Types as MT
 import           Data.Parameterized.Classes ( showF )
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.Nonce as PN
 import           Data.Parameterized.Some ( Some(..), mapSome )
 import           Data.Proxy ( Proxy(..) )
 import           Dismantle.ARM.A32 -- must be present to supply definitions for genExecInstruction output
-import qualified Lang.Crucible.Backend.Simple as CBS
+import qualified What4.Expr.Builder as WEB
 import qualified Language.Haskell.TH as TH
 import qualified SemMC.Architecture.AArch32 as ARMSem
 import           SemMC.Architecture.ARM.Opcodes ( ASLSemantics(..), allA32OpcodeInfo )
@@ -40,7 +40,7 @@ execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32)
                 -> Maybe (Generator ARMSem.AArch32 ids s ())
 execInstruction =
   $(do Some ng <- TH.runIO PN.newIONonceGenerator
-       sym <- TH.runIO (CBS.newSimpleBackend CBS.FloatIEEERepr ng)
+       sym <- TH.runIO (WEB.newExprBuilder WEB.FloatIEEERepr MacawSemMC ng)
        sem <- TH.runIO (loadSemantics sym)
        let
          aconv :: (MapF.Pair (Opcode Operand) x)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -46,7 +46,7 @@ import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.TraversableFC as FC
 import           Data.Parameterized.NatRepr
 import           GHC.TypeLits as TL
-import qualified Lang.Crucible.Backend.Simple as CBS
+import qualified What4.Expr.Builder as WEB
 import           Language.Haskell.TH
 import qualified SemMC.Architecture.AArch32 as ARM
 import qualified SemMC.Architecture.ARM.Opcodes as ARM
@@ -55,7 +55,7 @@ import qualified What4.Expr.Builder as WB
 
 import qualified Language.ASL.Globals as ASL
 
-loadSemantics :: CBS.SimpleBackend t fs -> IO (ARM.ASLSemantics (CBS.SimpleBackend t fs))
+loadSemantics :: WEB.ExprBuilder t st fs -> IO (ARM.ASLSemantics (WEB.ExprBuilder t st fs))
 loadSemantics sym = ARM.loadSemantics sym (ARM.ASLSemanticsOpts { ARM.aslOptTrimRegs = True})
 
 -- n.b. although MacawQ is a monad and therefore has a fail

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs
@@ -19,15 +19,15 @@ import           Data.Macaw.ARM.Arch ( t32InstructionMatcher )
 import           Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics, armTranslateType )
 import qualified Data.Macaw.CFG as MC
 import           Data.Macaw.SemMC.Generator ( Generator )
-import           Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction )
+import           Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction, MacawSemMC(..) )
 import qualified Data.Macaw.Types as MT
 import           Data.Parameterized.Classes ( showF )
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.Nonce as PN
 import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
 import           Dismantle.ARM.T32 -- as ThumbDis -- must be present to supply definitions for genExecInstruction output
-import qualified Lang.Crucible.Backend.Simple as CBS
+import qualified What4.Expr.Builder as WEB
 import qualified Language.Haskell.TH as TH
 import qualified SemMC.Architecture.AArch32 as ARMSem
 import           SemMC.Architecture.ARM.Opcodes ( ASLSemantics(..), allT32OpcodeInfo )
@@ -39,7 +39,7 @@ execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32)
                 -> Maybe (Generator ARMSem.AArch32 ids s ())
 execInstruction =
   $(do Some ng <- TH.runIO PN.newIONonceGenerator
-       sym <- TH.runIO (CBS.newSimpleBackend CBS.FloatIEEERepr ng)
+       sym <- TH.runIO (WEB.newExprBuilder WEB.FloatIEEERepr MacawSemMC ng)
        sem <- TH.runIO (loadSemantics sym)
        let
          aconv :: (MapF.Pair (Opcode Operand) x)
+4 −6		.github/workflows/ci-matrix.yml
+2 −2		asl-translator.cabal
+2 −4		exe/Concrete.hs
+0 −4		lib/Data/Parameterized/CtxFuns.hs
+29 −22		lib/Language/ASL.hs
+6 −4		lib/Language/ASL/Crucible/Extension.hs
+3 −4		lib/Language/ASL/Formulas/Normalize.hs
+7 −12		lib/Language/ASL/StaticExpr.hs
+14 −16		lib/Language/ASL/Translation/Driver.hs
+1 −1		submodules/crucible
+1 −1		submodules/what4
+2 −4		tests/Deserialize/Main.hs
+8 −8		semmc-aarch32/src/SemMC/Architecture/ARM/ASL.hs
+3 −2		semmc-aarch32/test/TestFormulas.hs
+0 −13		semmc-aarch32/test/TestMain.hs
+8 −5		semmc-arm/src/SemMC/Architecture/A32.hs
+3 −2		semmc-arm/test/TestFormulas.hs
+3 −2		semmc-arm/tools/GenBase.hs
+0 −13		semmc-arm/tools/Main.hs
+9 −9		semmc-fuzzer/programs/FuzzerMain.hs
+25 −19		semmc-learning/src/SemMC/Stochastic/CandidateProgram.hs
+40 −39		semmc-learning/src/SemMC/Stochastic/Classify.hs
+43 −41		semmc-learning/src/SemMC/Stochastic/Extract.hs
+1 −1		semmc-learning/src/SemMC/Stochastic/Generalize.hs
+22 −15		semmc-learning/src/SemMC/Stochastic/Initialize.hs
+45 −35		semmc-learning/src/SemMC/Stochastic/Monad.hs
+21 −18		semmc-learning/src/SemMC/Stochastic/Strata.hs
+24 −20		semmc-learning/src/SemMC/Stochastic/Synthesize.hs
+7 −3		semmc-ppc/src/SemMC/Architecture/PPC/Shared.hs
+25 −19		semmc-ppc/tests/Main.hs
+3 −1		semmc-ppc/tools/GenBase.hs
+29 −23		semmc-ppc/tools/SynthDemo.hs
+28 −20		semmc-synthesis/src/SemMC/Synthesis.hs
+32 −23		semmc-synthesis/src/SemMC/Synthesis/Cegis.hs
+22 −16		semmc-synthesis/src/SemMC/Synthesis/Cegis/EvalFormula.hs
+24 −17		semmc-synthesis/src/SemMC/Synthesis/Cegis/LLVMMem.hs
+20 −16		semmc-synthesis/src/SemMC/Synthesis/Cegis/ReadWriteEval.hs
+9 −7		semmc-synthesis/src/SemMC/Synthesis/Cegis/Tests.hs
+15 −7		semmc-synthesis/src/SemMC/Synthesis/Cegis/Types.hs
+32 −27		semmc-synthesis/src/SemMC/Synthesis/Core.hs
+20 −17		semmc-synthesis/src/SemMC/Synthesis/DivideAndConquer.hs
+11 −9		semmc-synthesis/src/SemMC/Synthesis/Template.hs
+24 −17		semmc-synthesis/src/SemMC/Synthesis/Testing.hs
+17 −10		semmc-toy/src/SemMC/Toy/Tests.hs
+4 −2		semmc/src/SemMC/Architecture.hs
+19 −12		semmc/src/SemMC/Architecture/Evaluate.hs
+43 −40		semmc/src/SemMC/Formula/Equivalence.hs
+14 −9		semmc/src/SemMC/Formula/Eval.hs
+15 −10		semmc/src/SemMC/Formula/Instantiate.hs
+6 −3		semmc/src/SemMC/Symbolic.hs
+52 −33		semmc/tests/semstore/ParamFormulaTests.hs
+11 −7		semmc/tests/semstore/TestUtils.hs
+1 −1		submodules/asl-translator
+1 −1		submodules/crucible
+1 −1		submodules/what4
+70 −42		.github/workflows/test.yml
+9 −0		README.md
+3 −5		what4-transition-system/test/Main.hs
+32 −0		what4/CHANGES.md
+3 −4		what4/README.md
+3 −4		what4/doc/QuickStart.hs
+6 −0		what4/src/What4/BaseTypes.hs
+62 −26		what4/src/What4/Config.hs
+16 −0		what4/src/What4/Expr.hs
+201 −0		what4/src/What4/Expr/Allocator.hs
+4 −1		what4/src/What4/Expr/App.hs
+1 −1		what4/src/What4/Expr/ArrayUpdateMap.hs
+1 −1		what4/src/What4/Expr/BoolMap.hs
+123 −236		what4/src/What4/Expr/Builder.hs
+4 −0		what4/src/What4/Expr/MATLAB.hs
+1 −1		what4/src/What4/Expr/StringSeq.hs
+2 −0		what4/src/What4/Expr/UnaryBV.hs
+7 −1		what4/src/What4/Expr/WeightedSum.hs
+76 −0		what4/src/What4/FloatMode.hs
+1 −1		what4/src/What4/Interface.hs
+2 −0		what4/src/What4/InterpretedFloatingPoint.hs
+82 −44		what4/src/What4/Protocol/SMTLib2.hs
+10 −10		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+21 −22		what4/src/What4/Protocol/SMTWriter.hs
+6 −0		what4/src/What4/SemiRing.hs
+2 −0		what4/src/What4/Solver.hs
+1 −1		what4/src/What4/Solver/Yices.hs
+15 −1		what4/src/What4/Solver/Z3.hs
+4 −1		what4/src/What4/SpecialFunctions.hs
+3 −0		what4/src/What4/Utils/OnlyIntRepr.hs
+30 −57		what4/test/AdapterTest.hs
+90 −106		what4/test/ExprBuilderSMTLib2.hs
+2 −4		what4/test/ExprsTest.hs
+2 −3		what4/test/IteExprs.hs
+67 −82		what4/test/OnlineSolverTest.hs
+55 −0		what4/test/ProbeSolvers.hs
+2 −3		what4/test/TestTemplate.hs
+11 −2		what4/what4.cabal