From f3012a85fa338b88e50a48a31075b10a2f3a2960 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sun, 17 Feb 2019 17:22:40 +0100
Subject: [PATCH] [Dive] Fix folded locations
---
src/plugins/dive/build.ml | 17 ++++++++++++-----
src/plugins/dive/graph_types.mli | 2 +-
src/plugins/dive/node_kind.ml | 13 ++++++++++---
3 files changed, 23 insertions(+), 9 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 5541adf826f..da7ebe43aa7 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -106,7 +106,7 @@ let build_node_kind ~is_folded_base lval location =
let offset = Ival.project_int ival
and matching = Bit_utils.MatchType typ in
let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in
- Scalar (vi, offset')
+ Scalar (vi, typ, offset')
with Ival.Not_Singleton_Int ->
Scattered (lval)
end
@@ -175,7 +175,13 @@ let build_node context kinstr location lval =
reference_file context node_locality.loc_file;
Graph.create_vertex context.graph ~node_kind ~node_locality
in
- let node = NodeTable.memo context.node_table location build_new_node in
+ (* Compute the new location which might have changed after folding *)
+ let location' =
+ match Node_kind.to_location node_kind with
+ | None -> location
+ | Some location' -> location'
+ in
+ let node = NodeTable.memo context.node_table location' build_new_node in
Some node
end
@@ -199,7 +205,7 @@ exception Too_many_deps of lval
let rec build_node_deps context node =
match node.node_kind with
- | Scalar (vi,offset) ->
+ | Scalar (vi,_typ,offset) ->
build_writes_deps context node (Cil_types.Var vi, offset);
if vi.vformal then build_arg_deps context node vi
| Composite (vi) ->
@@ -220,8 +226,9 @@ and build_writes_deps context src lval =
| _ -> ()
in
if List.length writes > 20 then
- raise (Too_many_deps lval);
- List.iter add_deps writes;
+ raise (Too_many_deps lval)
+ else
+ List.iter add_deps writes
and build_arg_deps context src vi =
assert vi.vformal;
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 81920d87b5d..0ea7ae35270 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
type node_kind =
- | Scalar of Cil_types.varinfo * Cil_types.offset
+ | 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
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index b5741e5e0a4..54fe77ac895 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -23,15 +23,23 @@
open Graph_types
let get_base = function
- | Scalar (vi,_) | Composite (vi) -> Some vi
+ | 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
+ Some (Locations.loc_of_typoffset base typ offset)
+ | Composite (vi) ->
+ Some (Locations.loc_of_varinfo vi)
+ | Scattered _ | Alarm _ | File -> None
+
let to_cil = function
- | Scalar (vi,offset) -> `Lval (Cil_types.Var vi, offset)
+ | 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
@@ -42,4 +50,3 @@ let pretty fmt kind =
| `Lval lval -> Cil_printer.pp_lval fmt lval
| `Exp exp -> Cil_printer.pp_exp fmt exp
| `None -> ()
-
--
GitLab