From a4084234e5cb9e883b2dacad13c897afbc89b14d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 23 Feb 2018 11:28:49 +0000 Subject: [PATCH 1/4] Simplified state merging in the dependence graph --- src/analyses/dependence_graph.cpp | 45 +++++------------------- src/util/container_utils.h | 57 +++++++++++++++++++++++++++++++ 2 files changed, 65 insertions(+), 37 deletions(-) create mode 100644 src/util/container_utils.h diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index dd9a770d837..eedd17a7fc3 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -16,6 +16,7 @@ Date: August 2013 #include +#include #include #include @@ -26,36 +27,16 @@ bool dep_graph_domaint::merge( goto_programt::const_targett from, goto_programt::const_targett to) { - bool changed=has_values.is_false(); - has_values=tvt::unknown(); + bool changed = false; - depst::iterator it=control_deps.begin(); - for(const auto &c_dep : src.control_deps) + if(is_bottom()) { - while(it!=control_deps.end() && *it(&(dep_graph->get_state(next))); assert(s!=nullptr); - depst::iterator it=s->control_deps.begin(); - for(const auto &c_dep : control_deps) - { - while(it!=s->control_deps.end() && *itcontrol_deps.end() || c_dep<*it) - s->control_deps.insert(it, c_dep); - else if(it!=s->control_deps.end()) - ++it; - } - + util_inplace_set_union(s->control_deps, control_deps); control_deps.clear(); } } diff --git a/src/util/container_utils.h b/src/util/container_utils.h new file mode 100644 index 00000000000..629896f5730 --- /dev/null +++ b/src/util/container_utils.h @@ -0,0 +1,57 @@ +/*******************************************************************\ + +Module: Container utilities + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_CONTAINER_UTILS_H +#define CPROVER_UTIL_CONTAINER_UTILS_H + +#include + +/// Compute union of two sets +/// +/// This function has complexity O(max(n1, n2)), with n1, n2 being the sizes of +/// the sets of which the union is formed. This is in contrast to +/// `target.insert(source.begin(), source.end())` which has complexity +/// O(n2 * log(n1 + n2)). +/// +/// \tparam T value type of the sets +/// \tparam Compare comparison predicate of the sets +/// \tparam Alloc allocator of the sets +/// \param target first input set, will contain the result of the union +/// \param source second input set +/// \return true iff `target` was changed +template +bool util_inplace_set_union( + std::set &target, + const std::set &source) +{ + bool changed = false; + typename std::set::iterator it = target.begin(); + + for(const auto &s : source) + { + while(it != target.end() && *it < s) + { + ++it; + } + + if(it == target.end() || s < *it) + { + // Insertion hint should point at element that will follow the new element + target.insert(it, s); + changed = true; + } + else if(it != target.end()) + { + ++it; + } + } + + return changed; +} + +#endif // CPROVER_UTIL_CONTAINER_UTILS_H From 3aa6dca7310f1e74405597f5ef0b2cd3ea58e59e Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 23 Feb 2018 12:01:26 +0000 Subject: [PATCH 2/4] Control dependency computation fix Previously in transform() only the control dependencies in the set control_deps (plus gotos and assumes at the from location) were considered candidates for the control dependencies at the to location. With this scheme however one misses control dependencies when there are nested if statements. We introduce a new set control_dep_candidates in addition to control_deps, which contains all control statements encountered so far. --- .../goto-analyzer/dependence-graph4/main.c | 16 +++++ .../goto-analyzer/dependence-graph4/test.desc | 9 +++ src/analyses/dependence_graph.cpp | 70 ++++++++++++------- src/analyses/dependence_graph.h | 14 +++- 4 files changed, 83 insertions(+), 26 deletions(-) create mode 100644 regression/goto-analyzer/dependence-graph4/main.c create mode 100644 regression/goto-analyzer/dependence-graph4/test.desc diff --git a/regression/goto-analyzer/dependence-graph4/main.c b/regression/goto-analyzer/dependence-graph4/main.c new file mode 100644 index 00000000000..cad28241847 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph4/main.c @@ -0,0 +1,16 @@ +int g_in1, g_in2; +int g_out; + +void main(void) +{ + int t; + if(g_in1) + { + if(g_in2) + t = 0; + else + t = 1; + + g_out = 1; // depends on "if(g_in1) + } +} diff --git a/regression/goto-analyzer/dependence-graph4/test.desc b/regression/goto-analyzer/dependence-graph4/test.desc new file mode 100644 index 00000000000..8a29e80131d --- /dev/null +++ b/regression/goto-analyzer/dependence-graph4/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--show --dependence-graph --text - +activate-multi-line-match +EXIT=0 +SIGNAL=0 +\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1 +-- +^warning: ignoring diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index eedd17a7fc3..bd4003dcd45 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -37,6 +37,8 @@ bool dep_graph_domaint::merge( } changed |= util_inplace_set_union(control_deps, src.control_deps); + changed |= + util_inplace_set_union(control_dep_candidates, src.control_dep_candidates); return changed; } @@ -48,42 +50,54 @@ void dep_graph_domaint::control_dependencies( { // Better Slicing of Programs with Jumps and Switches // Kumar and Horwitz, FASE'02: - // Node N is control dependent on node M iff N postdominates one - // but not all of M's CFG successors. + // "Node N is control dependent on node M iff N postdominates, in + // the CFG, one but not all of M's CFG successors." // - // candidates for M are from and all existing control-depended on - // nodes; from is added if it is a goto or assume instruction - if(from->is_goto() || - from->is_assume()) - control_deps.insert(from); + // The "successor" above refers to an immediate successor of M. + // + // When computing the control dependencies of a node N (i.e., "to" + // being N), candidates for M are all control statements (gotos or + // assumes) from which there is a path in the CFG to N. + + // Add new candidates + + if(from->is_goto() || from->is_assume()) + control_dep_candidates.insert(from); + else if(from->is_end_function()) + { + control_dep_candidates.clear(); + return; + } + + if(control_dep_candidates.empty()) + return; + + // Get postdominators const irep_idt id=from->function; const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id); - // check all candidates for M - for(depst::iterator - it=control_deps.begin(); - it!=control_deps.end(); - ) // no ++it - { - depst::iterator next=it; - ++next; + // Check all candidates - // check all CFG successors + for(const auto &control_dep_candidate : control_dep_candidates) + { + // check all CFG successors of M // special case: assumptions also introduce a control dependency - bool post_dom_all=!(*it)->is_assume(); + bool post_dom_all = !control_dep_candidate->is_assume(); bool post_dom_one=false; // we could hard-code assume and goto handling here to improve // performance - cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e= - pd.cfg.entry_map.find(*it); + cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e = + pd.cfg.entry_map.find(control_dep_candidate); - assert(e!=pd.cfg.entry_map.end()); + INVARIANT( + e != pd.cfg.entry_map.end(), "cfg must have an entry for every location"); const cfg_post_dominatorst::cfgt::nodet &m= pd.cfg[e->second]; + // successors of M for(const auto &edge : m.out) { const cfg_post_dominatorst::cfgt::nodet &m_s= @@ -95,11 +109,14 @@ void dep_graph_domaint::control_dependencies( post_dom_all=false; } - if(post_dom_all || - !post_dom_one) - control_deps.erase(it); - - it=next; + if(post_dom_all || !post_dom_one) + { + control_deps.erase(control_dep_candidate); + } + else + { + control_deps.insert(control_dep_candidate); + } } } @@ -190,7 +207,10 @@ void dep_graph_domaint::transform( assert(s!=nullptr); util_inplace_set_union(s->control_deps, control_deps); + util_inplace_set_union(s->control_dep_candidates, control_dep_candidates); + control_deps.clear(); + control_dep_candidates.clear(); } } else diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 30b97108776..694640f8977 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -162,7 +162,19 @@ class dep_graph_domaint:public ai_domain_baset node_indext node_id; typedef std::set depst; - depst control_deps, data_deps; + + // Set of locations with control instructions on which the instruction at this + // location has a control dependency on + depst control_deps; + + // Set of locations with control instructions from which there is a path in + // the CFG to the current location (with the locations being in the same + // function). The set control_deps is a subset of this set. + depst control_dep_candidates; + + // Set of locations with instructions on which the instruction at this + // location has a data dependency on + depst data_deps; friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &); From 66263ea3c6ad424c675bf5885c733b972659bc2b Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 23 Feb 2018 12:31:37 +0000 Subject: [PATCH 3/4] Make dependence graph merge() return true when abstract state changes The dependency graph has special handling for function entry edges (in transform()) where it merges the current state into the state of the return location before entering the function. This may change the abstract state at the return location. When later the function exit edge is handled, the merge() into the return location may not change the state, thus merge() may not return true, and thus the return location may not be inserted into the worklist of the fixpoint computation when it should. We introduce a flag has_changed that records whether the abstract state has changed on the handling of the function entry edge. On the function return edge later, merge() checks the flag to know whether it needs to return true. --- src/analyses/dependence_graph.cpp | 30 ++++++++++++++++++------ src/analyses/dependence_graph.h | 39 +++++++++++++++++++++++-------- 2 files changed, 52 insertions(+), 17 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index bd4003dcd45..95ae2de10ae 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -27,19 +27,28 @@ bool dep_graph_domaint::merge( goto_programt::const_targett from, goto_programt::const_targett to) { - bool changed = false; - - if(is_bottom()) + // An abstract state at location `to` may be non-bottom even if + // `merge(..., `to`) has not been called so far. This is due to the special + // handling of function entry edges (see transform()). + bool changed = is_bottom() || has_changed; + + // For computing the data dependencies, we would not need a fixpoint + // computation. The data dependencies at a location are computed from the + // result of the reaching definitions analysis at that location + // (in data_dependencies()). Thus, we only need to set the data dependencies + // part of an abstract state at a certain location once. + if(changed && data_deps.empty()) { - has_values = tvt::unknown(); data_deps = src.data_deps; - changed = true; + has_values = tvt::unknown(); } changed |= util_inplace_set_union(control_deps, src.control_deps); changed |= util_inplace_set_union(control_dep_candidates, src.control_dep_candidates); + has_changed = false; + return changed; } @@ -206,8 +215,15 @@ void dep_graph_domaint::transform( dynamic_cast(&(dep_graph->get_state(next))); assert(s!=nullptr); - util_inplace_set_union(s->control_deps, control_deps); - util_inplace_set_union(s->control_dep_candidates, control_dep_candidates); + if(s->is_bottom()) + { + s->has_values = tvt::unknown(); + s->has_changed = true; + } + + s->has_changed |= util_inplace_set_union(s->control_deps, control_deps); + s->has_changed |= util_inplace_set_union( + s->control_dep_candidates, control_dep_candidates); control_deps.clear(); control_dep_candidates.clear(); diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 694640f8977..de7ee8c5a20 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -68,9 +68,10 @@ class dep_graph_domaint:public ai_domain_baset public: typedef grapht::node_indext node_indext; - dep_graph_domaint(): - has_values(false), - node_id(std::numeric_limits::max()) + dep_graph_domaint() + : has_values(false), + node_id(std::numeric_limits::max()), + has_changed(false) { } @@ -101,6 +102,7 @@ class dep_graph_domaint:public ai_domain_baset has_values=tvt(true); control_deps.clear(); + control_dep_candidates.clear(); data_deps.clear(); } @@ -111,12 +113,24 @@ class dep_graph_domaint:public ai_domain_baset has_values=tvt(false); control_deps.clear(); + control_dep_candidates.clear(); data_deps.clear(); + + has_changed = false; } void make_entry() final override { - make_top(); + DATA_INVARIANT( + node_id != std::numeric_limits::max(), + "node_id must not be valid"); + + has_values = tvt::unknown(); + control_deps.clear(); + control_dep_candidates.clear(); + data_deps.clear(); + + has_changed = false; } bool is_top() const final override @@ -124,9 +138,11 @@ class dep_graph_domaint:public ai_domain_baset DATA_INVARIANT(node_id!=std::numeric_limits::max(), "node_id must be valid"); - DATA_INVARIANT(!has_values.is_true() || - (control_deps.empty() && data_deps.empty()), - "If the domain is top, it must have no dependencies"); + DATA_INVARIANT( + !has_values.is_true() || + (control_deps.empty() && control_dep_candidates.empty() && + data_deps.empty()), + "If the domain is top, it must have no dependencies"); return has_values.is_true(); } @@ -136,9 +152,11 @@ class dep_graph_domaint:public ai_domain_baset DATA_INVARIANT(node_id!=std::numeric_limits::max(), "node_id must be valid"); - DATA_INVARIANT(!has_values.is_false() || - (control_deps.empty() && data_deps.empty()), - "If the domain is bottom, it must have no dependencies"); + DATA_INVARIANT( + !has_values.is_false() || + (control_deps.empty() && control_dep_candidates.empty() && + data_deps.empty()), + "If the domain is bottom, it must have no dependencies"); return has_values.is_false(); } @@ -160,6 +178,7 @@ class dep_graph_domaint:public ai_domain_baset private: tvt has_values; node_indext node_id; + bool has_changed; typedef std::set depst; From 7002909f8b6bd768b8d981befabb54c92adb1fbb Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 28 Feb 2018 14:58:26 +0000 Subject: [PATCH 4/4] More dependence graph tests --- .../goto-analyzer/dependence-graph10/main.c | 15 ++++++ .../dependence-graph10/test.desc | 39 ++++++++++++++ .../goto-analyzer/dependence-graph11/main.c | 15 ++++++ .../dependence-graph11/test.desc | 23 ++++++++ .../goto-analyzer/dependence-graph12/main.c | 21 ++++++++ .../dependence-graph12/test.desc | 38 +++++++++++++ .../goto-analyzer/dependence-graph4/test.desc | 13 +++++ .../goto-analyzer/dependence-graph7/main.c | 10 ++++ .../goto-analyzer/dependence-graph7/test.desc | 50 +++++++++++++++++ .../goto-analyzer/dependence-graph8/main.c | 13 +++++ .../goto-analyzer/dependence-graph8/test.desc | 54 +++++++++++++++++++ .../goto-analyzer/dependence-graph9/main.c | 16 ++++++ .../goto-analyzer/dependence-graph9/test.desc | 38 +++++++++++++ 13 files changed, 345 insertions(+) create mode 100644 regression/goto-analyzer/dependence-graph10/main.c create mode 100644 regression/goto-analyzer/dependence-graph10/test.desc create mode 100644 regression/goto-analyzer/dependence-graph11/main.c create mode 100644 regression/goto-analyzer/dependence-graph11/test.desc create mode 100644 regression/goto-analyzer/dependence-graph12/main.c create mode 100644 regression/goto-analyzer/dependence-graph12/test.desc create mode 100644 regression/goto-analyzer/dependence-graph7/main.c create mode 100644 regression/goto-analyzer/dependence-graph7/test.desc create mode 100644 regression/goto-analyzer/dependence-graph8/main.c create mode 100644 regression/goto-analyzer/dependence-graph8/test.desc create mode 100644 regression/goto-analyzer/dependence-graph9/main.c create mode 100644 regression/goto-analyzer/dependence-graph9/test.desc diff --git a/regression/goto-analyzer/dependence-graph10/main.c b/regression/goto-analyzer/dependence-graph10/main.c new file mode 100644 index 00000000000..8cdfb5e4158 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph10/main.c @@ -0,0 +1,15 @@ +int a; + +void main(void) +{ + int i = 0; + + if(i < 10) + { + a = 1; + } + else + { + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph10/test.desc b/regression/goto-analyzer/dependence-graph10/test.desc new file mode 100644 index 00000000000..e0d118d2ac3 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph10/test.desc @@ -0,0 +1,39 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// First assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// Second assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 + +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + a = 1; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the assignment has a +control dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 +... +**** 5 file main.c line 13 function main +Control dependencies: + + // 5 file main.c line 13 function main + 1: a = 2; + diff --git a/regression/goto-analyzer/dependence-graph11/main.c b/regression/goto-analyzer/dependence-graph11/main.c new file mode 100644 index 00000000000..c3ab582f676 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph11/main.c @@ -0,0 +1,15 @@ +int a; + +void func() +{ +} + +void main(void) +{ + func(); + + if(a < 10) + { + a = 1; + } +} diff --git a/regression/goto-analyzer/dependence-graph11/test.desc b/regression/goto-analyzer/dependence-graph11/test.desc new file mode 100644 index 00000000000..d8112318ed4 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph11/test.desc @@ -0,0 +1,23 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +-- +^warning: ignoring +-- +The regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 1 +... +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + a = 1; diff --git a/regression/goto-analyzer/dependence-graph12/main.c b/regression/goto-analyzer/dependence-graph12/main.c new file mode 100644 index 00000000000..0257cb1f1c5 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph12/main.c @@ -0,0 +1,21 @@ +int a; + +void func() +{ +} + +void main(void) +{ + if(a < 7) + { + goto L; + } + + if(a < 10) + { + func(); + L: + a = 1; + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph12/test.desc b/regression/goto-analyzer/dependence-graph12/test.desc new file mode 100644 index 00000000000..b14ba9f7ba6 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph12/test.desc @@ -0,0 +1,38 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the first if +\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +// Assignment has a control dependency on the second if +\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 9 function main + IF a < 7 THEN GOTO 1 +... +**** 6 file main.c line 19 function main +Control dependencies: (,...)|(...,) + + // 6 file main.c line 19 function main + a = 2; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the assignment has a +control dependency on the goto statement. + + // file main.c line 14 function main + IF !(a < 10) THEN GOTO 2 +... +**** 6 file main.c line 19 function main +Control dependencies: (,...)|(...,) + + // 6 file main.c line 19 function main + a = 2; diff --git a/regression/goto-analyzer/dependence-graph4/test.desc b/regression/goto-analyzer/dependence-graph4/test.desc index 8a29e80131d..ba3ca2eb1f5 100644 --- a/regression/goto-analyzer/dependence-graph4/test.desc +++ b/regression/goto-analyzer/dependence-graph4/test.desc @@ -7,3 +7,16 @@ SIGNAL=0 \/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1 -- ^warning: ignoring +-- +The regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the goto statement. + + // file main.c line 7 function main + IF !(g_in1 != 0) THEN GOTO 3 +... +**** 3 file main.c line 9 function main +Control dependencies: + + // 3 file main.c line 9 function main + g_out = 1; diff --git a/regression/goto-analyzer/dependence-graph7/main.c b/regression/goto-analyzer/dependence-graph7/main.c new file mode 100644 index 00000000000..e0ab2d5b1a4 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph7/main.c @@ -0,0 +1,10 @@ +int a; + +void main(void) +{ + int i = 0; + while(i < 10) + { + a = 1; + } +} diff --git a/regression/goto-analyzer/dependence-graph7/test.desc b/regression/goto-analyzer/dependence-graph7/test.desc new file mode 100644 index 00000000000..62067ef188a --- /dev/null +++ b/regression/goto-analyzer/dependence-graph7/test.desc @@ -0,0 +1,50 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// Backedge has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}\s*GOTO [0-9]+ +// Loop head has a control dependency on itself +Control dependencies: ([0-9]+)\n(.*\n)?\n.*\/\/ \1.*\n.*IF.*i < 10.*THEN +-- +^warning: ignoring +-- +The first regex above match output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 +... +**** 3 file main.c line 8 function main +Control dependencies: + + // 3 file main.c line 8 function main + a = 1; + +The second regex above match output portions like shown below (with being a +location number). The intention is to check whether the backwards goto has a +control dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 +... +**** 4 file main.c line 6 function main +Control dependencies: + + // 4 file main.c line 6 function main + GOTO 1 + +The third regex above match output portions like shown below (with being a +location number). The intention is to check whether the loop head has a control +dependency on itself. + +Control dependencies: +Data dependencies: 1 + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 2 diff --git a/regression/goto-analyzer/dependence-graph8/main.c b/regression/goto-analyzer/dependence-graph8/main.c new file mode 100644 index 00000000000..ca7bf52632f --- /dev/null +++ b/regression/goto-analyzer/dependence-graph8/main.c @@ -0,0 +1,13 @@ +int a; + +void main(void) +{ + int i = 0; + while(i < 10) + { + if(i < 7) + { + a = 1; + } + } +} diff --git a/regression/goto-analyzer/dependence-graph8/test.desc b/regression/goto-analyzer/dependence-graph8/test.desc new file mode 100644 index 00000000000..50549bb686f --- /dev/null +++ b/regression/goto-analyzer/dependence-graph8/test.desc @@ -0,0 +1,54 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Assignment has a control dependency on the if +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +// If has a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*i < 7 +-- +^warning: ignoring +// Assignment does not have a control dependency on the loop head +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the if. + + // file main.c line 6 function main + 1: IF !(i < 7) THEN GOTO 2 +... +**** 3 file main.c line 8 function main +Control dependencies: + + // 3 file main.c line 8 function main + a = 1; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check whether the if has a control +dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 3 + +**** 3 file main.c line 8 function main +Control dependencies: +Data dependencies: 1 + + // 3 file main.c line 8 function main + IF !(i < 7) THEN GOTO 2 + +The third regex above matches output portions like shown below (with being a +location number). The intention is to check that the assignment does not have a +control dependency on the loop head. + + // file main.c line 6 function main + 1: IF !(i < 10) THEN GOTO 3 +... +**** 4 file main.c line 10 function main +Control dependencies: + + // 4 file main.c line 10 function main + a = 1; diff --git a/regression/goto-analyzer/dependence-graph9/main.c b/regression/goto-analyzer/dependence-graph9/main.c new file mode 100644 index 00000000000..d968c9f55e1 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph9/main.c @@ -0,0 +1,16 @@ +int a; + +void main(void) +{ + int i = 0; + + if(i < 10) + { + if(i < 7) + { + a = 1; + } + + a = 2; + } +} diff --git a/regression/goto-analyzer/dependence-graph9/test.desc b/regression/goto-analyzer/dependence-graph9/test.desc new file mode 100644 index 00000000000..2bcae4642df --- /dev/null +++ b/regression/goto-analyzer/dependence-graph9/test.desc @@ -0,0 +1,38 @@ +CORE +main.c +--dependence-graph --show +activate-multi-line-match +EXIT=0 +SIGNAL=0 +// Second assignment has a control dependency on the outer if +\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +^warning: ignoring +// Second assignment does not have a control dependency on the inner if +\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 +-- +The first regex above matches output portions like shown below (with being a +location number). The intention is to check whether the assignment has a control +dependency on the outer if. + + // file main.c line 7 function main + IF !(i < 10) THEN GOTO 2 +... +**** 6 file main.c line 14 function main +Control dependencies: + + // 6 file main.c line 14 function main + a = 2; + +The second regex above matches output portions like shown below (with being +a location number). The intention is to check that the assignment does not have +a control dependency on the inner if. + + // file main.c line 9 function main + IF !(i < 7) THEN GOTO 1 +... +**** 6 file main.c line 14 function main +Control dependencies: + + // 6 file main.c line 14 function main + a = 2;