diff --git a/regression/book-examples/sll_min/assertions.desc b/regression/book-examples/sll_min/assertions.desc index ce1d5a281..9be77676a 100644 --- a/regression/book-examples/sll_min/assertions.desc +++ b/regression/book-examples/sll_min/assertions.desc @@ -1,6 +1,6 @@ CORE sll_min.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/calendar/test.desc b/regression/heap-data/calendar/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/calendar/test.desc +++ b/regression/heap-data/calendar/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/cart/test.desc b/regression/heap-data/cart/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/cart/test.desc +++ b/regression/heap-data/cart/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/hash_fun/test.desc b/regression/heap-data/hash_fun/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/hash_fun/test.desc +++ b/regression/heap-data/hash_fun/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/min_max/test.desc b/regression/heap-data/min_max/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/min_max/test.desc +++ b/regression/heap-data/min_max/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/packet_filter/test.desc b/regression/heap-data/packet_filter/test.desc index 0b918f142..5652822cf 100644 --- a/regression/heap-data/packet_filter/test.desc +++ b/regression/heap-data/packet_filter/test.desc @@ -1,6 +1,6 @@ THOROUGH main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/process_queue/test.desc b/regression/heap-data/process_queue/test.desc index 0b918f142..5652822cf 100644 --- a/regression/heap-data/process_queue/test.desc +++ b/regression/heap-data/process_queue/test.desc @@ -1,6 +1,6 @@ THOROUGH main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/quick_sort_split/test.desc b/regression/heap-data/quick_sort_split/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/quick_sort_split/test.desc +++ b/regression/heap-data/quick_sort_split/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example/test.desc b/regression/heap-data/running_example/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/running_example/test.desc +++ b/regression/heap-data/running_example/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example_assume/test.desc b/regression/heap-data/running_example_assume/test.desc index 0c55e707a..d07fde486 100644 --- a/regression/heap-data/running_example_assume/test.desc +++ b/regression/heap-data/running_example_assume/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem1/test.desc b/regression/heap-data/shared_mem1/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/shared_mem1/test.desc +++ b/regression/heap-data/shared_mem1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem2/test.desc b/regression/heap-data/shared_mem2/test.desc index b83f79c6e..514cdca9e 100644 --- a/regression/heap-data/shared_mem2/test.desc +++ b/regression/heap-data/shared_mem2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine +--heap --values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/built_from_end/test.desc b/regression/heap/built_from_end/test.desc index df624d753..8050c4544 100644 --- a/regression/heap/built_from_end/test.desc +++ b/regression/heap/built_from_end/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --no-propagation +--heap --intervals --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/list_false/test.desc b/regression/heap/list_false/test.desc index 9556b3310..2f65dfc83 100644 --- a/regression/heap/list_false/test.desc +++ b/regression/heap/list_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --no-propagation +--heap --intervals --no-propagation ^EXIT=5$ ^SIGNAL=0$ ^VERIFICATION INCONCLUSIVE$ diff --git a/regression/heap/list_false_kind/test.desc b/regression/heap/list_false_kind/test.desc index 3d24fc98f..ccc2d5c7c 100644 --- a/regression/heap/list_false_kind/test.desc +++ b/regression/heap/list_false_kind/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --no-propagation --k-induction +--heap --intervals --no-propagation --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/heap/simple_false/test.desc b/regression/heap/simple_false/test.desc index 9556b3310..2f65dfc83 100644 --- a/regression/heap/simple_false/test.desc +++ b/regression/heap/simple_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --no-propagation +--heap --intervals --no-propagation ^EXIT=5$ ^SIGNAL=0$ ^VERIFICATION INCONCLUSIVE$ diff --git a/regression/heap/simple_false_kind/test.desc b/regression/heap/simple_false_kind/test.desc index 3d24fc98f..ccc2d5c7c 100644 --- a/regression/heap/simple_false_kind/test.desc +++ b/regression/heap/simple_false_kind/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --no-propagation --k-induction +--heap --intervals --no-propagation --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/heap/sll_simple/test.desc b/regression/heap/sll_simple/test.desc index b0b056464..c8ea94896 100644 --- a/regression/heap/sll_simple/test.desc +++ b/regression/heap/sll_simple/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap --no-propagation --heap-interval +--heap --no-propagation --intervals ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc index 6cb3dc340..a9c706a24 100644 --- a/regression/memsafety/built_from_end/test.desc +++ b/regression/memsafety/built_from_end/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --pointer-check --no-assertions +--heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc index 6875c0855..a91a719ec 100644 --- a/regression/memsafety/built_from_end_false/test.desc +++ b/regression/memsafety/built_from_end_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --pointer-check --no-assertions --k-induction +--heap --intervals --pointer-check --no-assertions --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc index 23247e589..8efda9ea8 100644 --- a/regression/memsafety/simple_false/test.desc +++ b/regression/memsafety/simple_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --pointer-check --k-induction +--heap --intervals --pointer-check --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc index 6cb3dc340..a9c706a24 100644 --- a/regression/memsafety/simple_true/test.desc +++ b/regression/memsafety/simple_true/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --pointer-check --no-assertions +--heap --intervals --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 6e964157b..24b30bf17 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -162,55 +162,78 @@ void twols_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("havoc")) options.set_option("havoc", true); - else if(cmdline.isset("equalities")) - { - options.set_option("equalities", true); - options.set_option("std-invariants", true); - } - else if(cmdline.isset("heap")) - { - options.set_option("heap", true); - } - else if(cmdline.isset("heap-interval")) - { - options.set_option("heap-interval", true); - if(cmdline.isset("sympath")) - options.set_option("sympath", true); - } - else if(cmdline.isset("heap-zones")) - { - options.set_option("heap-zones", true); - if(cmdline.isset("sympath")) - options.set_option("sympath", true); - } - else if(cmdline.isset("heap-values-refine")) - { - options.set_option("heap-values-refine", true); - options.set_option("heap-interval", true); - if(cmdline.isset("sympath")) - options.set_option("sympath", true); - } else { - if(cmdline.isset("zones")) + // Options for using simple domains + optionst::value_listt simple_domains; + if(cmdline.isset("equalities")) + { + options.set_option("equalities", true); + options.set_option("std-invariants", true); + simple_domains.push_back("equalities"); + } + if(cmdline.isset("heap")) + { + options.set_option("heap", true); + simple_domains.push_back("heap"); + } + + // Choose only a single value domain + if(cmdline.isset("values-refine")) + { + options.set_option("values-refine", true); + options.set_option("intervals", true); + simple_domains.push_back("intervals"); + } + else if(cmdline.isset("zones")) + { options.set_option("zones", true); + simple_domains.push_back("zones"); + } else if(cmdline.isset("qzones")) + { options.set_option("qzones", true); + simple_domains.push_back("qzones"); + } else if(cmdline.isset("octagons")) + { options.set_option("octagons", true); - else // if(cmdline.isset("intervals")) // default + simple_domains.push_back("octagons"); + } + else if(cmdline.isset("intervals")) + { + options.set_option("intervals", true); + simple_domains.push_back("intervals"); + } + + // If no simple domains are specified, use intervals + if(simple_domains.empty()) + { options.set_option("intervals", true); + simple_domains.push_back("intervals"); + } + + // TODO: due to various modifications of options during verification + // (e.g. in summary_checker_ait or in handle_special_functions), it is not + // possible to rely on the content of this option. + options.set_option("simple-domains", simple_domains); - if(cmdline.isset("enum-solver")) - options.set_option("enum-solver", true); - else // if(cmdline.isset("binsearch-solver")) // default - options.set_option("binsearch-solver", true); + if(options.get_bool_option("values-refine") || + options.get_bool_option("zones") || + options.get_bool_option("qzones") || + options.get_bool_option("octagons") || + options.get_bool_option("intervals")) + { + // Choose solver for numerical domains + if(cmdline.isset("enum-solver")) + options.set_option("enum-solver", true); + else // if(cmdline.isset("binsearch-solver")) // default + options.set_option("binsearch-solver", true); + } } - if(cmdline.isset("heap") || - cmdline.isset("heap-interval") || - cmdline.isset("heap-zones") || - cmdline.isset("heap-values-refine")) + // Heap domain requires full program inlining and usage of symbolic paths + if(cmdline.isset("heap")) { options.set_option("inline", true); options.set_option("sympath", true); @@ -379,14 +402,6 @@ int twols_parse_optionst::doit() return 6; const namespacet ns(goto_model.symbol_table); - ssa_heap_analysist heap_analysis(ns); - if((options.get_bool_option("heap") || - options.get_bool_option("heap-interval")) && - !options.get_bool_option("inline")) - { - heap_analysis(goto_model.goto_functions); - add_dynamic_object_symbols(heap_analysis, goto_model); - } if(cmdline.isset("show-stats")) { @@ -403,7 +418,6 @@ int twols_parse_optionst::doit() show_ssa( goto_model, options, - heap_analysis, function, simplify, std::cout, @@ -551,18 +565,18 @@ int twols_parse_optionst::doit() if(!options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) checker=std::unique_ptr( - new summary_checker_ait(options, heap_analysis)); + new summary_checker_ait(options)); if(options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) checker=std::unique_ptr( - new summary_checker_kindt(options, heap_analysis)); + new summary_checker_kindt(options)); if(!options.get_bool_option("k-induction") && options.get_bool_option("incremental-bmc")) checker=std::unique_ptr( - new summary_checker_bmct(options, heap_analysis)); + new summary_checker_bmct(options)); if(options.get_bool_option("nontermination")) checker=std::unique_ptr( - new summary_checker_nontermt(options, heap_analysis)); + new summary_checker_nontermt(options)); checker->set_message_handler(get_message_handler()); checker->simplify=!cmdline.isset("no-simplify"); @@ -1561,11 +1575,7 @@ void twols_parse_optionst::help() " --heap use heap domain\n" " --zones use zone domain\n" " --octagons use octagon domain\n" - " --heap-interval use heap domain with interval domain for\n" - " values\n" - " --heap-zones use heap domain with zones domain for values\n" // NOLINT(*) - " --heap-values-refine use heap domain with a dynamic refinement\n" - " of strength of the value domain\n" + " --values-refine use dynamic refinement of strength of the value domain\n" // NOLINT(*) " --sympath compute invariant for each symbolic path\n" " (only usable with --heap-* switches)\n" " --enum-solver use solver based on model enumeration\n" diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 838be69e7..3b617893b 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -47,9 +47,7 @@ class optionst; "(octagons)" \ "(equalities)" \ "(heap)" \ - "(heap-interval)" \ - "(heap-zones)" \ - "(heap-values-refine)" \ + "(values-refine)" \ "(sympath)" \ "(enum-solver)(binsearch-solver)(arrays)"\ "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ @@ -192,9 +190,6 @@ class twols_parse_optionst: void remove_loops_in_entry(goto_modelt &goto_model); void create_dynamic_objects(goto_modelt &goto_model); void add_dynamic_object_rec(exprt &expr, symbol_tablet &symbol_table); - void add_dynamic_object_symbols( - const ssa_heap_analysist &heap_analysis, - goto_modelt &goto_model); void split_same_symbolic_object_assignments(goto_modelt &goto_model); void remove_dead_goto(goto_modelt &goto_model); void compute_dynobj_instances( diff --git a/src/2ls/dynamic_cfg.h b/src/2ls/dynamic_cfg.h index 802276005..3d8a9537c 100644 --- a/src/2ls/dynamic_cfg.h +++ b/src/2ls/dynamic_cfg.h @@ -14,6 +14,7 @@ Author: Peter Schrammel #include #include +#include #include #include diff --git a/src/2ls/horn_encoding.cpp b/src/2ls/horn_encoding.cpp index cf130fa76..88a46080e 100644 --- a/src/2ls/horn_encoding.cpp +++ b/src/2ls/horn_encoding.cpp @@ -63,8 +63,7 @@ void horn_encodingt::translate( ";\n"; // compute SSA - ssa_heap_analysist heap_analysis(ns); - local_SSAt local_SSA(f_it->second, ns, options, heap_analysis, ""); + local_SSAt local_SSA(f_it->second, ns, options, ""); const goto_programt &body=f_it->second.body; diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index a31e747e3..a906678dd 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -435,44 +435,6 @@ void twols_parse_optionst::add_dynamic_object_rec( } } -/// Add symbols for all dynamic objects in the program into the symbol table. -void twols_parse_optionst::add_dynamic_object_symbols( - const ssa_heap_analysist &heap_analysis, - goto_modelt &goto_model) -{ - forall_goto_functions(f_it, goto_model.goto_functions) - { - forall_goto_program_instructions(i_it, f_it->second.body) - { - if(i_it->is_function_call()) - { - auto &fun_call=to_code_function_call(i_it->code); - const irep_idt fname= - to_symbol_expr(fun_call.function()).get_identifier(); - auto n_it=i_it; - ++n_it; - for(const symbol_exprt &o : - heap_analysis[n_it].new_caller_objects(fname, i_it)) - { - // New symbol - symbolt object_symbol; - - object_symbol.name=o.get_identifier(); - object_symbol.base_name=id2string(object_symbol.name).substr(5); - object_symbol.is_lvalue=true; - - object_symbol.type=o.type(); - object_symbol.type.set("#dynamic", true); - - object_symbol.mode=ID_C; - - goto_model.symbol_table.add(object_symbol); - } - } - } - } -} - /// Split assignments that have same symbolic dereference object on both sides /// into two separate assignments. void twols_parse_optionst::split_same_symbolic_object_assignments( @@ -662,8 +624,7 @@ std::map twols_parse_optionst::split_dynamic_objects( if(!f_it->second.body_available()) continue; namespacet ns(goto_model.symbol_table); - ssa_value_ait value_analysis( - f_it->second, ns, options, ssa_heap_analysist(ns)); + ssa_value_ait value_analysis(f_it->second, ns, options); dynobj_instance_analysist do_inst( f_it->second, ns, options, value_analysis); diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp index 1b413eb51..296b9740e 100644 --- a/src/2ls/show.cpp +++ b/src/2ls/show.cpp @@ -33,18 +33,16 @@ void show_assignments( const goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, - std::ostream &out, - const ssa_heap_analysist &heap_analysis) + std::ostream &out) { - ssa_objectst ssa_objects(goto_function, ns, heap_analysis); - ssa_value_ait ssa_value_ai(goto_function, ns, options, heap_analysis); + ssa_objectst ssa_objects(goto_function, ns); + ssa_value_ait ssa_value_ai(goto_function, ns, options); assignmentst assignments( goto_function.body, ns, options, ssa_objects, - ssa_value_ai, - heap_analysis); + ssa_value_ai); assignments.output(ns, goto_function.body, out); } @@ -57,8 +55,6 @@ void show_assignments( { const namespacet ns(goto_model.symbol_table); - ssa_heap_analysist heap_analysis(ns); - if(!function.empty()) { goto_functionst::function_mapt::const_iterator @@ -66,7 +62,7 @@ void show_assignments( if(f_it==goto_model.goto_functions.function_map.end()) out << "function " << function << " not found\n"; else - show_assignments(f_it->second, ns, options, out, heap_analysis); + show_assignments(f_it->second, ns, options, out); } else { @@ -74,7 +70,7 @@ void show_assignments( { out << ">>>> Function " << f_it->first << "\n"; - show_assignments(f_it->second, ns, options, out, heap_analysis); + show_assignments(f_it->second, ns, options, out); out << "\n"; } @@ -85,18 +81,16 @@ void show_defs( const goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, - std::ostream &out, - const ssa_heap_analysist &heap_analysis) + std::ostream &out) { - ssa_objectst ssa_objects(goto_function, ns, heap_analysis); - ssa_value_ait ssa_value_ai(goto_function, ns, options, heap_analysis); + ssa_objectst ssa_objects(goto_function, ns); + ssa_value_ait ssa_value_ai(goto_function, ns, options); assignmentst assignments( goto_function.body, ns, options, ssa_objects, - ssa_value_ai, - heap_analysis); + ssa_value_ai); ssa_ait ssa_analysis(assignments); ssa_analysis(goto_function, ns); ssa_analysis.output(ns, goto_function.body, out); @@ -111,8 +105,6 @@ void show_defs( { const namespacet ns(goto_model.symbol_table); - ssa_heap_analysist heap_analysis(ns); - if(!function.empty()) { goto_functionst::function_mapt::const_iterator @@ -120,7 +112,7 @@ void show_defs( if(f_it==goto_model.goto_functions.function_map.end()) out << "function " << function << " not found\n"; else - show_defs(f_it->second, ns, options, out, heap_analysis); + show_defs(f_it->second, ns, options, out); } else { @@ -128,7 +120,7 @@ void show_defs( { out << ">>>> Function " << f_it->first << "\n"; - show_defs(f_it->second, ns, options, out, heap_analysis); + show_defs(f_it->second, ns, options, out); out << "\n"; } @@ -176,7 +168,6 @@ void show_guards( void show_ssa( const goto_functionst::goto_functiont &goto_function, - const ssa_heap_analysist &heap_analysis, bool simplify, const namespacet &ns, const optionst &options, @@ -185,7 +176,7 @@ void show_ssa( if(!goto_function.body_available()) return; - unwindable_local_SSAt local_SSA(goto_function, ns, options, heap_analysis); + unwindable_local_SSAt local_SSA(goto_function, ns, options); if(simplify) ::simplify(local_SSA, ns); local_SSA.output_verbose(out); @@ -194,7 +185,6 @@ void show_ssa( void show_ssa( const goto_modelt &goto_model, const optionst &options, - const ssa_heap_analysist &heap_analysis, const irep_idt &function, bool simplify, std::ostream &out, @@ -210,7 +200,7 @@ void show_ssa( if(f_it==goto_model.goto_functions.function_map.end()) out << "function " << function << " not found\n"; else - show_ssa(f_it->second, heap_analysis, simplify, ns, options, out); + show_ssa(f_it->second, simplify, ns, options, out); } else { @@ -223,7 +213,7 @@ void show_ssa( out << ">>>> Function " << f_it->first << "\n"; - show_ssa(f_it->second, heap_analysis, simplify, ns, options, out); + show_ssa(f_it->second, simplify, ns, options, out); out << "\n"; } @@ -399,11 +389,10 @@ void show_value_set( const goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, - std::ostream &out, - const ssa_heap_analysist &heap_analysis) + std::ostream &out) { - ssa_objectst ssa_objects(goto_function, ns, heap_analysis); - ssa_value_ait ssa_value_ai(goto_function, ns, options, heap_analysis); + ssa_objectst ssa_objects(goto_function, ns); + ssa_value_ait ssa_value_ai(goto_function, ns, options); ssa_value_ai.output(ns, goto_function, out); } @@ -416,8 +405,6 @@ void show_value_sets( { const namespacet ns(goto_model.symbol_table); - ssa_heap_analysist heap_analysis(ns); - if(!function.empty()) { goto_functionst::function_mapt::const_iterator @@ -425,7 +412,7 @@ void show_value_sets( if(f_it==goto_model.goto_functions.function_map.end()) out << "function " << function << " not found\n"; else - show_value_set(f_it->second, ns, options, out, heap_analysis); + show_value_set(f_it->second, ns, options, out); } else { @@ -433,7 +420,7 @@ void show_value_sets( { out << ">>>> Function " << f_it->first << "\n"; - show_value_set(f_it->second, ns, options, out, heap_analysis); + show_value_set(f_it->second, ns, options, out); out << "\n"; } diff --git a/src/2ls/show.h b/src/2ls/show.h index 2a3bb7e02..c6621d283 100644 --- a/src/2ls/show.h +++ b/src/2ls/show.h @@ -27,7 +27,6 @@ class ssa_heap_analysist; void show_ssa( const goto_modelt &, const optionst &, - const ssa_heap_analysist &, const irep_idt &function, bool simplify, std::ostream &, diff --git a/src/2ls/summary_checker_ai.cpp b/src/2ls/summary_checker_ai.cpp index fcebd4d87..33a729484 100644 --- a/src/2ls/summary_checker_ai.cpp +++ b/src/2ls/summary_checker_ai.cpp @@ -17,7 +17,7 @@ property_checkert::resultt summary_checker_ait::operator()( { const namespacet ns(goto_model.symbol_table); - SSA_functions(goto_model, ns, heap_analysis); + SSA_functions(goto_model, ns); ssa_unwinder.init(false, false); @@ -74,12 +74,12 @@ property_checkert::resultt summary_checker_ait::operator()( report_statistics(); if(result==property_checkert::UNKNOWN && - options.get_bool_option("heap-values-refine") && - options.get_bool_option("heap-interval")) + options.get_bool_option("values-refine") && + options.get_bool_option("intervals")) { summary_db.clear(); - options.set_option("heap-interval", false); - options.set_option("heap-zones", true); + options.set_option("intervals", false); + options.set_option("zones", true); } else { diff --git a/src/2ls/summary_checker_ai.h b/src/2ls/summary_checker_ai.h index 10016d864..a9e30767b 100644 --- a/src/2ls/summary_checker_ai.h +++ b/src/2ls/summary_checker_ai.h @@ -17,12 +17,8 @@ Author: Peter Schrammel class summary_checker_ait:public summary_checker_baset { public: - inline summary_checker_ait( - optionst &_options, - const ssa_heap_analysist &heap_analysis): - summary_checker_baset(_options, heap_analysis) - { - } + explicit inline summary_checker_ait(optionst &_options): + summary_checker_baset(_options) {} virtual resultt operator()(const goto_modelt &); diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index 9faa5c5a1..c632a0e59 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -44,8 +44,7 @@ Author: Peter Schrammel void summary_checker_baset::SSA_functions( const goto_modelt &goto_model, - const namespacet &ns, - const ssa_heap_analysist &heap_analysis) + const namespacet &ns) { // compute SSA for all the functions forall_goto_functions(f_it, goto_model.goto_functions) @@ -56,7 +55,7 @@ void summary_checker_baset::SSA_functions( continue; status() << "Computing SSA of " << f_it->first << messaget::eom; - ssa_db.create(f_it->first, f_it->second, ns, heap_analysis); + ssa_db.create(f_it->first, f_it->second, ns); local_SSAt &SSA=ssa_db.get(f_it->first); // simplify, if requested diff --git a/src/2ls/summary_checker_base.h b/src/2ls/summary_checker_base.h index bf01b8aa9..e9b09c413 100644 --- a/src/2ls/summary_checker_base.h +++ b/src/2ls/summary_checker_base.h @@ -17,7 +17,6 @@ Author: Peter Schrammel #include #include -#include #include #include #include @@ -32,8 +31,7 @@ class summary_checker_baset:public property_checkert { public: summary_checker_baset( - optionst &_options, - const ssa_heap_analysist &_heap_analysis): + optionst &_options): show_vcc(false), simplify(false), fixed_point(false), @@ -41,7 +39,6 @@ class summary_checker_baset:public property_checkert ssa_db(_options), summary_db(), ssa_unwinder(ssa_db), ssa_inliner(summary_db), - heap_analysis(_heap_analysis), solver_instances(0), solver_calls(0), summaries_used(0), @@ -69,8 +66,6 @@ class summary_checker_baset:public property_checkert ssa_unwindert ssa_unwinder; ssa_inlinert ssa_inliner; - const ssa_heap_analysist &heap_analysis; - unsigned solver_instances; unsigned solver_calls; unsigned summaries_used; @@ -84,8 +79,7 @@ class summary_checker_baset:public property_checkert void SSA_functions( const goto_modelt &, - const namespacet &ns, - const ssa_heap_analysist &heap_analysis); + const namespacet &ns); void summarize( const goto_modelt &, diff --git a/src/2ls/summary_checker_bmc.cpp b/src/2ls/summary_checker_bmc.cpp index 247abbb63..729193298 100644 --- a/src/2ls/summary_checker_bmc.cpp +++ b/src/2ls/summary_checker_bmc.cpp @@ -17,7 +17,7 @@ property_checkert::resultt summary_checker_bmct::operator()( { const namespacet ns(goto_model.symbol_table); - SSA_functions(goto_model, ns, heap_analysis); + SSA_functions(goto_model, ns); ssa_unwinder.init(false, true); diff --git a/src/2ls/summary_checker_bmc.h b/src/2ls/summary_checker_bmc.h index 0135adb85..52fdbc439 100644 --- a/src/2ls/summary_checker_bmc.h +++ b/src/2ls/summary_checker_bmc.h @@ -17,12 +17,8 @@ Author: Peter Schrammel class summary_checker_bmct:public summary_checker_baset { public: - summary_checker_bmct( - optionst &_options, - const ssa_heap_analysist &heap_analysis): - summary_checker_baset(_options, heap_analysis) - { - } + explicit summary_checker_bmct(optionst &_options): + summary_checker_baset(_options) {} virtual resultt operator()(const goto_modelt &); }; diff --git a/src/2ls/summary_checker_kind.cpp b/src/2ls/summary_checker_kind.cpp index 7942cfc3b..849ef173d 100644 --- a/src/2ls/summary_checker_kind.cpp +++ b/src/2ls/summary_checker_kind.cpp @@ -9,7 +9,6 @@ Author: Peter Schrammel /// \file /// Summary Checker for k-induction -#include #include "summary_checker_kind.h" property_checkert::resultt summary_checker_kindt::operator()( @@ -17,7 +16,7 @@ property_checkert::resultt summary_checker_kindt::operator()( { const namespacet ns(goto_model.symbol_table); - SSA_functions(goto_model, ns, heap_analysis); + SSA_functions(goto_model, ns); ssa_unwinder.init(true, false); diff --git a/src/2ls/summary_checker_kind.h b/src/2ls/summary_checker_kind.h index 373143dd0..ec3c5f8fc 100644 --- a/src/2ls/summary_checker_kind.h +++ b/src/2ls/summary_checker_kind.h @@ -17,12 +17,8 @@ Author: Peter Schrammel class summary_checker_kindt:public summary_checker_baset { public: - inline summary_checker_kindt( - optionst &_options, - const ssa_heap_analysist &heap_analysis): - summary_checker_baset(_options, heap_analysis) - { - } + explicit inline summary_checker_kindt(optionst &_options): + summary_checker_baset(_options) {} virtual resultt operator()(const goto_modelt &); }; diff --git a/src/2ls/summary_checker_nonterm.cpp b/src/2ls/summary_checker_nonterm.cpp index a58dfd203..f512aaf68 100644 --- a/src/2ls/summary_checker_nonterm.cpp +++ b/src/2ls/summary_checker_nonterm.cpp @@ -25,7 +25,7 @@ property_checkert::resultt summary_checker_nontermt::operator()( { const namespacet ns(goto_model.symbol_table); - SSA_functions(goto_model, ns, heap_analysis); + SSA_functions(goto_model, ns); ssa_unwinder.init(false, true); diff --git a/src/2ls/summary_checker_nonterm.h b/src/2ls/summary_checker_nonterm.h index 47abb8eab..21695dc32 100644 --- a/src/2ls/summary_checker_nonterm.h +++ b/src/2ls/summary_checker_nonterm.h @@ -17,10 +17,8 @@ Author: Stefan Marticek class summary_checker_nontermt:public summary_checker_baset { public: - explicit summary_checker_nontermt( - optionst &_options, - const ssa_heap_analysist &heap_analysis): - summary_checker_baset(_options, heap_analysis) + explicit summary_checker_nontermt(optionst &_options): + summary_checker_baset(_options) { } diff --git a/src/2ls/version.h b/src/2ls/version.h index 1e1d3b264..33c465402 100644 --- a/src/2ls/version.h +++ b/src/2ls/version.h @@ -12,6 +12,6 @@ Author: Peter Schrammel #ifndef CPROVER_2LS_2LS_VERSION_H #define CPROVER_2LS_2LS_VERSION_H -#define TWOLS_VERSION "0.8.2" +#define TWOLS_VERSION "0.9.0" #endif diff --git a/src/domains/Makefile b/src/domains/Makefile index 9d025b344..188d60c1a 100644 --- a/src/domains/Makefile +++ b/src/domains/Makefile @@ -1,7 +1,6 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ predabs_domain.cpp heap_domain.cpp list_iterator.cpp \ - heap_tpolyhedra_domain.cpp heap_tpolyhedra_sympath_domain.cpp \ - symbolic_path.cpp\ + sympath_domain.cpp \ symbolic_path.cpp\ ssa_analyzer.cpp util.cpp incremental_solver.cpp \ strategy_solver_binsearch.cpp \ strategy_solver_base.cpp \ @@ -9,10 +8,11 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ template_generator_base.cpp template_generator_summary.cpp \ template_generator_callingcontext.cpp template_generator_ranking.cpp \ strategy_solver_binsearch2.cpp strategy_solver_binsearch3.cpp \ - strategy_solver_heap_tpolyhedra.cpp \ - strategy_solver_heap_tpolyhedra_sympath.cpp \ - strategy_solver.cpp -#solver_enumeration.cpp + strategy_solver_sympath.cpp \ + simple_domain.cpp \ + strategy_solver_simple.cpp \ + product_domain.cpp \ + strategy_solver_product.cpp include ../config.inc include $(CPROVER_DIR)/src/config.inc diff --git a/src/domains/domain.cpp b/src/domains/domain.cpp index b28d13a45..ae22acacd 100644 --- a/src/domains/domain.cpp +++ b/src/domains/domain.cpp @@ -10,73 +10,82 @@ Author: Peter Schrammel /// Abstract domain base class #include "domain.h" +#include "util.h" -domaint::kindt domaint::merge_kinds(kindt k1, kindt k2) +/// Abstract value join - not used by most of the domains since the join +/// is typically done between an abstract value and a model of satisfiability +/// in the strategy solver (see method edit_row). +void domaint::join(domaint::valuet &value1, const domaint::valuet &value2) { - return - (k1==OUT || k2==OUT ? (k1==LOOP || k2==LOOP ? OUTL : OUT) : - (k1==LOOP || k2==LOOP ? LOOP : IN)); + bool other_bottom= + value1.basic_value==valuet::OTHER && + value2.basic_value==valuet::BOTTOM; + if(value1.basic_value==value2.basic_value || + value1.basic_value==valuet::TOP || + other_bottom) + return; + value1.basic_value=value2.basic_value; } -void domaint::output_var_specs( - std::ostream &out, - const var_specst &var_specs, - const namespacet &ns) +/// Print information about guards to the given output stream. +void guardst::output(std::ostream &out, const namespacet &ns) const { - for(const auto &v : var_specs) + switch(kind) { - switch(v.kind) - { - case LOOP: - out << "(LOOP) [ " << from_expr(ns, "", v.pre_guard) << " | "; - out << from_expr(ns, "", v.post_guard) << " ]: "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", v.pre_guard) << ": "; - break; - case OUT: case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", v.post_guard) << ": "; - break; - default: assert(false); - } - out << from_expr(ns, "", v.var) << std::endl; + case LOOP: + out << "(LOOP) [ " << from_expr(ns, "", pre_guard) << " | "; + out << from_expr(ns, "", post_guard) << " | "; + out << from_expr(ns, "", aux_expr) + << " ] ===> " << std::endl << " "; + break; + case IN: + out << "(IN) "; + out << from_expr(ns, "", pre_guard) << " ===> " + << std::endl << " "; + break; + case OUT: + case OUTL: + out << "(OUT) "; + out << from_expr(ns, "", post_guard) << " ===> " + << std::endl << " "; + break; + default: + assert(false); } } -const exprt domaint::initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) -{ - return true_exprt(); -} - -void domaint::solver_iter_init(valuet &value) -{ -} - -bool domaint::has_something_to_solve() +/// Merge two guardst objects into one by conjunction of the guards +guardst guardst::merge_and_guards( + const guardst &g1, + const guardst &g2, + const namespacet &ns) { - return true; -} + guardst result; + // Merge kinds + const kindt k1=g1.kind; + const kindt k2=g2.kind; + result.kind=(k1==OUT || k2==OUT ? (k1==LOOP || k2==LOOP ? OUTL : OUT) : + (k1==LOOP || k2==LOOP ? LOOP : IN)); -exprt domaint::get_current_loop_guard(size_t row) -{ - return true_exprt(); -} + // Merge guards using conjunction + merge_and(result.pre_guard, g1.pre_guard, g2.pre_guard, ns); + merge_and(result.post_guard, g1.post_guard, g2.post_guard, ns); + merge_and(result.aux_expr, g1.aux_expr, g2.aux_expr, ns); -bool domaint::handle_unsat(valuet &value, bool improved) -{ - return improved; + return result; } -void domaint::post_edit() +/// Print information about a variable specification to the given output stream +void var_spect::output(std::ostream &out, const namespacet &ns) const { + guards.output(out, ns); + out << from_expr(ns, "", var) << std::endl; } -exprt domaint::make_permanent(valuet &value) +/// Print information about a vector of variable specifications to the given +/// output stream. +void var_specst::output(std::ostream &out, const namespacet &ns) const { - return true_exprt(); + for(auto &var_spec : (*this)) + var_spec.output(out, ns); } diff --git a/src/domains/domain.h b/src/domains/domain.h index a1f90e0b8..c7ffbfca1 100644 --- a/src/domains/domain.h +++ b/src/domains/domain.h @@ -21,11 +21,56 @@ Author: Peter Schrammel #include #include #include +#include +#include "symbolic_path.h" +#include "incremental_solver.h" // Forward declaration - real is in template_generator_base.h class template_generator_baset; +class strategy_solver_baset; + class local_SSAt; +/// Guards specification +struct guardst +{ + typedef exprt guardt; + typedef enum { LOOP, IN, OUT, OUTL } kindt; + + kindt kind; + guardt pre_guard; + guardt post_guard; + exprt aux_expr; + + void output(std::ostream &out, const namespacet &ns) const; + /// Merge two guardst objects into one by conjunction of the guards + static guardst merge_and_guards( + const guardst &g1, + const guardst &g2, + const namespacet &ns); +}; + +typedef exprt vart; +typedef std::vector var_listt; +typedef std::set var_sett; + +/// Variable specification +/// Contains a variable (exprt) and guards. +struct var_spect +{ + vart var; + guardst guards; + + void output(std::ostream &out, const namespacet &ns) const; +}; + +/// Vector of variable specifications. +/// Implements printing method. +struct var_specst:std::vector +{ + void output(std::ostream &out, const namespacet &ns) const; +}; + class domaint { public: @@ -39,269 +84,89 @@ class domaint { } - virtual ~domaint() - { - } - - typedef exprt vart; - typedef std::vector var_listt; - typedef std::set var_sett; - - typedef enum {LOOP, IN, OUT, OUTL, OUTHEAP} kindt; - - typedef exprt guardt; - typedef unsigned rowt; - - typedef struct - { - guardt pre_guard; - guardt post_guard; - vart var; - exprt aux_expr; // some auxiliary per-variable constraint - kindt kind; - } var_spect; - - typedef std::vector var_specst; - - // handles on values to retrieve from model - bvt strategy_cond_literals; - exprt::operandst strategy_value_exprs; - + virtual ~domaint()=default; + /// Base class for abstract value. Contains only the basic value, the rest is + /// defined per-domain. class valuet { public: - typedef enum {TOP, BOTTOM, OTHER} basic_valuet; - valuet():basic_value(OTHER) {} - virtual ~valuet() {} - - basic_valuet basic_value; - }; + typedef enum { TOP, BOTTOM, OTHER } basic_valuet; - virtual void initialize(valuet &value) { value.basic_value=valuet::BOTTOM; } - - /*******************************************************************\ - - Function: domaint:: + valuet():basic_value(OTHER) {} - Inputs: + virtual ~valuet() {} - Outputs: + /// Each abstract value needs to implement clone with covariant return type. + /// This is needed to properly clone abstract value when only a pointer to + /// valuet is available. + /// Since the method returns a raw pointer, the caller is responsible for + /// taking ownership of the created object. + virtual valuet *clone()=0; - Purpose: Initialize SMT solver when new strategy solver is created. - Returned value is written into SMT solver. + basic_valuet basic_value; + }; - \*******************************************************************/ - virtual const exprt initialize_solver( + /// Create a new empty abstract value for the domain + virtual std::unique_ptr new_value()=0; + /// Create a new strategy solver for the domain + virtual std::unique_ptr new_strategy_solver( + incremental_solvert &solver, const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Initialize strategy solver at beginning of each iteration. - - \*******************************************************************/ - virtual void solver_iter_init(valuet &value); - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Domain should return true if wants to improve its invariants. - Otherwise no further improvements of invariants is done. - - \*******************************************************************/ - virtual bool has_something_to_solve(); - - /*******************************************************************\ - - Function: domaint::get_current_loop_guard - - Inputs: - - Outputs: - - Purpose: Return current loop guard. - - \*******************************************************************/ - - virtual exprt get_current_loop_guard(size_t row); - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: + message_handlert &message_handler)=0; - Purpose: Edit invariant based on current model of satisfiability + // General methods for the strategy solver + // Each generic strategy solver should implement at least these. - \*******************************************************************/ - - virtual bool edit_row(const rowt &row, valuet &inv, bool improved)=0; - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: After each iteration of strategy solver it is possible to write - expression into SMT solver, which stay present in further - iterations. - - \*******************************************************************/ - virtual exprt make_permanent(valuet &value); - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Finalize domain - last step of each iteration of strategy solver. - - \*******************************************************************/ - virtual void post_edit(); - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Create entry constraints as a conjuction of entry expressions - for each template row. - - \*******************************************************************/ - /* - */ - virtual exprt to_pre_constraints(valuet &value)=0; - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Create exit constraints for each value row. Each expression is - a negation of a row expression - (for solving the "exists forall" problem) - - \*******************************************************************/ - virtual void make_not_post_constraints( - valuet &value, - exprt::operandst &cond_exprs)=0; - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Required values from SMT solver - - \*******************************************************************/ - virtual std::vector get_required_smt_values(size_t row)=0; - - /*******************************************************************\ - - Function: domaint:: - - Inputs: - - Outputs: - - Purpose: Domain can save vales from SMT solver (required by - get_required_smt_values) into internal representation - - \*******************************************************************/ - virtual void set_smt_values(std::vector got_values, size_t row)=0; - - /*******************************************************************\ - - Function: domaint:: - - Inputs: + /// Initialize an abstract value. + /// The derived class is expected to override this. + virtual void initialize_value(valuet &value) + { + value.basic_value=valuet::BOTTOM; + } - Outputs: + /// Initialize domain at the beginning of strategy solving + virtual void initialize() {} - Purpose: Method called when model is unsatisfiable + /// Initialize value at the beginning of strategy solver iteration + virtual void init_value_solver_iteration(valuet &value) {} - \*******************************************************************/ - virtual bool handle_unsat(valuet &value, bool improved); + /// Finalize the domain after a single iteration of strategy solving. + virtual void finalize_solver_iteration() {} - // returns true as long as further refinements are possible - virtual void reset_refinements() { } - virtual bool refine() { return false; } + /// Abstract value join - not used by most of the domains since the join + /// is typically done between an abstract value and a model of satisfiability + /// in the strategy solver (see method edit_row). + virtual void join(valuet &value1, const valuet &value2); - virtual void join(valuet &value1, const valuet &value2) - { - bool other_bottom= - value1.basic_value==valuet::OTHER && - value2.basic_value==valuet::BOTTOM; - if(value1.basic_value==value2.basic_value || - value1.basic_value==valuet::TOP || - other_bottom) - return; - value1.basic_value=value2.basic_value; - } + /// Output the domain (its template) + virtual void output_domain(std::ostream &out, const namespacet &ns) const=0; + /// Output the given abstract value in this domain. virtual void output_value( std::ostream &out, const valuet &value, - const namespacet &ns) const - { - assert(false); - } - - virtual void output_domain( - std::ostream &out, - const namespacet &ns) const - { - assert(false); - } + const namespacet &ns) const=0; + /// Project invariant (abstract value) onto a set of variables. + /// If vars is empty, project onto all variables (get the entire invariant). // (not useful to make value const (e.g. union-find)) virtual void project_on_vars( valuet &value, const var_sett &vars, - exprt &result) - { - if(value.basic_value==valuet::BOTTOM) - result=false_exprt(); - else - result=true_exprt(); - } - - static kindt merge_kinds(kindt k1, kindt k2); - - static void output_var_specs( - std::ostream &out, - const var_specst &var_specs, - const namespacet &ns); + exprt &result)=0; + + // Methods related to symbolic paths + + /// Restrict the template to the given symbolic path. + virtual void restrict_to_sympath(const symbolic_patht &sympath)=0; + /// Restrict template to any other paths than those specified. + virtual void eliminate_sympaths( + const std::vector &sympaths)=0; + /// Undo the last symbolic path restriction + virtual void undo_sympath_restriction()=0; + /// Remove all symbolic path restrictions. + virtual void remove_all_sympath_restrictions()=0; protected: unsigned domain_number; // serves as id for variables names diff --git a/src/domains/equality_domain.cpp b/src/domains/equality_domain.cpp index 2cd510da9..c01d7bd68 100644 --- a/src/domains/equality_domain.cpp +++ b/src/domains/equality_domain.cpp @@ -22,14 +22,22 @@ Author: Peter Schrammel #include "equality_domain.h" #include "util.h" -void equality_domaint::initialize(valuet &value) +exprt equality_domaint::equ_valuet::get_row_expr( + rowt row, + const simple_domaint::template_rowt &templ_row) const { - equ_valuet &v=static_cast(value); + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + return equal_exprt(templ_row_expr.first, templ_row_expr.second); +} + +void equality_domaint::initialize_value(domaint::valuet &value) +{ + auto &v=dynamic_cast(value); v.equs.clear(); v.disequs.clear(); } -void equality_domaint::solver_iter_init(valuet &value) +void equality_domaint::init_value_solver_iteration(domaint::valuet &value) { e_it=todo_equs.begin(); unsatisfiable=false; @@ -51,17 +59,6 @@ bool equality_domaint::has_something_to_solve() return false; } -std::vector equality_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - return r; -} - -void equality_domaint::set_smt_values(std::vector got_values, size_t row) -{ - todo_disequs.insert(*e_it); -} - bool equality_domaint::edit_row(const rowt &row, valuet &inv, bool improved) { if(!check_dis) @@ -69,7 +66,7 @@ bool equality_domaint::edit_row(const rowt &row, valuet &inv, bool improved) return true; } -void equality_domaint::post_edit() +void equality_domaint::finalize_solver_iteration() { if(check_dis) todo_disequs.erase(e_it); @@ -77,93 +74,44 @@ void equality_domaint::post_edit() todo_equs.erase(e_it); } -exprt equality_domaint::to_pre_constraints(valuet &_value) +exprt equality_domaint::to_pre_constraints(const valuet &value) { - if(check_dis) - return get_pre_disequ_constraint(*e_it); - assert(*e_it(value); + auto &inv=dynamic_cast(value); if(check_dis) set_disequal(*e_it, inv); unsatisfiable=true; return true; } -exprt equality_domaint::make_permanent(valuet &value) +exprt equality_domaint::get_permanent_expr(valuet &value) { - equality_domaint::equ_valuet &inv= - static_cast(value); + auto &inv=dynamic_cast(value); if(unsatisfiable) { if(!check_dis) @@ -180,39 +128,8 @@ exprt equality_domaint::make_permanent(valuet &value) return true_exprt(); } -exprt equality_domaint::get_pre_disequ_constraint(unsigned index) -{ - assert(index(value); + auto &v=dynamic_cast(value); exprt::operandst c; - for(unsigned index=0; index(*templ[row].expr); #if 0 std::cout << vv.second << std::endl; #endif - if(vars.find(vv.first)==vars.end() || - (vars.find(vv.second)==vars.end() && - !(vv.second.id()==ID_constant && - to_constant_expr(vv.second).get_value()=="NULL"))) + if(vars.find(templ_row_expr.first)==vars.end() || + (vars.find(templ_row_expr.second)==vars.end() && + !(templ_row_expr.second.id()==ID_constant && + to_constant_expr(templ_row_expr.second).get_value()=="NULL"))) continue; - if(v.equs.same_set(vv.first, vv.second)) + if(v.equs.same_set(templ_row_expr.first, templ_row_expr.second)) { - if(templ[index].kind==LOOP) - c.push_back( - implies_exprt( - templ[index].pre_guard, - equal_exprt(vv.first, vv.second))); + check_dis=false; + if(templ[row].guards.kind==guardst::LOOP) + c.push_back(get_row_pre_constraint(row, v)); else - c.push_back(equal_exprt(vv.first, vv.second)); + c.push_back(get_row_value_constraint(row, v)); } } - for(index_sett::const_iterator it=v.disequs.begin(); - it!=v.disequs.end(); it++) + for(auto &disequ : v.disequs) { - const var_pairt &vv=templ[*it].var_pair; + auto &templ_row_expr= + dynamic_cast(*templ[disequ].expr); - if(vars.find(vv.first)==vars.end() || - (vars.find(vv.second)==vars.end() && - !(vv.second.id()==ID_constant && - to_constant_expr(vv.second).get_value()=="NULL"))) + if(vars.find(templ_row_expr.first)==vars.end() || + (vars.find(templ_row_expr.second)==vars.end() && + !(templ_row_expr.second.id()==ID_constant && + to_constant_expr(templ_row_expr.second).get_value()=="NULL"))) continue; - if(templ[*it].kind==LOOP) - c.push_back( - implies_exprt( - templ[*it].pre_guard, - notequal_exprt(vv.first, vv.second))); + check_dis=true; + if(templ[disequ].guards.kind==guardst::LOOP) + c.push_back(get_row_pre_constraint(disequ, v)); else - c.push_back(notequal_exprt(vv.first, vv.second)); + c.push_back(get_row_value_constraint(disequ, v)); } result=conjunction(c); } @@ -275,81 +188,41 @@ void equality_domaint::set_equal( unsigned index, equ_valuet &value) { assert(index(*templ[index].expr); + value.set_equal(templ_row_expr.first, templ_row_expr.second); } void equality_domaint::set_disequal( unsigned index, equ_valuet &value) { assert(index(value); + auto &_v=dynamic_cast(value); equ_valuet v=_v; for(unsigned index=0; index(*templ[index].expr); + if(v.equs.same_set(templ_row_expr.first, templ_row_expr.second)) { - out << from_expr(ns, "", vv.first) << "==" - << from_expr(ns, "", vv.second) << std::endl; + out << from_expr(ns, "", templ_row_expr.first) << "==" + << from_expr(ns, "", templ_row_expr.second) << std::endl; } } for(index_sett::const_iterator it=v.disequs.begin(); it!=v.disequs.end(); it++) { - const var_pairt &vv=templ[*it].var_pair; - out << from_expr(ns, "", vv.first) << "!=" - << from_expr(ns, "", vv.second) << std::endl; - } -} - -void equality_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - for(unsigned index=0; index " << std::endl << " "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", templ_row.pre_guard) << "===> " - << std::endl << " "; - break; - case OUT: case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", templ_row.post_guard) << "===> " - << std::endl << " "; - break; - default: assert(false); - } - const var_pairt &vv=templ_row.var_pair; - out << from_expr(ns, "", vv.first) << "=!= " - << from_expr(ns, "", vv.second) << std::endl; + auto &templ_row_expr=dynamic_cast(*templ[*it].expr); + out << from_expr(ns, "", templ_row_expr.first) << "!=" + << from_expr(ns, "", templ_row_expr.second) << std::endl; } } @@ -432,18 +305,16 @@ void equality_domaint::make_template( { templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.var_pair= - var_pairt(v1->var, null_pointer_exprt(to_pointer_type(v1->var.type()))); - templ_row.pre_guard=v1->pre_guard; - templ_row.post_guard=v1->post_guard; - templ_row.aux_expr=v1->aux_expr; - templ_row.kind=v1->kind; + templ_row.expr=std::unique_ptr( + new template_row_exprt( + v1->var, null_pointer_exprt(to_pointer_type(v1->var.type())))); + templ_row.guards=v1->guards; } var_specst::const_iterator v2=v1; v2++; for(; v2!=var_specs.end(); v2++) { - kindt k=domaint::merge_kinds(v1->kind, v2->kind); + guardst guards=guardst::merge_and_guards(v1->guards, v2->guards, ns); #if 0 // TODO: must be done in caller (for preconditions, e.g.) @@ -451,11 +322,6 @@ void equality_domaint::make_template( continue; #endif - exprt pre_g, post_g, aux_expr; - merge_and(pre_g, v1->pre_guard, v2->pre_guard, ns); - merge_and(post_g, v1->post_guard, v2->post_guard, ns); - merge_and(aux_expr, v1->aux_expr, v2->aux_expr, ns); - exprt vv1=v1->var; exprt vv2=v2->var; if(!adapt_types(vv1, vv2)) @@ -463,22 +329,16 @@ void equality_domaint::make_template( templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.var_pair=var_pairt(vv1, vv2); - templ_row.pre_guard=pre_g; - templ_row.post_guard=post_g; - templ_row.aux_expr=aux_expr; - templ_row.kind=k; + templ_row.expr=std::unique_ptr( + new template_row_exprt(vv1, vv2)); + templ_row.guards=guards; } } } -const exprt equality_domaint::initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) +void equality_domaint::initialize() { get_index_set(todo_equs); - return true_exprt(); } void equality_domaint::get_index_set(std::set &indices) @@ -486,3 +346,11 @@ void equality_domaint::get_index_set(std::set &indices) for(unsigned i=0; i #include -#include "domain.h" +#include "simple_domain.h" -class equality_domaint:public domaint +class equality_domaint:public simple_domaint { public: - typedef std::pair var_pairt; - typedef std::set var_pairst; typedef std::set index_sett; -equality_domaint( - unsigned _domain_number, - replace_mapt &_renaming_map, - const var_specst &var_specs, - const namespacet &ns): - domaint(_domain_number, _renaming_map, ns) + equality_domaint( + unsigned _domain_number, + replace_mapt &_renaming_map, + const var_specst &var_specs, + const namespacet &ns): + simple_domaint(_domain_number, _renaming_map, ns) { make_template(var_specs, ns); } - class equ_valuet:public valuet + struct template_row_exprt:simple_domaint::template_row_exprt { - public: - union_find equs; - index_sett disequs; + vart first; + vart second; + + template_row_exprt(const vart &first, const vart &second): + first(first), second(second) {} + + std::vector get_row_exprs() override { return {}; }; + void output(std::ostream &out, const namespacet &ns) const override; }; - typedef struct + struct equ_valuet:simple_domaint::valuet { - guardt pre_guard; - guardt post_guard; - equality_domaint::var_pairt var_pair; - exprt aux_expr; - kindt kind; - } template_rowt; + union_find equs; + index_sett disequs; - typedef std::vector templatet; + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override; - const exprt initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); + void set_equal(const vart &first, const vart &second) + { + equs.make_union(first, second); + } - virtual void initialize(valuet &value); + void set_disequal(unsigned index) { disequs.insert(index); } - virtual void solver_iter_init(valuet &value); + equ_valuet *clone() override { return new equ_valuet(*this); } + }; - virtual bool has_something_to_solve(); + std::unique_ptr new_value() override + { + return std::unique_ptr(new equ_valuet()); + } + + void initialize() override; + + void initialize_value(domaint::valuet &value) override; - bool edit_row(const rowt &row, valuet &inv, bool improved); + void init_value_solver_iteration(domaint::valuet &value) override; - void post_edit(); + bool has_something_to_solve() override; - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); + bool edit_row(const rowt &row, valuet &inv, bool improved) override; - exprt to_pre_constraints(valuet &_value); + void finalize_solver_iteration() override; + + exprt to_pre_constraints(const valuet &_value) override; void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); + const valuet &_value, + exprt::operandst &cond_exprs) override; - bool handle_unsat(valuet &value, bool improved); - exprt make_permanent(valuet &value); + exprt get_row_value_constraint( + rowt row, + const simple_domaint::valuet &value) override; - exprt get_pre_equ_constraint(unsigned index); - exprt get_post_not_equ_constraint(unsigned index); - exprt get_pre_disequ_constraint(unsigned index); - exprt get_post_not_disequ_constraint(unsigned index); + bool handle_unsat(valuet &value, bool improved) override; + exprt get_permanent_expr(valuet &value) override; void set_equal(unsigned index, equ_valuet &value); void set_disequal(unsigned index, equ_valuet &value); - virtual void output_value( + void output_value( std::ostream &out, - const valuet &value, - const namespacet &ns) const; - - virtual void output_domain(std::ostream &out, const namespacet &ns) const; + const domaint::valuet &value, + const namespacet &ns) const override; - virtual void project_on_vars( - valuet &value, + void project_on_vars( + domaint::valuet &value, const var_sett &vars, - exprt &result); + exprt &result) override; void get_index_set(index_sett &indices); - const var_pairt &get_var_pair(unsigned index); protected: - templatet templ; - exprt value; - void make_template( const var_specst &var_specs, const namespacet &ns); @@ -118,8 +119,8 @@ equality_domaint( worklistt::iterator e_it; worklistt todo_equs; worklistt todo_disequs; - bool check_dis; - bool unsatisfiable; + bool check_dis=false; + bool unsatisfiable=false; }; #endif // CPROVER_2LS_DOMAINS_EQUALITY_DOMAIN_H diff --git a/src/domains/heap_domain.cpp b/src/domains/heap_domain.cpp index f43b38c78..7895ae004 100644 --- a/src/domains/heap_domain.cpp +++ b/src/domains/heap_domain.cpp @@ -11,34 +11,22 @@ Author: Viktor Malik #include "heap_domain.h" #include +#include #include /// Initialize abstract value. Clears value with empty value rows corresponding /// to template. -void heap_domaint::initialize(domaint::valuet &value) +void heap_domaint::initialize_value(domaint::valuet &value) { - heap_valuet &val=static_cast(value); - - for(const template_rowt &templ_row : templ) - { - if(templ_row.mem_kind==STACK) - val.emplace_back(new stack_row_valuet(ns)); - else if(templ_row.mem_kind==HEAP) - val.emplace_back( - new heap_row_valuet( - ns, - std::make_pair( - templ_row.dyn_obj, - templ_row.expr))); - else - assert(false); - } + auto &heap_val=dynamic_cast(value); + for(int i=0; i heap_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - if(strategy_value_exprs[row].id()==ID_and) - { - r.push_back(strategy_value_exprs[row].op0()); - r.push_back(strategy_value_exprs[row].op1()); - } - else - { - r.push_back(strategy_value_exprs[row]); - } - return r; -} - -void heap_domaint::set_smt_values(std::vector got_values, size_t row) -{ - solver_value_op0=got_values[0]; - if(strategy_value_exprs[row].id()==ID_and) - { - solver_value_op1=got_values[1]; - } -} - - /// Add a template row. -/// \param var_spec: Variable specification -/// \param pointed_type: Pointed type +/// \param guards: Variable specification +/// \param pointers: Pointed type void heap_domaint::add_template_row( - const var_spect &var_spec, - const typet &pointed_type) -{ - const vart &var=var_spec.var; - - templ.push_back(template_rowt()); - template_rowt &templ_row=templ.back(); - templ_row.expr=var; - templ_row.pre_guard=var_spec.pre_guard; - templ_row.post_guard=var_spec.post_guard; - templ_row.aux_expr=var_spec.aux_expr; - templ_row.kind=var_spec.kind; - - templ_row.mem_kind=STACK; - if(pointed_type.id()==ID_struct) - { - // Check if var is member field of heap object - const std::string identifier=id2string( - to_symbol_expr(var_spec.var).get_identifier()); - for(auto &component : to_struct_type(pointed_type).components()) - { - if(identifier.find("."+id2string(component.get_name()))!= - std::string::npos) - { -#if 0 - // It has shown that using stack rows only is sufficient to prove all - // tested programs and it seems that pointer access paths are not - // necessary. Therefore, we currently disable this code. - templ_row.mem_kind=HEAP; -#endif - templ_row.member=component.get_name(); - - std::string var_id=id2string(to_symbol_expr(var).get_identifier()); - std::string do_id=var_id.substr(0, var_id.find_last_of('.')); - templ_row.dyn_obj=symbol_exprt(do_id, var.type().subtype()); - } - } - } -} - -/// Add a template row with a pair of variables as expression. -/// \param var_spec1: First variable specification -/// \param var_spec2: Second variable specification -/// \param pointed_type: Pointed type -void heap_domaint::add_template_row_pair( - const domaint::var_spect &var_spec1, - const domaint::var_spect &var_spec2, - const typet &pointed_type) + var_listt pointers, + const guardst &guards) { - const exprt var_pair=and_exprt(var_spec1.var, var_spec2.var); - templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.expr=var_pair; - templ_row.pre_guard=var_spec1.pre_guard; - templ_row.post_guard=var_spec1.post_guard; - templ_row.aux_expr=var_spec1.aux_expr; - templ_row.kind=var_spec1.kind; - - templ_row.mem_kind=STACK; -} - -/// Create entry constraints as a conjuction of entry expressions for each -/// template row. -/// \return Entry constraints expression for a value. -exprt heap_domaint::to_pre_constraints(valuet &_value) -{ - heap_domaint::heap_valuet &value= - static_cast(_value); - assert(value.size()==templ.size()); - exprt::operandst c; - for(rowt row=0; row(_value); - assert(value.size()==templ.size()); - cond_exprs.resize(templ.size()); - strategy_value_exprs.resize(templ.size()); - - for(rowt row=0; row(value[from]); - heap_row_valuet &heap_val_to=static_cast(value[to]); - - bool result=false; - if(heap_val_from.add_all_paths( - heap_val_to, - std::make_pair(templ[to].dyn_obj, templ[to].expr))) - { - result=true; - } - if(from!=to) - { - if(heap_val_to.add_pointed_by(from)) - result=true; - } - - return result; -} - -/// Add new object pointed by a row. Calls add_points_to of the given row. For -/// stack rows, the destination is simply added into pointed objects set. For -/// heap rows, a new path is added. -bool heap_domaint::add_points_to( - const rowt &row, - heap_valuet &value, - const exprt &dest) -{ - assert(row(value); - for(rowt row=0; row " << std::endl - << " "; - break; - case IN: - out << "(IN) "; - break; - case OUT: - case OUTL: - out << "(OUT) "; - break; - case OUTHEAP: - out << "(HEAP) "; - break; - default: - assert(false); - } - out << "( " << from_expr(ns, "", templ_row.expr) << " == " - << from_expr(ns, "", val[row].get_row_expr(templ_row.expr, false)) - << " )" - << std::endl; - } -} - -void heap_domaint::output_domain(std::ostream &out, const namespacet &ns) const -{ - for(unsigned i=0; i " << std::endl << " "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", templ_row.pre_guard) << " ===> " - << std::endl << " "; - break; - case OUT: - case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", templ_row.post_guard) << " ===> " - << std::endl << " "; - break; - case OUTHEAP: - out << "(HEAP) [ " << from_expr(ns, "", templ_row.pre_guard) << " | "; - out << from_expr(ns, "", templ_row.post_guard) - << " ] ===> " << std::endl << " "; - break; - default: - assert(false); - } - const vart &var=templ_row.expr; - - const std::string info= - templ_row.mem_kind==STACK - ? " --points_to--> Locations" - : " --paths--> Destinations"; - out << i << ": " << from_expr(ns, "", var) << info << std::endl; - } -} - -void heap_domaint::project_on_vars( - domaint::valuet &value, - const domaint::var_sett &vars, - exprt &result) -{ - const heap_valuet &val=static_cast(value); - assert(val.size()==templ.size()); - - exprt::operandst c; - for(rowt row=0; row( + new template_row_exprt(std::move(pointers))); + templ_row.guards=guards; } /// Converts a constant returned from the solver to the corresponding @@ -444,29 +106,6 @@ exprt heap_domaint::value_to_ptr_exprt(const exprt &expr) return expr; } -/// Not used. -void heap_domaint::join(domaint::valuet &value1, const domaint::valuet &value2) -{ - heap_valuet &val1=static_cast(value1); - const heap_valuet &val2=static_cast(value2); - assert(val1.size()==templ.size()); - assert(val2.size()==val1.size()); -} - -/// Get location number of a given symbol. -/// \param expr: Symbol expression. -/// \return Number of location, or -1 if symbol is input. -int heap_domaint::get_symbol_loc(const exprt &expr) -{ - assert(expr.id()==ID_symbol); - std::string expr_id=id2string(to_symbol_expr(expr).get_identifier()); - if(expr_id.find('#')==std::string::npos) - return -1; - std::string loc_str=expr_id.substr(expr_id.find_last_not_of("0123456789")+1); - assert(!loc_str.empty()); - return std::stoi(loc_str); -} - /// \param ptr_expr: Pointer expression (variable) /// \param ptr_value: Value (object or address) of the pointer /// \return Equality between pointer and its value with correct types @@ -489,944 +128,84 @@ const exprt ptr_equality( return equal_exprt(ptr_expr, value); } -/// Stack row is a disjuction of equalities between templ_expr and addresses of -/// dynamic objects from points_to set. -/// \param templ_expr: Template expression +/// Row value is a disjuction of equalities between templ_expr and addresses of +/// dynamic objects from the points_to set. +/// \param templ_row_expr: Template expression /// \param rename_templ_expr: Unused /// \return Formula corresponding to the template row -exprt heap_domaint::stack_row_valuet::get_row_expr( - const vart &templ_expr, - bool rename_templ_expr) const +exprt heap_domaint::row_valuet::get_row_expr( + const template_row_exprt &templ_row_expr) const { if(nondet) return true_exprt(); - - if(empty()) + if(may_point_to.empty()) return false_exprt(); - else - { - // Points to expression - exprt::operandst result; - for(const exprt &pt : points_to) - { - if(templ_expr.id()==ID_and) - { - result.push_back( - and_exprt( - ptr_equality(templ_expr.op0(), pt.op0(), ns), - ptr_equality(templ_expr.op1(), pt.op1(), ns))); - } - else - result.push_back(ptr_equality(templ_expr, pt, ns)); - } - return disjunction(result); - } -} - -/// Add new object to the value of a row. The object is simply added to the set. -bool heap_domaint::stack_row_valuet::add_points_to(const exprt &expr) -{ - if(points_to.find(expr)==points_to.end()) - points_to.insert(expr); - else - nondet=true; - return true; -} - -/// Clear stack row value -void heap_domaint::stack_row_valuet::clear() -{ - nondet=false; - points_to.clear(); -} - -/// Heap row is a conjunction of paths: -/// nondet is TRUE -/// empty is FALSE -/// \param templ_expr: Template expression -/// \param rename_templ_expr: True if templ_expr should be renamed -/// (the corresponding template row is of OUTHEAP type) -/// \return Formula corresponding to the template row -exprt heap_domaint::heap_row_valuet::get_row_expr( - const vart &templ_expr_, - bool rename_templ_expr) const -{ - if(nondet) - return true_exprt(); - - exprt templ_expr=templ_expr_; - if(rename_templ_expr) - templ_expr=rename_outheap(to_symbol_expr(templ_expr_)); - - if(paths.empty()) - { - if(self_linkage) - { - return equal_exprt(templ_expr, address_of_exprt(dyn_obj.first)); - } - else - return false_exprt(); - } - else - { - exprt::operandst result; - for(const patht &path : paths) - { // path(o.m, d)[O] - const exprt &dest=templ_expr.type()==path.destination.type() ? - path.destination : address_of_exprt(path.destination); - exprt::operandst path_expr; - - // o.m = d - path_expr.push_back(equal_exprt(templ_expr, dest)); - - for(const dyn_objt &obj1 : path.dyn_objects) - { - // o.m = &o' - exprt equ_exprt=equal_exprt(templ_expr, address_of_exprt(obj1.first)); - - exprt::operandst steps_expr; - exprt member_expr=obj1.second; - // o'.m = d - steps_expr.push_back(equal_exprt(member_expr, dest)); - - for(const dyn_objt &obj2 : path.dyn_objects) - { - // o'.m = o'' - steps_expr.push_back( - equal_exprt( - member_expr, - address_of_exprt(obj2.first))); - } - - path_expr.push_back(and_exprt(equ_exprt, disjunction(steps_expr))); - } - - result.push_back(disjunction(path_expr)); - } - return conjunction(result); - } -} - -/// Add new object to the heap row - create new path or set self_linkage flag in -/// case the object is same as the row object. -bool heap_domaint::heap_row_valuet::add_points_to(const exprt &dest) -{ - if(dest==dyn_obj.first) - { - if(!add_self_linkage()) - nondet=true; - } - else - { - const dyn_objt through= - self_linkage ? dyn_obj : std::make_pair(nil_exprt(), nil_exprt()); - if(!add_path(dest, through)) - nondet=true; - } - return true; -} - -/// Add new path to the heap row -/// \param dest: Path destination -/// \param dyn_obj: Dynamic object that the path goes through -/// \return True if the value was changed (a path was added) -bool heap_domaint::heap_row_valuet::add_path( - const exprt &dest, - const dyn_objt &dyn_obj) -{ - if(paths.find(dest)==paths.end()) - { - // Path does not exist yet - std::set dyn_obj_set; - if(dyn_obj.first.id()!=ID_nil) - { // Path doesn't have zero length - dyn_obj_set.insert(dyn_obj); - } - if(self_linkage) - { - dyn_obj_set.insert(this->dyn_obj); - } - paths.emplace(dest, dyn_obj_set); - return true; - } - else - { - // Path exists already - if(dyn_obj.first.id()!=ID_nil) - // Try to insert new dynamic object on the path - return paths.find(dest)->dyn_objects.insert(dyn_obj).second; - else - return false; - } -} - -/// Add all paths from other heap row. -/// \return True if this has changed -bool heap_domaint::heap_row_valuet::add_all_paths( - const heap_row_valuet &other_val, - const dyn_objt &dyn_obj) -{ - bool result=false; - for(auto &path : other_val.paths) - { - bool new_dest=(paths.find(path.destination)==paths.end()); - if(add_path(path.destination, dyn_obj)) - { - if(!new_dest) - paths.erase(dyn_obj.first); - result=true; - for(auto &o : path.dyn_objects) - { - if(add_path(path.destination, o)) - result=true; - } - } - } - return result; -} - -bool heap_domaint::heap_row_valuet::add_pointed_by(const rowt &row) -{ - auto new_pb=pointed_by.insert(row); - return new_pb.second; -} - -bool heap_domaint::heap_row_valuet::add_self_linkage() -{ - bool result; - result=!self_linkage; - self_linkage=true; - if(result) - { - for(const patht &path : paths) - { - path.dyn_objects.insert(dyn_obj); - } - } - return result; -} - -/// Rename OUTHEAP row expression (used for post-expr). Simply remove 'lb' from -/// suffix. -/// \param expr: Expression to be renamed -/// \return Renamed expression -exprt heap_domaint::heap_row_valuet::rename_outheap(const symbol_exprt &expr) -{ - const std::string id=id2string(expr.get_identifier()); - return symbol_exprt( - id.substr(0, id.rfind("lb"))+id.substr(id.rfind("lb")+2), - expr.type()); -} - -/// \return Clear heap row value -void heap_domaint::heap_row_valuet::clear() -{ - nondet=false; - paths.clear(); -} - -/// \return List of variables (symbols) that were added to template during -/// analysis. -const std::list heap_domaint::get_new_heap_vars() -{ - std::list result; - for(const template_rowt &row : templ) - { - if(row.kind==OUTHEAP) - { - assert(row.expr.id()==ID_symbol); - symbol_exprt expr=to_symbol_expr(row.expr); - rename(expr); - result.push_back(expr); - } - } - return result; -} - -void heap_domaint::initialize_domain( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) -{ - // Bind list iterators - bind_iterators(SSA, precondition, template_generator); - - // Create preconditions for input variables if not exist - exprt::operandst equs; - for(const symbol_exprt ¶m : SSA.params) - create_precondition(param, precondition); - for(const symbol_exprt &global_in : SSA.globals_in) - create_precondition(global_in, precondition); -} - -/// Bind iterators in the \p template_generator from \p SSA to actual heap -/// objects from the calling context given by \p precondition -void heap_domaint::bind_iterators( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) -{ - new_heap_row_specs.clear(); - for(const list_iteratort &iterator : SSA.iterators) - { - for(const list_iteratort::accesst &access : iterator.accesses) - { - exprt access_binding=iterator_access_bindings( - iterator.pointer, - iterator.init_pointer, - iterator.iterator_symbol(), - iterator.fields, - access, - 0, - exprt::operandst(), - precondition, - SSA); - - // Special treatment for first element in the list - // @TODO this should be handled better - if(access.fields.size()>1 && access.location!=list_iteratort::IN_LOC) - { - const std::set first=collect_preconditions_rec( - iterator.init_pointer, - precondition); - for(const exprt &value : first) - { - if(value.id()==ID_address_of) - { - assert(to_address_of_expr(value).object().id()==ID_symbol); - const symbol_exprt &first_obj= - to_symbol_expr(to_address_of_expr(value).object()); - const symbol_exprt new_value= - recursive_member_symbol( - first_obj, - access.fields.back(), - access.location, - ns); - const symbol_exprt old_value= - recursive_member_symbol( - first_obj, - access.fields.back(), - list_iteratort::IN_LOC, - ns); - const exprt binding=equal_exprt(new_value, old_value); - access_binding=or_exprt(access_binding, binding); - - add_new_heap_row_spec( - old_value, - static_cast(access.location), - binding); - } - } - } - - iterator_bindings.push_back(access_binding); - } - } - - // Add template rows for bound heap objects - for(const heap_row_spect &row_spec : new_heap_row_specs) - { - new_output_template_row( - row_spec.expr, - row_spec.location_number, - row_spec.post_guard, - SSA, - template_generator); - } -} - -/// Insert new output template row into the template. -void heap_domaint::new_output_template_row( - const symbol_exprt &var, - const unsigned location_number, - const exprt &post_guard, - const local_SSAt &SSA, - template_generator_baset &template_generator) -{ - template_generator.var_specs.push_back(domaint::var_spect()); - domaint::var_spect &var_spec=template_generator.var_specs.back(); - - local_SSAt::locationt loc=SSA.get_location(location_number); - - const exprt pre_guard=SSA.guard_symbol(loc); - - const symbol_exprt pre_var= - SSA.name(ssa_objectt(var, SSA.ns), local_SSAt::LOOP_BACK, loc); - const symbol_exprt post_var= - SSA.name(ssa_objectt(var, SSA.ns), local_SSAt::OUT, loc); - - var_spec.var=pre_var; - var_spec.pre_guard=pre_guard; - var_spec.post_guard=post_guard; - var_spec.aux_expr=true_exprt(); - var_spec.kind=OUTHEAP; - - renaming_map[pre_var]=post_var; - assert(var.type().id()==ID_pointer); - const typet &pointed_type=ns.follow(var.type().subtype()); - add_template_row(var_spec, pointed_type); -} - -/// Create \p precondition for given \p var at the input of the function if it -/// does not exist in given calling context. -void heap_domaint::create_precondition( - const symbol_exprt &var, - const exprt &precondition) -{ - if(var.type().id()==ID_pointer) - { - auto pre=collect_preconditions_rec(var, precondition); - if(pre.empty() || (pre.size()==1 && *(pre.begin())==var)) - { - if(id2string(var.get_identifier()).find('.')==std::string::npos) - { - // For variables, create abstract address - const symbolt *symbol; - if(ns.lookup(id2string(var.get_identifier()), symbol)) - return; - - address_of_exprt init_value(symbol->symbol_expr()); - init_value.type()=symbol->type; - aux_bindings.push_back(equal_exprt(var, init_value)); - } - else - { - // For members of structs, find corresponding object in the calling - // context and return its member - std::string var_id_str=id2string(var.get_identifier()); - const symbol_exprt pointer( - var_id_str.substr(0, var_id_str.rfind("'obj")), - var.type()); - const irep_idt member=var_id_str.substr(var_id_str.rfind(".")); - - exprt::operandst d; - std::set pointed_objs= - collect_preconditions_rec(pointer, precondition); - for(exprt pointed : pointed_objs) - { - if(pointed.id()==ID_address_of) - { - const exprt pointed_object=to_address_of_expr(pointed).object(); - if(pointed_object.id()==ID_symbol) - { - symbol_exprt pointed_member( - id2string(to_symbol_expr(pointed_object).get_identifier())+ - id2string(member), - var.type()); - d.push_back(equal_exprt(var, pointed_member)); - } - } - } - if(!d.empty()) - { - iterator_bindings.push_back(disjunction(d)); - } - } - } - } -} - -exprt heap_domaint::get_iterator_bindings() const -{ - return conjunction(iterator_bindings); -} - -exprt heap_domaint::get_aux_bindings() const -{ - return conjunction(aux_bindings); -} - -exprt heap_domaint::get_input_bindings() const -{ - return and_exprt(get_iterator_bindings(), get_aux_bindings()); -} - -/// Create bindings of iterator with corresponding dynamic objects. Function is -/// called recursively, if there is access with multiple fields. -/// \param src: Source pointer (symbolic value) -/// \param init_pointed: Actual value of the source pointer -/// \param iterator_sym: Corresponding iterator symbol -/// \param fields: Set of fields to follow -/// \param access: Iterator access to be bound -/// \param level: Current access level -/// \param guards: Guards -/// \param precondition: Calling context -/// \param SSA: SSA -/// \return Formula corresponding to bindings -const exprt heap_domaint::iterator_access_bindings( - const symbol_exprt &src, - const exprt &init_pointer, - const symbol_exprt &iterator_sym, - const std::vector &fields, - const list_iteratort::accesst &access, - const unsigned level, - exprt::operandst guards, - const exprt &precondition, - const local_SSAt &SSA) -{ - const std::set reachable= - reachable_objects(init_pointer, fields, precondition); - - exprt::operandst d; - for(const symbol_exprt &r : reachable) + // Row expression is a disjunction of possible points-to relations. + exprt::operandst result; + for(auto &points_to : may_point_to) { + // Single points-to relation is a conjunction of pointer equalities for + // individual template row expressions and their corresponding targets. exprt::operandst c; - - equal_exprt points_to_eq(src, address_of_exprt(r)); - c.push_back(points_to_eq); - - if(level==0) - { - equal_exprt address_eq( - address_canonizer(address_of_exprt(iterator_sym), ns), - address_of_exprt(r)); - c.push_back(address_eq); - } - - equal_exprt access_eq=access.binding(iterator_sym, r, level, ns); - c.push_back(access_eq); - - guards.push_back(conjunction(c)); - - if(level(access.location), - conjunction(guards)); + c.push_back(ptr_equality(templ_row_expr.pointers[i], points_to[i], ns)); } - - guards.pop_back(); - - d.push_back(conjunction(c)); + result.push_back(conjunction(c)); } - - if(!d.empty()) - return disjunction(d); - else - return true_exprt(); + return disjunction(result); } -/// Find all objects reachable from source via the vector of fields -/// \param src: Source expression -/// \param fields: Set of fields to follow -/// \param precondition: Calling context -/// \return Set of reachable objects -const std::set heap_domaint::reachable_objects( - const exprt &src, - const std::vector &fields, - const exprt &precondition) const +/// Add new expression to the set of pointed objects. +/// In case it is already there, set row to nondet. +bool heap_domaint::row_valuet::add_points_to( + const points_to_relt &destinations) { - std::set result; - - if(!(src.id()==ID_symbol || src.id()==ID_member)) - return result; - - std::set pointed_objs; - if(src.id()==ID_member && to_member_expr(src).compound().get_bool(ID_pointed)) + if(may_point_to.find(destinations)==may_point_to.end()) { - const member_exprt &member=to_member_expr(src); - const exprt pointer= - get_pointer(member.compound(), pointed_level(member.compound())-1); - - std::set r= - reachable_objects(pointer, {member.get_component_name()}, precondition); - pointed_objs.insert(r.begin(), r.end()); - } - else - { - if(src.type().id()==ID_pointer) - { - std::set values=collect_preconditions_rec(src, precondition); - for(const exprt &v : values) - { - if(v.id()==ID_address_of) - { - assert(to_address_of_expr(v).object().id()==ID_symbol); - pointed_objs.insert(to_symbol_expr(to_address_of_expr(v).object())); - } - } - } - else - { - assert(src.type().get_bool("#dynamic")); - pointed_objs.insert(to_symbol_expr(src)); - } - } - - for(std::size_t i=0; i reachable_objs=collect_preconditions_rec( - obj_member, - precondition); - for(const exprt &reachable : reachable_objs) - { - if(reachable.id()==ID_address_of) - { - const exprt &reachable_obj=to_address_of_expr(reachable).object(); - assert(reachable_obj.id()==ID_symbol); - - result.insert(to_symbol_expr(reachable_obj)); - } - } - } - if(i!=fields.size()-1) - pointed_objs=result; - } - - return result; -} - -void heap_domaint::add_new_heap_row_spec( - const symbol_exprt &expr, - const unsigned location_number, - const exprt &post_guard) -{ - auto it=new_heap_row_specs.emplace(expr, location_number, post_guard); - if(!it.second) - { - if(it.first->post_guard!=post_guard) - it.first->post_guard=or_exprt(it.first->post_guard, post_guard); - } -} - -/// Recursively find all preconditions for the given expression in the calling -/// context. Returns right-hand sides of equalities where expr is left-hand -/// side. -/// \param expr: Expression -/// \param precondition: calling context -/// \return Set of preconditions corresponding to given expression. -const std::set heap_domaint::collect_preconditions_rec( - const exprt &expr, - const exprt &precondition) -{ - std::set result; - if(precondition.id()==ID_equal) - { - const equal_exprt &eq=to_equal_expr(precondition); - if((eq.lhs()==expr && eq.rhs()!=expr) || - (eq.lhs().id()==ID_symbol && - expr.id()==ID_symbol && - to_symbol_expr(eq.lhs()).get_identifier()== - to_symbol_expr(expr).get_identifier())) - { - result.insert(eq.rhs()); - } - } - else - { - forall_operands(it, precondition) - { - std::set op_result=collect_preconditions_rec(expr, *it); - result.insert(op_result.begin(), op_result.end()); - } - } - return result; -} - -/// Restrict template to a given symbolic path. For each template row, we add -/// all other loop guards in their positive or negative form (as specified by -/// path) to aux_expr. -/// \param sympath: Symbolic path -void heap_domaint::restrict_to_sympath(const symbolic_patht &sympath) -{ - for(auto &row : templ) - { - const exprt c=sympath.get_expr(row.pre_guard.op1()); - row.aux_expr=and_exprt(row.aux_expr, c); + may_point_to.insert(destinations); + return true; } -} -/// Reset aux symbols to true (remove all restricitions). -void heap_domaint::clear_aux_symbols() -{ - for(auto &row : templ) - row.aux_expr=true_exprt(); + return set_nondet(); } -/// Restrict template to other paths than those specified. -/// \param sympaths: Vector of symbolic paths -void heap_domaint::eliminate_sympaths( - const std::vector &sympaths) +bool heap_domaint::row_valuet::set_nondet() { - for(auto &row : templ) - { - exprt::operandst paths; - for(auto &sympath : sympaths) - { - const exprt path_expr=sympath.get_expr(row.pre_guard.op1()); - paths.push_back(path_expr); - } - row.aux_expr=paths.empty() - ? true_exprt() - : static_cast(not_exprt(disjunction(paths))); - } -} - -/// Undo last restriction (remove last conjunct from each aux_expr). -void heap_domaint::undo_restriction() -{ - for(auto &row : templ) - { - if(row.aux_expr.id()==ID_and) - { - row.aux_expr=to_and_expr(row.aux_expr).op0(); - } - } -} - -exprt heap_domaint::get_current_loop_guard(size_t row) -{ - return to_and_expr(templ[row].pre_guard).op1(); + bool changed=!nondet; + nondet=true; + return changed; } bool heap_domaint::edit_row(const rowt &row, valuet &_inv, bool improved) { - heap_domaint::heap_valuet &inv= - static_cast(_inv); - const heap_domaint::template_rowt &templ_row=templ[row]; + auto &value_row=dynamic_cast(_inv)[row]; + auto &templ_row_pointers= + dynamic_cast(*templ[row].expr).pointers; - if(templ_row.expr.id()==ID_and) + row_valuet::points_to_relt points_to_destinations; + for(unsigned i=0; i=0 && !inv[member_val_index].nondet) - { - // Add all paths from obj.next to p - if(add_transitivity( - row, - static_cast(member_val_index), - inv)) - { - improved=true; - const std::string expr_str= - from_expr(ns, "", templ[member_val_index].expr); - } - } + points_to_destinations.push_back(points_to_dest); } - // Recursively update all rows that are dependent on this row - if(templ_row.mem_kind==heap_domaint::HEAP) - { - updated_rows.clear(); - if(!inv[row].nondet) - update_rows_rec(row, inv); - else - clear_pointing_rows(row, inv); - } + if(value_row.add_points_to(points_to_destinations)) + improved=true; return improved; } - -/// Find the template row that contains specified member field of a dynamic -/// object at the given location. -/// \param obj: Object -/// \param member: Object field -/// \param actual_loc: Actual location -/// \param kind: Kind -/// \return Row number for obj.member#loc with maximal loc less than actual_loc -/// -1 if such template row does not exist -int heap_domaint::find_member_row( - const exprt &obj, - const irep_idt &member, - int actual_loc, - const domaint::kindt &kind) -{ - assert(obj.id()==ID_symbol); - std::string obj_id=id2string( - ssa_inlinert::get_original_identifier(to_symbol_expr(obj))); - - int result=-1; - int max_loc=-1; - for(unsigned i=0; imax_loc && - (kind==domaint::OUT || kind==domaint::OUTHEAP || loc<=actual_loc)) - { - max_loc=loc; - result=i; - } - } - } - } - return result; -} - -/// Recursively update rows that point to given row. -bool heap_domaint::update_rows_rec( - const heap_domaint::rowt &row, - heap_domaint::heap_valuet &value) -{ - heap_domaint::heap_row_valuet &row_value= - static_cast(value[row]); - const heap_domaint::template_rowt &templ_row=templ[row]; - - updated_rows.insert(row); - bool result=false; - for(const heap_domaint::rowt &ptr : row_value.pointed_by) - { - if(templ[ptr].mem_kind==heap_domaint::HEAP && - templ[ptr].member==templ_row.member) - { - if(add_transitivity(ptr, row, value)) - result=true; - - // Recursive update is called for each row only once - if(updated_rows.find(ptr)==updated_rows.end()) - result=update_rows_rec(ptr, value) || result; - } - } - return result; -} - -const exprt heap_domaint::initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) -{ - initialize_domain(SSA, precondition, template_generator); - - const exprt input_bindings=get_input_bindings(); - if(!input_bindings.is_true()) - { - return input_bindings; - } - return true_exprt(); -} - - -void heap_domaint::clear_pointing_rows( - const heap_domaint::rowt &row, - heap_domaint::heap_valuet &value) -{ - heap_domaint::heap_row_valuet &row_value= - static_cast(value[row]); - - std::vector to_remove; - for(auto &ptr : row_value.pointed_by) - { - if(ptr!=row) - { - value[ptr].clear(); - to_remove.push_back(ptr); - } - } - for(auto &r : to_remove) - row_value.pointed_by.erase(r); -} - /// Get an address where the given pointer points to in the current solver /// iteration. Returns nil_exprt if the value of the pointer is nondet. const exprt heap_domaint::get_points_to_dest( @@ -1473,3 +252,13 @@ const exprt heap_domaint::get_points_to_dest( else return nil_exprt(); } + +void heap_domaint::template_row_exprt::output( + std::ostream &out, + const namespacet &ns) const +{ + for(auto &ptr : pointers) + { + out << from_expr(ns, "", ptr) << " --points to--> ADDR" << std::endl; + } +} diff --git a/src/domains/heap_domain.h b/src/domains/heap_domain.h index 7504a923b..cfe3ed9dc 100644 --- a/src/domains/heap_domain.h +++ b/src/domains/heap_domain.h @@ -18,378 +18,97 @@ Author: Viktor Malik #include -#include "domain.h" +#include "simple_domain.h" #include "template_generator_base.h" #include -class heap_domaint:public domaint +class heap_domaint:public simple_domaint { public: - typedef unsigned rowt; - // Field of a dynamic object (a variable) - typedef vart member_fieldt; - // We represent dynamic object by the object itself and its member field - typedef std::pair dyn_objt; - - typedef enum { STACK, HEAP } mem_kindt; - heap_domaint( unsigned int _domain_number, replace_mapt &_renaming_map, const var_specst &var_specs, const local_SSAt &SSA): - domaint(_domain_number, _renaming_map, SSA.ns) + simple_domaint(_domain_number, _renaming_map, SSA.ns) { make_template(var_specs, ns); } - struct template_rowt - { - vart expr; - guardt pre_guard; - guardt post_guard; - exprt aux_expr; - kindt kind; - mem_kindt mem_kind; - exprt dyn_obj; - irep_idt member; - }; - typedef std::vector templatet; - - /*******************************************************************\ - Base class for a value of a row - \*******************************************************************/ - struct row_valuet - { - // Row is nondeterministic - row expression is TRUE - bool nondet=false; - - const namespacet &ns; - - explicit row_valuet(const namespacet &ns):ns(ns) {} - - virtual exprt get_row_expr( - const vart &templ_expr, - bool rename_templ_expr) const=0; - - virtual bool empty() const=0; - - virtual bool add_points_to(const exprt &dest)=0; - - virtual void clear()=0; - - virtual ~row_valuet() {} - }; - - /*******************************************************************\ - Stack row - used for pointer-typed stack objects (variables). - Value is a set of objects that the pointer can point to. - \*******************************************************************/ - struct stack_row_valuet:public row_valuet + /// Heap template row describes a set of pointer expressions + struct template_row_exprt:public simple_domaint::template_row_exprt { - // Set of objects (or NULL) the row variable can point to - std::set points_to; - - explicit stack_row_valuet(const namespacet &ns):row_valuet(ns) {} + var_listt pointers; - virtual exprt get_row_expr( - const vart &templ_expr, - bool rename_templ_expr) const override; + explicit template_row_exprt(var_listt pointers): + pointers(std::move(pointers)) {} - virtual bool add_points_to(const exprt &expr) override; - - virtual bool empty() const override - { - return points_to.empty(); - } + std::vector get_row_exprs() override { return {pointers}; } - virtual void clear() override; + void output(std::ostream &out, const namespacet &ns) const override; }; - /*******************************************************************\ - Heap row - used for pointer-typed fields of dynamic objects. - - Value is a disjunction of conjunctions of paths leading from the dynamic - object via the field. - \*******************************************************************/ - struct heap_row_valuet:public row_valuet + /// Value of a heap template row describes a may point-to relation for the row + /// pointers. + struct row_valuet { - /*******************************************************************\ - Path in a heap. Contains: - - destination object - - set of dynamic objects - set of SSA objects that the path is composed of - - Paths are ordered by destination only as it is unique within a value row. - \*******************************************************************/ - struct patht - { - exprt destination; - mutable std::set dyn_objects; - - patht(const exprt &dest_):destination(dest_) {} // NOLINT(*) - - patht(const exprt &dest_, const std::set &dyn_objs_): - destination(dest_), dyn_objects(dyn_objs_) {} - - bool operator<(const patht &rhs) const - { - return destination paths; - - // Set of rows whose variables point to this row - std::set pointed_by; - - // Dynamic object corresponding to the row (contains both object and field) - dyn_objt dyn_obj; - // Self link on an abstract dynamic object - bool self_linkage=false; - - heap_row_valuet(const namespacet &ns, const dyn_objt &dyn_obj_): - row_valuet(ns), dyn_obj(dyn_obj_) {} + // Single points-to relation for a vector of pointer expressions. + // For each pointer, it contains a single pointed object (or NULL). + // The order is important - it should match the order of pointers in + // the template row. + typedef std::vector points_to_relt; - virtual exprt get_row_expr( - const vart &templ_expr_, - bool rename_templ_expr) const override; + // May point-to relation: it is a set of possible points-to relations. + std::set may_point_to; - virtual bool add_points_to(const exprt &dest) override; - - virtual bool empty() const override - { - return paths.empty() && !self_linkage; - } - - virtual void clear() override; - - bool add_path(const exprt &dest, const dyn_objt &dyn_obj); + // Row is nondeterministic - row expression is TRUE + bool nondet=false; - bool add_all_paths( - const heap_row_valuet &other_val, - const dyn_objt &dyn_obj); + explicit row_valuet(const namespacet &ns):ns(ns) {} - bool add_pointed_by(const rowt &row); + exprt get_row_expr(const template_row_exprt &templ_row_expr) const; - bool add_self_linkage(); + bool add_points_to(const points_to_relt &destinations); + bool set_nondet(); protected: - static exprt rename_outheap(const symbol_exprt &expr); + const namespacet &ns; }; // Heap value is a conjunction of rows - class heap_valuet: - public valuet, - public std::vector> + struct heap_valuet:simple_domaint::valuet, std::vector { - public: - row_valuet &operator[](const rowt &row) const + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override { - return *(this->at(row).get()); + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + return (*this)[row].get_row_expr(templ_row_expr); } - }; - - // Initialize value and domain - virtual void initialize(valuet &value) override; - void initialize_domain( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); - - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); - - // Value -> constraints - exprt to_pre_constraints(valuet &_value); - - void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); - - // Row -> constraints - exprt get_row_pre_constraint( - const rowt &row, - const row_valuet &row_value) const; - - exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value); - - // Row modifications - bool add_transitivity(const rowt &from, const rowt &to, heap_valuet &value); - - bool add_points_to(const rowt &row, heap_valuet &value, const exprt &dest); - - bool set_nondet(const rowt &row, heap_valuet &value); + heap_valuet *clone() override { return new heap_valuet(*this); } + }; - // Printing - virtual void output_value( - std::ostream &out, - const valuet &value, - const namespacet &ns) const override; + std::unique_ptr new_value() override + { + return std::unique_ptr(new heap_valuet()); + } - virtual void output_domain( - std::ostream &out, - const namespacet &ns) const override; + // Initialize value and domain + void initialize_value(domaint::valuet &value) override; - // Projection - virtual void - project_on_vars(valuet &value, const var_sett &vars, exprt &result) override; + // Handle row edit - join the model obtained from SMT with inv + bool edit_row(const rowt &row, valuet &inv, bool improved) override; // Conversion of solver value to expression static exprt value_to_ptr_exprt(const exprt &expr); - // Join of values - virtual void join(valuet &value1, const valuet &value2) override; - - // Restriction to symbolic paths - void restrict_to_sympath(const symbolic_patht &sympath); - void undo_restriction(); - void eliminate_sympaths(const std::vector &sympaths); - void clear_aux_symbols(); - - // Getters for protected fields - const std::list get_new_heap_vars(); - - exprt get_iterator_bindings() const; - exprt get_aux_bindings() const; - exprt get_input_bindings() const; - - bool empty() const - { - return templ.empty(); - } - protected: - templatet templ; - - // Bindings computed during interprocedural analysis - exprt::operandst iterator_bindings; - exprt::operandst aux_bindings; - - std::set updated_rows; - exprt solver_value_op0; - exprt solver_value_op1; - - /*******************************************************************\ - Specification of a new heap row that is added dynamically - at the beginning of the analysis, after binding of iterators to the actual - dynamic objects from the calling context. - - Contains row expression and a location where the corresponding - iterator occured. - \*******************************************************************/ - class heap_row_spect - { - public: - symbol_exprt expr; - unsigned location_number; - - mutable exprt post_guard; - - heap_row_spect( - const symbol_exprt &expr, - unsigned location_number, - const exprt &post_guard): - expr(expr), location_number(location_number), post_guard(post_guard) {} - - bool operator<(const heap_row_spect &rhs) const - { - return std::tie(expr, location_number)< - std::tie(rhs.expr, rhs.location_number); - } - - bool operator==(const heap_row_spect &rhs) const - { - return std::tie(expr, location_number)== - std::tie(rhs.expr, rhs.location_number); - } - }; - - // Set of new heap rows added during analysis (used for interprocedural) - std::set new_heap_row_specs; - void make_template(const var_specst &var_specs, const namespacet &ns); - - void add_template_row(const var_spect &var_spec, const typet &pointed_type); - void add_template_row_pair( - const var_spect &var_spec1, - const var_spect &var_spec2, - const typet &pointed_type); - - // Initializing functions - void bind_iterators( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); - - void create_precondition(const symbol_exprt &var, const exprt &precondition); - - void new_output_template_row( - const symbol_exprt &var, - const unsigned location_number, - const exprt &post_guard, - const local_SSAt &SSA, - template_generator_baset &template_generator); - - const exprt iterator_access_bindings( - const symbol_exprt &src, - const exprt &init_pointer, - const symbol_exprt &iterator_sym, - const std::vector &fields, - const list_iteratort::accesst &access, - const unsigned level, - exprt::operandst guards, - const exprt &precondition, - const local_SSAt &SSA); - - const std::set reachable_objects( - const exprt &src, - const std::vector &fields, - const exprt &precondition) const; - - static const std::set collect_preconditions_rec( - const exprt &expr, - const exprt &precondition); - - virtual exprt get_current_loop_guard(size_t row) override; - - bool edit_row(const rowt &row, valuet &inv, bool improved); - - void add_new_heap_row_spec( - const symbol_exprt &expr, - const unsigned location_number, - const exprt &post_guard); + void add_template_row(var_listt pointers, const guardst &guards); // Utility functions - static int get_symbol_loc(const exprt &expr); const exprt get_points_to_dest( const exprt &solver_value, const exprt &templ_row_expr); - - int find_member_row( - const exprt &obj, - const irep_idt &member, - int actual_loc, - const domaint::kindt &kind); - - bool update_rows_rec( - const heap_domaint::rowt &row, - heap_domaint::heap_valuet &value); - void clear_pointing_rows( - const heap_domaint::rowt &row, - heap_domaint::heap_valuet &value); - const exprt initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); - - friend class strategy_solver_heapt; }; #endif // CPROVER_2LS_DOMAINS_HEAP_DOMAIN_H diff --git a/src/domains/heap_tpolyhedra_domain.cpp b/src/domains/heap_tpolyhedra_domain.cpp deleted file mode 100644 index f09a16724..000000000 --- a/src/domains/heap_tpolyhedra_domain.cpp +++ /dev/null @@ -1,121 +0,0 @@ -/*******************************************************************\ - -Module: Combination of heap and template polyhedra abstract domains - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Combination of heap and template polyhedra abstract domains - -#include "heap_tpolyhedra_domain.h" - -/// Initialize abstract value. -void heap_tpolyhedra_domaint::initialize(domaint::valuet &value) -{ - heap_tpolyhedra_valuet &v=static_cast(value); - - heap_domain.initialize(v.heap_value); - polyhedra_domain.initialize(v.tpolyhedra_value); -} - -void heap_tpolyhedra_domaint::output_value( - std::ostream &out, - const domaint::valuet &value, - const namespacet &ns) const -{ - const heap_tpolyhedra_valuet &v= - static_cast(value); - - heap_domain.output_value(out, v.heap_value, ns); - polyhedra_domain.output_value(out, v.tpolyhedra_value, ns); -} - -void heap_tpolyhedra_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - heap_domain.output_domain(out, ns); - polyhedra_domain.output_domain(out, ns); -} - -void heap_tpolyhedra_domaint::project_on_vars( - domaint::valuet &value, - const domaint::var_sett &vars, - exprt &result) -{ - heap_tpolyhedra_valuet &v=static_cast(value); - - exprt heap_result; - heap_domain.project_on_vars(v.heap_value, vars, heap_result); - exprt tpolyhedra_result; - polyhedra_domain.project_on_vars(v.tpolyhedra_value, vars, tpolyhedra_result); - - result=heap_result; - if(tpolyhedra_result!=true_exprt()) - result=and_exprt(result, tpolyhedra_result); -} - -/// Restrict template to a given symbolic path. -/// \param sympath: Symbolic path -void heap_tpolyhedra_domaint::restrict_to_sympath( - const symbolic_patht &sympath) -{ - heap_domain.restrict_to_sympath(sympath); - polyhedra_domain.restrict_to_sympath(sympath); -} - -/// Reset aux symbols to true (remove all restricitions). -void heap_tpolyhedra_domaint::clear_aux_symbols() -{ - heap_domain.clear_aux_symbols(); - polyhedra_domain.clear_aux_symbols(); -} - -/// Restrict template to other paths than those specified. -/// \param sympaths: Vector of symbolic paths -void heap_tpolyhedra_domaint::eliminate_sympaths( - const std::vector &sympaths) -{ - heap_domain.eliminate_sympaths(sympaths); - polyhedra_domain.eliminate_sympaths(sympaths); -} - -/// Undo last restriction. -void heap_tpolyhedra_domaint::undo_restriction() -{ - heap_domain.undo_restriction(); - polyhedra_domain.undo_restriction(); -} - -bool heap_tpolyhedra_domaint::edit_row( - const rowt &row, - valuet &inv, - bool improved) -{ - return improved; -} - -exprt heap_tpolyhedra_domaint::to_pre_constraints(valuet &value) -{ - return true_exprt(); -} - -void heap_tpolyhedra_domaint::make_not_post_constraints( - valuet &value, - exprt::operandst &cond_exprs) -{ -} - -std::vector heap_tpolyhedra_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - return r; -} - -void heap_tpolyhedra_domaint::set_smt_values( - std::vector got_values, - size_t row) -{ -} diff --git a/src/domains/heap_tpolyhedra_domain.h b/src/domains/heap_tpolyhedra_domain.h deleted file mode 100644 index e9684cfec..000000000 --- a/src/domains/heap_tpolyhedra_domain.h +++ /dev/null @@ -1,91 +0,0 @@ -/*******************************************************************\ - -Module: Combination of heap and template polyhedra abstract domains - -Author: Viktor Malik - -\*******************************************************************/ -/// \file -/// Combination of heap and template polyhedra abstract domains - -#ifndef CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H -#define CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H - - -#include "domain.h" -#include "tpolyhedra_domain.h" -#include "heap_domain.h" - -class heap_tpolyhedra_domaint:public domaint -{ -public: - enum polyhedra_kindt - { - INTERVAL, ZONES, OCTAGONS - }; - - heap_domaint heap_domain; - tpolyhedra_domaint polyhedra_domain; - - heap_tpolyhedra_domaint( - unsigned int _domain_number, - replace_mapt &_renaming_map, - const var_specst &var_specs, - const local_SSAt &SSA, - const polyhedra_kindt polyhedra_kind): - domaint(_domain_number, _renaming_map, SSA.ns), - heap_domain(_domain_number, _renaming_map, var_specs, SSA), - polyhedra_domain(_domain_number, _renaming_map, ns) - { - if(polyhedra_kind==INTERVAL) - polyhedra_domain.add_interval_template(var_specs, ns); - else if(polyhedra_kind==ZONES) - { - polyhedra_domain.add_difference_template(var_specs, ns); - polyhedra_domain.add_interval_template(var_specs, ns); - } - } - - class heap_tpolyhedra_valuet:public valuet - { - public: - heap_domaint::heap_valuet heap_value; - tpolyhedra_domaint::templ_valuet tpolyhedra_value; - }; - - virtual void initialize(valuet &value) override; - - virtual void output_value( - std::ostream &out, - const valuet &value, - const namespacet &ns) const override; - - virtual void output_domain( - std::ostream &out, - const namespacet &ns) const override; - - virtual void project_on_vars( - valuet &value, - const var_sett &vars, - exprt &result) override; - - // Restriction to symbolic paths - void restrict_to_sympath(const symbolic_patht &sympath); - void undo_restriction(); - void eliminate_sympaths(const std::vector &sympaths); - void clear_aux_symbols(); - - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); - - // Value -> constraints - exprt to_pre_constraints(valuet &_value); - - void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); - - bool edit_row(const rowt &row, valuet &inv, bool improved); -}; - -#endif // CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_DOMAIN_H diff --git a/src/domains/heap_tpolyhedra_sympath_domain.cpp b/src/domains/heap_tpolyhedra_sympath_domain.cpp deleted file mode 100644 index a918a0ff7..000000000 --- a/src/domains/heap_tpolyhedra_sympath_domain.cpp +++ /dev/null @@ -1,86 +0,0 @@ -/*******************************************************************\ - -Module: Abstract domain for computing invariants in heap-tpolyhedra - domain for different symbolic paths in program. - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Abstract domain for computing invariants in heap-tpolyhedra domain for -/// different symbolic paths in program. - -#include "heap_tpolyhedra_sympath_domain.h" - -void heap_tpolyhedra_sympath_domaint::output_value( - std::ostream &out, - const domaint::valuet &value, - const namespacet &ns) const -{ - const heap_tpolyhedra_sympath_valuet &v= - static_cast(value); - for(auto &config : v) - { - out << from_expr(ns, "", config.first) << "==>\n"; - heap_tpolyhedra_domain.output_value(out, config.second, ns); - } -} - -void heap_tpolyhedra_sympath_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - heap_tpolyhedra_domain.output_domain(out, ns); -} - -void heap_tpolyhedra_sympath_domaint::project_on_vars( - domaint::valuet &value, - const domaint::var_sett &vars, - exprt &result) -{ - heap_tpolyhedra_sympath_valuet &v= - static_cast(value); - exprt::operandst c; - for(auto &config : v) - { - exprt config_result; - heap_tpolyhedra_domain.project_on_vars(config.second, vars, config_result); - c.push_back(and_exprt(config.first, config_result)); - } - c.push_back(no_loops_path); - - result=c.empty() ? true_exprt() : disjunction(c); -} - -bool heap_tpolyhedra_sympath_domaint::edit_row( - const rowt &row, - valuet &inv, - bool improved) -{ - return improved; -} - -exprt heap_tpolyhedra_sympath_domaint::to_pre_constraints(valuet &value) -{ - return true_exprt(); -} - -void heap_tpolyhedra_sympath_domaint::make_not_post_constraints( - valuet &value, - exprt::operandst &cond_exprs) -{ -} - -std::vector heap_tpolyhedra_sympath_domaint::get_required_smt_values( - size_t row) -{ - std::vector r; - return r; -} - -void heap_tpolyhedra_sympath_domaint::set_smt_values( - std::vector got_values, - size_t row) -{ -} diff --git a/src/domains/heap_tpolyhedra_sympath_domain.h b/src/domains/heap_tpolyhedra_sympath_domain.h deleted file mode 100644 index f3dd04585..000000000 --- a/src/domains/heap_tpolyhedra_sympath_domain.h +++ /dev/null @@ -1,86 +0,0 @@ -/*******************************************************************\ - -Module: Abstract domain for computing invariants in heap-tpolyhedra - domain for different symbolic paths in program. - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Abstract domain for computing invariants in heap-tpolyhedra domain for -/// different symbolic paths in program. - -#ifndef CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H -#define CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H - - -#include "domain.h" -#include "heap_tpolyhedra_domain.h" - -class heap_tpolyhedra_sympath_domaint:public domaint -{ -public: - heap_tpolyhedra_domaint heap_tpolyhedra_domain; - - heap_tpolyhedra_sympath_domaint( - unsigned int _domain_number, - replace_mapt &_renaming_map, - const var_specst &var_specs, - const local_SSAt &SSA, - const heap_tpolyhedra_domaint::polyhedra_kindt polyhedra_kind): - domaint(_domain_number, _renaming_map, SSA.ns), - heap_tpolyhedra_domain( - _domain_number, _renaming_map, var_specs, SSA, polyhedra_kind) - { - exprt::operandst false_loop_guards; - for(auto &g : SSA.loop_guards) - false_loop_guards.push_back(not_exprt(g.first)); - no_loops_path=conjunction(false_loop_guards); - } - - // Value is a map from expression (symbolic path) to an invariant in heap - // tpolyhedra domain - class heap_tpolyhedra_sympath_valuet: - public valuet, - public std::map - { - }; - - void output_value( - std::ostream &out, - const valuet &value, - const namespacet &ns) const override; - - void output_domain( - std::ostream &out, - const namespacet &ns) const override; - - void project_on_vars( - valuet &value, - const var_sett &vars, - exprt &result) override; - - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); - - // Value -> constraints - exprt to_pre_constraints(valuet &_value); - - void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); - - bool edit_row(const rowt &row, valuet &inv, bool improved); - -protected: - // Special path containing conjunction negations of all loop-select guards - // This must be stored explicitly since the solver is not able to explore this - // path even though it can be feasible - exprt no_loops_path; - - friend class strategy_solver_heap_tpolyhedra_sympatht; -}; - - -#endif // CPROVER_2LS_DOMAINS_HEAP_TPOLYHEDRA_SYMPATH_DOMAIN_H diff --git a/src/domains/incremental_solver.h b/src/domains/incremental_solver.h index 251ebafc1..164c56faa 100644 --- a/src/domains/incremental_solver.h +++ b/src/domains/incremental_solver.h @@ -19,7 +19,6 @@ Author: Peter Schrammel #include #include -#include "domain.h" #include "util.h" // #define DISPLAY_FORMULA diff --git a/src/domains/lexlinrank_domain.cpp b/src/domains/lexlinrank_domain.cpp index a32e1f8db..36cc53d9a 100644 --- a/src/domains/lexlinrank_domain.cpp +++ b/src/domains/lexlinrank_domain.cpp @@ -31,33 +31,26 @@ Author: Peter Schrammel #define COEFF_C_SIZE 10 #define MAX_REFINEMENT 2 -void lexlinrank_domaint::initialize(valuet &value) +void lexlinrank_domaint::initialize_value(domaint::valuet &value) { - templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); v.resize(templ.size()); for(auto &row : v) { - row.resize(1); - row[0].c.resize(1); - row[0].c[0]=false_exprt(); + row.clear(); + row.add_element(); } } -const exprt lexlinrank_domaint::initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator) +void lexlinrank_domaint::initialize() { delete inner_solver; inner_solver=incremental_solvert::allocate(ns); - - return true_exprt(); } bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) { - lexlinrank_domaint::templ_valuet &rank= - static_cast(inv); + auto &rank=dynamic_cast(inv); lexlinrank_domaint::row_valuet symb_values; symb_values.resize(rank[row].size()); @@ -116,7 +109,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) improved=true; // update the current template - set_row_value(row, new_row_values, rank); + rank[row]=new_row_values; if(!refinement_constraint.is_true()) inner_solver->pop_context(); @@ -135,7 +128,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) if(number_elements_per_row[row]==max_elements-1) { // no ranking function for the current template - set_row_value_to_true(row, rank); + rank[row].set_to_true(); reset_refinements(); } else @@ -145,7 +138,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) inner_solver=incremental_solvert::allocate(ns); reset_refinements(); - add_element(row, rank); + rank[row].add_element(); number_inner_iterations=0; improved=true; } @@ -154,7 +147,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) return improved; } -exprt lexlinrank_domaint::to_pre_constraints(valuet &_value) +exprt lexlinrank_domaint::to_pre_constraints(const valuet &_value) { exprt rounding_mode=symbol_exprt( CPROVER_PREFIX "rounding_mode", @@ -165,33 +158,12 @@ exprt lexlinrank_domaint::to_pre_constraints(valuet &_value) from_integer(mp_integer(0), signedbv_typet(32))); } -void lexlinrank_domaint::solver_iter_init(domaint::valuet &_rank) +void lexlinrank_domaint::init_value_solver_iteration(domaint::valuet &_rank) { - lexlinrank_domaint::templ_valuet &rank= - static_cast(_rank); + auto &rank=dynamic_cast(_rank); number_elements_per_row.resize(rank.size()); } -std::vector lexlinrank_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - for(auto &row_expr : strategy_value_exprs[row]) - { - r.push_back(row_expr.first); - r.push_back(row_expr.second); - } - return r; -} - -void lexlinrank_domaint::set_smt_values( - std::vector got_values, - size_t row) -{ - values.clear(); - for(size_t i=0; i(_value); + auto &value=dynamic_cast(_value); cond_exprs.resize(value.size()); strategy_value_exprs.resize(value.size()); -for(std::size_t row=0; rowget_row_exprs(); + strategy_value_exprs[row].insert( + strategy_value_exprs[row].end(), + row_exprs.begin(), + row_exprs.end()); - if(is_row_value_true(value[row])) + if(value[row].is_true()) { // !(g=> true) cond_exprs[row]=false_exprt(); } - else if(is_row_value_false(value[row])) + else if(value[row].is_false()) { // !(g=> false) cond_exprs[row]= - and_exprt(templ[row].pre_guard, templ[row].post_guard); + and_exprt(templ[row].guards.pre_guard, templ[row].guards.post_guard); } else { @@ -241,7 +216,9 @@ for(std::size_t row=0; row(*templ[row].expr); + assert(value[row][elm].c.size()==templ_row_expr.pre_post_values.size()); assert(value[row][elm].c.size()>=1); exprt::operandst c; @@ -251,12 +228,16 @@ for(std::size_t row=0; row=0; --elm) { - symb_values[elm].c.resize(values.size()); - assert(values.size()>=1); + // smt_model_values is a vector of values of pre- and post-values + // two successive elements of the vector correspond to a single symbolic + // value + symb_values[elm].c.resize(smt_model_values.size()/2); + assert(!symb_values[elm].c.empty()); exprt::operandst c; c.reserve(1+symb_values.size()-(elm+1)); @@ -384,31 +378,31 @@ exprt lexlinrank_domaint::get_row_symb_constraint( #ifdef DIFFERENCE_ENCODING exprt sum=mult_exprt( symb_values[elm].c[0], - minus_exprt(values[0].first, values[0].second)); + minus_exprt(smt_model_values[0], smt_model_values[1])); #else - exprt sum_pre=mult_exprt(symb_values[elm].c[0], values[0].first); - exprt sum_post=mult_exprt(symb_values[elm].c[0], values[0].second); + exprt sum_pre=mult_exprt(symb_values[elm].c[0], smt_model_values[0]); + exprt sum_post=mult_exprt(symb_values[elm].c[0], smt_model_values[0]); #endif - for(std::size_t i=1; i(value); + auto &v=dynamic_cast(value); for(std::size_t row=0; row " << std::endl; - break; - default: assert(false); - } + auto &templ_row_expr=dynamic_cast(*templ[row].expr); + templ[row].guards.output(out, ns); for(std::size_t elm=0; elm0) out << "+"; out << from_expr(ns, "", v[row][elm].c[i]) << " * " - << from_expr(ns, "", templ_row.expr[i].first); + << from_expr(ns, "", templ_row_expr.pre_post_values[i].pre); } out << std::endl; } } } -void lexlinrank_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - for(std::size_t row=0; row " - << std::endl << " "; - break; - default: assert(false); - } - - for(std::size_t i=0; i0) - out << "+"; - out << "c!" << row << "$" << i << " * " - << from_expr(ns, "", templ_row.expr[i].first); - } - out << std::endl; - } -} - void lexlinrank_domaint::project_on_vars( - valuet &value, + domaint::valuet &value, const var_sett &vars, exprt &result) { // don't do any projection - const templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); assert(v.size()==templ.size()); exprt::operandst c; // c is the conjunction of all rows c.reserve(templ.size()); for(std::size_t row=0; row false) c.push_back( implies_exprt( - and_exprt(templ[row].pre_guard, templ[row].post_guard), + and_exprt(templ[row].guards.pre_guard, templ[row].guards.post_guard), false_exprt())); } - else if(is_row_value_true(v[row])) + else if(v[row].is_true()) { // (g=> true) c.push_back( implies_exprt( - and_exprt(templ[row].pre_guard, templ[row].post_guard), + and_exprt(templ[row].guards.pre_guard, templ[row].guards.post_guard), true_exprt())); } else { exprt::operandst d; // d is the disjunction of lexicographic elements d.reserve(v[row].size()); + auto &templ_row_expr=dynamic_cast(*templ[row].expr); for(std::size_t elm=0; elm=1); // con is the constraints for a single element of the lexicography @@ -663,8 +594,8 @@ void lexlinrank_domaint::project_on_vars( exprt sum=mult_exprt( v[row][elm].c[0], minus_exprt( - templ[row].expr[0].first, - templ[row].expr[0].second)); + templ_row_expr.pre_post_values[0].pre, + templ_row_expr.pre_post_values[0].post)); for(std::size_t i=1; i(new template_row_exprt()); + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + templ_row.guards.kind=guardst::LOOP; exprt::operandst preg; exprt::operandst postg; for(const auto &v : var_specs) { - if(v.kind!=LOOP) + if(v.guards.kind!=guardst::LOOP) continue; - preg.push_back(v.pre_guard); - postg.push_back(v.post_guard); + preg.push_back(v.guards.pre_guard); + postg.push_back(v.guards.post_guard); exprt vpost=v.var; // copy rename(vpost); - templ_row.expr.push_back(std::pair(v.var, vpost)); + templ_row_expr.pre_post_values.emplace_back(v.var, vpost); } - templ_row.pre_guard=conjunction(preg); - templ_row.post_guard=conjunction(postg); -} - -bool lexlinrank_domaint::is_row_value_false( - const row_valuet & row_value) const -{ - assert(row_value.size()>=1); - assert(row_value[0].c.size()>=1); - return row_value[0].c[0].get(ID_value)==ID_false; -} - -bool lexlinrank_domaint::is_row_element_value_false( - const row_value_elementt & row_value_element) const -{ - assert(false); - assert(row_value_element.c.size()>=1); - return row_value_element.c[0].get(ID_value)==ID_false; + templ_row.guards.pre_guard=conjunction(preg); + templ_row.guards.post_guard=conjunction(postg); } -bool lexlinrank_domaint::is_row_value_true(const row_valuet & row_value) const +std::vector lexlinrank_domaint::template_row_exprt::get_row_exprs() { - assert(row_value.size()>=1); - assert(row_value[0].c.size()>=1); - return row_value[0].c[0].get(ID_value)==ID_true; -} - -bool lexlinrank_domaint::is_row_element_value_true( - const row_value_elementt & row_value_element) const -{ - assert(false); - assert(row_value_element.c.size()>=1); - return row_value_element.c[0].get(ID_value)==ID_true; + std::vector exprs; + for(auto &pre_post : pre_post_values) + { + exprs.push_back(pre_post.pre); + exprs.push_back(pre_post.post); + } + return exprs; } -void lexlinrank_domaint::add_element( - const rowt &row, - templ_valuet &value) +void lexlinrank_domaint::template_row_exprt::output( + std::ostream &out, + const namespacet &ns) const { - value[row].push_back(row_value_elementt()); - for(unsigned i=0; i0) + out << "+"; + out << "c!" << row << "$" << i << " * " + << from_expr(ns, "", pre_post_values[i].pre); } } diff --git a/src/domains/lexlinrank_domain.h b/src/domains/lexlinrank_domain.h index fca42a56d..f22a925ae 100644 --- a/src/domains/lexlinrank_domain.h +++ b/src/domains/lexlinrank_domain.h @@ -23,34 +23,79 @@ Author: Peter Schrammel #include #include -#include "domain.h" +#include "simple_domain.h" -class lexlinrank_domaint:public domaint +class lexlinrank_domaint:public simple_domaint { public: - typedef unsigned rowt; - typedef std::vector > pre_post_valuest; - typedef pre_post_valuest row_exprt; - typedef struct + struct template_row_exprt:simple_domaint::template_row_exprt + { + struct pre_post_valuet + { + exprt pre; + exprt post; + + pre_post_valuet(const exprt &pre, const exprt &post): + pre(pre), post(post) {} + }; + + std::vector pre_post_values; + rowt row; + + std::vector get_row_exprs() override; + void output(std::ostream &out, const namespacet &ns) const override; + }; + + struct row_value_elementt { std::vector c; - } row_value_elementt; - typedef std::vector row_valuet; + void set_to_true() + { + c.clear(); + c.push_back(true_exprt()); + } + void clear() + { + c.clear(); + c.push_back(false_exprt()); + } + bool is_true() const { return c[0].get(ID_value)==ID_true; } + bool is_false() const { return c[0].get(ID_value)==ID_false; } + }; - class templ_valuet:public domaint::valuet, public std::vector + struct row_valuet:std::vector { + void add_element() + { + push_back(row_value_elementt()); + for(auto &elem : *this) + elem.clear(); + } + void set_to_true() + { + clear(); + push_back(row_value_elementt()); + at(0).set_to_true(); + } + bool is_true() const { return at(0).is_true(); } + bool is_false() const { return at(0).is_false(); } }; - typedef struct + struct templ_valuet:simple_domaint::valuet, std::vector { - guardt pre_guard; - guardt post_guard; - row_exprt expr; - kindt kind; - } template_rowt; + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override + { + return true_exprt(); + } + + templ_valuet *clone() override { return new templ_valuet(*this); } + }; - typedef std::vector templatet; + std::unique_ptr new_value() override + { + return std::unique_ptr(new templ_valuet()); + } lexlinrank_domaint( unsigned _domain_number, @@ -58,83 +103,59 @@ class lexlinrank_domaint:public domaint unsigned _max_elements, // lexicographic components unsigned _max_inner_iterations, const namespacet &_ns): - domaint(_domain_number, _renaming_map, _ns), + simple_domaint(_domain_number, _renaming_map, _ns), refinement_level(0), max_elements(_max_elements), max_inner_iterations(_max_inner_iterations), number_inner_iterations(0) - { - inner_solver=incremental_solvert::allocate(_ns); - } + { + inner_solver=incremental_solvert::allocate(_ns); + } // initialize value - virtual void initialize(valuet &value); + void initialize_value(domaint::valuet &value) override; - const exprt initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); + void initialize() override; - void solver_iter_init(domaint::valuet &rank); + void init_value_solver_iteration(domaint::valuet &rank) override; - bool edit_row(const rowt &row, valuet &inv, bool improved); + bool edit_row(const rowt &row, valuet &inv, bool improved) override; - exprt to_pre_constraints(valuet &_value); + exprt to_pre_constraints(const valuet &_value) override; void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); - virtual bool handle_unsat(valuet &value, bool improved); + const valuet &_value, + exprt::operandst &cond_exprs) override; - virtual bool refine(); - virtual void reset_refinements(); + bool handle_unsat(valuet &value, bool improved) override; + + bool refine() override; + void reset_refinements() override; // value -> constraints - exprt get_not_constraints( - const templ_valuet &value, - exprt::operandst &cond_exprs, // identical to before - std::vector &value_exprs); // (x, x') exprt get_row_symb_constraint( row_valuet &symb_values, // contains vars c and d const rowt &row, exprt &refinement_constraint); - void add_element(const rowt &row, templ_valuet &value); - - // set, get value - row_valuet get_row_value(const rowt &row, const templ_valuet &value); - void set_row_value( - const rowt &row, - const row_valuet &row_value, - templ_valuet &value); - void set_row_value_to_true(const rowt &row, templ_valuet &value); - // printing - virtual void output_value( + void output_value( std::ostream &out, - const valuet &value, - const namespacet &ns) const; - virtual void output_domain( - std::ostream &out, - const namespacet &ns) const; + const domaint::valuet &value, + const namespacet &ns) const override; // projection - virtual void project_on_vars( - valuet &value, + void project_on_vars( + domaint::valuet &value, const var_sett &vars, - exprt &result); - - unsigned template_size() {return templ.size();} + exprt &result) override; // generating templates void add_template( const var_specst &var_specs, const namespacet &ns); - templatet templ; unsigned refinement_level; // the "inner" solver const unsigned max_elements; // lexicographic components @@ -142,17 +163,6 @@ class lexlinrank_domaint:public domaint incremental_solvert *inner_solver; unsigned number_inner_iterations; -protected: - pre_post_valuest values; - bool is_row_value_false(const row_valuet & row_value) const; - bool is_row_value_true(const row_valuet & row_value) const; - bool is_row_element_value_false( - const row_value_elementt & row_value_element) const; - bool is_row_element_value_true( - const row_value_elementt & row_value_element) const; -public: - // handles on values to retrieve from model - std::vector strategy_value_exprs; std::vector number_elements_per_row; }; diff --git a/src/domains/linrank_domain.cpp b/src/domains/linrank_domain.cpp index 3374fa1c9..4441421ce 100644 --- a/src/domains/linrank_domain.cpp +++ b/src/domains/linrank_domain.cpp @@ -31,39 +31,17 @@ Author: Peter Schrammel #define COEFF_C_SIZE 10 #define MAX_REFINEMENT 2 -void linrank_domaint::initialize(valuet &value) +void linrank_domaint::initialize_value(domaint::valuet &value) { - templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); v.resize(templ.size()); for(unsigned row=0; row linrank_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - for(auto &row_expr : strategy_value_exprs[row]) - { - r.push_back(row_expr.first); - r.push_back(row_expr.second); - } - return r; -} - -void linrank_domaint::set_smt_values(std::vector got_values, size_t row) -{ - values.clear(); - for(size_t i=0; i(inv); + auto &rank=dynamic_cast(inv); exprt rounding_mode=symbol_exprt( CPROVER_PREFIX "rounding_mode", signedbv_typet(32)); @@ -90,7 +68,7 @@ bool linrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) // solve if((*inner_solver)()==decision_proceduret::D_SATISFIABLE && - number_inner_iterations c=symb_values.c; @@ -106,7 +84,7 @@ bool linrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) exprt rmv=inner_solver->solver->get(rounding_mode); // update the current template - set_row_value(row, new_row_values, rank); + rank[row]=new_row_values; improved=true; } @@ -119,7 +97,7 @@ bool linrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) else { // no ranking function for the current template - set_row_value_to_true(row, rank); + rank[row].set_to_true(); reset_refinements(); } } @@ -130,7 +108,7 @@ bool linrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) return improved; } -exprt linrank_domaint::to_pre_constraints(valuet &_value) +exprt linrank_domaint::to_pre_constraints(const valuet &_value) { exprt rounding_mode=symbol_exprt( CPROVER_PREFIX "rounding_mode", @@ -157,45 +135,50 @@ bool linrank_domaint::refine() } void linrank_domaint::make_not_post_constraints( - valuet &_value, + const valuet &_value, exprt::operandst &cond_exprs) { - linrank_domaint::templ_valuet &value= - static_cast(_value); + auto &value=dynamic_cast(_value); assert(value.size()==templ.size()); cond_exprs.resize(value.size()); strategy_value_exprs.resize(value.size()); for(unsigned row=0; rowget_row_exprs(); strategy_value_exprs[row].insert( strategy_value_exprs[row].end(), - templ[row].expr.begin(), - templ[row].expr.end()); + row_exprs.begin(), + row_exprs.end()); - if(is_row_value_true(value[row])) + if(value[row].is_true()) { // !(g=> true) cond_exprs[row]=false_exprt(); } - else if(is_row_value_false(value[row])) + else if(value[row].is_false()) { // !(g=> false) cond_exprs[row]= - and_exprt(templ[row].pre_guard, templ[row].post_guard); + and_exprt(templ[row].guards.pre_guard, templ[row].guards.post_guard); } else { - assert(value[row].c.size()==templ[row].expr.size()); + auto &templ_row_expr=dynamic_cast(*templ[row].expr); + assert(value[row].c.size()==templ_row_expr.pre_post_values.size()); assert(value[row].c.size()>=1); #ifdef DIFFERENCE_ENCODING exprt sum=mult_exprt( value[row].c[0], - minus_exprt(templ[row].expr[0].first, templ[row].expr[0].second)); + minus_exprt( + templ_row_expr.pre_post_values[0].pre, + templ_row_expr.pre_post_values[0].post)); #else - exprt sum_pre=mult_exprt(value[row].c[0], templ[row].expr[0].first); - exprt sum_post=mult_exprt(value[row].c[0], templ[row].expr[0].second); + exprt sum_pre=mult_exprt( + value[row].c[0], templ_row_expr.pre_post_values[0].pre); + exprt sum_post=mult_exprt( + value[row].c[0], templ_row_expr.pre_post_values[0].post); #endif for(unsigned i=1; i=1); + // smt_model_values is a vector of values of pre- and post-values + // two successive elements of the vector correspond to a single symbolic value + symb_values.c.resize(smt_model_values.size()/2); + assert(!symb_values.c.empty()); symb_values.c[0]=symbol_exprt( SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$0", signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers @@ -250,12 +237,12 @@ exprt linrank_domaint::get_row_symb_constraint( #ifdef DIFFERENCE_ENCODING exprt sum=mult_exprt( symb_values.c[0], - minus_exprt(values[0].first, values[0].second)); + minus_exprt(smt_model_values[0], smt_model_values[1])); #else - exprt sum_pre=mult_exprt(symb_values.c[0], values[0].first); - exprt sum_post=mult_exprt(symb_values.c[0], values[0].second); + exprt sum_pre=mult_exprt(symb_values.c[0], values[0]); + exprt sum_post=mult_exprt(symb_values.c[0], values[1]); #endif - for(unsigned i=1; i(value); + auto &v=dynamic_cast(value); for(unsigned row=0; row " << std::endl << " "; - break; - default: assert(false); - } + auto &templ_row_expr=dynamic_cast(*templ[row].expr); + templ[row].guards.output(out, ns); - for(unsigned i=0; i0) out << "+"; out << from_expr(ns, "", v[row].c[i]) << " * " - << from_expr(ns, "", templ_row.expr[i].first); - } - out << std::endl; - } -} - -void linrank_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - for(unsigned row=0; row " - << std::endl << " "; - break; - default: assert(false); - } - - for(unsigned i=0; i0) - out << "+"; - out << "c!" << row << "$" << i << " * " - << from_expr(ns, "", templ_row.expr[i].first); + << from_expr(ns, "", templ_row_expr.pre_post_values[i].pre); } out << std::endl; } } void linrank_domaint::project_on_vars( - valuet &value, + domaint::valuet &value, const var_sett &vars, exprt &result) { // don't do any projection - const templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); assert(v.size()==templ.size()); exprt::operandst c; c.reserve(templ.size()); for(unsigned row=0; row true) c.push_back(true_exprt()); } - else if(is_row_value_false(v[row])) + else if(v[row].is_false()) { // (g=> false) c.push_back( implies_exprt( - and_exprt(templ[row].pre_guard, templ[row].post_guard), + and_exprt(templ[row].guards.pre_guard, templ[row].guards.post_guard), false_exprt())); } else { - assert(v[row].c.size()==templ[row].expr.size()); + auto &templ_row_expr=dynamic_cast(*templ[row].expr); + assert(v[row].c.size()==templ_row_expr.pre_post_values.size()); assert(v[row].c.size()>=1); #ifdef DIFFERENCE_ENCODING exprt sum=mult_exprt( v[row].c[0], - minus_exprt(templ[row].expr[0].first, templ[row].expr[0].second)); + minus_exprt( + templ_row_expr.pre_post_values[0].pre, + templ_row_expr.pre_post_values[0].post)); #else - exprt sum_pre=mult_exprt(v[row].c[0], templ[row].expr[0].first); - exprt sum_post=mult_exprt(v[row].c[0], templ[row].expr[0].second); + exprt sum_pre=mult_exprt( + value[row].c[0], templ_row_expr.pre_post_values[0].pre); + exprt sum_post=mult_exprt( + value[row].c[0], templ_row_expr.pre_post_values[0].post); #endif for(unsigned i=1; ikind==LOOP) + if(v->guards.kind==guardst::LOOP) { has_loop=true; break; @@ -524,7 +453,9 @@ void linrank_domaint::add_template( templ.reserve(templ.size()+1); templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.kind=LOOP; + templ_row.expr=std::unique_ptr(new template_row_exprt()); + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + templ_row.guards.kind=guardst::LOOP; exprt::operandst preg; exprt::operandst postg; @@ -532,27 +463,39 @@ void linrank_domaint::add_template( for(var_specst::const_iterator v=var_specs.begin(); v!=var_specs.end(); v++) { - if(v->kind!=LOOP) + if(v->guards.kind!=guardst::LOOP) continue; - preg.push_back(v->pre_guard); - postg.push_back(v->post_guard); + preg.push_back(v->guards.pre_guard); + postg.push_back(v->guards.post_guard); exprt vpost=v->var; // copy rename(vpost); - templ_row.expr.push_back(std::pair(v->var, vpost)); + templ_row_expr.pre_post_values.emplace_back(v->var, vpost); } - templ_row.pre_guard=conjunction(preg); - templ_row.post_guard=conjunction(postg); + templ_row.guards.pre_guard=conjunction(preg); + templ_row.guards.post_guard=conjunction(postg); } -bool linrank_domaint::is_row_value_false(const row_valuet & row_value) const +void linrank_domaint::template_row_exprt::output( + std::ostream &out, + const namespacet &ns) const { - assert(row_value.c.size()>=1); - return row_value.c[0].get(ID_value)==ID_false; + for(unsigned i=0; i0) + out << "+"; + out << "c!" << row << "$" << i << " * " + << from_expr(ns, "", pre_post_values[i].pre); + } } -bool linrank_domaint::is_row_value_true(const row_valuet & row_value) const +std::vector linrank_domaint::template_row_exprt::get_row_exprs() { - assert(row_value.c.size()>=1); - return row_value.c[0].get(ID_value)==ID_true; + std::vector exprs; + for(auto &pre_post : pre_post_values) + { + exprs.push_back(pre_post.pre); + exprs.push_back(pre_post.post); + } + return exprs; } diff --git a/src/domains/linrank_domain.h b/src/domains/linrank_domain.h index c32e8480c..2a3aaeb61 100644 --- a/src/domains/linrank_domain.h +++ b/src/domains/linrank_domain.h @@ -23,32 +23,56 @@ Author: Peter Schrammel #include #include -#include "domain.h" +#include "simple_domain.h" -class linrank_domaint:public domaint +class linrank_domaint:public simple_domaint { public: - typedef unsigned rowt; - typedef std::vector > pre_post_valuest; - typedef pre_post_valuest row_exprt; - typedef struct + struct template_row_exprt:simple_domaint::template_row_exprt { - std::vector c; - } row_valuet; + struct pre_post_valuet + { + exprt pre; + exprt post; + + pre_post_valuet(const exprt &pre, const exprt &post): + pre(pre), post(post) {} + }; + + std::vector pre_post_values; + rowt row; - class templ_valuet:public domaint::valuet, public std::vector + std::vector get_row_exprs() override; + void output(std::ostream &out, const namespacet &ns) const override; + }; + + struct row_valuet { + std::vector c; + + void set_to_true() + { + c.clear(); + c.push_back(true_exprt()); + } + bool is_true() const { return c[0].get(ID_value)==ID_true; } + bool is_false() const { return c[0].get(ID_value)==ID_false; } }; - typedef struct + struct templ_valuet:simple_domaint::valuet, std::vector { - guardt pre_guard; - guardt post_guard; - row_exprt expr; - kindt kind; - } template_rowt; + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override + { + return true_exprt(); + } + + templ_valuet *clone() override { return new templ_valuet(*this); } + }; - typedef std::vector templatet; + std::unique_ptr new_value() override + { + return std::unique_ptr(new templ_valuet()); + } linrank_domaint( unsigned _domain_number, @@ -56,7 +80,7 @@ class linrank_domaint:public domaint unsigned _max_elements, // lexicographic components unsigned _max_inner_iterations, const namespacet &_ns): - domaint(_domain_number, _renaming_map, _ns), + simple_domaint(_domain_number, _renaming_map, _ns), refinement_level(0), max_elements(_max_elements), max_inner_iterations(_max_inner_iterations), @@ -64,76 +88,50 @@ class linrank_domaint:public domaint { inner_solver=incremental_solvert::allocate(_ns); } - // initialize value - virtual void initialize(valuet &value); - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); + // initialize value + void initialize_value(domaint::valuet &value) override; - bool edit_row(const rowt &row, valuet &inv, bool improved); + bool edit_row(const rowt &row, valuet &inv, bool improved) override; - exprt to_pre_constraints(valuet &_value); + exprt to_pre_constraints(const valuet &_value) override; void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); + const valuet &_value, + exprt::operandst &cond_exprs) override; - bool handle_unsat(valuet &value, bool improved); + bool handle_unsat(valuet &value, bool improved) override; - virtual bool refine(); + bool refine() override; exprt get_row_symb_constraint( row_valuet &symb_values, // contains vars c const rowt &row, exprt &refinement_constraint); - // set, get value - row_valuet get_row_value(const rowt &row, const templ_valuet &value); - void set_row_value( - const rowt &row, - const row_valuet &row_value, - templ_valuet &value); - void set_row_value_to_true(const rowt &row, templ_valuet &value); - // printing - virtual void output_value( - std::ostream &out, - const valuet &value, - const namespacet &ns) const; - virtual void output_domain( + void output_value( std::ostream &out, - const namespacet &ns) const; + const domaint::valuet &value, + const namespacet &ns) const override; // projection - virtual void project_on_vars( - valuet &value, + void project_on_vars( + domaint::valuet &value, const var_sett &vars, - exprt &result); - - unsigned template_size() { return templ.size(); } + exprt &result) override; // generating templates void add_template( const var_specst &var_specs, const namespacet &ns); - templatet templ; - exprt value; unsigned refinement_level; // the "inner" solver const unsigned max_elements; // lexicographic components const unsigned max_inner_iterations; incremental_solvert *inner_solver; unsigned number_inner_iterations; - - -protected: - pre_post_valuest values; - - bool is_row_value_false(const row_valuet & row_value) const; - bool is_row_value_true(const row_valuet & row_value) const; -public: - std::vector strategy_value_exprs; }; #endif // CPROVER_2LS_DOMAINS_LINRANK_DOMAIN_H diff --git a/src/domains/predabs_domain.cpp b/src/domains/predabs_domain.cpp index 3423e7260..7a6fa189b 100644 --- a/src/domains/predabs_domain.cpp +++ b/src/domains/predabs_domain.cpp @@ -25,9 +25,9 @@ Author: Peter Schrammel #define SYMB_COEFF_VAR "symb_coeff#" #define COMPLEXITY_COUNTER_PREFIX "__CPROVER_CPLX_CNT_" -void predabs_domaint::initialize(valuet &value) +void predabs_domaint::initialize_value(domaint::valuet &value) { - templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); v.resize(templ.size()); for(std::size_t row=0; row predabs_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - return r; -} - -void predabs_domaint::set_smt_values(std::vector got_values, size_t row) -{ -} - bool predabs_domaint::edit_row(const rowt &row, valuet &inv, bool improved) { todo_notpreds.insert(*e_it); return true; } -void predabs_domaint::post_edit() +void predabs_domaint::finalize_solver_iteration() { todo_preds.erase(e_it); } bool predabs_domaint::handle_unsat(valuet &value, bool improved) { - set_row_value(*e_it, true_exprt(), value); + dynamic_cast(value).set_row_value(*e_it, true_exprt()); return true; } -exprt predabs_domaint::make_permanent(valuet &value) +exprt predabs_domaint::get_permanent_expr(valuet &value) { exprt to_r=to_pre_constraints(value); todo_preds.insert(todo_notpreds.begin(), todo_notpreds.end()); @@ -91,240 +77,30 @@ exprt predabs_domaint::make_permanent(valuet &value) return to_r; } -/// pre_guard==> (row_value=> row_expr) -exprt predabs_domaint::get_row_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row (row_value=> row_expr) -exprt predabs_domaint::get_row_pre_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row (row_value=> row_expr) -exprt predabs_domaint::get_row_pre_constraint( - const rowt &row, - const templ_valuet &value) -{ - assert(value.size()==templ.size()); - return get_row_pre_constraint(row, value[row]); -} - -/// post_guard=> (row_value=> row_expr) -exprt predabs_domaint::get_row_post_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row (row_value=> row_expr) -exprt predabs_domaint::get_row_post_constraint( - const rowt &row, - const templ_valuet &value) -{ - assert(value.size()==templ.size()); - return get_row_post_constraint(row, value[row]); -} - /// /\_all_rows ( pre_guard==> (row_value=> row_expr) ) -exprt predabs_domaint::to_pre_constraints(valuet &_value) -{ - assert(*e_it (row_value=> row_expr) ) to be connected -/// disjunctively -void predabs_domaint::make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs) -{ - predabs_domaint::templ_valuet &value= - static_cast(_value); - assert(value.size()==templ.size()); - cond_exprs.resize(templ.size()); - - exprt::operandst c; - for(std::size_t row=0; row(value); - - assert(v.size()==templ.size()); - exprt::operandst c; - for(std::size_t row=0; row symbols; - find_symbols(templ_row.expr, symbols); - - bool pure=true; - for(const auto &symbol : symbols) - { - if(vars.find(symbol)==vars.end()) - { - pure=false; - break; - } - } - if(!pure) - continue; - - const row_valuet &row_v=v[row]; - if(templ_row.kind==LOOP) - { - c.push_back( - implies_exprt( - templ_row.pre_guard, - implies_exprt(row_v, templ_row.expr))); - } - else - { - c.push_back(implies_exprt(row_v, templ_row.expr)); - } + // Pre-constraint is (true => row_expr) + c=implies_exprt( + true_exprt(), + dynamic_cast(*templ[*e_it].expr)); } - result=conjunction(c); -} - -void predabs_domaint::set_row_value( - const rowt &row, - const predabs_domaint::row_valuet &row_value, - valuet &_value) -{ - predabs_domaint::templ_valuet &value= - static_cast(_value); - assert(row(value); - for(std::size_t row=0; row " << std::endl << " "; - break; - case IN: out << "(IN) "; break; - case OUT: case OUTL: out << "(OUT) "; break; - default: assert(false); - } - out << "( " << from_expr(ns, "", v[row]) << "==> " << - from_expr(ns, "", templ_row.expr) << " )" << std::endl; - } -} - -void predabs_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - for(std::size_t row=0; row " << std::endl << " "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", templ_row.pre_guard) - << "===> " << std::endl << " "; - break; - case OUT: case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", templ_row.post_guard) - << "===> " << std::endl << " "; - break; - default: assert(false); - } - out << "( " << from_expr(ns, "", templ_row.expr) << ")" << std::endl; - } -} - -unsigned predabs_domaint::template_size() -{ - return templ.size(); + return c; } predabs_domaint::template_rowt &predabs_domaint::add_template_row( - const exprt& expr, - const exprt& pre_guard, - const exprt& post_guard, - const exprt& aux_expr, - kindt kind - ) + const exprt &expr, + const guardst &guards) { templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.expr=expr; + templ_row.expr=std::unique_ptr( + new template_row_exprt(expr)); // extend_expr_types(templ_row.expr); - templ_row.pre_guard=pre_guard; - templ_row.post_guard=post_guard; - templ_row.aux_expr=aux_expr; - templ_row.kind=kind; + templ_row.guards=guards; return templ_row; } @@ -333,3 +109,10 @@ void predabs_domaint::get_row_set(std::set &rows) for(std::size_t i=0; i #include -#include "domain.h" +#include "simple_domain.h" -class predabs_domaint:public domaint +class predabs_domaint:public simple_domaint { public: typedef unsigned rowt; - typedef exprt row_exprt; // predicate - typedef constant_exprt row_valuet; // true/false - typedef std::set row_sett; - class templ_valuet:public domaint::valuet, public std::vector + struct template_row_exprt:simple_domaint::template_row_exprt, exprt { + explicit template_row_exprt(const exprt &expr):exprt(expr) {} + + std::vector get_row_exprs() override { return {*this}; } + void output(std::ostream &out, const namespacet &ns) const override; }; - typedef struct + typedef constant_exprt row_valuet; + + struct templ_valuet:simple_domaint::valuet, std::vector { - guardt pre_guard; - guardt post_guard; - row_exprt expr; - exprt aux_expr; - kindt kind; - } template_rowt; + void set_row_value(rowt row, const constant_exprt &value) + { + (*this)[row]=value; + } + + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override + { + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + // row_value => row_expr + return implies_exprt((*this)[row], templ_row_expr); + } + + templ_valuet *clone() override { return new templ_valuet(*this); } + }; - typedef std::vector templatet; + std::unique_ptr new_value() override + { + return std::unique_ptr(new templ_valuet()); + } predabs_domaint( unsigned _domain_number, replace_mapt &_renaming_map, - const namespacet _ns): - domaint(_domain_number, _renaming_map, _ns) - { - } + const namespacet &_ns): + simple_domaint(_domain_number, _renaming_map, _ns) {} - const exprt initialize_solver( - const local_SSAt &SSA, - const exprt &precondition, - template_generator_baset &template_generator); + void initialize() override; // initialize value - virtual void initialize(valuet &value); - - virtual void solver_iter_init(valuet &value); + void initialize_value(domaint::valuet &value) override; - virtual bool has_something_to_solve(); + void init_value_solver_iteration(domaint::valuet &value) override; - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); + bool has_something_to_solve() override; - bool edit_row(const rowt &row, valuet &inv, bool improved); + bool edit_row(const rowt &row, valuet &inv, bool improved) override; - void post_edit(); + void finalize_solver_iteration() override; - exprt to_pre_constraints(valuet &_value); + exprt to_pre_constraints(const valuet &_value) override; - void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); + bool handle_unsat(valuet &value, bool improved) override; - bool handle_unsat(valuet &value, bool improved); - - exprt make_permanent(valuet &value); - - // value -> constraints - exprt get_row_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_pre_constraint(const rowt &row, const templ_valuet &value); - exprt get_row_post_constraint(const rowt &row, const templ_valuet &value); - - // set, get value - row_valuet get_row_value(const rowt &row, const templ_valuet &value); - void set_row_value( - const rowt &row, - const row_valuet &row_value, - valuet &_value); - - // printing - virtual void output_value( - std::ostream &out, - const valuet &value, - const namespacet &ns) const; - virtual void output_domain(std::ostream &out, const namespacet &ns) const; - - // projection - virtual void project_on_vars( - valuet &value, - const var_sett &vars, - exprt &result); - - unsigned template_size(); + exprt get_permanent_expr(valuet &value) override; // generating templates - template_rowt &add_template_row( - const exprt& expr, - const exprt& pre_guard, - const exprt& post_guard, - const exprt& aux_expr, - kindt kind); + template_rowt &add_template_row(const exprt &expr, const guardst &guards); - void get_row_set(row_sett &rows); + void get_row_set(std::set &rows); -protected: - templatet templ; - exprt value; - -public: typedef std::set worklistt; worklistt::iterator e_it; worklistt todo_preds; diff --git a/src/domains/product_domain.cpp b/src/domains/product_domain.cpp new file mode 100644 index 000000000..2137b70a0 --- /dev/null +++ b/src/domains/product_domain.cpp @@ -0,0 +1,98 @@ +/*******************************************************************\ + +Module: Generic product combination domain + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic product combination domain +/// Can combine arbitrary number of abstract domains side-by-side. +/// Invariant is a conjunction of invariants of individual domains. +/// Designed to work with strategy_solver_productt. + +#include "product_domain.h" +#include "strategy_solver_product.h" + +void product_domaint::initialize_value(domaint::valuet &_value) +{ + auto &inv=dynamic_cast(_value); + for(unsigned i=0; iinitialize_value(*inv[i]); +} + +void product_domaint::output_domain( + std::ostream &out, + const namespacet &ns) const +{ + for(auto &domain : domains) + domain->output_domain(out, ns); +} + +void product_domaint::output_value( + std::ostream &out, + const domaint::valuet &_value, + const namespacet &ns) const +{ + auto &inv=dynamic_cast(_value); + for(unsigned i=0; ioutput_value(out, *inv[i], ns); +} + +/// Project onto a set of variables. The overall invariant is a conjunction of +/// invariants of inner domains. +void product_domaint::project_on_vars( + domaint::valuet &_value, + const var_sett &vars, + exprt &result) +{ + auto &inv=dynamic_cast(_value); + exprt::operandst c; + for(unsigned i=0; iproject_on_vars(*inv[i], vars, domain_result); + c.push_back(domain_result); + } + result=conjunction(c); +} + +void product_domaint::restrict_to_sympath(const symbolic_patht &sympath) +{ + for(auto &domain : domains) + domain->restrict_to_sympath(sympath); +} + +void product_domaint::eliminate_sympaths( + const std::vector &sympaths) +{ + for(auto &domain : domains) + domain->eliminate_sympaths(sympaths); +} + +void product_domaint::undo_sympath_restriction() +{ + for(auto &domain : domains) + domain->undo_sympath_restriction(); +} + +void product_domaint::remove_all_sympath_restrictions() +{ + for(auto &domain : domains) + domain->remove_all_sympath_restrictions(); +} + +std::unique_ptr product_domaint::new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) +{ + solver_vect solvers; + for(auto &d : domains) + solvers.push_back( + std::move(d->new_strategy_solver(solver, SSA, message_handler))); + return std::unique_ptr( + new strategy_solver_productt( + *this, std::move(solvers), solver, SSA, message_handler)); +} diff --git a/src/domains/product_domain.h b/src/domains/product_domain.h new file mode 100644 index 000000000..1b62afe4e --- /dev/null +++ b/src/domains/product_domain.h @@ -0,0 +1,101 @@ +/*******************************************************************\ + +Module: Generic product combination domain + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic product combination domain +/// Can combine arbitrary number of abstract domains side-by-side. +/// Invariant is a conjunction of invariants of individual domains. +/// Designed to work with strategy_solver_productt. + +#ifndef CPROVER_2LS_DOMAINS_PRODUCT_DOMAIN_H +#define CPROVER_2LS_DOMAINS_PRODUCT_DOMAIN_H + +#include "domain.h" +#include "strategy_solver_base.h" +#include + +typedef std::vector> domain_vect; +typedef std::vector> value_vect; + +class product_domaint:public domaint +{ +public: + product_domaint( + unsigned int domainNumber, + replace_mapt &renamingMap, + const namespacet &ns, + domain_vect domains): + domaint(domainNumber, renamingMap, ns), domains(std::move(domains)) {} + + /// Abstract value is a vector of abstract values of inner domains. + /// The order has to match the order of domains. + struct valuet:domaint::valuet, value_vect + { + valuet()=default; + explicit valuet(value_vect values):vector(std::move(values)) {} + + valuet *clone() override + { + auto new_value=new valuet(); + for(const auto &val : *this) + new_value->emplace_back(val->clone()); + return new_value; + } + }; + + std::unique_ptr new_value() override + { + value_vect values; + for(auto &d : domains) + values.push_back(std::move(d->new_value())); + return std::unique_ptr(new valuet(std::move(values))); + } + + // Most of the domain methods are implemented in such way that the + // corresponding method is called for each domain. + + void initialize_value(domaint::valuet &value) override; + void output_domain(std::ostream &out, const namespacet &ns) const override; + + void output_value( + std::ostream &out, + const domaint::valuet &value, + const namespacet &ns) const override; + + void project_on_vars( + domaint::valuet &value, + const var_sett &vars, + exprt &result) override; + + void restrict_to_sympath(const symbolic_patht &sympath) override; + void eliminate_sympaths(const std::vector &sympaths) override; + void undo_sympath_restriction() override; + void remove_all_sympath_restrictions() override; + + /// Get a vector of raw pointers to the inner domains + std::vector get_domains() + { + std::vector result; + for(auto &d : domains) + result.push_back(d.get()); + return result; + } + + std::unique_ptr new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) override; + + // Product domain contains a vector of domains + domain_vect domains; + + // Value is a vector of values in corresponding domains + valuet value; +}; + +#endif // CPROVER_2LS_DOMAINS_PRODUCT_DOMAIN_H diff --git a/src/domains/simple_domain.cpp b/src/domains/simple_domain.cpp new file mode 100644 index 000000000..ebfd12fe2 --- /dev/null +++ b/src/domains/simple_domain.cpp @@ -0,0 +1,243 @@ +/*******************************************************************\ + +Module: Generic simple abstract domain class + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic simple abstract domain class +/// Designed to work with the generic simple strategy solver located in +/// strategy_solver_simplet. +/// Implements a default behaviour for a number of methods that are common for +/// multiple simple abstract domains. + +#include "simple_domain.h" +#include "strategy_solver_simple.h" +#include "util.h" +#include +#include + +/// Get pre constraints from the given value. +/// Default behaviour: make a conjunction of row pre constraints for each +/// template row. +exprt simple_domaint::to_pre_constraints(const valuet &value) +{ + exprt::operandst c; + for(rowt row=0; row row_value_expression +exprt simple_domaint::get_row_pre_constraint(rowt row, const valuet &value) +{ + // For exit variables the result is true + if(templ[row].guards.kind==guardst::OUT || + templ[row].guards.kind==guardst::OUTL) + return true_exprt(); + + auto row_expr=get_row_value_constraint(row, value); + return implies_exprt(templ[row].guards.pre_guard, row_expr); +} + +/// Get post constraints from the given value. +/// Since it is necessary to know which constraint was satisfied by the SMT +/// solver, they are stored in a vector cond_exprs and the strategy solver +/// makes a disjunction of them and passes it to the SMT solver. +/// Post constraints are typically negations of row expressions (to solve the +/// "exists forall" problem). +/// Default behaviour: each template row has its own post constraint. +void simple_domaint::make_not_post_constraints( + const valuet &value, + exprt::operandst &cond_exprs) +{ + for(rowt row=0; rowget_row_exprs()); + for(auto &row_var : strategy_value_exprs[row]) + rename(row_var); + cond_exprs.push_back(get_row_post_constraint(row, value)); + } +} + +/// Get row post constraint for the given row from the given abstract value. +/// Default post constraint: +/// aux_expr && !(post_guard => row_value_expression) +exprt simple_domaint::get_row_post_constraint(rowt row, const valuet &value) +{ + exprt row_post_constraint; + if(templ[row].guards.kind==guardst::IN) + row_post_constraint=true_exprt(); + else + { + auto row_expr=get_row_value_constraint(row, value); + row_post_constraint=implies_exprt(templ[row].guards.post_guard, row_expr); + } + + if(templ[row].guards.kind==guardst::LOOP) + rename(row_post_constraint); + + return and_exprt(templ[row].guards.aux_expr, not_exprt(row_post_constraint)); +} + +/// Get value constraint for the given row. +/// Default is the row expression of the value. +exprt simple_domaint::get_row_value_constraint(rowt row, const valuet &value) +{ + return value.get_row_expr(row, templ[row]); +} + +/// Print the template to the given output stream +void simple_domaint::templatet::output( + std::ostream &out, + const namespacet &ns) const +{ + for(rowt row=0; rowoutput(out, ns); + } +} + +/// Output the domain (its template) +/// Default behaviour: output template. +void simple_domaint::output_domain( + std::ostream &out, + const namespacet &ns) const +{ + templ.output(out, ns); +} + +/// Output the given abstract value in this domain. +/// Default behavior: for each template row, print the row value expression. +void simple_domaint::output_value( + std::ostream &out, + const domaint::valuet &value, + const namespacet &ns) const +{ + auto &simple_value=dynamic_cast(value); + for(rowt row=0; row(value); + exprt::operandst c; + for(rowt row=0; row symbols; + for(auto &row_expr : templ[row].expr->get_row_exprs()) + { + std::set row_expr_symbols; + find_symbols(row_expr, row_expr_symbols); + symbols.insert(row_expr_symbols.begin(), row_expr_symbols.end()); + } + + // If any of the symbols is not in vars and vars is not empty, continue + if(!vars.empty() && std::any_of( + symbols.begin(), symbols.end(), + [&vars](const symbol_exprt &s) + { + return vars.find(s)==vars.end(); + })) + continue; + + if(templ[row].guards.kind==guardst::LOOP) + c.push_back(get_row_pre_constraint(row, simple_value)); + else + c.push_back(get_row_value_constraint(row, simple_value)); + } + + result=conjunction(c); +} + +/// Return the loop guard for the given template row. +/// By default, it is the second conjunct in the row pre-guard. +exprt simple_domaint::get_current_loop_guard(rowt row) +{ + if(templ[row].guards.pre_guard.id()==ID_and) + return to_and_expr(templ[row].guards.pre_guard).op1(); + + return true_exprt(); +} + +/// Restrict the template to the given symbolic path. +/// Default behaviour: for each template row, add all loop guards from the +/// symbolic path (except for the loop guard corresponding to the row) +/// to aux_expr. +void simple_domaint::restrict_to_sympath(const symbolic_patht &sympath) +{ + for(rowt row=0; row &sympaths) +{ + for(rowt row=0; row(true_exprt()) + : not_exprt(disjunction(paths)); + } +} + +/// Undo the last symbolic path restriction +/// Default behaviour: for each template row, remove the second conjunct +/// from aux_expr. +void simple_domaint::undo_sympath_restriction() +{ + for(auto &row : templ) + { + if(row.guards.aux_expr.id()==ID_and) + row.guards.aux_expr=to_and_expr(row.guards.aux_expr).op0(); + } +} + +/// Remove all symbolic path restrictions. +/// Default behaviour: for each template row, clear aux_expr. +void simple_domaint::remove_all_sympath_restrictions() +{ + for(auto &row : templ) + row.guards.aux_expr=true_exprt(); +} + +std::unique_ptr simple_domaint::new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) +{ + return std::unique_ptr( + new strategy_solver_simplet(*this, solver, SSA, message_handler)); +} diff --git a/src/domains/simple_domain.h b/src/domains/simple_domain.h new file mode 100644 index 000000000..6d01933b9 --- /dev/null +++ b/src/domains/simple_domain.h @@ -0,0 +1,180 @@ +/*******************************************************************\ + +Module: Generic simple abstract domain class + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic simple abstract domain class +/// Designed to work with the generic simple strategy solver located in +/// strategy_solver_simplet. +/// Implements a default behaviour for a number of methods that are common for +/// multiple simple abstract domains. + +#ifndef CPROVER_2LS_DOMAINS_SIMPLE_DOMAIN_H +#define CPROVER_2LS_DOMAINS_SIMPLE_DOMAIN_H + +#include "domain.h" +#include + +class simple_domaint:public domaint +{ +public: + simple_domaint( + unsigned domain_number, + replace_mapt &renaming_map, + const namespacet &ns): + domaint(domain_number, renaming_map, ns) {} + + typedef unsigned rowt; + + /// Template row expression - defined per-domain + struct template_row_exprt + { + /// Get a vector of expressions used in the row + virtual std::vector get_row_exprs()=0; + /// Output the template row (with the template row parameters) + virtual void output(std::ostream &out, const namespacet &ns) const=0; + }; + + /// Template row + /// Contains a row expression (defined per-domain) and row guards. + struct template_rowt + { + // The expression is defined as unique_ptr to enable polymorphism + std::unique_ptr expr; + guardst guards; + }; + + /// Template is a vector of template rows + struct templatet:std::vector + { + /// Output the domain template + virtual void output(std::ostream &out, const namespacet &ns) const; + }; + + templatet templ; + + struct valuet:domaint::valuet + { + /// Get expression corresponding to the current value of the given template + /// row parameter. + virtual exprt get_row_expr( + rowt row, + const template_rowt &templ_row) const=0; + }; + + /// Domain should return true if it wants to improve its invariants. + /// Otherwise no further improvements of invariants is done. + virtual bool has_something_to_solve() { return true; } + + /// Edit invariant based on the current model of satisfiability. + /// Every domain should implement this function. + virtual bool edit_row(const rowt &row, valuet &inv, bool improved)=0; + + /// Get expression that should be made permanent in the SMT solver. + /// This method is called after each iteration of strategy solver. + virtual exprt get_permanent_expr(valuet &value) { return true_exprt(); } + + /// Called when the model is unsatisfiable + /// Returns true if the invariant should be further improved. + virtual bool handle_unsat(valuet &value, bool improved) { return improved; } + + // Pre- and post- constraints + + /// Get pre constraints from the given value. + /// Default behaviour: make a conjunction of row pre constraints for each + /// template row. + virtual exprt to_pre_constraints(const valuet &value); + + /// Get row pre constraint for the given row from the given abstract value. + /// Default row pre constraint: + /// pre_guard => row_value_expression + virtual exprt get_row_pre_constraint(rowt row, const valuet &value); + + /// Get post constraints from the given value. + /// Since it is necessary to know which constraint was satisfied by the SMT + /// solver, they are stored in a vector cond_exprs and the strategy solver + /// makes a disjunction of them and passes it to the SMT solver. + /// Post constraints are typically negations of row expressions (to solve the + /// "exists forall" problem). + /// Default behaviour: each template row has its own post constraint. + virtual void make_not_post_constraints( + const valuet &value, + exprt::operandst &cond_exprs); + + /// Get row post constraint for the given row from the given abstract value. + /// Default post constraint: + /// aux_expr && !(post_guard => row_value_expression) + virtual exprt get_row_post_constraint(rowt row, const valuet &value); + + /// Get value constraint for the given row. + /// Default is the row expression of the value. + virtual exprt get_row_value_constraint(rowt row, const valuet &value); + + /// Output the domain (its template) + /// Default behaviour: output template. + void output_domain(std::ostream &out, const namespacet &ns) const override; + + /// Output the given abstract value in this domain. + /// Default behavior: for each template row, print the row value expression. + void output_value( + std::ostream &out, + const domaint::valuet &value, + const namespacet &ns) const override; + + /// Project invariant (abstract value) onto a set of variables. + /// Default behaviour: result is a conjunction of expressions of all template + /// row such that all symbols occurring in the row expression are in vars + /// Here, the projected expression is: + /// pre_constraint for LOOP rows + /// value_row_expression for IN and OUT rows + // (not useful to make value const (e.g. union-find)) + void project_on_vars( + domaint::valuet &value, + const var_sett &vars, + exprt &result) override; + + /// Return the loop guard for the given template row. + /// By default, it is the second conjunct in the row pre-guard. + virtual exprt get_current_loop_guard(rowt row); + /// Restrict the template to the given symbolic path. + /// Default behaviour: for each template row, add all loop guards from the + /// symbolic path (except for the loop guard corresponding to the row) + /// to aux_expr. + void restrict_to_sympath(const symbolic_patht &sympath) override; + /// Restrict template to any other paths than those specified. + void eliminate_sympaths(const std::vector &sympaths) override; + /// Undo the last symbolic path restriction + /// Default behaviour: for each template row, remove the second conjunct + /// from aux_expr. + void undo_sympath_restriction() override; + /// Remove all symbolic path restrictions. + /// Default behaviour: for each template row, clear aux_expr. + void remove_all_sympath_restrictions() override; + + // returns true as long as further refinements are possible + virtual void reset_refinements() {} + + virtual bool refine() { return false; } + + std::unique_ptr new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) override; + +protected: + // handles on values to retrieve from model + // each row has a condition literal and a vector of value expressions + bvt strategy_cond_literals; + std::vector strategy_value_exprs; + // values of value expressions for the current row retrieved from the model + exprt::operandst smt_model_values; + + friend class strategy_solver_simplet; +}; + + +#endif // CPROVER_2LS_DOMAINS_SIMPLE_DOMAIN_H diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 2ff5ed8bb..a84a4cc70 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -31,13 +31,22 @@ Author: Peter Schrammel #include "predabs_domain.h" #include "template_generator_ranking.h" #include "ssa_analyzer.h" -#include "strategy_solver_heap_tpolyhedra.h" -#include "strategy_solver_heap_tpolyhedra_sympath.h" -#include "strategy_solver.h" +#include "strategy_solver_sympath.h" +#include "strategy_solver_simple.h" +#include "heap_domain.h" +#include "strategy_solver_product.h" // NOLINTNEXTLINE(*) +#define SIMPLE_SOLVER(domain_ptr, domain_type) strategy_solver_simplet(\ + *dynamic_cast(domain_ptr), \ + solver, \ + SSA, \ + get_message_handler()) #define BINSEARCH_SOLVER strategy_solver_binsearcht(\ - *static_cast(domain), solver, SSA.ns) + *dynamic_cast(simple_domains[next_domain++]), \ + solver, \ + SSA, \ + get_message_handler()) #if 0 // NOLINTNEXTLINE(*) #define BINSEARCH_SOLVER strategy_solver_binsearch2t(\ @@ -67,120 +76,12 @@ void ssa_analyzert::operator()( domain=template_generator.domain(); - // get strategy solver from options - strategy_solver_baset *s_solver; - if(template_generator.options.get_bool_option("compute-ranking-functions")) - { - if(template_generator.options.get_bool_option( - "monolithic-ranking-function")) - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new linrank_domaint::templ_valuet(); - } - else - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new lexlinrank_domaint::templ_valuet(); - } - } - else if(template_generator.options.get_bool_option("equalities")) - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new equality_domaint::equ_valuet(); - } - else if(template_generator.options.get_bool_option("heap")) - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new heap_domaint::heap_valuet(); - } - else if(template_generator.options.get_bool_option("heap-interval") - || template_generator.options.get_bool_option("heap-zones")) - { - if(template_generator.options.get_bool_option("sympath")) - { - s_solver=new strategy_solver_heap_tpolyhedra_sympatht( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result= - new heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet(); - } - else - { - s_solver=new strategy_solver_heap_tpolyhedrat( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new heap_tpolyhedra_domaint::heap_tpolyhedra_valuet(); - } - } - else - { - if(template_generator.options.get_bool_option("enum-solver")) - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new tpolyhedra_domaint::templ_valuet(); - } - else if(template_generator.options.get_bool_option("predabs-solver")) - { - s_solver=new strategy_solvert( - *static_cast(domain), - solver, - SSA, - precondition, - get_message_handler(), - template_generator); - result=new predabs_domaint::templ_valuet(); - } - else if(template_generator.options.get_bool_option("binsearch-solver")) - { - result=new tpolyhedra_domaint::templ_valuet(); - s_solver=new BINSEARCH_SOLVER; - } - else - assert(false); - } - - s_solver->set_message_handler(get_message_handler()); + // Get a strategy solver and a new abstract value (invariant) + auto s_solver=domain->new_strategy_solver(solver, SSA, get_message_handler()); + result=domain->new_value(); // initialize inv - domain->initialize(*result); + domain->initialize_value(*result); // iterate while(s_solver->iterate(*result)) {} @@ -191,24 +92,9 @@ void ssa_analyzert::operator()( solver_instances+=s_solver->get_number_of_solver_instances(); solver_calls+=s_solver->get_number_of_solver_calls(); solver_instances+=s_solver->get_number_of_solver_instances(); - - delete s_solver; } -void ssa_analyzert::get_result(exprt &_result, const domaint::var_sett &vars) +void ssa_analyzert::get_result(exprt &_result, const var_sett &vars) { domain->project_on_vars(*result, vars, _result); } - -void ssa_analyzert::update_heap_out(summaryt::var_sett &out) -{ - heap_domaint &heap_domain=static_cast(*domain); - - auto new_heap_vars=heap_domain.get_new_heap_vars(); - out.insert(new_heap_vars.begin(), new_heap_vars.end()); -} - -const exprt ssa_analyzert::input_heap_bindings() -{ - return static_cast(*domain).get_iterator_bindings(); -} diff --git a/src/domains/ssa_analyzer.h b/src/domains/ssa_analyzer.h index cff07ed73..9843b4e24 100644 --- a/src/domains/ssa_analyzer.h +++ b/src/domains/ssa_analyzer.h @@ -26,36 +26,20 @@ class ssa_analyzert:public messaget typedef strategy_solver_baset::constraintst constraintst; typedef strategy_solver_baset::var_listt var_listt; - ssa_analyzert(): - result(NULL), - solver_instances(0), - solver_calls(0) - { - } - - ~ssa_analyzert() - { - if(result!=NULL) - delete result; - } - void operator()( incremental_solvert &solver, local_SSAt &SSA, const exprt &precondition, template_generator_baset &template_generator); - void get_result(exprt &result, const domaint::var_sett &vars); - - void update_heap_out(summaryt::var_sett &out); - const exprt input_heap_bindings(); + void get_result(exprt &result, const var_sett &vars); inline unsigned get_number_of_solver_instances() { return solver_instances; } inline unsigned get_number_of_solver_calls() { return solver_calls; } protected: - domaint *domain; // template generator is responsable for the domain object - domaint::valuet *result; + domaint *domain; // template generator is responsible for the domain object + std::unique_ptr result; // statistics unsigned solver_instances; diff --git a/src/domains/strategy_solver_base.cpp b/src/domains/strategy_solver_base.cpp index 9ab71d329..e4a017b83 100644 --- a/src/domains/strategy_solver_base.cpp +++ b/src/domains/strategy_solver_base.cpp @@ -33,3 +33,17 @@ void strategy_solver_baset::find_symbolic_path( symbolic_path[guard.first]=false; } } + +/// Function for printing out the value assigned to an expression and to all its +/// subexpressions by the SMT solver. +void strategy_solver_baset::debug_smt_model( + const exprt &expr, + const namespacet &ns) +{ + std::cerr << from_expr(ns, "", expr) << ": " + << from_expr(ns, "", solver.solver->get(expr)) << "\n"; + forall_operands(op, expr) + { + debug_smt_model(*op, ns); + } +} diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h index 547f78819..44ec1a6e9 100644 --- a/src/domains/strategy_solver_base.h +++ b/src/domains/strategy_solver_base.h @@ -26,12 +26,13 @@ class strategy_solver_baset:public messaget explicit strategy_solver_baset( incremental_solvert &_solver, - const namespacet &_ns): + const local_SSAt &SSA, + message_handlert &message_handler): + messaget(message_handler), solver(_solver), - ns(_ns), + SSA(SSA), solver_instances(0), - solver_calls(0) - {} + solver_calls(0) {} virtual bool iterate(invariantt &inv) { assert(false); } @@ -40,21 +41,31 @@ class strategy_solver_baset:public messaget symbolic_patht symbolic_path; + /// Notify the solver that symbolic paths are used + virtual void use_sympaths() { with_sympaths=true; } + /// Set symbolic path of this and all innner solvers + virtual void set_sympath(const symbolic_patht &sympath) + { + symbolic_path=sympath; + } + /// Clear the current symbolic path + virtual void clear_symbolic_path() {symbolic_path.clear(); } + protected: incremental_solvert &solver; - const namespacet &ns; - - // handles on values to retrieve from model - bvt strategy_cond_literals; - exprt::operandst strategy_value_exprs; + const local_SSAt &SSA; // statistics for additional solvers unsigned solver_instances; unsigned solver_calls; + bool with_sympaths; + void find_symbolic_path( std::set> &loop_guards, const exprt ¤t_guard=nil_exprt()); + + void debug_smt_model(const exprt &expr, const namespacet &ns); }; #endif diff --git a/src/domains/strategy_solver_binsearch.cpp b/src/domains/strategy_solver_binsearch.cpp index 6297aa698..4f418e137 100644 --- a/src/domains/strategy_solver_binsearch.cpp +++ b/src/domains/strategy_solver_binsearch.cpp @@ -14,6 +14,7 @@ Author: Peter Schrammel #endif #include "strategy_solver_binsearch.h" +#include "ssa/local_ssa.h" #include "util.h" bool strategy_solver_binsearcht::iterate(invariantt &_inv) @@ -119,8 +120,9 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv) tpolyhedra_domaint::row_valuet upper= tpolyhedra_domain.get_max_row_value(row); - tpolyhedra_domaint::row_valuet lower= - simplify_const(solver.get(tpolyhedra_domain.strategy_value_exprs[row])); + tpolyhedra_domaint::row_valuet lower=tpolyhedra_domaint::row_valuet( + simplify_const( + solver.get(tpolyhedra_domain.strategy_value_exprs[row][0]))); solver.pop_context(); // improvement check @@ -220,11 +222,11 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv) solver.pop_context(); // binary search iteration } - debug() << "update value: " << from_expr(ns, "", lower) << eom; + debug() << "update value: " << from_expr(SSA.ns, "", lower) << eom; solver.pop_context(); // symbolic value system - tpolyhedra_domain.set_row_value(row, lower, inv); + inv[row]=lower; improved=true; } else diff --git a/src/domains/strategy_solver_binsearch.h b/src/domains/strategy_solver_binsearch.h index bb87a53f4..b25bca20b 100644 --- a/src/domains/strategy_solver_binsearch.h +++ b/src/domains/strategy_solver_binsearch.h @@ -21,11 +21,10 @@ class strategy_solver_binsearcht:public strategy_solver_baset strategy_solver_binsearcht( tpolyhedra_domaint &_tpolyhedra_domain, incremental_solvert &_solver, - const namespacet &_ns): - strategy_solver_baset(_solver, _ns), - tpolyhedra_domain(_tpolyhedra_domain) - { - } + const local_SSAt &SSA, + message_handlert &message_handler): + strategy_solver_baset(_solver, SSA, message_handler), + tpolyhedra_domain(_tpolyhedra_domain) {} virtual bool iterate(invariantt &inv); diff --git a/src/domains/strategy_solver_binsearch2.cpp b/src/domains/strategy_solver_binsearch2.cpp index 842d6a513..4c6fa4ee9 100644 --- a/src/domains/strategy_solver_binsearch2.cpp +++ b/src/domains/strategy_solver_binsearch2.cpp @@ -20,6 +20,7 @@ Author: Peter Schrammel #include #include "strategy_solver_binsearch2.h" +#include "ssa/local_ssa.h" #include "util.h" #define SUM_BOUND_VAR "sum_bound#" @@ -94,11 +95,10 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) symb_values[row]=tpolyhedra_domain.get_row_symb_value(row); lower_values[row]= simplify_const( - solver.get(tpolyhedra_domain.strategy_value_exprs[row])); + solver.get(tpolyhedra_domain.strategy_value_exprs[row][0])); blocking_constraint.push_back( literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row])); - if(tpolyhedra_domain.is_row_value_neginf( - tpolyhedra_domain.get_row_value(row, inv))) + if(inv[row].is_neg_inf()) improved_from_neginf=true; } } @@ -126,9 +126,9 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) exprt _lower=lower_values[it->first]; #if 1 debug() << "update row " << it->first << ": " - << from_expr(ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values[it->first]) << eom; #endif - tpolyhedra_domain.set_row_value(it->first, lower_values[it->first], inv); + inv[it->first]=lower_values[it->first]; exprt _upper= tpolyhedra_domain.get_max_row_value(it->first); exprt sum=it->second; @@ -140,9 +140,9 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) #if 1 debug() << "update row " << it->first << ": " - << from_expr(ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values[it->first]) << eom; #endif - tpolyhedra_domain.set_row_value(it->first, lower_values[it->first], inv); + inv[it->first]=lower_values[it->first]; } // do not solve system if we have just reached a new loop @@ -156,9 +156,9 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) extend_expr_types(sum); extend_expr_types(_upper); extend_expr_types(_lower); - tpolyhedra_domaint::row_valuet upper=simplify_const(_upper); + auto upper=tpolyhedra_domaint::row_valuet(simplify_const(_upper)); // from_integer(mp_integer(512), _upper.type()); - tpolyhedra_domaint::row_valuet lower=simplify_const(_lower); + auto lower=tpolyhedra_domaint::row_valuet(simplify_const(_lower)); assert(sum.type()==upper.type()); assert(sum.type()==lower.type()); @@ -208,14 +208,14 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) { #if 1 debug() << "update row " << sv.first << " " - << from_expr(ns, "", sv.second) << ": "; + << from_expr(SSA.ns, "", sv.second) << ": "; #endif constant_exprt lower_row= simplify_const(solver.get(sv.second)); #if 1 - debug() << from_expr(ns, "", lower_row) << eom; + debug() << from_expr(SSA.ns, "", lower_row) << eom; #endif - tpolyhedra_domain.set_row_value(sv.first, lower_row, inv); + inv[sv.first]=lower_row; } } else diff --git a/src/domains/strategy_solver_binsearch2.h b/src/domains/strategy_solver_binsearch2.h index 9ad10f53b..18dba8680 100644 --- a/src/domains/strategy_solver_binsearch2.h +++ b/src/domains/strategy_solver_binsearch2.h @@ -23,12 +23,11 @@ class strategy_solver_binsearch2t:public strategy_solver_baset strategy_solver_binsearch2t( tpolyhedra_domaint &_tpolyhedra_domain, incremental_solvert &_solver, - const namespacet &_ns): - strategy_solver_baset(_solver, _ns), + const local_SSAt &SSA, + message_handlert &message_handler): + strategy_solver_baset(_solver, SSA, message_handler), tpolyhedra_domain(_tpolyhedra_domain), - sum_bound_counter(0) - { - } + sum_bound_counter(0) {} virtual bool iterate(invariantt &inv); diff --git a/src/domains/strategy_solver_binsearch3.cpp b/src/domains/strategy_solver_binsearch3.cpp index 9b48c9103..24d1716ea 100644 --- a/src/domains/strategy_solver_binsearch3.cpp +++ b/src/domains/strategy_solver_binsearch3.cpp @@ -90,11 +90,10 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) symb_values[row]=tpolyhedra_domain.get_row_symb_value(row); lower_values[row]= simplify_const( - solver.get(tpolyhedra_domain.strategy_value_exprs[row])); + solver.get(tpolyhedra_domain.strategy_value_exprs[row][0])); blocking_constraint.push_back( literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row])); - if(tpolyhedra_domain.is_row_value_neginf( - tpolyhedra_domain.get_row_value(row, inv))) + if(inv[row].is_neg_inf()) improved_from_neginf=true; } } @@ -122,9 +121,9 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) exprt _lower=lower_values[it->first]; #if 1 debug() << "update row " << it->first << ": " - << from_expr(ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values[it->first]) << eom; #endif - tpolyhedra_domain.set_row_value(it->first, lower_values[it->first], inv); + inv[it->first]=lower_values[it->first]; exprt _upper= tpolyhedra_domain.get_max_row_value(it->first); exprt sum=it->second; @@ -136,9 +135,9 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) #if 1 debug() << "update row " << it->first << ": " - << from_expr(ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values[it->first]) << eom; #endif - tpolyhedra_domain.set_row_value(it->first, lower_values[it->first], inv); + inv[it->first]=lower_values[it->first]; } // do not solve system if we have just reached a new loop @@ -152,15 +151,15 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) #if 1 debug() << "symbolic value system: " << eom; - debug() << "pre-inv: " << from_expr(ns, "", pre_inv_expr) << eom; - debug() << "post-inv: " << from_expr(ns, "", post_inv_expr) << eom; + debug() << "pre-inv: " << from_expr(SSA.ns, "", pre_inv_expr) << eom; + debug() << "post-inv: " << from_expr(SSA.ns, "", post_inv_expr) << eom; #endif extend_expr_types(sum); extend_expr_types(_upper); extend_expr_types(_lower); - tpolyhedra_domaint::row_valuet upper=simplify_const(_upper); - tpolyhedra_domaint::row_valuet lower=simplify_const(_lower); + auto upper=tpolyhedra_domaint::row_valuet(simplify_const(_upper)); + auto lower=tpolyhedra_domaint::row_valuet(simplify_const(_lower)); assert(sum.type()==upper.type()); assert(sum.type()==lower.type()); @@ -170,7 +169,7 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) solver << equal_exprt(sum_bound, sum); #if 1 - debug() << from_expr(ns, "", equal_exprt(sum_bound, sum)) << eom; + debug() << from_expr(SSA.ns, "", equal_exprt(sum_bound, sum)) << eom; #endif while(tpolyhedra_domain.less_than(lower, upper)) @@ -185,15 +184,15 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) exprt c=binary_relation_exprt(sum_bound, ID_ge, middle); #if 1 - debug() << "upper: " << from_expr(ns, "", upper) << eom; - debug() << "middle: " << from_expr(ns, "", middle) << eom; - debug() << "lower: " << from_expr(ns, "", lower) << eom; + debug() << "upper: " << from_expr(SSA.ns, "", upper) << eom; + debug() << "middle: " << from_expr(SSA.ns, "", middle) << eom; + debug() << "lower: " << from_expr(SSA.ns, "", lower) << eom; #endif solver.new_context(); // binary search iteration #if 1 - debug() << "constraint: " << from_expr(ns, "", c) << eom; + debug() << "constraint: " << from_expr(SSA.ns, "", c) << eom; #endif solver << c; @@ -210,14 +209,14 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) { #if 1 debug() << "update row " << sv.first << " " - << from_expr(ns, "", sv.second) << ": "; + << from_expr(SSA.ns, "", sv.second) << ": "; #endif constant_exprt lower_row= simplify_const(solver.get(sv.second)); #if 1 - debug() << from_expr(ns, "", lower_row) << eom; + debug() << from_expr(SSA.ns, "", lower_row) << eom; #endif - tpolyhedra_domain.set_row_value(sv.first, lower_row, inv); + inv[sv.first]=lower_row; } } else diff --git a/src/domains/strategy_solver_binsearch3.h b/src/domains/strategy_solver_binsearch3.h index e15285013..22849bd5d 100644 --- a/src/domains/strategy_solver_binsearch3.h +++ b/src/domains/strategy_solver_binsearch3.h @@ -23,17 +23,15 @@ class strategy_solver_binsearch3t:public strategy_solver_baset explicit strategy_solver_binsearch3t( tpolyhedra_domaint &_tpolyhedra_domain, incremental_solvert &_solver, - local_SSAt& _SSA, - const namespacet &_ns): - strategy_solver_baset(_solver, _ns), - SSA(_SSA), + const local_SSAt& _SSA, + message_handlert &message_handler): + strategy_solver_baset(_solver, SSA, message_handler), tpolyhedra_domain(_tpolyhedra_domain), sum_bound_counter(0) {} virtual bool iterate(invariantt &inv); protected: - local_SSAt &SSA; tpolyhedra_domaint &tpolyhedra_domain; unsigned sum_bound_counter; }; diff --git a/src/domains/strategy_solver_heap_tpolyhedra.cpp b/src/domains/strategy_solver_heap_tpolyhedra.cpp deleted file mode 100644 index 0fd8f9563..000000000 --- a/src/domains/strategy_solver_heap_tpolyhedra.cpp +++ /dev/null @@ -1,65 +0,0 @@ -/*******************************************************************\ - -Module: Strategy solver for combination of shape and template - polyhedra domains. - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Strategy solver for combination of shape and template polyhedra domains. - -#include "strategy_solver_heap_tpolyhedra.h" - -/// Run iteration of each solver separately, but every time in the context of -/// the current invariant found by the other solver. The template polyhedra -/// solving is also restricted to a symbolic path found by the heap solver. -bool strategy_solver_heap_tpolyhedrat::iterate( - strategy_solver_baset::invariantt &_inv) -{ - heap_tpolyhedra_domaint::heap_tpolyhedra_valuet &inv= - static_cast(_inv); - - // Run one iteration of heap solver in the context of invariant from - // the template polyhedra solver - solver.new_context(); - solver << heap_tpolyhedra_domain.polyhedra_domain.to_pre_constraints( - inv.tpolyhedra_value); - bool heap_improved=heap_solver.iterate(inv.heap_value); - solver.pop_context(); - - if(heap_improved) - { - // If heap part was improved, restrict template polyhedra part to the found - // symbolic path - symbolic_path=heap_solver.symbolic_path; - heap_tpolyhedra_domain.polyhedra_domain.restrict_to_sympath(symbolic_path); - } - - // Run one interation of the template polyhedra solver in the context of - // invariant from the heap solver - solver.new_context(); - solver << heap_tpolyhedra_domain.heap_domain.to_pre_constraints( - inv.heap_value); - bool tpolyhedra_improved=tpolyhedra_solver.iterate(inv.tpolyhedra_value); - solver.pop_context(); - - if(heap_improved) - heap_tpolyhedra_domain.polyhedra_domain.undo_restriction(); - - return heap_improved || tpolyhedra_improved; -} - -void strategy_solver_heap_tpolyhedrat::set_message_handler( - message_handlert &_message_handler) -{ - heap_solver.set_message_handler(_message_handler); - tpolyhedra_solver.set_message_handler(_message_handler); -} - -void strategy_solver_heap_tpolyhedrat::clear_symbolic_path() -{ - heap_solver.symbolic_path.clear(); - tpolyhedra_solver.symbolic_path.clear(); -} diff --git a/src/domains/strategy_solver_heap_tpolyhedra.h b/src/domains/strategy_solver_heap_tpolyhedra.h deleted file mode 100644 index 7704c6636..000000000 --- a/src/domains/strategy_solver_heap_tpolyhedra.h +++ /dev/null @@ -1,59 +0,0 @@ -/*******************************************************************\ - -Module: Strategy solver for combination of shape and template - polyhedra domains. - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Strategy solver for combination of shape and template polyhedra domains. - -#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H -#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H - - -#include "strategy_solver_base.h" -#include "heap_tpolyhedra_domain.h" -#include "strategy_solver.h" -#include "strategy_solver_binsearch.h" - -class strategy_solver_heap_tpolyhedrat:public strategy_solver_baset -{ -public: - strategy_solver_heap_tpolyhedrat( - heap_tpolyhedra_domaint &_heap_tpolyhedra_domain, - incremental_solvert &_solver, - const local_SSAt &SSA, - const exprt &precondition, - message_handlert &message_handler, - template_generator_baset &template_generator): - strategy_solver_baset(_solver, SSA.ns), - heap_tpolyhedra_domain(_heap_tpolyhedra_domain), - heap_solver( - heap_tpolyhedra_domain.heap_domain, - _solver, - SSA, - precondition, - message_handler, - template_generator), - tpolyhedra_solver(heap_tpolyhedra_domain.polyhedra_domain, _solver, SSA.ns) - { - tpolyhedra_solver.set_message_handler(message_handler); - } - - virtual bool iterate(invariantt &_inv) override; - - virtual void set_message_handler(message_handlert &_message_handler) override; - void clear_symbolic_path(); - -protected: - heap_tpolyhedra_domaint &heap_tpolyhedra_domain; - - strategy_solvert heap_solver; - strategy_solver_binsearcht tpolyhedra_solver; -}; - - -#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_H diff --git a/src/domains/strategy_solver_heap_tpolyhedra_sympath.h b/src/domains/strategy_solver_heap_tpolyhedra_sympath.h deleted file mode 100644 index 950ae51dd..000000000 --- a/src/domains/strategy_solver_heap_tpolyhedra_sympath.h +++ /dev/null @@ -1,68 +0,0 @@ -/*******************************************************************\ - -Module: Strategy solver for heap-tpolyhedra domain using symbolic paths - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Strategy solver for heap-tpolyhedra domain using symbolic paths - -#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H -#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H - - -#include "strategy_solver_base.h" -#include "heap_tpolyhedra_sympath_domain.h" -#include "strategy_solver_heap_tpolyhedra.h" - -class strategy_solver_heap_tpolyhedra_sympatht:public strategy_solver_baset -{ -public: - strategy_solver_heap_tpolyhedra_sympatht( - heap_tpolyhedra_sympath_domaint &_domain, - incremental_solvert &_solver, - const local_SSAt &SSA, - const exprt &precondition, - message_handlert &message_handler, - template_generator_baset &template_generator): - strategy_solver_baset(_solver, SSA.ns), - domain(_domain), - heap_tpolyhedra_solver( - domain.heap_tpolyhedra_domain, - _solver, - SSA, - precondition, - message_handler, - template_generator) - { - build_loop_conds_map(SSA); - } - - virtual bool iterate(invariantt &inv) override; - - virtual void set_message_handler(message_handlert &_message_handler) override; - - void clear_symbolic_path(); - -protected: - heap_tpolyhedra_sympath_domaint &domain; - strategy_solver_heap_tpolyhedrat heap_tpolyhedra_solver; - - std::vector visited_paths; - bool new_path=true; - - // Mapping for each loop: - // g#ls -> (g#lh && g#le) - // ^ loop select ^ loop head ^ loop end - // This is used to check feasibility of symbolic paths - std::map loop_conds_map; - void build_loop_conds_map(const local_SSAt &SSA); - - bool is_current_path_feasible( - heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet &value); -}; - - -#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_HEAP_TPOLYHEDRA_SYMPATH_H diff --git a/src/domains/strategy_solver_product.cpp b/src/domains/strategy_solver_product.cpp new file mode 100644 index 000000000..2726cefa2 --- /dev/null +++ b/src/domains/strategy_solver_product.cpp @@ -0,0 +1,96 @@ +/*******************************************************************\ + +Module: Generic strategy solver for product combination domains + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic strategy solver for product combination domains +/// The strategy solver infers invariants for multiple domains in parallel +/// (domains are side-by-side). Iteration of each domain is run in the context +/// of candidate invariants already inferred in all other domains. + +#include "strategy_solver_product.h" + +bool strategy_solver_productt::iterate( + strategy_solver_baset::invariantt &_inv) +{ + auto &inv=dynamic_cast(_inv); + + bool improved=false; + for(unsigned i=0; isymbolic_path.get_expr()!=symbolic_path.get_expr()) + { + new_sympath=true; + solvers[i]->symbolic_path=symbolic_path; + domain.domains[i]->restrict_to_sympath(symbolic_path); + } + + solver.new_context(); + // Get context from all domains except the current one + for(unsigned j=0; jproject_on_vars(*inv[j], {}, domain_context); + solver << domain_context; +#ifdef DEBUG + std::cerr << "Context for domain " << j << ": " << std::endl; + debug_smt_model(domain_context, ns); +#endif + } + + // Run one iteration of strategy solving for the current domain + if(solvers[i]->iterate(*inv[i])) + { + improved=true; + // The symbolic path used in the first domain that was improved must be + // used for the rest of the domains. + if(with_sympaths && !solvers[i]->symbolic_path.empty() && + solvers[i]->symbolic_path!=symbolic_path) + { + symbolic_path=solvers[i]->symbolic_path; + } + } + + // If a symbolic path restriction was done above for this domain, undo it. + if(new_sympath) + domain.domains[i]->undo_sympath_restriction(); + solver.pop_context(); + } + + return improved; +} + +void strategy_solver_productt::use_sympaths() +{ + strategy_solver_baset::use_sympaths(); + for(auto &solver : solvers) + solver->use_sympaths(); +} + +void strategy_solver_productt::set_sympath(const symbolic_patht &sympath) +{ + strategy_solver_baset::set_sympath(sympath); + for(auto &solver : solvers) + solver->set_sympath(sympath); +} + +void strategy_solver_productt::clear_symbolic_path() +{ + strategy_solver_baset::clear_symbolic_path(); + for(auto &solver : solvers) + solver->clear_symbolic_path(); +} diff --git a/src/domains/strategy_solver_product.h b/src/domains/strategy_solver_product.h new file mode 100644 index 000000000..80d422d38 --- /dev/null +++ b/src/domains/strategy_solver_product.h @@ -0,0 +1,49 @@ +/*******************************************************************\ + +Module: Generic strategy solver for product combination domains + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic strategy solver for product combination domains +/// The strategy solver infers invariants for multiple domains in parallel +/// (domains are side-by-side). Iteration of each domain is run in the context +/// of candidate invariants already inferred in all other domains. + +#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_PRODUCT_H +#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_PRODUCT_H + +#include "strategy_solver_base.h" +#include "product_domain.h" +#include + +typedef std::vector> solver_vect; + +class strategy_solver_productt:public strategy_solver_baset +{ +public: + strategy_solver_productt( + product_domaint &domain, + solver_vect solvers, + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler): + strategy_solver_baset(solver, SSA, message_handler), + domain(domain), + solvers(std::move(solvers)) {} + + bool iterate(invariantt &inv) override; + + void use_sympaths() override; + void set_sympath(const symbolic_patht &sympath) override; + void clear_symbolic_path() override; + +protected: + product_domaint &domain; + // The solver contains a list of inner solvers + solver_vect solvers; +}; + +#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_PRODUCT_H diff --git a/src/domains/strategy_solver.cpp b/src/domains/strategy_solver_simple.cpp similarity index 57% rename from src/domains/strategy_solver.cpp rename to src/domains/strategy_solver_simple.cpp index 16b37cc11..5f19c4641 100644 --- a/src/domains/strategy_solver.cpp +++ b/src/domains/strategy_solver_simple.cpp @@ -10,17 +10,20 @@ Author: Matej Marusak /// Generic strategy solver #include -#include "strategy_solver.h" +#include "strategy_solver_simple.h" #include -bool strategy_solvert::iterate(invariantt &inv) +bool strategy_solver_simplet::iterate(invariantt &_inv) { + auto &inv=dynamic_cast(_inv); + bool improved=false; - domain.solver_iter_init(inv); + domain.init_value_solver_iteration(inv); if(domain.has_something_to_solve()) { solver.new_context(); + domain.strategy_value_exprs.clear(); // Entry value constraints exprt pre_expr=domain.to_pre_constraints(inv); @@ -38,26 +41,34 @@ bool strategy_solvert::iterate(invariantt &inv) } exprt cond=disjunction(strategy_cond_exprs); - adjust_float_expressions(cond, ns); + adjust_float_expressions(cond, SSA.ns); solver << cond; if(solver()==decision_proceduret::D_SATISFIABLE) { +#ifdef DEBUG + std::cerr << "Pre-condition:\n"; + debug_smt_model(pre_expr, ns); + std::cerr << "Post-condition:\n"; + debug_smt_model(cond, ns); +#endif for(std::size_t row=0; row required_values= - domain.get_required_smt_values(row); - std::vector got_values; - for(auto &c_exprt : required_values) + // Retrieve values of domain strategy expressions from the model + // and store them into smt_model_values. + if(domain.strategy_value_exprs.size()>row) { - got_values.push_back(solver.solver->get(c_exprt)); + domain.smt_model_values.clear(); + for(auto &c_exprt : domain.strategy_value_exprs[row]) + { + domain.smt_model_values.push_back(solver.solver->get(c_exprt)); + } } - domain.set_smt_values(got_values, row); - find_symbolic_path(loop_guards, domain.get_current_loop_guard(row)); + if(with_sympaths) + find_symbolic_path(loop_guards, domain.get_current_loop_guard(row)); improved=domain.edit_row(row, inv, improved); } @@ -65,12 +76,14 @@ bool strategy_solvert::iterate(invariantt &inv) } else { +#ifdef DEBUG debug() << "Outer solver: UNSAT!!" << eom; +#endif improved=domain.handle_unsat(inv, improved); } solver.pop_context(); - solver << domain.make_permanent(inv); - domain.post_edit(); + solver << domain.get_permanent_expr(inv); + domain.finalize_solver_iteration(); } return improved; } diff --git a/src/domains/strategy_solver.h b/src/domains/strategy_solver_simple.h similarity index 57% rename from src/domains/strategy_solver.h rename to src/domains/strategy_solver_simple.h index ce42245c5..42ea5114d 100644 --- a/src/domains/strategy_solver.h +++ b/src/domains/strategy_solver_simple.h @@ -13,30 +13,28 @@ Author: Matej Marusak #include #include "strategy_solver_base.h" -#include "domain.h" +#include "simple_domain.h" #include "template_generator_base.h" -class strategy_solvert:public strategy_solver_baset +class strategy_solver_simplet:public strategy_solver_baset { public: - strategy_solvert( - domaint &_domain, + strategy_solver_simplet( + simple_domaint &_domain, incremental_solvert &_solver, const local_SSAt &SSA, - const exprt &precondition, - message_handlert &message_handler, - template_generator_baset &template_generator): - strategy_solver_baset(_solver, SSA.ns), domain(_domain), + message_handlert &message_handler): + strategy_solver_baset(_solver, SSA, message_handler), + domain(_domain), loop_guards(SSA.loop_guards) { - set_message_handler(message_handler); - solver << domain.initialize_solver(SSA, precondition, template_generator); + domain.initialize(); } - virtual bool iterate(invariantt &_inv) override; + bool iterate(invariantt &_inv) override; protected: - domaint &domain; + simple_domaint &domain; std::set> loop_guards; }; diff --git a/src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp b/src/domains/strategy_solver_sympath.cpp similarity index 65% rename from src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp rename to src/domains/strategy_solver_sympath.cpp index b405d7b49..85da97624 100644 --- a/src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp +++ b/src/domains/strategy_solver_sympath.cpp @@ -1,29 +1,20 @@ /*******************************************************************\ -Module: Strategy solver for heap-tpolyhedra domain using symbolic paths +Module: Generic strategy solver for domain with symbolic paths Author: Viktor Malik \*******************************************************************/ /// \file -/// Strategy solver for heap-tpolyhedra domain using symbolic paths +/// Generic strategy solver for domain with symbolic paths -// #define DEBUG +#include "strategy_solver_sympath.h" -#include "strategy_solver_heap_tpolyhedra_sympath.h" - -void strategy_solver_heap_tpolyhedra_sympatht::set_message_handler( - message_handlert &_message_handler) -{ - solver.set_message_handler(_message_handler); -} - -bool strategy_solver_heap_tpolyhedra_sympatht::iterate( +bool strategy_solver_sympatht::iterate( strategy_solver_baset::invariantt &_inv) { - auto &inv=static_cast - (_inv); + auto &inv=dynamic_cast(_inv); bool improved; if(!new_path) @@ -38,8 +29,9 @@ bool strategy_solver_heap_tpolyhedra_sympatht::iterate( const exprt sympath=symbolic_path.get_expr(); - domain.heap_tpolyhedra_domain.restrict_to_sympath(symbolic_path); - improved=heap_tpolyhedra_solver.iterate(inv.at(sympath)); + inner_solver->set_sympath(symbolic_path); + domain.inner_domain->restrict_to_sympath(symbolic_path); + improved=inner_solver->iterate(*inv.at(sympath)); if(!improved) { // Invariant for the current symbolic path cannot be improved @@ -54,42 +46,43 @@ bool strategy_solver_heap_tpolyhedra_sympatht::iterate( inv.erase(sympath); visited_paths.push_back(symbolic_path); - domain.heap_tpolyhedra_domain.clear_aux_symbols(); - domain.heap_tpolyhedra_domain.eliminate_sympaths(visited_paths); + domain.inner_domain->remove_all_sympath_restrictions(); + domain.inner_domain->eliminate_sympaths(visited_paths); clear_symbolic_path(); improved=true; new_path=true; } - else if(heap_tpolyhedra_solver.symbolic_path.get_expr()!=sympath) + else if(inner_solver->symbolic_path.get_expr()!=sympath) { // The path has been altered during computation (solver has found another // loop-select guard that can be true - auto new_sympath=heap_tpolyhedra_solver.symbolic_path.get_expr(); + auto new_sympath=inner_solver->symbolic_path.get_expr(); inv.emplace(new_sympath, std::move(inv.at(sympath))); inv.erase(sympath); - symbolic_path=heap_tpolyhedra_solver.symbolic_path; + symbolic_path=inner_solver->symbolic_path; #ifdef DEBUG std::cerr << "Path altered\n"; std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n"; #endif } - domain.heap_tpolyhedra_domain.undo_restriction(); + domain.inner_domain->undo_sympath_restriction(); } else { // Computing invariant for a new path - heap_tpolyhedra_domaint::heap_tpolyhedra_valuet new_value; - domain.heap_tpolyhedra_domain.initialize(new_value); - improved=heap_tpolyhedra_solver.iterate(new_value); + auto new_value=std::unique_ptr( + inv.inner_value_template->clone()); + domain.inner_domain->initialize_value(*new_value); + improved=inner_solver->iterate(*new_value); if(improved) { - symbolic_path=heap_tpolyhedra_solver.symbolic_path; + symbolic_path=inner_solver->symbolic_path; #ifdef DEBUG std::cerr << "Symbolic path:\n"; std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n"; #endif - const exprt sympath=heap_tpolyhedra_solver.symbolic_path.get_expr(); + const exprt sympath=inner_solver->symbolic_path.get_expr(); inv.emplace(sympath, std::move(new_value)); new_path=false; } @@ -97,10 +90,10 @@ bool strategy_solver_heap_tpolyhedra_sympatht::iterate( return improved; } -void strategy_solver_heap_tpolyhedra_sympatht::clear_symbolic_path() +void strategy_solver_sympatht::clear_symbolic_path() { - symbolic_path.clear(); - heap_tpolyhedra_solver.clear_symbolic_path(); + strategy_solver_baset::clear_symbolic_path(); + inner_solver->clear_symbolic_path(); } /// Check if the current symbolic path is feasible while the computed invariant @@ -109,8 +102,8 @@ void strategy_solver_heap_tpolyhedra_sympatht::clear_symbolic_path() /// must be reachable (g#lb => g#le must be SAT) - for each loop whose loop- /// select guard occurs in negative form, if its loop head is reachable, then /// its end is not reachable (g#lb => !g#le must be SAT) -bool strategy_solver_heap_tpolyhedra_sympatht::is_current_path_feasible( - heap_tpolyhedra_sympath_domaint::heap_tpolyhedra_sympath_valuet &value) +bool strategy_solver_sympatht::is_current_path_feasible( + sympath_domaint::sympath_valuet &value) { bool result=true; auto sympath=symbolic_path.get_expr(); @@ -118,8 +111,8 @@ bool strategy_solver_heap_tpolyhedra_sympatht::is_current_path_feasible( // Path invariant exprt invariant; - domain.heap_tpolyhedra_domain.project_on_vars( - value.at(sympath), {}, invariant); + domain.inner_domain->project_on_vars( + *value.at(sympath), {}, invariant); solver << invariant; for(auto &guard : symbolic_path.path_map) @@ -149,7 +142,7 @@ bool strategy_solver_heap_tpolyhedra_sympatht::is_current_path_feasible( return result; } -void strategy_solver_heap_tpolyhedra_sympatht::build_loop_conds_map( +void strategy_solver_sympatht::build_loop_conds_map( const local_SSAt &SSA) { for(auto &node : SSA.nodes) diff --git a/src/domains/strategy_solver_sympath.h b/src/domains/strategy_solver_sympath.h new file mode 100644 index 000000000..cfd49f293 --- /dev/null +++ b/src/domains/strategy_solver_sympath.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + +Module: Generic strategy solver for domain with symbolic paths + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Generic strategy solver for domain with symbolic paths + +#ifndef CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_SYMPATH_H +#define CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_SYMPATH_H + + +#include "strategy_solver_base.h" +#include "sympath_domain.h" + +class strategy_solver_sympatht:public strategy_solver_baset +{ +public: + strategy_solver_sympatht( + sympath_domaint &_domain, + std::unique_ptr _inner_solver, + incremental_solvert &_solver, + const local_SSAt &SSA, + message_handlert &message_handler): + strategy_solver_baset(_solver, SSA, message_handler), + domain(_domain), + inner_solver(std::move(_inner_solver)) + { + build_loop_conds_map(SSA); + inner_solver->use_sympaths(); + } + + bool iterate(invariantt &inv) override; + + void clear_symbolic_path() override; + +protected: + sympath_domaint &domain; + + // Strategy solver for the inner domain + std::unique_ptr inner_solver; + + std::vector visited_paths; + bool new_path=true; + + // Mapping for each loop: + // g#ls -> (g#lh && g#le) + // ^ loop select ^ loop head ^ loop end + // This is used to check feasibility of symbolic paths + std::map loop_conds_map; + void build_loop_conds_map(const local_SSAt &SSA); + + bool is_current_path_feasible( + sympath_domaint::sympath_valuet &value); +}; + +#endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_SYMPATH_H diff --git a/src/domains/symbolic_path.h b/src/domains/symbolic_path.h index 1a70c419c..c671fcb0e 100644 --- a/src/domains/symbolic_path.h +++ b/src/domains/symbolic_path.h @@ -26,6 +26,14 @@ class symbolic_patht bool &operator[](const exprt &expr) { return path_map[expr]; } + // Compare for equality by comparing expressions + bool operator==(const symbolic_patht &rhs) const + { + return get_expr()==rhs.get_expr(); + } + bool operator!=(const symbolic_patht &rhs) const { return !(rhs==*this); } + + bool empty() { return path_map.empty(); } void clear() { path_map.clear(); } }; diff --git a/src/domains/sympath_domain.cpp b/src/domains/sympath_domain.cpp new file mode 100644 index 000000000..d1cc112df --- /dev/null +++ b/src/domains/sympath_domain.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: Abstract domain for computing invariants for different + program symbolic paths + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Abstract domain for computing invariants for different program symbolic +/// paths. The invariants can be computed in arbitrary domain (called the inner +/// domain). +/// Designed to work with strategy_solver_sympatht. + +#include "sympath_domain.h" +#include "strategy_solver_sympath.h" + +void sympath_domaint::output_value( + std::ostream &out, + const domaint::valuet &value, + const namespacet &ns) const +{ + auto &v=dynamic_cast(value); + for(auto &config : v) + { + out << from_expr(ns, "", config.first) << "==>\n"; + inner_domain->output_value(out, *config.second, ns); + } +} + +void sympath_domaint::output_domain( + std::ostream &out, + const namespacet &ns) const +{ + inner_domain->output_domain(out, ns); +} + +/// Project onto a set of variables. The result invariant is a disjunction of +/// expressions: +/// sympath_expr && sympath_inv +/// where sympath_expr is the formula representing the symbolic path and +/// sympath_inv is the invariant computed for the given symbolic path. +void sympath_domaint::project_on_vars( + domaint::valuet &value, + const var_sett &vars, + exprt &result) +{ + auto &v=dynamic_cast(value); + exprt::operandst c; + for(auto &config : v) + { + exprt config_result; + inner_domain->project_on_vars( + *config.second, vars, config_result); + c.push_back(and_exprt(config.first, config_result)); + } + c.push_back(no_loops_path); + + result=c.empty() ? true_exprt() : disjunction(c); +} + +std::unique_ptr sympath_domaint::new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) +{ + auto inner_solver=inner_domain->new_strategy_solver( + solver, SSA, message_handler); + return std::unique_ptr( + new strategy_solver_sympatht( + *this, std::move(inner_solver), solver, SSA, message_handler)); +} diff --git a/src/domains/sympath_domain.h b/src/domains/sympath_domain.h new file mode 100644 index 000000000..a46cd91b4 --- /dev/null +++ b/src/domains/sympath_domain.h @@ -0,0 +1,114 @@ +/*******************************************************************\ + +Module: Abstract domain for computing invariants for different + program symbolic paths + +Author: Viktor Malik + +\*******************************************************************/ + +/// \file +/// Abstract domain for computing invariants for different program symbolic +/// paths. The invariants can be computed in arbitrary domain (called the inner +/// domain). +/// Designed to work with strategy_solver_sympatht. + +#ifndef CPROVER_2LS_DOMAINS_SYMPATH_DOMAIN_H +#define CPROVER_2LS_DOMAINS_SYMPATH_DOMAIN_H + +#include "domain.h" +#include + +class sympath_domaint:public domaint +{ +public: + sympath_domaint( + unsigned int _domain_number, + replace_mapt &_renaming_map, + const local_SSAt &SSA, + std::unique_ptr inner_domain): + domaint(_domain_number, _renaming_map, SSA.ns), + inner_domain(std::move(inner_domain)) + { + exprt::operandst false_loop_guards; + for(auto &g : SSA.loop_guards) + false_loop_guards.push_back(not_exprt(g.first)); + no_loops_path=conjunction(false_loop_guards); + } + + std::unique_ptr inner_domain; + + // Value is a map from expression (symbolic path) to an invariant in the + // inner domain + class sympath_valuet: + public valuet, + public std::map> + { + public: + explicit sympath_valuet( + std::unique_ptr inner_value_template): + inner_value_template(std::move(inner_value_template)) {} + + sympath_valuet *clone() override + { + // Clone the inner value template + auto new_inner_value=std::unique_ptr( + inner_value_template->clone()); + auto new_value=new sympath_valuet(std::move(new_inner_value)); + // Clone the inner map + for(auto &val : *this) + new_value->emplace( + val.first, + std::unique_ptr(val.second->clone())); + return new_value; + } + + // A template of the inner value (corresponding to the inner domain) that + // will be used to create new values. + std::unique_ptr inner_value_template; + }; + + std::unique_ptr new_value() override + { + return std::unique_ptr( + new sympath_valuet(inner_domain->new_value())); + } + + void output_value( + std::ostream &out, + const valuet &value, + const namespacet &ns) const override; + + void output_domain( + std::ostream &out, + const namespacet &ns) const override; + + void project_on_vars( + valuet &value, + const var_sett &vars, + exprt &result) override; + + // These do not need to be implemented since there is no domain above this + // one that would use it. + void restrict_to_sympath(const symbolic_patht &sympath) override {} + void eliminate_sympaths( + const std::vector &sympaths) override {} + void undo_sympath_restriction() override {} + void remove_all_sympath_restrictions() override {} + + std::unique_ptr new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) override; + +protected: + // Special path containing conjunction negations of all loop-select guards + // This must be stored explicitly since the solver is not able to explore this + // path even though it can be feasible + exprt no_loops_path; + + friend class strategy_solver_sympatht; +}; + + +#endif // CPROVER_2LS_DOMAINS_SYMPATH_DOMAIN_H diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index 7ab4f9e8a..bde9917f6 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -22,8 +22,10 @@ Author: Peter Schrammel #include "tpolyhedra_domain.h" #include "predabs_domain.h" #include "heap_domain.h" -#include "heap_tpolyhedra_domain.h" -#include "heap_tpolyhedra_sympath_domain.h" +#include "sympath_domain.h" +#include "product_domain.h" + +#include #ifdef DEBUG #include @@ -166,7 +168,12 @@ void template_generator_baset::collect_variables_loop( exprt init_expr; get_init_expr(SSA, o_it, n_it, init_expr); - add_var(pre_var, pre_guard, obj_post_guard, domaint::LOOP, var_specs); + add_var( + pre_var, + pre_guard, + obj_post_guard, + guardst::kindt::LOOP, + var_specs); #ifdef DEBUG std::cout << "Adding " << from_expr(ns, "", in) << " " << @@ -177,9 +184,9 @@ void template_generator_baset::collect_variables_loop( } } -domaint::var_sett template_generator_baset::all_vars() +var_sett template_generator_baset::all_vars() { - domaint::var_sett vars; + var_sett vars; for(const auto &v : var_specs) { vars.insert(v.var); @@ -187,41 +194,42 @@ domaint::var_sett template_generator_baset::all_vars() return vars; } -void template_generator_baset::filter_template_domain() +var_specst template_generator_baset::filter_template_domain() { - domaint::var_specst new_var_specs(var_specs); - var_specs.clear(); - for(const auto &v : new_var_specs) + var_specst new_var_specs; + for(const auto &v : var_specs) { - const domaint::vart &s=v.var; + const vart &s=v.var; #ifdef DEBUG std::cout << "var: " << s << std::endl; #endif + if(s.id()==ID_symbol && is_pointed(s) && + id2string(to_symbol_expr(s).get_identifier()).find(".")!= + std::string::npos) + continue; + + if((s.type().id()==ID_unsignedbv || s.type().id()==ID_signedbv || s.type().id()==ID_floatbv /*|| s.type().id()==ID_c_enum_tag*/)) { - var_specs.push_back(v); + new_var_specs.push_back(v); } } + return new_var_specs; } -void template_generator_baset::filter_equality_domain() +var_specst template_generator_baset::filter_equality_domain() { - domaint::var_specst new_var_specs(var_specs); - var_specs.clear(); - for(const auto &v : new_var_specs) - { - var_specs.push_back(v); - } + var_specst new_var_specs(var_specs); + return new_var_specs; } -void template_generator_baset::filter_heap_domain() +var_specst template_generator_baset::filter_heap_domain() { - domaint::var_specst new_var_specs(var_specs); - var_specs.clear(); - for(auto &var : new_var_specs) + var_specst new_var_specs; + for(auto &var : var_specs) { if(var.var.id()==ID_symbol && var.var.type().id()==ID_pointer) { @@ -230,20 +238,21 @@ void template_generator_baset::filter_heap_domain() std::string::npos) continue; // Filter out non-assigned OUT variables - if(var.kind!=domaint::OUT || + if(var.guards.kind!=guardst::OUT || ssa_inlinert::get_original_identifier(to_symbol_expr(var.var))!= to_symbol_expr(var.var).get_identifier()) - var_specs.push_back(var); + new_var_specs.push_back(var); } } + return new_var_specs; } void template_generator_baset::add_var( - const domaint::vart &var, - const domaint::guardt &pre_guard, - domaint::guardt post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs) + const vart &var, + const guardst::guardt &pre_guard, + guardst::guardt post_guard, + const guardst::kindt &kind, + var_specst &var_specs) { exprt aux_expr=true_exprt(); if(std_invariants && pre_guard.id()==ID_and) @@ -260,12 +269,12 @@ void template_generator_baset::add_var( } if(var.type().id()!=ID_array) { - var_specs.push_back(domaint::var_spect()); - domaint::var_spect &var_spec=var_specs.back(); - var_spec.pre_guard=pre_guard; - var_spec.post_guard=post_guard; - var_spec.aux_expr=aux_expr; - var_spec.kind=kind; + var_specs.push_back(var_spect()); + var_spect &var_spec=var_specs.back(); + var_spec.guards.pre_guard=pre_guard; + var_spec.guards.post_guard=post_guard; + var_spec.guards.aux_expr=aux_expr; + var_spec.guards.kind=kind; var_spec.var=var; } @@ -277,13 +286,13 @@ void template_generator_baset::add_var( to_integer(array_type.size(), size); for(mp_integer i=0; itemplates.begin(); + nn_it->templates.begin(); t_it!=nn_it->templates.end(); t_it++) { debug() << "Template expression: " @@ -463,10 +472,12 @@ bool template_generator_baset::instantiate_custom_templates( debug() << "Custom template polyhedron found" << eom; if(!found_poly) // create domain { - domain_ptr=new tpolyhedra_domaint( - domain_number, - post_renaming_map, - SSA.ns); // TODO: aux_renaming_map + domain_ptr=std::unique_ptr( + new tpolyhedra_domaint( + domain_number, + post_renaming_map, + SSA.ns, + options)); // TODO: aux_renaming_map found_poly=true; } @@ -475,16 +486,16 @@ bool template_generator_baset::instantiate_custom_templates( if(contains_new_var) add_post_vars=true; - static_cast(domain_ptr) - ->add_template_row( - expr, - pre_guard, - contains_new_var ? - and_exprt(pre_guard, post_guard) : post_guard, - aux_expr, - contains_new_var ? domaint::OUT : domaint::LOOP); + guardst guards; + guards.pre_guard=pre_guard; + guards.post_guard=contains_new_var ? + and_exprt(pre_guard, post_guard) : post_guard; + guards.aux_expr=aux_expr; + guards.kind=contains_new_var ? guardst::OUT : guardst::LOOP; + dynamic_cast(domain_ptr.get()) + ->add_template_row(expr, guards); } - // pred abs domain + // pred abs domain else if(predabs) { options.set_option("predabs-solver", true); @@ -492,9 +503,10 @@ bool template_generator_baset::instantiate_custom_templates( debug() << "Custom predicate template found" << eom; if(!found_predabs) // create domain { - domain_ptr=new predabs_domaint( - domain_number, - post_renaming_map, SSA.ns); // TODO: aux_renaming_map + domain_ptr=std::unique_ptr( + new predabs_domaint( + domain_number, + post_renaming_map, SSA.ns)); // TODO: aux_renaming_map found_predabs=true; } @@ -503,14 +515,14 @@ bool template_generator_baset::instantiate_custom_templates( if(contains_new_var) add_post_vars=true; - static_cast(domain_ptr) - ->add_template_row( - expr, - pre_guard, - contains_new_var ? - and_exprt(pre_guard, post_guard) : post_guard, - aux_expr, - contains_new_var ? domaint::OUT : domaint::LOOP); + guardst guards; + guards.pre_guard=pre_guard; + guards.post_guard=contains_new_var ? + and_exprt(pre_guard, post_guard) : post_guard; + guards.aux_expr=aux_expr; + guards.kind=contains_new_var ? guardst::OUT : guardst::LOOP; + dynamic_cast(domain_ptr.get()) + ->add_template_row(expr, guards); } else // neither pred abs, nor polyhedra { @@ -520,16 +532,16 @@ bool template_generator_baset::instantiate_custom_templates( } if(add_post_vars) // for result retrieval via all_vars() only { - domaint::var_specst new_var_specs(var_specs); + var_specst new_var_specs(var_specs); var_specs.clear(); - for(domaint::var_specst::const_iterator v=new_var_specs.begin(); + for(var_specst::const_iterator v=new_var_specs.begin(); v!=new_var_specs.end(); v++) { var_specs.push_back(*v); - if(v->kind==domaint::LOOP) + if(v->guards.kind==guardst::LOOP) { var_specs.push_back(*v); - var_specs.back().kind=domaint::OUTL; + var_specs.back().guards.kind=guardst::OUTL; replace_expr(aux_renaming_map, var_specs.back().var); } } @@ -547,108 +559,71 @@ void template_generator_baset::instantiate_standard_domains( replace_mapt &renaming_map= std_invariants ? aux_renaming_map : post_renaming_map; - // get domain from command line options + domain_vect domains; + // get domains from command line options if(options.get_bool_option("equalities")) { - filter_equality_domain(); - domain_ptr= - new equality_domaint(domain_number, renaming_map, var_specs, SSA.ns); + auto eq_var_specs=filter_equality_domain(); + domains.emplace_back( + new equality_domaint(domain_number, renaming_map, eq_var_specs, SSA.ns)); } - else if(options.get_bool_option("heap")) + + if(options.get_bool_option("heap")) { - filter_heap_domain(); - domain_ptr=new heap_domaint(domain_number, renaming_map, var_specs, SSA); + auto heap_var_specs=filter_heap_domain(); + domains.emplace_back( + new heap_domaint(domain_number, renaming_map, heap_var_specs, SSA)); } - else if(options.get_bool_option("intervals")) + + if(options.get_bool_option("intervals")) { - domain_ptr= - new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); - filter_template_domain(); - static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns); + auto new_domain=new tpolyhedra_domaint( + domain_number, renaming_map, SSA.ns, options); + auto templ_var_specs=filter_template_domain(); + new_domain->add_interval_template(templ_var_specs, SSA.ns); + domains.emplace_back(new_domain); } else if(options.get_bool_option("zones")) { - domain_ptr= - new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); - filter_template_domain(); - static_cast(domain_ptr) - ->add_difference_template(var_specs, SSA.ns); - static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns); + auto new_domain=new tpolyhedra_domaint( + domain_number, renaming_map, SSA.ns, options); + auto templ_var_specs=filter_template_domain(); + new_domain->add_difference_template(templ_var_specs, SSA.ns); + new_domain->add_interval_template(templ_var_specs, SSA.ns); + domains.emplace_back(new_domain); } else if(options.get_bool_option("octagons")) { - domain_ptr= - new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); - filter_template_domain(); - static_cast(domain_ptr) - ->add_sum_template(var_specs, SSA.ns); - static_cast(domain_ptr) - ->add_difference_template(var_specs, SSA.ns); - static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns); + auto new_domain=new tpolyhedra_domaint( + domain_number, renaming_map, SSA.ns, options); + auto templ_var_specs=filter_template_domain(); + new_domain->add_sum_template(templ_var_specs, SSA.ns); + new_domain->add_difference_template(templ_var_specs, SSA.ns); + new_domain->add_interval_template(templ_var_specs, SSA.ns); + domains.emplace_back(new_domain); } else if(options.get_bool_option("qzones")) { - domain_ptr= - new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); - filter_template_domain(); - static_cast(domain_ptr) - ->add_difference_template(var_specs, SSA.ns); - static_cast(domain_ptr) - ->add_quadratic_template(var_specs, SSA.ns); - } - else if(options.get_bool_option("heap-interval") || - options.get_bool_option("heap-zones")) - { - filter_heap_interval_domain(); - auto polyhedra_kind=options.get_bool_option("heap-interval") - ? heap_tpolyhedra_domaint::INTERVAL - : heap_tpolyhedra_domaint::ZONES; - if(options.get_bool_option("sympath")) - domain_ptr=new heap_tpolyhedra_sympath_domaint( - domain_number, renaming_map, var_specs, SSA, polyhedra_kind); - else - domain_ptr=new heap_tpolyhedra_domaint( - domain_number, renaming_map, var_specs, SSA, polyhedra_kind); + auto new_domain=new tpolyhedra_domaint( + domain_number, renaming_map, SSA.ns, options); + auto templ_var_specs=filter_template_domain(); + new_domain->add_difference_template(templ_var_specs, SSA.ns); + new_domain->add_quadratic_template(templ_var_specs, SSA.ns); + domains.emplace_back(new_domain); } -} - -void template_generator_baset::filter_heap_interval_domain() -{ - domaint::var_specst new_var_specs(var_specs); - var_specs.clear(); - for(domaint::var_specst::const_iterator v=new_var_specs.begin(); - v!=new_var_specs.end(); v++) - { - const domaint::vart &s=v->var; - if(s.id()==ID_symbol && is_pointed(s) && - id2string(to_symbol_expr(s).get_identifier()).find(".")!= - std::string::npos) - continue; - - if(s.type().id()==ID_unsignedbv || - s.type().id()==ID_signedbv || - s.type().id()==ID_floatbv) - { - var_specs.push_back(*v); - continue; - } - - if(s.id()==ID_symbol && s.type().id()==ID_pointer) - { - // Filter out non-assigned OUT variables - if(v->kind!=domaint::OUT || - ssa_inlinert::get_original_identifier(to_symbol_expr(s))!= - to_symbol_expr(s).get_identifier()) - { - var_specs.push_back(*v); - continue; - } - } - } + // If multiple simple domains are used, use a product domain. + if(domains.size()==1) + domain_ptr=std::move(domains[0]); + else + domain_ptr=std::unique_ptr( + new product_domaint( + domain_number, renaming_map, SSA.ns, std::move(domains))); + + if(options.get_bool_option("sympath")) + domain_ptr=std::unique_ptr( + new sympath_domaint( + domain_number, renaming_map, SSA, std::move(domain_ptr))); } std::vector template_generator_baset::collect_record_frees( diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index c41944765..0bcea5eff 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -37,12 +37,6 @@ class template_generator_baset:public messaget std_invariants=options.get_bool_option("std-invariants"); } - virtual ~template_generator_baset() - { - if(domain_ptr!=NULL) - delete domain_ptr; - } - virtual void operator()( unsigned _domain_number, const local_SSAt &SSA, @@ -52,11 +46,15 @@ class template_generator_baset:public messaget assert(false); } - virtual domaint::var_sett all_vars(); + virtual var_sett all_vars(); - inline domaint *domain() { assert(domain_ptr!=NULL); return domain_ptr; } + inline domaint *domain() + { + assert(domain_ptr); + return domain_ptr.get(); + } - domaint::var_specst var_specs; + var_specst var_specs; replace_mapt post_renaming_map; replace_mapt init_renaming_map; replace_mapt aux_renaming_map; @@ -67,7 +65,7 @@ class template_generator_baset:public messaget protected: const ssa_dbt &ssa_db; const ssa_local_unwindert &ssa_local_unwinder; - domaint *domain_ptr; + std::unique_ptr domain_ptr; bool std_invariants; // include value at loop entry virtual void collect_variables_loop( @@ -79,35 +77,34 @@ class template_generator_baset:public messaget local_SSAt::nodest::const_iterator loop_begin, local_SSAt::nodest::const_iterator loop_end); - void filter_template_domain(); - void filter_equality_domain(); - void filter_heap_domain(); - void filter_heap_interval_domain(); + var_specst filter_template_domain(); + var_specst filter_equality_domain(); + var_specst filter_heap_domain(); void add_var( - const domaint::vart &var_to_add, - const domaint::guardt &pre_guard, - domaint::guardt post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs); + const vart &var_to_add, + const guardst::guardt &pre_guard, + guardst::guardt post_guard, + const guardst::kindt &kind, + var_specst &var_specs); void add_vars( const var_listt &vars_to_add, - const domaint::guardt &pre_guard, - const domaint::guardt &post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs); + const guardst::guardt &pre_guard, + const guardst::guardt &post_guard, + const guardst::kindt &kind, + var_specst &var_specs); void add_vars( const local_SSAt::var_listt &vars_to_add, - const domaint::guardt &pre_guard, - const domaint::guardt &post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs); + const guardst::guardt &pre_guard, + const guardst::guardt &post_guard, + const guardst::kindt &kind, + var_specst &var_specs); void add_vars( const local_SSAt::var_sett &vars_to_add, - const domaint::guardt &pre_guard, - const domaint::guardt &post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs); + const guardst::guardt &pre_guard, + const guardst::guardt &post_guard, + const guardst::kindt &kind, + var_specst &var_specs); void get_pre_post_guards( const local_SSAt &SSA, diff --git a/src/domains/template_generator_callingcontext.cpp b/src/domains/template_generator_callingcontext.cpp index 18e110cc6..51e3dbc71 100644 --- a/src/domains/template_generator_callingcontext.cpp +++ b/src/domains/template_generator_callingcontext.cpp @@ -35,7 +35,7 @@ void template_generator_callingcontextt::operator()( #if 1 debug() << "Template variables: " << eom; - domaint::output_var_specs(debug(), var_specs, SSA.ns); debug() << eom; + var_specs.output(debug(), SSA.ns); debug() << eom; debug() << "Template: " << eom; domain_ptr->output_domain(debug(), SSA.ns); debug() << eom; #endif @@ -80,7 +80,7 @@ void template_generator_callingcontextt::collect_variables_callingcontext( *v_it, guard, guard, - domaint::OUT, // the same for both forward and backward + guardst::OUT, // the same for both forward and backward var_specs); } } @@ -97,16 +97,16 @@ void template_generator_callingcontextt::collect_variables_callingcontext( std::set args; find_symbols(*a_it, args); exprt arg=*a_it; - add_vars(args, guard, guard, domaint::OUT, var_specs); + add_vars(args, guard, guard, guardst::OUT, var_specs); } } -domaint::var_sett template_generator_callingcontextt::callingcontext_vars() +var_sett template_generator_callingcontextt::callingcontext_vars() { - domaint::var_sett vars; + var_sett vars; for(const auto &v : var_specs) { - if(v.kind==domaint::OUT) + if(v.guards.kind==guardst::OUT) vars.insert(v.var); } return vars; diff --git a/src/domains/template_generator_callingcontext.h b/src/domains/template_generator_callingcontext.h index b48159afd..c17a821a4 100644 --- a/src/domains/template_generator_callingcontext.h +++ b/src/domains/template_generator_callingcontext.h @@ -32,7 +32,7 @@ class template_generator_callingcontextt:public template_generator_baset local_SSAt::nodet::function_callst::const_iterator f_it, bool forward=true); - virtual domaint::var_sett callingcontext_vars(); + virtual var_sett callingcontext_vars(); protected: virtual void collect_variables_callingcontext( diff --git a/src/domains/template_generator_ranking.cpp b/src/domains/template_generator_ranking.cpp index 6dd9156f2..33e53bbcb 100644 --- a/src/domains/template_generator_ranking.cpp +++ b/src/domains/template_generator_ranking.cpp @@ -32,22 +32,23 @@ void template_generator_rankingt::operator()( if(options.get_bool_option("monolithic-ranking-function")) { - domain_ptr=new linrank_domaint( - domain_number, - post_renaming_map, - options.get_unsigned_int_option("lexicographic-ranking-function"), - options.get_unsigned_int_option("max-inner-ranking-iterations"), SSA.ns); + domain_ptr=std::unique_ptr( + new linrank_domaint( + domain_number, + post_renaming_map, + options.get_unsigned_int_option("lexicographic-ranking-function"), + options.get_unsigned_int_option("max-inner-ranking-iterations"), + SSA.ns)); } else { - domain_ptr=new lexlinrank_domaint( - domain_number, - post_renaming_map, - options.get_unsigned_int_option( - "lexicographic-ranking-function"), - options.get_unsigned_int_option( - "max-inner-ranking-iterations"), - SSA.ns); + domain_ptr=std::unique_ptr( + new lexlinrank_domaint( + domain_number, + post_renaming_map, + options.get_unsigned_int_option("lexicographic-ranking-function"), + options.get_unsigned_int_option("max-inner-ranking-iterations"), + SSA.ns)); } collect_variables_ranking(SSA, forward); @@ -55,7 +56,7 @@ void template_generator_rankingt::operator()( #if 1 debug() << "Template variables: " << eom; - domaint::output_var_specs(debug(), var_specs, SSA.ns); debug() << eom; + var_specs.output(debug(), SSA.ns); debug() << eom; debug() << "Template: " << eom; domain_ptr->output_domain(debug(), SSA.ns); debug() << eom; #endif @@ -74,7 +75,7 @@ void template_generator_rankingt::collect_variables_ranking( // we've found a loop if(node.loophead!=SSA.nodes.end()) { - domaint::var_specst new_var_specs; + var_specst new_var_specs; exprt lhguard=SSA.guard_symbol(node.loophead->location); ssa_local_unwinder.unwinder_rename(to_symbol_expr(lhguard), node, true); @@ -109,7 +110,7 @@ void template_generator_rankingt::collect_variables_ranking( symbol_exprt out=SSA.read_rhs(object, node.location); ssa_local_unwinder.unwinder_rename(out, node, false); - add_var(in, pre_guard, post_guard, domaint::LOOP, new_var_specs); + add_var(in, pre_guard, post_guard, guardst::LOOP, new_var_specs); // building map for renaming from pre into post-state post_renaming_map[in]=out; @@ -122,13 +123,12 @@ void template_generator_rankingt::collect_variables_ranking( filter_ranking_domain(new_var_specs); -#ifndef LEXICOGRAPHIC - static_cast(domain_ptr) - ->add_template(new_var_specs, SSA.ns); -#else - static_cast(domain_ptr) - ->add_template(new_var_specs, SSA.ns); -#endif + if(options.get_bool_option("monolithic-ranking-function")) + dynamic_cast(domain_ptr.get()) + ->add_template(new_var_specs, SSA.ns); + else + dynamic_cast(domain_ptr.get()) + ->add_template(new_var_specs, SSA.ns); var_specs.insert( var_specs.end(), new_var_specs.begin(), new_var_specs.end()); @@ -137,13 +137,13 @@ void template_generator_rankingt::collect_variables_ranking( } void template_generator_rankingt::filter_ranking_domain( - domaint::var_specst &var_specs) + var_specst &var_specs) { - domaint::var_specst new_var_specs(var_specs); + var_specst new_var_specs(var_specs); var_specs.clear(); for(const auto &v : new_var_specs) { - const domaint::vart &s=v.var; + const vart &s=v.var; if(s.type().id()==ID_unsignedbv || s.type().id()==ID_signedbv || s.type().id()==ID_floatbv) diff --git a/src/domains/template_generator_ranking.h b/src/domains/template_generator_ranking.h index 4696fee04..0a7f2bbbc 100644 --- a/src/domains/template_generator_ranking.h +++ b/src/domains/template_generator_ranking.h @@ -35,7 +35,7 @@ class template_generator_rankingt:public template_generator_baset const local_SSAt &SSA, bool forward); - void filter_ranking_domain(domaint::var_specst &var_specs); + void filter_ranking_domain(var_specst &var_specs); }; #endif // CPROVER_2LS_DOMAINS_TEMPLATE_GENERATOR_RANKING_H diff --git a/src/domains/template_generator_summary.cpp b/src/domains/template_generator_summary.cpp index 3951aa95f..267dd35e6 100644 --- a/src/domains/template_generator_summary.cpp +++ b/src/domains/template_generator_summary.cpp @@ -65,13 +65,13 @@ void template_generator_summaryt::collect_variables_inout( SSA.params, first_guard, first_guard, - forward ? domaint::IN : domaint::OUT, + forward ? guardst::IN : guardst::OUT, var_specs); add_vars( SSA.globals_in, first_guard, first_guard, - forward ? domaint::IN : domaint::OUT, + forward ? guardst::IN : guardst::OUT, var_specs); // add globals_out (includes return values) @@ -81,43 +81,42 @@ void template_generator_summaryt::collect_variables_inout( SSA.globals_out, last_guard, last_guard, - forward ? domaint::OUT : domaint::IN, + forward ? guardst::OUT : guardst::IN, var_specs); } -domaint::var_sett template_generator_summaryt::inout_vars() +var_sett template_generator_summaryt::inout_vars() { - domaint::var_sett vars; - for(domaint::var_specst::const_iterator v=var_specs.begin(); + var_sett vars; + for(var_specst::const_iterator v=var_specs.begin(); v!=var_specs.end(); v++) { - if(v->kind==domaint::IN || - v->kind==domaint::OUT || - v->kind==domaint::OUTHEAP) + if(v->guards.kind==guardst::IN || + v->guards.kind==guardst::OUT) vars.insert(v->var); } return vars; } -domaint::var_sett template_generator_summaryt::out_vars() +var_sett template_generator_summaryt::out_vars() { - domaint::var_sett vars; - for(domaint::var_specst::const_iterator v=var_specs.begin(); + var_sett vars; + for(var_specst::const_iterator v=var_specs.begin(); v!=var_specs.end(); v++) { - if(v->kind==domaint::OUT) + if(v->guards.kind==guardst::OUT) vars.insert(v->var); } return vars; } -domaint::var_sett template_generator_summaryt::loop_vars() +var_sett template_generator_summaryt::loop_vars() { - domaint::var_sett vars; - for(domaint::var_specst::const_iterator v=var_specs.begin(); + var_sett vars; + for(var_specst::const_iterator v=var_specs.begin(); v!=var_specs.end(); v++) { - if(v->kind==domaint::LOOP || v->kind==domaint::IN) + if(v->guards.kind==guardst::LOOP || v->guards.kind==guardst::IN) vars.insert(v->var); } return vars; diff --git a/src/domains/template_generator_summary.h b/src/domains/template_generator_summary.h index 886348171..125f4b309 100644 --- a/src/domains/template_generator_summary.h +++ b/src/domains/template_generator_summary.h @@ -30,9 +30,9 @@ class template_generator_summaryt:public template_generator_baset const local_SSAt &SSA, bool forward=true); - virtual domaint::var_sett inout_vars(); - virtual domaint::var_sett loop_vars(); - virtual domaint::var_sett out_vars(); + virtual var_sett inout_vars(); + virtual var_sett loop_vars(); + virtual var_sett out_vars(); protected: virtual void collect_variables_inout(const local_SSAt &SSA, bool forward); diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index 3ca8bfa61..aa3f8b43e 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -19,6 +19,9 @@ Author: Peter Schrammel #include #include "tpolyhedra_domain.h" +#include "strategy_solver_binsearch.h" +#include "strategy_solver_binsearch2.h" +#include "strategy_solver_binsearch3.h" #include "util.h" #include "domain.h" @@ -26,64 +29,51 @@ Author: Peter Schrammel #define ENABLE_HEURISTICS -void tpolyhedra_domaint::initialize(valuet &value) +void tpolyhedra_domaint::initialize_value(domaint::valuet &value) { #if 0 if(templ.size()==0) return domaint::initialize(value); #endif - templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); v.resize(templ.size()); for(std::size_t row=0; row tpolyhedra_domaint::get_required_smt_values(size_t row) -{ - std::vector r; - r.push_back(strategy_value_exprs[row]); - return r; -} - -void tpolyhedra_domaint::set_smt_values( - std::vector got_values, - size_t row) -{ - value=got_values[0]; -} - bool tpolyhedra_domaint::edit_row(const rowt &row, valuet &_inv, bool improved) { - tpolyhedra_domaint::templ_valuet &inv= - static_cast(_inv); - set_row_value(row, simplify_const(value), inv); - return true; + auto &inv=dynamic_cast(_inv); + inv[row]=simplify_const(smt_model_values[0]); + return true; } -void tpolyhedra_domaint::join(valuet &value1, const valuet &value2) +void tpolyhedra_domaint::join( + domaint::valuet &value1, + const domaint::valuet &value2) { #if 0 if(templ.size()==0) return domaint::join(value1, value2); #endif - templ_valuet &v1=static_cast(value1); - const templ_valuet &v2=static_cast(value2); + auto &v1=dynamic_cast(value1); + auto &v2=dynamic_cast(value2); assert(v1.size()==templ.size()); assert(v1.size()==v2.size()); for(std::size_t row=0; row=vlower); if(vlower+1==vupper) - return from_integer(vlower, lower.type()); // floor + return row_valuet(from_integer(vlower, lower.type())); // floor #ifdef ENABLE_HEURISTICS // heuristics @@ -111,43 +101,43 @@ tpolyhedra_domaint::row_valuet tpolyhedra_domaint::between( { mp_integer vlargest=to_unsignedbv_type(type).largest(); if(vlower==mp_integer(0) && vupper==vlargest) - return from_integer(mp_integer(1), type); + return row_valuet(from_integer(mp_integer(1), type)); if(vlower==mp_integer(1) && vupper==vlargest) - return from_integer(mp_integer(vupper-1), type); + return row_valuet(from_integer(mp_integer(vupper-1), type)); if(vlower==mp_integer(1) && vupper==vlargest-1) - return from_integer(mp_integer(2), type); + return row_valuet(from_integer(mp_integer(2), type)); if(vlower row_expr<=row_value -exprt tpolyhedra_domaint::get_row_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row row_expr<=row_value -exprt tpolyhedra_domaint::get_row_pre_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row row_expr<=row_value -exprt tpolyhedra_domaint::get_row_pre_constraint( - const rowt &row, - const templ_valuet &value) -{ - assert(value.size()==templ.size()); - return get_row_pre_constraint(row, value[row]); -} - -/// row_expr<=row_value -exprt tpolyhedra_domaint::get_row_post_constraint( - const rowt &row, - const row_valuet &row_value) -{ - assert(row (row_expr<=row_value) ) -exprt tpolyhedra_domaint::to_pre_constraints(valuet &_value) -{ - tpolyhedra_domaint::templ_valuet &value= - static_cast(_value); - assert(value.size()==templ.size()); - exprt::operandst c; - for(std::size_t row=0; row (row_expr<=row_value)) to be connected -/// disjunctively -void tpolyhedra_domaint::make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs) -{ - tpolyhedra_domaint::templ_valuet &value= - static_cast(_value); - assert(value.size()==templ.size()); - cond_exprs.resize(templ.size()); - strategy_value_exprs.resize(templ.size()); - - exprt::operandst c; - for(std::size_t row=0; row(*templ[row].expr); return symbol_exprt( - SYMB_BOUND_VAR+i2string(domain_number)+"$"+ - i2string(row), templ[row].expr.type()); + SYMB_BOUND_VAR+i2string(domain_number)+"$"+i2string(row), + row_expr.type()); } /// pre_guard==> (row_expr<=symb_value) @@ -337,11 +197,13 @@ exprt tpolyhedra_domaint::get_row_symb_pre_constraint( { assert(row(*templ_row.expr); + if(templ_row.guards.kind==guardst::OUT || + templ_row.guards.kind==guardst::OUTL) return true_exprt(); return implies_exprt( - templ_row.pre_guard, // REMARK: and_expr==> loop15 regression - binary_relation_exprt(templ_row.expr, ID_le, get_row_symb_value(row))); + templ_row.guards.pre_guard, // REMARK: and_expr==> loop15 regression + binary_relation_exprt(templ_row_expr, ID_le, get_row_symb_value(row))); } /// post_guard && (row_expr >= row_symb_value) (!!!) @@ -349,15 +211,16 @@ exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row) { assert(row(*templ_row.expr); + if(templ_row.guards.kind==guardst::IN) return true_exprt(); exprt c=and_exprt( - templ_row.post_guard, - binary_relation_exprt(templ_row.expr, ID_ge, get_row_symb_value(row))); + templ_row.guards.post_guard, + binary_relation_exprt(templ_row_expr, ID_ge, get_row_symb_value(row))); rename(c); c=and_exprt( - c, not_exprt(equal_exprt(get_row_symb_value(row), templ_row.expr))); - return and_exprt(templ_row.aux_expr, c); + c, not_exprt(equal_exprt(get_row_symb_value(row), templ_row_expr))); + return and_exprt(templ_row.guards.aux_expr, c); } /// pre_guard==> (row_expr<=symb_row_value) @@ -384,7 +247,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints( if(symb_rows.find(row)!=symb_rows.end()) c.push_back(get_row_symb_pre_constraint(row, value[row])); else - c.push_back(get_row_pre_constraint(row, value[row])); + c.push_back(get_row_pre_constraint(row, value)); } return conjunction(c); } @@ -407,9 +270,9 @@ exprt tpolyhedra_domaint::get_row_symb_value_constraint( const row_valuet &row_value, bool geq) { - if(is_row_value_neginf(row_value)) + if(row_value.is_neg_inf()) return false_exprt(); - if(is_row_value_inf(row_value)) + if(row_value.is_inf()) return true_exprt(); exprt c=binary_relation_exprt( get_row_symb_value(row), @@ -418,86 +281,24 @@ exprt tpolyhedra_domaint::get_row_symb_value_constraint( return c; } - -tpolyhedra_domaint::row_valuet tpolyhedra_domaint::get_row_value( - const rowt &row, - const templ_valuet &value) -{ - assert(row(value); - - assert(v.size()==templ.size()); - exprt::operandst c; - for(std::size_t row=0; row symbols; - find_symbols(templ_row.expr, symbols); - - bool pure=true; - for(const auto &symbol : symbols) - { - if(!vars.empty() && vars.find(symbol)==vars.end()) - { - pure=false; - break; - } - } - if(!pure) - continue; - - const row_valuet &row_v=v[row]; - const exprt row_constraint=get_row_constraint(row, row_v); - if(templ_row.kind==LOOP) - c.push_back(implies_exprt(templ_row.pre_guard, row_constraint)); - else - c.push_back(row_constraint); - } - result=conjunction(c); -} - -void tpolyhedra_domaint::set_row_value( - const rowt &row, - const tpolyhedra_domaint::row_valuet &row_value, - templ_valuet &value) -{ - assert(row(*templ_row.expr); + if(templ_row_expr.type().id()==ID_signedbv) { - return to_signedbv_type(templ_row.expr.type()).largest_expr(); + return row_valuet(to_signedbv_type(templ_row_expr.type()).largest_expr()); } - if(templ_row.expr.type().id()==ID_unsignedbv) + if(templ_row_expr.type().id()==ID_unsignedbv) { - return to_unsignedbv_type(templ_row.expr.type()).largest_expr(); + return row_valuet(to_unsignedbv_type(templ_row_expr.type()).largest_expr()); } - if(templ_row.expr.type().id()==ID_floatbv) + if(templ_row_expr.type().id()==ID_floatbv) { - ieee_floatt max(to_floatbv_type(templ_row.expr.type())); + ieee_floatt max(to_floatbv_type(templ_row_expr.type())); max.make_fltmax(); - return max.to_expr(); + return row_valuet(max.to_expr()); } assert(false); // type not supported } @@ -506,48 +307,39 @@ tpolyhedra_domaint::row_valuet tpolyhedra_domaint::get_min_row_value( const tpolyhedra_domaint::rowt &row) { const template_rowt &templ_row=templ[row]; - if(templ_row.expr.type().id()==ID_signedbv) + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + if(templ_row_expr.type().id()==ID_signedbv) { - return to_signedbv_type(templ_row.expr.type()).smallest_expr(); + return row_valuet(to_signedbv_type(templ_row_expr.type()).smallest_expr()); } - if(templ_row.expr.type().id()==ID_unsignedbv) + if(templ_row_expr.type().id()==ID_unsignedbv) { - return to_unsignedbv_type(templ_row.expr.type()).smallest_expr(); + return row_valuet( + to_unsignedbv_type(templ_row_expr.type()).smallest_expr()); } - if(templ_row.expr.type().id()==ID_floatbv) + if(templ_row_expr.type().id()==ID_floatbv) { - ieee_floatt min(to_floatbv_type(templ_row.expr.type())); + ieee_floatt min(to_floatbv_type(templ_row_expr.type())); min.make_fltmin(); - return min.to_expr(); + return row_valuet(min.to_expr()); } assert(false); // type not supported } void tpolyhedra_domaint::output_value( std::ostream &out, - const valuet &value, + const domaint::valuet &value, const namespacet &ns) const { - const templ_valuet &v=static_cast(value); + auto &v=dynamic_cast(value); for(std::size_t row=0; row " << std::endl << " "; - break; - case IN: out << "(IN) "; break; - case OUT: case OUTL: out << "(OUT) "; break; - default: assert(false); - } - out << "( " << from_expr(ns, "", templ_row.expr) << "<="; - if(is_row_value_neginf(v[row])) + auto &templ_row_expr=dynamic_cast(*templ[row].expr); + templ[row].guards.output(out, ns); + out << "( " << from_expr(ns, "", templ_row_expr) << "<="; + if(v[row].is_inf()) out << "-oo"; - else if(is_row_value_inf(v[row])) + else if(v[row].is_neg_inf()) out << "oo"; else out << from_expr(ns, "", v[row]); @@ -555,54 +347,6 @@ void tpolyhedra_domaint::output_value( } } -void tpolyhedra_domaint::output_domain( - std::ostream &out, - const namespacet &ns) const -{ - for(std::size_t row=0; row " - << std::endl << " "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", templ_row.pre_guard) << "===> " - << std::endl << " "; - break; - case OUT: case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", templ_row.post_guard) << "===> " - << std::endl << " "; - break; - default: assert(false); - } - out << "( " << - from_expr(ns, "", templ_row.expr) << "<=CONST )" << std::endl; - } -} - -unsigned tpolyhedra_domaint::template_size() -{ - return templ.size(); -} - -bool tpolyhedra_domaint::is_row_value_neginf( - const row_valuet & row_value) const -{ - return row_value.get(ID_value)==ID_false; -} - -bool tpolyhedra_domaint::is_row_value_inf(const row_valuet & row_value) const -{ - return row_value.get(ID_value)==ID_true; -} - /// add row suffix to non-symbolic-bound variables in expression (required for /// strategy iteration (binsearch3)) void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row) @@ -623,21 +367,15 @@ void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row) } tpolyhedra_domaint::template_rowt &tpolyhedra_domaint::add_template_row( - const exprt& expr, - const exprt& pre_guard, - const exprt& post_guard, - const exprt& aux_expr, - kindt kind - ) + const exprt &expr, + const guardst &guards) { templ.push_back(template_rowt()); template_rowt &templ_row=templ.back(); - templ_row.expr=expr; - extend_expr_types(templ_row.expr); - templ_row.pre_guard=pre_guard; - templ_row.post_guard=post_guard; - templ_row.aux_expr=aux_expr; - templ_row.kind=kind; + templ_row.expr=std::unique_ptr( + new template_row_exprt(expr)); + extend_expr_types(dynamic_cast(*templ_row.expr)); + templ_row.guards=guards; return templ_row; } @@ -649,28 +387,18 @@ void tpolyhedra_domaint::add_interval_template( unsigned size=2*var_specs.size(); templ.reserve(templ.size()+size); - for(const auto v : var_specs) + for(const auto &v : var_specs) { - if(v.kind==IN) + if(v.guards.kind==guardst::IN) continue; if(v.var.type().id()==ID_pointer) continue; // x - add_template_row( - v.var, - v.pre_guard, - v.post_guard, - v.aux_expr, - v.kind); + add_template_row(v.var, v.guards); // -x - add_template_row( - unary_minus_exprt(v.var, v.var.type()), - v.pre_guard, - v.post_guard, - v.aux_expr, - v.kind); + add_template_row(unary_minus_exprt(v.var, v.var.type()), v.guards); } } @@ -714,28 +442,22 @@ void tpolyhedra_domaint::add_difference_template( } } - kindt k=domaint::merge_kinds(v1->kind, v2->kind); - if(k==IN) + guardst guards=guardst::merge_and_guards(v1->guards, v2->guards, ns); + if(guards.kind==guardst::IN) continue; - if(k==LOOP && v1->pre_guard!=v2->pre_guard) + if(guards.kind==guardst::LOOP && + v1->guards.pre_guard!=v2->guards.pre_guard) continue; // TEST: we need better heuristics if(v2->var.type().id()==ID_pointer) continue; - - exprt pre_g, post_g, aux_expr; - merge_and(pre_g, v1->pre_guard, v2->pre_guard, ns); - merge_and(post_g, v1->post_guard, v2->post_guard, ns); - merge_and(aux_expr, v1->aux_expr, v2->aux_expr, ns); - if(post_g.is_false()) + if(guards.post_guard.is_false()) continue; // x1-x2 - add_template_row( - minus_exprt(v1->var, v2->var), pre_g, post_g, aux_expr, k); + add_template_row(minus_exprt(v1->var, v2->var), guards); // x2-x1 - add_template_row( - minus_exprt(v2->var, v1->var), pre_g, post_g, aux_expr, k); + add_template_row(minus_exprt(v2->var, v1->var), guards); } } } @@ -750,24 +472,15 @@ void tpolyhedra_domaint::add_quadratic_template( for(const auto v : var_specs) { - if(v.kind==IN) + if(v.guards.kind==guardst::IN) continue; // x - add_template_row( - mult_exprt(v.var, v.var), - v.pre_guard, - v.post_guard, - v.aux_expr, - v.kind); + add_template_row(mult_exprt(v.var, v.var), v.guards); // -x add_template_row( - unary_minus_exprt(mult_exprt(v.var, v.var), v.var.type()), - v.pre_guard, - v.post_guard, - v.aux_expr, - v.kind); + unary_minus_exprt(mult_exprt(v.var, v.var), v.var.type()), v.guards); } } @@ -785,71 +498,49 @@ void tpolyhedra_domaint::add_sum_template( var_specst::const_iterator v2=v1; ++v2; for(; v2!=var_specs.end(); ++v2) { - kindt k=domaint::merge_kinds(v1->kind, v2->kind); - if(k==IN) + auto guards=guardst::merge_and_guards(v1->guards, v2->guards, ns); + if(guards.kind==guardst::IN) continue; - if(k==LOOP && v1->pre_guard!=v2->pre_guard) + if(guards.kind==guardst::LOOP && + v1->guards.pre_guard!=v2->guards.pre_guard) continue; // TEST: we need better heuristics - exprt pre_g, post_g, aux_expr; - merge_and(pre_g, v1->pre_guard, v2->pre_guard, ns); - merge_and(post_g, v1->post_guard, v2->post_guard, ns); - merge_and(aux_expr, v1->aux_expr, v2->aux_expr, ns); - // -x1-x2 add_template_row( minus_exprt(unary_minus_exprt(v1->var, v1->var.type()), v2->var), - pre_g, - post_g, - aux_expr, - k); + guards); // x1+x2 - add_template_row( - plus_exprt(v1->var, v2->var), pre_g, post_g, aux_expr, k); + add_template_row(plus_exprt(v1->var, v2->var), guards); } } } -void tpolyhedra_domaint::restrict_to_sympath(const symbolic_patht &sympath) +/// Choose a correct solver based on the used strategy +std::unique_ptr tpolyhedra_domaint::new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) { - for(auto &row : templ) + switch(strategy) { - const exprt c=sympath.get_expr(row.pre_guard.op1()); - row.aux_expr=and_exprt(row.aux_expr, c); + case ENUMERATION: + return simple_domaint::new_strategy_solver(solver, SSA, message_handler); + case BINSEARCH: + return std::unique_ptr( + new strategy_solver_binsearcht(*this, solver, SSA, message_handler)); + case BINSEARCH2: + return std::unique_ptr( + new strategy_solver_binsearch2t(*this, solver, SSA, message_handler)); + case BINSEARCH3: + return std::unique_ptr( + new strategy_solver_binsearch3t(*this, solver, SSA, message_handler)); } } -void tpolyhedra_domaint::clear_aux_symbols() -{ - for(auto &row : templ) - row.aux_expr=true_exprt(); -} - -void tpolyhedra_domaint::undo_restriction() -{ - for(auto &row : templ) - { - if(row.aux_expr.id()==ID_and) - { - row.aux_expr=to_and_expr(row.aux_expr).op0(); - } - } -} - -void tpolyhedra_domaint::eliminate_sympaths( - const std::vector &sympaths) +void tpolyhedra_domaint::template_row_exprt::output( + std::ostream &out, + const namespacet &ns) const { - for(auto &row : templ) - { - exprt::operandst paths; - for(const symbolic_patht &sympath : sympaths) - { - const exprt path_expr=sympath.get_expr(row.pre_guard.op1()); - paths.push_back(path_expr); - } - row.aux_expr=paths.empty() - ? true_exprt() - : static_cast(not_exprt(disjunction(paths))); - } + out << from_expr(ns, "", *this) << "<=CONST" << std::endl; } diff --git a/src/domains/tpolyhedra_domain.h b/src/domains/tpolyhedra_domain.h index 476ef91d8..2cf90f1c0 100644 --- a/src/domains/tpolyhedra_domain.h +++ b/src/domains/tpolyhedra_domain.h @@ -17,61 +17,85 @@ Author: Peter Schrammel #include #include #include +#include -#include "domain.h" +#include "simple_domain.h" #include "symbolic_path.h" -class tpolyhedra_domaint:public domaint +class tpolyhedra_domaint:public simple_domaint { public: - typedef exprt row_exprt; - typedef constant_exprt row_valuet; // "bound" + /// Template row expression is a simple expression + struct template_row_exprt:simple_domaint::template_row_exprt, exprt + { + explicit template_row_exprt(const exprt &expr) : exprt(expr) {} + + std::vector get_row_exprs() override { return {*this}; } + void output(std::ostream &out, const namespacet &ns) const override; + }; - class templ_valuet:public domaint::valuet, public std::vector + /// Row value (parameter) is a constant + struct row_valuet:constant_exprt { + row_valuet()=default; + explicit row_valuet(const constant_exprt &value) : constant_exprt(value) {} + using constant_exprt::operator=; + + bool is_inf() const { return get(ID_value)==ID_true; } + bool is_neg_inf() const { return get(ID_value)==ID_false; } + + exprt get_row_expr(const template_row_exprt &templ_row_expr) const + { + if(is_inf()) + return true_exprt(); + if(is_neg_inf()) + return false_exprt(); + // row_expr <= row_value + return binary_relation_exprt(templ_row_expr, ID_le, *this); + } }; - typedef struct + /// Template value is conjunction of rows + struct templ_valuet:simple_domaint::valuet, std::vector { - guardt pre_guard; - guardt post_guard; - row_exprt expr; - exprt aux_expr; - kindt kind; - } template_rowt; + exprt get_row_expr(rowt row, const template_rowt &templ_row) const override + { + auto &templ_row_expr=dynamic_cast(*templ_row.expr); + return (*this)[row].get_row_expr(templ_row_expr); + } - typedef std::vector templatet; + templ_valuet *clone() override { return new templ_valuet(*this); } + }; - tpolyhedra_domaint( - unsigned _domain_number, - replace_mapt &_renaming_map, - const namespacet &_ns): - domaint(_domain_number, _renaming_map, _ns) + std::unique_ptr new_value() override { + return std::unique_ptr(new templ_valuet()); } - // initialize value - virtual void initialize(valuet &value); - - std::vector get_required_smt_values(size_t row); - void set_smt_values(std::vector got_values, size_t row); - - bool edit_row(const rowt &row, valuet &inv, bool improved); + enum strategyt + { + ENUMERATION, + BINSEARCH, + BINSEARCH2, + BINSEARCH3 + }; + strategyt strategy; - exprt to_pre_constraints(valuet &_value); + tpolyhedra_domaint( + unsigned _domain_number, + replace_mapt &_renaming_map, + const namespacet &_ns, + const optionst &options): + simple_domaint(_domain_number, _renaming_map, _ns), + strategy(options.get_bool_option("enum-solver") ? ENUMERATION : BINSEARCH) + {} - void make_not_post_constraints( - valuet &_value, - exprt::operandst &cond_exprs); + // initialize value + void initialize_value(domaint::valuet &value) override; - virtual void join(valuet &value1, const valuet &value2); + bool edit_row(const rowt &row, valuet &inv, bool improved) override; - // value -> constraints - exprt get_row_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_pre_constraint(const rowt &row, const templ_valuet &value); - exprt get_row_post_constraint(const rowt &row, const templ_valuet &value); + void join(domaint::valuet &value1, const domaint::valuet &value2) override; // value -> symbolic bound constraints (for optimization) exprt to_symb_pre_constraints(const templ_valuet &value); @@ -89,45 +113,21 @@ class tpolyhedra_domaint:public domaint exprt get_row_symb_post_constraint(const rowt &row); - // set, get value - row_valuet get_row_value(const rowt &row, const templ_valuet &value); - void set_row_value( - const rowt &row, - const row_valuet &row_value, - templ_valuet &value); - // max, min, comparison row_valuet get_max_row_value(const rowt &row); row_valuet get_min_row_value(const rowt &row); row_valuet between(const row_valuet &lower, const row_valuet &upper); bool less_than(const row_valuet &v1, const row_valuet &v2); - bool is_row_value_inf(const row_valuet & row_value) const; - bool is_row_value_neginf(const row_valuet & row_value) const; // printing - virtual void output_value( + void output_value( std::ostream &out, - const valuet &value, - const namespacet &ns) const; - virtual void output_domain( - std::ostream &out, - const namespacet &ns) const; - - // projection - virtual void project_on_vars( - valuet &value, - const var_sett &vars, - exprt &result); - - unsigned template_size(); + const domaint::valuet &value, + const namespacet &ns) const override; // generating templates - template_rowt &add_template_row( - const exprt& expr, - const exprt& pre_guard, - const exprt& post_guard, - const exprt& aux_expr, - kindt kind); + tpolyhedra_domaint::template_rowt & + add_template_row(const exprt &expr, const guardst &guards); void add_interval_template( const var_specst &var_specs, @@ -142,21 +142,19 @@ class tpolyhedra_domaint:public domaint const var_specst &var_specs, const namespacet &ns); - void restrict_to_sympath(const symbolic_patht &sympath); - void undo_restriction(); - void eliminate_sympaths(const std::vector &sympaths); - void clear_aux_symbols(); - symbol_exprt get_row_symb_value(const rowt &row); void rename_for_row(exprt &expr, const rowt &row); + std::unique_ptr new_strategy_solver( + incremental_solvert &solver, + const local_SSAt &SSA, + message_handlert &message_handler) override; + protected: friend class strategy_solver_binsearcht; - friend class strategy_solvert; - - templatet templ; - exprt value; + friend class strategy_solver_binsearch2t; + friend class strategy_solver_binsearch3t; }; #endif diff --git a/src/solver/summarizer_bw_term.cpp b/src/solver/summarizer_bw_term.cpp index 7683b8f11..2f922f5ba 100644 --- a/src/solver/summarizer_bw_term.cpp +++ b/src/solver/summarizer_bw_term.cpp @@ -277,7 +277,7 @@ bool summarizer_bw_termt::bootstrap_preconditions( exprt &termination_argument) { // bootstrap with a concrete model for input variables - const domaint::var_sett &invars=template_generator2.out_vars(); + const var_sett &invars=template_generator2.out_vars(); solver.new_context(); unsigned number_bootstraps=0; @@ -298,7 +298,7 @@ bool summarizer_bw_termt::bootstrap_preconditions( if(solver()==decision_proceduret::D_SATISFIABLE) { exprt::operandst c; - for(domaint::var_sett::const_iterator it=invars.begin(); + for(var_sett::const_iterator it=invars.begin(); it!=invars.end(); it++) { c.push_back(equal_exprt(*it, solver.solver->get(*it))); diff --git a/src/solver/summarizer_fw.cpp b/src/solver/summarizer_fw.cpp index 66e6b5ff1..4604b0e31 100644 --- a/src/solver/summarizer_fw.cpp +++ b/src/solver/summarizer_fw.cpp @@ -146,16 +146,6 @@ void summarizer_fwt::do_summary( debug() << "whole result: " << from_expr(SSA.ns, "", whole_result) << eom; #endif - if(options.get_bool_option("heap")) - { - analyzer.update_heap_out(summary.globals_out); - const exprt advancer_bindings=analyzer.input_heap_bindings(); - if(!advancer_bindings.is_true()) - { - summary.aux_precondition=advancer_bindings; - } - } - if(context_sensitive && !summary.fw_precondition.is_true()) { summary.fw_transformer= diff --git a/src/ssa/Makefile b/src/ssa/Makefile index c3fda6e99..f2fd9787f 100644 --- a/src/ssa/Makefile +++ b/src/ssa/Makefile @@ -1,11 +1,11 @@ SRC = local_ssa.cpp ssa_var_collector.cpp \ ssa_domain.cpp translate_union_member.cpp \ - malloc_ssa.cpp ssa_pointed_objects.cpp ssa_heap_domain.cpp \ + malloc_ssa.cpp ssa_pointed_objects.cpp \ guard_map.cpp ssa_object.cpp assignments.cpp ssa_dereference.cpp \ ssa_value_set.cpp address_canonizer.cpp simplify_ssa.cpp \ ssa_build_goto_trace.cpp ssa_inliner.cpp ssa_unwinder.cpp \ unwindable_local_ssa.cpp ssa_db.cpp \ - ssa_pointed_objects.cpp ssa_heap_domain.cpp may_alias_analysis.cpp \ + ssa_pointed_objects.cpp may_alias_analysis.cpp \ dynobj_instance_analysis.cpp include ../config.inc diff --git a/src/ssa/assignments.cpp b/src/ssa/assignments.cpp index 1d1b41d2b..10c93b28f 100644 --- a/src/ssa/assignments.cpp +++ b/src/ssa/assignments.cpp @@ -64,20 +64,6 @@ void assignmentst::build_assignment_map( ++n_it; const irep_idt fname=to_symbol_expr( code_function_call.function()).get_identifier(); - std::list new_objects; - std::set modified_objects; - - if(ssa_heap_analysis.has_location(n_it)) - { - new_objects=ssa_heap_analysis[n_it].new_caller_objects(fname, it); - modified_objects=ssa_heap_analysis[n_it].modified_objects(fname); - } - - // Assign new objects - for(auto &o : new_objects) - { - assign(o, it, ns); - } for(objectst::const_iterator o_it=ssa_objects.globals.begin(); @@ -87,36 +73,6 @@ void assignmentst::build_assignment_map( assign(*o_it, it, ns); } - // Assign all modified objects - for(const exprt &modified : modified_objects) - { - const exprt arg= - ssa_heap_analysis[n_it].function_map.at(fname). - corresponding_expr(modified, code_function_call.arguments(), 0); - - if(arg!=modified) - { - bool comp=options.get_bool_option("competition-mode"); - const exprt arg_deref=dereference( - arg, ssa_value_ai[it], "", ns, comp); - assign(arg_deref, it, ns); - - std::set symbols; - find_symbols(arg_deref, symbols); - for(const symbol_exprt &symbol : symbols) - { - if(symbol.type()==arg_deref.type()) - { - auto &aliases=ssa_value_ai[n_it](symbol, ns).value_set; - for(auto &alias : aliases) - { - assign(alias.get_expr(), it, ns); - } - } - } - } - } - // the call might come with an assignment if(code_function_call.lhs().is_not_nil()) { diff --git a/src/ssa/assignments.h b/src/ssa/assignments.h index 4648ab096..2118745b3 100644 --- a/src/ssa/assignments.h +++ b/src/ssa/assignments.h @@ -25,7 +25,6 @@ class assignmentst const ssa_objectst &ssa_objects; const ssa_value_ait &ssa_value_ai; - const ssa_heap_analysist &ssa_heap_analysis; typedef ssa_objectst::objectst objectst; @@ -55,11 +54,9 @@ class assignmentst const namespacet &_ns, const optionst &_options, const ssa_objectst &_ssa_objects, - const ssa_value_ait &_ssa_value_ai, - const ssa_heap_analysist &_ssa_heap_analysis): + const ssa_value_ait &_ssa_value_ai): ssa_objects(_ssa_objects), ssa_value_ai(_ssa_value_ai), - ssa_heap_analysis(_ssa_heap_analysis), options(_options) { build_assignment_map(_goto_program, _ns); diff --git a/src/ssa/local_ssa.h b/src/ssa/local_ssa.h index 125bcdc6f..41c243450 100644 --- a/src/ssa/local_ssa.h +++ b/src/ssa/local_ssa.h @@ -19,11 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "ssa_domain.h" #include "guard_map.h" #include "ssa_object.h" -#include "ssa_heap_domain.h" #include "may_alias_analysis.h" #define TEMPLATE_PREFIX "__CPROVER_template" @@ -41,19 +41,16 @@ class local_SSAt const goto_functiont &_goto_function, const namespacet &_ns, const optionst &_options, - const ssa_heap_analysist &_heap_analysis, const std::string &_suffix=""): ns(_ns), goto_function(_goto_function), options(_options), - heap_analysis(_heap_analysis), - ssa_objects(_goto_function, ns, _heap_analysis), - ssa_value_ai(_goto_function, ns, options, _heap_analysis), + ssa_objects(_goto_function, ns), + ssa_value_ai(_goto_function, ns, options), assignments( _goto_function.body, ns, options, ssa_objects, - ssa_value_ai, - heap_analysis), + ssa_value_ai), alias_analysis(_goto_function, ns), guard_map(_goto_function.body), ssa_analysis(assignments), @@ -245,8 +242,6 @@ class local_SSAt const namespacet &ns, const locationt loc); - const ssa_heap_analysist &heap_analysis; - ssa_objectst ssa_objects; typedef ssa_objectst::objectst objectst; ssa_value_ait ssa_value_ai; diff --git a/src/ssa/ssa_db.h b/src/ssa/ssa_db.h index 7f00a3a46..3e33974bb 100644 --- a/src/ssa/ssa_db.h +++ b/src/ssa/ssa_db.h @@ -67,11 +67,9 @@ class ssa_dbt inline void create( const function_namet &function_name, const goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - const ssa_heap_analysist &heap_analysis) + const namespacet &ns) { - store[function_name]= - new unwindable_local_SSAt(goto_function, ns, options, heap_analysis); + store[function_name]=new unwindable_local_SSAt(goto_function, ns, options); } protected: diff --git a/src/ssa/ssa_heap_domain.cpp b/src/ssa/ssa_heap_domain.cpp deleted file mode 100644 index 63808d3cc..000000000 --- a/src/ssa/ssa_heap_domain.cpp +++ /dev/null @@ -1,494 +0,0 @@ -/*******************************************************************\ - -Module: Dynamic objects analysis - -Author: Viktor Malik - -\*******************************************************************/ - -/// \file -/// Dynamic objects analysis - -#include -#include "ssa_heap_domain.h" - -void ssa_heap_domaint::transform( - const namespacet &ns, - domain_baset::locationt from, - domain_baset::locationt to) -{ - if(from->is_assign()) - { - const code_assignt &assign=to_code_assign(from->code); - assign_lhs_rec(assign.lhs(), assign.rhs(), ns); - } - else if(from->is_function_call() && from->function==to->function) - { - const code_function_callt &fun_call=to_code_function_call(from->code); - assert(fun_call.function().id()==ID_symbol); - const irep_idt &fun_id=to_symbol_expr(fun_call.function()).get_identifier(); - - if(function_map.find(fun_id)!=function_map.end()) - { - unsigned counter=0; - for(auto &obj : function_map.at(fun_id).new_objects) - { - symbol_exprt new_obj=obj.first; - rename_to_caller(new_obj, from, counter); - - const symbolt *symbol; - if(!ns.lookup(new_obj.get_identifier(), symbol)) - new_obj=symbol->symbol_expr(); - - if(function_map[function].new_objects.find(new_obj)== - function_map[function].new_objects.end()) - { - function_map[function].new_objects.insert( - std::make_pair( - new_obj, - std::set())); - } - - for(auto &expr : obj.second) - { - const exprt pointer=function_map.at(fun_id).corresponding_expr( - expr, fun_call.arguments(), 0); - - objectst old_objects=value_map[pointer]; - value_map[pointer]={new_obj}; - - if(is_function_output(pointer, function, ns, false)) - { - function_map[function].new_objects.at(new_obj).insert(pointer); - } - - for(auto &o : old_objects) - { - if(o.id()==ID_symbol && o.type().get_bool("#dynamic") && - new_obj!=o) - function_map[function].new_objects.at(to_symbol_expr(o)).erase( - pointer); - } - } - } - - for(auto &obj : function_map.at(fun_id).modified_objects) - { - const exprt caller_obj=function_map.at(fun_id).corresponding_expr( - obj, fun_call.arguments(), 0); - if(is_function_output(caller_obj, function, ns, false)) - function_map[function].modified_objects.insert(caller_obj); - } - } - } -} - -bool ssa_heap_domaint::merge( - const ssa_heap_domaint &other, - domain_baset::locationt to) -{ - bool result=false; - - if(to->function=="" || to->function==other.function) - { - function=other.function; - - // Merge value maps - union - for(auto &other_value : other.value_map) - { - if(value_map.find(other_value.first)==value_map.end()) - { - value_map[other_value.first]=other_value.second; - result=true; - } - else - { - unsigned long old_size=value_map[other_value.first].size(); - value_map[other_value.first].insert( - other_value.second.begin(), - other_value.second.end()); - result=old_size!=value_map[other_value.first].size(); - } - } - } - else - { - function=to->function; - } - - for(auto &f : other.function_map) - { - auto &objects=function_map[f.first].new_objects; - const auto &other_objects=f.second.new_objects; - - if(f.first==function && function==other.function) - { - for(auto &other_object : other_objects) - { - if(objects.find(other_object.first)==objects.end()) - { - objects[other_object.first]=other_object.second; - result=true; - } - else if(!other_object.second.empty()) - { - unsigned long old_size=objects[other_object.first].size(); - std::set intersection; - std::set_intersection( - objects[other_object.first].begin(), - objects[other_object.first].end(), - other_object.second.begin(), - other_object.second.end(), - std::inserter( - intersection, - intersection.begin())); - if(!intersection.empty()) - objects[other_object.first]=intersection; - else - objects.erase(other_object.first); - - if(old_size!=objects[other_object.first].size()) - result=true; - } - } - } - else - { - for(auto &o : other_objects) - { - std::size_t old_size=objects[o.first].size(); - objects[o.first]=o.second; - if(old_size!=objects[o.first].size()) - result=true; - } - } - - function_map[f.first].params=f.second.params; - - std::size_t old_size=function_map[f.first].modified_objects.size(); - function_map[f.first].modified_objects.insert( - f.second.modified_objects.begin(), - f.second.modified_objects.end()); - if(old_size!=function_map[f.first].modified_objects.size()) - result=true; - } - - return result; -} - -void ssa_heap_domaint::assign_rhs( - const exprt &rhs, - const irep_idt &function, - objectst &objects, - const namespacet &ns) -{ - if(rhs.get_bool("#malloc_result")) - { - exprt malloc_result=rhs; - if(malloc_result.id()==ID_typecast) - malloc_result=to_typecast_expr(malloc_result).op(); - assert(malloc_result.id()==ID_address_of); - - const symbol_exprt new_object=to_symbol_expr( - to_address_of_expr(malloc_result).object()); - - function_infot &function_info=function_map[function]; - if(function_info.new_objects.find(new_object)== - function_info.new_objects.end()) - { - function_info.new_objects.insert( - std::make_pair( - new_object, - std::set())); - } - - objects={new_object}; - } - else if(rhs.id()==ID_typecast) - { - assign_rhs(to_typecast_expr(rhs).op(), function, objects, ns); - } - else - { - auto values=value_map.find(rhs); - if(values!=value_map.end()) - { - objects=values->second; - } - } -} - -bool ssa_heap_domaint::is_function_output( - const exprt &expr, - const irep_idt &function, - const namespacet &ns, - bool in_deref) -{ - if(expr.id()==ID_dereference) - { - return is_function_output( - to_dereference_expr(expr).pointer(), - function, - ns, - true); - } - else if(expr.id()==ID_member) - { - return is_function_output( - to_member_expr(expr).compound(), - function, - ns, - in_deref); - } - else if(expr.id()==ID_symbol) - { - const symbol_exprt &symbol_expr=to_symbol_expr(expr); - if(id2string(symbol_expr.get_identifier()).find("#return_value")!= - std::string::npos) - { - return symbol_expr.get_identifier()==id2string(function)+"#return_value"; - } - - const symbolt *symbol; - if(!ns.lookup(symbol_expr.get_identifier(), symbol) && - ((in_deref && symbol->is_parameter) || !symbol->is_procedure_local())) - return true; - } - return false; -} - -const std::set ssa_heap_domaint::value(const exprt &expr) const -{ - std::set result; - if(value_map.find(expr)!=value_map.end()) - { - for(auto &value : value_map.at(expr)) - { - if(value.id()==ID_symbol) - result.insert(to_symbol_expr(value)); - } - } - return result; -} - -const std::list ssa_heap_domaint::new_objects() const -{ - return new_objects(function); -} - -const std::list ssa_heap_domaint::new_objects( - const irep_idt &fname) const -{ - std::list result; - if(function_map.find(fname)!=function_map.end()) - { - for(auto &obj : function_map.at(fname).new_objects) - result.push_back(obj.first); - } - return result; -} - -void ssa_heap_domaint::rename_to_caller( - symbol_exprt &object, - domain_baset::locationt loc, - unsigned &index) const -{ - object.set_identifier( - "ssa::dynamic_object$"+std::to_string(loc->location_number)+"$"+ - std::to_string(index++)); -} - -const std::list ssa_heap_domaint::new_caller_objects( - const irep_idt &fname, - domain_baset::locationt loc) const -{ - std::list result=new_objects(fname); - unsigned counter=0; - for(symbol_exprt &o : result) - { - rename_to_caller(o, loc, counter); - } - return result; -} - -const std::set ssa_heap_domaint::modified_objects( - const irep_idt &fname) const -{ - std::set result; - if(function_map.find(fname)!=function_map.end()) - { - result=function_map.at(fname).modified_objects; - } - return result; -} - -void ssa_heap_domaint::assign_lhs_rec( - const exprt &lhs, - const exprt &rhs, - const namespacet &ns) -{ - objectst rhs_objects; - assign_rhs(rhs, function, rhs_objects, ns); - - if(!rhs_objects.empty()) - value_map[lhs]=rhs_objects; - else - value_map.erase(lhs); - - if(is_function_output(lhs, function, ns, false)) - { - auto &objects=function_map[function].new_objects; - for(const exprt &o : rhs_objects) - { - if(o.id()==ID_symbol && o.type().get_bool("#dynamic")) - { - const symbol_exprt new_o=to_symbol_expr(o); - if(objects.find(new_o)!=objects.end()) - { - objects[new_o].insert(lhs); - } - } - } - } - - update_modified(lhs, ns); -} - -void ssa_heap_domaint::update_modified(const exprt &expr, const namespacet &ns) -{ - if(expr.id()==ID_member) - { - update_modified(to_member_expr(expr).compound(), ns); - } - else if(expr.id()==ID_dereference) - { - for(const exprt &v : value_map[to_dereference_expr(expr).pointer()]) - { - if(is_function_output(v, function, ns, false)) - function_map[function].modified_objects.insert(v); - } - } - else if(is_function_output(expr, function, ns, false)) - function_map[function].modified_objects.insert(expr); -} - -void ssa_heap_analysist::initialize(const goto_functionst &goto_functions) -{ - static_analysis_baset::initialize(goto_functions); - - if(goto_functions.function_map.at("main").body_available()) - { - locationt e=goto_functions.function_map.at( - "main").body.instructions.begin(); - ssa_heap_domaint &entry=operator[](e); - - entry.function=e->function; - - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - locationt f_e=f_it->second.body.instructions.begin(); - ssa_heap_domaint &f_entry=operator[](f_e); - for(auto ¶m : f_it->second.type.parameters()) - { - entry.function_map[f_it->first].params.push_back( - param.get_identifier()); - const symbol_exprt param_expr(param.get_identifier(), param.type()); - init_ptr_param(param_expr, f_entry); - } - } - } - } -} - -void ssa_heap_analysist::init_ptr_param( - const exprt &expr, - ssa_heap_domaint &f_entry) -{ - const typet &type=ns.follow(expr.type()); - if(type.id()==ID_pointer) - { - const dereference_exprt dereference(expr, type.subtype()); - f_entry.value_map[expr].insert(dereference); - init_ptr_param(dereference, f_entry); - } - else if(type.id()==ID_struct) - { - assert(expr.id()==ID_dereference); - for(auto &component : to_struct_type(type).components()) - { - if(component.type().id()==ID_pointer && - ns.follow(component.type().subtype())==type) - { - const member_exprt member(expr, component.get_name(), component.type()); - f_entry.value_map[member].insert(expr); - } - } - } -} - -const exprt ssa_heap_domaint::function_infot::corresponding_expr( - const exprt &expr, - const code_function_callt::argumentst &arguments, - unsigned deref_level) const -{ - if(expr.id()==ID_symbol) - { - const irep_idt expr_id=to_symbol_expr(expr).get_identifier(); - exprt result=expr; - for(std::size_t i=0; i - -class ssa_heap_domaint:public domain_baset -{ -public: - virtual void transform( - const namespacet &ns, - locationt from, - locationt to) override; - bool merge(const ssa_heap_domaint &, locationt); - - irep_idt function; - - typedef std::set objectst; - std::map value_map; - - const std::set value(const exprt &expr) const; - - class function_infot - { - public: - std::map > new_objects; - std::set modified_objects; - std::vector params; - - const exprt corresponding_expr( - const exprt &expr, - const code_function_callt::argumentst &arguments, - unsigned deref_level) const; - - protected: - const exprt apply_deref(const exprt &expr, unsigned level) const; - }; - - std::map function_map; - - const std::list new_objects() const; - const std::list new_objects(const irep_idt &fname) const; - const std::list - new_caller_objects(const irep_idt &fname, locationt loc) const; - - const std::set modified_objects(const irep_idt &fname) const; -protected: - void assign_lhs_rec(const exprt &lhs, const exprt &rhs, const namespacet &ns); - - void assign_rhs( - const exprt &rhs, - const irep_idt &function, - objectst &objects, - const namespacet &ns); - - bool is_function_output( - const exprt &expr, - const irep_idt &function, - const namespacet &ns, - bool in_deref); - - void rename_to_caller( - symbol_exprt &object, - locationt loc, - unsigned &index) const; - - void update_modified(const exprt &expr, const namespacet &ns); -}; - -class ssa_heap_analysist:public static_analysist -{ -public: - explicit ssa_heap_analysist(const namespacet &_ns): - static_analysist(_ns) {} - - virtual void initialize(const goto_functionst &goto_functions) override; - -protected: - void init_ptr_param(const exprt &expr, ssa_heap_domaint &f_entry); -}; - - -#endif // CPROVER_2LS_SSA_SSA_HEAP_DOMAIN_H diff --git a/src/ssa/ssa_inliner.cpp b/src/ssa/ssa_inliner.cpp index 2c437ccec..378d3f6d8 100644 --- a/src/ssa/ssa_inliner.cpp +++ b/src/ssa/ssa_inliner.cpp @@ -58,8 +58,6 @@ void ssa_inlinert::get_summary( std::cout << std::endl; #endif - bindings.push_back(get_replace_new_objects(SSA, *f_it, loc, summary)); - // equalities for arguments bindings.push_back( get_replace_params( @@ -1211,56 +1209,3 @@ bool ssa_inlinert::cs_heap_covered(const exprt &expr) covered_cs_heap_out.end(); } -exprt ssa_inlinert::get_replace_new_objects( - const local_SSAt &SSA, - const function_application_exprt funapp_expr, - local_SSAt::locationt loc, - const summaryt &summary) -{ - exprt::operandst binding; - - const irep_idt &fname=to_symbol_expr(funapp_expr.function()).get_identifier(); - - auto next_loc=loc; - ++next_loc; - if(SSA.heap_analysis.has_location(next_loc)) - { - const ssa_heap_domaint &heap_domain=SSA.heap_analysis[next_loc]; - - const std::list callee_objects= - heap_domain.new_objects(fname); - const std::list caller_objects= - heap_domain.new_caller_objects(fname, loc); - - auto callee_it=callee_objects.begin(); - for(auto caller_it=caller_objects.begin(); caller_it!=caller_objects.end(); - ++caller_it, ++callee_it) - { - const typet symbol_type=caller_it->type(); - const typet type=SSA.ns.follow(symbol_type); - - const exprt lhs_expr= - param_out_transformer(*callee_it, type, summary.globals_out); - const exprt rhs_expr= - arg_out_transformer(*caller_it, symbol_type, type, SSA, loc); - binding.push_back(equal_exprt(lhs_expr, rhs_expr)); - - if(type.id()==ID_struct) - { - for(auto &component : to_struct_type(type).components()) - { - const exprt lhs_comp_expr= - param_out_member_transformer( - *callee_it, - component, - summary.globals_out); - const exprt rhs_comp_expr= - arg_out_member_transformer(*caller_it, component, SSA, loc); - binding.push_back(equal_exprt(lhs_comp_expr, rhs_comp_expr)); - } - } - } - } - - return conjunction(binding); -} diff --git a/src/ssa/ssa_inliner.h b/src/ssa/ssa_inliner.h index 4d0734985..f5bc70ad9 100644 --- a/src/ssa/ssa_inliner.h +++ b/src/ssa/ssa_inliner.h @@ -150,11 +150,6 @@ class ssa_inlinert:public messaget const function_application_exprt &funapp_expr, const local_SSAt &SSA, local_SSAt::locationt loc); - exprt get_replace_new_objects( - const local_SSAt &SSA, - const function_application_exprt funapp_expr, - local_SSAt::locationt loc, - const summaryt &summary); void rename(exprt &expr); void rename(local_SSAt::nodet &node); diff --git a/src/ssa/ssa_object.cpp b/src/ssa/ssa_object.cpp index e3aefa4e3..79b8d271f 100644 --- a/src/ssa/ssa_object.cpp +++ b/src/ssa/ssa_object.cpp @@ -213,18 +213,6 @@ void ssa_objectst::collect_objects( collect_objects_rec(it->guard, ns, objects, literals); collect_objects_rec(it->code, ns, objects, literals); } - - // Add new objects created within the function - goto_programt::const_targett exit=--(src.body.instructions.end()); - if(heap_analysis.has_location(exit)) - { - const std::list &new_objects= - heap_analysis[exit].new_objects(); - for(const symbol_exprt &o : new_objects) - { - collect_objects_rec(o, ns, objects, literals); - } - } } void ssa_objectst::categorize_objects( diff --git a/src/ssa/ssa_object.h b/src/ssa/ssa_object.h index d04ab107c..5ec666a98 100644 --- a/src/ssa/ssa_object.h +++ b/src/ssa/ssa_object.h @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "ssa_pointed_objects.h" #include -#include "ssa_heap_domain.h" class ssa_objectt { @@ -134,13 +133,9 @@ class ssa_objectst typedef std::set literalst; literalst literals; - const ssa_heap_analysist &heap_analysis; - ssa_objectst( const goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - const ssa_heap_analysist &_heap_analysis): - heap_analysis(_heap_analysis) + const namespacet &ns) { collect_objects(goto_function, ns); categorize_objects(goto_function, ns); diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index dbd101c0a..8fa42c69b 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -13,6 +13,7 @@ Author: Peter Schrammel, Saurabh Joshi #define COMPETITION #include +#include #include "ssa_unwinder.h" diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp index acde85194..eb08782ff 100644 --- a/src/ssa/ssa_value_set.cpp +++ b/src/ssa/ssa_value_set.cpp @@ -60,11 +60,6 @@ void ssa_value_domaint::transform( const ssa_value_ait &value_analysis=static_cast(ai); - const ssa_heap_domaint *heap_domain=NULL; - if(value_analysis.heap_analysis.has_location(to)) - heap_domain=&value_analysis.heap_analysis[to]; - - // functions may alter state almost arbitrarily: // * any global-scoped variables // * any dirty locals @@ -93,24 +88,7 @@ void ssa_value_domaint::transform( { symbol_exprt pointed_obj=pointed_object(arg, ns); pointed_obj.type().set("#dynamic", true); - - std::set new_objects; - if(heap_domain) - new_objects=heap_domain->value(arg_expr); - if(new_objects.empty()) - { - new_objects.insert(pointed_obj); - } - - auto it=new_objects.begin(); - assign_lhs_rec(arg, address_of_exprt(*it), ns); - objects.push_back(*it); - - for(++it; it!=new_objects.end(); ++it) - { - assign_lhs_rec(arg, address_of_exprt(*it), ns, true); - objects.push_back(*it); - } + objects.push_back(pointed_obj); arg_expr=dereference_exprt(arg_expr, arg.type().subtype()); arg=pointed_obj; @@ -145,33 +123,9 @@ void ssa_value_domaint::transform( if(return_value.type().id()==ID_pointer && return_value.get_identifier()==id2string(fname)+"#return_value") { - std::set new_objects; - if(heap_domain) - new_objects=heap_domain->value(return_value); - if(new_objects.empty()) - { - symbol_exprt pointed_obj=pointed_object(return_value, ns); - pointed_obj.type().set("#dynamic", true); - new_objects.insert(pointed_obj); - } - - auto it=new_objects.begin(); - assign_lhs_rec(return_value, address_of_exprt(*it), ns); - objects.push_back(*it); - - for(++it; it!=new_objects.end(); ++it) - { - assign_lhs_rec(return_value, address_of_exprt(*it), ns, true); - objects.push_back(*it); - } - - if(heap_domain) - { - for(auto &new_o : heap_domain->new_caller_objects(fname, from)) - { - objects.push_back(new_o); - } - } + symbol_exprt pointed_obj=pointed_object(return_value, ns); + pointed_obj.type().set("#dynamic", true); + objects.push_back(pointed_obj); } } diff --git a/src/ssa/ssa_value_set.h b/src/ssa/ssa_value_set.h index 2337546d2..7b4a13908 100644 --- a/src/ssa/ssa_value_set.h +++ b/src/ssa/ssa_value_set.h @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "ssa_object.h" -#include "ssa_heap_domain.h" class ssa_value_domaint:public ai_domain_baset { @@ -120,11 +119,9 @@ class ssa_value_ait:public ait ssa_value_ait( const goto_functionst::goto_functiont &goto_function, const namespacet &ns_, - const optionst &_options, - const ssa_heap_analysist &_heap_analysis): + const optionst &_options): ns(ns_), - options(_options), - heap_analysis(_heap_analysis) + options(_options) { operator()(goto_function, ns_); } @@ -140,8 +137,6 @@ class ssa_value_ait:public ait const namespacet &ns; const optionst &options; - const ssa_heap_analysist &heap_analysis; - friend class ssa_value_domaint; }; diff --git a/src/ssa/ssa_var_collector.cpp b/src/ssa/ssa_var_collector.cpp index 8b6c26621..18b9bb43f 100644 --- a/src/ssa/ssa_var_collector.cpp +++ b/src/ssa/ssa_var_collector.cpp @@ -12,11 +12,11 @@ Author: Peter Schrammel, Stefan Marticek #include "ssa_var_collector.h" void ssa_var_collectort::add_var( - const domaint::vart &var, - const domaint::guardt &pre_guard, - domaint::guardt post_guard, - const domaint::kindt &kind, - domaint::var_specst &var_specs) + const vart &var, + const guardst::guardt &pre_guard, + guardst::guardt post_guard, + const guardst::kindt &kind, + var_specst &var_specs) { exprt aux_expr=true_exprt(); if(std_invariants && pre_guard.id()==ID_and) @@ -38,12 +38,12 @@ void ssa_var_collectort::add_var( } if(var.type().id()!=ID_array) { - var_specs.push_back(domaint::var_spect()); - domaint::var_spect &var_spec=var_specs.back(); - var_spec.pre_guard=pre_guard; - var_spec.post_guard=post_guard; - var_spec.aux_expr=aux_expr; - var_spec.kind=kind; + var_specs.push_back(var_spect()); + var_spect &var_spec=var_specs.back(); + var_spec.guards.pre_guard=pre_guard; + var_spec.guards.post_guard=post_guard; + var_spec.guards.aux_expr=aux_expr; + var_spec.guards.kind=kind; var_spec.var=var; } @@ -55,13 +55,13 @@ void ssa_var_collectort::add_var( to_integer(array_type.size(), size); for(mp_integer i=0; i +#include #include #include #include diff --git a/src/ssa/unwindable_local_ssa.h b/src/ssa/unwindable_local_ssa.h index cd2429821..c3fbba516 100644 --- a/src/ssa/unwindable_local_ssa.h +++ b/src/ssa/unwindable_local_ssa.h @@ -15,7 +15,6 @@ Author: Peter Schrammel, Saurabh Joshi #include #include "local_ssa.h" -#include "ssa_heap_domain.h" class unwindable_local_SSAt:public local_SSAt { @@ -24,9 +23,8 @@ class unwindable_local_SSAt:public local_SSAt const goto_functiont &_goto_function, const namespacet &_ns, const optionst &_options, - const ssa_heap_analysist &heap_analysis, const std::string &_suffix=""): - local_SSAt(_goto_function, _ns, _options, heap_analysis, _suffix), + local_SSAt(_goto_function, _ns, _options, _suffix), current_unwinding(-1) { compute_loop_hierarchy();