Print concrete override precondition failures

[langston-barrett]

Progress on #414.

Here's what the message looks like now:

  No override specification applies for SHA256_Init.
  The following overrides had some preconditions  that failed concretely:
  
  - Name: SHA256_Init
    Location: /build/fizz-hkdf/main.saw:127:19
    Argument types: 
      %struct.SHA256state_st*
    Return type: i32
    * global initializer equality precondition for global sha256_md
      in _SAW_verify_prestate at /build/fizz-hkdf/main.saw:127:19
    * global initializer equality precondition for global allow_customize
      in _SAW_verify_prestate at /build/fizz-hkdf/main.saw:127:19
  in overrideBranches at /build/fizz-hkdf/main.saw:190:1

re: the redundancy in the line numbers, see #415

[langston-barrett]

The error messages now include the expected and actual values. These are a little more unwieldy than I'd like...

[atomb]

Do you have an example of unwieldy values? I'm inclined to merge this regardless, as it's probably more useful than what we currently have.

[langston-barrett]

Here's another example. To get an unwieldy message, you can change the global to a big struct. I'll do that in a minute and post the result here:

/*
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; clang_7" --run "clang -O0 -emit-llvm -c *.c"
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; llvm_7" --run "llvm-dis *.bc"
*/

int z = 4;

int f(int x) {
  return x + x;
}

int g(int x) {
  z = 3;
  return f(f(x));
}

int main() {
  return g(5);
}

m <- llvm_load_module "test.bc";

let init_global name = do {
  crucible_points_to (crucible_global name) (crucible_global_initializer name);
};

let f_spec = do {
  init_global "z";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 2 * x : [32] }});
};

let g_spec = do {
  init_global "z";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 4 * x : [32] }});
};

f_spec <- crucible_llvm_verify m "f" [] false f_spec z3;
crucible_llvm_verify m "g" [f_spec] false g_spec z3;

Loading file "/home/siddharthist/code/tmp/test.saw"
Proof succeeded! f
Registering override for `f`
  variant `f`
"crucible_llvm_verify" (/home/siddharthist/code/tmp/test.saw:22:1-22:21):
Symbolic execution failed.
Abort due to false assumption:
  No override specification applies for f.
  The following overrides had some preconditions that failed concretely:
  - Name: f
    Location: /home/siddharthist/code/tmp/test.saw:21:11
    Argument types: 
      i32
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(z)
      Actual value: 
      literal integer: unsigned value = 3, signed value = 3, width = 32
      in _SAW_verify_prestate at /home/siddharthist/code/tmp/test.saw:21:11
  in overrideBranches at /home/siddharthist/code/tmp/test.saw:22:1
Stack frame
  Allocations:
    StackAlloc 5 0x4:[64] Mutable "internal"
  Writes:
    *(4, 0x0:[64]) := 0x3:[32]
    *(5, 0x0:[64]) := c@8:bv
Base memory
  Allocations:
    GlobalAlloc 4 0x4:[64] Mutable z
    GlobalAlloc 3 0x0:[64] Immutable main
    GlobalAlloc 2 0x0:[64] Immutable g
    GlobalAlloc 1 0x0:[64] Immutable f
  Writes:
    *(4, 0x0:[64]) := 0x4:[32]

[langston-barrett]

If we change the global in the above example to be a struct, we get something like the following. Extrapolating to larger structs (e.g. those generated by clang++), you can see where the message might be a bit awkward.

struct foo {
  int u;
  long w;
  char o;
} foo;

Loading file "/home/siddharthist/code/tmp/test.saw"
Proof succeeded! f
Registering override for `f`
  variant `f`
"crucible_llvm_verify" (/home/siddharthist/code/tmp/test.saw:22:1-22:21):
Symbolic execution failed.
Abort due to false assumption:
  No override specification applies for f.
  The following overrides had some preconditions that failed concretely:
  - Name: f
    Location: /home/siddharthist/code/tmp/test.saw:21:11
    Argument types: 
      i32
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(z)
      Actual value: 
      {literal integer: unsigned value = 12, signed value = 12, width = 32
      ;literal integer: unsigned value = 32, signed value = 32, width = 64
      ;literal integer: unsigned value = 8, signed value = 8, width = 8}
      in _SAW_verify_prestate at /home/siddharthist/code/tmp/test.saw:21:11
  in overrideBranches at /home/siddharthist/code/tmp/test.saw:22:1
Stack frame
  Allocations:
    StackAlloc 6 0x4:[64] Mutable "internal"
  Writes:
    *(4, 0x0:[64]) := 0xc:[32]
    *(6, 0x0:[64]) := c@8:bv
Base memory
  Allocations:
    GlobalAlloc 5 0x18:[64] Mutable foo
    GlobalAlloc 4 0x18:[64] Mutable z
    GlobalAlloc 3 0x0:[64] Immutable main
    GlobalAlloc 2 0x0:[64] Immutable g
    GlobalAlloc 1 0x0:[64] Immutable f
  Writes:
    *(4, 0x0:[64]) := {base+0 = 0x22:[32]
                      ,base+8 = 0x20:[64]
                      ,base+16 = 0x8:[8]}

[langston-barrett]

@atomb Here's a better example of the unwieldy values:

  No override specification applies for EVP_DigestInit_ex.
  The following overrides had some preconditions that failed concretely:
  - Name: EVP_DigestInit_ex
    Location: /build/fizz-hkdf/digest.saw:149:3
    Argument types: 
      %struct.env_md_ctx_st*
      %struct.env_md_st*
      %struct.engine_st*
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(sha256_md)
      Actual value: 
      {literal integer: unsigned value = 672, signed value =  672, width = 32
      ;literal integer: unsigned value = 668, signed value =  668, width = 32
      ;literal integer: unsigned value = 32, signed value =  32, width = 32
      ;literal integer: unsigned value = 12, signed value =  12, width = 64
      ;concrete pointer: allocation = 512, offset = 0
      ;concrete pointer: allocation = 552, offset = 0
      ;concrete pointer: allocation = 510, offset = 0
      ;<zero : bitvectorType 8>
      ;<zero : bitvectorType 8>
      ;concrete pointer: allocation = 44, offset = 0
      ;concrete pointer: allocation = 45, offset = 0
      ;[literal integer: unsigned value = 6, signed value =  6, width = 32
       ,literal integer: unsigned value = 19, signed value =  19, width = 32
       ,<zero : bitvectorType 4>
       ,<zero : bitvectorType 4>
       ,<zero : bitvectorType 4>]
      ;literal integer: unsigned value = 64, signed value =  64, width = 32
      ;literal integer: unsigned value = 120, signed value =  120, width = 32
      ;<zero : bitvectorType 8>}
      in _SAW_verify_prestate at /build/fizz-hkdf/digest.saw:149:3