Merge pull request #826 from GaloisInc/methodspec

Fix soundness bug related to disjointness checking (#641)

Author: brianhuffman

.travis.yml

@@ -85,7 +85,7 @@ jobs:
         - mkdir -p s2n/test-deps/saw/bin
         - cp bin/saw s2n/test-deps/saw/bin
         - cd s2n
-        - git checkout cd7282102bf5e65cc8b324c4127c7943c71c8513
+        - git checkout 90b8913a01c6421444d19aaab798d413872cf6f0
       before_script:
         - export TESTS=sawHMAC
       script:

intTests/test_llvm_non_fresh/Makefile

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

intTests/test_llvm_non_fresh/test.bc

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

intTests/test_llvm_non_fresh/test.c

@@ -0,0 +1,48 @@
+// This test checks whether we can verify a spec that says a function
+// returns a fresh pointer, when in actuality the function returns
+// a pointer from the input. It is a regression test for saw-script
+// issue #641.
+// https://github.com/GaloisInc/saw-script/issues/641
+
+bc <- llvm_load_module "test.bc";
+
+let i64 = llvm_int 64;
+
+foo_ov <-
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      x <- crucible_alloc i64;
+      crucible_execute_func [x];
+      crucible_return x;
+    }
+    z3;
+
+fails (
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      x <- crucible_alloc i64;
+      crucible_execute_func [x];
+      y <- crucible_alloc i64;
+      crucible_return y;
+    }
+    z3
+  );
+
+fails (
+  crucible_llvm_verify bc "bar" [foo_ov] false
+    do {
+      x <- crucible_alloc i64;
+      crucible_execute_func [x];
+      crucible_return (crucible_term {{ 0 : [32] }});
+    }
+    z3
+  );
+
+bar_ov1 <-
+  crucible_llvm_verify bc "bar" [] false
+    do {
+      x <- crucible_alloc i64;
+      crucible_execute_func [x];
+      crucible_return (crucible_term {{ 1 : [32] }});
+    }
+    z3;

intTests/test_llvm_non_fresh/test.saw

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

intTests/test_llvm_non_fresh/test.sh

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

intTests/test_llvm_return_global/Makefile

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

intTests/test_llvm_return_global/test.bc

