llvm_verify crashes (Prelude.tail: empty list) when verifying a function whose name contains "__breakpoint__" without a # afterwards

[RyanGlScott]

Consider the following variant of the test0041_invariant_1 test case:

// test.c
#include <stdlib.h>

extern size_t __breakpoint__inv(size_t*);

size_t add2(size_t x) {
  ++x;
  __breakpoint__inv(&x);
  ++x;
  return x;
}

// test.saw
m <- llvm_load_module "test.bc";

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

let add2_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 64);
  llvm_execute_func [llvm_term x];
  llvm_return (llvm_term {{ x + 2 }});
};

let inv_spec = do {
  (px, x) <- ptr_to_fresh "x" (llvm_int 64);
  llvm_execute_func [px];
  llvm_return (llvm_term {{ x + 1 }});
};

inv <- llvm_verify m "__breakpoint__inv#add2" [] false inv_spec abc;
inv2 <- llvm_verify m "__breakpoint__inv" [] false inv_spec abc;

This SAW script uses the inv_spec twice: once to verify a function named __breakpoint__inv#add2, and once more to verify a function named __breakpoint__inv. The former succeeds, but the latter causes SAW to crash:

$ clang test.c -g -emit-llvm -c
$ ~/Software/saw-1.1/bin/saw test.saw
[12:52:07.373] Loading file "/home/ryanglscott/Documents/Hacking/Haskell/saw-script/test.saw"
[12:52:07.416] Verifying __breakpoint__inv ...
[12:52:07.416] Simulating __breakpoint__inv ...
[12:52:07.417] Checking proof obligations __breakpoint__inv ...
[12:52:07.469] Proof succeeded! __breakpoint__inv
[12:52:07.507] Verifying __breakpoint__inv ...
[12:52:07.507] Simulating __breakpoint__inv ...
[12:52:07.507] Prelude.tail: empty list

From my reading of this code, llvm_verify has a requirement that if the name of the function being verified contains "__breakpoint__", then the function must end with "#<parent_name>", where <parent_name> is the name of the function that contains the breakpoint. Unfortunately, this requirement is not documented anywhere (as far as I can tell), and the error message that SAW produces when you violate this requirement (Prelude.tail: empty list) is rather poor. We should fix the documentation and improve the error message.