From 1847a8a9c4b2cfac343c19caa7ea35fda773e11d Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 8 Oct 2022 13:45:42 +0200
Subject: [PATCH] [Dive] Add constant nodes
---
ivette/src/frama-c/plugins/dive/style.json | 9 +++
src/plugins/dive/build.ml | 17 ++++--
src/plugins/dive/dive_graph.ml | 2 +
src/plugins/dive/dive_types.ml | 1 +
src/plugins/dive/node_kind.ml | 14 ++++-
.../dive/tests/dive/oracle/manydeps.dot | 8 ++-
src/plugins/dive/tests/dive/oracle/ranges.dot | 58 ++++++++++++++++++-
7 files changed, 98 insertions(+), 11 deletions(-)
diff --git a/ivette/src/frama-c/plugins/dive/style.json b/ivette/src/frama-c/plugins/dive/style.json
index 9b4b706fcba..b218be3b0e8 100644
--- a/ivette/src/frama-c/plugins/dive/style.json
+++ b/ivette/src/frama-c/plugins/dive/style.json
@@ -141,6 +141,15 @@
"background-color": "#e44"
}
},
+ {
+ "selector": "node[kind='const']",
+ "style": {
+ "shape": "ellipse",
+ "background-color": "#bbb",
+ "border-width": "1px",
+ "border-style": "dashed"
+ }
+ },
{
"selector": "node[kind='alarm']",
"style": {
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index a8ef4ad5078..9952c76cf11 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -265,6 +265,9 @@ let build_lval context callstack kinstr lval =
update_node_values node kinstr lval;
node
+let build_const context callstack exp =
+ add_or_update_node context callstack (Const exp)
+
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
let node_locality = build_node_locality callstack node_kind in
@@ -367,8 +370,14 @@ let build_node_writes context node =
Seq.append callee_deps return_deps
and build_exp_deps callstack stmt kind exp : deps_builder =
- List.to_seq (EnumLvals.in_exp exp) |>
- Seq.flat_map (build_lval_deps callstack stmt kind)
+ let lvals = EnumLvals.in_exp exp in
+ if lvals <> [] then
+ List.to_seq lvals |>
+ Seq.flat_map (build_lval_deps callstack stmt kind)
+ else
+ let kinstr = Kstmt stmt in
+ let dst = build_const context callstack exp in
+ Seq.return (Graph.create_dependency graph kinstr dst kind node)
and build_lval_deps callstack stmt kind lval : deps_builder =
let kinstr = Kstmt stmt in
@@ -397,7 +406,7 @@ let build_node_writes context node =
build_scattered_deps callstack kinstr lval
| Alarm (stmt,alarm) ->
build_alarm_deps callstack stmt alarm
- | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+ | Unknown _ | AbsoluteMemory | String _ | Const _ | Error _ ->
Seq.empty
@@ -512,7 +521,7 @@ let build_node_reads context node =
build_reads_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (_lval,kinstr) ->
build_kinstr_deps callstack None kinstr
- | Alarm _ | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+ | Alarm _ | Unknown _ | AbsoluteMemory | Const _ | String _ | Error _ ->
Seq.empty
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 1c60f09ba34..0b3f40c3240 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -233,6 +233,7 @@ let ouptput_to_dot out_channel g =
`Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ]
| AbsoluteMemory | String _ -> [`Shape `Box3d]
+ | Const _ -> [`Shape `Ellipse]
| Error _ -> [`Color 0xff0000]
and range = match v.node_range with
| Empty -> []
@@ -295,6 +296,7 @@ struct
| Alarm _ -> "alarm"
| AbsoluteMemory -> "absolute"
| String _ -> "string"
+ | Const _ -> "const"
| Error _ -> "error"
in
`String s
diff --git a/src/plugins/dive/dive_types.ml b/src/plugins/dive/dive_types.ml
index 9f4235dc75f..744900c6ee9 100644
--- a/src/plugins/dive/dive_types.ml
+++ b/src/plugins/dive/dive_types.ml
@@ -28,6 +28,7 @@ type node_kind =
| Alarm of Cil_types.stmt * Alarms.alarm
| AbsoluteMemory
| String of int * Base.cstring
+ | Const of Cil_types.exp
| Error of string
type callstack = Callstack.t
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index 40e5bedeaf8..03db93576e5 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -70,6 +70,10 @@ struct
Datatype.Int.compare i1 i2
| String _, _ -> 1
| _, String _ -> -1
+ | Const (e1), Const(e2) ->
+ Cil_datatype.Exp.compare e1 e2
+ | Const _, _ -> 1
+ | _, Const _ -> -1
| Error s1, Error s2 ->
Datatype.String.compare s1 s2
@@ -86,6 +90,7 @@ struct
Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
| AbsoluteMemory, AbsoluteMemory -> true
| String (i,_), String (j,_) -> Datatype.Int.equal i j
+ | Const (e1), Const(e2) -> Cil_datatype.Exp.equal e1 e2
| Error s1, Error s2 -> Datatype.String.equal s1 s2
| _ -> false
@@ -102,6 +107,7 @@ struct
Hashtbl.hash (5, Stmt.hash stmt, Alarms.hash alarm)
| AbsoluteMemory -> 6
| String (i, _) -> Hashtbl.hash (7, i)
+ | Const (e) -> Hashtbl.hash (7, Cil_datatype.Exp.hash e)
| Error s -> Hashtbl.hash (8, s)
end
@@ -110,15 +116,15 @@ include Datatype.Make (DatatypeInput)
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
- | Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory | String _ | Error _ ->
- None
+ | Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory
+ | String _ | Const _ | Error _ -> 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
| Unknown (lval,_) -> Some lval
- | Alarm (_,_) | AbsoluteMemory | String _ | Error _ -> None
+ | Alarm (_,_) | AbsoluteMemory | String _ | Const _ | Error _ -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind ->
@@ -131,5 +137,7 @@ let pretty fmt = function
Format.fprintf fmt "%S" s
| String (_, CSWstring s) ->
Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s)
+ | Const (e) ->
+ Format.fprintf fmt "%a" Cil_printer.pp_exp e
| Error s ->
Format.fprintf fmt "%s" s
diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot
index bcffeba804e..6f314995b98 100644
--- a/src/plugins/dive/tests/dive/oracle/manydeps.dot
+++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot
@@ -12,12 +12,13 @@ digraph G {
cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
cp14 [label=<__retres>, shape=box, style="bold", ];
- cp15 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
+ cp15 [label=<0>, shape=ellipse, ];
+ cp17 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
color="#88AAFF", style="filled,dotted", ];
subgraph cluster_cs_1 { label=<many_writes>; cp12;cp10;cp8;cp6;cp4;cp2;
};
- subgraph cluster_cs_2 { label=<many_values>; cp15;cp14;
+ subgraph cluster_cs_2 { label=<many_values>; cp17;cp15;cp14;
};
cp2 -> cp2 [style="bold", ];
@@ -26,6 +27,7 @@ digraph G {
cp8 -> cp2;
cp10 -> cp2;
cp12 -> cp2;
- cp15 -> cp14;
+ cp15 -> cp14 [style="bold", ];
+ cp17 -> cp14;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/ranges.dot b/src/plugins/dive/tests/dive/oracle/ranges.dot
index c6e74f511d0..5a8ea529a6c 100644
--- a/src/plugins/dive/tests/dive/oracle/ranges.dot
+++ b/src/plugins/dive/tests/dive/oracle/ranges.dot
@@ -36,8 +36,36 @@ digraph G {
style="filled", ];
cp37 [label=<f7>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
+ cp39 [label=<0>, shape=ellipse, ];
+ cp41 [label=<3>, shape=ellipse, ];
+ cp43 [label=<0>, shape=ellipse, ];
+ cp45 [label=<12>, shape=ellipse, ];
+ cp47 [label=<0>, shape=ellipse, ];
+ cp49 [label=<127>, shape=ellipse, ];
+ cp51 [label=<0>, shape=ellipse, ];
+ cp53 [label=<42000>, shape=ellipse, ];
+ cp55 [label=<0>, shape=ellipse, ];
+ cp57 [label=<1350000>, shape=ellipse, ];
+ cp59 [label=<0>, shape=ellipse, ];
+ cp61 [label=<910000000>, shape=ellipse, ];
+ cp63 [label=<0>, shape=ellipse, ];
+ cp65 [label=<2000000000>, shape=ellipse, ];
+ cp67 [label=<0.f>, shape=ellipse, ];
+ cp69 [label=<0.001f>, shape=ellipse, ];
+ cp71 [label=<0.f>, shape=ellipse, ];
+ cp73 [label=<3.14f>, shape=ellipse, ];
+ cp75 [label=<0.f>, shape=ellipse, ];
+ cp77 [label=<1020.f>, shape=ellipse, ];
+ cp79 [label=<0.f>, shape=ellipse, ];
+ cp81 [label=<1e7f>, shape=ellipse, ];
+ cp83 [label=<0.f>, shape=ellipse, ];
+ cp85 [label=<1e20f>, shape=ellipse, ];
+ cp87 [label=<0.f>, shape=ellipse, ];
+ cp89 [label=<1e36f>, shape=ellipse, ];
+ cp91 [label=<0.f>, shape=ellipse, ];
+ cp93 [label=<1e37f>, shape=ellipse, ];
- subgraph cluster_cs_1 { label=<main>; cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
+ subgraph cluster_cs_1 { label=<main>; cp93;cp91;cp89;cp87;cp85;cp83;cp81;cp79;cp77;cp75;cp73;cp71;cp69;cp67;cp65;cp63;cp61;cp59;cp57;cp55;cp53;cp51;cp49;cp47;cp45;cp43;cp41;cp39;cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
};
cp3 -> cp2;
@@ -58,5 +86,33 @@ digraph G {
cp33 -> cp5;
cp35 -> cp5;
cp37 -> cp5;
+ cp39 -> cp9;
+ cp41 -> cp9;
+ cp43 -> cp11;
+ cp45 -> cp11;
+ cp47 -> cp13;
+ cp49 -> cp13;
+ cp51 -> cp15;
+ cp53 -> cp15;
+ cp55 -> cp17;
+ cp57 -> cp17;
+ cp59 -> cp19;
+ cp61 -> cp19;
+ cp63 -> cp21;
+ cp65 -> cp21;
+ cp67 -> cp25;
+ cp69 -> cp25;
+ cp71 -> cp27;
+ cp73 -> cp27;
+ cp75 -> cp29;
+ cp77 -> cp29;
+ cp79 -> cp31;
+ cp81 -> cp31;
+ cp83 -> cp33;
+ cp85 -> cp33;
+ cp87 -> cp35;
+ cp89 -> cp35;
+ cp91 -> cp37;
+ cp93 -> cp37;
}
\ No newline at end of file
--
GitLab