CBMC contracts crash when dynamic allocation is not in the harness.

[jaisnan]

CBMC currently needs free to be in scope. In order to enforce this, Kani currently creates an empty Box before to force free to be in scope.

The workaround on Kani's side looks like this,

// Filling the body of a contract
pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
    let args = proc_macro2::TokenStream::from(attr);
    let ItemFn { attrs, vis, sig, block } = parse_macro_input!(item as ItemFn);
    quote!(
        #[allow(dead_code)]
        #[kanitool::proof_for_contract = stringify!(#args)]
        #(#attrs)*
        #vis #sig {
            let _ = std::boxed::Box::new(0_usize);
            #block
        }
    )
    .into()
}

When we remove the culprit line let _ = std::boxed::Box::new(0_usize);. We get the following error from CBMC:

error: test failed: expected output to contain the line(s):
Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0
status: exit status: 1
command: "kani" "/home/ubuntu/kani/tests/expected/function-contract/gcd_rec_contract_fail.rs" "-Zfunction-contracts"
stdout:
------------------------------------------
Kani Rust Verifier 0.52.0 (standalone)
Reading GOTO program from '/home/ubuntu/kani/tests/expected/function-contract/gcd_rec_contract_fail__RNvCsjbTzZZm4LvF_21gcd_rec_contract_fail14simple_harness.out'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
Contract '_RNvCsjbTzZZm4LvF_21gcd_rec_contract_fail18gcd_wrapper_7a7962' not found, deriving empty pure contract 'contract::_RNvCsjbTzZZm4LvF_21gcd_rec_contract_fail18gcd_wrapper_7a7962' from function '_RNvCsjbTzZZm4LvF_21gcd_rec_contract_fail18gcd_wrapper_7a7962'
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
file <builtin-library-__CPROVER_contracts_library> line 1048 function __CPROVER_contracts_write_set_deallocate_freeable: no body for function 'free'
No body for 'free' during inlining
Numeric exception : 0
error: goto-instrument exited with status exit status: 6

CBMC version: 5.95.1
Operating system: Both Ubuntu 22.04.4
Exact command line resulting in the issue:
"kani" "/home/ubuntu/kani/tests/expected/function-contract/gcd_rec_contract_fail.rs" "-Zfunction-contracts"

[tautschnig]

I am sorry, I don't understand how to reproduce this. Where can I find that let _ = std::boxed::Box::new(0_usize); that needs to be removed in order to observe the problem?

[remi-delmas-3000]

Contracts instrumentation attempts to load free from the CPROVER library no matter what the GOTO model contains

CF here:

cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

Line 278 in 2a5151c

void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)

The contracts instrumentation assumes that if an entry for a library function like free is found in the symbol table then the body of the function is present too, and it doesn't attempt to force-load the function. So the only way contracts would not load the free function into the model is if the symbol table produced by Kani contains an entry for the free function but does not contain the body of the function.

[tautschnig]

The output mentioning builtin-library-free suggests it is loaded, so I’m quite confused what is actually going on here. Needs details to reproduce and debug.

[remi-delmas-3000]

This is an extract of kani_lib.c

// Declare functions instead of importing more headers in order to avoid conflicting definitions.
// See https://github.com/model-checking/kani/issues/1774 for more details.
void  free(void *ptr);
void *memcpy(void *dst, const void *src, size_t n);
void *calloc(size_t nmemb, size_t size);

Could these declarations result in an entry being present for free in the symbol table but the value of the symbol being absent ? or the entry being present but the GOTO function being pruned if its not actually used before contracts instrumentation is applied ?

[tautschnig]

file <builtin-library-free> really suggests that we are reading (using?) the definition from CBMC's library, though admittedly this is part of a warning, so it could be that we don't actually link in the implementation. So, still, we need a way to actually reproduce this.