Add more toggles for memory model-related options

[RyanGlScott]

SV-COMP has various benchmark programs that are expected to verify despite technically having memory model issues. For instance, s3_clnt.blast.01.i.cil-1.c is expected to verify successfully in the unreach-call category, but Crux will currently reject it thusly:

$ crux-llvm --config config.crux --target=i386-unknown-linux-elf sv-benchmarks/c/openssl/s3_clnt.blast.01.i.cil-1.c 
[Crux] Using pointer width: 32 for file crux-build/crux~s3_clnt.blast.01.i.cil-1.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] Found counterexample for verification goal
[Crux]   sv-benchmarks/c/openssl/s3_clnt.blast.01.i.cil-1.c:1120:19: error: in ssl3_connect
[Crux]   Error during memory load
[Crux]     No previous write to this location was found
[Crux]       Attempting load at type: i32
[Crux]       Via pointer: (20, 0x1c:[32])
[Crux]     Performing overall load at type: i32
[Crux]       Via pointer: (20, 0x1c:[32])
...

In order to make Crux handle these sorts of SV-COMP programs, we'll need to add a toggle to suppress this particular class of error. We already have various memory-model–related toggles, however. These include lax-pointer-ordering and lax-constant-equality. Although we could just tack on more one-off toggles like these, it might make sense to consolidate all of these options somehow, similarly to how ub-sanitizers consolidates toggles related to undefined behavior.

[robdockins]

In my ideal vision for this, we have a tree-based taxonomy of errors. Then users can specify sets of errors to check for by specifying boolean combinations of sets of errors as named by the taxonomy.

For example, we might have a category of memory-error that includes no-previous-write, and unaligned-pointer, invalid-cast, etc. etc.

[robdockins]

Ultimately, I'd like every proof obligation that is asserted in a Crucible program to have an associated identifier in this taxonomy, and assertions get filtered in the Backend module. That way we don't have to add a bunch of invasive options throughout the codebase. We just identify the class of assertion at the time it is made, and the filtering happens in one unified place.

[RyanGlScott]

That sounds like a reasonable approach to me. I don't have a clear sense of all possible proof obligations in Crucible, so do you think it would make sense to only add a memory-error category for now?

[robdockins]

Yes, I think we can add meaningful categories later. As a first step, I'd probably just change the API for assertions to accept a category tag and make all use sites provide a "generic" or "trivial" tag. Later, we can go through and provide meaningful categories.

[RyanGlScott]

I looked into fixing this recently, but I'm a bit stuck on how to implement a no-previous-write toggle. Presumably, we'd need to alter this code:

crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

Lines 758 to 769 in 7942801

	fallback0 ::
	StorageType ->
	LLVMPtr sym w ->
	ReadMem sym (PartLLVMVal sym)
	fallback0 tp l =
	do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be
	-- sure it always fails. But, because it's a variable, it won't be constant-folded away
	-- and we can be relatively sure the annotation will survive.
	liftIO $ do
	b <- freshConstant sym emptySymbol BaseBoolRepr
	Partial.Err <$>
	Partial.annotateME sym mop (NoSatisfyingWrite tp l) b

In the event a user disables the no-previous-write error, then we'd presumably want to return NoErr instead of Err, providing NoErr with a fresh, uninterpreted value of some sort. However, the payload of NoErr is an LLVMVal, and for the life of me, I can't figure out a clean way to create an uninterpreted LLVMVal from just a StorageType. Am I missing something, or is my approach flawed?

[robdockins]

Yeah, Ideally we'd figure out how to generate an appropriate LLVMVal here. Let me look into what we have to work with at this point. We might need to add a new LLVMVal constructor for "arbitrary" data and figure out what to do with it later.

[robdockins]

OK, there is already an LLVMValUndef, and I think we should use it for this purpose. I think we might need to update some other surrounding code to make sure it is handled correctly (e.g., unpackMemValue should not panic), but that seems like a good way forward.

[RyanGlScott]

Ah. I was aware of LLVMValUndef, but my understanding is that its semantics aren't quite the same as "fresh constant", since optimization passes are allowed to assume that undef can take on whatever arbitrary value it finds convenient. This is in contrast to something like, say, the return value of a freeze instruction, which is closer to crucible's freshConstant. Perhaps we do want reads from previously unwritten memory to behave like undef after all, but I wanted to double check, since I was previously under the impression that you envisioned something closer to the latter.

