SAW error messages obscure names of LLVM functions that lack implementations

[RyanGlScott]

Sometimes, LLVM functions are declared without function bodies, which means that Crucible will abort if it tries to simulate them. When using a tool like Crux-LLVM to drive Crucible, the resulting error message pinpoints the declared function that is responsible, but SAW's equivalent of the same error message does not.

To better illustrate what I mean, consider the following C program and corresponding SAW spec:

// test.c
extern int foo(void);

int main(void) {
  return foo();
}

// test.saw
let main_spec = llvm_execute_func [];
m <- llvm_load_module "test.bc";
llvm_verify m "main" [] false main_spec z3;

This program declares foo as an extern function without defining it, so naturally, Crucible won't know what to do with it at the LLVM level either:

$ clang -g -emit-llvm test.c -c
$ clang -g -emit-llvm test.c -S
$ cat test.ll
; ModuleID = 'test.c'
source_filename = "test.c"
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 !dbg !10 {
  %1 = alloca i32, align 4
  store i32 0, i32* %1, align 4
  %2 = call i32 @foo(), !dbg !15
  ret i32 %2, !dbg !16
}

declare i32 @foo() #1

<snip>

If we run the main function through Crux-LLVM, here is the error message that we get:

$ ~/Software/crux-llvm-0.9/bin/crux-llvm test.bc --no-compile
[Crux] Using pointer width: 64 for file test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Found counterexample for verification goal
[Crux]   test.c:5:10: error: in main
[Crux]   Failed to load function handle
[Crux]   Details:
[Crux]     No implementation or override found for pointer
[Crux]     The given pointer could not be resolved to a callable function
[Crux]     No implementation or override found for pointer
[Crux]     Attempting to load callable function with type: i32()
[Crux]       Via pointer: Global symbol "foo" (1, 0x0:[64])
[Crux]     In memory state:
[Crux]       Stack frame main
[Crux]         Allocations:
[Crux]           StackAlloc 3 0x4:[64] Mutable 4-byte-aligned internal
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             3 |->   memset (3, 0x0:[64]) 0x0:[8] 0x4:[64]
[Crux]       Base memory
[Crux]         Allocations:
[Crux]           GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [defined function ] main
[Crux]           GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] foo
[Crux]     in context:
[Crux]       main

Note the Via pointer: Global symbol "foo" (1, 0x0:[64]) part, which clues us in to the function that is responsible for the error. If you try to simulate main using SAW, however, this is the error that you get:

$ ~/Software/saw-1.2/bin/saw test.saw
[20:50:29.822] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[20:50:29.825] Verifying main ...
[20:50:29.825] Simulating main ...
[20:50:29.825] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:4:1-4:12)
Symbolic execution failed.
Abort due to assertion failure:
  test.c:5:10: error: in main
  Failed to load function handle
  Details:
    No implementation or override found for pointer
Stack frame main
  No writes or allocations
Base memory
  Allocations:
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [defined function ] main
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] foo

This time, the error message is much more vague. It hints about No implementation or override found for pointer, but which one? The only mention of foo at all is in the LLVM memory at the bottom, but the connection between this function and the error message above is not at all obvious from a quick glance. (The connection is even less obvious if there are many external functions involved in the program, as is likely to be the case in larger programs.)

What is especially unfortunate here is that I think both Crux-LLVM and SAW are recorded the same type of Crucible error under the hood, but Crux-LLVM is choosing to display more information about the error than SAW is. As such, I think this is mostly a matter of error reporting rather than Crux-LLVM being more clever than SAW.

[RyanGlScott]

To expand upon this a little more, here is the code path that SAW uses to print its error message:

saw-script/src/SAWScript/Crucible/Common.hs

Lines 118 to 122 in 24c180f

	ppAbortedResult ppGP (AbortedExec abt gp) = do
	PP.vcat
	[ ppAbortExecReason abt
	, ppGP gp
	]

In turn, ppAbortExecReason is defined here in crucible:

ppAbortExecReason :: AbortExecReason -> PP.Doc ann
ppAbortExecReason e =
  case e of
    ...
    AssertionFailure err ->
      PP.vcat
      [ "Abort due to assertion failure:"
      , PP.indent 2 (ppSimError err)
      ]
    ...

And ppSimError is responsible for printing the indented messages following Abort due to assertion failure:.

The reason that Crux-LLVM is able to print more information in the indented messages is that when Crux-LLVM prints an error message, it does so using the explainCex function. This also calls ppSimError, but in addition, it also consults the LLVMAnnMap, which tracks all of the LLVM-related memory errors that are recorded during simulation. The LLVMAnnMap is what records the Via pointer: Global symbol "foo" (1, 0x0:[64]) bit, which is the crucible part of the Crux-LLVM error message.

I think that we should update SAW's error message machinery to do something closer to what Crux-LLVM is doing. At a minimum, SAW will need to update its LLVMAnnMap like Crux-LLVM does, i.e.,

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index fd1096125..40a967436 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -1780,7 +1780,11 @@ setupLLVMCrucibleContext pathSat lm action =
                           , Crucible.noSatisfyingWriteFreshConstant = noSatisfyingWriteFreshConstant
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
-          let ?recordLLVMAnnotation = \_ _ _ -> return ()
+          bbMapRef <- io $ newIORef (Map.empty :: Crucible.LLVMAnnMap sym)
+          let ?recordLLVMAnnotation =
+                \callStack an bb ->
+                  modifyIORef bbMapRef (Map.insert an (callStack, bb))
           let ?w4EvalTactic = W4EvalTactic { doW4Eval = what4Eval }
           let ?checkAllocSymInit = allocSymInitCheck
           cc <-

We will likely also need to record the bbMapRef somewhere so that it can be plumbed through to the part of SAW that reports error messages.

[langston-barrett]

I think that we should update SAW's error message machinery to do something closer to what Crux-LLVM is doing. At a minimum, SAW will need to update its LLVMAnnMap like Crux-LLVM does, i.e.,

IIRC, the ?recordLLVMAnnotation API was designed to explicitly make recording this extra information optional precisely because it ended up being a performance problem for SAW. The extra info contains views of the entire LLVM memory. I think it is even recorded in the case that the safety assertion is trivially OK. So I'd advise testing such a change against some hairy SAW proofs and especially taking a look at the memory usage.