Panic with enable_lax_loads_and_stores and nested structs

[RyanGlScott]

Given the following example, which requires a sufficiently recent nightly version of SAW:

// bug.c
#include <stdint.h>

struct a {
  uint16_t x;
  uint32_t y;
};

struct b {
  struct a aa;
};

void f(struct b *bb) {}

// bug.saw
enable_experimental;
enable_lax_loads_and_stores;

let f_spec = do {
  aa <- llvm_fresh_var "aa" (llvm_alias "struct.a");
  bb <- llvm_alloc (llvm_alias "struct.b");
  llvm_points_to (llvm_field bb "aa") (llvm_term aa);

  llvm_execute_func [bb];
};

m <- llvm_load_module "bug.bc";
llvm_verify m "f" [] false f_spec (w4_unint_yices []);

SAW will panic when the example is compiled and run as follows:

$ clang-10 bug.c -emit-llvm -g -c -o bug.bc
$ ~/Software/saw-0.9.0.99-Linux-x86_64/bin/saw bug.saw


[22:08:43.500] Loading file "/home/rscott/Documents/Hacking/SAW/bug.saw"
[22:08:43.504] Verifying f ...
[22:08:43.505] You have encountered a bug in Crucible's implementation.
*** Please create an issue at https://github.com/GaloisInc/crucible/issues

%< ---------------------------------------------------
  Revision:  d18505d1ad1fe03e142371359852b5f52ea0b1f0
  Branch:    HEAD
  Location:  wrietMemWithAllocationCheck
  Message:   Expected succesful byte load when updating SMT array
             but got an error instead
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/Generic.hs:1295:19 in crucible-llvm-0.3-inplace:Lang.Crucible.LLVM.MemModel.Generic
%< ---------------------------------------------------

Note that enable_lax_loads_and_stores is crucial to triggering this bug, as if it is commented out, then the proof will succeed.

[RyanGlScott]

I spent some time looking into this, and the culprit appears to be the way SMT-array-backed memory treats structs with padding. In particular, struct a values take up 8 bytes of space, but there are 2 bytes of padding between the x and y fields. When the crucible-llvm memory model attempts to update the array backing the aa field in a struct b value, it does so by doing a pointwise update of array indices in the array backing it. That is, it updates indices 0 through 7, corresponding to each of the 8 bytes that make up a struct a value.

The first two bytes correspond to the x field, which works as expected. The next two bytes corresponding to padding, however, and this is where things go awry. Here is the relevant case of crucible-llvm's loadBitvector function:

    Struct sflds -> assert (not (null r)) $ snd $ foldl1 cv r
      where cv (wx,x) (wy,y) = (wx+wy, concatBV wx x wy y)
            r = concat (zipWith val [0..] (V.toList sflds))
            val i f = v1
              where eo = so + fieldOffset f
                    ee = eo + storageTypeSize (f^.fieldVal)
                    v1 | le <= eo = v2
                       | ee <= lo = v2
                       | otherwise = retValue eo (FieldVal sflds i v) : v2
                    v2 | fieldPad f == 0 = []   -- Return no padding.
                       | le <= ee = [] -- Nothing of load ends before padding.
                         -- Nothing if padding ends before load begins.
                       | ee+fieldPad f <= lo = []
                       | otherwise = [(p, ValueCtorVar badMem)]
                      where p = min (ee+fieldPad f) le - (max lo ee)
                            tpPad  = bitvectorType p
                            badMem = InvalidMemory tpPad

If you squint, you'll see that attempting to load struct padding results in InvalidMemory. That, in turn, is treated as an error here:

            InvalidMemory tp'-> Partial.partErr sym mop $ Invalid tp'

And converted to a panic here:

              Partial.Err _ ->
                  panic "wrietMemWithAllocationCheck"
                         [ "Expected succesful byte load when updating SMT array"
                         , "but got an error instead"
                         ]

---

The question to answer, then, is what should this do? Given that the semantics of enable_lax_loads_and_stores is to treat uninitialized memory as containing symbolic bytes, it seems like this kind of thing should succeed. Would it suffice to skip the cases that return InvalidMemory in the event that enable_lax_loads_and_stores is enabled? Admittedly, I don't understand much of the code in Lang.Crucible.LLVM.MemModel.Common, so I'm not sure if doing that would have unintended consequences.

[robdockins]

I think the intent of "lax loads" is basically to make it so that invalid memory exceptions don't occur, so I think skipping that check when it is enabled feels like the right thing to do.

We should probably also downgrade that panic if we can; it can clearly be caused by legitimate user input.

[RyanGlScott]

I tried the following naïve fix in crucible-llvm:

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs
index 66e2de872..3cdadd993 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs
@@ -496,7 +496,10 @@ loadBitvector lo lw so v = do
                     v1 | le <= eo = v2
                        | ee <= lo = v2
                        | otherwise = retValue eo (FieldVal sflds i v) : v2
-                    v2 | fieldPad f == 0 = []   -- Return no padding.
+                    v2 | laxLoadsAndStores ?memOpts
+                       , indeterminateLoadBehavior ?memOpts == StableSymbolic
+                       = []
+                       | fieldPad f == 0 = []   -- Return no padding.
                        | le <= ee = [] -- Nothing of load ends before padding.
                          -- Nothing if padding ends before load begins.
                        | ee+fieldPad f <= lo = []

