From 69d4c5da041c656dbdd23809dffc0a2b0d070de9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 30 Jan 2019 11:26:58 +0000 Subject: [PATCH 1/4] Mark symex_level0 and level1 operator() const Make obvious the operator doesn't change the state of the object. --- src/goto-symex/renaming_level.cpp | 4 ++-- src/goto-symex/renaming_level.h | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 3cc68081a17..849886cd7a0 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -18,7 +18,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "goto_symex_state.h" void symex_level0t:: -operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) +operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) const { // already renamed? if(!ssa_expr.get_level_0().empty()) @@ -42,7 +42,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) ssa_expr.set_level_0(thread_nr); } -void symex_level1t::operator()(ssa_exprt &ssa_expr) +void symex_level1t::operator()(ssa_exprt &ssa_expr) const { // already renamed? if(!ssa_expr.get_level_1().empty()) diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index a1406d7138f..b520de10dce 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -56,8 +56,8 @@ struct symex_renaming_levelt /// The renaming is built for one particular interleaving. struct symex_level0t : public symex_renaming_levelt { - void - operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr); + void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) + const; symex_level0t() = default; ~symex_level0t() override = default; @@ -68,7 +68,7 @@ struct symex_level0t : public symex_renaming_levelt /// This is to preserve locality in case of recursion struct symex_level1t : public symex_renaming_levelt { - void operator()(ssa_exprt &ssa_expr); + void operator()(ssa_exprt &ssa_expr) const; /// Insert the content of \p other into this renaming void restore_from(const current_namest &other); From eebe60576647a30244ba487402a805645e67d145 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 22 Jan 2019 19:48:11 +0000 Subject: [PATCH 2/4] Use namespace follow on type in rename(typet) This avoids a disjunction of cases for the different type of tags and makes the rename function simpler. --- src/goto-symex/goto_symex_state.cpp | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index c5d484c7c8b..d0b8a7d9836 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -701,6 +701,9 @@ void goto_symex_statet::rename( } } + // expand struct and union tag types + type = ns.follow(type); + if(type.id()==ID_array) { auto &array_type = to_array_type(type); @@ -725,24 +728,6 @@ void goto_symex_statet::rename( { rename(to_pointer_type(type).subtype(), irep_idt(), ns, level); } - else if(type.id() == ID_symbol_type) - { - const symbolt &symbol = ns.lookup(to_symbol_type(type)); - type = symbol.type; - rename(type, l1_identifier, ns, level); - } - else if(type.id() == ID_union_tag) - { - const symbolt &symbol = ns.lookup(to_union_tag_type(type)); - type = symbol.type; - rename(type, l1_identifier, ns, level); - } - else if(type.id() == ID_struct_tag) - { - const symbolt &symbol = ns.lookup(to_struct_tag_type(type)); - type=symbol.type; - rename(type, l1_identifier, ns, level); - } if(level==L2 && !l1_identifier.empty()) From 9945782e99a25b24cca0fe7071c66a0602e46488 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 23 Jan 2019 09:10:55 +0000 Subject: [PATCH 3/4] Replace insert by emplace and UNREACHABLE by CHECK_RETURN Using emplace avoids a call to make_pair, and CHECK_RETURN is more adapted to the situation were we check the return value of insert/emplace. --- src/goto-symex/symex_start_thread.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 12e5e83e3e3..b339f85f489 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -68,10 +68,11 @@ void goto_symext::symex_start_thread(statet &state) lhs.set_level_0(t); // set up L1 name - if(!state.level1.current_names.insert( - std::make_pair(lhs.get_l1_object_identifier(), - std::make_pair(lhs, 0))).second) - UNREACHABLE; + auto emplace_result = state.level1.current_names.emplace( + std::piecewise_construct, + std::forward_as_tuple(lhs.get_l1_object_identifier()), + std::forward_as_tuple(lhs, 0)); + CHECK_RETURN(emplace_result.second); state.rename(lhs, ns, goto_symex_statet::L1); const irep_idt l1_name=lhs.get_l1_object_identifier(); // store it From 2c74ebeace5ba05a629b87d1f5cfa768eb2283ef Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 23 Jan 2019 12:48:27 +0000 Subject: [PATCH 4/4] Make get_failed_symbol return optional symbol_exprt This is more precise on the type of object returned. --- src/goto-symex/symex_dead.cpp | 7 ++----- src/goto-symex/symex_decl.cpp | 8 ++------ src/pointer-analysis/add_failed_symbols.cpp | 11 +++++------ src/pointer-analysis/add_failed_symbols.h | 6 +++--- src/pointer-analysis/value_set.cpp | 7 ++----- 5 files changed, 14 insertions(+), 25 deletions(-) diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index d72933a2e78..52b0f98b307 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -32,12 +32,9 @@ void goto_symext::symex_dead(statet &state) // in case of pointers, put something into the value set if(code.symbol().type().id() == ID_pointer) { - exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns); - exprt rhs; - - if(failed.is_not_nil()) - rhs = address_of_exprt(failed, to_pointer_type(code.symbol().type())); + if(auto failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns)) + rhs = address_of_exprt(*failed, to_pointer_type(code.symbol().type())); else rhs=exprt(ID_invalid); diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 529c7aceb9e..aa4122826ab 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -48,13 +48,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) // in case of pointers, put something into the value set if(expr.type().id() == ID_pointer) { - exprt failed= - get_failed_symbol(expr, ns); - exprt rhs; - - if(failed.is_not_nil()) - rhs=address_of_exprt(failed, to_pointer_type(expr.type())); + if(auto failed = get_failed_symbol(expr, ns)) + rhs = address_of_exprt(*failed, to_pointer_type(expr.type())); else rhs=exprt(ID_invalid); diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index 9969dd360cc..89d9b5ccc5b 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -89,17 +89,16 @@ void add_failed_symbols(symbol_table_baset &symbol_table) /// Get the failed-dereference symbol for the given symbol /// \param expr: symbol expression to get a failed symbol for /// \param ns: global namespace -/// \return symbol expression for the failed-dereference symbol, or nil_exprt -/// if none exists. -exprt get_failed_symbol( - const symbol_exprt &expr, - const namespacet &ns) +/// \return symbol expression for the failed-dereference symbol, or an empty +/// optional if none exists. +optionalt +get_failed_symbol(const symbol_exprt &expr, const namespacet &ns) { const symbolt &symbol=ns.lookup(expr); irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol); if(failed_symbol_id.empty()) - return nil_exprt(); + return {}; const symbolt &failed_symbol=ns.lookup(failed_symbol_id); diff --git a/src/pointer-analysis/add_failed_symbols.h b/src/pointer-analysis/add_failed_symbols.h index 94c8bd94059..777049aa021 100644 --- a/src/pointer-analysis/add_failed_symbols.h +++ b/src/pointer-analysis/add_failed_symbols.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H #include +#include class symbol_table_baset; class symbolt; @@ -27,8 +28,7 @@ void add_failed_symbol_if_needed( irep_idt failed_symbol_id(const irep_idt &identifier); -exprt get_failed_symbol( - const symbol_exprt &expr, - const namespacet &ns); +optionalt +get_failed_symbol(const symbol_exprt &expr, const namespacet &ns); #endif // CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 486b0e1b365..664b2fde7e6 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1471,12 +1471,9 @@ void value_sett::apply_code_rec( (lhs_type.id() == ID_array && lhs_type.subtype().id() == ID_pointer)) { // assign the address of the failed object - exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns); - - if(failed.is_not_nil()) + if(auto failed = get_failed_symbol(to_symbol_expr(lhs), ns)) { - address_of_exprt address_of_expr( - failed, to_pointer_type(lhs.type())); + address_of_exprt address_of_expr(*failed, to_pointer_type(lhs.type())); assign(lhs, address_of_expr, ns, false, false); } else