From d97687f7db258cbf97d0ebf5c5c901cc706cf7ba Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 19 Feb 2019 18:38:02 +0100
Subject: [PATCH] [Dive] Generate nodes from alarms
---
src/plugins/dive/build.ml | 66 ++++++++++++++-----
src/plugins/dive/build.mli | 5 +-
src/plugins/dive/graph_types.mli | 2 +-
src/plugins/dive/imprecision_graph.ml | 4 +-
src/plugins/dive/imprecision_graph.mli | 5 +-
src/plugins/dive/main.ml | 14 +++-
src/plugins/dive/node_kind.ml | 26 ++++----
src/plugins/dive/self.ml | 7 +-
src/plugins/dive/self.mli | 2 +-
.../dive/oracle/assigned_param.res.oracle | 2 +-
.../dive/tests/dive/oracle/various.dot | 13 +++-
src/plugins/dive/tests/dive/various.i | 2 +-
12 files changed, 97 insertions(+), 51 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 069c91edd68..d4df4d5751b 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -118,6 +118,11 @@ let build_node_kind ~is_folded_base lval location =
| None ->
Scattered (lval)
+let stmt_to_node_locality stmt =
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let file = get_loc_filename (Kernel_function.get_location kf) in
+ { loc_file = file ; loc_function = Some kf }
+
let build_node_locality kinstr kind =
match Node_kind.get_base kind with
| Some vi ->
@@ -127,10 +132,7 @@ let build_node_locality kinstr kind =
| None ->
match kinstr with
| Kglobal -> assert false
- | Kstmt stmt ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let file = get_loc_filename (Kernel_function.get_location kf) in
- { loc_file = file ; loc_function = Some kf }
+ | Kstmt stmt -> stmt_to_node_locality stmt
(* --- Context object --- *)
@@ -206,6 +208,12 @@ let build_lval context kinstr lval =
Graph.update_node_precision node node_precision;
Some node
+let build_alarm context stmt alarm =
+ let node_kind = Alarm (stmt,alarm)
+ and node_locality = stmt_to_node_locality stmt
+ and node_precision = Critical in
+ Graph.create_node context.graph ~node_precision ~node_kind ~node_locality
+
exception Too_many_deps of lval
let rec build_node_deps context node =
@@ -217,8 +225,8 @@ let rec build_node_deps context node =
build_writes_deps context node (Cil_types.Var vi, Cil_types.NoOffset);
if vi.vformal then build_arg_deps context node vi
| Scattered (_lval) -> () (* TODO: implements *)
- | Alarm (stmt,exp) ->
- build_exp_deps context node stmt Data exp
+ | Alarm (stmt,alarm) ->
+ build_alarm_deps context node stmt alarm
| File -> ()
and build_writes_deps context src lval =
@@ -274,6 +282,22 @@ and build_call_deps context src stmt callee args =
let _,set = !Db.Value.expr_to_kernel_function kinstr ~deps:None callee in
Kernel_function.Hptset.iter (build_return_deps context src stmt args) set
+and build_alarm_deps context src stmt alarm =
+ let for_exp e =
+ build_exp_deps context src stmt Data e
+ in
+ let open Alarms in
+ match alarm with
+ | Division_by_zero e | Index_out_of_bound (e, _) | Invalid_shift (e,_)
+ | Overflow (_,e,_,_) | Float_to_int (e,_,_) | Is_nan_or_infinite (e,_)
+ | Is_nan (e,_) | Function_pointer (e,_) -> for_exp e
+ | Pointer_comparison (opt_e1,e2) -> Extlib.may for_exp opt_e1; for_exp e2
+ | Differing_blocks (e1,e2) -> for_exp e1; for_exp e2
+ | Memory_access _ | Not_separated _ | Overlap _
+ | Uninitialized _ | Dangling _ | Uninitialized_union _ -> ()
+ (* TODO: adress depencies inside lval *)
+ | Invalid_bool lv -> build_lval_deps context src stmt Data lv
+
and build_instr_deps context src stmt = function
| Set (_, exp, _) ->
build_exp_deps context src stmt Data exp
@@ -353,33 +377,39 @@ let unhide_base context vi =
context.hidden_bases <- BaseSet.add vi context.hidden_bases
let should_auto_explore node =
- Node_kind.is_precise node.node_kind
+ match node.node_kind with
+ | Scalar _ | Composite _ | Alarm _ -> true
+ | Scattered _ | File -> false
-let complete_in_depth ~depth_limit context root =
+let complete_in_depth ~depth context root =
context.roots <- root :: context.roots;
(* Breadth first search *)
let queue : (node * int) Queue.t = Queue.create () in
Queue.add (root,0) queue;
while not (Queue.is_empty queue) do
- let v,depth = Queue.take queue in
- if depth < depth_limit then begin
- if not (v.node_deps_computed) && should_auto_explore v then begin
+ let (n,d) = Queue.take queue in
+ if d < depth then begin
+ if not (n.node_deps_computed) && should_auto_explore n then begin
begin try
- build_node_deps context v;
+ build_node_deps context n;
with Too_many_deps lval ->
Self.warning "Too many dependencies for %a ; throwing them out"
Cil_printer.pp_lval lval;
end;
- v.node_deps_computed <- true;
+ n.node_deps_computed <- true;
end;
- Graph.iter_pred (fun w -> Queue.add (w,depth+1) queue) context.graph v
+ Graph.iter_pred (fun n' -> Queue.add (n',d+1) queue) context.graph n
end;
done
-let add_var ?(depth_limit=1) context varinfo =
+let add_var ?(depth=1) context varinfo =
let node = build_var context varinfo in
- Extlib.may (complete_in_depth ~depth_limit context) node
+ Extlib.may (complete_in_depth ~depth context) node
-let add_lval ?(depth_limit=1) context kinstr lval =
+let add_lval ?(depth=1) context kinstr lval =
let node = build_lval context kinstr lval in
- Extlib.may (complete_in_depth ~depth_limit context) node
+ Extlib.may (complete_in_depth ~depth context) node
+
+let add_alarm ?(depth=1) context stmt alarm =
+ let node = build_alarm context stmt alarm in
+ complete_in_depth ~depth context node
diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli
index 299170387ad..23e0d2911d6 100644
--- a/src/plugins/dive/build.mli
+++ b/src/plugins/dive/build.mli
@@ -32,5 +32,6 @@ val fold_base : t -> Cil_types.varinfo -> unit
val hide_base : t -> Cil_types.varinfo -> unit
val unhide_base : t -> Cil_types.varinfo -> unit
-val add_lval : ?depth_limit:int -> t -> Cil_types.kinstr -> Cil_types.lval -> unit
-val add_var : ?depth_limit:int -> t -> Cil_types.varinfo -> unit
+val add_lval : ?depth:int -> t -> Cil_types.kinstr -> Cil_types.lval -> unit
+val add_var : ?depth:int -> t -> Cil_types.varinfo -> unit
+val add_alarm : ?depth:int -> t -> Cil_types.stmt -> Alarms.alarm -> unit
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 85a18a67ad0..59fd3707a55 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -24,7 +24,7 @@ type node_kind =
| Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset
| Composite of Cil_types.varinfo
| Scattered of Cil_types.lval
- | Alarm of Cil_types.stmt * Cil_types.exp
+ | Alarm of Cil_types.stmt * Alarms.alarm
| File (* Dummy node, hack for Ocamlgraph Graphviz Dot module *)
type node_locality = {
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index d55741bfbb9..9c4aab6de23 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -49,12 +49,12 @@ include G
let next_node_key = ref 0
let next_dependency_key = ref 0
-let create_node g ~node_kind ~node_locality =
+let create_node ?(node_precision=Singleton) ~node_kind ~node_locality g =
let node = {
node_key = !next_node_key;
node_kind;
node_locality;
- node_precision = Singleton;
+ node_precision;
node_deps_computed = false;
}
in
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index b5a67e65db0..9598baf375d 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -26,9 +26,10 @@ include Graph.Sig.G with type V.t = node
val create : ?size:int -> unit -> t
-val create_node : t ->
+val create_node :
+ ?node_precision:node_precision ->
node_kind:node_kind ->
- node_locality:node_locality -> node
+ node_locality:node_locality -> t -> node
val update_node_precision : node -> node_precision -> unit
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 51c905e88ab..1f7419db4e3 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -21,15 +21,23 @@
(**************************************************************************)
let main () =
- if not (Self.FromBases.is_empty ()) then begin
+ if not (Self.FromBases.is_empty () &&
+ Self.FromFunctionAlarms.is_empty ()) then begin
(* Create the initial graph *)
let context = Build.create () in
(* Handle parameters *)
Self.UnfoldedBases.iter (Build.unfold_base context);
Self.HiddenBases.iter (Build.hide_base context);
+ let depth = Self.DepthLimit.get () in
(* Add targeted vars to it *)
- let depth_limit = Self.DepthLimit.get () in
- Self.FromBases.iter (Build.add_var ~depth_limit context);
+ Self.FromBases.iter (Build.add_var ~depth context);
+ (* Add alarms *)
+ let add_alarm _emitter kf stmt ~rank:_ alarm _code_annot =
+ if Self.FromFunctionAlarms.mem kf then
+ Build.add_alarm ~depth context stmt alarm
+ in
+ if not (Self.FromFunctionAlarms.is_empty ()) then
+ Alarms.iter add_alarm;
(* Output it *)
let output_basename = Self.OutputBasename.get () in
if output_basename <> "" then begin
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index 54fe77ac895..bbcf645bc16 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -26,10 +26,6 @@ let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
| Scattered _ | Alarm _ | File -> None
-let is_precise = function
- | Scalar _ | Composite _ -> true
- | Scattered _ | Alarm _ | File -> false
-
let to_location = function
| Scalar (vi,typ,offset) ->
let base = Base.of_varinfo vi in
@@ -38,15 +34,15 @@ let to_location = function
Some (Locations.loc_of_varinfo vi)
| Scattered _ | Alarm _ | File -> None
-let to_cil = function
- | Scalar (vi,_typ,offset) -> `Lval (Cil_types.Var vi, offset)
- | Composite (vi) -> `Lval (Cil_types.Var vi, Cil_types.NoOffset)
- | Scattered (lval) -> `Lval lval
- | Alarm (_stmt,exp) -> `Exp exp
- | File -> `None
+let to_lval = function
+ | Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
+ | Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
+ | Scattered (lval) -> Some lval
+ | Alarm (_,_) | File -> None
-let pretty fmt kind =
- match to_cil kind with
- | `Lval lval -> Cil_printer.pp_lval fmt lval
- | `Exp exp -> Cil_printer.pp_exp fmt exp
- | `None -> ()
+let pretty fmt = function
+ | (Scalar _ | Composite _ | Scattered _) as kind ->
+ Cil_printer.pp_lval fmt (Extlib.the (to_lval kind))
+ | Alarm (_stmt,alarm) ->
+ Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)
+ | File -> ()
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 09a9616fd6b..87adec5f7ee 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -44,10 +44,11 @@ module DepthLimit = Int
let default = 3
end)
-module FromAlarms = True
+module FromFunctionAlarms = Kernel_function_set
(struct
- let option_name = "-dive-from-alarms"
- let help = "Build the graph from alarms presents in the code."
+ let option_name = "-dive-from-function-alarms"
+ let help = "Build the graph from alarms presents in the functions."
+ let arg_name = "f1,..."
end)
module Varinfo =
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index 8d9f9f8b0ec..77fdb5a3f8f 100644
--- a/src/plugins/dive/self.mli
+++ b/src/plugins/dive/self.mli
@@ -28,7 +28,7 @@ module type Varinfo_set = Parameter_sig.Set
module OutputBasename : Parameter_sig.String
module DepthLimit : Parameter_sig.Int
-module FromAlarms : Parameter_sig.Bool
+module FromFunctionAlarms : Parameter_sig.Kernel_function_set
module FromBases : Varinfo_set
module UnfoldedBases : Varinfo_set
module HiddenBases : Varinfo_set
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
index 01978d95470..cdf86a2a995 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
@@ -2,7 +2,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva:alarm] tests/dive/assigned_param.i:18: Warning:
+[eva:alarm] tests/dive/assigned_param.i:17: Warning:
signed overflow. assert w + 1 ≤ 2147483647;
[eva] done for function main
[dive] output to tests/dive/result/assigned_param.dot
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index e9d2bb149ea..acc4db37e9f 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -18,11 +18,17 @@ digraph G {
style="filled", ];
cp9 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled,dotted", ];
+ cp10 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
+ shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000",
+ style="bold,filled,bold", ];
+ cp11 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
+ shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000",
+ style="bold,filled,bold", ];
subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0;
- subgraph cluster_function_19 { label=<f>; cp2;cp1;
+ subgraph cluster_function_19 { label=<f>; cp10;cp2;cp1;
};
- subgraph cluster_function_24 { label=<main>; cp9;cp8;cp7;cp6;cp5;cp3;
+ subgraph cluster_function_24 { label=<main>; cp11;cp9;cp8;cp7;cp6;cp5;cp3;
};
};
@@ -30,10 +36,13 @@ digraph G {
cp1 -> cp6;
cp1 -> cp8;
cp2 -> cp1;
+ cp2 -> cp10;
cp3 -> cp1;
cp4 -> cp3;
cp6 -> cp5;
+ cp6 -> cp11;
cp7 -> cp5;
+ cp7 -> cp11;
cp8 -> cp7;
cp9 -> cp8 [color="#00FF00", ];
diff --git a/src/plugins/dive/tests/dive/various.i b/src/plugins/dive/tests/dive/various.i
index 84c0f7788f7..c8766e6a7ad 100644
--- a/src/plugins/dive/tests/dive/various.i
+++ b/src/plugins/dive/tests/dive/various.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from main::z,f::x2"
+STDOPT: +"-dive-from main::z,f::x2 -dive-from-function-alarms f,main"
*/
float g;
--
GitLab