[robdockins]

You're right, the semantics of LLVM undef are quite unsettled, and perhaps we shouldn't overload it this way.

Thinking about it some more, perhaps what we want to do is reinterpret the PartialLLVMVal type. In one mode (our current default) a partial value represents an error. In another (new) mode, a partial value represents a fresh value of the expected type. This, I think, would be a pretty minimal change that achieves the desired result.

[RyanGlScott]

Just to make sure I understand correctly, you're proposing that in the new mode, we change the semantics of the assertSafe function?

crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

Lines 320 to 328 in 168f000

	-- | Take a partial value and assert its safety
	assertSafe :: (IsSymInterface sym)
	=> sym
	-> PartLLVMVal sym
	-> IO (LLVMVal sym)
	assertSafe sym (NoErr p v) =
	do let rsn = AssertFailureSimError "Error during memory load" ""
	assert sym p rsn
	return v

That is, rather than invoking assert on a NoErr, we should create a fresh LLVMVal? If so, how does one know what the type of the LLVMVal should be? As far as I can tell, we don't thread StorageTypes down to NoErrs. Should we?

[robdockins]

Indeed, at about this level of the API is where I was thinking about changing things. assertSafe doesn't have very many call sites, so if we want to rearrange how it works, we have some flexibility. If we need to pass in more information, or just do this some other way, I think it wouldn't be too disruptive.

[robdockins]

Just a bit more flavor: in the current mode a PartLLVMVal is morally a predicate and a value (or no value at all), and it means roughly if p then v else error. In the new mode, it would basically mean if p then v else fresh for some appropriate fresh value (with the obvious simplifications if p is either concretely true or false).

[RyanGlScott]

I've tried a couple of approaches to plumb through type information, and I'm encountering difficulties with both approaches:

1. One approach is to add a StorageType field to the Err constructor of PartLLVMVal and consult that type when creating a fresh constant in assertSafe.
2. Another approach is to not change the definition of PartLLVMVal at all, but instead pass an additional StorageType argument to assertSafe.

Approach (1) requires changing the logic of several functions that match on PartLLVMVals, and sometimes in non-obvious ways. For instance, what should this case of appendArray do when given two Err arguments that don't have Array types? Since this case returns an Err, we have to return some sort of StorageType, but it's not obvious to me what that should be.

For this reason, I decided to implement approach (2), as it seems less invasive. I'm still not confident that my patch which implements this approach is correct, however. Here is a WIP patch:

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
index afea8c0b..b55d84ff 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
@@ -559,7 +559,7 @@ doLoad ::
   IO (RegValue sym tp)
 doLoad sym mem ptr valType tpr alignment = do
   unpackMemValue sym tpr =<<
-    Partial.assertSafe sym =<<
+    Partial.assertSafe sym valType =<<
       loadRaw sym mem ptr valType alignment
 
 -- | Store a 'RegValue' in memory. Both the 'StorageType' and 'TypeRepr'
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
index 7f9ec7d5..c1f96a01 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -1247,7 +1247,7 @@ writeMemWithAllocationCheck is_allocated sym w gsym ptr tp alignment val mem = d
               =<< traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
 
             -- TODO! we're abusing assertSafe here a little
-            v <- Partial.assertSafe sym partial_byte
+            v <- Partial.assertSafe sym tp partial_byte
             case v of
               LLVMValInt _ byte
                 | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
index 51ed3a10..a1869b6f 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
@@ -320,14 +320,20 @@ totalLLVMVal sym = NoErr (truePred sym)
 -- | Take a partial value and assert its safety
 assertSafe :: (IsSymInterface sym)
            => sym
+           -> StorageType
            -> PartLLVMVal sym
            -> IO (LLVMVal sym)
-assertSafe sym (NoErr p v) =
+assertSafe sym tp (NoErr p v) =
   do let rsn = AssertFailureSimError "Error during memory load" ""
+     unless (tp == Value.llvmValStorableType v) $
+       panic "RGS assertSafe"
+         [ "tp: " ++ show tp
+         , "llvmValStorableType v: " ++ show (Value.llvmValStorableType v)
+         ]
      assert sym p rsn
      return v
 
-assertSafe sym (Err p) = do
+assertSafe sym _ (Err p) = do
   do let rsn = AssertFailureSimError "Error during memory load" ""
      loc <- getCurrentProgramLoc sym
      let err = SimError loc rsn
