[Eva] keep real lower/upper bounds for floating-point widening hints

src/kernel_services/abstract_interp/fc_float.ml

@@ -61,6 +61,7 @@ let cmp_ieee = (compare: float -> float -> int)
 (* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
 [@@@ warning "-3"]
 external compare : float -> float -> int = "float_compare_total" "noalloc"
+let total_compare = compare
 [@@@ warning "+3"]
 
 let of_float round prec f = round >>% fun () -> round_to_precision prec f
@@ -118,7 +119,7 @@ let le f1 f2 = compare f1 f2 <= 0
 
 module Widen_Hints = struct
 
-  include Datatype.Float.Set
+  include Cil_datatype.Logic_real.Set
 
   let pretty fmt s =
     if not (is_empty s) then
@@ -126,29 +127,55 @@ module Widen_Hints = struct
         ~pre:"@[<hov 1>{"
         ~suf:"}@]"
         ~sep:";@ "
-        iter Floating_point.pretty fmt s
+        iter
+        (fun fmt r -> Format.pp_print_string fmt r.Cil_types.r_literal) fmt s
 
-  let of_list l =
+  let logic_real_of_float f =
+    { Cil_types.r_literal = Format.asprintf "%10.7g" f;
+      r_nearest = f;
+      r_lower = f;
+      r_upper = f; }
+
+  let of_float_list l =
     match l with
     | [] -> empty
-    | [e] -> singleton e
+    | [e] -> singleton (logic_real_of_float e)
     | e :: q ->
-      List.fold_left (fun acc x -> add x acc) (singleton e) q
-
-  let m_pi = 3.1415929794311523 (* single-precision *)
-  let m_pi_2 = 1.5707964897155761 (* single-precision *)
-  let max_single_float = Floating_point.max_single_precision_float
+      List.fold_left
+        (fun acc x -> add (logic_real_of_float x) acc)
+        (singleton (logic_real_of_float e)) q
 
   let default_widen_hints =
-    let l = [0.0;1.0;m_pi_2;m_pi;10.;1e10;max_single_float;1e80] in
-    union (of_list l) (of_list (List.map (fun x -> -. x) l))
+    let l = [0.0;1.0;10.0;1e10;Floating_point.max_single_precision_float;1e80] in
+    union (of_float_list l) (of_float_list (List.map (fun x -> -. x) l))
+
+  exception Found of float
+
+  let nearest_float_ge f s =
+    try
+      iter (fun e ->
+          if total_compare e.Cil_types.r_upper f >= 0
+          then raise (Found e.Cil_types.r_upper))
+        s;
+      raise Not_found
+    with Found r -> r
+
+  let nearest_float_le f s =
+    try
+      let els_desc = List.rev (elements s) in
+      List.iter (fun e ->
+          if total_compare e.Cil_types.r_lower f <= 0
+          then raise (Found e.Cil_types.r_lower))
+        els_desc;
+      raise Not_found
+    with Found r -> r
 
 end
 
 type widen_hints = Widen_Hints.t
 
 let widen_up wh prec f =
-  let r = try Widen_Hints.nearest_elt_ge f wh
+  let r = try Widen_Hints.nearest_float_ge f wh
     with Not_found ->
       if le f max_float then max_float
       else infinity
@@ -156,14 +183,13 @@ let widen_up wh prec f =
   round_to_precision Up prec r
 
 let widen_down wh prec f =
-  let r = try Widen_Hints.nearest_elt_le f wh
+  let r = try Widen_Hints.nearest_float_le f wh
     with Not_found ->
       if le (-. max_float) f then (-. max_float)
       else neg_infinity
   in
   round_to_precision Down prec r
 
-
 let neg = (~-.)
 let abs = abs_float
 

src/kernel_services/abstract_interp/float_sig.mli

@@ -32,7 +32,7 @@ type prec = Single | Double | Long_Double | Real
 
 
 module type Widen_Hints = sig
-  include FCSet.S with type elt = Datatype.Float.t
+  include FCSet.S with type elt = Cil_datatype.Logic_real.t
   include Datatype.S with type t:=t
 
   val default_widen_hints: t

src/kernel_services/ast_queries/cil_datatype.ml

@@ -1446,15 +1446,26 @@ let is_exact_float r =
   classify_float r.r_upper = FP_normal &&
   Datatype.Float.equal r.r_upper r.r_lower
 
+[@@@ warning "-3"]
+(* [float_compare_total] is used to ensure -0.0 and 0.0 are distinct *)
+external float_compare_total : float -> float -> int = "float_compare_total" "noalloc"
+[@@@ warning "+3"]
+
+let compare_logic_real r1 r2 =
+  let c = float_compare_total r1.r_lower r2.r_lower in
+  if c <> 0 then c else
+    let c = float_compare_total r1.r_nearest r2.r_nearest in
+    if c <> 0 then c else
+      let c = float_compare_total r1.r_upper r2.r_upper in
+      if c <> 0 then c else
+        String.compare r1.r_literal r2.r_literal
+
 let compare_logic_constant c1 c2 = match c1,c2 with
   | Integer (i1,_), Integer(i2,_) -> Integer.compare i1 i2
   | LStr s1, LStr s2 -> Datatype.String.compare s1 s2
   | LWStr s1, LWStr s2 -> compare_list Datatype.Int64.compare s1 s2
   | LChr c1, LChr c2 -> Datatype.Char.compare c1 c2
-  | LReal r1, LReal r2 ->
-    if is_exact_float r1 && is_exact_float r2
-    then Datatype.Float.compare r1.r_lower r2.r_lower
-    else Datatype.String.compare r1.r_literal r2.r_literal
+  | LReal r1, LReal r2 -> compare_logic_real r1 r2
   | LEnum e1, LEnum e2 -> Enumitem.compare e1 e2
   | Integer _,(LStr _|LWStr _ |LChr _|LReal _|LEnum _) -> 1
   | LStr _ ,(LWStr _ |LChr _|LReal _|LEnum _) -> 1
@@ -1882,6 +1893,27 @@ module Logic_label = struct
     end)
 end
 
