From b49354de6cd54e806c75c2b6d3d2c3fc2db506c8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 5 Mar 2019 06:52:53 +0000 Subject: [PATCH 1/3] Make set_l0_indices return a renamedt This makes explicit that the result is a renamed expression and can be propagated in through other functions. --- src/goto-symex/goto_symex_state.cpp | 11 ++++------- src/goto-symex/goto_symex_state.h | 2 +- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b4971b14e10..fffe6d46dfe 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -235,13 +235,10 @@ void goto_symex_statet::assignment( #endif } -void goto_symex_statet::set_l0_indices( - ssa_exprt &ssa_expr, - const namespacet &ns) +renamedt +goto_symex_statet::set_l0_indices(ssa_exprt ssa_expr, const namespacet &ns) { - renamedt renamed = - level0(std::move(ssa_expr), ns, source.thread_nr); - ssa_expr = renamed.get(); + return level0(std::move(ssa_expr), ns, source.thread_nr); } void goto_symex_statet::set_l1_indices( @@ -275,7 +272,7 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns) level == L0 || level == L1, "rename_ssa can only be used for levels L0 and L1"); if(level == L0) - set_l0_indices(ssa, ns); + ssa = set_l0_indices(std::move(ssa), ns).get(); else if(level == L1) set_l1_indices(ssa, ns); else diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index cf73640bba7..c5065b87848 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -114,7 +114,7 @@ class goto_symex_statet final : public goto_statet void rename_address(exprt &expr, const namespacet &ns); /// Update level 0 values. - void set_l0_indices(ssa_exprt &expr, const namespacet &ns); + renamedt set_l0_indices(ssa_exprt expr, const namespacet &ns); /// Update level 0 and 1 values. void set_l1_indices(ssa_exprt &expr, const namespacet &ns); From 22653052617aaa383059e3d0fa72a04ad76f064f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 5 Mar 2019 11:11:30 +0000 Subject: [PATCH 2/3] Make set_l1_indices return a renamedt This carries the information about which renaming the expression has been through. This requires a change in symex_level1t::operator() so that it takes care of the non-empty level 2 case. --- src/goto-symex/goto_symex_state.cpp | 19 ++++++------------- src/goto-symex/goto_symex_state.h | 2 +- src/goto-symex/renaming_level.cpp | 6 +++++- 3 files changed, 12 insertions(+), 15 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index fffe6d46dfe..424cfbbde58 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -241,17 +241,10 @@ goto_symex_statet::set_l0_indices(ssa_exprt ssa_expr, const namespacet &ns) return level0(std::move(ssa_expr), ns, source.thread_nr); } -void goto_symex_statet::set_l1_indices( - ssa_exprt &ssa_expr, - const namespacet &ns) +renamedt +goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns) { - if(!ssa_expr.get_level_2().empty()) - return; - if(!ssa_expr.get_level_1().empty()) - return; - renamedt l1 = - level1(level0(std::move(ssa_expr), ns, source.thread_nr)); - ssa_expr = l1.get(); + return level1(level0(std::move(ssa_expr), ns, source.thread_nr)); } void goto_symex_statet::set_l2_indices( @@ -274,7 +267,7 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns) if(level == L0) ssa = set_l0_indices(std::move(ssa), ns).get(); else if(level == L1) - set_l1_indices(ssa, ns); + ssa = set_l1_indices(std::move(ssa), ns).get(); else UNREACHABLE; @@ -309,7 +302,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns) } else if(level==L2) { - set_l1_indices(ssa, ns); + ssa = set_l1_indices(std::move(ssa), ns).get(); rename(expr.type(), ssa.get_identifier(), ns); ssa.update_type(); @@ -560,7 +553,7 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns) ssa_exprt &ssa=to_ssa_expr(expr); // only do L1! - set_l1_indices(ssa, ns); + ssa = set_l1_indices(std::move(ssa), ns).get(); rename(expr.type(), ssa.get_identifier(), ns); ssa.update_type(); diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index c5065b87848..5fc04dbd40b 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -117,7 +117,7 @@ class goto_symex_statet final : public goto_statet renamedt set_l0_indices(ssa_exprt expr, const namespacet &ns); /// Update level 0 and 1 values. - void set_l1_indices(ssa_exprt &expr, const namespacet &ns); + renamedt set_l1_indices(ssa_exprt expr, const namespacet &ns); /// Update level 0, 1 and 2 values. void set_l2_indices(ssa_exprt &expr, const namespacet &ns); diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 370bc1018af..c2768f943f7 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -46,8 +46,12 @@ operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const renamedt symex_level1t:: operator()(renamedt l0_expr) const { - if(!l0_expr.get().get_level_1().empty()) + if( + !l0_expr.get().get_level_1().empty() || + !l0_expr.get().get_level_2().empty()) + { return renamedt{std::move(l0_expr.value)}; + } const irep_idt l0_name = l0_expr.get().get_l1_object_identifier(); From 1bb05b68eb8d3dbc159d01e5f67edadab2c49a98 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 5 Mar 2019 13:08:55 +0000 Subject: [PATCH 3/3] Make set_l2_indices return a renamedt This captures the information of which renaming the expression has been through. This requires making symex_level2t::operator() handle non-empty L2. This was handled by set_l2_indices, but it is neccessary to handle it in symex_level2t for making set_l2_indices return a renamedt. --- src/goto-symex/goto_symex_state.cpp | 38 +++++++++++------------------ src/goto-symex/goto_symex_state.h | 2 +- src/goto-symex/renaming_level.cpp | 2 ++ 3 files changed, 17 insertions(+), 25 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 424cfbbde58..e64dc11c6d7 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -188,7 +188,7 @@ void goto_symex_statet::assignment( const auto level2_it = level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first; symex_renaming_levelt::increase_counter(level2_it); - set_l2_indices(lhs, ns); + lhs = set_l2_indices(std::move(lhs), ns).get(); // in case we happen to be multi-threaded, record the memory access bool is_shared=l2_thread_write_encoding(lhs, ns); @@ -247,15 +247,10 @@ goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns) return level1(level0(std::move(ssa_expr), ns, source.thread_nr)); } -void goto_symex_statet::set_l2_indices( - ssa_exprt &ssa_expr, - const namespacet &ns) +renamedt +goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns) { - if(!ssa_expr.get_level_2().empty()) - return; - renamedt l2 = - level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr))); - ssa_expr = l2.get(); + return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr))); } template @@ -323,7 +318,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns) if(p_it != propagation.end()) expr=p_it->second; // already L2 else - set_l2_indices(ssa, ns); + ssa = set_l2_indices(std::move(ssa), ns).get(); } } } @@ -437,8 +432,7 @@ bool goto_symex_statet::l2_thread_read_encoding( if(!no_write.op().is_false()) cond |= guardt{no_write.op()}; - if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1); - set_l2_indices(to_ssa_expr(tmp.true_case()), ns); + const renamedt l2_true_case = set_l2_indices(ssa_l1, ns); if(a_s_read.second.empty()) { @@ -448,14 +442,13 @@ bool goto_symex_statet::l2_thread_read_encoding( symex_renaming_levelt::increase_counter(level2_it); a_s_read.first=level2.current_count(l1_identifier); } + const renamedt l2_false_case = set_l2_indices(ssa_l1, ns); - to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first); - + exprt tmp; if(cond.is_false()) - { - exprt t=tmp.false_case(); - t.swap(tmp); - } + tmp = l2_false_case.get(); + else + tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()}; const bool record_events_bak=record_events; record_events=false; @@ -471,8 +464,7 @@ bool goto_symex_statet::l2_thread_read_encoding( source, symex_targett::assignment_typet::PHI); - set_l2_indices(ssa_l1, ns); - expr=ssa_l1; + expr = set_l2_indices(std::move(ssa_l1), ns).get(); a_s_read.second.push_back(guard); if(!no_write.op().is_false()) @@ -488,15 +480,13 @@ bool goto_symex_statet::l2_thread_read_encoding( // No event and no fresh index, but avoid constant propagation if(!record_events) { - set_l2_indices(ssa_l1, ns); - expr=ssa_l1; + expr = set_l2_indices(std::move(ssa_l1), ns).get(); return true; } // produce a fresh L2 name symex_renaming_levelt::increase_counter(level2_it); - set_l2_indices(ssa_l1, ns); - expr=ssa_l1; + expr = set_l2_indices(std::move(ssa_l1), ns).get(); // and record that INVARIANT_STRUCTURED( diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 5fc04dbd40b..3b6bf032252 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -120,7 +120,7 @@ class goto_symex_statet final : public goto_statet renamedt set_l1_indices(ssa_exprt expr, const namespacet &ns); /// Update level 0, 1 and 2 values. - void set_l2_indices(ssa_exprt &expr, const namespacet &ns); + renamedt set_l2_indices(ssa_exprt expr, const namespacet &ns); // this maps L1 names to (L2) types typedef std::unordered_map l1_typest; diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index c2768f943f7..ced74b85a52 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -67,6 +67,8 @@ operator()(renamedt l0_expr) const renamedt symex_level2t:: operator()(renamedt l1_expr) const { + if(!l1_expr.get().get_level_2().empty()) + return renamedt{std::move(l1_expr.value)}; l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier())); return renamedt{std::move(l1_expr.value)}; }