Updates to track the cex-errors2 branch of crucible.

Along the way, deduplicate some functions that exist in essentially the same form internally in crucible.
GaloisInc · Sep 11, 2020 · 9c6d6ab · 9c6d6ab
1 parent 5f24a64
commit 9c6d6ab
Show file tree

Hide file tree

Showing 6 changed files with 18 additions and 48 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/macaw b/deps/macaw
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -511,12 +511,10 @@ verifyMethodSpec bic opts cc methodSpec lemmas checkSat tactic asp =
          Nothing   -> fail "internal error: LLVM Memory global not found"
          Just mem0 -> return mem0
      -- push a memory stack frame if starting from a breakpoint
-     let mem = if isJust (methodSpec^.csParentName)
-               then mem0
-                 { Crucible.memImplHeap = Crucible.pushStackFrameMem
-                   (Crucible.memImplHeap mem0)
-                 }
-               else mem0
+     let mem = case methodSpec^.csParentName of
+                 Just nm -> mem0 { Crucible.memImplHeap = Crucible.pushStackFrameMem (Text.pack nm)
+                                                             (Crucible.memImplHeap mem0) }
+                 Nothing -> mem0
      let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem
 
      -- construct the initial state for verifications
@@ -897,7 +895,7 @@ ppGlobalPair cc gp =
       globals = gp ^. Crucible.gpGlobals in
   case Crucible.lookupGlobal mvar globals of
     Nothing -> text "LLVM Memory global variable not initialized"
-    Just mem -> Crucible.ppMem mem
+    Just mem -> Crucible.ppMem (Crucible.memImplHeap mem)
 
 
 --------------------------------------------------------------------------------

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1442,7 +1442,8 @@ instantiateExtResolveSAWSymBV sc cc w tm = do
 -- is overwritten by a postcondition memory write is not invalidated.
 -- Return a map containing the overwritten memory allocations.
 invalidateMutableAllocs ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym) =>
   Options ->
   SharedContext ->
   LLVMCrucibleContext arch ->

diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -17,7 +17,6 @@ Stability   : provisional
 module SAWScript.Crucible.LLVM.ResolveSetupValue
   ( LLVMVal, LLVMPtr
   , resolveSetupVal
-  , typeOfLLVMVal
   , typeOfSetupValue
   , resolveTypedTerm
   , resolveSAWPred
@@ -33,7 +32,6 @@ import Control.Monad
 import qualified Control.Monad.Fail as Fail
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
-import Data.Foldable (toList)
 import Data.Maybe (fromMaybe, listToMaybe, fromJust)
 import Data.IORef
 import           Data.Map (Map)
@@ -280,7 +278,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do
     SetupTerm tm -> resolveTypedTerm cc tm
     SetupStruct () packed vs -> do
       vals <- mapM (resolveSetupVal cc mem env tyenv nameEnv) vs
-      let tps = map (typeOfLLVMVal dl) vals
+      let tps = map Crucible.llvmValStorableType vals
       let t = Crucible.mkStructType (V.fromList (mkFields packed dl Crucible.noAlignment 0 tps))
       let flds = case Crucible.storageTypeF t of
                    Crucible.Struct v -> v
@@ -289,7 +287,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do
     SetupArray () [] -> fail "resolveSetupVal: invalid empty array"
     SetupArray () vs -> do
       vals <- V.mapM (resolveSetupVal cc mem env tyenv nameEnv) (V.fromList vs)
-      let tp = typeOfLLVMVal dl (V.head vals)
+      let tp = Crucible.llvmValStorableType (V.head vals)
       return $ Crucible.LLVMValArray tp vals
     SetupField () v n -> do
       i <- resolveSetupFieldIndexOrFail cc tyenv nameEnv v n
@@ -543,48 +541,19 @@ typeAlignment dl ty =
     Crucible.Array _sz ty'   -> typeAlignment dl ty'
     Crucible.Struct flds     -> V.foldl max Crucible.noAlignment (fmap (typeAlignment dl . (^. Crucible.fieldVal)) flds)
 
-typeOfLLVMVal :: Crucible.DataLayout -> LLVMVal -> Crucible.StorageType
-typeOfLLVMVal _dl val =
-  case val of
-    Crucible.LLVMValInt _bkl bv ->
-       Crucible.bitvectorType (Crucible.intWidthSize (fromIntegral (natValue (W4.bvWidth bv))))
-    Crucible.LLVMValFloat _ _   -> error "FIXME: typeOfLLVMVal LLVMValFloat"
-    Crucible.LLVMValStruct flds -> Crucible.mkStructType (fmap fieldType flds)
-    Crucible.LLVMValArray tp vs -> Crucible.arrayType (fromIntegral (V.length vs)) tp
-    Crucible.LLVMValZero tp     -> tp
-    Crucible.LLVMValUndef tp    -> tp
-  where
-    fieldType (f, _) = (f ^. Crucible.fieldVal, Crucible.fieldPad f)
 
 equalValsPred ::
   LLVMCrucibleContext wptr ->
   LLVMVal ->
   LLVMVal ->
   IO (W4.Pred Sym)
-equalValsPred cc v1 v2 = go (v1, v2)
-  where
-  go :: (LLVMVal, LLVMVal) -> IO (W4.Pred Sym)
-
-  go (Crucible.LLVMValInt blk1 off1, Crucible.LLVMValInt blk2 off2)
-       | Just Refl <- testEquality (W4.bvWidth off1) (W4.bvWidth off2)
-       = do blk_eq <- W4.natEq sym blk1 blk2
-            off_eq <- W4.bvEq sym off1 off2
-            W4.andPred sym blk_eq off_eq
-  --go (Crucible.LLVMValFloat xsz x, Crucible.LLVMValFloat ysz y) | xsz == ysz
-  --     = W4.floatEq sym x y -- TODO
-  go (Crucible.LLVMValStruct xs, Crucible.LLVMValStruct ys)
-       | V.length xs == V.length ys
-       = do cs <- mapM go (zip (map snd (toList xs)) (map snd (toList ys)))
-            foldM (W4.andPred sym) (W4.truePred sym) cs
-  go (Crucible.LLVMValArray _tpx xs, Crucible.LLVMValArray _tpy ys)
-       | V.length xs == V.length ys
-       = do cs <- mapM go (zip (toList xs) (toList ys))
-            foldM (W4.andPred sym) (W4.truePred sym) cs
-
-  go _ = return (W4.falsePred sym)
+equalValsPred cc v1 v2 =
+   fromMaybe (W4.falsePred sym) <$> Crucible.testEqual sym v1 v2
 
+  where
   sym = cc^.ccBackend
 
+
 memArrayToSawCoreTerm ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
   LLVMCrucibleContext arch ->

diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs
@@ -999,7 +999,8 @@ checkAlloc sym s (l := a) =
 -- If the region ID is concretely zero, it should be the case that the
 -- 'RegionIndex' map would translate it into a real 'LLVMPtr' since the only map
 -- entry (established in 'setupGlobals') is for 0.
-mkGlobalMap :: Map.Map RegionIndex (LLVMPtr Sym 64) -> GlobalMap Sym Crucible.Mem 64
+mkGlobalMap :: Crucible.HasLLVMAnn Sym =>
+  Map.Map RegionIndex (LLVMPtr Sym 64) -> GlobalMap Sym Crucible.Mem 64
 mkGlobalMap rmap sym mem region off =
   mapConcreteRegion <|> passThroughConcreteRegion <|> mapSymbolicRegion
   where
@@ -1259,6 +1260,7 @@ lookupCry x mp =
 
 
 adjustPtr ::
+  Crucible.HasLLVMAnn Sym =>
   Sym -> MemImpl Sym -> LLVMPtr Sym 64 -> Integer -> IO (LLVMPtr Sym 64)
 adjustPtr sym mem ptr amt
   | amt == 0  = return ptr
+0 −12		crucible-jvm/cabal.project
+1 −1		crucible-jvm/tool/Main.hs
+7 −5		crucible-llvm/crucible-llvm.cabal
+4 −1		crucible-llvm/src/Lang/Crucible/LLVM.hs
+151 −0		crucible-llvm/src/Lang/Crucible/LLVM/Errors.hs
+239 −0		crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs
+157 −94		crucible-llvm/src/Lang/Crucible/LLVM/Errors/Poison.hs
+7 −7		crucible-llvm/src/Lang/Crucible/LLVM/Errors/Standards.hs
+239 −183		crucible-llvm/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs
+8 −9		crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs
+0 −1		crucible-llvm/src/Lang/Crucible/LLVM/Extension.hs
+0 −240		crucible-llvm/src/Lang/Crucible/LLVM/Extension/Safety.hs
+10 −6		crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs
+11 −4		crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+7 −7		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs
+12 −12		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
+26 −22		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+1 −1		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs
+184 −138		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+175 −431		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+443 −0		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
+418 −258		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+38 −15		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
+15 −0		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Type.hs
+72 −23		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Value.hs
+2 −1		crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
+6 −1		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs
+10 −3		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+1 −1		crucible-syntax/test-data/simulator-tests/assert.out.good
+2 −2		crucible-syntax/test-data/simulator-tests/assume-merge.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/assume-merge2.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/assume.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/branch.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/calls.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/double-branch.out.good
+2 −2		crucible-syntax/test-data/simulator-tests/float-cast.out.good
+2 −2		crucible-syntax/test-data/simulator-tests/from-maybe.out.good
+4 −4		crucible-syntax/test-data/simulator-tests/loop-err.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/loop.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/mjrty.out.good
+1 −1		crucible-syntax/test-data/simulator-tests/override-test.out.good
+2 −2		crucible-syntax/test-data/simulator-tests/override-test2.out.good
+1 −0		crucible/src/Lang/Crucible/Simulator.hs
+3 −3		crucible/src/Lang/Crucible/Simulator/SimError.hs
+10 −0		crux-llvm/c-src/includes/crucible.h
+4 −4		crux-llvm/src/Crux/LLVM/Compile.hs
+12 −1		crux-llvm/src/Crux/LLVM/Config.hs
+9 −2		crux-llvm/src/Crux/LLVM/Overrides.hs
+48 −28		crux-llvm/src/Crux/LLVM/Simulate.hs
+2 −2		crux-llvm/svcomp/Main.hs
+4 −4		crux-llvm/test-data/golden/float-cast.good
+1 −1		crux-llvm/test-data/golden/float-cast2.good
+1 −2		crux-llvm/test-data/golden/strlen_test2.c
+4 −4		crux-llvm/test-data/golden/uint-cast.good
+5 −5		crux-llvm/test-data/golden/vector-cmp.good
+47 −11		crux/src/Crux.hs
+10 −0		crux/src/Crux/Config.hs
+11 −9		crux/src/Crux/Config/Common.hs
+39 −30		crux/src/Crux/Goal.hs
+9 −4		crux/src/Crux/Model.hs
+5 −4		crux/src/Crux/Report.hs
+7 −3		crux/src/Crux/Types.hs
+1 −1		deps/crucible
+1 −1		deps/what4
+2 −0		symbolic/src/Data/Macaw/Symbolic/Memory.hs
+3 −3		x86_symbolic/tests/Main.hs