From 879a47b4622cfc19e7be712b716c9e720f989109 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 08:11:09 +0000 Subject: [PATCH 1/8] Symex support for lhs-typecasts and side effects --- src/path-symex/path_symex.cpp | 8 ++++++++ src/path-symex/path_symex_state_read.cpp | 9 ++++++++- src/path-symex/var_map.h | 10 ++++++++-- 3 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index f64071ec617..6c86d9c416c 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -422,6 +422,14 @@ void path_symext::assign_rec( var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt(); } } + else if(ssa_lhs.id()==ID_typecast) + { + // dereferencing might yield a typecast + const exprt &new_lhs=to_typecast_expr(ssa_lhs).op(); + typecast_exprt new_rhs(ssa_rhs, new_lhs.type()); + + assign_rec(state, guard, new_lhs, new_rhs); + } else if(ssa_lhs.id()==ID_member) { #ifdef DEBUG diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index 87dea21be4a..06a7f10f59d 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec( { irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count); var_map.nondet_count++; - return symbol_exprt(id, src.type()); + + auxiliary_symbolt nondet_symbol; + nondet_symbol.name=id; + nondet_symbol.base_name=id; + nondet_symbol.type=src.type(); + var_map.new_symbols.add(nondet_symbol); + + return nondet_symbol.symbol_expr(); } else throw "instantiate_rec: unexpected side effect "+id2string(statement); diff --git a/src/path-symex/var_map.h b/src/path-symex/var_map.h index 7b17169c441..09511174cab 100644 --- a/src/path-symex/var_map.h +++ b/src/path-symex/var_map.h @@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include class var_mapt { public: explicit var_mapt(const namespacet &_ns): - ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0) + ns(_ns.get_symbol_table(), new_symbols), + shared_count(0), + local_count(0), + nondet_count(0), + dynamic_count(0) { } @@ -93,7 +98,8 @@ class var_mapt void init(var_infot &var_info); - const namespacet &ns; + const namespacet ns; + symbol_tablet new_symbols; void output(std::ostream &) const; From 08f1a9e1dc5e546d81baf1620a8d792b183dfa74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:30:19 +0000 Subject: [PATCH 2/8] Extract elements of array, struct directly instead of simplifying vectors don't need to be handled, they have been removed via remove_vector. --- src/path-symex/path_symex.cpp | 78 ++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 34 deletions(-) diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 6c86d9c416c..043ac0fb05c 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -549,14 +549,30 @@ void path_symext::assign_rec( assert(operands.size()==components.size()); - for(std::size_t i=0; i Date: Sun, 26 Jun 2016 13:32:51 +0000 Subject: [PATCH 3/8] Removed redundant get_pc() (there is pc()) --- src/path-symex/path_symex_state.cpp | 6 ------ src/path-symex/path_symex_state.h | 7 ++++--- src/symex/path_search.cpp | 4 ++-- 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 495f598202a..fe663da5b7c 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -41,12 +41,6 @@ path_symex_statet initial_state( return s; } -loc_reft path_symex_statet::get_pc() const -{ - assert(current_thread + #include "locs.h" #include "var_map.h" #include "path_symex_history.h" @@ -111,11 +113,9 @@ struct path_symex_statet current_thread=_thread; } - loc_reft get_pc() const; - goto_programt::const_targett get_instruction() const { - return locs[get_pc()].target; + return locs[pc()].target; } bool is_executable() const @@ -145,6 +145,7 @@ struct path_symex_statet loc_reft pc() const { + PRECONDITION(current_thread Date: Sun, 26 Jun 2016 13:42:44 +0000 Subject: [PATCH 4/8] Fix symex thread statistics --- src/symex/path_search.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 4a510d1840a..42de78a32f7 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -103,7 +103,7 @@ path_searcht::resultt path_searcht::operator()( if(number_of_steps%1000==0) { status() << "Queue " << queue.size() - << " thread " << state.get_current_thread() + << " thread " << state.get_current_thread()+1 << '/' << state.threads.size() << " PC " << state.pc() << messaget::eom; } From c69a21b1923f94a06f0ddb82415119aa197353f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:45:11 +0000 Subject: [PATCH 5/8] Extended symex progres statistics --- src/symex/path_search.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 42de78a32f7..2d7d8faedb6 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -102,10 +102,13 @@ path_searcht::resultt path_searcht::operator()( if(number_of_steps%1000==0) { + time_periodt running_time=current_time()-start_time; status() << "Queue " << queue.size() << " thread " << state.get_current_thread()+1 << '/' << state.threads.size() - << " PC " << state.pc() << messaget::eom; + << " PC " << state.pc() + << " [" << number_of_steps << " steps, " + << running_time << "s]" << messaget::eom; } // an error, possibly? From acdc797f7bdbab7fb255ec0d1dfdb4ba606134fd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:47:58 +0000 Subject: [PATCH 6/8] Symex: output instruction processing and loop unwinding like CBMC Unlike CBMC, all output is enabled in debug mode only. --- src/symex/path_search.cpp | 55 +++++++++++++++++++++++++++++++++++++-- src/symex/path_search.h | 2 ++ 2 files changed, 55 insertions(+), 2 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 2d7d8faedb6..639ee701d9d 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -267,6 +267,19 @@ bool path_searcht::drop_state(const statet &state) { goto_programt::const_targett pc=state.get_instruction(); + const source_locationt &source_location=pc->source_location; + + if(!source_location.is_nil() && + last_source_location!=source_location) + { + debug() << "SYMEX at file " << source_location.get_file() + << " line " << source_location.get_line() + << " function " << source_location.get_function() + << eom; + + last_source_location=source_location; + } + // depth limit if(depth_limit_set && state.get_depth()>depth_limit) return true; @@ -282,17 +295,55 @@ bool path_searcht::drop_state(const statet &state) // unwinding limit -- loops if(unwind_limit_set && state.get_instruction()->is_backwards_goto()) { + bool stop=false; + for(const auto &loop_info : state.unwinding_map) if(loop_info.second>unwind_limit) - return true; + { + stop=true; + break; + } + + const irep_idt id=goto_programt::loop_id(pc); + path_symex_statet::unwinding_mapt::const_iterator entry= + state.unwinding_map.find(state.pc()); + debug() << (stop?"Not unwinding":"Unwinding") + << " loop " << id << " iteration " + << (entry==state.unwinding_map.end()?-1:entry->second) + << " (" << unwind_limit << " max)" + << " " << source_location + << " thread " << state.get_current_thread() << eom; + + if(stop) + return true; } // unwinding limit -- recursion if(unwind_limit_set && state.get_instruction()->is_function_call()) { + bool stop=false; + for(const auto &rec_info : state.recursion_map) if(rec_info.second>unwind_limit) - return true; + { + stop=true; + break; + } + + exprt function=to_code_function_call(pc->code).function(); + const irep_idt id=function.get(ID_identifier); // could be nil + path_symex_statet::recursion_mapt::const_iterator entry= + state.recursion_map.find(id); + if(entry!=state.recursion_map.end()) + debug() << (stop?"Not unwinding":"Unwinding") + << " recursion " << id << " iteration " + << entry->second + << " (" << unwind_limit << " max)" + << " " << source_location + << " thread " << state.get_current_thread() << eom; + + if(stop) + return true; } if(pc->is_assume() && diff --git a/src/symex/path_search.h b/src/symex/path_search.h index ca570819cc8..e0a64270e22 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -137,6 +137,8 @@ class path_searcht:public safety_checkert bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; + + source_locationt last_source_location; }; #endif // CPROVER_SYMEX_PATH_SEARCH_H From 260e03d4184d8114ec58506662ffc31f18a69902 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 26 Jun 2016 13:49:57 +0000 Subject: [PATCH 7/8] symex --max-search-time limit and cleanup All symex limits use value -1 as marking "not set". Use size_t for counting statistics. --- src/symex/path_search.cpp | 15 ++++++--- src/symex/path_search.h | 52 ++++++++++++++++--------------- src/symex/symex_parse_options.cpp | 5 +++ src/symex/symex_parse_options.h | 2 +- 4 files changed, 43 insertions(+), 31 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 639ee701d9d..b6743063401 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -281,19 +281,19 @@ bool path_searcht::drop_state(const statet &state) } // depth limit - if(depth_limit_set && state.get_depth()>depth_limit) + if(depth_limit>=0 && state.get_depth()>depth_limit) return true; // context bound - if(context_bound_set && state.get_no_thread_interleavings()>context_bound) + if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound) return true; // branch bound - if(branch_bound_set && state.get_no_branches()>branch_bound) + if(branch_bound>=0 && state.get_no_branches()>branch_bound) return true; // unwinding limit -- loops - if(unwind_limit_set && state.get_instruction()->is_backwards_goto()) + if(unwind_limit>=0 && pc->is_backwards_goto()) { bool stop=false; @@ -319,7 +319,7 @@ bool path_searcht::drop_state(const statet &state) } // unwinding limit -- recursion - if(unwind_limit_set && state.get_instruction()->is_function_call()) + if(unwind_limit>=0 && pc->is_function_call()) { bool stop=false; @@ -346,6 +346,11 @@ bool path_searcht::drop_state(const statet &state) return true; } + // search time limit (--max-search-time) + if(time_limit>=0 && + current_time().get_t()>start_time.get_t()+time_limit*1000) + return true; + if(pc->is_assume() && simplify_expr(pc->guard, ns).is_false()) { diff --git a/src/symex/path_search.h b/src/symex/path_search.h index e0a64270e22..4823998ef8a 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -26,10 +26,11 @@ class path_searcht:public safety_checkert safety_checkert(_ns), show_vcc(false), eager_infeasibility(false), - depth_limit_set(false), // no limit - context_bound_set(false), - unwind_limit_set(false), - branch_bound_set(false), + depth_limit(-1), // no limit + context_bound(-1), + branch_bound(-1), + unwind_limit(-1), + time_limit(-1), search_heuristic(search_heuristict::DFS) { } @@ -37,42 +38,43 @@ class path_searcht:public safety_checkert virtual resultt operator()( const goto_functionst &goto_functions); - void set_depth_limit(unsigned limit) + void set_depth_limit(int limit) { - depth_limit_set=true; depth_limit=limit; } - void set_context_bound(unsigned limit) + void set_context_bound(int limit) { - context_bound_set=true; context_bound=limit; } - void set_branch_bound(unsigned limit) + void set_branch_bound(int limit) { - branch_bound_set=true; branch_bound=limit; } - void set_unwind_limit(unsigned limit) + void set_unwind_limit(int limit) { - unwind_limit_set=true; unwind_limit=limit; } + void set_time_limit(int limit) + { + time_limit=limit; + } + bool show_vcc; bool eager_infeasibility; // statistics - unsigned number_of_dropped_states; - unsigned number_of_paths; - unsigned number_of_steps; - unsigned number_of_feasible_paths; - unsigned number_of_infeasible_paths; - unsigned number_of_VCCs; - unsigned number_of_VCCs_after_simplification; - unsigned number_of_failed_properties; + std::size_t number_of_dropped_states; + std::size_t number_of_paths; + std::size_t number_of_steps; + std::size_t number_of_feasible_paths; + std::size_t number_of_infeasible_paths; + std::size_t number_of_VCCs; + std::size_t number_of_VCCs_after_simplification; + std::size_t number_of_failed_properties; std::size_t number_of_locs; absolute_timet start_time; time_periodt sat_time; @@ -130,11 +132,11 @@ class path_searcht:public safety_checkert void initialize_property_map( const goto_functionst &goto_functions); - unsigned depth_limit; - unsigned context_bound; - unsigned branch_bound; - unsigned unwind_limit; - bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set; + int depth_limit; + int context_bound; + int branch_bound; + int unwind_limit; + int time_limit; enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 5fc475ee154..03a5486f0e1 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -186,6 +186,10 @@ int symex_parse_optionst::doit() path_search.set_unwind_limit( unsafe_string2unsigned(cmdline.get_value("unwind"))); + if(cmdline.isset("max-search-time")) + path_search.set_time_limit( + safe_string2unsigned(cmdline.get_value("max-search-time"))); + if(cmdline.isset("dfs")) path_search.set_dfs(); @@ -607,6 +611,7 @@ void symex_parse_optionst::help() " --depth nr limit search depth\n" " --context-bound nr limit number of context switches\n" " --branch-bound nr limit number of branches taken\n" + " --max-search-time s limit search to approximately s seconds\n" "\n" "Other options:\n" " --version show version and exit\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index b4fc6fe2e1c..a9f3d9e3e83 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -30,7 +30,7 @@ class optionst; #define SYMEX_OPTIONS \ "(function):" \ "D:I:" \ - "(depth):(context-bound):(branch-bound):(unwind):" \ + "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ From 73adfb0fe4bfd2337895bda90bfe1cfe092869fc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 19 Apr 2017 16:28:05 +0000 Subject: [PATCH 8/8] Perform function-pointer removal in symex --- src/symex/symex_parse_options.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 03a5486f0e1..c2e567cc643 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -304,6 +305,12 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // remove stuff remove_complex(goto_model); remove_vector(goto_model); + // remove function pointers + status() << "Removal of function pointers and virtual functions" << eom; + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); // Java throw and catch -> explicit exceptional return variables: