[topl] False positive issue recently introduced

[danielmercier]

While merging our local fork of infer, we saw the following regression on a topl testcase.

Here is the testcase translated in Java:

class Valid {
  public static boolean is_valid_vn(int i) { return i >= 1 && i <= 10; }
  public static void id_to_vn(int i) {}

  public static void safe_call(int id) {
    if (is_valid_vn(id)) {
      id_to_vn(id);
    }
  }

  public static void test() { safe_call(1); }
}

and the following topl properties:

property ValidVN
   prefix "Valid"
   start -> error: "id_to_vn"(IgnoreArg, IgnoreRet)
   start -> ok: "is_valid_vn"(Arg, Ret) when Ret != 0 => good := Arg
   ok -> ok: "is_valid_vn"(Arg, Ret) when Ret != 0 => good := Arg
   ok -> error: "id_to_vn"(Arg, IgnoreRet) when Arg != good

What we are trying to say with the above topl property is basically that "id_to_vn(x)" should be called only if "is_valid_vn(x)" is true.

We are getting a spurious message on the test() subrogram:

Valid.java:11: error: Topl Error
  property ValidVN fails.
   9.     }
  10.
  11. >   public static void test() { safe_call(1); }
  12.   }

No warning should be emitted for any call to safe_call as is_valid_vn is always called before id_to_vn there.

This was recently introduced, I believe by commits 2a8ca1e8 and 1852f694.

One weird thing that I can see on the pulse and topl states is that Topl is keeping inconsistent states in safe_call:

Here are two inconsistent topl states:

{ topl-simple-state pre={ topl-config vertex=1 memory=[good↦v2] } post={ topl-config vertex=0 memory=[good↦v2] } pruned=(v3!=v2∧v6==0) },
{ topl-simple-state pre={ topl-config vertex=1 memory=[good↦v2] } post={ topl-config vertex=1 memory=[good↦v2] } pruned=(v3==v2∧v6==0) }

While in the Pulse corresponding disjonction, v6 is equal to 1:

(conditions: {1 ≤ [v3]}∧{[v3] ≤ 10}
     phi: var_eqs: a10=a8
          && linear_eqs: a9 = -a10 +9 ∧ a7 = -a10 +9 ∧ v3 = a7 +1 ∧ v6 = 1
          && term_eqs: 1=v6∧[a7 +1]=v3∧[-a8 +9]=a7∧[-a10 +9]=a9∧[-a10 +10]=v3
          && tableau: a9 = -a10 +9 ∧ a8 = -a7 +9 ∧ a7 = -a10 +9
          && intervals: v3∈[1,10] ∧ v6=1
          && atoms: {is_int([v3]) = 1}

[rgrig]

Thanks for the report. Should be fixed in 0ab8f14.