Unsound handling of alignment in llvm overrides

[brianhuffman]

Here is a pair of C functions that should not work: Function foo passes a non-aligned pointer to function write, so the symbolic simulation should fail when function write tries to write value x to memory.

#include <stdint.h>

void write (uint64_t *p, uint64_t x) {
	*p = x;
}

void foo (uint8_t *p, uint64_t x) {
	write((uint64_t *)(p + 1), x);
}

If we try to verify foo directly without an override for write, then symbolic simulation fails as expected:

bc <- llvm_load_module "alignment.bc";

let i8 = llvm_int 8;
let i64 = llvm_int 64;

foo_ov <-
  crucible_llvm_verify bc "foo" [] false
    do {
      p <- crucible_alloc (llvm_array 16 i8);
      b <- crucible_fresh_var "b" (llvm_array 16 i8);
      x <- crucible_fresh_var "x" i64;
      crucible_points_to p (crucible_term b);
      crucible_execute_func [p, crucible_term x];
      crucible_points_to p (crucible_term {{ take`{1} b # reverse (split x) # drop`{9} b }});
    }
    z3;

Symbolic execution failed.
Abort due to false assumption:
  Invalid memory store
  in write at /Users/huffman/Documents/saw/alignment.c:4:5
  Details:
  The region's alignment wasn't correct
    address (4, 0x1:[64])
    at type i64

But if we prove and use an override for write, then we can get the verification to go through:

bc <- llvm_load_module "alignment.bc";

let i8 = llvm_int 8;
let i64 = llvm_int 64;

write_ov <-
  crucible_llvm_verify bc "write" [] false
    do {
      p <- crucible_alloc i64;
      x <- crucible_fresh_var "x" i64;
      crucible_execute_func [p, crucible_term x];
      crucible_points_to p (crucible_term x);
    }
    z3;

foo_ov <-
  crucible_llvm_verify bc "foo" [write_ov] false
    do {
      p <- crucible_alloc (llvm_array 16 i8);
      b <- crucible_fresh_var "b" (llvm_array 16 i8);
      x <- crucible_fresh_var "x" i64;
      crucible_points_to p (crucible_term b);
      crucible_execute_func [p, crucible_term x];
      crucible_points_to p (crucible_term {{ take`{1} b # reverse (split x) # drop`{9} b }});
    }
    z3;

[21:29:37.453] Loading file "/Users/huffman/Documents/saw/alignment.saw"
[21:29:37.461] Verifying write ...
[21:29:37.461] Simulating write ...
[21:29:37.461] Checking proof obligations write ...
[21:29:37.461] Proof succeeded! write
[21:29:37.482] Verifying foo ...
[21:29:37.484] Simulating foo ...
[21:29:37.484] Registering overrides for `write`
[21:29:37.485]   variant `Symbol "write"`
[21:29:37.485] Matching 1 overrides of  write ...
[21:29:37.486] Branching on 1 override variants of write ...
[21:29:37.486] Applied override! write
[21:29:37.491] Checking proof obligations foo ...
[21:29:37.519] Proof succeeded! foo

Apparently, when we run an override, we aren't checking the alignment preconditions at all. We should fix that.

[brianhuffman]

I'm going to reopen this until we add a proper regression test for it.

[langston-barrett]

Closed via #750