diff --git a/crucible-llvm/test/TestMemory.hs b/crucible-llvm/test/TestMemory.hs
index 73d7c049..2d029ed2 100644
--- a/crucible-llvm/test/TestMemory.hs
+++ b/crucible-llvm/test/TestMemory.hs
@@ -375,7 +375,7 @@ testPointerStore = testCase "pointer store" $ withMem LLVMD.BigEndian $ \sym mem
                                     noAlignment
 
   -- Assert that the read pointer is equal to the original pointer
-  base_ptr1_back_safe <- LLVMMem.assertSafe sym base_ptr1_back
+  base_ptr1_back_safe <- LLVMMem.assertSafe sym pointer_storage_type base_ptr1_back
   is_equal <- LLVMMem.testEqual sym base_ptr1_val base_ptr1_back_safe
   case is_equal of
     Nothing -> assertFailure "testEqual failed"
diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
index 3bf0202b..5c9e0d49 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
@@ -201,11 +201,12 @@ wasmStoreDouble sym off v mem =
 wasmLoadInt :: (1 <= w, IsSymInterface sym) => sym -> SymBV sym 32 -> NatRepr w -> WasmMemImpl sym -> IO (SymBV sym w)
 wasmLoadInt sym off w mem =
   do let bs = Bytes (intValue w `div` 8)
+         tp = bitvectorType bs
      assertInBounds sym off bs mem
      p <- mkPtr sym off
      let ?recordLLVMAnnotation = \_ _ -> return ()
-     pval <- G.readMem sym knownNat Nothing p (bitvectorType bs) noAlignment (wasmMemHeap mem)
-     Partial.assertSafe sym pval >>= \case
+     pval <- G.readMem sym knownNat Nothing p tp noAlignment (wasmMemHeap mem)
+     Partial.assertSafe sym tp pval >>= \case
        LLVMValZero _ -> bvLit sym w (BV.zero w)
        LLVMValInt _ v | Just Refl <- testEquality (bvWidth v) w -> pure v
        _ -> panic "wasmLoadInt" ["type mismatch"]
@@ -222,7 +223,7 @@ wasmLoadFloat sym off mem =
      p <- mkPtr sym off
      let ?recordLLVMAnnotation = \_ _ -> return ()
      pval <- G.readMem sym knownNat Nothing p floatType noAlignment (wasmMemHeap mem)
-     Partial.assertSafe sym pval >>= \case
+     Partial.assertSafe sym floatType pval >>= \case
        LLVMValZero _ -> iFloatLitRational sym SingleFloatRepr 0
        LLVMValFloat SingleSize v -> pure v
        _ -> panic "wasmLoadFloat" ["type mismatch"]
@@ -239,7 +240,7 @@ wasmLoadDouble sym off mem =
      p <- mkPtr sym off
      let ?recordLLVMAnnotation = \_ _ -> return ()
      pval <- G.readMem sym knownNat Nothing p doubleType noAlignment (wasmMemHeap mem)
-     Partial.assertSafe sym pval >>= \case
+     Partial.assertSafe sym doubleType pval >>= \case
        LLVMValZero _ -> iFloatLitRational sym DoubleFloatRepr 0
        LLVMValFloat DoubleSize v -> pure v
        _ -> panic "wasmLoadDouble" ["type mismatch"]

I would expect assertSafe to uphold an invariant that if it is invoked with a particular StorageType tp on a NoErr, then the type of the underlying LLVMVal in the NoErr constructor should match tp. To test this invariant, I added an additional assertion in the NoErr case of assertSafe which checks this in the patch above. This assertion fails, however, when I run the crucible-llvm test suite:

