Incorrect encoding of function pointer operations in CBMC

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

How to reproduce

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

#define SUCCESS 1
#define FAILURE 0
#define IMPLIES(a, b) (!(a) || (b))

struct obj_st;

/** A function table. */
typedef struct ftbl_st {
    int (*set_value)(struct obj_st *);
} ftbl_st;

/** An object. */
typedef struct obj_st {
    int a;
    ftbl_st *ftbl;
} obj_st;

static bool set_once = 0;
static bool __is_in_mode_0 = 0;

bool is_in_mode_0() {
    if (!set_once) {
        set_once = 1;
        __is_in_mode_0 = nondet_int() >= 0 ? true : false;
    }
    return __is_in_mode_0;
}

static int set_value_0(obj_st *obj) {
    if (obj == NULL)
        return FAILURE;
    obj->a = 0;
    return SUCCESS;
}

static int set_value_1(obj_st *obj) {
    if (obj == NULL)
        return FAILURE;
    obj->a = 1;
    return SUCCESS;
}

static const ftbl_st ftbl_0 = { .set_value = set_value_0 };
static const ftbl_st ftbl_1 = { .set_value = set_value_1 };

int set_value(obj_st *obj)
// obj is either null or some fresh object
__CPROVER_requires(IMPLIES(obj != NULL, __CPROVER_is_fresh(obj, sizeof(*obj))))

// the function table of the object is only one of two possible tables, which depends on the current mode
__CPROVER_requires(IMPLIES(obj != NULL && is_in_mode_0(), obj->ftbl == &ftbl_0))
__CPROVER_requires(IMPLIES(obj != NULL && !is_in_mode_0(), obj->ftbl == &ftbl_1))

// if the function succeeds, then obj is not null and updated according to the mode
__CPROVER_ensures(IMPLIES(__CPROVER_return_value == SUCCESS && is_in_mode_0(), obj != NULL && obj->a == 0))
__CPROVER_ensures(IMPLIES(__CPROVER_return_value == SUCCESS && !is_in_mode_0(), obj != NULL && obj->a == 1))

// for convenience
__CPROVER_assigns(obj->ftbl)
{
    if (obj == NULL)
        return FAILURE;

    // adding this statement makes everything work as expected
    //obj->ftbl = is_in_mode_0()? &ftbl_0 : &ftbl_1;

    // this assertion is proved, showing that the contract preconditions are enforced
    __CPROVER_assert(obj->ftbl == &ftbl_0 || obj->ftbl == &ftbl_1, "two_tables");
    
    // we copy the obj fields in local vars for diagnosis
    obj_st dummy0 = *obj;
    ftbl_st dummy1 = *(dummy0.ftbl);
    int (*dummy2)(obj_st *) = dummy1.set_value;
    int (*dummy3)(obj_st *) = dummy2;

    // this assertion fails, but it should not since the "two_tables" assertion holds
    // and ftbl_0 and ftbl_1 have non-null function pointers.
    //__CPROVER_assert(obj->ftbl->set_value != NULL, "function pointer not null");
    __CPROVER_assert(dummy3 != NULL, "function_pointer_is_not_null");

    int res;

    if (dummy3 == set_value_0)
        res = set_value_0(obj);
    else if (dummy3 == set_value_1)
        res = set_value_1(obj);
    else
        __CPROVER_assert(false, "unknown_function_pointer");

    return res;
}

all:
	# export static symbols
	goto-cc --export-file-local-symbols example.c -o example.c1.goto	
	
	# remove function pointers calls 
	# goto-instrument  --restrict-function-pointer set_value.function_pointer_call.1/__CPROVER_file_local_example_c_set_to_0,__CPROVER_file_local_example_c_set_to_1 example.c1.goto example.c2.goto
	cp example.c1.goto example.c2.goto
	
	# compile the set_value function
	goto-cc --function set_value example.c2.goto -o example.c3.goto	
	
	# build contract-checking program
	goto-instrument --enforce-contract set_value example.c3.goto example.c4.goto
	
	# drop unused functions
	goto-instrument --drop-unused-functions example.c4.goto example.c5.goto
	#cp example.c4.goto example.c5.goto

	# slice initialisation
	goto-instrument --slice-global-inits example.c5.goto example.c6.goto
	#cp example.c5.goto example.c6.goto

	# show functions
	goto-instrument --show-goto-functions example.c6.goto > example.c6.txt

	# compute coverage
	cbmc --unwind 1  --flush --object-bits 8 --malloc-may-fail --malloc-fail-null --cover location example.c6.goto >coverage.txt 2>coverage-err.log
	
	# compute properties
	cbmc --unwind 1  --flush --object-bits 8 --pointer-primitive-check  --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --show-properties $(XML_UI) example.c6.goto >property.txt 2>property-err.log
	
	# dump program POs
	cbmc --program-only --unwind 1  --flush --object-bits 8 --pointer-primitive-check  --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace $(XML_UI) example.c6.goto >result-program-only.txt 2>result-program-only-err.log
	
	# analyse program POs
	cbmc --unwind 1  --flush --object-bits 8 --pointer-primitive-check  --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace $(XML_UI) example.c6.goto >result.txt 2>result-err.log

