Merge pull request #752 from GaloisInc/issue642

Issue642

Author: brianhuffman

intTests/test_issue642/Makefile

@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c

intTests/test_issue642/test.bc

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int glob;
+
+int foo (int *x) {
+	return (x == &glob);
+}
+
+int bar () {
+	return foo(&glob);
+}

intTests/test_issue642/test.c

@@ -0,0 +1,37 @@
+// This test checks whether we can use an override with a pointer
+// argument that aliases a global. It is a regression test for
+// saw-script issue #642.
+// https://github.com/GaloisInc/saw-script/issues/642
+
+bc <- llvm_load_module "test.bc";
+
+let i32 = llvm_int 32;
+
+foo_ov <-
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      crucible_alloc_global "glob";
+      x <- crucible_alloc i32;
+      crucible_execute_func [x];
+      crucible_return (crucible_term {{ 0 : [32] }});
+    }
+    z3;
+
+bar_ov1 <-
+  crucible_llvm_verify bc "bar" [] false
+    do {
+      crucible_alloc_global "glob";
+      crucible_execute_func [];
+      crucible_return (crucible_term {{ 1 : [32] }});
+    }
+    z3;
+
+fails (
+  crucible_llvm_verify bc "bar" [foo_ov] false
+    do {
+      crucible_alloc_global "glob";
+      crucible_execute_func [];
+      crucible_return (crucible_term {{ 0 : [32] }});
+    }
+    z3
+  );

intTests/test_issue642/test.saw

@@ -0,0 +1 @@
+$SAW test.saw

intTests/test_issue642/test.sh

@@ -1131,7 +1131,7 @@ verifyPoststate opts sc cc mspec env0 globals ret =
        io $
        runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $
        do matchResult
-          learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState)
+          learnCond opts sc cc mspec PostState (mspec ^. MS.csGlobalAllocs) (mspec ^. MS.csPostState)
 
      st <-
        case matchPost of

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -592,7 +592,7 @@ methodSpecHandler_prestate opts sc cc args cs =
 
        sequence_ [ matchArg opts sc cc cs PreState x y z | (x, y, z) <- xs]
 
-       learnCond opts sc cc cs PreState (cs ^. MS.csPreState)
+       learnCond opts sc cc cs PreState (cs ^. MS.csGlobalAllocs) (cs ^. MS.csPreState)
 
 
 -- | Use a method spec to override the behavior of a function.
@@ -619,14 +619,15 @@ learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWi
           -> LLVMCrucibleContext arch
           -> MS.CrucibleMethodSpecIR (LLVM arch)
           -> PrePost
+          -> [MS.AllocGlobal (LLVM arch)]
           -> MS.StateSpec (LLVM arch)
           -> OverrideMatcher (LLVM arch) md ()
-learnCond opts sc cc cs prepost ss =
+learnCond opts sc cc cs prepost globals ss =
   do let loc = cs ^. MS.csLoc
      matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos)
      traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions)
      enforcePointerValidity cc loc ss
-     enforceDisjointness loc ss
+     enforceDisjointness cc loc globals ss
      enforceCompleteSubstitution loc ss
 
 
