No bound_texpr support for polyhedra domain

[jboillot]

Hello, I am trying to test the replacement of Apron by Elina in a toy analyzer. The problem is that it seems the function bound_texpr is not defined for the polyhedra domain https://github.com/eth-sri/ELINA/blob/f524156d292ac3a6f3cd676e2d2e7db6629e2b6f/elina_poly/opt_pk_internal.c#L233 I tried to add its support by calling the generic method https://github.com/eth-sri/ELINA/blob/f524156d292ac3a6f3cd676e2d2e7db6629e2b6f/elina_linearize/elina_generic.c#L75 Sadly, the precision is very little. As an example, when 0 <= x-a < 256 and -2^15 <= b < 2^15 the analyzer cannot prove that -2^15 <= (x-a)*b/256 < 2^15. I guess no relational information is used since the method called is the generic one.

Here is the corresponding code

#require "elina";;
#require "apron.polkaMPQ";;

open Apron
open Texpr1

let to_mpqf (x: int): Mpqf.t =
  x |> string_of_int |> Mpqf.of_string

let to_cst (x: int) : expr =
  Cst (x |> to_mpqf |> Coeff.s_of_mpqf)

let to_interval (l: int) (u: int): Interval.t =
  Interval.of_mpqf (to_mpqf l) (to_mpqf (u-1))

let () =
  let man = Elina_poly.manager_alloc_loose () in
  (*let man = Polka.manager_alloc_loose () in*)
  let x = Var.of_string "x" in
  let a = Var.of_string "a" in
  let b = Var.of_string "b" in
  let env = Environment.make [|x;a;b|] [||] in
  let vars = [x; a; b] in
  let boxes = [to_interval 0 (1 lsl 16); to_interval 0 (1 lsl 16); to_interval (-1 lsl 15) (1 lsl 15)] in
  let s = Abstract1.of_box man env (Array.of_list vars) (Array.of_list boxes) in

  let e1 = Binop (Sub, Var x, Var a, Real, Zero) in
  let ar = let open Tcons1 in
    let cons = make (of_expr env e1) SUPEQ in
    let ar = array_make env 1 in
    let _ = array_set ar 0 cons in
    ar
  in
  let s = Abstract1.meet_tcons_array man s ar in

  let e2 = Binop (Sub, to_cst 256, Binop (Sub, Var x, Var a, Real, Zero), Real, Zero) in
  let ar = let open Tcons1 in
    let cons = make (of_expr env e2) SUPEQ in
    let ar = array_make env 1 in
    let _ = array_set ar 0 cons in
    ar
  in
  let s = Abstract1.meet_tcons_array man s ar in

  let e3 = Binop (Div,
                 Binop (Mul,
                        Binop (Sub, Var x, Var a, Real, Zero)
                       , Var b, Real, Zero),
                 to_cst 256, Real, Zero) in
  let bounds = Abstract1.bound_texpr man s (of_expr env e3) in
  Format.printf "%a\n" Interval.print bounds
;;

Apron returns the interval [-8388480; 8388480] while Elina returns [-4294836225/256; 4294836225/256].