Override failure message could be more informative

[msaaltink]

With the C source

#include <stdint.h>

extern uint32_t foo(uint32_t *p);

uint32_t frob() {
  uint32_t a[10];
  return foo(a);
}

and with the SAWScript

m <- llvm_load_module "override.bc";

let foo_spec  = do {
  p <- crucible_alloc (llvm_array 11 (llvm_int 32));
  crucible_execute_func [p];
  crucible_return (crucible_term {{0:[32]}});
  };

let frob_spec  = do {
  crucible_execute_func [];
  crucible_return (crucible_term {{0:[32]}});
  };

foo_ov <- crucible_llvm_unsafe_assume_spec m "foo" foo_spec;
crucible_llvm_verify m "frob" [foo_ov] false frob_spec z3;

I have made a silly mistake: passing in a 10-element array to something expecting 11 elements. Running in SAW does fail, as you'd hope, but the error message is not very useful:

[15:26:10.534] Loading file "override.saw"
[15:26:10.559] Assume override foo
[15:26:10.578] Verifying frob ...
[15:26:10.578] Simulating frob ...
[15:26:10.578] Registering overrides for `foo`
[15:26:10.578]   variant `Symbol "foo"`
[15:26:10.578] Matching 1 overrides of  foo ...
[15:26:10.580] Branching on 0 override variants of foo ...
[15:26:10.581] Stack trace:
"crucible_llvm_verify" (override.saw:40:1-40:21):
Symbolic execution failed.
Abort due to false assumption:
  Could not parse acknowledgement result.
*** Exception: Parse exception: Failed reading: empty

  in overrideBranches at override.saw:40:1
Stack frame
  Allocations:
    StackAlloc 3 0x28:[64] Mutable 16-byte-aligned "internal"
  Writes:

Base memory
  Allocations:
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned frob
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned foo
  Writes:

I suppose that Branching on 0 override variants of foo tells me that the override failed to match, but surely SAW could be a bit more informative about the nature of the mismatch. It is not always so clear in the source code what the actual parameters in the call are.

[robdockins]

Thanks for the report. Agreed, that error message is not very helpful!

[robdockins]

In current master, I'm getting the following output, which clearly states the problem is that no override applied. I'm not exactly sure what's changed in the meantime, but I think we can close this.

[18:24:29.535] Loading file "/Users/rdockins/code/saw-script/override_msg/test.saw"
[18:24:29.561] Assume override foo
[18:24:29.575] Verifying frob ...
[18:24:29.575] Simulating frob ...
[18:24:29.575] Registering overrides for `foo`
[18:24:29.575]   variant `Symbol "foo"`
[18:24:29.575] Matching 1 overrides of  foo ...
[18:24:29.576] Branching on 0 override variants of foo ...
[18:24:29.576] Stack trace:
"crucible_llvm_verify" (/Users/rdockins/code/saw-script/override_msg/test.saw:15:1-15:21):
Symbolic execution failed.
Abort due to false assumption:
  /Users/rdockins/code/saw-script/override_msg/test.saw:15:1: error: in overrideBranches
  No override specification applies for foo.
Arguments:
- concrete pointer: allocation = 4, offset = 0
The following overrides had some preconditions that failed concretely:
- Name: foo
  Location: /Users/rdockins/code/saw-script/override_msg/test.saw:14:11
  Argument types:
  - i32*
  Return type: i32
  * /Users/rdockins/code/saw-script/override_msg/test.saw:14:11: error: in _SAW_verify_prestate
    Pointer not valid:
  base = (4, 0x0:[64])
  size = Prelude.bvNat 64 44
  required alignment = 4-byte
  required mutability = Mutable
Run SAW with --sim-verbose=3 to see a description of each override.
Stack frame "frob"
  Allocations:
    StackAlloc 4 0x28:[64] Mutable 16-byte-aligned "/Users/rdockins/code/saw-script/override_msg/test.c:6:12"
Base memory
  Allocations:
    GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [defined function ] frob
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] foo
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare