Refine pointer sets upon assertion about pointee

[michael-schwarz]

I just realized that we do not refine pointers when they are dereferenced in an assertion. In some cases, the assertion can only hold for some pointees, and in this case the pointer set should also be refined.

// PARAM: --enable ana.int.interval

int two = 2;
int three = 3;

int main() {
	int* ptr;
	int top;

	if(top) {
		ptr = &two;
	} else {
		ptr = &three;
	}

	if(*ptr == 2) {
                // This can only be true if ptr is &two
                // The assertion however does not succeed
		__goblint_check(ptr == &two);
	}

  	return 0;
}

[michael-schwarz]

Adding something like this

    | Mem (Lval lv), NoOffset ->
      let lvals = eval_lv ~man st x in
      let res = AD.fold (fun a acc -> 
        if M.tracing then M.tracel "inv" "PUHHH improving lval %a setting to %a" d_lval lv VD.pretty (Address (AD.singleton a));
        let st = set' lv (Address (AD.singleton a)) st in
        let old_val = get ~man st (AD.singleton a) None in
        (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
        (* let old_val = eval_rv_lval_refine ~man st exp x in *)
        let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
        let v = apply_invariant ~old_val ~new_val:c' in
        if is_some_bot v then 
          acc
        else (
          if M.tracing then M.tracel "inv" "PUHHH improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
          D.join acc (set' x v st)
        )   
      ) lvals (D.bot ()) in
      res

to refine_lv in basInvariant.ml gets us 95% of the way there. This case now passes, but some others fail.

[michael-schwarz]

The three failing tests 3 test(s) failed: ["01/34 def-exc", "03/05 deslash", "67/29 def-exc"] all somehow concern exception IntDomain0.IncompatibleIKinds("ikinds char and unsigned char are incompatible. Values: (Unknown int([-7,7])) and (Not {0}([0,8]))"