"Pointer is not a function pointer"

[weaversa]

#include <stdint.h>
#include <string.h>
#include <stdlib.h>

uint32_t f() {
  uint32_t *x	= malloc(1 * sizeof(uint32_t));
  memset(x, 0, 1 * sizeof(uint32_t));
  uint32_t y = x[0];
  free(x);
  return y;
}

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

test_bc <- llvm_load_module "test.bc";

f_result <- crucible_llvm_verify test_bc "f" [] true f_spec z3;

$ clang -g -O0 test.c -o test.bc -emit-llvm -c && saw test.saw
[00:39:45.262] Loading file "test.saw"
[00:39:45.287] Verifying f ...
[00:39:45.287] Simulating f ...
[00:39:45.290] "crucible_llvm_verify" (test.saw:8:13-8:33):
Symbolic execution failed.
Abort due to false assumption:
  Pointer is not a function pointer:
(4, 0x0:[64])
  in f at test.c:7:3
Stack frame
  Allocations:
    HeapAlloc 9 0x4:[64] Mutable 16-byte-aligned test.c:6:17
    StackAlloc 8 0x4:[64] Mutable 4-byte-aligned "test.c:8:12"
    StackAlloc 7 0x8:[64] Mutable 8-byte-aligned "test.c:6:13"
  Writes:
    
Base memory
  Allocations:
    GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned f
    GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned free
    GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned llvm.objectsize.i64.p0i8
    GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned __memset_chk
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned malloc
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned llvm.dbg.declare
  Writes:

What function pointer?

I've only gotten this error when using memset, and only when passing in an array to f or mallocing an array (as I did above). If I give a stack allocated array uint32_t x[1] to memset then saw does not complain.

Also, there is a printing inconsistency --- HeapAlloc does not put quotes around the filename whereas StackAlloc does, and the stuff at the beginning uses parens around the filename.

[atomb]

We should really improve the error message here. What it should be is something like call to undefined external function llvm.objectsize.i64.p0i8. In the meantime, the trick to tracking this down is that the pointer (4, 0x0:[64]) means "offset 0 from allocation ID 4". Down in the "Allocations" section below you can see that GlobalAlloc 4 is the global variable containing the pointer to the function llvm.objectsize.i64.p0i8. I'm wondering whether that LLVM intrinsic has changed types again in recent LLVM versions. We have two different types for it in our LLVM support modules already, because it changed types once in the past.

[weaversa]

I'm having the same problem with memcpy.

[atomb]

Which version of Clang are you using?

[weaversa]

I just updated to the latest xcode...so you're probably right that the latest LLVM has some tweaks that break things.

$ clang --version
Apple clang version 11.0.3 (clang-1103.0.32.59)
Target: x86_64-apple-darwin19.4.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

[atomb]

I've just confirmed that I can replicate this using the latest Xcode. I think it should be easy to fix.

[atomb]

The specific example listed here works now, but the error message is still misleading.

[robdockins]

The error message should get the metadata about the pointer, so we can at least see what the symbol we tried to call was.

[robdockins]

Current status: the specific problem that started this thread has been solved. If I deliberately call an external function that does not have an override, I get a message saying "no implementation or override found", and a useful source location, but it still doesn't tell me what function it tried to call.

[robdockins]

Some fixes to the pretty printers in GaloisInc/crucible#574 should fix this bug.

[atomb]

The error message seems good now.