Fully simplifying assertions with base sometimes harmful for precision of relational analyses

[michael-schwarz]

Currently, when translating CIL expression -> Apron expression for guards, we fully simplify all appearing expressions, which is usually beneficial.

Thus, if base knows something will hold it gets simplified to 1. However, this can have adverse effects when a relational domain is not as precise as the base domain, as the information from the guard is not added to the relational domain, even if is expressible.
After a control-flow join, base may no longer be able to show the invariant even if it could in both branches. If the information was added to the relational domain, it would survive.

Consider, e.g., the following example with intervals and lin2vareq:

• In both branches, a and b are constant and b == a+2 holds which is checked by __goblint_check. However, as the constant value for a and b is established by a sequence of inequalities, this information is not available in the equality-based lin2vareq. Then, a guard asserting b == a+2 is executed. Normally, this would cause 2vareq to pick up on the equality, but we simplify it to 1 before passing it to the domain. Thus the value in 2vareq remains T.

• After join, base can no longer establish b == a+2. As it was not added to 2vareq either, it cannot be shown.

//SKIP PARAM:  --enable ana.int.interval  --set sem.int.signed_overflow assume_none  --set ana.activated[+] lin2vareq

int main() {
  int a;
  int b;

  if(a <= 7 && a >= 7 && b <= 9 && b >= 9) {
    // a = 7, b = 9
    // But the lin2vareq does not know about it as it is established via guards
    // Holds trivially => is simplified to Pos(1) before being passed to linvareq
    if(b == a+2) {
      __goblint_check(b == a+2); // Assertion passes because base knows about it
    } else {
      return 0;
    }
  }
  else if(a <= 5 && a >= 5 && b <= 7 && b >= 7) {
    // a = 5, b = 7
    if(b == a+2) {
      __goblint_check(b == a+2);
    } else {
      return 0;
    }
  }
  else {
    return 0;
  }

  // b == a+2 no longer can be shown by base, but was not added to lin2vareq
  // Assertion fails despite b == a+2 guard on all paths that lead here and being expressioble by lin2vareq
  __goblint_check(b == a+2);


  return 0;
}

There seem to be various things that could be done here:

• Ensure that the information from base is propagated to relational analyses when it is expressible.
• Ensure that guards do not get completely simplified if basencan show them, but instead get simplified into (all?) implied guards of the form that the domain can handle?

@DrMichaelPetter, @jerhard and I jointly came across this while talking about #1610.