Confusing error message when passing uninitialized memory that should be initialized

[nano-o]

In the following C example, f1 expects initialized memory but is passed uninitialized memory. SAW reports an error, but there is seemingly no indication in the output that uninitialized memory is the cause of the error. Moreover, I don't understand why HeapAlloc 4 is 1-byte-aligned and not 8-byte-aligned.

void f1(unsigned long * ptr);

void test_1(unsigned long * ptr) {
  f1(ptr);
}

m <- llvm_load_module "./test_1.o.bc";

let alloc_init ty v = do {
  p <- crucible_alloc ty;
  crucible_points_to p v;
  return p;
};

let ptr_to_fresh n ty = do {
  x <- crucible_fresh_var n ty;
  p <- alloc_init ty (crucible_term x);
  return (x, p);
};

let f1_spec = do { //expects initialized memory
  (_, ptr) <- ptr_to_fresh "ptr" (llvm_array 1 (llvm_int 8));
  crucible_execute_func [ptr];
};

let test_1_spec = do {
  ptr <- crucible_alloc (llvm_array 1 (llvm_int 8)); // an uninitialized long
  crucible_execute_func [ptr];
};

f1_ov <- crucible_llvm_unsafe_assume_spec m "f1" f1_spec;
_ <- crucible_llvm_verify m "test_1" [f1_ov] false test_1_spec abc;

[00:46:00.383] Matching 1 overrides of  f1 ...
[00:46:00.383] Stack trace:
"crucible_llvm_verify" (/workdir/tests/misc/test_1.saw:26:6-26:26):
Symbolic execution failed.
Abort due to false assumption:
  All overrides failed during structural matching:
*  Name: f1
   Location: /workdir/tests/misc/test_1.saw:25:10
   Argument types: 
   - i64*
   Return type: <void>
   Arguments:
   - concrete pointer: allocation = 4, offset = 0
   at /workdir/tests/misc/test_1.saw:5:3
   error when loading through pointer that appeared in the override's points-to precondition(s):
   Precondition:
     Pointer: concrete pointer: allocation = 4, offset = 0
     Pointee: ptr : [1][8]

     Assertion made at: /workdir/tests/misc/test_1.saw:5:3
   Failure reason: 
     When reading through pointer: (4, 0x0:[64])
     in the  precondition of an override
     Tried to read something of size: 1
     And type: [1 x i8]
     Found 1 possibly matching allocation(s):
     - HeapAlloc 4 0x1:[64] Mutable 1-byte-aligned /workdir/tests/misc/test_1.saw:21:10
  in test_1 at /workdir/tests/misc/test_1.c:4:3
Stack frame
  Allocations:
    StackAlloc 5 0x8:[64] Mutable 8-byte-aligned "/workdir/tests/misc/test_1.c:3:29"
  Writes:
    Indexed chunk:
      5 |->
        *(5, 0x0:[64]) := (4, 0x0:[64])
Base memory
  Allocations:
    HeapAlloc 4 0x1:[64] Mutable 1-byte-aligned /workdir/tests/misc/test_1.saw:21:10
    GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned test_1
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned f1
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned llvm.dbg.declare
  Writes:

[nano-o]

Another information that would be useful here is the C source file and line number of the call site for which no override applies.

[brianhuffman]

The line ptr <- crucible_alloc (llvm_array 1 (llvm_int 8)); // an uninitialized long is actually not allocating a value of type long, as the comment suggests; it's allocating an 8-bit integer, which should have 1-byte alignment.