Unfortunately, that just changes the panic to... this:

[20:58:16.519] Loading file "/home/rscott/Documents/Hacking/SAW/bug.saw"
[20:58:16.524] Verifying f ...
[20:58:16.525] Prelude.foldl1: empty list

I'm presuming that the foldl1 in question comes from here. That being said, I'm not yet clear on why the list being passed to foldl1 is empty.

[RyanGlScott]

After reading the implementation of loadBitvector a bit more closely, I think it's actually fine for loadBitvector to return InvalidMemory in the case when struct padding is loaded. The important thing is to interpret InvalidMemory differently when enable_lax_loads_and_stores is on. With this in mind, this suggests a different way to fix the issue in writeMemWithAllocationCheck:

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
index 2a7e3a8b..74db4795 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -1259,15 +1259,21 @@ writeMemWithAllocationCheck is_allocated sym w gsym ptr tp alignment val mem = d
                            , case val of
                                LLVMValInt block _ -> (asNat block) == (Just 0)
                                _ -> True -> do
-      let subFn :: ValueLoad Addr -> IO (PartLLVMVal sym)
+      let subFn :: ValueLoad Addr -> IO (Maybe (PartLLVMVal sym))
           subFn = \case
-            LastStore val_view -> applyView
+            LastStore val_view -> fmap Just $ applyView
               sym
               (memEndianForm mem)
               mop
               (Partial.totalLLVMVal sym val)
               val_view
-            InvalidMemory tp'-> Partial.partErr sym mop $ Invalid tp'
+            InvalidMemory tp'
+              |  laxLoadsAndStores ?memOpts
+              ,  indeterminateLoadBehavior ?memOpts == StableSymbolic
+              -> pure Nothing
+
+              |  otherwise
+              -> fmap Just $ Partial.partErr sym mop $ Invalid tp'
             OldMemory off _ -> panic "Generic.writeMemWithAllocationCheck"
               [ "Unexpected offset in storage type"
               , "*** Offset:  " ++ show off
@@ -1279,32 +1285,39 @@ writeMemWithAllocationCheck is_allocated sym w gsym ptr tp alignment val mem = d
             Offset ->
             IO (SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))
           storeArrayByteFn acc_arr off = do
-            partial_byte <- genValueCtor sym (memEndianForm mem) mop
-              =<< traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
-
-            case partial_byte of
-              Partial.NoErr _ (LLVMValInt _ byte)
-                | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do
-                  idx <- bvAdd sym (llvmPointerOffset ptr)
-                    =<< bvLit sym w (bytesToBV w off)
-                  arrayUpdate sym acc_arr (Ctx.singleton idx) byte
-
-              Partial.NoErr _ (LLVMValZero _) -> do
-                  byte <- bvLit sym knownRepr (BV.zero knownRepr)
-                  idx <- bvAdd sym (llvmPointerOffset ptr)
-                    =<< bvLit sym w (bytesToBV w off)
-                  arrayUpdate sym acc_arr (Ctx.singleton idx) byte
-
-              Partial.NoErr _ v ->
-                  panic "wrietMemWithAllocationCheck"
-                         [ "Expected byte value when updating SMT array, but got:"
-                         , show v
-                         ]
-              Partial.Err _ ->
-                  panic "wrietMemWithAllocationCheck"
-                         [ "Expected succesful byte load when updating SMT array"
-                         , "but got an error instead"
-                         ]
+            ctor_mb <- traverse subFn (loadBitvector off 1 0 (ValueViewVar tp))
+            let mb_ctor = sequenceA ctor_mb
+            mb_partial_byte <- traverse (genValueCtor sym (memEndianForm mem) mop)
+                                        mb_ctor
+
+            case mb_partial_byte of
+              Nothing -> pure acc_arr
+              Just partial_byte ->
+                case partial_byte of
+                  Partial.NoErr _ (LLVMValInt _ byte)
+                    | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> do
+                      idx <- bvAdd sym (llvmPointerOffset ptr)
+                        =<< bvLit sym w (bytesToBV w off)
+                      arrayUpdate sym acc_arr (Ctx.singleton idx) byte
+
+                  Partial.NoErr _ (LLVMValZero _) -> do
+                      byte <- bvLit sym knownRepr (BV.zero knownRepr)
+                      idx <- bvAdd sym (llvmPointerOffset ptr)
+                        =<< bvLit sym w (bytesToBV w off)
+                      arrayUpdate sym acc_arr (Ctx.singleton idx) byte
+
+                  Partial.NoErr _ v ->
+                      panic "writeMemWithAllocationCheck"
+                             [ "Expected byte value when updating SMT array, but got:"
+                             , show v
+                             ]
+                  Partial.Err _ ->
+                      panic "writeMemWithAllocationCheck"
+                             [ "Expected succesful byte load when updating SMT array"
+                             , "but got an error instead"
+                             ]

       res_arr <- foldM storeArrayByteFn arr [0 .. (sz - 1)]
       overwriteArrayMem sym w ptr res_arr arr_sz mem

The key idea is that when we load a byte from a struct that corresponds to struct padding, we skip updating the corresponding byte in the SymArray. I've tested this patch locally and it appears to fix the issue, so I'll open a PR on the crucible side shortly for further discussion.