From 534a47c45448215cf0ac39f50ff2cc5743166f1a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sun, 9 Oct 2022 00:32:38 +0200
Subject: [PATCH] [Dive] Update nodes values each time a write is detected
- also for the special case of formal parameters
- values gathered should now be consistent with the partial graph built
---
src/plugins/dive/build.ml | 49 ++++++++++++++-----
.../dive/tests/dive/oracle/assigned_param.dot | 3 +-
.../tests/dive/oracle/callstack_global.dot | 3 +-
.../tests/dive/oracle/callstack_strategy.dot | 3 +-
src/plugins/dive/tests/dive/oracle/const.dot | 3 +-
.../dive/tests/dive/oracle/exceptional.dot | 3 +-
src/plugins/dive/tests/dive/oracle/global.dot | 3 +-
.../dive/tests/dive/oracle/manydeps.dot | 3 +-
.../dive/tests/dive/oracle/per_callstack.dot | 3 +-
.../dive/tests/dive/oracle/pointed_param.dot | 3 +-
src/plugins/dive/tests/dive/oracle/ranges.dot | 3 +-
.../dive/tests/dive/oracle/various.dot | 9 ++--
12 files changed, 61 insertions(+), 27 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 2e86d33bb6c..b013a4ca0ee 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -87,12 +87,17 @@ module Eval =
struct
open Eva.Results
+ let rq kinstr =
+ match kinstr with
+ | Kglobal -> at_start
+ | Kstmt stmt -> after stmt
+
let to_kf_list kinstr callee =
before_kinstr kinstr |> eval_callee callee |>
Result.value ~default:[]
let to_cvalue kinstr lval =
- before_kinstr kinstr |> eval_lval lval |> as_cvalue
+ rq kinstr |> eval_lval lval |> as_cvalue
let to_location kinstr lval =
before_kinstr kinstr |> eval_address lval |> as_location
@@ -105,7 +110,7 @@ struct
let is_tainted kinstr lval =
let zone = to_zone kinstr lval in
- before_kinstr kinstr |> is_tainted zone |> Result.to_option
+ rq kinstr |> is_tainted zone |> Result.to_option
let studia_direct_effect = function
| e, { Studia.Writes.direct = true } -> Some e
@@ -141,11 +146,27 @@ end
(* --- Precision evaluation --- *)
-let update_node_values node kinstr lval =
- let typ = Cil.typeOfLval lval
- and cvalue = Eval.to_cvalue kinstr lval
- and taint = Eval.is_tainted kinstr lval in
- Graph.update_node_values node ~typ ~cvalue ~taint
+(* For folded bases, lval may be strictly included in the node zone *)
+let update_node_values node ?(lval=Node_kind.to_lval node.node_kind) kinstr =
+ match lval with
+ | None -> () (* can't evaluate node *)
+ | Some lval ->
+ (* Evaluate parameters inside functions instead that at call point *)
+ let kinstr =
+ match lval with
+ | (Var vi,_) when vi.vformal ->
+ let kf = Option.get (Kernel_function.find_defining_kf vi) in
+ begin try
+ Kstmt (Kernel_function.find_first_stmt kf)
+ with
+ Kernel_function.No_Statement -> kinstr
+ end
+ | _ -> kinstr
+ in
+ let typ = Cil.typeOfLval lval
+ and cvalue = Eval.to_cvalue kinstr lval
+ and taint = Eval.is_tainted kinstr lval in
+ Graph.update_node_values node ~typ ~cvalue ~taint
(* --- Locations handling --- *)
@@ -269,7 +290,7 @@ let build_var context callstack varinfo =
let build_lval context callstack kinstr lval =
let node = build_node context callstack lval kinstr in
- update_node_values node kinstr lval;
+ update_node_values ~lval:(Some lval) node kinstr;
node
let build_const context callstack exp =
@@ -292,6 +313,9 @@ let build_node_writes context node =
let rec build_write_deps callstack kinstr lval : deps_builder =
let add_deps = function
| { skind=Instr instr } as stmt ->
+ (* Update the values at the light of new discovered write *)
+ update_node_values node (Kstmt stmt);
+ (* Add dependencies for each callstack *)
List.to_seq (find_compatible_callstacks stmt callstack) |>
Seq.flat_map (fun cs -> build_instr_deps cs stmt instr)
| _ -> assert false (* Studia invariant *)
@@ -306,7 +330,9 @@ let build_node_writes context node =
List.to_seq (EnumLvals.in_alarm alarm) |>
Seq.flat_map (build_lval_deps callstack stmt Data)
- and build_instr_deps callstack stmt : Cil_types.instr -> deps_builder = function
+ and build_instr_deps callstack stmt instr : deps_builder =
+ (* Add dependencies found in the instruction *)
+ match instr with
| Set (_, exp, _) ->
build_exp_deps callstack stmt Data exp
| Call (_, callee, args, _) ->
@@ -394,10 +420,7 @@ let build_node_writes context node =
and build_scattered_deps callstack kinstr lval : deps_builder =
let add_cell node_kind =
let node' = add_or_update_node context callstack node_kind in
- begin match Node_kind.to_lval node_kind with
- | Some lval' -> update_node_values node kinstr lval';
- | _ -> ()
- end;
+ update_node_values node kinstr;
Graph.create_dependency graph kinstr node' Composition node
in
enumerate_cells ~is_folded_base lval kinstr |> Seq.map add_cell
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
index 198c8cfc1b7..a1190d2d94f 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<w>, shape=box, style="bold", ];
+ cp2 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_global.dot b/src/plugins/dive/tests/dive/oracle/callstack_global.dot
index 620122edbd9..7de57293c7e 100644
--- a/src/plugins/dive/tests/dive/oracle/callstack_global.dot
+++ b/src/plugins/dive/tests/dive/oracle/callstack_global.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<r>, shape=box, style="bold", ];
+ cp2 [label=<r>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled,bold", ];
cp3 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
cp5 [label=<tmp_0>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
index 0ef329150cf..1944fac8cbf 100644
--- a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<r>, shape=box, style="bold", ];
+ cp2 [label=<r>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
index 6ea580760fe..bb67ee0a8f1 100644
--- a/src/plugins/dive/tests/dive/oracle/const.dot
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<res>, shape=box, style="bold", ];
+ cp2 [label=<res>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<c>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.dot b/src/plugins/dive/tests/dive/oracle/exceptional.dot
index a512210f1c4..b2e11483ced 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.dot
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<__retres>, shape=box, style="bold", ];
+ cp2 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot
index de476dbaf1e..36c6ca1aa9f 100644
--- a/src/plugins/dive/tests/dive/oracle/global.dot
+++ b/src/plugins/dive/tests/dive/oracle/global.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<z>, shape=box, style="bold", ];
+ cp2 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<g>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot
index 6f314995b98..844c7191d6d 100644
--- a/src/plugins/dive/tests/dive/oracle/manydeps.dot
+++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot
@@ -11,7 +11,8 @@ digraph G {
style="filled", ];
cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp14 [label=<__retres>, shape=box, style="bold", ];
+ cp14 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled,bold", ];
cp15 [label=<0>, shape=ellipse, ];
cp17 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
color="#88AAFF", style="filled,dotted", ];
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.dot b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
index 22fa39f4a0b..0ae6f71c8c4 100644
--- a/src/plugins/dive/tests/dive/oracle/per_callstack.dot
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<w>, shape=box, style="bold", ];
+ cp2 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/pointed_param.dot b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
index f2713a435f6..92f57336174 100644
--- a/src/plugins/dive/tests/dive/oracle/pointed_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<y>, shape=box, style="bold", ];
+ cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/ranges.dot b/src/plugins/dive/tests/dive/oracle/ranges.dot
index 5a8ea529a6c..4c9ebfa3ebd 100644
--- a/src/plugins/dive/tests/dive/oracle/ranges.dot
+++ b/src/plugins/dive/tests/dive/oracle/ranges.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<res>, shape=box, style="bold", ];
+ cp2 [label=<res>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<i>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<f>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index 26e624b5675..6e3b9370076 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -1,5 +1,5 @@
digraph G {
- cp2 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp2 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
@@ -7,12 +7,13 @@ digraph G {
style="filled", ];
cp8 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp11 [label=<z>, shape=box, style="bold", ];
+ cp11 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp12 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp14 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp16 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp16 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
cp18 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
@@ -20,7 +21,7 @@ digraph G {
style="filled", ];
cp23 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp25 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp25 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
cp29 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
--
GitLab