SAW fails to match LLVM override involving top-level string constants

[RyanGlScott]

Consider the following C code:

// test.c
#include "stdint.h"
#include "stdbool.h"

void foo(uint8_t xs[4]);

void bar() {
    uint8_t xs[4] = {0,1,2,3};
    for (int i = 0; i < 10; ++i) {
        foo(xs);
    }
}

And Cryptol file:

// test.cry
foo : [4][8] -> [4][8]
foo xs = xs

And SAW spec:

// test.saw
let alloc_init ty v = do {
    p <- llvm_alloc ty;
    llvm_points_to p v;
    return p;
};

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

let foo_spec = do {
    (x, p_x) <- ptr_to_fresh "xs" (llvm_array 4 (llvm_int 8));

    llvm_execute_func [p_x];

    llvm_points_to p_x (llvm_term x);
};

let bar_spec = do {
    llvm_execute_func [];
};

import "test.cry";
m <- llvm_load_module "test.bc";

ov <- llvm_unsafe_assume_spec m "foo" foo_spec;
res <- llvm_verify m "bar" [ov] true bar_spec z3;

Surprisingly, SAW fails with:

``` $ ~/Software/saw-1.2/bin/saw test.saw [15:29:10.768] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw" [15:29:10.839] Assume override foo [15:29:10.841] Verifying bar ... [15:29:10.853] Simulating bar ... [15:29:10.854] Registering overrides for `foo` [15:29:10.854] variant `Symbol "foo"` [15:29:10.854] Matching 1 overrides of foo ... [15:29:10.854] Stack trace: "llvm_verify" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:30:8-30:19) Symbolic execution failed. Abort due to assertion failure: test.c:10:3: error: in bar All overrides failed during structural matching: * Name: foo Location: /home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:29:1 Argument types: - i8* Return type: Arguments: - concrete pointer: allocation = 6, offset = 0 at /home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:4:5 could not match specified value with actual value: actual (simulator) value: "\NUL\SOH\STX\ETX" specified value: fresh:xs#802 : [4][8] type of actual value: [4 x i8] type of specified value: [4 x i8] Stack frame bar Allocations: StackAlloc 7 0x4:[64] Mutable 4-byte-aligned test.c:9:11 StackAlloc 6 0x4:[64] Mutable 1-byte-aligned test.c:8:10 Writes: Indexed chunk: 7 |-> memset (7, 0x0:[64]) 0x0:[8] 0x4:[64] memcopy (6, 0x0:[64]) (5, 0x0:[64]) 0x4:[64] Base memory Allocations: GlobalAlloc 5 0x4:[64] Immutable 1-byte-aligned [global variable ] __const.bar.xs GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [defined function ] bar GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] foo GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.memcpy.p0i8.p0i8.i64 GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare Writes: Indexed chunk: 5 |-> *(5, 0x0:[64]) := "\NUL\SOH\STX\ETX" ```

In particular, note this part of the error message:

     could not match specified value with actual value:
       actual (simulator) value: "\NUL\SOH\STX\ETX"
       specified value:          fresh:xs#802 : [4][8]
       type of actual value:    [4 x i8]
       type of specified value: [4 x i8]

This is utterly bizarre, since the types of the actual and specified values are exactly the same! What's more, the specified value is a fresh variable, so it should have no issue matching against the actual value.

Ultimately, this is a bug in the logic that SAW's override matching logic. The key part is that the actual value is "\NUL\SOH\STX\ETX", an LLVM string literal. At the LLVM level, string literals are no different than other values of type [<N> x i8]—they're just a convenient way to write certain constants in a more compact way. At the crucible-llvm level, however, we perform an optimization where we represent these string constants as ByteString in a dedicated LLVMValString data constructor, which is separate from the more general LLVMValArray. SAW's override matching logic has a case for LLVMValArray, but it is missing a corresponding case for LLVMValString. As such, it falls through to this catch-all case that causes override matching to fail.

There is a similar bug where we have a case for LLVMValArray here, but not a corresponding LLVMValString case. As such, this will cause a slight variation of the spec above to fail to match:

// test.saw
let alloc_init ty v = do {
    p <- llvm_alloc ty;
    llvm_points_to p v;
    return p;
};

let foo_spec = do {
    let ty = llvm_array 4 (llvm_int 8);
    x <- llvm_fresh_expanded_val ty;
    p_x <- alloc_init ty x;

    llvm_execute_func [p_x];

    llvm_points_to p_x x;
};

let bar_spec = do {
    llvm_execute_func [];
};

import "test.cry";
m <- llvm_load_module "test.bc";

ov <- llvm_unsafe_assume_spec m "foo" foo_spec;
res <- llvm_verify m "bar" [ov] true bar_spec z3;

``` $ ~/Software/saw-1.2/bin/saw test.saw [15:39:09.379] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw" [15:39:09.423] Assume override foo [15:39:09.424] Verifying bar ... [15:39:09.432] Simulating bar ... [15:39:09.432] Registering overrides for `foo` [15:39:09.432] variant `Symbol "foo"` [15:39:09.432] Matching 1 overrides of foo ... [15:39:09.433] Stack trace: "llvm_verify" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:26:8-26:19) Symbolic execution failed. Abort due to assertion failure: test.c:10:3: error: in bar All overrides failed during structural matching: * Name: foo Location: /home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:25:1 Argument types: - i8* Return type: Arguments: - concrete pointer: allocation = 6, offset = 0 at /home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:4:5 could not match specified value with actual value: actual (simulator) value: "\NUL\SOH\STX\ETX" specified value: [fresh:_#802 : [8], fresh:_#803 : [8], fresh:_#804 : [8], fresh:_#805 : [8]] type of actual value: [4 x i8] type of specified value: [4 x i8] Stack frame bar Allocations: StackAlloc 7 0x4:[64] Mutable 4-byte-aligned test.c:9:11 StackAlloc 6 0x4:[64] Mutable 1-byte-aligned test.c:8:10 Writes: Indexed chunk: 7 |-> memset (7, 0x0:[64]) 0x0:[8] 0x4:[64] memcopy (6, 0x0:[64]) (5, 0x0:[64]) 0x4:[64] Base memory Allocations: GlobalAlloc 5 0x4:[64] Immutable 1-byte-aligned [global variable ] __const.bar.xs GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [defined function ] bar GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] foo GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.memcpy.p0i8.p0i8.i64 GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare Writes: Indexed chunk: 5 |-> *(5, 0x0:[64]) := "\NUL\SOH\STX\ETX" ```

      could not match specified value with actual value:
       actual (simulator) value: "\NUL\SOH\STX\ETX"
       specified value:          [fresh:_#802 : [8], fresh:_#803 : [8], fresh:_#804 : [8], fresh:_#805 : [8]]
       type of actual value:    [4 x i8]
       type of specified value: [4 x i8]

Both of these issues are easily fixed by adding LLVMValString cases. Patch incoming.