AWS tasks with wrong expected verdict due to truncating pointer-to-int cast

83 AWS tasks contain code where a pointer is passed as argument to __VERIFIER_assert(int), and due to truncation during casts this causes unintended property violations, i.e., wrong expected verdicts. This was not caught by our checks because the respective compiler warning int-conversion was explicitly disabled in the Makefile when the tasks were submitted.

More details:

__VERIFIER_assert is declared as

sv-benchmarks/c/aws-c-common/prelude.h

Lines 20 to 22 in 494a357

    
           void __VERIFIER_assert(int cond) { 
        
               if(!cond) {reach_error();abort();}  
        
           }

The parameter is a 32-bit int. The function is often called with a pointer as argument with the intent of checking that the pointer is not null, e.g.:

sv-benchmarks/c/aws-c-common/aws_byte_buf_cat_harness.i

Line 8022 in 494a357

__VERIFIER_assert(from->ptr);

Pointers are 64 bit in this category, so when __VERIFIER_assert is called, the upper 32 bit of the pointer are discarded. This means that even a non-null pointer that happens to have only zeroes in the lower 32 bit will fail the assertion. Because pointer values must be assumed to be nondeterministic, every reachable instance of such code is a property violation, but all of these tasks are labeled with expected verdict true.

Here is an example log from SV-COMP'20 where a verifier found such a property violation.

The same problem also occurs for the function assume_abort_if_not(int cond) (previously __VERIFIER_assume).

These problems due not exist in the original AWS code, they were introduced while preparing the tasks for this repository. In the original code, assertions are handled via the standard macro assert which does not have this problem (because the if (!cond) part is inlined, there is no parameter of type int and no truncating cast). AWS_ASSUME is a macro that delegates to __CPROVER_assume, which takes a parameter of type _Bool instead of int.

The casting rules to _Bool are different than for all other integer types in C: Casts to _Bool do not truncate but compare the input value against 0 (cf. C11 § 6.3.1.2) and avoid this problem.

So the suggested fix is to change the parameter type of __VERIFIER_assert and assume_abort_if_not from int to _Bool. I do not think it is worth it to keep the current set of programs with a changed verdict, because detecting that a pointer can have zeroes in the 32 lower bits is a rather trivial task.

However, this shows how important the compiler warnings are, and all the warnings that are currently suppressed in the Makefile should be analyzed and fixed!

	void __VERIFIER_assert(int cond) {
	if(!cond) {reach_error();abort();}
	}