From b8aa9be272290c29b3fe3a689d423e04031d86db Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 23 Aug 2019 19:37:48 +0200
Subject: [PATCH] [Dive] Also compute integer intervals
---
src/plugins/dive/build.ml | 66 ++++++++++++++++++----
src/plugins/dive/graph_types.mli | 11 ++--
src/plugins/dive/imprecision_graph.ml | 78 ++++++++++++++++++++------
src/plugins/dive/imprecision_graph.mli | 4 +-
src/plugins/dive/node_kind.mli | 2 -
5 files changed, 124 insertions(+), 37 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index b888bc94484..920a9a8a932 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -47,7 +47,7 @@ let fkind_limits =
| FDouble -> double
| FLongDouble -> assert false
-let precision_limits =
+let float_grade_limits =
let single = float_of_string "0x1p+120"
and double = float_of_string "0x1p+960"
and long_double = float_of_string "0x1p+15360"
@@ -56,39 +56,83 @@ let precision_limits =
| FDouble -> double
| FLongDouble -> long_double
-let is_large_range fkind (min,max) =
- let limit = precision_limits fkind in
+let is_large_float_range fkind (min,max) =
+ let limit = float_grade_limits fkind in
if (min < 0.0) = (max < 0.0) then (* if bounds have same sign *)
max -. min >= limit
else
min <= -.limit || max >= limit
-let qualify_range fkind (min,max) =
+let float_grade fkind (min,max) =
if min = max then
Singleton
- else if is_large_range fkind (min,max) then
+ else if is_large_float_range fkind (min,max) then
Wide
else
Normal
+let ikind_limits ikind =
+ let open Cil in
+ let bits = bitsSizeOfInt ikind in
+ if isSigned ikind then
+ { min=min_signed_number bits; max=max_signed_number bits }
+ else
+ { min=Integer.zero; max=max_unsigned_number bits }
+
+let int_grade_limits ikind =
+ let bits = Cil.bitsSizeOfInt ikind in
+ Integer.(pred (two_power_of_int (bits - bits / 8)))
+
+let is_large_int_range ikind (l,u) =
+ let limit = int_grade_limits ikind in
+ if Integer.(lt l zero) = Integer.(lt u zero) then (* if bounds have same sign *)
+ Integer.(ge (sub u l) limit)
+ else
+ Integer.(le l (neg limit)) || Integer.(ge u limit)
+
+let int_grade ikind (min,max) =
+ if min = max then
+ Singleton
+ else if is_large_int_range ikind (min,max) then
+ Wide
+ else
+ Normal
+
+
let update_node_values node kinstr lval =
let typ = Cil.typeOfLval lval in
let state = Db.Value.get_state kinstr in
let _,cvalue = !Db.Value.eval_lval None state lval in
- try match typ with
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ match typ with
+ | TInt (ikind,_) ->
+ let size = Integer.of_int (Cil.bitsSizeOfInt ikind)
+ and signed = Cil.isSigned ikind in
+ let ival = Ival.reinterpret_as_int ~size ~signed ival in
+ let min, max = match Ival.min_and_max ival with
+ | Some min, Some max -> min, max
+ | _, _ -> assert false (* ival have been reinterpreted *)
+ in
+ Imprecision_graph.update_node_int_values node {
+ values_interval = {min;max};
+ values_limits = ikind_limits ikind;
+ values_grade = int_grade ikind (min,max)
+ }
+
| TFloat (fkind,_) ->
- begin match Ival.min_and_max_float (Cvalue.V.project_ival cvalue) with
+ begin match Ival.min_and_max_float ival with
| None, _can_be_nan -> ()
| Some (min, max), _can_be_nan ->
let min = Fval.F.to_float min and max = Fval.F.to_float max in
- Imprecision_graph.update_node_values node {
+ Imprecision_graph.update_node_float_values node {
values_interval = {min;max};
values_limits = fkind_limits fkind;
- values_grade = qualify_range fkind (min,max);
+ values_grade = float_grade fkind (min,max);
}
end
- | _ -> ()
- with Cvalue.V.Not_based_on_null -> ()
+ | _ -> Self.result "node %a has type %a" Node_kind.pretty node.node_kind Cil_printer.pp_typ typ
+ with Cvalue.V.Not_based_on_null -> Self.result "node %a is not numeric" Node_kind.pretty node.node_kind
(* --- Locations handling --- *)
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 2089520d8d2..e98e37d3063 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -31,13 +31,13 @@ type node_locality = {
loc_callstack : Callstack.t;
}
-type float_interval = {min: float; max: float}
+type 'a interval = {min: 'a; max: 'a}
type precision_grade = Singleton | Normal | Wide
-type node_values = {
- values_interval : float_interval;
- values_limits : float_interval;
+type 'a node_values = {
+ values_interval : 'a interval;
+ values_limits : 'a interval;
values_grade : precision_grade;
}
@@ -46,7 +46,8 @@ type node = {
node_kind : node_kind;
node_locality : node_locality;
mutable node_hidden : bool;
- mutable node_values : node_values option;
+ mutable node_int_values : (Integer.t node_values) option;
+ mutable node_float_values : (float node_values) option;
mutable node_deps_computed : bool;
}
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 01732d253bb..2a51d52943b 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -55,13 +55,14 @@ let edges g =
let next_key = ref 0
-let create_node ?node_values ~node_kind ~node_locality g =
+let create_node ~node_kind ~node_locality g =
let node = {
node_key = !next_key;
node_kind;
node_locality;
node_hidden = false;
- node_values;
+ node_int_values = None;
+ node_float_values = None;
node_deps_computed = false;
}
in
@@ -71,7 +72,10 @@ let create_node ?node_values ~node_kind ~node_locality g =
let remove_node = remove_vertex
-let union_interval i1 i2 =
+let union_int_interval i1 i2 =
+ { min = Integer.min i1.min i2.min ; max = Integer.max i1.max i2.max }
+
+let union_float_interval i1 i2 =
{ min = min i1.min i2.min ; max = max i1.max i2.max }
let worst_precision_grade q1 q2 =
@@ -80,18 +84,32 @@ let worst_precision_grade q1 q2 =
| Normal, _ | _, Normal -> Normal
| Singleton, Singleton -> Singleton
-let merge_precisions p1 p2 =
+let merge_int_values p1 p2 =
+ (* TODO: prevent assertion failure *)
+ assert (Integer.equal p1.values_limits.min p2.values_limits.min);
+ assert (Integer.equal p1.values_limits.max p2.values_limits.max);
+ {
+ values_interval = union_int_interval p1.values_interval p2.values_interval;
+ values_limits = p1.values_limits;
+ values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+ }
+
+let merge_float_values p1 p2 =
(* TODO: prevent assertion failure *)
assert (p1.values_limits = p2.values_limits);
{
- values_interval = union_interval p1.values_interval p2.values_interval;
+ values_interval = union_float_interval p1.values_interval p2.values_interval;
values_limits = p1.values_limits;
values_grade = worst_precision_grade p1.values_grade p2.values_grade;
}
-let update_node_values node new_values =
- node.node_values <-
- Some (Extlib.opt_fold merge_precisions node.node_values new_values)
+let update_node_int_values node new_values =
+ node.node_int_values <-
+ Some (Extlib.opt_fold merge_int_values node.node_int_values new_values)
+
+let update_node_float_values node new_values =
+ node.node_float_values <-
+ Some (Extlib.opt_fold merge_float_values node.node_float_values new_values)
let create_dependency ~allow_folding g v1 dependency_kind v2 =
@@ -178,6 +196,13 @@ let ouptput_to_dot out_channel g =
let default_vertex_attributes _g = []
let vertex_name v = "cp" ^ (string_of_int v.node_key)
let vertex_attributes v =
+ let grade = match v.node_int_values, v.node_float_values with
+ | Some v1, Some v2 ->
+ Some (worst_precision_grade v1.values_grade v2.values_grade)
+ | Some v, _ -> Some v.values_grade
+ | _, Some v -> Some v.values_grade
+ | None, None -> None
+ in
let l = ref [] in
let text = Pretty_utils.to_string Node_kind.pretty v.node_kind in
if text <> "" then
@@ -189,13 +214,13 @@ let ouptput_to_dot out_channel g =
| Alarm _ -> [ `Shape `Doubleoctagon ;
`Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ]
- and values = match v.node_values with
+ and values = match grade with
| None -> []
- | Some ({values_grade=Singleton}) ->
+ | Some Singleton ->
[`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ]
- | Some ({values_grade=Normal}) ->
+ | Some Normal ->
[ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ]
- | Some ({values_grade=Wide}) ->
+ | Some Wide ->
[ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ]
in
l := values @ kind @ !l;
@@ -269,13 +294,27 @@ struct
in
Json.of_string s
+ let output_int_interval interval =
+ (* TODO: handle overflow *)
+ Json.of_fields [
+ ("min", Json.of_int (Integer.to_int interval.min)) ;
+ ("max", Json.of_int (Integer.to_int interval.max)) ;
+ ]
+
let output_float_interval interval =
Json.of_fields [
("min", Json.of_float interval.min) ;
("max", Json.of_float interval.max) ;
]
- let output_node_values values =
+ let output_node_int_values values =
+ Json.of_fields [
+ ("computed", output_int_interval values.values_interval) ;
+ ("limits", output_int_interval values.values_limits) ;
+ ("grade", output_node_precision_grade values.values_grade) ;
+ ]
+
+ let output_node_float_values values =
Json.of_fields [
("computed", output_float_interval values.values_interval) ;
("limits", output_float_interval values.values_limits) ;
@@ -291,11 +330,16 @@ struct
("locality", output_node_locality node.node_locality) ;
("explored", Json.of_bool node.node_deps_computed) ;
] @
- begin match node.node_values with
+ begin match node.node_int_values with
+ | None -> []
+ | Some node_values ->
+ [("int_values", output_node_int_values node_values)]
+ end @
+ begin match node.node_float_values with
| None -> []
- | Some node_values -> [("values", output_node_values node_values)]
- end
- @
+ | Some node_values ->
+ [("float_values", output_node_float_values node_values)]
+ end @
begin match Node_kind.to_lval node.node_kind with
| None -> []
| Some lval ->
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index 890cee867a9..59c9d4709fe 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -33,13 +33,13 @@ module Dependency : Graph.Sig.COMPARABLE with type t = dependency
val create : ?size:int -> unit -> t
val create_node :
- ?node_values:node_values ->
node_kind:node_kind ->
node_locality:node_locality -> t -> node
val remove_node : t -> node -> unit
-val update_node_values : node -> node_values -> unit
+val update_node_int_values : node -> Integer.t node_values -> unit
+val update_node_float_values : node -> float node_values -> unit
val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
node -> unit
diff --git a/src/plugins/dive/node_kind.mli b/src/plugins/dive/node_kind.mli
index 923348cf197..9d4bcefed67 100644
--- a/src/plugins/dive/node_kind.mli
+++ b/src/plugins/dive/node_kind.mli
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-open Graph_types
-
include Datatype.S with type t = Graph_types.node_kind
val get_base : t -> Cil_types.varinfo option
--
GitLab