How to bridge a CPROVER function without an undefined assertion violation?

[zpzigi754]

I tried this code:

(in src/main.rs)

extern "C" {
    fn CPROVER_allocated_memory(address: usize, size: usize);
}

#[kani::proof]
fn main() {
    unsafe {
        CPROVER_allocated_memory(0x1000, 4);
    }
}

(in stub.c)

struct Unit CPROVER_allocated_memory(unsigned long address, unsigned long size) {
    __CPROVER_allocated_memory(address, size);
}

using the following command line invocation:

cargo kani --enable-unstable --c-lib stub.c

with Kani version:
0.18 (c135fa9)

I expected to see this happen: Verification successful.
I've confirmed that __CPROVER_allocated_memory() indeed affects the model by allocating the passed region.

Instead, this happened:

RESULTS:
Check 1: __CPROVER_allocated_memory.assertion.1
	 - Status: FAILURE
	 - Description: "undefined function should be unreachable"
	 - Location: <builtin-architecture-strings>:20 in function __CPROVER_allocated_memory


SUMMARY:
 ** 1 of 1 failed
Failed Checks: undefined function should be unreachable
 File: "<builtin-architecture-strings>", line 20, in __CPROVER_allocated_memory

VERIFICATION:- FAILED
Verification Time: 0.052587587s

I'm not sure why there is an assertion violation regarding undefined function here while the internal function (__CPROVER_allocated_memory()) seems to be linked well in the generated goto binary.

[zpzigi754]

It seems that passing the option --no-undefined-function-checks could bypass the above issue.

[zhassan-aws]

Thanks for reporting the issue @zpzigi754. I tried this with other CProver functions, and it worked fine without needing --no-undefined-function-checks:

test.rs:

extern "C" {
    fn CPROVER_assert(cond: bool);
}

#[kani::proof]
fn main() {
    unsafe {
        CPROVER_assert(1 == 1);
    }
}

stub.c:

struct Unit CPROVER_assert(_Bool cond) {
    __CPROVER_assert(cond, "Message");
}

$ kani test.rs --enable-unstable --c-lib stub.c 
Checking harness main...
CBMC 5.72.0 (cbmc-5.72.0)
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/iss2052/test.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.000644884s
size of program expression: 41 steps
slicing removed 20 assignments
Generated 1 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 1.883e-05s

RESULTS:
Check 1: CPROVER_assert.assertion.1
         - Status: SUCCESS
         - Description: "Message"
         - Location: stub.c:2 in function CPROVER_assert


SUMMARY:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.012643958s

Not sure if there's something special about __CPROVER_allocated_memory.

[tautschnig]

Yes, __CPROVER_allocated_memory is special (in an unhealthy way). There is a goal of removing it: diffblue/cbmc#6748 (and replacing it by a command-line option).

[zpzigi754]

@zhassan-aws and @tautschnig , thank you for the trial and information. I've also confirmed that the symptom did not appear when CPROVER_assert is used. It seems that only some of CPROVER functions have this issue. For example, bridging __CPROVER_mm_io_r also triggers the same behavior with __CPROVER_allocated_memory (an assertion violation regarding undefined function).