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

ELINA/elina_poly/opt_pk_internal.c

Line 233 in f524156

//funptr[ELINA_FUNID_BOUND_TEXPR] = &opt_pk_bound_texpr;

I tried to add its support by calling the generic method

ELINA/elina_linearize/elina_generic.c

Line 75 in f524156

elina_interval_t* elina_generic_bound_texpr(elina_manager_t* man, void* abs, elina_texpr0_t* expr,

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].