`--enum-range-check` has false positives after harness or dfcc instrumentation

[archigup]

I'm not sure if this is intended behavior or a bug.

Take the following example c file:

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>

enum TestEnum {
    EnumValA,
    EnumValB
};

bool foo(enum TestEnum val)
    __CPROVER_requires(__CPROVER_enum_is_in_range(val)) {
    switch (val) {
    case EnumValA:
        return true;
    case EnumValB:
        return false;
    }
    assert(false);
}

Then the following validates successfully:

goto-cc -c test.c -o test.goto 
goto-instrument --enum-range-check test.goto test.goto
goto-harness --harness-function-name main --harness-type call-function --function foo test.goto test.goto
goto-cc test.goto -o test.goto
goto-instrument --dfcc main --enforce-contract foo test.goto test.goto
cbmc test.goto 

However the following sequence fails:

goto-cc -c test.c -o test.goto 
goto-harness --harness-function-name main --harness-type call-function --function foo test.goto test.goto
goto-instrument --enum-range-check test.goto test.goto
goto-cc test.goto -o test.goto
goto-instrument --dfcc main --enforce-contract foo test.goto test.goto
cbmc test.goto 

output:

CBMC version 6.7.1 (n/a) 64-bit x86_64 linux
Reading GOTO program from file test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
[enum-range-check.2] enum range check in nondet: FAILURE
[pointer_dereference.1] dereference failure: pointer NULL in *result_: SUCCESS
[pointer_dereference.2] dereference failure: pointer invalid in *result_: SUCCESS
[pointer_dereference.3] dereference failure: deallocated dynamic object in *result_: SUCCESS
[pointer_dereference.4] dereference failure: dead object in *result_: SUCCESS
[pointer_dereference.5] dereference failure: pointer outside object bounds in *result_: SUCCESS
[pointer_dereference.6] dereference failure: invalid integer address in *result_: SUCCESS
function type_constructor_
[type_constructor_.1] assertion: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_make_invalid_pointer
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.1] line 1186 dereference failure: pointer NULL in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.2] line 1186 dereference failure: pointer invalid in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.3] line 1186 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.4] line 1186 dereference failure: dead object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.5] line 1186 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.6] line 1186 dereference failure: invalid integer address in *ptr: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_check_assignment
[__CPROVER_contracts_write_set_check_assignment.assertion.1] line 805 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.2] line 822 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.3] line 828 no offset bits overflow on CAR upper bound computation: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.unwind.1] line 837 unwinding assertion loop 0: SUCCESS

[enum-range-check.1] file test.c line 10 enum range check in val: FAILURE
test.c function foo
[foo.no_alloc_dealloc_in_ensures.1] line 10 Check that ensures do not allocate or deallocate memory: SUCCESS
[foo.no_alloc_dealloc_in_requires.1] line 10 Check that requires do not allocate or deallocate memory: SUCCESS
[foo.no_recursive_call.1] line 10 No recursive call to function foo when checking contract foo: SUCCESS
[foo.single_top_level_call.1] line 10 Only a single top-level call to function foo when checking contract foo: SUCCESS
[foo.enum-range-check.1] line 12 enum range check in val: SUCCESS
[foo.assertion.1] line 18 assertion false: SUCCESS

** 2 of 28 failed (2 iterations)
VERIFICATION FAILED

Additionally the following sequence has even more false positives:

goto-cc -c test.c -o test.goto 
goto-harness --harness-function-name main --harness-type call-function --function foo test.goto test.goto
goto-cc test.goto -o test.goto
goto-instrument --enum-range-check --dfcc main --enforce-contract foo test.goto test.goto
cbmc test.goto 

output:

CBMC version 6.7.1 (n/a) 64-bit x86_64 linux
Reading GOTO program from file test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
[enum-range-check.7] enum range check in nondet: FAILURE
[pointer_dereference.1] dereference failure: pointer NULL in *result_: SUCCESS
[pointer_dereference.2] dereference failure: pointer invalid in *result_: SUCCESS
[pointer_dereference.3] dereference failure: deallocated dynamic object in *result_: SUCCESS
[pointer_dereference.4] dereference failure: dead object in *result_: SUCCESS
[pointer_dereference.5] dereference failure: pointer outside object bounds in *result_: SUCCESS
[pointer_dereference.6] dereference failure: invalid integer address in *result_: SUCCESS
function type_constructor_
[type_constructor_.1] assertion: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_make_invalid_pointer
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.1] line 1186 dereference failure: pointer NULL in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.2] line 1186 dereference failure: pointer invalid in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.3] line 1186 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.4] line 1186 dereference failure: dead object in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.5] line 1186 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[__CPROVER_contracts_make_invalid_pointer.pointer_dereference.6] line 1186 dereference failure: invalid integer address in *ptr: SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_obj_set_create_indexed_by_object_id
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS
[__CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3] line 264 count leading zeros is undefined for value zero in __builtin_clz(__CPROVER_max_malloc_size): SUCCESS

<builtin-library-__CPROVER_contracts_library> function __CPROVER_contracts_write_set_check_assignment
[__CPROVER_contracts_write_set_check_assignment.assertion.1] line 805 ptr NULL or writable up to size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.2] line 822 CAR size is less than __CPROVER_max_malloc_size: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.assertion.3] line 828 no offset bits overflow on CAR upper bound computation: SUCCESS
[__CPROVER_contracts_write_set_check_assignment.unwind.1] line 837 unwinding assertion loop 0: SUCCESS

[enum-range-check.1] file test.c line 10 enum range check in val: FAILURE
[enum-range-check.2] file test.c line 10 enum range check in val_wrapper: FAILURE
[enum-range-check.3] file test.c line 10 enum range check in val_wrapper: FAILURE
[enum-range-check.4] file test.c line 10 enum range check in val_wrapper: SUCCESS
[enum-range-check.5] file test.c line 10 enum range check in val_wrapper: SUCCESS
[enum-range-check.6] file test.c line 10 enum range check in val_wrapper: SUCCESS
test.c function foo
[foo.no_alloc_dealloc_in_ensures.1] line 10 Check that ensures do not allocate or deallocate memory: SUCCESS
[foo.no_alloc_dealloc_in_requires.1] line 10 Check that requires do not allocate or deallocate memory: SUCCESS
[foo.no_recursive_call.1] line 10 No recursive call to function foo when checking contract foo: SUCCESS
[foo.single_top_level_call.1] line 10 Only a single top-level call to function foo when checking contract foo: SUCCESS
[foo.enum-range-check.1] line 12 enum range check in val: SUCCESS
[foo.assertion.1] line 18 assertion false: SUCCESS

** 4 of 33 failed (2 iterations)
VERIFICATION FAILED

[tautschnig]

goto-harness does not currently restrict values for enum-typed parameters as the C type checker would happily accept programs where an arbitrary integer is passed as argument for such a parameter. But then we at least to to silence those checks in the auto-generated harness itself. So, yes, there are bugs for us to fix here.