From 41ce82a4010409a76e90043e6a2e128f8d608961 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 26 Mar 2019 20:02:11 +0100
Subject: [PATCH] [Eva] keep real lower/upper bounds for floating-point
widening hints
---
.../abstract_interp/fc_float.ml | 54 ++++++++++++++-----
.../abstract_interp/float_sig.mli | 2 +-
.../ast_queries/cil_datatype.ml | 40 ++++++++++++--
.../ast_queries/cil_datatype.mli | 2 +
src/plugins/value/utils/widen.ml | 24 +++++----
5 files changed, 94 insertions(+), 28 deletions(-)
diff --git a/src/kernel_services/abstract_interp/fc_float.ml b/src/kernel_services/abstract_interp/fc_float.ml
index 58da42b53ee..5f0b009bab1 100644
--- a/src/kernel_services/abstract_interp/fc_float.ml
+++ b/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
diff --git a/src/kernel_services/abstract_interp/float_sig.mli b/src/kernel_services/abstract_interp/float_sig.mli
index 5febce60c3d..50ade7d97da 100644
--- a/src/kernel_services/abstract_interp/float_sig.mli
+++ b/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
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 49792655353..f0b07d285ac 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/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
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index f2552c6d88b..983c6ba3a37 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/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
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 94d70a29988..8bd8db47b52 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/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"
--
GitLab