From cffdfb0bf131a8044cca2a6c76bc829cbf9f3037 Mon Sep 17 00:00:00 2001
From: Marc Coudriau <marc.coudriau@ens.fr>
Date: Thu, 8 Aug 2019 17:32:01 +0200
Subject: [PATCH] [Dive] Add precision_width field to json output
---
src/plugins/dive/build.ml | 15 +++++++++-----
src/plugins/dive/graph_types.mli | 5 ++++-
src/plugins/dive/imprecision_graph.ml | 30 +++++++++++++++++++--------
3 files changed, 35 insertions(+), 15 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index ed0d5855126..9fe45931406 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -64,10 +64,15 @@ let compute_node_precision kinstr lval =
then Singleton
else
match Cvalue.V.project_ival cvalue, typ with
- | Ival.Float fval, TFloat (fkind,_) ->
- if fval_has_large_range fkind fval then Wide else Normal
- | _ -> Normal
- | exception Cvalue.V.Not_based_on_null -> Normal
+ | Ival.Float fval, TFloat (fkind,_) -> begin
+ match Fval.min_and_max fval with
+ | Some (min,max), _ ->
+ let ival = {min=Fval.F.to_float min; max=Fval.F.to_float max} in
+ if fval_has_large_range fkind fval then Wide ival else Normal ival
+ | None, _ -> Unevaluated
+ end
+ | _ -> Unevaluated
+ | exception Cvalue.V.Not_based_on_null -> Unevaluated
(* --- Locations handling --- *)
@@ -244,7 +249,7 @@ let build_lval context callstack kinstr lval =
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
let node_locality = build_node_locality callstack node_kind
- and node_precision = Critical in
+ and node_precision = Critical {min=0.; max=0.} in
Graph.create_node context.graph ~node_precision ~node_kind ~node_locality
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 2bdf37f3952..a1cce6545e5 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -32,7 +32,10 @@ type node_locality = {
loc_callstack : Callstack.t;
}
-type node_precision = Unevaluated | Singleton | Normal | Wide | Critical
+type precision_interval = {min: float; max: float}
+
+type node_precision = Unevaluated | Singleton | Normal of precision_interval |
+ Wide of precision_interval | Critical of precision_interval
type node = {
node_key : int;
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index a2bd2a9b454..8dd39791320 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -65,9 +65,9 @@ let create_node ?(node_precision=Unevaluated) ~node_kind ~node_locality g =
let update_node_precision node new_precision =
node.node_precision <-
match node.node_precision, new_precision with
- | Critical, _ | _, Critical -> Critical
- | Wide, _ | _, Wide -> Wide
- | Normal, _ | _, Normal -> Normal
+ | Critical i, _ | _, Critical i -> Critical i
+ | Wide i, _ | _, Wide i -> Wide i
+ | Normal i, _ | _, Normal i -> Normal i
| Singleton, _ | _, Singleton -> Singleton
| Unevaluated, Unevaluated -> Unevaluated
@@ -152,11 +152,11 @@ let ouptput_to_dot out_channel g =
| Unevaluated -> []
| Singleton -> [`Color 0x88aaff ;
`Style `Filled ; `Fillcolor 0xaaccff]
- | Normal -> [ `Color 0x004400 ;
+ | Normal _ -> [ `Color 0x004400 ;
`Style `Filled ; `Fillcolor 0xeeffee ]
- | Wide -> [ `Color 0xff0000 ;
+ | Wide _ -> [ `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xffbbbb ]
- | Critical -> [ `Color 0xff0000 ; `Style `Bold ;
+ | Critical _ -> [ `Color 0xff0000 ; `Style `Bold ;
`Style `Filled ; `Fillcolor 0xff0000 ]
in
l := precision @ kind @ !l;
@@ -213,9 +213,9 @@ let to_json g =
let s = match precision with
| Unevaluated -> "unevaluated"
| Singleton -> "singleton"
- | Normal -> "normal"
- | Wide -> "wide"
- | Critical -> "critical"
+ | Normal _ -> "normal"
+ | Wide _ -> "wide"
+ | Critical _ -> "critical"
in
Json.of_string s
and output_dep_kind kind =
@@ -226,6 +226,17 @@ let to_json g =
| Control -> "ctrl"
in
Json.of_string s
+ and output_node_precision_width precision =
+ let precision_with_ival ival =
+ Json.of_float (ival.max -. ival.min);
+ in
+ let precision_no_ival = Json.of_float 0. in
+ match precision with
+ | Unevaluated -> precision_no_ival
+ | Singleton -> precision_no_ival
+ | Normal iv -> precision_with_ival iv
+ | Wide iv -> precision_with_ival iv
+ | Critical iv -> precision_with_ival iv
in
let output_node node acc =
if node.node_kind = Cluster then acc
@@ -237,6 +248,7 @@ let to_json g =
("kind", output_node_kind node.node_kind) ;
("locality", output_node_locality node.node_locality) ;
("precision", output_node_precision node.node_precision) ;
+ ("precision_width", output_node_precision_width node.node_precision) ;
("explored", Json.of_bool node.node_deps_computed)
] :: acc
and output_dep (n1,dep,n2) acc =
--
GitLab