From d9cd00f9348b50fbed4bdb5c33fef5706d1e02be Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Feb 2019 15:39:38 +0000 Subject: [PATCH 1/3] Use type equality, not base_type_eq in local safe pointers We no longer need to resort to tag/symbol type resolution. --- .../virtual_call_null_checks.cpp | 2 +- src/analyses/local_safe_pointers.cpp | 23 +++++----- src/analyses/local_safe_pointers.h | 43 +++++-------------- .../goto_instrument_parse_options.cpp | 6 +-- src/goto-symex/symex_function_call.cpp | 2 +- src/goto-symex/symex_main.cpp | 2 +- 6 files changed, 29 insertions(+), 49 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp index 0211ee72acf..3b27b681fc5 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp @@ -74,7 +74,7 @@ SCENARIO( // This analysis checks that any usage of a pointer is preceded by an // assumption that it is non-null // (e.g. assume(x != nullptr); y = x->...) - local_safe_pointerst safe_pointers(ns); + local_safe_pointerst safe_pointers; safe_pointers(main_function.body); for(auto instrit = main_function.body.instructions.begin(), diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 6bd3fb87ca9..9233f94bfc3 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd #include "local_safe_pointers.h" -#include #include #include #include @@ -82,8 +81,7 @@ static optionalt get_null_checked_expr(const exprt &expr) /// \param goto_program: program to analyse void local_safe_pointerst::operator()(const goto_programt &goto_program) { - std::set checked_expressions( - base_type_comparet{ns}); + std::set checked_expressions(type_comparet{}); for(const auto &instruction : goto_program.instructions) { @@ -98,8 +96,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) checked_expressions = findit->second; else { - checked_expressions = - std::set(base_type_comparet{ns}); + checked_expressions = std::set(type_comparet{}); } } @@ -179,8 +176,11 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) /// \param out: stream to write output to /// \param goto_program: GOTO program analysed (the same one passed to /// operator()) +/// \param ns: namespace void local_safe_pointerst::output( - std::ostream &out, const goto_programt &goto_program) + std::ostream &out, + const goto_programt &goto_program, + const namespacet &ns) { forall_goto_program_instructions(i_it, goto_program) { @@ -220,8 +220,11 @@ void local_safe_pointerst::output( /// \param out: stream to write output to /// \param goto_program: GOTO program analysed (the same one passed to /// operator()) +/// \param ns: namespace void local_safe_pointerst::output_safe_dereferences( - std::ostream &out, const goto_programt &goto_program) + std::ostream &out, + const goto_programt &goto_program, + const namespacet &ns) { forall_goto_program_instructions(i_it, goto_program) { @@ -274,10 +277,10 @@ bool local_safe_pointerst::is_non_null_at_program_point( return findit->second.count(*tocheck) != 0; } -bool local_safe_pointerst::base_type_comparet::operator()( - const exprt &e1, const exprt &e2) const +bool local_safe_pointerst::type_comparet:: +operator()(const exprt &e1, const exprt &e2) const { - if(base_type_eq(e1, e2, ns)) + if(e1.type() == e2.type()) return false; else return e1 < e2; diff --git a/src/analyses/local_safe_pointers.h b/src/analyses/local_safe_pointers.h index 2c041d3abb5..efb49d0eb58 100644 --- a/src/analyses/local_safe_pointers.h +++ b/src/analyses/local_safe_pointers.h @@ -23,45 +23,17 @@ Author: Diffblue Ltd /// possibly-aliasing operations are handled pessimistically. class local_safe_pointerst { - /// Comparator that regards base_type_eq expressions as equal, and otherwise + /// Comparator that regards type-equal expressions as equal, and otherwise /// uses the natural (operator<) ordering on irept. - /// An expression is base_type_eq another one if their types, and types of - /// their subexpressions, are identical except that one may use a symbol_typet - /// while the other uses that type's expanded (namespacet::follow'd) form. - class base_type_comparet + class type_comparet { - const namespacet &ns; - public: - explicit base_type_comparet(const namespacet &ns) - : ns(ns) - { - } - - base_type_comparet(const base_type_comparet &other) - : ns(other.ns) - { - } - - base_type_comparet &operator=(const base_type_comparet &other) - { - INVARIANT(&ns == &other.ns, "base_type_comparet: clashing namespaces"); - return *this; - } - bool operator()(const exprt &e1, const exprt &e2) const; }; - std::map> non_null_expressions; - - const namespacet &ns; + std::map> non_null_expressions; public: - local_safe_pointerst(const namespacet &ns) - : ns(ns) - { - } - void operator()(const goto_programt &goto_program); bool is_non_null_at_program_point( @@ -74,10 +46,15 @@ class local_safe_pointerst return is_non_null_at_program_point(deref.op(), program_point); } - void output(std::ostream &stream, const goto_programt &program); + void output( + std::ostream &stream, + const goto_programt &program, + const namespacet &ns); void output_safe_dereferences( - std::ostream &stream, const goto_programt &program); + std::ostream &stream, + const goto_programt &program, + const namespacet &ns); }; #endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 186e328bf90..92326be3707 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -319,17 +319,17 @@ int goto_instrument_parse_optionst::doit() forall_goto_functions(it, goto_model.goto_functions) { - local_safe_pointerst local_safe_pointers(ns); + local_safe_pointerst local_safe_pointers; local_safe_pointers(it->second.body); std::cout << ">>>>\n"; std::cout << ">>>> " << it->first << '\n'; std::cout << ">>>>\n"; if(cmdline.isset("show-local-safe-pointers")) - local_safe_pointers.output(std::cout, it->second.body); + local_safe_pointers.output(std::cout, it->second.body, ns); else { local_safe_pointers.output_safe_dereferences( - std::cout, it->second.body); + std::cout, it->second.body, ns); } std::cout << '\n'; } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index c576ea72864..c430b63aec6 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -240,7 +240,7 @@ void goto_symext::symex_function_call_code( state.dirty.populate_dirty_for_function(identifier, goto_function); auto emplace_safe_pointers_result = - state.safe_pointers.emplace(identifier, local_safe_pointerst{ns}); + state.safe_pointers.emplace(identifier, local_safe_pointerst{}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(goto_function.body); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 94e46ea9220..2242f77f467 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -310,7 +310,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // initialize support analyses auto emplace_safe_pointers_result = - state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{ns}); + state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(start_function->body); From d16c097e862e16bf059b214f5976a3a5009d52aa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Feb 2019 16:00:20 +0000 Subject: [PATCH 2/3] Code cleanup in local_safe_pointers 1) Inline (now trivial) comparision function. 2) Use skip_typecast. --- src/analyses/local_safe_pointers.cpp | 13 +------------ src/analyses/local_safe_pointers.h | 8 +++++--- 2 files changed, 6 insertions(+), 15 deletions(-) diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 9233f94bfc3..f543147a82e 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -271,17 +271,6 @@ bool local_safe_pointerst::is_non_null_at_program_point( auto findit = non_null_expressions.find(program_point->location_number); if(findit == non_null_expressions.end()) return false; - const exprt *tocheck = &expr; - while(tocheck->id() == ID_typecast) - tocheck = &tocheck->op0(); - return findit->second.count(*tocheck) != 0; -} -bool local_safe_pointerst::type_comparet:: -operator()(const exprt &e1, const exprt &e2) const -{ - if(e1.type() == e2.type()) - return false; - else - return e1 < e2; + return findit->second.count(skip_typecast(expr)) != 0; } diff --git a/src/analyses/local_safe_pointers.h b/src/analyses/local_safe_pointers.h index efb49d0eb58..807a4649224 100644 --- a/src/analyses/local_safe_pointers.h +++ b/src/analyses/local_safe_pointers.h @@ -25,10 +25,12 @@ class local_safe_pointerst { /// Comparator that regards type-equal expressions as equal, and otherwise /// uses the natural (operator<) ordering on irept. - class type_comparet + struct type_comparet { - public: - bool operator()(const exprt &e1, const exprt &e2) const; + bool operator()(const exprt &e1, const exprt &e2) const + { + return e1.type() != e2.type() && e1 < e2; + } }; std::map> non_null_expressions; From e1bfc15191780d4198aaf1b8e77268f11eb46f7a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Feb 2019 15:39:57 +0000 Subject: [PATCH 3/3] goto-symex: move safe_pointers to path storage As local_safe_pointerst no longer needs a namespace we can do a partial revert of 959c7a5f7f653a7 (Bugfix: Maintain safe_pointers per-path). On SV-COMP's ReachSafety-ECA, copying safe_pointers accounted for 14% of the time spent in goto_symext::symex_goto (715 of 5119 seconds). --- src/goto-symex/goto_symex.h | 2 -- src/goto-symex/goto_symex_state.h | 3 --- src/goto-symex/path_storage.h | 18 +++++++++++++----- src/goto-symex/symex_dereference.cpp | 5 ++--- src/goto-symex/symex_function_call.cpp | 2 +- src/goto-symex/symex_main.cpp | 2 +- 6 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 5aa920fa0b1..e6272086918 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -17,9 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "goto_symex_state.h" #include "path_storage.h" -#include "symex_target_equation.h" class byte_extract_exprt; class typet; diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index c4eab3bfc59..77a016d520b 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -68,7 +67,6 @@ class goto_statet /// Threads unsigned atomic_section_id = 0; - std::unordered_map safe_pointers; unsigned total_vccs = 0; unsigned remaining_vccs = 0; @@ -320,7 +318,6 @@ inline goto_statet::goto_statet(const class goto_symex_statet &s) source(s.source), propagation(s.propagation), atomic_section_id(s.atomic_section_id), - safe_pointers(s.safe_pointers), total_vccs(s.total_vccs), remaining_vccs(s.remaining_vccs) { diff --git a/src/goto-symex/path_storage.h b/src/goto-symex/path_storage.h index aa15f79249c..0742b291d67 100644 --- a/src/goto-symex/path_storage.h +++ b/src/goto-symex/path_storage.h @@ -5,16 +5,18 @@ #ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H #define CPROVER_GOTO_SYMEX_PATH_STORAGE_H -#include "goto_symex_state.h" -#include "symex_target_equation.h" - -#include #include -#include #include +#include +#include + +#include #include +#include "goto_symex_state.h" +#include "symex_target_equation.h" + /// Functor generating fresh nondet symbols class symex_nondet_generatort { @@ -90,6 +92,12 @@ class path_storaget /// Counter for nondet objects, which require unique names symex_nondet_generatort build_symex_nondet; + /// Map function identifiers to \ref local_safe_pointerst instances. This is + /// to identify derferences that are guaranteed to be safe in a given + /// execution context, thus helping to avoid symex to follow spurious + /// error-handling paths. + std::unordered_map safe_pointers; + private: // Derived classes should override these methods, allowing the base class to // enforce preconditions. diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index a8e30ada387..cc91f3c4125 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -211,9 +211,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state) { get_original_name(to_check); - expr_is_not_null = - state.safe_pointers.at(expr_function).is_safe_dereference( - to_check, state.source.pc); + expr_is_not_null = path_storage.safe_pointers.at(expr_function) + .is_safe_dereference(to_check, state.source.pc); } } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index c430b63aec6..3e489f312b9 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -240,7 +240,7 @@ void goto_symext::symex_function_call_code( state.dirty.populate_dirty_for_function(identifier, goto_function); auto emplace_safe_pointers_result = - state.safe_pointers.emplace(identifier, local_safe_pointerst{}); + path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(goto_function.body); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 2242f77f467..4384384ae0b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -310,7 +310,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // initialize support analyses auto emplace_safe_pointers_result = - state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{}); + path_storage.safe_pointers.emplace(entry_point_id, local_safe_pointerst{}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(start_function->body);