Test suite crucible-llvm-tests: RUNNING...
Tests
  ...
  Memory
    ...
    smt array memory model (with constant indexing): FAIL
      Exception: You have encountered a bug in Crucible's implementation.
      *** Please create an issue at https://github.com/GaloisInc/crucible/issues
      
      %< --------------------------------------------------- 
        Revision:  5419ec4892fd829e361f946ea16075a8c7ee9777
        Branch:    master
        Location:  RGS assertSafe
        Message:   tp: bitvectorType 8
                   llvmValStorableType v: bitvectorType 1
      CallStack (from HasCallStack):
        panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.5-inplace:Lang.Crucible.Panic
        panic, called at src/Lang/Crucible/LLVM/MemModel/Partial.hs:329:8 in crucible-llvm-0.3-inplace:Lang.Crucible.LLVM.MemModel.Partial
      %< --------------------------------------------------- 
    smt array memory model:                          FAIL
      Exception: You have encountered a bug in Crucible's implementation.
      *** Please create an issue at https://github.com/GaloisInc/crucible/issues
      
      %< --------------------------------------------------- 
        Revision:  5419ec4892fd829e361f946ea16075a8c7ee9777
        Branch:    master
        Location:  RGS assertSafe
        Message:   tp: bitvectorType 8
                   llvmValStorableType v: bitvectorType 1
      CallStack (from HasCallStack):
        panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.5-inplace:Lang.Crucible.Panic
        panic, called at src/Lang/Crucible/LLVM/MemModel/Partial.hs:329:8 in crucible-llvm-0.3-inplace:Lang.Crucible.LLVM.MemModel.Partial
      %< ---------------------------------------------------

[RyanGlScott]

This type mismatch ultimately arises from writeMemWithAllocationCheck's use of assertSafe:

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
index 7f9ec7d5..c1f96a01 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -1247,7 +1247,7 @@ writeMemWithAllocationCheck is_allocated sym w gsym ptr tp alignment val mem = d
               =<< traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
 
             -- TODO! we're abusing assertSafe here a little
-            v <- Partial.assertSafe sym partial_byte
+            v <- Partial.assertSafe sym tp partial_byte
             case v of
               LLVMValInt _ byte
                 | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do

I'm sure I'm doing this wrong, but at the same time, I'm not sure what the correct way to compute the StorageType here should be.

[robdockins]

The bitvectorType of StorageType counts bytes, not bits. Maybe that got mixed up somewhere.

[robdockins]

OK, I've paged in what that code is doing. The type you pass into that particular assertSafe should be bitvectorType 1, as it's breaking down the value to be stored into individual bytes. The tp passed in as an argument there is the overall type of the read, and shouldn't be passed in here.

[RyanGlScott]

It turns out that just adding the option to read from unwritten memory is a pretty formidable task on its own, even without the proposed taxonomy of errors layered on top of it. I've submitted a draft PR for the former at #794, which doesn't quite work yet, but is getting closer.

[RyanGlScott]

In order to make the original program in #783 (comment) pass through Crux without failing, we'll need to avoid generating the following obligations:

• NoSatisfyingWrite:

  crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

  Lines 768 to 777 in 9cfcc7b

  	fallback0 tp l =
  	liftIO $
  	if readUnwrittenMemory ?memOpts
  	then Partial.totalLLVMVal sym <$> freshLLVMVal sym tp
  	else do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be
  	-- sure it always fails. But, because it's a variable, it won't be constant-folded away
  	-- and we can be relatively sure the annotation will survive.
  	b <- freshConstant sym emptySymbol BaseBoolRepr
  	Partial.Err <$>
  	Partial.annotateME sym mop (NoSatisfyingWrite tp l) b

  (This was done in crucible-llvm: Add readUnwrittenMemory option, use it in readMem' #794.)

• UnreadableRegion:

  crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

  Line 721 in 9cfcc7b

  Partial.attachMemoryError sym p1 mop UnreadableRegion =<<

• ReadBadAlignment:

  crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

  Line 722 in 9cfcc7b

  Partial.attachSideCondition sym p2 (UB.ReadBadAlignment (RV l) alignment) part_val

The latter two work by attaching additional Preds to a NoErr value, which later gets asserted. The first one, on the other hand, works in a different way—it uses a different code path to avoid the use of addProofObligation entirely. As a result, I'm having trouble figuring out a way to control whether or not obligations get asserted or not purely as a modification to the assertion API (like what is proposed in #783 (comment)), as the changes in #794 seem to require a completely different code path than the assertion API. Perhaps there's a cleaner way to express the first one that puts in back into the domain of the assertion API.

[robdockins]

Thinking about this some more, maybe we don't need (for now, at least) specific toggles for all the various kinds of errors here (e.g. bad alignment vs unreadable region). Perhaps it suffices to have a single toggle for all classes of memory load errors.

[RyanGlScott]

Now that #808 has landed, the only remaining task is to implement a taxonomy of errors, as suggested in #783 (comment). Since the original goal of this ticket was to implement what is now known as lax-loads-and-stores, I'll close this in favor of a new issue, #809.