From e9f8c9f101f3f29abccb176af3bc81600af7068d Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Sun, 9 Oct 2022 00:52:21 +0200 Subject: [PATCH] [Dive] Also add Const nodes for Local_init --- src/plugins/dive/build.ml | 14 ++- .../tests/dive/oracle/callstack_global.dot | 6 +- .../dive/tests/dive/oracle/manydeps.dot | 24 +++-- .../tests/dive/oracle/pointers_to_local.dot | 16 ++-- src/plugins/dive/tests/dive/oracle/ranges.dot | 92 ++++++++++--------- .../dive/tests/dive/oracle/various.dot | 24 ++--- 6 files changed, 104 insertions(+), 72 deletions(-) diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index b013a4ca0ee..19681116427 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -343,8 +343,18 @@ let build_node_writes context node = in Cil.treat_constructor_as_func as_func dest f args k loc | Local_init (vi, AssignInit init, _) -> - List.to_seq (EnumLvals.in_init vi init) |> - Seq.flat_map (build_lval_deps callstack stmt Data) + let lvals = EnumLvals.in_init vi init in + if lvals <> [] then + List.to_seq lvals |> + Seq.flat_map (build_lval_deps callstack stmt Data) + else + begin match init with + | CompoundInit _ -> Seq.empty (* Do not generate nodes for Compounds for now *) + | SingleInit exp -> + let kinstr = Kstmt stmt in + let dst = build_const context callstack exp in + Seq.return (Graph.create_dependency graph kinstr dst Data node) + end | Asm _ | Skip _ | Code_annot _ -> Seq.empty (* Cases not returned by Studia *) and build_arg_deps callstack : deps_builder * stmt list = diff --git a/src/plugins/dive/tests/dive/oracle/callstack_global.dot b/src/plugins/dive/tests/dive/oracle/callstack_global.dot index 7de57293c7e..d2245d10a58 100644 --- a/src/plugins/dive/tests/dive/oracle/callstack_global.dot +++ b/src/plugins/dive/tests/dive/oracle/callstack_global.dot @@ -17,8 +17,10 @@ digraph G { style="filled", ]; cp19 [label=<x1>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; + cp21 [label=<39>, shape=ellipse, ]; + cp23 [label=<3>, shape=ellipse, ]; - subgraph cluster_cs_1 { label=<main>; cp19;cp17;cp5;cp3;cp2; + subgraph cluster_cs_1 { label=<main>; cp23;cp21;cp19;cp17;cp5;cp3;cp2; subgraph cluster_cs_2 { label=<f>; cp7; }; subgraph cluster_cs_3 { label=<f>; cp9; @@ -39,5 +41,7 @@ digraph G { cp15 -> cp11; cp17 -> cp15; cp19 -> cp15; + cp21 -> cp17; + cp23 -> cp19; } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot index 844c7191d6d..d00972c3173 100644 --- a/src/plugins/dive/tests/dive/oracle/manydeps.dot +++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot @@ -11,15 +11,20 @@ digraph G { style="filled", ]; cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - cp14 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF", + cp14 [label=<0>, shape=ellipse, ]; + cp16 [label=<0>, shape=ellipse, ]; + cp18 [label=<0>, shape=ellipse, ]; + cp20 [label=<0>, shape=ellipse, ]; + cp22 [label=<0>, shape=ellipse, ]; + cp24 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled,bold", ]; - cp15 [label=<0>, shape=ellipse, ]; - cp17 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF", + cp25 [label=<0>, shape=ellipse, ]; + cp27 [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_1 { label=<many_writes>; cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;cp2; }; - subgraph cluster_cs_2 { label=<many_values>; cp17;cp15;cp14; + subgraph cluster_cs_2 { label=<many_values>; cp27;cp25;cp24; }; cp2 -> cp2 [style="bold", ]; @@ -28,7 +33,12 @@ digraph G { cp8 -> cp2; cp10 -> cp2; cp12 -> cp2; - cp15 -> cp14 [style="bold", ]; - cp17 -> cp14; + cp14 -> cp4; + cp16 -> cp6; + cp18 -> cp8; + cp20 -> cp10; + cp22 -> cp12; + cp25 -> cp24 [style="bold", ]; + cp27 -> cp24; } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot index 243f81deb0c..b7876f50b92 100644 --- a/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot +++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot @@ -1,20 +1,22 @@ digraph G { cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled,bold", ]; - cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", + cp3 [label=<0.0f>, shape=ellipse, ]; + cp5 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - cp6 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", + cp8 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - subgraph cluster_cs_1 { label=<main>; cp2; - subgraph cluster_cs_4 { label=<f2>; cp6; + subgraph cluster_cs_1 { label=<main>; cp3;cp2; + subgraph cluster_cs_4 { label=<f2>; cp8; }; }; cp2 -> cp2; - cp2 -> cp3; - cp2 -> cp6; + cp2 -> cp5; + cp2 -> cp8; cp3 -> cp2; - cp6 -> cp2; + cp5 -> cp2; + cp8 -> cp2; } \ 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 4c9ebfa3ebd..6c5989ea7f6 100644 --- a/src/plugins/dive/tests/dive/oracle/ranges.dot +++ b/src/plugins/dive/tests/dive/oracle/ranges.dot @@ -37,36 +37,38 @@ 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, ]; + cp39 [label=<2>, shape=ellipse, ]; + cp41 [label=<0>, shape=ellipse, ]; + cp43 [label=<3>, shape=ellipse, ]; + cp45 [label=<0>, shape=ellipse, ]; + cp47 [label=<12>, shape=ellipse, ]; + cp49 [label=<0>, shape=ellipse, ]; + cp51 [label=<127>, shape=ellipse, ]; + cp53 [label=<0>, shape=ellipse, ]; + cp55 [label=<42000>, shape=ellipse, ]; + cp57 [label=<0>, shape=ellipse, ]; + cp59 [label=<1350000>, shape=ellipse, ]; + cp61 [label=<0>, shape=ellipse, ]; + cp63 [label=<910000000>, shape=ellipse, ]; + cp65 [label=<0>, shape=ellipse, ]; + cp67 [label=<2000000000>, shape=ellipse, ]; + cp69 [label=<(float)0.>, shape=ellipse, ]; cp71 [label=<0.f>, shape=ellipse, ]; - cp73 [label=<3.14f>, shape=ellipse, ]; + cp73 [label=<0.001f>, shape=ellipse, ]; cp75 [label=<0.f>, shape=ellipse, ]; - cp77 [label=<1020.f>, shape=ellipse, ]; + cp77 [label=<3.14f>, shape=ellipse, ]; cp79 [label=<0.f>, shape=ellipse, ]; - cp81 [label=<1e7f>, shape=ellipse, ]; + cp81 [label=<1020.f>, shape=ellipse, ]; cp83 [label=<0.f>, shape=ellipse, ]; - cp85 [label=<1e20f>, shape=ellipse, ]; + cp85 [label=<1e7f>, shape=ellipse, ]; cp87 [label=<0.f>, shape=ellipse, ]; - cp89 [label=<1e36f>, shape=ellipse, ]; + cp89 [label=<1e20f>, shape=ellipse, ]; cp91 [label=<0.f>, shape=ellipse, ]; - cp93 [label=<1e37f>, shape=ellipse, ]; + cp93 [label=<1e36f>, shape=ellipse, ]; + cp95 [label=<0.f>, shape=ellipse, ]; + cp97 [label=<1e37f>, shape=ellipse, ]; - 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; + subgraph cluster_cs_1 { label=<main>; cp97;cp95;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; @@ -87,33 +89,35 @@ digraph G { cp33 -> cp5; cp35 -> cp5; cp37 -> cp5; - cp39 -> cp9; + cp39 -> cp7; cp41 -> cp9; - cp43 -> cp11; + cp43 -> cp9; cp45 -> cp11; - cp47 -> cp13; + cp47 -> cp11; cp49 -> cp13; - cp51 -> cp15; + cp51 -> cp13; cp53 -> cp15; - cp55 -> cp17; + cp55 -> cp15; cp57 -> cp17; - cp59 -> cp19; + cp59 -> cp17; cp61 -> cp19; - cp63 -> cp21; + cp63 -> cp19; 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; + cp67 -> cp21; + cp69 -> cp23; + cp71 -> cp25; + cp73 -> cp25; + cp75 -> cp27; + cp77 -> cp27; + cp79 -> cp29; + cp81 -> cp29; + cp83 -> cp31; + cp85 -> cp31; + cp87 -> cp33; + cp89 -> cp33; + cp91 -> cp35; + cp93 -> cp35; + cp95 -> cp37; + cp97 -> cp37; } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot index 6e3b9370076..f18754cae5a 100644 --- a/src/plugins/dive/tests/dive/oracle/various.dot +++ b/src/plugins/dive/tests/dive/oracle/various.dot @@ -23,21 +23,22 @@ digraph G { style="filled", ]; cp25 [label=<x2>, shape=box, fillcolor="#EEFFEE", color="#004400", style="filled", ]; - cp29 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + cp28 [label=<& f>, shape=ellipse, ]; + cp31 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000", style="filled", ]; - cp32 [label=<is_nan_or_infinite: \is_finite((float)\mul_double((double)y, (double)2.0))>, + cp34 [label=<is_nan_or_infinite: \is_finite((float)\mul_double((double)y, (double)2.0))>, fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon, style="filled,bold,bold", ]; - cp34 [label=<is_nan_or_infinite: \is_finite(\add_float(y, w))>, + cp36 [label=<is_nan_or_infinite: \is_finite(\add_float(y, w))>, fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon, style="filled,bold,bold", ]; - subgraph cluster_cs_1 { label=<f>; cp32;cp5;cp2; + subgraph cluster_cs_1 { label=<f>; cp34;cp5;cp2; }; - subgraph cluster_cs_2 { label=<main>; cp34;cp23;cp18;cp14;cp12;cp11;cp3; + subgraph cluster_cs_2 { label=<main>; cp36;cp28;cp23;cp18;cp14;cp12;cp11;cp3; subgraph cluster_cs_3 { label=<f>; cp21;cp16; }; - subgraph cluster_cs_4 { label=<f>; cp29;cp25; + subgraph cluster_cs_4 { label=<f>; cp31;cp25; }; }; subgraph cluster_file_1 { label=<various.i>; cp8; @@ -49,19 +50,20 @@ digraph G { cp3 -> cp16; cp3 -> cp25; cp5 -> cp2; - cp5 -> cp32; + cp5 -> cp34; cp8 -> cp3; cp12 -> cp11; - cp12 -> cp34; + cp12 -> cp36; cp14 -> cp11; - cp14 -> cp34; + cp14 -> cp36; cp16 -> cp12; cp16 -> cp21; cp18 -> cp14; cp21 -> cp16; cp23 -> cp18 [color="#00FF00", ]; cp25 -> cp18; - cp25 -> cp29; - cp29 -> cp25; + cp25 -> cp31; + cp28 -> cp23; + cp31 -> cp25; } \ No newline at end of file -- GitLab