unsoundness on non-linear arithmethics

[kanigsson]

Hello Alt-ergo team,

We believe we have found an unsoundness on this small file:

logic div : int, int -> int

logic bit_index : int

predicate in_range(x: int) = (((- 2147483648) <= x) and (x <= 2147483647))

predicate in_range2(x: int) = ((1 <= x) and (x <= 17179869183))

axiom cdiv_cases :
 (forall n:int. forall d:int [div(n, d)].
 (((0 <= n) -> ((0 < d) -> (div(n, d) = (n / d))))
 and (((n < 0) -> ((0 < d) -> (div(n, d) = (-((-n) / d))))))))

axiom Div_1 : (forall x:int. (div(x, 1) = x))

goal VC_1 : (in_range2 (bit_index) ->
 (in_range ((div((bit_index - 1), 8) + 1))))

(*goal VC_2 : (not
 (in_range ((div((17179869183 - 1), 8) + 1))))*)

Our comments:

• VC_1 proves with option -max-split 5, without it alt-ergo suffers from an internal crash
• when we comment VC_1 and uncomment VC_2, it proves too, which is bad since VC_2 is (not VC_1) when bit_index is 17179869183
• cdiv_cases cannot be unsound since it gives a value to an otherwise undefined symbol
• Div_1 can be proved from cdiv_cases if we comment VC1 and VC2 and change the axiom to be a goal, so it cannot introduce an unsoundness either.
• We have a slightly modified version of alt-ergo, can you tell us if you can reproduce the unsoundness on the regular 2.3 version?

[Gbury]

We can reproduce using the next branch, so it is likely the bug is also there in 2.3.
The internal crash has been fixed in fd7c757
We are still looking at how and why alt-ergo manages to prove VC1 when it is incorrect (doing it by hand, we have that : div(17179869183 - 1, 8) + 1 = 2147483648, thus VC1 should not be provable).

[kanigsson]

Were you able to find anything? This is a quite urgent issue for us, as it directly impacts the soundness of SPARK.

[iguerNL]

@Gbury and @OCamlPro-Coquera managed to locate the origin of the issue. We'll see what is the best fix

[kanigsson]

Thank you for the update.

[Gbury]

I opened a PR ( #249 ) with a fix for the problem. It will be merged as soon as it is reviewed.
With that fix, alt-ergo no longer proves VC_1, as is expected.

[ACoquereau]

The PR (#249) has been reviewed, bench and merge into next.

[kanigsson]

We can confirm that this fixed the bug for us.