clean: 
	rm -f *.goto *.txt *.log *~

.PHONY: all clean

Run make all.

Assertions are falsified when they shouldn't.

The issue

Consider the function below:

int set_value(obj_st *obj)
// obj is either null or some fresh object
__CPROVER_requires(IMPLIES(obj != NULL, __CPROVER_is_fresh(obj, sizeof(*obj))))

// the function table of the object is only one of two possible tables, which depends on the current mode
__CPROVER_requires(IMPLIES(obj != NULL && is_in_mode_0(), obj->ftbl == &ftbl_0))
__CPROVER_requires(IMPLIES(obj != NULL && !is_in_mode_0(), obj->ftbl == &ftbl_1))

// if the function succeeds, then obj is not null and updated according to the mode
__CPROVER_ensures(IMPLIES(__CPROVER_return_value == SUCCESS && is_in_mode_0(), obj != NULL && obj->a == 0))
__CPROVER_ensures(IMPLIES(__CPROVER_return_value == SUCCESS && !is_in_mode_0(), obj != NULL && obj->a == 1))

// for convenience
__CPROVER_assigns(obj->ftbl)
{
    if (obj == NULL)
        return FAILURE;

    // adding this statement makes everything work as expected
    //obj->ftbl = is_in_mode_0()? &ftbl_0 : &ftbl_1;

    // this assertion is proved, showing that the contract preconditions are enforced
    __CPROVER_assert(obj->ftbl == &ftbl_0 || obj->ftbl == &ftbl_1, "two_tables");
    
    // we copy the obj fields in local vars to have CBMC print them in the trace for diagnosis
    obj_st dummy0 = *obj;
    ftbl_st dummy1 = *(dummy0.ftbl);
    int (*dummy2)(obj_st *) = dummy1.set_value;
    int (*dummy3)(obj_st *) = dummy2;

    // this assertion fails, but it should not since the "two_tables" assertion holds
    // and ftbl_0 and ftbl_1 have non-null function pointers.
    //__CPROVER_assert(obj->ftbl->set_value != NULL, "function pointer not null");
    __CPROVER_assert(dummy3 != NULL, "function_pointer_is_not_null");

    int res;

    if (dummy3 == set_value_0)
        res = set_value_0(obj);
    else if (dummy3 == set_value_1)
        res = set_value_1(obj);
    else
        __CPROVER_assert(false, "unknown_function_pointer");

    return res;
}

The contract says that the obj->ftbl can point to ftbl_0 or ftbl_1, two static structs that contain a field .set_value which is a function pointer to function set_value_0 or set_value_1 respectively. The contract declares the conditions under which ftbl_0 or ftlb_1 gets used, and ensures the post conditions of whichever one is used. The contract and implementation are correct wrt each other.

Yet the verification of this contract fails.

for the postcondition.1 assertion: The function table in dummy0 is set to ftbl_1, but extracting the function from the function table yields set_value_0 in dummy_1, should be set_value_1. So it really seems like any value can be dreamed up from this function pointer.

