Fix fixpoint option ana.int.refinement - loop was never executed

[michael-schwarz]

While investigating #1671, @jerhard and i discovered that the option to refine int domains until a fixpoint is reached has been broken since the very beginning.

In the PR #260 adding refinement, commit 1aee2eb added a special detection for bottom to ensure bottom values are normalized across all domains.

if is_bot !dt then dt := bot_of ik; quit_loop := true;

There, parentheses are missing. Thus, the loop is always left after one iteration.

[sim642]

Well, this is a surprising find!

Could you add some 38=int-refinements test that actually requires more than one iteration?

[michael-schwarz]

Could you add some 38=int-refinements test that actually requires more than one iteration?

We have not managed to construct such an example. A hypothesis is that the outer fixpoint algorithm will cause such an iteration to a fixpoint anyway (albeit non-locally) as values will keep changing, so I'm not even sure if such examples exist.

[sim642]

For reference Miné's tutorial (Section 6.2.4, 2017) says:

In the reduction between intervals and congruences, only one application of each reduction is necessary, provided we first refine intervals from congruences, and then congruences from intervals.

If I remember correctly, our int domain refinement does all directions in a single pass rather than in some arbitrary order, no? In that case such example should exist (perhaps one in the tutorial?) where two iterations are needed.

[michael-schwarz]

In that case such example should exist (perhaps one in the tutorial?) where two iterations are needed.

Yes, the point was not about needing two rounds (there are such examples), but about there being an observable difference in the end result between once and fixpoint.
For once, the outer fixpoint will see values have changed after each step refinement, and cause a re-evaluation.
So I think the end result with both strategies will be the same, only that the iteration happens outside instead of locally.
The only way I could see there being a difference would be if more of these outer evaluations have an effect on whether widening is applied.

[sim642]

Such outer fixpoint iteration only exists when such refinement is within a loop though. If it's outside a loop (just a chain of ifs or something), then solver's fixpoint iteration doesn't come back to do the following iterations for the int refinement.

[michael-schwarz]

We actually refine one after the other, and in the direction where iteration may be necessary

  let refine_functions ik : (t -> t) list =
    let maybe reffun ik domtup dom =
      match dom with Some y -> reffun ik domtup y | _ -> domtup
    in
    [(fun (a, b, c, d, e) -> refine_with_excl_list ik (a, b, c, d, e) (to_excl_list (a, b, c, d, e)));
     (fun (a, b, c, d, e) -> refine_with_incl_list ik (a, b, c, d, e) (to_incl_list (a, b, c, d, e)));
     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); (* TODO: get interval across all domains with minimal and maximal *)
     (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)]

  let refine ik ((a, b, c, d, e) : t ) : t =
    let dt = ref (a, b, c, d, e) in
    (match get_refinement () with
     | "never" -> ()
     | "once" ->
       List.iter (fun f -> dt := f !dt) (refine_functions ik);
     | "fixpoint" ->
       let quit_loop = ref false in
       while not !quit_loop do
         let old_dt = !dt in
         List.iter (fun f -> dt := f !dt) (refine_functions ik);
         quit_loop := equal old_dt !dt;
         if is_bot !dt then (dt := bot_of ik; quit_loop := true);
         if M.tracing then M.trace "cong-refine-loop" "old: %a, new: %a" pretty old_dt pretty !dt;
       done;
     | _ -> ()
    ); !dt

I tried

int main() {
  int x = 0;
  int v;

  __goblint_assume(v <= 13);
  __goblint_assume(v >= 7);

  if(v % 5 == 1) {
    __goblint_check(v == 11);
  }

 }

and some variants, but to no avail. I don't think it's worth sinking more time here. This PR is clearly an improvement, even if we cannot find an example where it pays off. I would thus propose merging it.