@@ -0,0 +1,38 @@
+// This test checks whether we can verify a spec that says a function
+// returns a fresh pointer, when in actuality the function returns
+// a global. It is a regression test for saw-script issue #641.
+// https://github.com/GaloisInc/saw-script/issues/641
+
+bc <- llvm_load_module "test.bc";
+
+let i64 = llvm_int 64;
+
+fails (
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      crucible_alloc_global "glob";
+      crucible_execute_func [];
+      x <- crucible_alloc i64;
+      crucible_return x;
+    }
+    z3
+  );
+
+/*
+bar_ov0 <-
+  crucible_llvm_verify bc "bar" [foo_ov] false
+    do {
+      crucible_execute_func [];
+      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;

intTests/test_llvm_return_global/test.c

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

intTests/test_llvm_return_global/test.saw

@@ -19,7 +19,7 @@ RUN mkdir -p /saw-script && \
     git clone https://github.com/GaloisInc/s2n.git && \
     mkdir -p s2n/test-deps/saw/bin && \
     cd s2n && \
-    git checkout cd7282102bf5e65cc8b324c4127c7943c71c8513
+    git checkout 90b8913a01c6421444d19aaab798d413872cf6f0
 
 COPY scripts/s2n-entrypoint.sh /entrypoint.sh
 ENTRYPOINT [ "/entrypoint.sh" ]

intTests/test_llvm_return_global/test.sh

@@ -325,9 +325,7 @@ deriving instance ( SetupValueHas Show ext
 -- | Verification state (either pre- or post-) specification
 data StateSpec ext = StateSpec
   { _csAllocs        :: Map AllocIndex (AllocSpec ext)
-    -- ^ allocated pointers
-  , _csFreshPointers :: Map AllocIndex (AllocSpec ext)
-    -- ^ symbolic pointers
+    -- ^ allocated or declared pointers
   , _csPointsTos     :: [PointsTo ext]
     -- ^ points-to statements
   , _csConditions    :: [SetupCondition ext]
@@ -343,7 +341,6 @@ makeLenses ''StateSpec
 initialStateSpec :: StateSpec ext
 initialStateSpec =  StateSpec
   { _csAllocs        = Map.empty
-  , _csFreshPointers = Map.empty -- TODO: this is LLVM-specific
   , _csPointsTos     = []
   , _csConditions    = []
   , _csFreshVars     = []
@@ -396,7 +393,7 @@ ppMethodSpec methodSpec =
 csAllocations :: CrucibleMethodSpecIR ext -> Map AllocIndex (AllocSpec ext)
 csAllocations
   = Map.unions
-  . toListOf ((csPreState <> csPostState) . (csAllocs <> csFreshPointers))
+  . toListOf ((csPreState <> csPostState) . csAllocs)
 
 csTypeNames :: CrucibleMethodSpecIR ext -> Map AllocIndex (TypeName ext)
 csTypeNames

s2nTests/docker/s2n.dockerfile

@@ -693,16 +693,10 @@ verifyPrestate opts cc mspec globals =
      let Just mem = Crucible.lookupGlobal lvar globals
 
      -- Allocate LLVM memory for each 'crucible_alloc'
-     (env1, mem') <- runStateT
-       (traverse (doAlloc cc)  $ mspec ^. MS.csPreState . MS.csAllocs)
+     (env, mem') <- runStateT
+       (Map.traverseWithKey (doAlloc cc) (mspec ^. MS.csPreState . MS.csAllocs))
        mem
 
-     env2 <-
-       Map.traverseWithKey
-         (\k _ -> executeFreshPointer cc k)
-         (mspec ^. MS.csPreState . MS.csFreshPointers)
-     let env = Map.unions [env1, env2]
-
      mem'' <- setupGlobalAllocs cc mspec mem'
 
      mem''' <- setupPrePointsTos mspec opts cc env (mspec ^. MS.csPreState . MS.csPointsTos) mem''
@@ -875,9 +869,13 @@ assertEqualVals cc v1 v2 =
 doAlloc ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   LLVMCrucibleContext arch       ->
+  AllocIndex ->
   LLVMAllocSpec ->
   StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
-doAlloc cc (LLVMAllocSpec mut _memTy alignment sz loc) = StateT $ \mem ->
+doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh)
+  | fresh = liftIO $ executeFreshPointer cc i
+  | otherwise =
+  StateT $ \mem ->
   do let sym = cc^.ccBackend
      sz' <- liftIO $ resolveSAWSymBV cc Crucible.PtrWidth sz
      let l = show (W4.plSourceLoc loc)
@@ -1157,7 +1155,10 @@ 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.csGlobalAllocs) (mspec ^. MS.csPostState)
+          learnCond opts sc cc mspec PostState
+            (mspec ^. MS.csGlobalAllocs)
+            (mspec ^. MS.csPreState . MS.csAllocs)
+            (mspec ^. MS.csPostState)
 
      st <-
        case matchPost of
@@ -1756,6 +1757,7 @@ crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty =
        , _allocSpecAlign = alignment'
        , _allocSpecBytes = sz''
        , _allocSpecLoc = loc
+       , _allocSpecFresh = False
        }
 
 crucible_alloc ::
@@ -1861,6 +1863,7 @@ crucible_symbolic_alloc bic _opts ro align_bytes sz =
            , _allocSpecAlign = alignment
            , _allocSpecBytes = sz
            , _allocSpecLoc = loc
+           , _allocSpecFresh = False
            }
      n <- Setup.csVarCounter <<%= nextAllocIndex
      Setup.currentState . MS.csAllocs . at n ?= spec
@@ -1907,12 +1910,13 @@ constructFreshPointer mid loc memTy =
      n <- Setup.csVarCounter <<%= nextAllocIndex
      sz <- liftIO $ scPtrWidthBvNat cctx $ Crucible.memTypeSize ?dl memTy
      let alignment = Crucible.memTypeAlign ?dl memTy
-     Setup.currentState . MS.csFreshPointers . at n ?=
+     Setup.currentState . MS.csAllocs . at n ?=
        LLVMAllocSpec { _allocSpecMut = Crucible.Mutable
                      , _allocSpecType = memTy
                      , _allocSpecAlign = alignment
                      , _allocSpecBytes = sz
                      , _allocSpecLoc = loc
+                     , _allocSpecFresh = True
                      }
      -- TODO: refactor
      case mid of

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -43,6 +43,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , allocSpecMut
   , allocSpecLoc
   , allocSpecBytes
+  , allocSpecFresh
   , mutIso
   , isMut
     -- * LLVMModule
@@ -187,6 +188,7 @@ data LLVMAllocSpec =
     , _allocSpecAlign :: CL.Alignment
     , _allocSpecBytes :: Term
     , _allocSpecLoc   :: ProgramLoc
+    , _allocSpecFresh :: Bool -- ^ Whether declared with @crucible_fresh_pointer@
     }
   deriving (Eq, Show)