Add enable_lax_pointer_ordering

Fixes #1308.

CHANGES.md

@@ -20,6 +20,10 @@ Several improvements have been made to JVM verification:
   "current" status, so that `enable_experimental` is no longer
   necessary for JVM verification.
 
+A new `enable_lax_pointer_ordering` function exists, which relaxes the
+restrictions that Crucible imposes on comparisons between pointers from
+different allocation blocks.
+
 # Version 0.8
 
 ## New Features

intTests/test1308/Makefile

@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O2
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test1308/test.c

@@ -0,0 +1,10 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+const size_t LEN = 42;
+
+void zip_with_add(uint64_t c[LEN], const uint64_t a[LEN], const uint64_t b[LEN]) {
+  for (size_t i = 0; i < LEN; i++) {
+    c[i] = a[i] + b[i];
+  }
+}

intTests/test1308/test.saw

@@ -0,0 +1,29 @@
+enable_lax_pointer_ordering;
+
+let alloc_init_readonly ty v = do {
+  p <- llvm_alloc_readonly ty;
+  llvm_points_to p v;
+  return p;
+};
+
+let ptr_to_fresh_readonly n ty = do {
+  x <- llvm_fresh_var n ty;
+  p <- alloc_init_readonly ty (llvm_term x);
+  return (x, p);
+};
+
+let LEN = 42;
+
+let zip_with_add_spec = do {
+  let array_ty = llvm_array LEN (llvm_int 64);
+  c_ptr <- llvm_alloc array_ty;
+  (a, a_ptr) <- ptr_to_fresh_readonly "a" array_ty;
+  (b, b_ptr) <- ptr_to_fresh_readonly "b" array_ty;
+
+  llvm_execute_func [c_ptr, a_ptr, b_ptr];
+
+  llvm_points_to c_ptr (llvm_term {{ zipWith`{LEN} (+) a b }});
+};
+
+mod <- llvm_load_module "test.bc";
+llvm_verify mod "zip_with_add" [] false zip_with_add_spec z3;

intTests/test1308/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/docs/SAW.rst

@@ -291,7 +291,7 @@ SAW/set option (command)
 
 
 ``option``
-  The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``SMT array memory model``, or ``What4 hash consing``
+  The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``SMT array memory model``, or ``What4 hash consing``
 
 
 Set a SAW option in the server.

saw-remote-api/docs/old-Saw.rst

@@ -165,6 +165,7 @@ Setting Options
   - ``option``: The name of the option to set. This is one of:
 
     * ``lax arithmetic``
+    * ``lax pointer ordering``
     * ``SMT array memory model``
     * ``What4 hash consing``
 

saw-remote-api/src/SAWServer.hs

@@ -216,6 +216,7 @@ initialState readFileFn =
                 , rwProfilingFile = Nothing
                 , rwCrucibleAssertThenAssume = False
                 , rwLaxArith = False
+                , rwLaxPointerOrdering = False
                 , rwWhat4HashConsing = False
                 , rwWhat4HashConsingX86 = False
                 , rwStackBaseAlign = defaultStackBaseAlign

saw-remote-api/src/SAWServer/SetOption.hs

@@ -30,6 +30,8 @@ setOption opt =
      case opt of
        EnableLaxArithmetic enabled ->
          updateRW rw { rwLaxArith = enabled }
+       EnableLaxPointerOrdering enabled ->
+         updateRW rw { rwLaxPointerOrdering = enabled }
        EnableSMTArrayMemoryModel enabled -> undefined
          updateRW rw { rwSMTArrayMemoryModel = enabled }
        EnableWhat4HashConsing enabled -> undefined
@@ -38,13 +40,15 @@ setOption opt =
 
 data SetOptionParams
   = EnableLaxArithmetic Bool
+  | EnableLaxPointerOrdering Bool
   | EnableSMTArrayMemoryModel Bool
   | EnableWhat4HashConsing Bool
 
 parseOption :: Object -> String -> Parser SetOptionParams
 parseOption o name =
   case name of
     "lax arithmetic" -> EnableLaxArithmetic <$> o .: "value"
+    "lax pointer ordering" -> EnableLaxPointerOrdering <$> o .: "value"
     "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value"
     "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value"
     _ -> empty
@@ -59,6 +63,7 @@ instance Doc.DescribedParams SetOptionParams where
     [ ("option",
        Doc.Paragraph [Doc.Text "The option to set and its accompanying value (i.e., true or false); one of the following:"
                      , Doc.Literal "lax arithmetic", Doc.Text ", "
+                     , Doc.Literal "lax pointer ordering", Doc.Text ", "
                      , Doc.Literal "SMT array memory model", Doc.Text ", or "
                      , Doc.Literal "What4 hash consing"
                      ])

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1312,6 +1312,7 @@ setupLLVMCrucibleContext pathSat lm action =
      smt_array_memory_model_enabled <- gets rwSMTArrayMemoryModel
      crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume
      what4HashConsing <- gets rwWhat4HashConsing
+     laxPointerOrdering <- gets rwLaxPointerOrdering
      Crucible.llvmPtrWidth ctx $ \wptr ->
        Crucible.withPtrWidth wptr $
        do let ?lc = ctx^.Crucible.llvmTypeCtx
@@ -1348,8 +1349,11 @@ setupLLVMCrucibleContext pathSat lm action =
                  crucible_assert_then_assume_enabled
 
                let bindings = Crucible.fnBindingsFromList []
+               let memOpts  = Crucible.defaultMemOptions
+                                { Crucible.laxPointerOrdering = laxPointerOrdering
+                                }
                let simctx   = Crucible.initSimContext sym intrinsics halloc stdout
-                                 bindings (Crucible.llvmExtensionImpl Crucible.defaultMemOptions)
+                                 bindings (Crucible.llvmExtensionImpl memOpts)
                                  Common.SAWCruciblePersonality
                mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans)
                         =<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod

src/SAWScript/Interpreter.hs

@@ -470,6 +470,7 @@ buildTopLevelEnv proxy opts =
                    , rwCrucibleAssertThenAssume = False
                    , rwProfilingFile = Nothing
                    , rwLaxArith = False
+                   , rwLaxPointerOrdering = False
                    , rwWhat4HashConsing = False
                    , rwWhat4HashConsingX86 = False
                    , rwPreservedRegs = []
@@ -538,6 +539,11 @@ enable_lax_arithmetic = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwLaxArith = True }
 
+enable_lax_pointer_ordering :: TopLevel ()
+enable_lax_pointer_ordering = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwLaxPointerOrdering = True }
+
 enable_what4_hash_consing :: TopLevel ()
 enable_what4_hash_consing = do
   rw <- getTopLevelRW
@@ -759,6 +765,11 @@ primitives = Map.fromList
     Current
     [ "Enable lax rules for arithmetic overflow in Crucible." ]
 
+  , prim "enable_lax_pointer_ordering" "TopLevel ()"
+    (pureVal enable_lax_pointer_ordering)
+    Current
+    [ "Enable lax rules for pointer ordering comparisons in Crucible." ]
+
   , prim "enable_what4_hash_consing" "TopLevel ()"
     (pureVal enable_what4_hash_consing)
     Current

src/SAWScript/Value.hs

@@ -220,7 +220,7 @@ showsProofResult opts r =
   case r of
     ValidProof _ _ -> showString "Valid"
     InvalidProof _ ts _ -> showString "Invalid: [" . showMulti "" ts
-    UnfinishedProof st  -> showString "Unfinished: " . shows (length (psGoals st)) . showString " goals remaining" 
+    UnfinishedProof st  -> showString "Unfinished: " . shows (length (psGoals st)) . showString " goals remaining"
   where
     opts' = sawPPOpts opts
     showVal t = shows (ppFirstOrderValue opts' t)
@@ -402,6 +402,7 @@ data TopLevelRW =
   , rwCrucibleAssertThenAssume :: Bool
   , rwProfilingFile :: Maybe FilePath
   , rwLaxArith :: Bool
+  , rwLaxPointerOrdering :: Bool
 
   -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing"
   , rwWhat4HashConsing :: Bool