From 3b5c79e88a36f1a5fb010bfa9a5bc26cc4753416 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 25 Oct 2022 17:51:28 +0200
Subject: [PATCH] [Dive] Small fix to the evaluation of formal parameters.
---
src/plugins/dive/build.ml | 32 ++++++++++---------
.../dive/tests/dive/oracle/various.dot | 6 ++--
2 files changed, 20 insertions(+), 18 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 74ca6330a46..4ff42c4f711 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -96,8 +96,8 @@ struct
before_kinstr kinstr |> eval_callee callee |>
Result.value ~default:[]
- let to_cvalue kinstr lval =
- rq kinstr |> eval_lval lval |> as_cvalue
+ let to_cvalue request lval =
+ eval_lval lval request |> as_cvalue
let to_location kinstr lval =
before_kinstr kinstr |> eval_address lval |> as_location
@@ -108,9 +108,9 @@ struct
let to_callstacks stmt =
before stmt |> callstacks
- let is_tainted kinstr lval =
- let zone = to_zone kinstr lval in
- rq kinstr |> is_tainted zone |> Result.to_option
+ let is_tainted request lval =
+ let zone = eval_address lval request |> as_zone in
+ is_tainted zone request |> Result.to_option
let studia_direct_effect = function
| e, { Studia.Writes.direct = true } -> Some e
@@ -146,26 +146,28 @@ end
(* --- Precision evaluation --- *)
+let kf_contains_kinstr kf = function
+ | Kglobal -> false
+ | Kstmt stmt -> Kernel_function.(equal (find_englobing_kf stmt) kf)
+
(* 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 =
+ (* Evaluate parameters inside their functions rather than at call sites. *)
+ let request =
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
+ if kf_contains_kinstr kf kinstr
+ then Eval.rq kinstr
+ else Eva.Results.at_start_of kf
+ | _ -> Eval.rq kinstr
in
let typ = Cil.typeOfLval lval
- and cvalue = Eval.to_cvalue kinstr lval
- and taint = Eval.is_tainted kinstr lval in
+ and cvalue = Eval.to_cvalue request lval
+ and taint = Eval.is_tainted request lval in
Graph.update_node_values node ~typ ~cvalue ~taint
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index f18754cae5a..d661acee21a 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="#EEFFEE", color="#004400",
+ cp2 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
@@ -13,7 +13,7 @@ digraph G {
style="filled", ];
cp14 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp16 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp16 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp18 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
@@ -21,7 +21,7 @@ digraph G {
style="filled", ];
cp23 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp25 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp25 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp28 [label=<& f>, shape=ellipse, ];
cp31 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
--
GitLab