Basic incremental can be more precise than from-scratch due to type-based interval widening

[sim642]

On knot_comb from our bench, basic incremental analysis is surprisingly more precise than from-scratch analysis. A manually minimized program that still shows the same behavior is the following:

struct input_state;
typedef struct input_state input_state;
struct input_state {
   char buf[512] ;
   int valid ;
};

char *input_get_line(input_state *state ) 
{ char *result ;
  int done ;
  char *start ;
  char *newline ;
  int n ;

  {
  result = (char *)((void *)0);
  while (! done) {
    start = & state->buf[state->valid];
    if (newline != ((void *)0)) {
      result = start;
      state->valid = (newline - state->buf) + 2;
    } else {
      if (state->valid < 511) {
        if (n <= 0) {
          result = (char *)((void *)0);
        }
      }
    }
  }
  return (result);
}
}

int main() 
{
  input_state state ;
  char *line ;
  state.valid = 0;
  while (1) {
    line = input_get_line(& state);
  }
  return 0;
}

With the following patch:

diff --git pthread/knot_comb.c pthread/knot_comb.c
index ad59515..de401be 100644
--- pthread/knot_comb.c
+++ pthread/knot_comb.c
@@ -709,7 +709,7 @@ char *input_get_line(input_state *state )
         empty = & state->buf[state->valid];
         tmp = read(state->socket, (void *)empty, (unsigned int )(511 - state->valid));
       if (state->valid < 511) {
-        if (n <= 0) {
+        if (n == 0) {
           result = (char *)((void *)0);
           done = 1;
         } else {

The precision comparison says that line in incremental is more precise than in from-scratch:

{state.buf[def_exc:Unknown int([-31,31]); intervals:[-9223372036854775808,9223372036854775807]], NULL, ?} not leq {state.buf[def_exc:Unknown int([-31,31]); intervals:[-2147483648,2147483647]], NULL, ?}

Note the inconsistency in the first offset's int domains: def_exc has 32bit range, but intervals have 64bit range.

This occurs due to the following widening taking place in the main loop (for the address offset):

%%% int: (../goblint-bench/pthread/knot_comb.c:41:5-41:35)   intdomtuple widen (0,[0,0]) (Unknown int([-31,31]),[-2147483648,2147483647]) -> (Unknown int([-31,31]),[-9223372036854775808,9223372036854775807])

Notably, def_exc simply joins, while intervals widen to the type's maximum bounds, which in this case are ptrdiff_t 64bit bounds. This isn't a bug in the interval domain because it is correctly widening to infinity (for the type).

The reason this allows basic incremental to be more precise is because it reuses the locally stored value, initially has no widening point, the main loop reaches fixpoint immediately with the stored value and hence widening is never applied!
This demonstrates a pitfall we have suspected a long ago, but not yet seen in Goblint: widening may allow "jumping over" certain values. That is, if a leq b leq c leq d and a widen (a join c) = d and b widen (b join c) = c, then surprisingly widening from a lower value a to c may jump over compared to if the widening happens from a higher value b.

[sim642]

It's probably possible to create a much simpler non-incremental program, which contains the same behavior, but this very likely wouldn't be observable since any assertion/branching would account for the more precise bound from def_exc.

There are multiple ways this could be worked around in the int domains:

1. Make intervals also widen in jumps of type sizes, like the def_exc ranges do by default.
2. Apply int domain refinement to refine the interval from the def_exc bounds.

But much more notable is still the fact that certain valid widenings may not have some intuitively nice property of "not jumping over" and this is actually observable from our incremental analysis results.

[michael-schwarz]

Apply int domain refinement to refine the interval from the def_exc bounds.

I would actually be interested whether this works out of the box. Can you try with ana.int.refinement once or fixpoint?

[sim642]

I would actually be interested whether this works out of the box. Can you try with ana.int.refinement once or fixpoint?

I tried now and it doesn't. The reason is "visible" from the implementation of refining intervals with exclusion sets (in this case an empty exclusion set):

analyzer/src/cdomains/intDomain.ml

Lines 877 to 891 in 6958d4b

	let refine_with_excl_list ik (intv : t) (excl : (int_t list) option) : t =
	match intv, excl with
	| None, _ | _, None -> intv
	| Some(l, u), Some(ls) ->
	let rec shrink op b =
	let new_b = (op b (Ints_t.of_int(Bool.to_int(List.mem b ls)))) in
	if not (Ints_t.equal b new_b) then shrink op new_b else new_b
	in
	let l' =
	if Ints_t.equal l (min_int ik) then l else
	shrink Ints_t.add l in
	let u' =
	if Ints_t.equal u (max_int ik) then u else
	shrink Ints_t.sub u in
	norm ik @@ Some(l', u')

It doesn't get as argument the range of def_exc, only the list of values. Meanwhile the ik argument corresponds to the outer 64bit type.

[sim642]

I will try to enhance this refinement such that the def_exc range is also passed to intervals and used for refining. Then we can at least see how many of the internal precision comparisons from incremental bench are due to this.

[sim642]

This specific case was closed by #640.