Binary operations on pointers should not generate overflow warnings in SV-COMP

[karoliineh]

Looking into the no-overflow tasks, there were many tasks (array-memsafety/cstr..-alloca-..) where the signed integer overflow warnings came from pointer arithmetic. For example:

char* nondetArea = (char*) __builtin_alloca (length1 * sizeof(char));
char* nondetString = (char*) __builtin_alloca (length2 * sizeof(char));

char *(cstrcpy)(char *s1, const char *s2)
 {
     char *dst = s1;
     const char *src = s2;
     while ((*dst++ = *src++) != '\0') // [Warning][Integer > Overflow][CWE-190] Signed integer overflow 
         ;
     return s1;
 }

cstrcpy(nondetArea,nondetString);

This PR turns off producing the overflow warnings when IntDomain values are used for pointer arithmetic.

[michael-schwarz]

Thanks for looking into it!

I started wondering whether this is actually true in general? I would intuitively think some snippet such as this would be Undefined Behavior?

int* ptr = (int*) 0;

while(1) {
   ptr += MAX_INT;
}

I think if the offset is within the bounds of the objects, it should be safe for sure, otherwise I don't know.

If the standard indeed mandates that such computations are not UB, we still need to be careful, as we keep the abstract type pointer even after a cast to int iiirc, and

int x;
int* ptr = &x;

long l = (long) ptr; // Goblint iirc has abstract state with:   l -> {&x}

while(1) {
   l += MAX_INT; //UB!
}

is UB for sure!

[sim642]

I started wondering whether this is actually true in general? I would intuitively think some snippet such as this would be Undefined Behavior?

int* ptr = (int*) 0;

while(1) {
   ptr += MAX_INT;
}

I think if the offset is within the bounds of the objects, it should be safe for sure, otherwise I don't know.

N1570 6.5.6.8 says:

[...] If both the pointer operand and the result point to elements of the same array object, or one past the last element of the array object, the evaluation shall not produce an overflow; otherwise, the behavior is undefined.

So it is UB, although I'm not sure if it could be called "integer overflow". Not for SV-COMP flagging for sure.
As to Goblint warning output, if we want something, we should probably call it differently anyway ("pointer overflow" or whatnot).
Although our current overflow warnings from pointer offset calculations don't soundly even reflect that: it's just about overflow from the index itself, without considering possible addresses (as integers) of the pointer itself. If the pointer itself has value MAX_INT (which it won't on any sensible system, but I guess the standard doesn't forbid), then even p + 2 would "pointer overflow" (p + 1 is fine according to the quote even!). But currently we just compute the address &p[2] and don't output such warning.

[sim642]

If the standard indeed mandates that such computations are not UB, we still need to be careful, as we keep the abstract type pointer even after a cast to int iiirc, and

int x;
int* ptr = &x;

long l = (long) ptr; // Goblint iirc has abstract state with:   l -> {&x}

while(1) {
   l += MAX_INT; //UB!
}

is UB for sure!

We don't do such thing on master even. The code for cast has this for casting v to integer:

analyzer/src/cdomain/value/cdomains/valueDomain.ml

Lines 476 to 487 in 4812b07

	let v' = match t with
	| TInt (ik,_) ->
	Int (ID.cast_to ?torg ik (match v with
	| Int x -> x
	| Address x -> AD.to_int x
	| Float x -> FD.to_int ik x
	(*| Struct x when Structs.cardinal x > 0 ->
	let some = List.hd (Structs.keys x) in
	let first = List.hd some.fcomp.cfields in
	(match Structs.get x first with Int x -> x | _ -> raise CastError)*)
	| _ -> log_top __POS__; ID.top_of ik
	))

The result is always an integer abstraction.

Also, the only non-UB cast of pointer to integer would be to some unsigned integer type anyway, so I don't see this being an issue.

Even if this were the case, we wouldn't be soundly warning about it on master anyway. l + 2 (where l has been cast from a pointer) may also overflow and our current behavior just adds an index offset 2 without emitting any warnings.

[sim642]

On sv-benchmarks with no-overflow property, this gives 53 new correct results with 60s timeout. Nothing becomes unsound.