+module Logic_real = struct
+  let pretty_ref = ref (fun _ _ -> assert false)
+  include Make_with_collections
+            (struct
+              type t = logic_real
+              let name = "Logic_real"
+              let reprs =
+                [{ r_literal = ""; r_nearest = 0.0; r_lower = 0.0; r_upper = 0.0; }]
+              let compare = compare_logic_real
+              let hash r =
+                let fhash = Datatype.Float.hash in
+                fhash r.r_lower + 3 * fhash r.r_nearest + 7 * fhash r.r_upper +
+                  11 * Datatype.String.hash r.r_literal
+              let equal r1 r2 = compare r1 r2 = 0
+              let copy = Datatype.undefined
+              let internal_pretty_code = Datatype.undefined
+              let pretty fmt t = !pretty_ref fmt t
+              let varname _ = "logic_real"
+            end)
+end
+
 module Global_annotation = struct
   let pretty_ref = ref (fun _ -> assert false)
   include Make_with_collections

src/kernel_services/ast_queries/cil_datatype.mli

@@ -279,6 +279,8 @@ module Term_lhost: S_with_collections_pretty with type t = term_lhost
 module Term_offset: S_with_collections_pretty with type t = term_offset
 module Term_lval: S_with_collections_pretty with type t = term_lval
 
+module Logic_real: S_with_collections_pretty with type t = logic_real
+
 module Predicate: S_with_pretty with type t = predicate
 module Identified_predicate: 
   S_with_collections_pretty with type t = identified_predicate

src/plugins/value/utils/widen.ml

@@ -34,12 +34,18 @@ let dkey = Widen_hints_ext.dkey
    reuse loop indexes...
 *)
 
-let rec constFoldTermToNearestFloat = function
-  | TConst (LReal r) -> Some (r.r_nearest)
+let rec constFoldTermToLogicReal = function
+  | TConst (LReal r) -> Some r
   | TUnOp (Neg,e) -> begin
-      match (constFoldTermToNearestFloat e.term_node) with
+      match (constFoldTermToLogicReal e.term_node) with
       | None -> None
-      | Some e -> Some (-. e)
+      | Some e -> Some { r_literal =
+                           if String.get e.r_literal 0 = '-' then
+                             String.sub e.r_literal 1 (String.length e.r_literal - 1)
+                           else "-" ^ e.r_literal;
+                         r_nearest = -. e.r_nearest;
+                         r_lower = -. e.r_upper;
+                         r_upper = -. e.r_lower; }
     end
   | _ -> None
 
@@ -87,7 +93,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
           | { term_node= TConst (Integer(v,_))} ->
             (lv, Ival.Widen_Hints.add v lint, lfloat, lt)
           | _ ->
-            match constFoldTermToNearestFloat t.term_node with
+            match constFoldTermToLogicReal t.term_node with
             | Some f -> (lv, lint, Fc_float.Widen_Hints.add f lfloat, lt)
             | None -> (lv, lint, lfloat, t::lt)
         in
@@ -277,7 +283,7 @@ let base_of_static_hvars hvars =
     (* syntactic constraints prevent this from happening *)
     Value_parameters.fatal "unsupported lhost: %a" Printer.pp_lval (Mem e, offset)
 
-type threshold = Int_th of Integer.t | Float_th of float
+type threshold = Int_th of Integer.t | Real_th of logic_real
 
 (* try parsing as int, then as float *)
 let threshold_of_threshold_term ht =
@@ -290,8 +296,8 @@ let threshold_of_threshold_term ht =
   match Logic_utils.constFoldTermToInt ht with
   | Some i -> Int_th i
   | None ->
-    match constFoldTermToNearestFloat ht.term_node with
-    | Some f -> Float_th f
+    match constFoldTermToLogicReal ht.term_node with
+    | Some f -> Real_th f
     | None ->
       Value_parameters.abort ~source:(fst ht.term_loc)
         "could not parse widening hint: %a@ \
@@ -310,7 +316,7 @@ let thresholds_of_threshold_terms hts =
             Printer.pp_term ht;
         has_int := true;
         Ival.Widen_Hints.add i int_acc, float_acc
-      | Float_th f ->
+      | Real_th f ->
         if !has_int then
           Value_parameters.abort ~source:(fst ht.term_loc)
             "widening hint mixing integers and floats: %a"