From 28ee2282c4e0b4acd526ed51ca2a59e10aa74629 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 27 Aug 2019 16:35:05 +0200
Subject: [PATCH] [Dive] Scattered nodes are identified by statement and can be
explored
---
src/plugins/dive/build.ml | 65 ++++++++++++++++++--------------
src/plugins/dive/graph_types.mli | 2 +-
src/plugins/dive/node_kind.ml | 33 ++++++----------
src/plugins/dive/node_kind.mli | 1 -
4 files changed, 49 insertions(+), 52 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 9dc8ff560a0..91a9ba52e59 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -163,7 +163,9 @@ let build_simple_location lval (l : Locations.location)
end
| _ -> None
-let build_node_kind ~is_folded_base lval location =
+let build_node_kind ~is_folded_base lval kinstr =
+ (* If possible, refine the lval to a non-symbolic one *)
+ let location = !Db.Value.lval_to_loc kinstr lval in
match build_simple_location lval location with
| Some (vi, ival) ->
if is_foldable_type vi.vtype && is_folded_base vi then
@@ -177,10 +179,10 @@ let build_node_kind ~is_folded_base lval location =
Scalar (vi, typ, offset')
with Bit_utils.NoMatchingOffset | Ival.Not_Singleton_Int ->
(* TODO: handle Bit_utils.NoMatchingOffset (strict aliasing ?) *)
- Scattered (lval, location)
+ Scattered (lval, kinstr)
end
| None ->
- Scattered (lval, location)
+ Scattered (lval, kinstr)
let default_node_locality callstack =
match callstack with
@@ -276,21 +278,18 @@ let remove_node context node =
(* --- Graph building --- *)
(* Update or create a node *)
-let build_node context callstack location lval =
+let build_node context callstack lval kinstr =
let is_folded_base = is_folded context in
- let node_kind = build_node_kind ~is_folded_base lval location in
+ let node_kind = build_node_kind ~is_folded_base lval kinstr in
let node_locality = build_node_locality callstack node_kind in
add_node context ~node_kind ~node_locality
let build_var context callstack varinfo =
- let location = Locations.loc_of_varinfo varinfo
- and lval = Var varinfo, NoOffset in
- build_node context callstack location lval
+ let lval = Var varinfo, NoOffset in
+ build_node context callstack lval Kglobal
let build_lval context callstack kinstr lval =
- (* If possible, refine the lval to a non-symbolic one *)
- let location = !Db.Value.lval_to_loc kinstr lval in
- let node = build_node context callstack location lval in
+ let node = build_node context callstack lval kinstr in
update_node_values node kinstr lval;
node
@@ -300,12 +299,15 @@ let build_alarm context callstack stmt alarm =
add_node context ~node_kind ~node_locality
-exception Too_many_deps of lval
+exception Too_many_deps
let build_node_deps context node =
- let rec build_writes_deps callstack lval =
- Self.debug ~dkey "computing deps for %a" Cil_printer.pp_lval lval;
- let zone = !Db.Value.lval_to_zone Kglobal lval in
+ let rec build_lval_write_deps callstack kinstr lval =
+ let zone = !Db.Value.lval_to_zone kinstr lval in
+ build_write_deps callstack zone
+
+ and build_write_deps callstack zone =
+ Self.debug ~dkey "computing deps for %a" Node_kind.pretty node.node_kind;
let writes = Studia.Writes.compute zone
and add_deps (stmt,effects) =
match stmt.skind with
@@ -341,7 +343,7 @@ let build_node_deps context node =
let count = List.length writes in
Self.debug ~dkey "%d found" count;
if count > 20 then
- raise (Too_many_deps lval)
+ raise Too_many_deps
else
List.iter add_deps writes
@@ -449,16 +451,23 @@ let build_node_deps context node =
in
update_node context node;
let callstack = node.node_locality.loc_callstack in
- match node.node_kind with
- | Scalar (vi,_typ,offset) ->
- build_writes_deps callstack (Cil_types.Var vi, offset);
- if vi.vformal then build_arg_deps callstack vi
- | Composite (vi) ->
- build_writes_deps callstack (Cil_types.Var vi, Cil_types.NoOffset);
- if vi.vformal then build_arg_deps callstack vi
- | Scattered (_lval, _location) -> () (* TODO: implements *)
- | Alarm (stmt,alarm) ->
- build_alarm_deps callstack stmt alarm
+ begin match node.node_kind with
+ | Scalar (vi,_typ,offset) ->
+ let lval = (Cil_types.Var vi, offset) in
+ build_lval_write_deps callstack Kglobal lval
+ | Composite (vi) ->
+ let lval = (Cil_types.Var vi, Cil_types.NoOffset) in
+ build_lval_write_deps callstack Kglobal lval
+ | Scattered (lval,kinstr) ->
+ build_lval_write_deps callstack kinstr lval
+ | Alarm (stmt,alarm) ->
+ build_alarm_deps callstack stmt alarm
+ end;
+ begin match Node_kind.get_base node.node_kind with
+ (* TODO refine formal dependency computation for non-scalar formals *)
+ | Some vi when vi.vformal -> build_arg_deps callstack vi
+ | _ -> ()
+ end
(* --- Graph initialization --- *)
@@ -527,10 +536,10 @@ let explore ~depth context root =
begin
begin try
build_node_deps context n;
- with Too_many_deps lval ->
+ with Too_many_deps ->
(* TODO: give a mean to explore more dependencies *)
Self.warning "Too many dependencies for %a ; throwing them out"
- Cil_printer.pp_lval lval;
+ Node_kind.pretty n.node_kind;
end;
n.node_deps_computed <- true;
end;
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index e98e37d3063..b66fa2ace0e 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -23,7 +23,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 * Locations.location
+ | Scattered of Cil_types.lval * Cil_types.kinstr
| Alarm of Cil_types.stmt * Alarms.alarm
type node_locality = {
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index a59e6de12f3..b63fe2a0be6 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -26,6 +26,8 @@ module DatatypeInput =
struct
include Datatype.Undefined
+ open Cil_datatype
+
type t = node_kind
let (<?>) c (cmp,x,y) =
@@ -36,12 +38,11 @@ struct
let name = "Node_kind"
let reprs = [ Scalar (
- List.hd Cil_datatype.Varinfo.reprs,
- List.hd Cil_datatype.Typ.reprs,
- List.hd Cil_datatype.Offset.reprs) ]
+ List.hd Varinfo.reprs,
+ List.hd Typ.reprs,
+ List.hd Offset.reprs) ]
let compare k1 k2 =
- let open Cil_datatype in
match k1, k2 with
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.compare vi1 vi2 <?> (OffsetStructEq.compare, offset1, offset2)
@@ -50,33 +51,31 @@ struct
| Composite vi1, Composite vi2 -> Varinfo.compare vi1 vi2
| Composite _, _ -> 1
| _, Composite _ -> -1
- | Scattered (lv1,loc1), Scattered (lv2,loc2) ->
- LvalStructEq.compare lv1 lv2 <?> (Locations.Location.compare, loc1, loc2)
+ | Scattered (lv1,ki1), Scattered (lv2,ki2) ->
+ LvalStructEq.compare lv1 lv2 <?> (Kinstr.compare, ki1, ki2)
| Scattered _, _ -> 1
| _, Scattered _ -> -1
| Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2)
let equal k1 k2 =
- let open Cil_datatype in
match k1, k2 with
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
| Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
- | Scattered (lv1, loc1), Scattered (lv2, loc2) ->
- LvalStructEq.equal lv1 lv2 && Locations.Location.equal loc1 loc2
+ | Scattered (lv1, ki1), Scattered (lv2, ki2) ->
+ LvalStructEq.equal lv1 lv2 && Kinstr.equal ki1 ki2
| Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
| _ -> false
let hash k =
- let open Cil_datatype in
match k with
| Scalar (vi, _, offset) ->
Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
| Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
- | Scattered (lv, loc) ->
- Hashtbl.hash (3, LvalStructEq.hash lv, Locations.Location.hash loc)
+ | Scattered (lv, ki) ->
+ Hashtbl.hash (3, LvalStructEq.hash lv, Kinstr.hash ki)
| Alarm (stmt, alarm) ->
Hashtbl.hash (4, Stmt.hash stmt, Alarms.hash alarm)
end
@@ -88,16 +87,6 @@ let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
| Scattered _ | Alarm _ -> None
-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 (_,loc) ->
- Some loc
- | Alarm _ -> 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)
diff --git a/src/plugins/dive/node_kind.mli b/src/plugins/dive/node_kind.mli
index 9d4bcefed67..160f1b80f44 100644
--- a/src/plugins/dive/node_kind.mli
+++ b/src/plugins/dive/node_kind.mli
@@ -23,5 +23,4 @@
include Datatype.S with type t = Graph_types.node_kind
val get_base : t -> Cil_types.varinfo option
-val to_location : t -> Locations.location option
val to_lval : t -> Cil_types.lval option
--
GitLab