Bitfield-related proof works with llvm_alloc, but not llvm_alloc_readonly

[RyanGlScott]

This SAW proof works with a sufficiently recent nightly build of SAW, as expected:

// test.c
struct s {
  unsigned x:1;
  unsigned y:1;
};

int f(const struct s *ss) {
  return ss->x == ss->y;
}

// test.saw
enable_experimental;
enable_lax_loads_and_stores;

let f_spec = do {
  ss <- llvm_alloc (llvm_alias "struct.s");
  x <- llvm_fresh_var "x" (llvm_int 1);
  y <- llvm_fresh_var "y" (llvm_int 1);
  llvm_points_to_bitfield ss "x" (llvm_term x);
  llvm_points_to_bitfield ss "y" (llvm_term y);

  llvm_execute_func [ss];

  llvm_return (llvm_term {{ if x == y then 1 else 0 : [32] }});
};

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

$ clang -O0 test.c -emit-llvm -g -c
$ ~/Software/saw-0.9.0.99-Linux-x86_64/bin/saw test.saw


[14:29:54.577] Loading file "/home/rscott/Documents/Hacking/SAW/test.saw"
[14:29:54.612] Verifying f ...
[14:29:54.613] Simulating f ...
[14:29:54.615] Checking proof obligations f ...
Calling Yices to check sat
Running check sat
[14:29:54.617] Proof succeeded! f

If I change the use of llvm_alloc to llvm_alloc_readonly in f_spec, however, then the proof fails:

$ ~/Software/saw-0.9.0.99-Linux-x86_64/bin/saw test.saw


[14:32:29.646] Loading file "/home/rscott/Documents/Hacking/SAW/test.saw"
[14:32:29.682] Verifying f ...
[14:32:29.682] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/SAW/test.saw:18:7-18:18):
When reading through pointer: (3, 0x0:[64])
in the  precondition of an override
Tried to read something of size: 1
And type: i8
Found 1 possibly matching allocation(s):
- HeapAlloc 3 0x4:[64] Immutable 1-byte-aligned /home/rscott/Documents/Hacking/SAW/test.saw:6:9

I don't see any reason why this should fail, so this smells like a SAW bug. I will investigate.

[RyanGlScott]

Here is what I believe is happening here:

• llvm_alloc and llvm_alloc_readonly invoke crucible-llvm's doMalloc function, which has a special case for lax-loads-and-stores here. In particular, note that this special case only happens if mut == Mutable. Since llvm_alloc uses Mutable and llvm_alloc_readonly uses Immutable, the special case occurs for the former command but not the latter.

• What happens if you remove the mut == Mutable check? I tried, but that doesn't quite work either, since every llvm_points_to{,_bitfield} statement after an llvm_alloc_readonly will fail thusly:

  [15:44:08.794] Loading file "/home/rscott/Documents/Hacking/SAW/test.saw"
  [15:44:08.829] Verifying f ...
  [15:44:08.829] Simulating f ...
  [15:44:08.831] Checking proof obligations f ...
  Calling Yices to check sat
  Running check sat
  [15:44:08.833] Subgoal failed: f internal: error: in _SAW_verify_prestate
  Memory store failed
  Details:
    The region wasn't allocated, wasn't large enough, or was marked as readonly
  [15:44:08.833] SolverStats {solverStatsSolvers = fromList ["W4 ->yices"], solverStatsGoalSize = 29}
  [15:44:08.833] ----------Counterexample----------
  [15:44:08.833] <<All settings of the symbolic variables constitute a counterexample>>
  [15:44:08.833] ----------------------------------
  [15:44:08.833] Stack trace:
  "llvm_verify" (/home/rscott/Documents/Hacking/SAW/test.saw:18:7-18:18):
  Proof failed.
  

  I believe the reason this happens is because when memory in crucible-llvm is marked as Immutable, it can only be written to once. The special lax-loads-and-stores case writes symbolic bytes to the memory, which means that the subsequent llvm_points_to statement would constitute an additional write (at least, from crucible-llvm's perspective), leading to an assertion failure.

I'm not quite sure what to do about this. We need to write symbolic bytes to structs with bitfields to ensure that fields in a bitfield can successfully be loaded. On the other hand, writing symbolic bytes prevents other subsequent writes from happening. Is there a way to resolve this tension?

[RyanGlScott]

One possible solution to this problem (which may be half-baked):

• First, don't change the special case in doMalloc at all.
• Second, whenever we use llvm_alloc_readonly, SAW keeps track of the fact that the memory is immutable here in an LLVMAllocSpec. When executing an llvm_points_to_bitfield statement, if the LLVMAllocSpec for the corresponding pointer's memory is immutable, then we avoid loading the bytes in the bitfield. Instead, we simply create fresh bytes of the appropriate size, do the necessary bit-twiddling to write the values into these bytes, and then store the resulting value into the bitfield. This avoids both issues: we no longer load uninitialized memory and we only write to immutable memory once.

[RyanGlScott]

Actually, the idea in #1691 (comment) isn't baked at all, as it wouldn't even work on the simple test case in #1691 (comment). This is because each llvm_points_to_bitfield statement would store fresh bytes into the bitfield, which has the potential to overwrite the results of previous llvm_points_to_bitfield statements. To see how this works, recall the case case:

let f_spec = do {
  ss <- llvm_alloc (llvm_alias "struct.s");
  x <- llvm_fresh_var "x" (llvm_int 1);
  y <- llvm_fresh_var "y" (llvm_int 1);
  llvm_points_to_bitfield ss "x" (llvm_term x);
  llvm_points_to_bitfield ss "y" (llvm_term y);
  
  ...
  
};

1. The first llvm_points_to_bitfield statement would write a fresh byte to the bitfield in ss, but with the first bit set to the value of x.
2. The second llvm_points_to_bitfield statement would write another fresh byte to the bitfield in ss, but with the second bit set to the value of y. Note that because we allocated a fresh byte instead of loading it from memory, the first bit in the bitfield is a new, symbolic bit. Moreover, this bit has no relationship with the value of x, so this symbolic bit will completely overwrite the result of the first llvm_points_to_bitfield statement. Eek!

In short, the idea in #1691 (comment) is completely unworkable.

---

Thankfully, it turns out that there is a less hacky way to solve this. My analysis in #1691 (comment) was incorrect in the sense that Immutable memory in crucible-llvm can be written to multiple times. In order to do so, however, you need to use special memory model functions prefixed with -Const (e.g., storeConstRaw). crucible-llvm's doStoreStableSymbolic function, which powers lax-loads-and-stores, uses doArrayStore instead of doArrayConstStore, which is the real source of the problem. I've opened GaloisInc/crucible#1004 on the crucible side to fix this bug.

[RyanGlScott]

GaloisInc/crucible#1004 has been merged upstream, so all that remains is to bump the crucible submodule in saw-script and add a test case.