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/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..ba3ca2eb1f5 --- /dev/null +++ b/regression/goto-analyzer/dependence-graph4/test.desc @@ -0,0 +1,22 @@ +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 +-- +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; diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index dd9a770d837..95ae2de10ae 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,27 @@ 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(); - - depst::iterator it=control_deps.begin(); - for(const auto &c_dep : src.control_deps) + // 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()) { - while(it!=control_deps.end() && *itis_goto() || - from->is_assume()) - control_deps.insert(from); + // 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= @@ -114,11 +118,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); + } } } @@ -208,18 +215,18 @@ void dep_graph_domaint::transform( dynamic_cast(&(dep_graph->get_state(next))); assert(s!=nullptr); - depst::iterator it=s->control_deps.begin(); - for(const auto &c_dep : control_deps) + if(s->is_bottom()) { - 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; + 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(); } } else diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 30b97108776..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,9 +178,22 @@ class dep_graph_domaint:public ai_domain_baset private: tvt has_values; node_indext node_id; + bool has_changed; 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 &); 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