State 193 file example.c function set_value line 103 thread 0
----------------------------------------------------
  dummy0.ftbl=&ftbl_1 (00001001 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 194 file example.c function set_value line 104 thread 0
----------------------------------------------------
  dummy1={ .set_value=dummy1!0@1#1..set_value } ({ ? })

State 203 file example.c function set_value line 104 thread 0
----------------------------------------------------
  dummy1={ .set_value=set_value_0 } ({ 00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

For the set_value.assertion.2 assertion: the null function pointer back-propagates through the dummy assignments:

State 203 file example.c function set_value line 104 thread 0
----------------------------------------------------
  dummy1={ .set_value=((signed int (*)(struct obj_st *))NULL) } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 204 file example.c function set_value line 104 thread 0
----------------------------------------------------
  dummy1.set_value=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 205 file example.c function set_value line 105 thread 0
----------------------------------------------------
  dummy2=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 208 file example.c function set_value line 105 thread 0
----------------------------------------------------
  dummy2=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 209 file example.c function set_value line 106 thread 0
----------------------------------------------------
  dummy3=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 212 file example.c function set_value line 106 thread 0
----------------------------------------------------
  dummy3=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

for the set_value.assertion.3, the dummy3 function pointer is equal to set_value_0` + a non-zero offset ?
(Are function pointers encoded as object pointers in CBMC ?)

State 205 file example.c function set_value line 105 thread 0
----------------------------------------------------
  dummy2=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 208 file example.c function set_value line 105 thread 0
----------------------------------------------------
  dummy2=set_value_0 + 262144l (00000010 00000000 00000000 00000000 00000000 00000100 00000000 00000000)

State 209 file example.c function set_value line 106 thread 0
----------------------------------------------------
  dummy3=((signed int (*)(struct obj_st *))NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 212 file example.c function set_value line 106 thread 0
----------------------------------------------------
  dummy3=set_value_0 + 262144l (00000010 00000000 00000000 00000000 00000000 00000100 00000000 00000000)

State 214 file example.c function set_value line 119 thread 0
----------------------------------------------------
  res=1 (00000000 00000000 00000000 00000001)

Violated property:
  file example.c function set_value line 126 thread 0
  unknown_function_pointer
  0 != 0

Here’s what is odd (in the program dump obtained using cbmc --program-only ... ):

// 323 file example.c line 104 function set_value
(276) dummy1!0@1#1 == { .set_value=dummy0!0@1#2..ftbl == &ftbl_0 ? set_value_0 : invalid_object!0#0..set_value }
      guard: !\guard#8

when dummy1 gets assigned from dummy0 it seems like cbmc assumes rather arbitrarily that dummy0.ftbl is either ftbl_0 or some invalid object and can be nothing else.
However, what the contract tries to say is that dummy0 is free function pointer required to be equal to one of two possible addresses &ftbl_0 or &ftbl_1 (see the contract's __CPROVER_requires clauses of the contract).

So we see that this C code

obj_st dummy0 = *obj;

yields this goto code :

(267) dummy0!0@1#2..ftbl == dynamic_object1#5..ftbl

and this realtively similar C-code :

ftbl_st dummy1 = *(dummy0.ftbl);

yields this very different goto code:

(276) dummy1!0@1#1 == { .set_value=dummy0!0@1#2..ftbl == &ftbl_0 ? set_value_0 : invalid_object!0#0..set_value }

I would have expected something like

(276) dummy1!0@1#1 == dummy0!0@1#2..ftbl

It may be the encoding of the deref operation on *(dummy.ftbl) (since dummy0.ftbl is a pointer, the deref could fail)
so this is modelled like this, but it still does not explain why CBMC assumes that dummy0!0@1#2..ftbl can only be equal to &ftbl_0 (in reality it can also point to &ftbl_1).

Next investigation steps

• Check what is the rule used by CMBC to generate this goto code and the rationale behind it.
• Check if CBMC really allows offsets on function pointers.

[feliperodri]

The example can be distilled down to this.

#include <assert.h>
struct s_t {
int value;
};

struct s_t a = {.value = 0};
struct s_t b = {.value = 1};

int main() {
struct s_t *ptr;
__CPROVER_assume(ptr == &a || ptr == &b);
assert(ptr == &a || ptr == &b);
// if the assertion above holds then this should also hold
assert(ptr->value == 0 || ptr->value == 1);
return 0;
}

The underlying problem is that pointer dereference depends on the value set associated with the pointer, and that the value set only reflects imperative updates made to the pointer and not declarative assumptions.

[tautschnig]

I believe that #6326 was built to specifically address this case. Would adding explicit nondet initialisers solve the problem?

[remi-delmas-3000]

Adding a nondet initializer does not seem to fix the problem:

#include <assert.h>
struct s_t {
  int value;
};

struct s_t a = {.value = 0};
struct s_t b = {.value = 1};

struct s_t *nondet_ptr();

int main() {
  struct s_t *ptr = nondet_ptr();
  __CPROVER_assume(ptr == &a || ptr == &b);
  assert(ptr == &a || ptr == &b);
  struct s_t * dummy_a = &a;
  struct s_t * dummy_b = &b;
  struct s_t * dummy_ptr = ptr;
  int dummy_ptr_value = ptr->value;
  // passes 
  assert(a.value == 0 && b.value == 1);
  
  // fails with ptr->value == 3
  assert(ptr->value == 0 || ptr->value == 1);
  return 0;
}

** Results:
ptrs.c function main
[main.assertion.1] line 14 assertion ptr == &a || ptr == &b: SUCCESS
[main.assertion.2] line 19 assertion a.value == 0 && b.value == 1: SUCCESS
[main.assertion.3] line 21 assertion ptr->value == 0 || ptr->value == 1: FAILURE

Trace for main.assertion.3:

State 26 file ptrs.c function main line 12 thread 0
----------------------------------------------------
  ptr=&b (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Assumption:
  file ptrs.c line 13 function main
  ptr == &a || ptr == &b

State 30 file ptrs.c function main line 15 thread 0
----------------------------------------------------
  dummy_a=&a (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 32 file ptrs.c function main line 16 thread 0
----------------------------------------------------
  dummy_b=&b (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 34 file ptrs.c function main line 17 thread 0
----------------------------------------------------
  dummy_ptr=&b (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 36 file ptrs.c function main line 18 thread 0
----------------------------------------------------
  dummy_ptr_value=1073741824 (01000000 00000000 00000000 00000000)

Violated property:
  file ptrs.c function main line 21 thread 0
  assertion ptr->value == 0 || ptr->value == 1
  !((signed long int)(signed long int)!(ptr->value == 0 || ptr->value == 1) != 0l)



** 1 of 3 failed (2 iterations)
VERIFICATION FAILED

[feliperodri]

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