Overrides fail with bad pointer loads for functions with locally allocated arrays

[WeeknightMVP]

In this example, we have a C file which exports two functions (xor_static and xor_local) that each run XOR in place on output dst with input src, such that dst' = dst ^ src. Each function calls an auxiliary method _xor_aux, which copies src into a provided tmp array and then XORs dst with tmp. The only difference between the exported functions is that xor_static allocates tmp statically, whereas xor_local allocates it locally.

SAW can verify both methods without overrides, but can only apply the override for _xor_aux to verify xor_static; trying to override it for xor_local fails due to a bad pointer load...

// Example.c

#define BUF_LEN 4

static void _xor_aux(unsigned char * dst, const unsigned char * src, unsigned char * tmp, size_t len) {
    for (size_t i = 0; i < len; i++) {
        tmp[i] = src[i];
    }

    for (int i = 0; i < BUF_LEN; i++) {
        dst[i] ^= tmp[i];
    }
}

void xor_static(unsigned char * dst, const unsigned char * src) {
    static unsigned char tmp[BUF_LEN];
    _xor_aux(dst, src, tmp, BUF_LEN);
}

void xor_local(unsigned char * dst, const unsigned char * src) {
    unsigned char tmp[BUF_LEN];
    _xor_aux(dst, src, tmp, BUF_LEN);
}

// Example.saw

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 {{
    type size_t = [64]
    type BUF_SIZE = 4
}};

let BUF_SIZE = (eval_int {{ `BUF_SIZE:size_t }});
let void_ptr w = (llvm_array w (llvm_int 8));

let _xor_aux_setup (len:Int) : CrucibleSetup () = do {
    (dst, p_dst) <- ptr_to_fresh "dst" (void_ptr len);
    (src, p_src) <- ptr_to_fresh "src" (void_ptr len);
    (tmp, p_tmp) <- ptr_to_fresh "tmp" (void_ptr len);

    let v_src = crucible_term {{ src }};
    let v_len = crucible_term {{ `len:size_t }};

    crucible_execute_func [p_dst, p_src, p_tmp, v_len];

    crucible_points_to p_dst (crucible_term {{ dst ^ src }});
    crucible_points_to p_src (crucible_term {{ src }});
    crucible_points_to p_tmp (crucible_term {{ src }});
};

let xor_setup : CrucibleSetup () = do {
    (dst, p_dst) <- ptr_to_fresh "dst" (void_ptr BUF_SIZE);
    (src, p_src) <- ptr_to_fresh "src" (void_ptr BUF_SIZE);

    crucible_execute_func [p_dst, p_src];

    crucible_points_to p_dst (crucible_term {{ dst ^ src }});
    crucible_points_to p_src (crucible_term {{ src }});
};

let main : TopLevel () = do {
    print "*** Loading Example.bc... ***";
    Example <- llvm_load_module "Example.bc";
    print Example;

    print "*** Verifying _xor_aux... ***";
    _xor_aux_thm <- crucible_llvm_verify Example "_xor_aux" [] false (_xor_aux_setup BUF_SIZE) abc;

    print "*** Verifying xor_static without overrides... ***";
    xor_static_thm <- crucible_llvm_verify Example "xor_static" [] false xor_setup abc;

    print "*** Verifying xor_static using override for _xor_aux... ***";
    xor_static_using_override_thm <- crucible_llvm_verify Example "xor_static" [ _xor_aux_thm ] false xor_setup abc;

    print "*** Verifying xor_local without overrides... ***";
    xor_local_thm <- crucible_llvm_verify Example "xor_local" [] false xor_setup abc;

    print "*** Verifying xor_local using override for _xor_aux... ***";
    xor_local_using_override_thm <- crucible_llvm_verify Example "xor_local" [ _xor_aux_thm ] false xor_setup abc;

    print "*** Example verified. ***";
};

>clang -c -emit-llvm Example.c
>saw Example.saw
Loading file "Example.saw"
*** Loading Example.bc... ***
Module: Example.bc
Types:

Globals:
  @xor_static.tmp = internal default global [4 x i8]

External references:

Definitions:
  void @xor_static(i8* %dst, i8* %src)
  internal void @_xor_aux(i8* %dst, i8* %src, i8* %tmp, i64 %len)
  void @xor_local(i8* %dst, i8* %src)


*** Verifying _xor_aux... ***
Proof succeeded! _xor_aux
*** Verifying xor_static without overrides... ***
Proof succeeded! xor_static
*** Verifying xor_static using override for _xor_aux... ***
Registering override for `_xor_aux`
Proof succeeded! xor_static
*** Verifying xor_local without overrides... ***
Proof succeeded! xor_local
*** Verifying xor_local using override for _xor_aux... ***
Registering override for `_xor_aux`
All overrides failed: [BadPointerLoad "Invalid memory load: address (9, 0x0:[64]) at type [4 x i8]"]
in xor_local at internal
  When calling _xor_aux
  In xor_local at internal
user error ("crucible_llvm_verify" (Example.saw:64:37-64:57):
Symbolic execution failed.
All overrides failed: [BadPointerLoad "Invalid memory load: address (9, 0x0:[64]) at type [4 x i8]"]
in xor_local at internal
Stack frame
  Allocations:
    StackAlloc 9 0x4:[64] Mutable "internal"
    StackAlloc 8 0x8:[64] Mutable "internal"
    StackAlloc 7 0x8:[64] Mutable "internal"
  Writes:
    *(8, 0x0:[64]) := (5, 0x0:[64])
    *(7, 0x0:[64]) := (6, 0x0:[64])
Base memory
  Allocations:
    HeapAlloc 6 0x4:[64] Mutable <malloc>
    HeapAlloc 5 0x4:[64] Mutable <malloc>
    GlobalAlloc 4 0x4:[64] Mutable xor_static.tmp
    GlobalAlloc 3 0x0:[64] Mutable xor_static
    GlobalAlloc 2 0x0:[64] Mutable xor_local
    GlobalAlloc 1 0x0:[64] Mutable _xor_aux
  Writes:
    *(5, 0x0:[64]) := [c@128:bv
                      ,c@129:bv
                      ,c@130:bv
                      ,c@131:bv]
    *(6, 0x0:[64]) := [c@124:bv
                      ,c@125:bv
                      ,c@126:bv
                      ,c@127:bv]
    *(4, 0x0:[64]) := [0x0:[8]
                      ,0x0:[8]
                      ,0x0:[8]
                      ,0x0:[8]]
)

[brianhuffman]

This example fails because the spec for _xor_aux is too restrictive. In _xor_aux_setup you have the line

    (tmp, p_tmp) <- ptr_to_fresh "tmp" (void_ptr len);

which declares that p_tmp should be a pointer to initialized memory containing the value tmp. So when the function override runs, it tries to read the input value tmp from the pointer p_tmp. However, xor_local calls _xor_aux with a pointer to an uninitialized memory area, so the read fails. On the other hand, xor_static works because the static local tmp is compiled as a global variable, which is implicitly zero-initialized.

Everything works if you replace the above line in _xor_aux_setup with

    p_tmp <- crucible_alloc (void_ptr len);

We could probably improve the error message. In particular, it would be nice if we had a little more detail than just "Invalid memory load". We should at least differentiate between loading from an out-of-bounds offset vs. reading uninitialized memory.

[langston-barrett]

See also #366.

[brianhuffman]

I'm closing, as there doesn't seem to be anything to do here. I believe the error messages for failed memory reads in llvm_verify are quite detailed now. (But feel free to reopen or make a new ticket if the error messages are still in need of improvement.)