Integer division of n/d where n = [-1, 1], d = -1 yields bottom

[rmonat]

Originally encountered by @svenkeidel, I'm providing an OCaml MWE.

We found that integer division of n/d yields bottom when -1 <= n <= 1 and d = -1. I have checked the documentation and I am not sure to understand this behavior?

MWE:

open Apron 

let run nv man = 
  let vars = Array.map Var.of_string [| "n"; "d1"; "d2"; "r" |] in 
  let nd = Array.sub vars 0 3 in
  let env = Environment.make vars [||] in
  let values = Array.map
      (fun (l, h) -> Texpr1.cst env (Coeff.i_of_int l h))
      [|nv; (-1, -1); (1, 1) |] in
  let abs = Abstract1.assign_texpr_array man (Abstract1.top man env) nd values None in
  let () = Format.printf "%a@." Abstract1.print abs  in
  let div1 = Texpr1.binop Div
      (Texpr1.var env vars.(0))
      (Texpr1.var env vars.(1)) Int Down in
  let abs1 = Abstract1.assign_texpr man abs vars.(3) div1 None in
  let () = Format.printf "assign(%a, %a) = %a\t=> r in %a@."
    Var.print vars.(3)
    Texpr1.print div1 
    Abstract1.print abs1
    Interval.print (Abstract1.bound_variable man abs vars.(3)) in
  ()

let () = run (-1, 1) (Polka.manager_alloc_loose ())

[svenkeidel]

@rmonat, thanks for submitting this issue.

I want to add, before the assignment of expression div1 to variable r, querying the bounds of div1 yields [-inf, inf]. I would have expected [-1,1].

Furthermore, with d = 1 everything works as expected.

[antoinemine]

Thanks for the report and sorry for the bug.

PR #101 should fix the issue. Could you confirm?

After the patch, I get no bottom, and the bounds for expression n/d1 is [-1,1].

Note that there is still an imprecision in the result of the assignment r = n/d1. The linearisation and relational assignment provides -1-n <= r <= 1-n, so , the bound for r are [-2,2], despite the fact that the interval evaluation of n/d1 is [-1,1]. This is due to the way the assignment is performed: first the constraint n/d1 - tmp = 0 is linearized and added, and then r is removed and tmp renamed to r. Thus, it does not currently exploit the interval bound of the assigned expression (although it is easy to fix in the client application by adding this bound explicitly after the assignment).

[svenkeidel]

@antoinemine, thank you for the quick response. I can confirm that it works now. Thanks!

[rmonat]

Thank you @antoinemine for your lightning fast fix! I concur, the abstract state after assignment is correct.

As a side note, it seems that Interval.print (Abstract1.bound_variable man abs vars.(3)) is still imprecise -- it returns the top interval. But this may be more related to #96.