@@ -743,41 +744,87 @@ enforcePointerValidity cc loc ss =
 -- allowed to alias other read-only allocations, however.
 enforceDisjointness ::
   (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  LLVMCrucibleContext arch ->
   W4.ProgramLoc ->
+  [MS.AllocGlobal (LLVM arch)] ->
   MS.StateSpec (LLVM arch) ->
   OverrideMatcher (LLVM arch) md ()
-enforceDisjointness loc ss =
+enforceDisjointness cc loc globals ss =
   do sym <- Ov.getSymInterface
      sub <- OM (use setupValueSub)
+     mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc
      let (allocsRW, allocsRO) = Map.partition (view isMut) (view MS.csAllocs ss)
          memsRW = Map.elems $ Map.intersectionWith (,) allocsRW sub
          memsRO = Map.elems $ Map.intersectionWith (,) allocsRO sub
 
      -- Ensure that all RW regions are disjoint from each other, and
      -- that all RW regions are disjoint from all RO regions.
      sequence_
-        [ do c <- liftIO $
-               do W4.setCurrentProgramLoc sym ploc
-                  psz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToBV Crucible.PtrWidth psz
-                  W4.setCurrentProgramLoc sym qloc
-                  qsz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToBV Crucible.PtrWidth qsz
-                  W4.setCurrentProgramLoc sym loc
-                  Crucible.buildDisjointRegionsAssertion
-                    sym Crucible.PtrWidth
-                    p psz'
-                    q qsz'
-             let msg =
-                   "Memory regions not disjoint: "
-                   ++ "(base=" ++ show (Crucible.ppPtr p) ++ ", size=" ++ show psz ++ ")"
-                   ++ " and "
-                   ++ "(base=" ++ show (Crucible.ppPtr q) ++ ", size=" ++ show qsz ++ ")"
-             addAssert c $ Crucible.SimError loc $
-               Crucible.AssertFailureSimError msg ""
-
-        | (LLVMAllocSpec _mut _pty _align psz ploc, p) : ps <- tails memsRW
-        , (LLVMAllocSpec _mut _qty _align qsz qloc, q) <- ps ++ memsRO
+        [ enforceDisjointAllocSpec sym loc p q
+        | p : ps <- tails memsRW
+        , q <- ps ++ memsRO
         ]
 
+     -- Ensure that all RW and RO regions are disjoint from mutable
+     -- global regions.
+     let resolveAllocGlobal g@(LLVMAllocGlobal _ nm) =
+           do ptr <- liftIO $ Crucible.doResolveGlobal sym mem nm
+              pure (g, ptr)
+     globals' <- traverse resolveAllocGlobal globals
+     sequence_
+       [ enforceDisjointAllocGlobal sym loc p q
+       | p <- memsRW ++ memsRO
+       , q <- globals'
+       ]
+
+-- | Assert that two LLVM allocations are disjoint from each other.
+enforceDisjointAllocSpec ::
+  (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  Sym -> W4.ProgramLoc ->
+  (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
+  (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
+  OverrideMatcher (LLVM arch) md ()
+enforceDisjointAllocSpec sym loc
+  (LLVMAllocSpec _pmut _pty _palign psz ploc, p)
+  (LLVMAllocSpec _qmut _qty _qalign qsz qloc, q) =
+  do c <- liftIO $
+       do W4.setCurrentProgramLoc sym ploc
+          psz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToBV Crucible.PtrWidth psz
+          W4.setCurrentProgramLoc sym qloc
+          qsz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToBV Crucible.PtrWidth qsz
+          W4.setCurrentProgramLoc sym loc
+          Crucible.buildDisjointRegionsAssertion
+            sym Crucible.PtrWidth
+            p psz'
+            q qsz'
+     let msg =
+           "Memory regions not disjoint: "
+           ++ "(base=" ++ show (Crucible.ppPtr p) ++ ", size=" ++ show psz ++ ")"
+           ++ " and "
+           ++ "(base=" ++ show (Crucible.ppPtr q) ++ ", size=" ++ show qsz ++ ")"
+     addAssert c $ Crucible.SimError loc $
+       Crucible.AssertFailureSimError msg ""
+
+-- | Assert that an LLVM allocation is disjoint from a global region.
+enforceDisjointAllocGlobal ::
+  Sym -> W4.ProgramLoc ->
+  (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
+  (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) ->
+  OverrideMatcher (LLVM arch) md ()
+enforceDisjointAllocGlobal sym loc
+  (LLVMAllocSpec _pmut _pty _palign psz _ploc, p)
+  (LLVMAllocGlobal _qloc (L.Symbol qname), q) =
+  do let Crucible.LLVMPointer pblk _ = p
+     let Crucible.LLVMPointer qblk _ = q
+     c <- liftIO $ W4.notPred sym =<< W4.natEq sym pblk qblk
+     let msg =
+           "Memory regions not disjoint: "
+           ++ "(base=" ++ show (Crucible.ppPtr p) ++ ", size=" ++ show psz ++ ")"
+           ++ " and "
+           ++ "global " ++ show qname ++ " (base=" ++ show (Crucible.ppPtr q) ++ ")"
+     addAssert c $ Crucible.SimError loc $
+       Crucible.AssertFailureSimError msg ""
+
 ------------------------------------------------------------------------
 
 -- | For each points-to statement read the memory value through the