goto-instrument internal error with function pointers

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

A function takes a state struct which contains some hash data a pointer hash_impl to a struct containing pointers to some functions.

The contract requires that the state->hash_impl->digest is one of two possible static object defined in the C file.

The function under analysis just calls this function on the state return state->hash_impl->digest(state).

Analysing this contract triggers a goto-instrument error which prevents from analysing the function.

➜  s2n_hash_digest git:(function-contract-s2n_hash_digest-function-pointer-bug) goto-instrument  --enforce-contract s2n_hash_digest /Users/delmasrd/projects/private-s2n-cbmc/tests/cbmc/proofs/s2n_hash_digest/gotos/s2n_hash_digest_harness.c1.goto /Users/delmasrd/projects/private-s2n-cbmc/tests/cbmc/proofs/s2n_hash_digest/gotos/s2n_hash_digest_harness.c2.goto
Reading GOTO program from '/Users/delmasrd/projects/private-s2n-cbmc/tests/cbmc/proofs/s2n_hash_digest/gotos/s2n_hash_digest_harness.c1.goto'
--- begin invariant violation report ---
Invariant check failed
File: /Users/delmasrd/projects/cbmc/src/util/std_expr.h:200 function: to_symbol_expr
Condition: expr.id()==ID_symbol
Reason: Precondition
Backtrace:
0   goto-instrument                     0x0000000108395dea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   goto-instrument                     0x0000000108396382 _Z13get_backtracev + 210
2   goto-instrument                     0x0000000107df7c4c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   goto-instrument                     0x0000000107df7c19 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   goto-instrument                     0x00000001083adc0e _Z14to_symbol_exprR5exprt + 318
5   goto-instrument                     0x0000000107e328ec _ZN15code_contractst24check_for_looped_mallocsERK13goto_programt + 380
6   goto-instrument                     0x0000000107e32ed0 _ZN15code_contractst31check_frame_conditions_functionERK8dstringt + 192
7   goto-instrument                     0x0000000107e33bb1 _ZN15code_contractst16enforce_contractERK8dstringt + 33
8   goto-instrument                     0x0000000107e3819c _ZN15code_contractst17enforce_contractsERKNSt3__13setINS0_12basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEENS0_4lessIS7_EENS5_IS7_EEEE + 284
9   goto-instrument                     0x0000000107e7d2d5 _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 7797
10  goto-instrument                     0x0000000107e76fed _ZN30goto_instrument_parse_optionst4doitEv + 541
11  goto-instrument                     0x00000001083b2c1c _ZN19parse_options_baset4mainEv + 140
12  goto-instrument                     0x0000000107df73e8 main + 40
13  libdyld.dylib                       0x00007fff20438f5d start + 1


--- end invariant violation report ---
[1]    48780 abort      goto-instrument --enforce-contract s2n_hash_digest

Further comments:

The function under analysis just receives a state struct and there is no statement in the function that actually constructs a value for the state->hash_impl pointer. So we want to require declaratively that this function pointer can resolve to some element of a known set of functions, possibly depending on the value of returned by some other function. This seems is impossible to do today.

How to reproduce:

• using this branch
• run make report2 in tests/cbmc/proofs/s2n_evp_hash_digest
• the function contract in question is s2n_evp_hash_digest

[feliperodri]

@remi-delmas-3000 haven't you address this issue with the latest DFCC work?

[remi-delmas-3000]

This is supported by the __CPROVER_is_in_range predicate introduced in PR #7401

We can use this predicate to say that a pointer points to some object or some other object:

#include <stdbool.h>
#include <stdlib.h>

// A vtable is a struct containing function pointers
typedef struct vtable_s
{
  int (*f)(void);
} vtable_t;

int return_0()
{
  return 0;
}

int return_1()
{
  return 1;
}

// we have two possible vtables
vtable_t vtable_0 = {.f = &return_0};
vtable_t vtable_1 = {.f = &return_1};

// foo takes a vtable and calls f
int foo(vtable_t *vtable)
  // clang-format off
__CPROVER_requires(
    __CPROVER_is_in_range(&vtable_0, vtable, &vtable_0) ||
    __CPROVER_is_in_range(&vtable_1, vtable, &vtable_1))
__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == 1)
// clang-format on
{
  CALL:
  return vtable->f();
}

int main()
{
  vtable_t *vtable;
  foo(vtable);
}

goto-cc main.c
goto-instrument --restrict-function-pointer foo.CALL/return_0,return_1 --nondet-static-exclude vtable_0 --nondet-static-exclude vtable_1 --dfcc main --enforce-contract foo a.out b.out
cbmc --pointer-check --pointer-primitive-check b.out
...
main.c function foo
[foo.postcondition.1] line 30 Check ensures clause of contract contract::foo for function foo: SUCCESS
[foo.pointer_dereference.1] line 34 dereference failure: pointer NULL in vtable->f: SUCCESS
[foo.pointer_dereference.2] line 34 dereference failure: pointer invalid in vtable->f: SUCCESS
[foo.pointer_dereference.3] line 34 dereference failure: deallocated dynamic object in vtable->f: SUCCESS
[foo.pointer_dereference.4] line 34 dereference failure: dead object in vtable->f: SUCCESS
[foo.pointer_dereference.5] line 34 dereference failure: pointer outside object bounds in vtable->f: SUCCESS
[foo.pointer_dereference.6] line 34 dereference failure: invalid integer address in vtable->f: SUCCESS
[foo.pointer_dereference.7] line 34 dereference failure: pointer NULL in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.8] line 34 dereference failure: pointer invalid in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.9] line 34 dereference failure: deallocated dynamic object in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.10] line 34 dereference failure: dead object in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.11] line 34 dereference failure: pointer outside object bounds in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.12] line 34 dereference failure: invalid integer address in foo_function_pointer_call_1: SUCCESS
[foo.pointer_dereference.13] line 34 dereferenced function pointer must be one of [return_0, return_1]: SUCCESS
** 0 of 1167 failed (1 iterations)
VERIFICATION SUCCESSFUL

[remi-delmas-3000]

It would perhaps be more convenient to have a predicate __CPROVER_points_to_nondet(ptr, target1, target2, ...) that lets you say that a pointer nondeterministically points into some finite set of targets, and have the rest of the precondition refine under which circumstances which target is expected.