From 7c9c51393d117c0004f144e5c1a453dd147b17ab Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 19 Nov 2015 14:33:59 +0000 Subject: [PATCH 1/2] Maintain ID_C_expr_simplified --- src/goto-symex/goto_symex.h | 4 +-- src/goto-symex/goto_symex_state.cpp | 44 +++++++++++++++++--------- src/goto-symex/goto_symex_state.h | 4 +-- src/goto-symex/symex_dereference.cpp | 47 +++++++++++++++++++--------- src/util/irep_ids.def | 1 + src/util/replace_expr.cpp | 6 ++++ src/util/replace_symbol.cpp | 6 ++++ 7 files changed, 80 insertions(+), 32 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index f45d722ebf7..a00828f6e51 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -131,13 +131,13 @@ class goto_symext statet &state, const bool write); - void dereference_rec( + bool dereference_rec( exprt &expr, statet &state, guardt &guard, const bool write); - void dereference_rec_address_of( + bool dereference_rec_address_of( exprt &expr, statet &state, guardt &guard); diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index d88e9c68bac..df89504d8a8 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -436,12 +436,13 @@ void goto_symex_statet::set_ssa_indices( } } -void goto_symex_statet::rename( +bool goto_symex_statet::rename( exprt &expr, const namespacet &ns, levelt level) { // rename all the symbols with their last known value + bool result=false; if(expr.id()==ID_symbol && expr.get_bool(ID_C_SSA_symbol)) @@ -476,7 +477,10 @@ void goto_symex_statet::rename( propagation.values.find(ssa.get_identifier()); if(p_it!=propagation.values.end()) + { expr=p_it->second; // already L2 + result=true; + } else set_ssa_indices(ssa, ns, L2); } @@ -493,16 +497,16 @@ void goto_symex_statet::rename( ns, level); - return; + return false; } expr=ssa_exprt(expr); - rename(expr, ns, level); + result=rename(expr, ns, level); } else if(expr.id()==ID_address_of) { assert(expr.operands().size()==1); - rename_address(expr.op0(), ns, level); + result=rename_address(expr.op0(), ns, level); assert(expr.type().id()==ID_pointer); expr.type().subtype()=expr.op0().type(); } @@ -513,7 +517,7 @@ void goto_symex_statet::rename( // do this recursively Forall_operands(it, expr) - rename(*it, ns, level); + result=rename(*it, ns, level) || result; // some fixes if(expr.id()==ID_with) @@ -525,6 +529,11 @@ void goto_symex_statet::rename( expr.type()=to_if_expr(expr).true_case().type(); } } + + if(result) + expr.remove(ID_C_expr_simplified); + + return result; } /// thread encoding @@ -709,11 +718,13 @@ bool goto_symex_statet::l2_thread_write_encoding( return threads.size()>1; } -void goto_symex_statet::rename_address( +bool goto_symex_statet::rename_address( exprt &expr, const namespacet &ns, levelt level) { + bool result=false; + if(expr.id()==ID_symbol && expr.get_bool(ID_C_SSA_symbol)) { @@ -728,7 +739,7 @@ void goto_symex_statet::rename_address( else if(expr.id()==ID_symbol) { expr=ssa_exprt(expr); - rename_address(expr, ns, level); + result=rename_address(expr, ns, level); } else { @@ -736,20 +747,20 @@ void goto_symex_statet::rename_address( { index_exprt &index_expr=to_index_expr(expr); - rename_address(index_expr.array(), ns, level); + result=rename_address(index_expr.array(), ns, level); assert(index_expr.array().type().id()==ID_array); expr.type()=index_expr.array().type().subtype(); // the index is not an address - rename(index_expr.index(), ns, level); + result=rename(index_expr.index(), ns, level) || result; } else if(expr.id()==ID_if) { // the condition is not an address if_exprt &if_expr=to_if_expr(expr); - rename(if_expr.cond(), ns, level); - rename_address(if_expr.true_case(), ns, level); - rename_address(if_expr.false_case(), ns, level); + result=rename(if_expr.cond(), ns, level); + result=rename_address(if_expr.true_case(), ns, level) || result; + result=rename_address(if_expr.false_case(), ns, level) || result; if_expr.type()=if_expr.true_case().type(); } @@ -757,7 +768,7 @@ void goto_symex_statet::rename_address( { member_exprt &member_expr=to_member_expr(expr); - rename_address(member_expr.struct_op(), ns, level); + result=rename_address(member_expr.struct_op(), ns, level); // type might not have been renamed in case of nesting of // structs and pointers/arrays @@ -781,9 +792,14 @@ void goto_symex_statet::rename_address( // do this recursively; we assume here // that all the operands are addresses Forall_operands(it, expr) - rename_address(*it, ns, level); + result=rename_address(*it, ns, level) || result; } } + + if(result) + expr.remove(ID_C_expr_simplified); + + return result; } void goto_symex_statet::rename( diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index d62d4a66af9..cfbfa2bac15 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -148,7 +148,7 @@ class goto_symex_statet enum levelt { L0=0, L1=1, L2=2 }; // performs renaming _up to_ the given level - void rename(exprt &expr, const namespacet &ns, levelt level=L2); + bool rename(exprt &expr, const namespacet &ns, levelt level=L2); void rename( typet &type, const irep_idt &l1_identifier, @@ -170,7 +170,7 @@ class goto_symex_statet void get_original_name(exprt &expr) const; void get_original_name(typet &type) const; protected: - void rename_address(exprt &expr, const namespacet &ns, levelt level); + bool rename_address(exprt &expr, const namespacet &ns, levelt level); void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2); // only required for value_set.assign diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 6b28ec35adf..d26a24f0f99 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -23,44 +23,48 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" #include "symex_dereference_state.h" -void goto_symext::dereference_rec_address_of( +bool goto_symext::dereference_rec_address_of( exprt &expr, statet &state, guardt &guard) { + bool result=false; + // Could be member, could be if, could be index. if(expr.id()==ID_member) - dereference_rec_address_of( + result=dereference_rec_address_of( to_member_expr(expr).struct_op(), state, guard); else if(expr.id()==ID_if) { // the condition is not an address - dereference_rec( + result=dereference_rec( to_if_expr(expr).cond(), state, guard, false); // add to guard? - dereference_rec_address_of( - to_if_expr(expr).true_case(), state, guard); - dereference_rec_address_of( - to_if_expr(expr).false_case(), state, guard); + result=dereference_rec_address_of( + to_if_expr(expr).true_case(), state, guard) || result; + result=dereference_rec_address_of( + to_if_expr(expr).false_case(), state, guard) || result; } else if(expr.id()==ID_index) { // the index is not an address - dereference_rec( + result=dereference_rec( to_index_expr(expr).index(), state, guard, false); // the array _is_ an address - dereference_rec_address_of( - to_index_expr(expr).array(), state, guard); + result=dereference_rec_address_of( + to_index_expr(expr).array(), state, guard) || result; } else { // give up and dereference - dereference_rec(expr, state, guard, false); + result=dereference_rec(expr, state, guard, false); } + + return result; } bool goto_symext::is_index_member_symbol_if(const exprt &expr) @@ -226,12 +230,14 @@ exprt goto_symext::address_arithmetic( return result; } -void goto_symext::dereference_rec( +bool goto_symext::dereference_rec( exprt &expr, statet &state, guardt &guard, const bool write) { + bool result=false; + if(expr.id()==ID_dereference) { if(expr.operands().size()!=1) @@ -267,6 +273,8 @@ void goto_symext::dereference_rec( // this may yield a new auto-object trigger_auto_object(expr, state); + + result=true; } else if(expr.id()==ID_index && to_index_expr(expr).array().id()==ID_member && @@ -291,6 +299,8 @@ void goto_symext::dereference_rec( dereference_rec(tmp, state, guard, write); expr.swap(tmp); + + result=true; } else if(expr.id()==ID_index && to_index_expr(expr).array().type().id()==ID_pointer) @@ -307,6 +317,8 @@ void goto_symext::dereference_rec( const typet &expr_type=ns.follow(expr.type()); expr=address_arithmetic(object, state, guard, expr_type.subtype().id()==ID_array); + + result=true; } else if(expr.id()==ID_typecast) { @@ -327,17 +339,24 @@ void goto_symext::dereference_rec( from_integer(0, index_type()))); dereference_rec(expr, state, guard, write); + + result=true; } else { - dereference_rec(tc_op, state, guard, write); + result=dereference_rec(tc_op, state, guard, write) || result; } } else { Forall_operands(it, expr) - dereference_rec(*it, state, guard, write); + result=dereference_rec(*it, state, guard, write) || result; } + + if(result) + expr.remove(ID_C_expr_simplified); + + return result; } void goto_symext::dereference( diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e31eceb1e98..513cecc1c4b 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -810,6 +810,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func) IREP_ID_ONE(cprover_string_trim_func) IREP_ID_ONE(cprover_string_value_of_func) IREP_ID_ONE(array_replace) +IREP_ID_TWO(C_expr_simplified, #expr_simplified) #undef IREP_ID_ONE #undef IREP_ID_TWO diff --git a/src/util/replace_expr.cpp b/src/util/replace_expr.cpp index 9655359796a..0187072418a 100644 --- a/src/util/replace_expr.cpp +++ b/src/util/replace_expr.cpp @@ -22,6 +22,9 @@ bool replace_expr(const exprt &what, const exprt &by, exprt &dest) Forall_operands(it, dest) result=replace_expr(what, by, *it) && result; + if(!result) + dest.remove(ID_C_expr_simplified); + return result; } @@ -42,5 +45,8 @@ bool replace_expr(const replace_mapt &what, exprt &dest) Forall_operands(it, dest) result=replace_expr(what, *it) && result; + if(!result) + dest.remove(ID_C_expr_simplified); + return result; } diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 51d4a140493..607737baa1d 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -70,6 +70,9 @@ bool replace_symbolt::replace(exprt &dest) const !replace(static_cast(dest.add(ID_C_va_arg_type)))) result=false; + if(!result) + dest.remove(ID_C_expr_simplified); + return result; } @@ -162,6 +165,9 @@ bool replace_symbolt::replace(typet &dest) const result=false; } + if(!result) + dest.remove(ID_C_expr_simplified); + return result; } From 88e52cfec3649cfdf536c8a284c9ea41bae84d57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Jan 2016 21:56:07 +0100 Subject: [PATCH 2/2] Use ID_C_expr_simplified --- src/util/simplify_expr.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index d8d62fee483..73305ac39bd 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2334,20 +2334,22 @@ bool simplify_exprt::simplify_rec(exprt &expr) exprt tmp=expr; bool result=true; + if(!tmp.get_bool(ID_C_expr_simplified)) + { result=simplify_node_preorder(tmp); if(!simplify_node(tmp)) result=false; - #if 1 replace_mapt::const_iterator it=local_replace_map.find(tmp); if(it!=local_replace_map.end()) { tmp=it->second; result=false; } - #else - if(!local_replace_map.empty() && + } + #if 0 + else if(!local_replace_map.empty() && !replace_expr(local_replace_map, tmp)) { simplify_rec(tmp); @@ -2357,6 +2359,7 @@ bool simplify_exprt::simplify_rec(exprt &expr) if(!result) { + tmp.set(ID_C_expr_simplified, true); expr.swap(tmp); #ifdef USE_CACHE