Unexpected bottom after meeting constraints using elina_poly

[rmonat]

I have an edge case were adding constraint x - (-9223372036854775808) >= 0 and then adding constraint -9223372036854775808 - x >= 0 yields bottom for elina_poly, which is unsound. Would there be an easy way to fix this issue?

MWE:

open Apron

let test_assume name man =
  let env = Environment.make (Array.map Var.of_string [|"x"; "y"; "z"|]) [||] in
  let a = Abstract1.top man env in 
  (* assume x <= -9223372036854775808 /\ x >= -9223372036854775808,
     but in two steps (no issue otherwise) *)
  let e =
    Texpr1.binop Sub
      (Texpr1.var env (Var.of_string "x"))
      (Texpr1.cst env (Coeff.neg @@ Coeff.s_of_mpq (Mpq.of_string "9223372036854775808")))
      Int Near in
  let arr = Tcons1.array_make env 1 in
  let () = Tcons1.array_set arr 0 (Tcons1.make e Tcons1.SUPEQ) in
  let a = Abstract1.meet_tcons_array man a arr in
  let () = Format.printf "[%s] after meeting with constraint %a, a = %a@." name
    (fun fmt x -> Tcons1.array_print fmt x)
    arr Abstract1.print a in 
  let e' =
    Texpr1.binop Sub
      (Texpr1.cst env (Coeff.neg @@ Coeff.s_of_mpq (Mpq.of_string "9223372036854775808")))
      (Texpr1.var env (Var.of_string "x"))
      Int Near
  in
  let () = Tcons1.array_set arr 0 (Tcons1.make e' Tcons1.SUPEQ) in 
  let a = Abstract1.meet_tcons_array man a arr in
  Format.printf "[%s] after meeting with constraint %a, a = %a@." name
    (fun fmt x -> Tcons1.array_print fmt x)
    arr Abstract1.print a


let () = test_assume "elina_poly" (Elina_poly.manager_alloc_loose ())
let () = test_assume "elina_oct" (Elina_oct.manager_alloc ())
let () = test_assume "apron_oct" (Oct.manager_alloc ())
let () = test_assume "apron_poly" (Polka.manager_alloc_loose ())

Output (with the unexpected bottom for elina_poly):

$ dune exec apron_test
[elina_poly] after meeting with constraint [|x -_i,n -9223372036854775808 >= 0|], a = [|
x>=0|]
[elina_poly] after meeting with constraint [|-9223372036854775808 -_i,n x >= 0|], a = bottom
[elina_oct] after meeting with constraint [|x -_i,n -9223372036854775808 >= 0|], a = [|
x+9.22337203686e+18>=0|]
[elina_oct] after meeting with constraint [|-9223372036854775808 -_i,n x >= 0|], a = [|
x+9.22337203686e+18>=0; -x-9.22337203685e+18>=0|]
[apron_oct] after meeting with constraint [|x -_i,n -9223372036854775808 >= 0|], a = [|
x+9223372036854775808>=0|]
[apron_oct] after meeting with constraint [|-9223372036854775808 -_i,n x >= 0|], a = [|
x+9223372036854775808>=0; -x-9223372036854775808>=0|]
[apron_poly] after meeting with constraint [|x -_i,n -9223372036854775808 >= 0|], a = [|
x+9223372036854775808>=0|]
[apron_poly] after meeting with constraint [|-9223372036854775808 -_i,n x >= 0|], a = [|
x+9223372036854775808=0|]

[rmonat]

In an email exchange with @GgnDpSngh highlighted that NewPolka with 64-bit integers does not seem to terminate in this case. Explanations about Elina's behavior:

The cause for issue #96 is due to the fact the constraint that you pass gets converted into x+9223372036854775808>=0. 9223372036854775808 encoded as MPQ in initial tcons is ultimately converted into int64 (the datatype used for Polyhedra in ELINA) using the call at https://github.com/eth-sri/ELINA/blob/f524156d292ac3a6f3cd676e2d2e7db6629e2b6f/elina_linearize/elina_int.h#L79. Since 9223372036854775808 cannot be represented as int64, mpz_get_si returns 0 and instead of adding x+9223372036854775808>=0, we add x>=0. The intersection of this with the second constraint you pass is empty. This is also an unavoidable error unless mpz_get_si has some form of error detection that I can propagate through.