diff --git a/.gitignore b/.gitignore index dd06a376eff..cf449ea4f76 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,16 @@ # Local files generated by IDEs +.vs/* .vscode/* +~AutoRecover.* +*.sln +*.vcxproj* +scripts/__pycache__/* +src/goto-analyzer/taint_driver_scripts/.idea/* +/*.config +/*.creator +/*.creator.user +/*.files +/*.includes # compilation files *.lo diff --git a/COMPILING b/COMPILING index 60579fe9f3b..93fc65c2938 100644 --- a/COMPILING +++ b/COMPILING @@ -10,10 +10,10 @@ environments: - Solaris 11 -- FreeBSD 10 or 11 +- FreeBSD 11 - Cygwin - (We recommend the i686-pc-mingw32-g++ cross compiler, version 4.7 or above.) + (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or above.) - Microsoft's Visual Studio version 12 (2013), version 14 (2015), or version 15 (older versions won't work) @@ -29,16 +29,16 @@ COMPILATION ON LINUX We assume that you have a Debian/Ubuntu or Red Hat-like distribution. 0) You need a C/C++ compiler, Flex and Bison, and GNU make. - The GNU Make needs to be version 3.81 or higher. On Debian-like - distributions, do + The GNU Make needs to be version 3.81 or higher. + On Debian-like distributions, do - apt-get install g++ gcc flex bison make git libz-dev libwww-perl patch libzip-dev + apt-get install g++-6 gcc flex bison make git libwww-perl patch On Red Hat/Fedora or derivates, do yum install gcc gcc-c++ flex bison perl-libwww-perl patch - Note that you need g++ version 4.9 or newer. + Note that you need g++ version 5.2 or newer. 1) As a user, get the CBMC source via @@ -57,7 +57,7 @@ COMPILATION ON SOLARIS 11 1) As root, get the necessary development tools: pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git - pkg install --accept developer/gcc-49 + pkg install --accept developer/gcc-5 2) As a user, get the CBMC source via @@ -83,8 +83,8 @@ COMPILATION ON SOLARIS 11 It will mis-optimize MiniSat2. -COMPILATION ON FREEBSD 10/11 ----------------------------- +COMPILATION ON FREEBSD 11 +------------------------- 1) As root, get the necessary tools: diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc index 14ee7eb85a8..77b1aeea6d8 100644 --- a/regression/cbmc-java/VarLengthArrayTrace1/test.desc +++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc @@ -3,7 +3,7 @@ VarLengthArrayTrace1.class --trace ^EXIT=10$ ^SIGNAL=0$ -dynamic_3_array\[1l\]=10 +dynamic_3_array\[1.*\]=10 -- ^warning: ignoring assignment removed diff --git a/regression/cbmc-java/classtest1/classtest1.class b/regression/cbmc-java/classtest1/classtest1.class new file mode 100644 index 00000000000..e105964df91 Binary files /dev/null and b/regression/cbmc-java/classtest1/classtest1.class differ diff --git a/regression/cbmc-java/classtest1/classtest1.java b/regression/cbmc-java/classtest1/classtest1.java new file mode 100644 index 00000000000..532926c474d --- /dev/null +++ b/regression/cbmc-java/classtest1/classtest1.java @@ -0,0 +1,11 @@ +public class classtest1 +{ + static void main(String[] args) + { + g(classtest1.class); + } + static void g(Object c) + { + assert true; + } +} diff --git a/regression/cbmc-java/classtest1/test.desc b/regression/cbmc-java/classtest1/test.desc new file mode 100644 index 00000000000..f56857c7bf6 --- /dev/null +++ b/regression/cbmc-java/classtest1/test.desc @@ -0,0 +1,8 @@ +CORE +classtest1.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 9e34fa7f422..4bd6cbdc141 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ pointer outside dynamic object bounds in \*p: FAILURE pointer outside dynamic object bounds in \*p: FAILURE -pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE -pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE +pointer outside dynamic object bounds in p2\[.*1\]: FAILURE +pointer outside dynamic object bounds in p2\[.*0\]: FAILURE \*\* 4 of 36 failed \(3 iterations\) -- ^warning: ignoring diff --git a/regression/cbmc/byte_update2/main.c b/regression/cbmc/byte_update2/main.c index 12493e4267c..cee6e19ecc4 100644 --- a/regression/cbmc/byte_update2/main.c +++ b/regression/cbmc/byte_update2/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718; diff --git a/regression/cbmc/byte_update3/main.c b/regression/cbmc/byte_update3/main.c index 6d9b3c293c0..e20eb6588c3 100644 --- a/regression/cbmc/byte_update3/main.c +++ b/regression/cbmc/byte_update3/main.c @@ -13,7 +13,7 @@ int main(int argc, char** argv) { x[3]=0x0708; x[4]=0x090a; - unsigned long* alias=(unsigned long*)(((char*)x)+0); + unsigned long long* alias=(unsigned long long*)(((char*)x)+0); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update4/main.c b/regression/cbmc/byte_update4/main.c index 0285f3058fe..2866b20a0ff 100644 --- a/regression/cbmc/byte_update4/main.c +++ b/regression/cbmc/byte_update4/main.c @@ -18,7 +18,7 @@ int main(int argc, char** argv) { x[8]=0x09; x[9]=0x0a; - unsigned long* alias=(unsigned long*)(((char*)x)+1); + unsigned long long* alias=(unsigned long long*)(((char*)x)+1); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update5/main.c b/regression/cbmc/byte_update5/main.c index e2f9da4defc..fc698a20143 100644 --- a/regression/cbmc/byte_update5/main.c +++ b/regression/cbmc/byte_update5/main.c @@ -13,7 +13,7 @@ int main(int argc, char** argv) { x[3]=0x0708; x[4]=0x090a; - unsigned long* alias=(unsigned long*)(((char*)x)+1); + unsigned long long* alias=(unsigned long long*)(((char*)x)+1); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update6/main.c b/regression/cbmc/byte_update6/main.c index cb92364572d..d0e3680b83a 100644 --- a/regression/cbmc/byte_update6/main.c +++ b/regression/cbmc/byte_update6/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718; diff --git a/regression/cbmc/byte_update7/main.c b/regression/cbmc/byte_update7/main.c index 599df60afd7..35690acc90d 100644 --- a/regression/cbmc/byte_update7/main.c +++ b/regression/cbmc/byte_update7/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718; diff --git a/regression/goto-instrument/inline_13/main.c b/regression/goto-instrument/inline_13/main.c new file mode 100644 index 00000000000..825cf41adf1 --- /dev/null +++ b/regression/goto-instrument/inline_13/main.c @@ -0,0 +1,18 @@ + +int x; + +void g() +{ + x = 1; +} + +void f() +{ + g(); +} + +int main() +{ + f(); +} + diff --git a/regression/goto-instrument/inline_13/test.desc b/regression/goto-instrument/inline_13/test.desc new file mode 100644 index 00000000000..675022c3d73 --- /dev/null +++ b/regression/goto-instrument/inline_13/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function-inline main --log - +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/inline_14/main.c b/regression/goto-instrument/inline_14/main.c new file mode 100644 index 00000000000..058c25c43b9 --- /dev/null +++ b/regression/goto-instrument/inline_14/main.c @@ -0,0 +1,23 @@ + +int x; + +void h() +{ + x = 1; +} + +void g() +{ + h(); +} + +void f() +{ + g(); +} + +int main() +{ + f(); +} + diff --git a/regression/goto-instrument/inline_14/test.desc b/regression/goto-instrument/inline_14/test.desc new file mode 100644 index 00000000000..77c30406741 --- /dev/null +++ b/regression/goto-instrument/inline_14/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function-inline main --log - --no-caching +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/inline_15/main.c b/regression/goto-instrument/inline_15/main.c new file mode 100644 index 00000000000..058c25c43b9 --- /dev/null +++ b/regression/goto-instrument/inline_15/main.c @@ -0,0 +1,23 @@ + +int x; + +void h() +{ + x = 1; +} + +void g() +{ + h(); +} + +void f() +{ + g(); +} + +int main() +{ + f(); +} + diff --git a/regression/goto-instrument/inline_15/test.desc b/regression/goto-instrument/inline_15/test.desc new file mode 100644 index 00000000000..9e1da6adc9c --- /dev/null +++ b/regression/goto-instrument/inline_15/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function-inline main --log - --no-caching --verbosity 9 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/slice02/test.desc b/regression/goto-instrument/slice02/test.desc index 362da05d33c..2d61905c826 100644 --- a/regression/goto-instrument/slice02/test.desc +++ b/regression/goto-instrument/slice02/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --full-slice ^EXIT=0$ diff --git a/regression/goto-instrument/slice14/test.desc b/regression/goto-instrument/slice14/test.desc index ef912633761..a2b36885fc7 100644 --- a/regression/goto-instrument/slice14/test.desc +++ b/regression/goto-instrument/slice14/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --full-slice ^EXIT=10$ diff --git a/regression/goto-instrument/slice16/test.desc b/regression/goto-instrument/slice16/test.desc index 0f63776547f..846baaf2a8b 100644 --- a/regression/goto-instrument/slice16/test.desc +++ b/regression/goto-instrument/slice16/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --full-slice --unwind 2 ^EXIT=0$ diff --git a/scripts/filter_lint_by_diff.py b/scripts/filter_lint_by_diff.py index 534c642a6ba..7a4c506e27e 100755 --- a/scripts/filter_lint_by_diff.py +++ b/scripts/filter_lint_by_diff.py @@ -11,20 +11,19 @@ added_lines = set() repository_root = sys.argv[2] -with open(sys.argv[1], "r") as f: - diff = unidiff.PatchSet(f) - for diff_file in diff: - filename = diff_file.target_file - # Skip files deleted in the tip (b side of the diff): - if filename == "/dev/null": - continue - assert filename.startswith("b/") - filename = os.path.join(repository_root, filename[2:]) - added_lines.add((filename, 0)) - for diff_hunk in diff_file: - for diff_line in diff_hunk: - if diff_line.line_type == "+": - added_lines.add((filename, diff_line.target_line_no)) +diff = unidiff.PatchSet.from_filename(sys.argv[1]) +for diff_file in diff: + filename = diff_file.target_file + # Skip files deleted in the tip (b side of the diff): + if filename == "/dev/null": + continue + assert filename.startswith("b/") + filename = os.path.join(repository_root, filename[2:]) + added_lines.add((filename, 0)) + for diff_hunk in diff_file: + for diff_line in diff_hunk: + if diff_line.line_type == "+": + added_lines.add((filename, diff_line.target_line_no)) for l in sys.stdin: bits = l.split(":") diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 538f2c70dee..93588e209a7 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -94,6 +94,9 @@ void dep_graph_domaint::control_dependencies( from->is_assume()) control_deps.insert(from); + const irep_idt id=goto_programt::get_function_id(from); + const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id); + // check all candidates for M for(depst::iterator it=control_deps.begin(); @@ -111,15 +114,17 @@ void dep_graph_domaint::control_dependencies( // we could hard-code assume and goto handling here to improve // performance cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e= - dep_graph.cfg_post_dominators().cfg.entry_map.find(*it); - assert(e!=dep_graph.cfg_post_dominators().cfg.entry_map.end()); + pd.cfg.entry_map.find(*it); + + assert(e!=pd.cfg.entry_map.end()); + const cfg_post_dominatorst::cfgt::nodet &m= - dep_graph.cfg_post_dominators().cfg[e->second]; + pd.cfg[e->second]; for(const auto &edge : m.out) { const cfg_post_dominatorst::cfgt::nodet &m_s= - dep_graph.cfg_post_dominators().cfg[edge.first]; + pd.cfg[edge.first]; if(m_s.dominators.find(to)!=m_s.dominators.end()) post_dom_one=true; @@ -252,7 +257,7 @@ void dep_graph_domaint::transform( const namespacet &ns) { dependence_grapht *dep_graph=dynamic_cast(&ai); - assert(dep_graph!=0); + assert(dep_graph!=nullptr); // propagate control dependencies across function calls if(from->is_function_call()) @@ -260,22 +265,31 @@ void dep_graph_domaint::transform( goto_programt::const_targett next=from; ++next; - dep_graph_domaint *s= - dynamic_cast(&(dep_graph->get_state(next))); - assert(s!=0); - - depst::iterator it=s->control_deps.begin(); - for(const auto &c_dep : control_deps) + if(next==to) { - while(it!=s->control_deps.end() && *itcontrol_deps.end() || c_dep<*it) - s->control_deps.insert(it, c_dep); - else if(it!=s->control_deps.end()) - ++it; + control_dependencies(from, to, *dep_graph); + } + else + { + // edge to function entry point + + dep_graph_domaint *s= + dynamic_cast(&(dep_graph->get_state(next))); + assert(s!=nullptr); + + depst::iterator it=s->control_deps.begin(); + for(const auto &c_dep : control_deps) + { + while(it!=s->control_deps.end() && *itcontrol_deps.end() || c_dep<*it) + s->control_deps.insert(it, c_dep); + else if(it!=s->control_deps.end()) + ++it; + } + + control_deps.clear(); } - - control_dependencies(from, next, *dep_graph); } else control_dependencies(from, to, *dep_graph); diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index f82d6f369ec..8b627dd36b0 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -154,6 +154,8 @@ class dependence_grapht: using ait::operator[]; using grapht::operator[]; + typedef std::map post_dominators_mapt; + explicit dependence_grapht(const namespacet &_ns): ns(_ns), rd(ns) @@ -169,7 +171,13 @@ class dependence_grapht: void initialize(const goto_programt &goto_program) { ait::initialize(goto_program); - post_dominators(goto_program); + + if(!goto_program.empty()) + { + const irep_idt id=goto_programt::get_function_id(goto_program); + cfg_post_dominatorst &pd=post_dominators[id]; + pd(goto_program); + } } void add_dep( @@ -177,7 +185,7 @@ class dependence_grapht: goto_programt::const_targett from, goto_programt::const_targett to); - const cfg_post_dominatorst &cfg_post_dominators() const + const post_dominators_mapt &cfg_post_dominators() const { return post_dominators; } @@ -205,7 +213,7 @@ class dependence_grapht: protected: const namespacet &ns; - cfg_post_dominatorst post_dominators; + post_dominators_mapt post_dominators; reaching_definitions_analysist rd; }; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 4c080b10ceb..e33e700e0ca 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -900,13 +900,6 @@ bool cbmc_parse_optionst::process_goto_program( // Similar removal of RTTI inspection: remove_instanceof(symbol_table, goto_functions); - // full slice? - if(cmdline.isset("full-slice")) - { - status() << "Performing a full slice" << eom; - full_slicer(goto_functions, ns); - } - // do partial inlining status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); @@ -920,6 +913,14 @@ bool cbmc_parse_optionst::process_goto_program( // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(ns, options, goto_functions); + + // full slice? + if(cmdline.isset("full-slice")) + { + status() << "Performing a full slice" << eom; + full_slicer(goto_functions, ns); + } + // checks don't know about adjusted float expressions adjust_float_expressions(goto_functions, ns); diff --git a/src/cbmc/version.h b/src/cbmc/version.h index d7a7a08a8ed..017ded44272 100644 --- a/src/cbmc/version.h +++ b/src/cbmc/version.h @@ -1,6 +1,6 @@ #ifndef CPROVER_CBMC_VERSION_H #define CPROVER_CBMC_VERSION_H -#define CBMC_VERSION "5.6" +#define CBMC_VERSION "5.7" #endif // CPROVER_CBMC_VERSION_H diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index b706e789c29..4cbd6121b24 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -37,7 +37,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../json/json$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../miniz/miniz$(OBJEXT) \ ../json/json$(LIBEXT) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index b82ecc35bd9..46914d78fb0 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -9,6 +9,7 @@ Date: February 2016 \*******************************************************************/ #include +#include #include #include @@ -291,20 +292,13 @@ const symbolt &code_contractst::new_tmp_symbol( const typet &type, const source_locationt &source_location) { - auxiliary_symbolt new_symbol; - new_symbol.type=type; - new_symbol.location=source_location; - - symbolt *symbol_ptr; - - do - { - new_symbol.base_name="tmp_cc$"+std::to_string(++temporary_counter); - new_symbol.name=new_symbol.base_name; - } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; + return get_fresh_aux_symbol( + type, + "", + "tmp_cc", + source_location, + irep_idt(), + symbol_table); } /*******************************************************************\ diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 4eb720744e3..59bda7f0af0 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -140,7 +140,7 @@ Function: full_slicert::add_jumps void full_slicert::add_jumps( queuet &queue, jumpst &jumps, - const cfg_post_dominatorst &cfg_post_dominators) + const dependence_grapht::post_dominators_mapt &post_dominators) { // Based on: // On slicing programs with jump statements @@ -197,11 +197,16 @@ void full_slicert::add_jumps( continue; } + const irep_idt id=goto_programt::get_function_id(j.PC); + const cfg_post_dominatorst &pd=post_dominators.at(id); + cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e= - cfg_post_dominators.cfg.entry_map.find(j.PC); - assert(e!=cfg_post_dominators.cfg.entry_map.end()); + pd.cfg.entry_map.find(j.PC); + + assert(e!=pd.cfg.entry_map.end()); + const cfg_post_dominatorst::cfgt::nodet &n= - cfg_post_dominators.cfg[e->second]; + pd.cfg[e->second]; // find the nearest post-dominator in slice if(n.dominators.find(lex_succ)==n.dominators.end()) @@ -226,11 +231,16 @@ void full_slicert::add_jumps( if(cfg[entry->second].node_required) { + const irep_idt id2=goto_programt::get_function_id(*d_it); + assert(id==id2); + cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2= - cfg_post_dominators.cfg.entry_map.find(*d_it); - assert(e2!=cfg_post_dominators.cfg.entry_map.end()); + pd.cfg.entry_map.find(*d_it); + + assert(e2!=pd.cfg.entry_map.end()); + const cfg_post_dominatorst::cfgt::nodet &n2= - cfg_post_dominators.cfg[e2->second]; + pd.cfg[e2->second]; if(n2.dominators.size()>post_dom_size) { diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index cf5be5685c2..4495fa95246 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -95,7 +95,7 @@ class full_slicert void add_jumps( queuet &queue, jumpst &jumps, - const cfg_post_dominatorst &cfg_post_dominators); + const dependence_grapht::post_dominators_mapt &post_dominators); void add_to_queue( queuet &queue, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 0a322cf299f..f747f87f3dc 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1052,6 +1052,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() std::string function=cmdline.get_value("function-inline"); assert(!function.empty()); + bool caching=!cmdline.isset("no-caching"); + do_indirect_call_and_rtti_removal(); status() << "Inlining calls of function `" << function << "'" << eom; @@ -1063,7 +1065,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() function, ns, ui_message_handler, - true); + true, + caching); } else { @@ -1076,7 +1079,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() function, ns, ui_message_handler, - true); + true, + caching); if(have_file) { @@ -1432,6 +1436,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // full slice? if(cmdline.isset("full-slice")) { + remove_returns(symbol_table, goto_functions); do_indirect_call_and_rtti_removal(); status() << "Performing a full slice" << eom; @@ -1547,6 +1552,7 @@ void goto_instrument_parse_optionst::help() " --inline perform full inlining\n" " --partial-inline perform partial inlining\n" " --function-inline transitively inline all calls makes\n" // NOLINT(*) + " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) " --add-library add models of C library functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1db5f0bdb4d..d3efb975767 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -53,7 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-struct-alignment)(interval-analysis)(show-intervals)" \ "(show-uninitialized)(show-locations)" \ "(full-slice)(reachability-slice)(slice-global-inits)" \ - "(inline)(partial-inline)(function-inline):(log):" \ + "(inline)(partial-inline)(function-inline):(log):(no-caching)" \ "(remove-function-pointers)" \ "(show-claims)(show-properties)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 9b5b44a44d9..c7fa8637194 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -33,24 +34,21 @@ symbol_exprt goto_convertt::make_compound_literal( { const source_locationt source_location=expr.find_source_location(); - auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - - do - { - new_symbol.base_name="literal$"+std::to_string(++temporary_counter); - new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); - new_symbol.is_static_lifetime=source_location.get_function().empty(); - new_symbol.value=expr; - new_symbol.type=expr.type(); - new_symbol.location=source_location; - } - while(symbol_table.move(new_symbol, symbol_ptr)); + symbolt &new_symbol= + get_fresh_aux_symbol( + expr.type(), + tmp_symbol_prefix, + "literal", + source_location, + irep_idt(), + symbol_table); + new_symbol.is_static_lifetime=source_location.get_function().empty(); + new_symbol.value=expr; // The value might depend on a variable, thus // generate code for this. - symbol_exprt result=symbol_ptr->symbol_expr(); + symbol_exprt result=new_symbol.symbol_expr(); result.add_source_location()=source_location; // The lifetime of compound literals is really that of @@ -62,7 +60,7 @@ symbol_exprt goto_convertt::make_compound_literal( convert(code_assign, dest); // now create a 'dead' instruction - if(!symbol_ptr->is_static_lifetime) + if(!new_symbol.is_static_lifetime) { code_deadt code_dead(result); targets.destructor_stack.push_back(code_dead); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 58cf6666897..25118d0b223 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -2754,24 +2755,21 @@ symbolt &goto_convertt::new_tmp_symbol( goto_programt &dest, const source_locationt &source_location) { - auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - - do - { - new_symbol.base_name="tmp_"+suffix+"$"+std::to_string(++temporary_counter); - new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); - new_symbol.type=type; - new_symbol.location=source_location; - } - while(symbol_table.move(new_symbol, symbol_ptr)); + symbolt &new_symbol= + get_fresh_aux_symbol( + type, + tmp_symbol_prefix, + "tmp_"+suffix, + source_location, + irep_idt(), + symbol_table); code_declt decl; - decl.symbol()=symbol_ptr->symbol_expr(); + decl.symbol()=new_symbol.symbol_expr(); decl.add_source_location()=source_location; convert_decl(decl, dest); - return *symbol_ptr; + return new_symbol; } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 05c35efa3c0..b018810e76e 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -32,7 +32,7 @@ class goto_convertt:public messaget symbol_table(_symbol_table), ns(_symbol_table), temporary_counter(0), - tmp_symbol_prefix("goto_convertt::") + tmp_symbol_prefix("goto_convertt") { } diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index c8c97f8d4a5..3c7359edebd 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -278,13 +278,15 @@ void goto_function_inline( const irep_idt function, const namespacet &ns, message_handlert &message_handler, - bool adjust_function) + bool adjust_function, + bool caching) { goto_inlinet goto_inline( goto_functions, ns, message_handler, - adjust_function); + adjust_function, + caching); goto_functionst::function_mapt::iterator f_it= goto_functions.function_map.find(function); @@ -332,13 +334,15 @@ jsont goto_function_inline_and_log( const irep_idt function, const namespacet &ns, message_handlert &message_handler, - bool adjust_function) + bool adjust_function, + bool caching) { goto_inlinet goto_inline( goto_functions, ns, message_handler, - adjust_function); + adjust_function, + caching); goto_functionst::function_mapt::iterator f_it= goto_functions.function_map.find(function); @@ -354,6 +358,7 @@ jsont goto_function_inline_and_log( // gather all calls goto_inlinet::inline_mapt inline_map; + // create empty call list goto_inlinet::call_listt &call_list=inline_map[f_it->first]; goto_programt &goto_program=goto_function.body; diff --git a/src/goto-programs/goto_inline.h b/src/goto-programs/goto_inline.h index 33566319100..5d3dd54fa6d 100644 --- a/src/goto-programs/goto_inline.h +++ b/src/goto-programs/goto_inline.h @@ -50,20 +50,23 @@ void goto_function_inline( goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, - bool adjust_function=false); + bool adjust_function=false, + bool caching=true); void goto_function_inline( goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, - bool adjust_function=false); + bool adjust_function=false, + bool caching=true); jsont goto_function_inline_and_log( goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, - bool adjust_function=false); + bool adjust_function=false, + bool caching=true); #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 5afb49f7ae3..ed423a35629 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -682,6 +682,20 @@ void goto_inlinet::expand_function_call( function, arguments, constrain); + + progress() << "Inserting " << identifier << " into caller" << eom; + progress() << "Number of instructions: " + << cached.body.instructions.size() << eom; + + if(!caching) + { + progress() << "Removing " << identifier << " from cache" << eom; + progress() << "Number of instructions: " + << cached.body.instructions.size() << eom; + + inline_log.cleanup(cached.body); + cache.erase(identifier); + } } else { @@ -944,6 +958,11 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive( goto_functiont &cached=cache[identifier]; assert(cached.body.empty()); + + progress() << "Creating copy of " << identifier << eom; + progress() << "Number of instructions: " + << goto_function.body.instructions.size() << eom; + cached.copy_from(goto_function); // location numbers not changed inline_log.copy_from(goto_function.body, cached.body); @@ -1146,6 +1165,29 @@ void goto_inlinet::output_inline_map( /*******************************************************************\ +Function: output_cache + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::output_cache(std::ostream &out) const +{ + for(auto it=cache.begin(); it!=cache.end(); it++) + { + if(it!=cache.begin()) + out << ", "; + + out << it->first << "\n"; + } +} + +/*******************************************************************\ + Function: cleanup Inputs: @@ -1257,8 +1299,9 @@ void goto_inlinet::goto_inline_logt::copy_from( assert(it1->location_number==it2->location_number); log_mapt::const_iterator l_it=log_map.find(it1); - if(l_it!=log_map.end()) + if(l_it!=log_map.end()) // a segment starts here { + // as 'to' is a fresh copy assert(log_map.find(it2)==log_map.end()); goto_inline_log_infot info=l_it->second; diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 495ce7d9155..e043bf48807 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -24,11 +24,13 @@ class goto_inlinet:public messaget goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, - bool adjust_function): + bool adjust_function, + bool caching=true): messaget(message_handler), goto_functions(goto_functions), ns(ns), - adjust_function(adjust_function) + adjust_function(adjust_function), + caching(caching) { } @@ -64,6 +66,8 @@ class goto_inlinet:public messaget std::ostream &out, const inline_mapt &inline_map); + void output_cache(std::ostream &out) const; + // call after goto_functions.update()! jsont output_inline_log_json() { @@ -127,6 +131,8 @@ class goto_inlinet:public messaget const namespacet &ns; const bool adjust_function; + const bool caching; + goto_inline_logt inline_log; void goto_inline_nontransitive( diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index bd9cb39c73e..14f9e4a519e 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -288,6 +288,23 @@ class goto_program_templatet return t; } + static const irep_idt get_function_id( + const_targett l) + { + while(!l->is_end_function()) + l++; + + return l->function; + } + + static const irep_idt get_function_id( + const goto_program_templatet &p) + { + assert(!p.empty()); + + return get_function_id(--p.instructions.end()); + } + void get_successors( targett target, targetst &successors); diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index b5dac445fda..3893729a1e1 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -68,8 +69,6 @@ class remove_function_pointerst code_function_callt &function_call, goto_programt &dest); - symbolt &new_tmp_symbol(); - void compute_address_taken_in_symbols( std::set &address_taken) { @@ -110,37 +109,6 @@ remove_function_pointerst::remove_function_pointerst( /*******************************************************************\ -Function: remove_function_pointerst::new_tmp_symbol - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -symbolt &remove_function_pointerst::new_tmp_symbol() -{ - static int temporary_counter; - - auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - - do - { - new_symbol.base_name= - "tmp_return_val$"+std::to_string(++temporary_counter); - new_symbol.name= - "remove_function_pointers::"+id2string(new_symbol.base_name); - } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; -} - -/*******************************************************************\ - Function: remove_function_pointerst::arg_is_type_compatible Inputs: @@ -311,9 +279,14 @@ void remove_function_pointerst::fix_return_type( code_type.return_type(), ns)) return; - symbolt &tmp_symbol=new_tmp_symbol(); - tmp_symbol.type=code_type.return_type(); - tmp_symbol.location=function_call.source_location(); + symbolt &tmp_symbol= + get_fresh_aux_symbol( + code_type.return_type(), + "remove_function_pointers", + "tmp_return_val", + function_call.source_location(), + irep_idt(), + symbol_table); symbol_exprt tmp_symbol_expr; tmp_symbol_expr.type()=tmp_symbol.type; diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index ee7f5979332..3fc2699ef47 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -9,6 +9,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "class_hierarchy.h" #include "class_identifier.h" #include "remove_instanceof.h" +#include #include @@ -20,8 +21,7 @@ class remove_instanceoft goto_functionst &_goto_functions): symbol_table(_symbol_table), ns(_symbol_table), - goto_functions(_goto_functions), - lowered_count(0) + goto_functions(_goto_functions) { class_hierarchy(_symbol_table); } @@ -34,7 +34,6 @@ class remove_instanceoft namespacet ns; class_hierarchyt class_hierarchy; goto_functionst &goto_functions; - int lowered_count; bool lower_instanceof(goto_programt &); @@ -128,15 +127,14 @@ void remove_instanceoft::lower_instanceof( symbol_typet jlo("java::java.lang.Object"); exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns); - std::ostringstream symname; - symname << "instanceof_tmp::instanceof_tmp" << (++lowered_count); - auxiliary_symbolt newsym; - newsym.name=symname.str(); - newsym.type=object_clsid.type(); - newsym.base_name=newsym.name; - newsym.mode=ID_java; - newsym.is_type=false; - assert(!symbol_table.add(newsym)); + symbolt &newsym= + get_fresh_aux_symbol( + object_clsid.type(), + "instanceof_tmp", + "instanceof_tmp", + source_locationt(), + ID_java, + symbol_table); auto newinst=goto_program.insert_after(this_inst); newinst->make_assignment(); diff --git a/src/goto-programs/show_symbol_table.h b/src/goto-programs/show_symbol_table.h index a7cc99ec9ba..6e3b387f863 100644 --- a/src/goto-programs/show_symbol_table.h +++ b/src/goto-programs/show_symbol_table.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +class goto_modelt; + void show_symbol_table( const goto_modelt &, ui_message_handlert::uit ui); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index c8e6bbf5bb4..db5f63b08b9 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -40,6 +40,8 @@ java_bytecode_parse_treet &java_class_loadert::operator()( queue.push("java.lang.Object"); // java.lang.String queue.push("java.lang.String"); + // add java.lang.Class + queue.push("java.lang.Class"); queue.push(class_name); while(!queue.empty()) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 569a5895bdc..5234a53200f 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "java_entry_point.h" #include "java_object_factory.h" @@ -326,6 +327,24 @@ void java_record_outputs( init_code.move_to_operands(output); } } + + // record exceptional return variable as output + codet output(ID_output); + output.operands().resize(2); + + assert(symbol_table.has_symbol(id2string(function.name)+EXC_SUFFIX)); + + // retrieve the exception variable + const symbolt exc_symbol=symbol_table.lookup( + id2string(function.name)+EXC_SUFFIX); + + output.op0()=address_of_exprt( + index_exprt(string_constantt(exc_symbol.base_name), + from_integer(0, index_type()))); + output.op1()=exc_symbol.symbol_expr(); + output.add_source_location()=function.location; + + init_code.move_to_operands(output); } main_function_resultt get_main_symbol( @@ -592,6 +611,15 @@ bool java_entry_point( call_main.lhs()=return_symbol.symbol_expr(); } + // add the exceptional return value + auxiliary_symbolt exc_symbol; + exc_symbol.mode=ID_C; + exc_symbol.is_static_lifetime=false; + exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; + exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + exprt::operandst main_arguments= java_build_arguments( symbol, diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 0647b0dd37e..c06387469cf 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -108,8 +109,7 @@ exprt java_object_factoryt::allocate_object( bool cast_needed=allocate_type_resolved!=target_type; if(!create_dynamic_objects) { - symbolt &aux_symbol=new_tmp_symbol(symbol_table); - aux_symbol.type=allocate_type; + symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type); aux_symbol.is_static_lifetime=true; exprt object=aux_symbol.symbol_expr(); @@ -137,8 +137,11 @@ exprt java_object_factoryt::allocate_object( // Create a symbol for the malloc expression so we can initialize // without having to do it potentially through a double-deref, which // breaks the to-SSA phase. - symbolt &malloc_sym=new_tmp_symbol(symbol_table, "malloc_site"); - malloc_sym.type=pointer_typet(allocate_type); + symbolt &malloc_sym=new_tmp_symbol( + symbol_table, + loc, + pointer_typet(allocate_type), + "malloc_site"); code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); code_assignt &malloc_assign=assign; malloc_assign.add_source_location()=loc; @@ -506,8 +509,11 @@ void java_object_factoryt::gen_nondet_array_init( if(update_in_place==NO_UPDATE_IN_PLACE) { - symbolt &length_sym=new_tmp_symbol(symbol_table, "nondet_array_length"); - length_sym.type=java_int_type(); + const symbolt &length_sym=new_tmp_symbol( + symbol_table, + loc, + java_int_type(), + "nondet_array_length"); length_sym_expr=length_sym.symbol_expr(); // Initialise array with some undetermined length: @@ -560,8 +566,11 @@ void java_object_factoryt::gen_nondet_array_init( // Interpose a new symbol, as the goto-symex stage can't handle array indexing // via a cast. - symbolt &array_init_symbol=new_tmp_symbol(symbol_table, "array_data_init"); - array_init_symbol.type=init_array_expr.type(); + symbolt &array_init_symbol=new_tmp_symbol( + symbol_table, + loc, + init_array_expr.type(), + "array_data_init"); const auto &array_init_symexpr=array_init_symbol.symbol_expr(); codet data_assign=code_assignt(array_init_symexpr, init_array_expr); data_assign.add_source_location()=loc; @@ -569,8 +578,11 @@ void java_object_factoryt::gen_nondet_array_init( // Emit init loop for(array_init_iter=0; array_init_iter!=array.length; // ++array_init_iter) init(array[array_init_iter]); - symbolt &counter=new_tmp_symbol(symbol_table, "array_init_iter"); - counter.type=length_sym_expr.type(); + symbolt &counter=new_tmp_symbol( + symbol_table, + loc, + length_sym_expr.type(), + "array_init_iter"); exprt counter_expr=counter.symbol_expr(); exprt java_zero=from_integer(0, java_int_type()); @@ -707,22 +719,19 @@ Function: new_tmp_symbol \*******************************************************************/ -symbolt &new_tmp_symbol(symbol_tablet &symbol_table, const std::string &prefix) +symbolt &new_tmp_symbol( + symbol_tablet &symbol_table, + const source_locationt &loc, + const typet &type, + const std::string &prefix) { - static size_t temporary_counter=0; // TODO encapsulate as class variable - - auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - - do - { - new_symbol.name="tmp_object_factory$"+std::to_string(++temporary_counter); - new_symbol.base_name=new_symbol.name; - new_symbol.mode=ID_java; - } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; + return get_fresh_aux_symbol( + type, + "", + prefix, + loc, + ID_java, + symbol_table); } /*******************************************************************\ @@ -758,8 +767,10 @@ exprt object_factory( { if(type.id()==ID_pointer) { - symbolt &aux_symbol=new_tmp_symbol(symbol_table); - aux_symbol.type=type; + symbolt &aux_symbol=new_tmp_symbol( + symbol_table, + loc, + type); aux_symbol.is_static_lifetime=true; exprt object=aux_symbol.symbol_expr(); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index f0b77b343fb..9820efcb6cc 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -46,6 +46,8 @@ exprt get_nondet_bool(const typet &); symbolt &new_tmp_symbol( symbol_tablet &symbol_table, + const source_locationt &, + const typet &, const std::string &prefix="tmp_object_factory"); #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp index 2408f9816ed..3ed2a07bc7d 100644 --- a/src/pointer-analysis/value_set_analysis_fi.cpp +++ b/src/pointer-analysis/value_set_analysis_fi.cpp @@ -202,31 +202,21 @@ void value_set_analysis_fit::add_vars( get_globals(globals); value_set_fit &v=state.value_set; + v.add_vars(globals); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { // get the locals std::set locals; get_local_identifiers(f_it->second, locals); - forall_goto_program_instructions(i_it, f_it->second.body) + for(auto l : locals) { - v.add_vars(globals); + const symbolt &symbol=ns.lookup(l); - for(std::set::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) - { - const symbolt &symbol=ns.lookup(*l_it); - - std::list entries; - get_entries(symbol, entries); - v.add_vars(entries); - } + std::list entries; + get_entries(symbol, entries); + v.add_vars(entries); } } } diff --git a/src/pointer-analysis/value_set_analysis_fivr.cpp b/src/pointer-analysis/value_set_analysis_fivr.cpp index fe428100a72..0180768250c 100644 --- a/src/pointer-analysis/value_set_analysis_fivr.cpp +++ b/src/pointer-analysis/value_set_analysis_fivr.cpp @@ -84,33 +84,23 @@ void value_set_analysis_fivrt::add_vars( entry_cachet entry_cache; value_set_fivrt &v=state.value_set; + v.add_vars(globals); - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + for(auto l : locals) { - v.add_vars(globals); + // cache hit? + entry_cachet::const_iterator e_it=entry_cache.find(l); - for(goto_programt::decl_identifierst::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) + if(e_it==entry_cache.end()) { - // cache hit? - entry_cachet::const_iterator e_it=entry_cache.find(*l_it); + const symbolt &symbol=ns.lookup(l); - if(e_it==entry_cache.end()) - { - const symbolt &symbol=ns.lookup(*l_it); - - std::list &entries=entry_cache[*l_it]; - get_entries(symbol, entries); - v.add_vars(entries); - } - else - v.add_vars(e_it->second); + std::list &entries=entry_cache[l]; + get_entries(symbol, entries); + v.add_vars(entries); } + else + v.add_vars(e_it->second); } } @@ -202,31 +192,21 @@ void value_set_analysis_fivrt::add_vars( get_globals(globals); value_set_fivrt &v=state.value_set; + v.add_vars(globals); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { // get the locals std::set locals; get_local_identifiers(f_it->second, locals); - forall_goto_program_instructions(i_it, f_it->second.body) + for(auto l : locals) { - v.add_vars(globals); + const symbolt &symbol=ns.lookup(l); - for(std::set::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) - { - const symbolt &symbol=ns.lookup(*l_it); - - std::list entries; - get_entries(symbol, entries); - v.add_vars(entries); - } + std::list entries; + get_entries(symbol, entries); + v.add_vars(entries); } } } diff --git a/src/pointer-analysis/value_set_analysis_fivrns.cpp b/src/pointer-analysis/value_set_analysis_fivrns.cpp index d2f9e966437..1b7d2422186 100644 --- a/src/pointer-analysis/value_set_analysis_fivrns.cpp +++ b/src/pointer-analysis/value_set_analysis_fivrns.cpp @@ -84,33 +84,23 @@ void value_set_analysis_fivrnst::add_vars( entry_cachet entry_cache; value_set_fivrnst &v=state.value_set; + v.add_vars(globals); - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + for(auto l : locals) { - v.add_vars(globals); + // cache hit? + entry_cachet::const_iterator e_it=entry_cache.find(l); - for(goto_programt::decl_identifierst::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) + if(e_it==entry_cache.end()) { - // cache hit? - entry_cachet::const_iterator e_it=entry_cache.find(*l_it); + const symbolt &symbol=ns.lookup(l); - if(e_it==entry_cache.end()) - { - const symbolt &symbol=ns.lookup(*l_it); - - std::list &entries=entry_cache[*l_it]; - get_entries(symbol, entries); - v.add_vars(entries); - } - else - v.add_vars(e_it->second); + std::list &entries=entry_cache[l]; + get_entries(symbol, entries); + v.add_vars(entries); } + else + v.add_vars(e_it->second); } } @@ -202,31 +192,21 @@ void value_set_analysis_fivrnst::add_vars( get_globals(globals); value_set_fivrnst &v=state.value_set; + v.add_vars(globals); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { // get the locals std::set locals; get_local_identifiers(f_it->second, locals); - forall_goto_program_instructions(i_it, f_it->second.body) + for(auto l : locals) { - v.add_vars(globals); + const symbolt &symbol=ns.lookup(l); - for(std::set::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) - { - const symbolt &symbol=ns.lookup(*l_it); - - std::list entries; - get_entries(symbol, entries); - v.add_vars(entries); - } + std::list entries; + get_entries(symbol, entries); + v.add_vars(entries); } } } diff --git a/src/solvers/miniBDD/miniBDD.inc b/src/solvers/miniBDD/miniBDD.inc index a48f56770cd..091725ed333 100644 --- a/src/solvers/miniBDD/miniBDD.inc +++ b/src/solvers/miniBDD/miniBDD.inc @@ -2,21 +2,21 @@ // inline functions -mini_bddt::mini_bddt():node(0) +inline mini_bddt::mini_bddt():node(0) { } -mini_bddt::mini_bddt(const mini_bddt &x):node(x.node) +inline mini_bddt::mini_bddt(const mini_bddt &x):node(x.node) { if(is_initialized()) node->add_reference(); } -mini_bddt::mini_bddt(class mini_bdd_nodet *_node):node(_node) +inline mini_bddt::mini_bddt(class mini_bdd_nodet *_node):node(_node) { if(is_initialized()) node->add_reference(); } -mini_bddt &mini_bddt::operator=(const mini_bddt &x) +inline mini_bddt &mini_bddt::operator=(const mini_bddt &x) { assert(&x!=this); clear(); @@ -28,56 +28,56 @@ mini_bddt &mini_bddt::operator=(const mini_bddt &x) return *this; } -mini_bddt::~mini_bddt() +inline mini_bddt::~mini_bddt() { clear(); } -bool mini_bddt::is_constant() const +inline bool mini_bddt::is_constant() const { assert(is_initialized()); return node->node_number<=1; } -bool mini_bddt::is_true() const +inline bool mini_bddt::is_true() const { assert(is_initialized()); return node->node_number==1; } -bool mini_bddt::is_false() const +inline bool mini_bddt::is_false() const { assert(is_initialized()); return node->node_number==0; } -unsigned mini_bddt::var() const +inline unsigned mini_bddt::var() const { assert(is_initialized()); return node->var; } -unsigned mini_bddt::node_number() const +inline unsigned mini_bddt::node_number() const { assert(is_initialized()); return node->node_number; } -const mini_bddt &mini_bddt::low() const +inline const mini_bddt &mini_bddt::low() const { assert(is_initialized()); assert(node->node_number>=2); return node->low; } -const mini_bddt &mini_bddt::high() const +inline const mini_bddt &mini_bddt::high() const { assert(is_initialized()); assert(node->node_number>=2); return node->high; } -void mini_bddt::clear() +inline void mini_bddt::clear() { if(is_initialized()) { @@ -86,7 +86,7 @@ void mini_bddt::clear() } } -mini_bdd_nodet::mini_bdd_nodet( +inline mini_bdd_nodet::mini_bdd_nodet( class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high): @@ -96,33 +96,33 @@ mini_bdd_nodet::mini_bdd_nodet( { } -mini_bdd_mgrt::var_table_entryt::var_table_entryt( +inline mini_bdd_mgrt::var_table_entryt::var_table_entryt( const std::string &_label):label(_label) { } -const mini_bddt &mini_bdd_mgrt::True() const +inline const mini_bddt &mini_bdd_mgrt::True() const { return true_bdd; } -const mini_bddt &mini_bdd_mgrt::False() const +inline const mini_bddt &mini_bdd_mgrt::False() const { return false_bdd; } -void mini_bdd_nodet::add_reference() +inline void mini_bdd_nodet::add_reference() { reference_counter++; } -mini_bdd_mgrt::reverse_keyt::reverse_keyt( +inline mini_bdd_mgrt::reverse_keyt::reverse_keyt( unsigned _var, const mini_bddt &_low, const mini_bddt &_high): var(_var), low(_low.node->node_number), high(_high.node->node_number) { } -std::size_t mini_bdd_mgrt::number_of_nodes() +inline std::size_t mini_bdd_mgrt::number_of_nodes() { return nodes.size()-free.size(); } diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index 493271afd27..d7c89ed8921 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include #include @@ -1555,7 +1553,7 @@ void smt1_convt::convert_typecast( convert_expr(src, true); out << " "; convert_expr( - zero_initializer(src_type, expr.source_location(), ns), + from_integer(0, src_type), true); out << "))"; } @@ -1584,7 +1582,7 @@ void smt1_convt::convert_typecast( convert_expr(src, true); out << " "; convert_expr( - zero_initializer(src_type, expr.source_location(), ns), + from_integer(0, src_type), true); out << ")) "; // not, = out << " bv1[" << to_width << "]"; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d6fcd8f5b89..badc8646993 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include #include @@ -2089,8 +2087,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "(not (= "; convert_expr(src); out << " "; - convert_expr( - zero_initializer(src_type, expr.source_location(), ns)); + convert_expr(from_integer(0, src_type)); out << "))"; } else if(src_type.id()==ID_floatbv) @@ -2116,8 +2113,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << "(not (= "; convert_expr(src); out << " "; - convert_expr( - zero_initializer(src_type, expr.source_location(), ns)); + convert_expr(from_integer(0, src_type)); out << ")) "; // not, = out << " (_ bv1 " << to_width << ")"; out << " (_ bv0 " << to_width << ")"; diff --git a/src/symex/Makefile b/src/symex/Makefile index 51b672e7a72..e887ca55352 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -16,7 +16,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ - ../json/json$(LIBEXT) \ ../path-symex/path-symex$(LIBEXT) \ ../miniz/miniz$(OBJEXT) \ ../json/json$(LIBEXT) diff --git a/src/util/Makefile b/src/util/Makefile index 4cacd3dbc0f..e9dd739db8e 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -22,6 +22,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \ memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ ssa_expr.cpp json_irep.cpp json_expr.cpp \ + fresh_symbol.cpp \ format_number_range.cpp string_utils.cpp nondet_ifthenelse.cpp INCLUDES= -I .. diff --git a/src/util/fixedbv.h b/src/util/fixedbv.h index 14e5946c445..8354e0bef7c 100644 --- a/src/util/fixedbv.h +++ b/src/util/fixedbv.h @@ -46,6 +46,10 @@ class fixedbvt { } + explicit fixedbvt(const fixedbv_spect &_spec):spec(_spec), v(0) + { + } + explicit fixedbvt(const constant_exprt &expr); void from_integer(const mp_integer &i); @@ -68,6 +72,11 @@ class fixedbvt return v==0; } + static fixedbvt zero(const fixedbv_typet &type) + { + return fixedbvt(fixedbv_spect(type)); + } + void negate(); fixedbvt &operator/=(const fixedbvt &other); diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp new file mode 100644 index 00000000000..fbe6f09b871 --- /dev/null +++ b/src/util/fresh_symbol.cpp @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Fresh auxiliary symbol creation + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include "fresh_symbol.h" + +/*******************************************************************\ + +Function: get_fresh_aux_symbol + + Inputs: `type`: type of new symbol + `name_prefix`, `basename_prefix`: + new symbol will be named name_prefix::basename_prefix$num + unless name_prefix is empty, in which case the :: prefix + is omitted. + `source_location`: new symbol source loc + `symbol_mode`: new symbol mode + `symbol_table`: table to add the new symbol to + + Outputs: + + Purpose: Installs a fresh-named symbol with the requested name pattern + +\*******************************************************************/ + +symbolt &get_fresh_aux_symbol( + const typet &type, + const std::string &name_prefix, + const std::string &basename_prefix, + const source_locationt &source_location, + const irep_idt &symbol_mode, + symbol_tablet &symbol_table) +{ + static size_t temporary_counter=0; + auxiliary_symbolt new_symbol; + symbolt *symbol_ptr; + + do + { + new_symbol.base_name= + basename_prefix+ + "$"+ + std::to_string(++temporary_counter); + if(name_prefix.empty()) + new_symbol.name=new_symbol.base_name; + else + new_symbol.name= + name_prefix+ + "::"+ + id2string(new_symbol.base_name); + new_symbol.type=type; + new_symbol.location=source_location; + new_symbol.mode=symbol_mode; + } + while(symbol_table.move(new_symbol, symbol_ptr)); + + return *symbol_ptr; +} diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h new file mode 100644 index 00000000000..c3b2749cbe3 --- /dev/null +++ b/src/util/fresh_symbol.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Fresh auxiliary symbol creation + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_FRESH_SYMBOL_H +#define CPROVER_UTIL_FRESH_SYMBOL_H + +#include + +#include +#include +#include +#include + +symbolt &get_fresh_aux_symbol( + const typet &type, + const std::string &name_prefix, + const std::string &basename_prefix, + const source_locationt &source_location, + const irep_idt &symbol_mode, + symbol_tablet &symbol_table); + +#endif // CPROVER_UTIL_FRESH_SYMBOL_H diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index c051351e30d..20239cd92aa 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -169,6 +169,13 @@ class ieee_floatt infinity_flag=false; } + static ieee_floatt zero(const floatbv_typet &type) + { + ieee_floatt result(type); + result.make_zero(); + return result; + } + void make_NaN(); void make_plus_infinity(); void make_minus_infinity(); diff --git a/src/util/infix.h b/src/util/infix.h new file mode 100644 index 00000000000..2fcc1338d5d --- /dev/null +++ b/src/util/infix.h @@ -0,0 +1,22 @@ +/*******************************************************************\ + +Module: String infix shorthand + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_INFIX_H +#define CPROVER_UTIL_INFIX_H + +#include + +inline bool has_infix( + const std::string &s, + const std::string &infix, + size_t offset) +{ + return s.compare(offset, infix.size(), infix)==0; +} + +#endif diff --git a/src/util/irep_hash.h b/src/util/irep_hash.h index 1674caaf906..b0d24221ff3 100644 --- a/src/util/irep_hash.h +++ b/src/util/irep_hash.h @@ -148,6 +148,8 @@ inline std::size_t basic_hash_finalize( return h1; } +// Boost uses the symbol hash_combine, if you're getting problems here then +// you've probably included a Boost header after this one #define hash_combine(h1, h2) \ basic_hash_combine(h1, h2) #define hash_finalize(h1, len) \ diff --git a/src/util/json.h b/src/util/json.h index 1c817e2c78a..c6ddd1b1d19 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -147,13 +147,13 @@ class json_arrayt:public jsont jsont &push_back(const jsont &json) { array.push_back(json); - return static_cast(array.back()); + return array.back(); } jsont &push_back() { array.push_back(jsont()); - return static_cast(array.back()); + return array.back(); } }; diff --git a/src/util/language_file.h b/src/util/language_file.h index 9fffc7f14f1..f023047b32a 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -89,7 +89,7 @@ class language_filest:public messaget bool has_lazy_method(const irep_idt &id) { - return lazy_method_map.count(id); + return lazy_method_map.count(id)!=0; } // The method must have been added to the symbol table and registered diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h new file mode 100644 index 00000000000..23f08d0bb06 --- /dev/null +++ b/src/util/sharing_map.h @@ -0,0 +1,832 @@ +/*******************************************************************\ + +Module: Sharing map + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_SHARING_MAP_H +#define CPROVER_UTIL_SHARING_MAP_H + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +#define _sm_assert(b) assert(b) +//#define _sm_assert(b) + +#define SHARING_MAPT(R) \ + template \ + R sharing_mapt + +#define SHARING_MAPT2(CV, ST) \ + template \ + CV typename sharing_mapt::ST \ + sharing_mapt + +template < + class keyT, + class valueT, + class hashT=std::hash, + class predT=std::equal_to> +class sharing_mapt +{ +public: + friend void sharing_map_interface_test(); + friend void sharing_map_copy_test(); + friend void sharing_map_collision_test(); + friend void sharing_map_view_test(); + + ~sharing_mapt() + { + } + + typedef keyT key_type; + typedef valueT mapped_type; + typedef std::pair value_type; + + typedef hashT hash; + typedef predT key_equal; + + typedef sharing_mapt self_type; + typedef sharing_nodet node_type; + + typedef size_t size_type; + + typedef const std::pair const_find_type; + typedef const std::pair find_type; + + typedef std::vector keyst; + + typedef typename node_type::subt subt; + typedef typename node_type::containert containert; + + // key-value map + node_type map; + + // number of elements in the map + size_type num=0; + + // dummy element returned when no element was found + static mapped_type dummy; + + // compile-time configuration + + static const std::string not_found_msg; + + static const size_t bits; + static const size_t chunk; + + static const size_t mask; + static const size_t steps; + + // interface + + size_type erase( + const key_type &k, + const tvt &key_exists=tvt::unknown()); + + size_type erase_all( + const keyst &ks, + const tvt &key_exists=tvt::unknown()); // applies to all keys + + // return true if element was inserted + const_find_type insert( + const key_type &k, + const mapped_type &v, + const tvt &key_exists=tvt::unknown()); + + const_find_type insert( + const value_type &p, + const tvt &key_exists=tvt::unknown()); + + find_type place( + const key_type &k, + const mapped_type &v); + + find_type place( + const value_type &p); + + find_type find( + const key_type &k, + const tvt &key_exists=tvt::unknown()); + + const_find_type find(const key_type &k) const; + + mapped_type &at( + const key_type &k, + const tvt &key_exists=tvt::unknown()); + + const mapped_type &at(const key_type &k) const; + + mapped_type &operator[](const key_type &k); + + void swap(self_type &other) + { + map.swap(other.map); + + size_t tmp=num; + num=other.num; + other.num=tmp; + } + + size_type size() const + { + return num; + } + + bool empty() const + { + return num==0; + } + + void clear() + { + map.clear(); + num=0; + } + + bool has_key(const key_type &k) const + { + return get_leaf_node(k)!=nullptr; + } + + // views + + typedef std::pair view_itemt; + typedef std::vector viewt; + + class delta_view_itemt + { + public: + delta_view_itemt( + const bool in_both, + const key_type &k, + const mapped_type &m, + const mapped_type &other_m) : + in_both(in_both), + k(k), + m(m), + other_m(other_m) {} + + // if true key is in both maps, if false key is only in the map + // from which the view was obtained + const bool in_both; + + const key_type &k; + + const mapped_type &m; + const mapped_type &other_m; + }; + + typedef std::vector delta_viewt; + + void get_view(viewt &view) const; + + void get_delta_view( + const self_type &other, + delta_viewt &delta_view, + const bool only_common=true) const; + +protected: + // helpers + + node_type *get_container_node(const key_type &k); + const node_type *get_container_node(const key_type &k) const; + + const node_type *get_leaf_node(const key_type &k) const; + + void gather_all(const node_type &n, delta_viewt &delta_view) const; +}; + +/*******************************************************************\ + +Function: get_view + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT(void)::get_view(viewt &view) const +{ + assert(view.empty()); + + std::stack stack; + + if(empty()) + return; + + stack.push(&map); + + do + { + const node_type *n=stack.top(); + stack.pop(); + + if(n->is_container()) + { + for(const auto &child : n->get_container()) + { + view.push_back(view_itemt(child.get_key(), child.get_value())); + } + } + else + { + assert(n->is_internal()); + + for(const auto &child : n->get_sub()) + { + stack.push(&child.second); + } + } + } + while(!stack.empty()); +} + +/*******************************************************************\ + +Function: gather_all + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT(void)::gather_all(const node_type &n, delta_viewt &delta_view) + const +{ + std::stack stack; + stack.push(&n); + + do + { + const node_type *n=stack.top(); + stack.pop(); + + if(n->is_container()) + { + for(const auto &child : n->get_container()) + { + delta_view.push_back( + delta_view_itemt( + false, + child.get_key(), + child.get_value(), + dummy)); + } + } + else + { + assert(n->is_internal()); + + for(const auto &child : n->get_sub()) + { + stack.push(&child.second); + } + } + } + while(!stack.empty()); +} + +/*******************************************************************\ + +Function: get_delta_view + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT(void)::get_delta_view( + const self_type &other, + delta_viewt &delta_view, + const bool only_common) const +{ + assert(delta_view.empty()); + + typedef std::pair stack_itemt; + std::stack stack; + + if(empty()) + return; + + if(other.empty()) + { + if(!only_common) + { + gather_all(map, delta_view); + } + return; + } + + stack.push(stack_itemt(&map, &other.map)); + + do + { + const stack_itemt si=stack.top(); + stack.pop(); + + const node_type *n1=si.first; + const node_type *n2=si.second; + + if(n1->is_internal()) + { + _sn_assert(n2->is_internal()); + + for(const auto &child : n1->get_sub()) + { + const node_type *p; + + p=n2->find_child(child.first); + if(p==nullptr) + { + if(!only_common) + { + gather_all(child.second, delta_view); + } + } + else if(!child.second.shares_with(*p)) + { + stack.push(stack_itemt(&child.second, p)); + } + } + } + else if(n1->is_container()) + { + _sn_assert(n2->is_container()); + + for(const auto &l1 : n1->get_container()) + { + const key_type &k1=l1.get_key(); + bool found=false; + + for(const auto &l2 : n2->get_container()) + { + const key_type &k2=l2.get_key(); + + if(l1.shares_with(l2)) + { + found=true; + break; + } + + if(key_equal()(k1, k2)) + { + delta_view.push_back( + delta_view_itemt( + true, + k1, + l1.get_value(), + l2.get_value())); + + found=true; + break; + } + } + + if(!only_common && !found) + { + delta_view.push_back( + delta_view_itemt( + false, + l1.get_key(), + l1.get_value(), + dummy)); + } + } + } + else + { + assert(false); + } + } + while(!stack.empty()); +} + +/*******************************************************************\ + +Function: get_container_node + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, node_type *)::get_container_node(const key_type &k) +{ + size_t key=hash()(k); + node_type *p=↦ + + for(unsigned i=0; i>=chunk; + + p=p->add_child(bit); + } + + return p; +} + +/*******************************************************************\ + +Function: get_container_node + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(const, node_type *)::get_container_node(const key_type &k) const +{ + size_t key=hash()(k); + const node_type *p=↦ + + for(unsigned i=0; i>=chunk; + + p=p->find_child(bit); + if(p==nullptr) + return nullptr; + } + + assert(p->is_container()); + + return p; +} + +/*******************************************************************\ + +Function: get_leaf_node + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(const, node_type *)::get_leaf_node(const key_type &k) const +{ + const node_type *p=get_container_node(k); + if(p==nullptr) + return nullptr; + + p=p->find_leaf(k); + + return p; +} + +/*******************************************************************\ + +Function: erase + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, size_type)::erase( + const key_type &k, + const tvt &key_exists) +{ + assert(!key_exists.is_false()); + + // check if key exists + if(key_exists.is_unknown() && !has_key(k)) + return 0; + + node_type *del=nullptr; + unsigned del_bit; + + size_t key=hash()(k); + node_type *p=↦ + + for(unsigned i=0; i>=chunk; + + const subt &sub=as_const(p)->get_sub(); + if(sub.size()>1 || del==nullptr) + { + del=p; + del_bit=bit; + } + + p=p->add_child(bit); + } + + _sm_assert(p->is_container()); + + { + const containert &c=as_const(p)->get_container(); + + if(c.size()==1) + { + del->remove_child(del_bit); + num--; + return 1; + } + } + + containert &c=p->get_container(); + _sm_assert(c.size()>1); + p->remove_leaf(k); + num--; + + return 1; +} + +/*******************************************************************\ + +Function: erase_all + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, size_type)::erase_all( + const keyst &ks, + const tvt &key_exists) +{ + size_type cnt=0; + + for(const key_type &k : ks) + { + cnt+=erase(k, key_exists); + } + + return cnt; +} + +/*******************************************************************\ + +Function: insert + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, const_find_type)::insert( + const key_type &k, + const mapped_type &m, + const tvt &key_exists) +{ + _sn_assert(!key_exists.is_true()); + + if(key_exists.is_unknown()) + { + const node_type *p=as_const(this)->get_leaf_node(k); + if(p!=nullptr) + return const_find_type(p->get_value(), false); + } + + node_type *p=get_container_node(k); + _sn_assert(p!=nullptr); + + p=p->place_leaf(k, m); + num++; + + return const_find_type(as_const(p)->get_value(), true); +} + +/*******************************************************************\ + +Function: insert + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, const_find_type)::insert( + const value_type &p, + const tvt &key_exists) +{ + return insert(p.first, p.second, key_exists); +} + +/*******************************************************************\ + +Function: place + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, find_type)::place( + const key_type &k, + const mapped_type &m) +{ + node_type *c=get_container_node(k); + _sm_assert(c!=nullptr); + + node_type *p=c->find_leaf(k); + + if(p!=nullptr) + return find_type(p->get_value(), false); + + p=c->place_leaf(k, m); + num++; + + return find_type(p->get_value(), true); +} + +/*******************************************************************\ + +Function: place + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, find_type)::place( + const value_type &p) +{ + return place(p.first, p.second); +} + +/*******************************************************************\ + +Function: find + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, find_type)::find( + const key_type &k, + const tvt &key_exists) +{ + _sm_assert(!key_exists.is_false()); + + if(key_exists.is_unknown() && !has_key(k)) + return find_type(dummy, false); + + node_type *p=get_container_node(k); + _sm_assert(p!=nullptr); + + p=p->find_leaf(k); + _sm_assert(p!=nullptr); + + return find_type(p->get_value(), true); + +} + +/*******************************************************************\ + +Function: find + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, const_find_type)::find(const key_type &k) const +{ + const node_type *p=get_leaf_node(k); + + if(p==nullptr) + return const_find_type(dummy, false); + + return const_find_type(p->get_value(), true); +} + +/*******************************************************************\ + +Function: at + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, mapped_type &)::at( + const key_type &k, + const tvt &key_exists) +{ + find_type r=find(k, key_exists); + + if(!r.second) + throw std::out_of_range(not_found_msg); + + return r.first; +} + +/*******************************************************************\ + +Function: at + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(const, mapped_type &)::at(const key_type &k) const +{ + const_find_type r=find(k); + if(!r.second) + throw std::out_of_range(not_found_msg); + + return r.first; +} + +/*******************************************************************\ + +Function: operator[] + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +SHARING_MAPT2(, mapped_type &)::operator[](const key_type &k) +{ + return place(k, mapped_type()).first; +} + +// static constants + +SHARING_MAPT(const std::string)::not_found_msg="key not found"; + +// config +SHARING_MAPT(const size_t)::bits=18; +SHARING_MAPT(const size_t)::chunk=3; + +// derived config +SHARING_MAPT(const size_t)::mask=0xffff>>(16-chunk); +SHARING_MAPT(const size_t)::steps=bits/chunk; + +SHARING_MAPT2(, mapped_type)::dummy; + +#endif diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h new file mode 100644 index 00000000000..1e3d29a413e --- /dev/null +++ b/src/util/sharing_node.h @@ -0,0 +1,346 @@ +/*******************************************************************\ + +Module: Sharing node + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_SHARING_NODE_H +#define CPROVER_UTIL_SHARING_NODE_H + +#include +#include +#include +#include + +#define _sn_assert(b) assert(b) +//#define _sn_assert(b) + +template +const T *as_const(T *t) +{ + return t; +} + +template < + class keyT, + class valueT, + class predT=std::equal_to, + bool no_sharing=false> +class sharing_nodet +{ +public: + friend void sharing_node_test(); + + typedef keyT key_type; + typedef valueT mapped_type; + + typedef predT key_equal; + + typedef sharing_nodet self_type; + + typedef std::map subt; + typedef std::list containert; + + typedef const std::pair const_find_type; + typedef const std::pair find_type; + + sharing_nodet() : data(empty_data) + { + _sn_assert(data.use_count()>=2); + } + + sharing_nodet(const key_type &k, const mapped_type &m) : data(empty_data) + { + _sn_assert(data.use_count()>=2); + + dt &d=write(); + + _sn_assert(d.k==nullptr); + d.k=std::make_shared(k); + + _sn_assert(d.m==nullptr); + d.m.reset(new mapped_type(m)); + } + + sharing_nodet(const self_type &other) + { +#ifdef SM_NO_SHARING + data=std::make_shared
(*other.data); +#else + if(no_sharing) + { + data=std::make_shared
(*other.data); + } + else + { + data=other.data; + } +#endif + } + + // check type of node + + bool is_empty() const + { + _sn_assert(is_well_formed()); + return data==empty_data; + } + + bool is_internal() const + { + _sn_assert(is_well_formed()); + _sn_assert(!is_empty()); + return !get_sub().empty(); + } + + bool is_container() const + { + _sn_assert(is_well_formed()); + _sn_assert(!is_empty()); + return !get_container().empty(); + } + + bool is_leaf() const + { + _sn_assert(is_well_formed()); + _sn_assert(!is_empty()); + return read().is_leaf(); + } + + // accessors + + const key_type &get_key() const + { + _sn_assert(is_leaf()); + return *read().k; + } + + const mapped_type &get_value() const + { + _sn_assert(is_leaf()); + return *read().m; + } + + mapped_type &get_value() + { + _sn_assert(is_leaf()); + return *write().m; + } + + subt &get_sub() + { + return write().sub; + } + + const subt &get_sub() const + { + return read().sub; + } + + containert &get_container() + { + return write().con; + } + + const containert &get_container() const + { + return read().con; + } + + // internal nodes + + const self_type *find_child(const unsigned n) const + { + const subt &s=get_sub(); + typename subt::const_iterator it=s.find(n); + + if(it!=s.end()) + return &it->second; + + return nullptr; + } + + self_type *add_child(const unsigned n) + { + subt &s=get_sub(); + return &s[n]; + } + + void remove_child(const unsigned n) + { + subt &s=get_sub(); + size_t r=s.erase(n); + + _sn_assert(r==1); + } + + // container nodes + + const self_type *find_leaf(const key_type &k) const + { + const containert &c=get_container(); + + for(const auto &n : c) + { + if(key_equal()(n.get_key(), k)) + return &n; + } + + return nullptr; + } + + self_type *find_leaf(const key_type &k) + { + containert &c=get_container(); + + for(auto &n : c) + { + if(key_equal()(n.get_key(), k)) + return &n; + } + + return nullptr; + } + + // add leaf, key must not exist yet + self_type *place_leaf(const key_type &k, const mapped_type &m) + { + _sn_assert(as_const(this)->find_leaf(k)==nullptr); + + containert &c=get_container(); + c.push_back(self_type(k, m)); + + return &c.back(); + } + + // remove leaf, key must exist + void remove_leaf(const key_type &k) + { + containert &c=get_container(); + + for(typename containert::const_iterator it=c.begin(); + it!=c.end(); it++) + { + const self_type &n=*it; + + if(key_equal()(n.get_key(), k)) + { + c.erase(it); + return; + } + } + + assert(false); + } + + // misc + + void clear() + { + *this=self_type(); + } + + bool shares_with(const self_type &other) const + { + return data==other.data; + } + + void swap(self_type &other) + { + data.swap(other.data); + } + +protected: + class dt + { + public: + dt() {} + + dt(const dt &d) : k(d.k), sub(d.sub), con(d.con) + { + if(d.is_leaf()) + { + _sn_assert(m==nullptr); + m.reset(new mapped_type(*d.m)); + } + } + + bool is_leaf() const + { + _sn_assert(k==nullptr || m!=nullptr); + return k!=nullptr; + } + + std::shared_ptr k; + std::unique_ptr m; + + subt sub; + containert con; + }; + + const dt &read() const + { + return *data; + } + + dt &write() + { + detach(); + return *data; + } + + void detach() + { + _sn_assert(data.use_count()>0); + + if(data==empty_data) + data=std::make_shared
(); + else if(data.use_count()>1) + data=std::make_shared
(*data); + + _sn_assert(data.use_count()==1); + } + + bool is_well_formed() const + { + if(data==nullptr) + return false; + + const dt &d=*data; + + bool b; + + // empty node + b=data==empty_data; + // internal node + b|=d.k==nullptr && d.m==nullptr && get_container().empty() && + !get_sub().empty(); + // container node + b|=d.k==nullptr && d.m==nullptr && !get_container().empty() && + get_sub().empty(); + // leaf node + b|=d.k!=nullptr && d.m!=nullptr && get_container().empty() && + get_sub().empty(); + + return b; + } + + std::shared_ptr
data; + static std::shared_ptr
empty_data; + + // dummy node returned when node was not found + static sharing_nodet dummy; +}; + +template +std::shared_ptr::dt> + sharing_nodet::empty_data( + new sharing_nodet::dt()); + +template +sharing_nodet + sharing_nodet::dummy; + +#endif diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 31ca2171549..837138258d0 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -32,8 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "endianness_map.h" #include "simplify_utils.h" -#include - // #define DEBUGX #ifdef DEBUGX @@ -277,8 +275,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal); inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); - inequality.rhs()= - zero_initializer(expr.op0().type(), expr.source_location(), ns); + inequality.rhs()=from_integer(0, op_type); assert(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.swap(inequality); @@ -294,8 +291,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal); inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); - inequality.rhs()= - zero_initializer(expr.op0().type(), expr.source_location(), ns); + inequality.rhs()=from_integer(0, op_type); assert(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.op0()=inequality; diff --git a/unit/Makefile b/unit/Makefile index 0b442445a0f..007ebd3c70d 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,6 +1,8 @@ SRC = cpp_parser.cpp cpp_scanner.cpp elf_reader.cpp float_utils.cpp \ ieee_float.cpp json.cpp miniBDD.cpp osx_fat_reader.cpp \ - smt2_parser.cpp wp.cpp string_utils.cpp + smt2_parser.cpp wp.cpp string_utils.cpp \ + sharing_map.cpp \ + sharing_node.cpp INCLUDES= -I ../src/ @@ -59,3 +61,9 @@ wp$(EXEEXT): wp$(OBJEXT) string_utils$(EXEEXT): string_utils$(OBJEXT) $(LINKBIN) +sharing_map$(EXEEXT): sharing_map$(OBJEXT) + $(LINKBIN) + +sharing_node$(EXEEXT): sharing_node$(OBJEXT) + $(LINKBIN) + diff --git a/unit/sharing_map.cpp b/unit/sharing_map.cpp new file mode 100644 index 00000000000..9911f460855 --- /dev/null +++ b/unit/sharing_map.cpp @@ -0,0 +1,336 @@ +#include +#include + +#include + +typedef sharing_mapt smt; + +// helpers +void fill(smt &sm) +{ + sm.insert("i", "0"); + sm.insert("j", "1"); + sm.insert("k", "2"); +} + +void fill2(smt &sm) +{ + sm.insert("l", "3"); + sm.insert("m", "4"); + sm.insert("n", "5"); +} + +// tests + +void sharing_map_interface_test() +{ + std::cout << "Running interface test" << std::endl; + + // empty map + { + smt sm; + + assert(sm.empty()); + assert(sm.size()==0); + assert(!sm.has_key("i")); + } + + // insert elements + { + smt sm; + + smt::const_find_type r1=sm.insert(std::make_pair("i", "0")); + assert(r1.second); + + smt::const_find_type r2=sm.insert("j", "1"); + assert(r2.second); + + smt::const_find_type r3=sm.insert(std::make_pair("i", "0")); + assert(!r3.second); + + assert(sm.size()==2); + assert(!sm.empty()); + } + + // place elements + { + smt sm1; + smt sm2(sm1); + + smt::find_type r1=sm1.place("i", "0"); + assert(r1.second); + assert(!sm2.has_key("i")); + + std::string &s1=r1.first; + s1="1"; + + assert(sm1.at("i")=="1"); + } + + // retrieve elements + { + smt sm; + sm.insert("i", "0"); + sm.insert("j", "1"); + + const smt &sm2=sm; + + std::string s; + s=sm2.at("i"); + assert(s=="0"); + + try { + sm2.at("k"); + assert(false); + } catch (...) {} + + s=sm2.at("j"); + assert(s=="1"); + + assert(sm.has_key("i")); + assert(sm.has_key("j")); + assert(!sm.has_key("k")); + + std::string &s2=sm.at("i"); + s2="3"; + assert(sm2.at("i")=="3"); + + assert(sm.size()==2); + + smt::find_type r=sm.find("i"); + assert(r.second); + r.first="4"; + assert(sm2.at("i")=="4"); + + smt::const_find_type rc=sm2.find("k"); + assert(!rc.second); + } + + // remove elements + { + smt sm; + sm.insert("i", "0"); + sm.insert("j", "1"); + + assert(sm.erase("k")==0); + assert(sm.size()==2); + + assert(sm.erase("i")==1); + assert(!sm.has_key("i")); + + assert(sm.erase("j")==1); + assert(!sm.has_key("j")); + + sm.insert("i", "0"); + sm.insert("j", "1"); + + smt sm3(sm); + + assert(sm.has_key("i")); + assert(sm.has_key("j")); + assert(sm3.has_key("i")); + assert(sm3.has_key("j")); + + sm.erase("i"); + + assert(!sm.has_key("i")); + assert(sm.has_key("j")); + + assert(sm3.has_key("i")); + assert(sm3.has_key("j")); + + sm3.erase("i"); + assert(!sm3.has_key("i")); + } + + // operator[] + { + smt sm; + + sm["i"]; + assert(sm.has_key("i")); + + sm["i"]="0"; + assert(sm.at("i")=="0"); + + sm["j"]="1"; + assert(sm.at("j")=="1"); + } +} + +void sharing_map_copy_test() +{ + std::cout << "Running copy test" << std::endl; + + smt sm1; + const smt &sm2=sm1; + + fill(sm1); + + assert(sm2.find("i").first=="0"); + assert(sm2.find("j").first=="1"); + assert(sm2.find("k").first=="2"); + + smt sm3=sm1; + const smt &sm4=sm3; + + assert(sm3.erase("l")==0); + assert(sm3.erase("i")==1); + + assert(!sm4.has_key("i")); + sm3.place("i", "3"); + assert(sm4.find("i").first=="3"); +} + +class some_keyt +{ +public: + some_keyt(size_t s) : s(s) + { + } + + size_t s; + + bool operator==(const some_keyt &other) const + { + return s==other.s; + } +}; + +class some_key_hash +{ +public: + size_t operator()(const some_keyt &k) const + { + return k.s & 0x3; + } +}; + +void sharing_map_collision_test() +{ + std::cout << "Running collision test" << std::endl; + + typedef sharing_mapt smt; + + smt sm; + + sm.insert(0, "a"); + sm.insert(8, "b"); + sm.insert(16, "c"); + + sm.insert(1, "d"); + sm.insert(2, "e"); + + sm.erase(8); + + assert(sm.has_key(0)); + assert(sm.has_key(16)); + + assert(sm.has_key(1)); + assert(sm.has_key(2)); + + assert(!sm.has_key(8)); +} + +void sharing_map_view_test() +{ + std::cout << "Running view test" << std::endl; + + // view test + { + smt sm; + + fill(sm); + + smt::viewt view; + sm.get_view(view); + + assert(view.size()==3); + } + + // delta view test (no sharing, same keys) + { + smt sm1; + fill(sm1); + + smt sm2; + fill(sm2); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + assert(delta_view.size()==3); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + assert(delta_view.size()==3); + } + + // delta view test (all shared, same keys) + { + smt sm1; + fill(sm1); + + smt sm2(sm1); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + assert(delta_view.size()==0); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + assert(delta_view.size()==0); + } + + // delta view test (some sharing, same keys) + { + smt sm1; + fill(sm1); + + smt sm2(sm1); + auto r=sm2.find("i"); + assert(r.second); + r.first="3"; + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + assert(delta_view.size()>0); // not everything is shared + assert(delta_view.size()<3); // there is some sharing + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + assert(delta_view.size()>0); // not everything is shared + assert(delta_view.size()<3); // there is some sharing + } + + // delta view test (no sharing, different keys) + { + smt sm1; + fill(sm1); + + smt sm2; + fill2(sm2); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + assert(delta_view.size()==0); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + assert(delta_view.size()==3); + } +} + +int main() +{ + sharing_map_interface_test(); + sharing_map_copy_test(); + sharing_map_collision_test(); + sharing_map_view_test(); + + return 0; +} + diff --git a/unit/sharing_node.cpp b/unit/sharing_node.cpp new file mode 100644 index 00000000000..2d256b8dd45 --- /dev/null +++ b/unit/sharing_node.cpp @@ -0,0 +1,129 @@ +#include +#include + +#include + +void sharing_node_test() +{ + std::cout << "Running sharing node test" << std::endl; + + typedef sharing_nodet snt; + + // internal node test + { + snt sn1; + const snt &sn2=sn1; + + const snt *p2; + + assert(sn1.is_empty()); + + sn1.add_child(0); + sn1.add_child(1); + sn1.add_child(2); + + assert(!sn2.is_empty()); + assert(sn2.is_internal()); + assert(!sn2.is_container()); + assert(!sn2.is_leaf()); + + assert(sn2.get_sub().size()==3); + + p2=sn2.find_child(0); + assert(p2!=nullptr); + + p2=sn1.find_child(0); + assert(p2!=nullptr); + + p2=sn2.find_child(3); + assert(p2==nullptr); + + p2=sn1.find_child(3); + assert(p2==nullptr); + + sn1.remove_child(0); + assert(sn2.get_sub().size()==2); + + sn1.clear(); + assert(sn2.is_empty()); + } + + // container node test + { + snt sn1; + + snt *p1; + const snt *p2; + + sn1.add_child(0); + sn1.add_child(1); + + p1=sn1.add_child(2); + p2=p1; + + assert(p1->find_leaf("a")==nullptr); + assert(p2->find_leaf("a")==nullptr); + + p1->place_leaf("a", "b"); + assert(p2->get_container().size()==1); + p1->place_leaf("c", "d"); + assert(p2->get_container().size()==2); + + assert(p2->is_container()); + + p1->remove_leaf("a"); + assert(p2->get_container().size()==1); + } + + // copy test 1 + { + snt sn1; + snt sn2; + + sn2=sn1; + assert(sn1.data.use_count()==3); + assert(sn2.data.use_count()==3); + + sn1.add_child(0); + assert(sn1.data.use_count()==1); + // the newly created node is empty as well + assert(sn2.data.use_count()==3); + + sn2=sn1; + assert(sn2.data.use_count()==2); + } + + // copy test 2 + { + snt sn1; + const snt &sn1c=sn1; + snt *p; + + p=sn1.add_child(0); + p->place_leaf("x", "y"); + + p=sn1.add_child(1); + p->place_leaf("a", "b"); + p->place_leaf("c", "d"); + + snt sn2; + const snt &sn2c=sn2; + sn2=sn1; + + assert(sn1.is_internal()); + assert(sn2.is_internal()); + + sn1.remove_child(0); + assert(sn1c.get_sub().size()==1); + + assert(sn2c.get_sub().size()==2); + } +} + +int main() +{ + sharing_node_test(); + + return 0; +} +