diff --git a/.travis.yml b/.travis.yml index 82ce565d776..324ee8e837b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,22 +1,43 @@ language: cpp -os: - - linux - - osx sudo: required +matrix: + include: + - os: linux + dist: trusty + compiler: clang + addons: + apt: + sources: + - ubuntu-toolchain-r-test + packages: + # newer g++ version (also pulls libstdc++) + - g++-4.9 + - libwww-perl + - os: linux + dist: trusty + compiler: gcc + addons: + apt: + sources: + - ubuntu-toolchain-r-test + packages: + # newer g++ version (also pulls libstdc++) + - g++-4.9 + - libwww-perl + before_install: + - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.9 90 + - os: osx + compiler: clang + - os: osx + compiler: gcc + addons: apt: packages: - libwww-perl -compiler: - - gcc - - clang - -before_install: - - if [ "$(expr substr $(uname -s) 1 5)" == "Linux" ] ; then sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test && sudo apt-get -qq update && sudo apt-get -qq install g++-4.8 gcc-4.8 && sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 90 && sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 90 ; fi - install: - chmod a+x regression/failed-tests-printer.pl - cd src && make minisat2-download diff --git a/regression/Makefile b/regression/Makefile index de8c70edd3c..2ebcb257207 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -1,4 +1,4 @@ -DIRS = ansi-c cbmc cpp goto-instrument +DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) diff --git a/regression/goto-instrument-unwind/Makefile b/regression/goto-instrument-unwind/Makefile index 8346f07d4d1..5af34f6d089 100644 --- a/regression/goto-instrument-unwind/Makefile +++ b/regression/goto-instrument-unwind/Makefile @@ -21,9 +21,10 @@ tests.log: ../test.pl clean: @for dir in *; do \ if [ -d "$$dir" ]; then \ - rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \ + rm -f $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \ fi; \ - done; + done; + rm -f tests.log show: @for dir in *; do \ diff --git a/regression/goto-instrument-unwind/assert1/main.c b/regression/goto-instrument-unwind/assert1/main.c new file mode 100644 index 00000000000..efff5eb8ba0 --- /dev/null +++ b/regression/goto-instrument-unwind/assert1/main.c @@ -0,0 +1,6 @@ + +int main() +{ + int i; + for(i = 0; i < 10; i++) {} +} diff --git a/regression/goto-instrument-unwind/assert1/test.desc b/regression/goto-instrument-unwind/assert1/test.desc new file mode 100644 index 00000000000..e328d96c8d8 --- /dev/null +++ b/regression/goto-instrument-unwind/assert1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--unwind 10 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-unwind/assert2/main.c b/regression/goto-instrument-unwind/assert2/main.c new file mode 100644 index 00000000000..efff5eb8ba0 --- /dev/null +++ b/regression/goto-instrument-unwind/assert2/main.c @@ -0,0 +1,6 @@ + +int main() +{ + int i; + for(i = 0; i < 10; i++) {} +} diff --git a/regression/goto-instrument-unwind/assert2/test.desc b/regression/goto-instrument-unwind/assert2/test.desc new file mode 100644 index 00000000000..1c4d4739f3a --- /dev/null +++ b/regression/goto-instrument-unwind/assert2/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 9 --unwinding-assertions +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-unwind/assert3/main.c b/regression/goto-instrument-unwind/assert3/main.c new file mode 100644 index 00000000000..8f04d60e6ac --- /dev/null +++ b/regression/goto-instrument-unwind/assert3/main.c @@ -0,0 +1,9 @@ + +int main() +{ + int i; + i = 0; + do { + i++; + } while(i < 10); +} diff --git a/regression/goto-instrument-unwind/assert3/test.desc b/regression/goto-instrument-unwind/assert3/test.desc new file mode 100644 index 00000000000..e328d96c8d8 --- /dev/null +++ b/regression/goto-instrument-unwind/assert3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--unwind 10 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-unwind/assume1/main.c b/regression/goto-instrument-unwind/assume1/main.c new file mode 100644 index 00000000000..0987b00a37a --- /dev/null +++ b/regression/goto-instrument-unwind/assume1/main.c @@ -0,0 +1,7 @@ + +int main() +{ + int i; + for(i = 0; i < 10; i++) {} + assert(0); +} diff --git a/regression/goto-instrument-unwind/assume1/test.desc b/regression/goto-instrument-unwind/assume1/test.desc new file mode 100644 index 00000000000..178d0f4fbd6 --- /dev/null +++ b/regression/goto-instrument-unwind/assume1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 10 +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-unwind/assume2/main.c b/regression/goto-instrument-unwind/assume2/main.c new file mode 100644 index 00000000000..0987b00a37a --- /dev/null +++ b/regression/goto-instrument-unwind/assume2/main.c @@ -0,0 +1,7 @@ + +int main() +{ + int i; + for(i = 0; i < 10; i++) {} + assert(0); +} diff --git a/regression/goto-instrument-unwind/assume2/test.desc b/regression/goto-instrument-unwind/assume2/test.desc new file mode 100644 index 00000000000..d8bb57ee3c2 --- /dev/null +++ b/regression/goto-instrument-unwind/assume2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--unwind 9 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/goto-instrument-unwind/break-loop1/test.desc b/regression/goto-instrument-unwind/break-loop1/test.desc index 6d9a8177c73..b6b7cbeb857 100644 --- a/regression/goto-instrument-unwind/break-loop1/test.desc +++ b/regression/goto-instrument-unwind/break-loop1/test.desc @@ -1,6 +1,7 @@ CORE main.c -10 +--unwind 10 --partial-loops +^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/goto-instrument-unwind/break-loop2/test.desc b/regression/goto-instrument-unwind/break-loop2/test.desc index 7639d204406..93131a64724 100644 --- a/regression/goto-instrument-unwind/break-loop2/test.desc +++ b/regression/goto-instrument-unwind/break-loop2/test.desc @@ -1,6 +1,7 @@ CORE main.c -100 +--unwind 100 --partial-loops +^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/goto-instrument-unwind/continue-as-loops1/main.c b/regression/goto-instrument-unwind/continue-as-loops1/main.c new file mode 100644 index 00000000000..1777ed02b4d --- /dev/null +++ b/regression/goto-instrument-unwind/continue-as-loops1/main.c @@ -0,0 +1,7 @@ + +int main() +{ + int i; + for(i = 0; i < 10; i++) {} + assert(i==10); +} diff --git a/regression/goto-instrument-unwind/continue-as-loops1/test.desc b/regression/goto-instrument-unwind/continue-as-loops1/test.desc new file mode 100644 index 00000000000..7f4b4a94a08 --- /dev/null +++ b/regression/goto-instrument-unwind/continue-as-loops1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--unwind 5 --continue-as-loops +^Unwinding loop.*iteration 5 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^Unwinding loop.*iteration 6 diff --git a/regression/goto-instrument-unwind/continue-loop1/test.desc b/regression/goto-instrument-unwind/continue-loop1/test.desc index 6d9a8177c73..b6b7cbeb857 100644 --- a/regression/goto-instrument-unwind/continue-loop1/test.desc +++ b/regression/goto-instrument-unwind/continue-loop1/test.desc @@ -1,6 +1,7 @@ CORE main.c -10 +--unwind 10 --partial-loops +^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/goto-instrument-unwind/continue-loop2/test.desc b/regression/goto-instrument-unwind/continue-loop2/test.desc index 7639d204406..93131a64724 100644 --- a/regression/goto-instrument-unwind/continue-loop2/test.desc +++ b/regression/goto-instrument-unwind/continue-loop2/test.desc @@ -1,6 +1,7 @@ CORE main.c -100 +--unwind 100 --partial-loops +^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/goto-instrument-unwind/do-while-loop1/main.c b/regression/goto-instrument-unwind/do-while-loop1/main.c new file mode 100644 index 00000000000..2e68c337cbd --- /dev/null +++ b/regression/goto-instrument-unwind/do-while-loop1/main.c @@ -0,0 +1,27 @@ + +void f() {} + +int main() +{ + /** + * This is a test case for the unwind operation of goto-instrument; + * every loop will be unwound K times + **/ + const unsigned K=10; + + const unsigned n=100; + unsigned c=0, i; + + i=1; + do + { + f(); + c++; + i++; + } while(i<=n); + + unsigned eva=n; + if(K1) + throw "more than one of --unwinding-assertions,--partial-loops," + "--continue-as-loops selected"; + + goto_unwindt::unwind_strategyt unwind_strategy=goto_unwindt::ASSUME; + + if(unwinding_assertions) + { + unwind_strategy=goto_unwindt::ASSERT; + } + else if(partial_loops) + { + unwind_strategy=goto_unwindt::PARTIAL; + } + else if(continue_as_loops) + { + unwind_strategy=goto_unwindt::CONTINUE; + } + + goto_unwindt goto_unwind; + goto_unwind(goto_functions, unwind_set, k, unwind_strategy); + + goto_functions.update(); + goto_functions.compute_loop_numbers(); + + if(cmdline.isset("log")) + { + std::string filename=cmdline.get_value("log"); + bool have_file=!filename.empty() && filename!="-"; + + jsont result=goto_unwind.output_log_json(); + + if(have_file) + { +#ifdef _MSC_VER + std::ofstream of(widen(filename)); +#else + std::ofstream of(filename); +#endif + if(!of) + throw "failed to open file "+filename; + + of << result; + of.close(); + } + else + { + std::cout << result << std::endl; + } + } + } } if(cmdline.isset("show-value-sets")) @@ -1324,6 +1407,11 @@ void goto_instrument_parse_optionst::help() "Semantic transformations:\n" " --nondet-volatile makes reads from volatile variables non-deterministic\n" " --unwind unwinds the loops times\n" + " --unwindset L:B,... unwind loop L with a bound of B\n" + " --unwindset-file read unwindset from file\n" + " --partial-loops permit paths with partial loops\n" + " --unwinding-assertions generate unwinding assertions\n" + " --continue-as-loops add loop for remaining iterations after unwound part\n" " --isr instruments an interrupt service routine\n" " --mmio instruments memory-mapped I/O\n" " --nondet-static add nondeterministic initialization of variables with static lifetime\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1123a1ec6e9..d778cffabe5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -31,7 +31,10 @@ Author: Daniel Kroening, kroening@kroening.com "(nan-check)(no-nan-check)" \ "(race-check)(scc)(one-event-per-cycle)" \ "(minimum-interference)" \ - "(mm):(my-events)(unwind):" \ + "(mm):(my-events)" \ + "(unwind):(unwindset):(unwindset-file):" \ + "(unwinding-assertions)(partial-loops)(continue-as-loops)" \ + "(log):" \ "(max-var):(max-po-trans):(ignore-arrays)" \ "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ "(call-graph)" \ diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index a2f7d7d0d7c..0d62bd4a95d 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -77,7 +77,9 @@ void k_inductiont::process_loop( if(base_case) { // now unwind k times - unwind(goto_function.body, loop_head, loop_exit, k); + goto_unwindt goto_unwind; + goto_unwind.unwind(goto_function.body, loop_head, loop_exit, k, + goto_unwindt::PARTIAL); // assume the loop condition has become false goto_programt::instructiont assume(ASSUME); @@ -99,7 +101,10 @@ void k_inductiont::process_loop( // unwind to get k+1 copies std::vector iteration_points; - unwind(goto_function.body, loop_head, loop_exit, k+1, iteration_points); + + goto_unwindt goto_unwind; + goto_unwind.unwind(goto_function.body, loop_head, loop_exit, k+1, + goto_unwindt::PARTIAL, iteration_points); // we can remove everything up to the first assertion for(goto_programt::targett t=loop_head; t!=loop_exit; t++) diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 3a9e44e4a17..6d33bbe3a11 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -1,18 +1,133 @@ /*******************************************************************\ -Module: loop unwinding +Module: Loop unwinding Author: Daniel Kroening, kroening@kroening.com + Daniel Poetzl \*******************************************************************/ #include +#include #include + #include "unwind.h" #include "loop_utils.h" /*******************************************************************\ +Function: parse_unwindset + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void parse_unwindset(const std::string &us, unwind_sett &unwind_set) +{ + assert(unwind_set.empty()); + + std::vector result; + split_string(us, ',', result, true, true); + assert(!result.empty()); + + if(result.front().empty()) // allow empty string as unwindset + return; + + for(std::vector::const_iterator it=result.begin(); + it!=result.end(); it++) + { + std::string loop; + std::string bound; + + split_string(*it, ':', loop, bound, true); + + std::string func; + std::string id; + + split_string(loop, '.', func, id, true); + + unsigned loop_id=std::stoi(id); + int loop_bound=std::stoi(bound); + + if(loop_bound<-1) + throw "given unwind bound < -1"; + + unwind_set[func][loop_id]=loop_bound; + } +} + +/*******************************************************************\ + +Function: copy_segment + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_unwindt::copy_segment( + const goto_programt::const_targett start, + const goto_programt::const_targett end, // exclusive + goto_programt &goto_program) // result +{ + assert(start->location_numberlocation_number); + assert(goto_program.empty()); + + // build map for branch targets inside the loop + typedef std::map target_mapt; + target_mapt target_map; + + unsigned i=0; + + for(goto_programt::const_targett t=start; t!=end; t++, i++) + target_map[t]=i; + + // make a copy + std::vector target_vector; + target_vector.reserve(target_map.size()); + assert(target_vector.empty()); + + for(goto_programt::const_targett t=start; t!=end; t++) + { + goto_programt::targett t_new=goto_program.add_instruction(); + *t_new=*t; + unwind_log.insert(t_new, t->location_number); + target_vector.push_back(t_new); // store copied instruction + } + + assert(goto_program.instructions.size()==target_vector.size()); + + // adjust intra-segment gotos + for(std::size_t i=0; iis_goto()) + continue; + + goto_programt::const_targett tgt=t->get_target(); + + target_mapt::const_iterator m_it=target_map.find(tgt); + + if(m_it!=target_map.end()) + { + unsigned j=m_it->second; + + assert(jset_target(target_vector[j]); + } + } +} + +/*******************************************************************\ + Function: unwind Inputs: @@ -23,14 +138,16 @@ Function: unwind \*******************************************************************/ -void unwind( +void goto_unwindt::unwind( goto_programt &goto_program, - goto_programt::targett loop_head, - goto_programt::targett loop_exit, - const unsigned k) + const goto_programt::const_targett loop_head, + const goto_programt::const_targett loop_exit, + const unsigned k, + const unwind_strategyt unwind_strategy) { - std::vector exit_points; - unwind(goto_program, loop_head, loop_exit, k, exit_points); + std::vector iteration_points; + unwind(goto_program, loop_head, loop_exit, k, unwind_strategy, + iteration_points); } /*******************************************************************\ @@ -45,136 +162,260 @@ Function: unwind \*******************************************************************/ -void unwind( +void goto_unwindt::unwind( goto_programt &goto_program, - goto_programt::targett loop_head, - goto_programt::targett loop_exit, + const goto_programt::const_targett loop_head, + const goto_programt::const_targett loop_exit, const unsigned k, + const unwind_strategyt unwind_strategy, std::vector &iteration_points) { - assert(k!=0); - - iteration_points.resize(k); + assert(iteration_points.empty()); + assert(loop_head->location_numberlocation_number); - // loop_exit: where to go after the loop ends - // loop_iter: where to go for the next iteration + // rest program after unwound part + goto_programt rest_program; - // Add a 'goto' and a 'skip' _before_ loop_exit. - // The goto is to take care of 'fall-out' loop exit, and is - // not needed if there is an unconditional goto before loop_exit. + if(unwind_strategy==PARTIAL) + { + goto_programt::targett t=rest_program.add_instruction(); + unwind_log.insert(t, loop_head->location_number); - if(loop_exit!=goto_program.instructions.begin()) + t->make_skip(); + t->source_location=loop_head->source_location; + t->function=loop_head->function; + t->location_number=loop_head->location_number; + } + else if(unwind_strategy==CONTINUE) { - goto_programt::targett t_before=loop_exit; - t_before--; + copy_segment(loop_head, loop_exit, rest_program); + } + else + { + goto_programt::const_targett t=loop_exit; + t--; + assert(t->is_backwards_goto()); - if(t_before->is_goto() && t_before->guard.is_true()) + exprt exit_cond; + exit_cond.make_false(); // default is false + + if(!t->guard.is_true()) // cond in backedge + { + exit_cond=t->guard; + exit_cond.make_not(); + } + else if(loop_head->is_goto()) { - // no 'fall-out' + if(loop_head->get_target()==loop_exit) // cond in forward edge + exit_cond=loop_head->guard; } + + goto_programt::targett new_t=rest_program.add_instruction(); + + if(unwind_strategy==ASSERT) + new_t->make_assertion(exit_cond); + else if(unwind_strategy==ASSUME) + new_t->make_assumption(exit_cond); else + assert(false); + + new_t->source_location=loop_head->source_location; + new_t->function=loop_head->function; + new_t->location_number=loop_head->location_number; + unwind_log.insert(new_t, loop_head->location_number); + } + + assert(!rest_program.empty()); + + // to be filled with copies of the loop body + goto_programt copies; + + if(k!=0) + { + iteration_points.resize(k); + + // add a goto before the loop exit to guard against 'fall-out' + + goto_programt::const_targett t_before=loop_exit; + t_before--; + + if(!t_before->is_goto() || !t_before->guard.is_true()) { - // guard against 'fall-out' goto_programt::targett t_goto=goto_program.insert_before(loop_exit); + unwind_log.insert(t_goto, loop_exit->location_number); - t_goto->make_goto(loop_exit); + t_goto->make_goto(get_mutable(goto_program, loop_exit)); t_goto->source_location=loop_exit->source_location; t_goto->function=loop_exit->function; t_goto->guard=true_exprt(); + t_goto->location_number=loop_exit->location_number; } - } - goto_programt::targett t_skip=goto_program.insert_before(loop_exit); - goto_programt::targett loop_iter=t_skip; + // add a skip before the loop exit - t_skip->make_skip(); - t_skip->source_location=loop_head->source_location; - t_skip->function=loop_head->function; + goto_programt::targett t_skip=goto_program.insert_before(loop_exit); + unwind_log.insert(t_skip, loop_exit->location_number); - // record the exit point of first iteration - iteration_points[0]=loop_iter; + t_skip->make_skip(); + t_skip->source_location=loop_head->source_location; + t_skip->function=loop_head->function; + t_skip->location_number=loop_head->location_number; - // build a map for branch targets inside the loop - std::map target_map; + // where to go for the next iteration + goto_programt::targett loop_iter=t_skip; - { - unsigned count=0; - for(goto_programt::targett t=loop_head; - t!=loop_exit; t++, count++) - { - assert(t!=goto_program.instructions.end()); - target_map[t]=count; - } - } + // record the exit point of first iteration + iteration_points[0]=loop_iter; - // re-direct any branches that go to loop_head to loop_iter + // re-direct any branches that go to loop_head to loop_iter - for(goto_programt::targett t=loop_head; - t!=loop_iter; t++) - { - assert(t!=goto_program.instructions.end()); - for(goto_programt::instructiont::targetst::iterator - t_it=t->targets.begin(); - t_it!=t->targets.end(); - t_it++) - if(*t_it==loop_head) *t_it=loop_iter; - } - - // we make k-1 copies, to be inserted before loop_exit - goto_programt copies; + for(goto_programt::targett t=get_mutable(goto_program, loop_head); + t!=loop_iter; t++) + { + if(!t->is_goto()) + continue; - for(unsigned i=1; i target_vector; - target_vector.reserve(target_map.size()); + if(t->get_target()==loop_head) + t->set_target(loop_iter); + } - for(goto_programt::targett t=loop_head; - t!=loop_exit; t++) + // k-1 additional copies + for(unsigned i=1; ilocation_number); - // adjust the intra-loop branches + t_skip->make_skip(); + t_skip->source_location=loop_head->source_location; + t_skip->function=loop_head->function; + t_skip->location_number=loop_head->location_number; - for(std::size_t i=0; iis_goto()) + continue; - for(goto_programt::instructiont::targetst::iterator - t_it=t->targets.begin(); - t_it!=t->targets.end(); - t_it++) + goto_programt::const_targett t=i_it->get_target(); + + if(t->location_number>=loop_head->location_number || + t->location_numberlocation_number) { - std::map::const_iterator - m_it=target_map.find(*t_it); - if(m_it!=target_map.end()) // intra-loop? - { - assert(m_it->secondsecond]; - } + i_it->set_target(t_skip); } } - } - assert(copies.instructions.size()==(k-1)*target_map.size()); + // delete loop body + goto_program.instructions.erase(loop_head, loop_exit); + } + // after unwound part + copies.destructive_append(rest_program); + // now insert copies before loop_exit goto_program.destructive_insert(loop_exit, copies); +} + +/*******************************************************************\ + +Function: get_k + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +int goto_unwindt::get_k( + const irep_idt func, + const unsigned loop_id, + const int global_k, + const unwind_sett &unwind_set) const +{ + assert(global_k>=-1); + + unwind_sett::const_iterator f_it=unwind_set.find(func); + if(f_it==unwind_set.end()) + return global_k; + + const std::map &m=f_it->second; + std::map::const_iterator l_it=m.find(loop_id); + if(l_it==m.end()) + return global_k; + + int k=l_it->second; + assert(k>=-1); + + return k; +} + +/*******************************************************************\ + +Function: unwind + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_unwindt::unwind( + goto_programt &goto_program, + const unwind_sett &unwind_set, + const int k, + const unwind_strategyt unwind_strategy) +{ + assert(k>=-1); + + for(goto_programt::const_targett i_it=goto_program.instructions.begin(); + i_it!=goto_program.instructions.end(); i_it++) + { + if(!i_it->is_backwards_goto()) + continue; + + const irep_idt func=i_it->function; + assert(!func.empty()); + + unsigned loop_number=i_it->loop_number; + + int final_k=get_k(func, loop_number, k, unwind_set); + + if(final_k==-1) + continue; + + goto_programt::const_targett loop_head=i_it->get_target(); + goto_programt::const_targett loop_exit=i_it; + loop_exit++; + assert(loop_exit!=goto_program.instructions.end()); + + unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy); - // update it all - goto_program.update(); + // necessary as we change the goto program in the previous line + i_it=loop_exit; + i_it--; // as for loop first increments + } } /*******************************************************************\ -Function: goto_unwind +Function: operator() Inputs: @@ -184,47 +425,58 @@ Function: goto_unwind \*******************************************************************/ -void goto_unwind( +void goto_unwindt::operator()( goto_functionst &goto_functions, - const unsigned k) + const unwind_sett &unwind_set, + const int k, + const unwind_strategyt unwind_strategy) { - // Here we unwind all loops in the program. - // Each loop body is simply repeated k times (if condition holds) + assert(k>=-1); + Forall_goto_functions(it, goto_functions) { goto_functionst::goto_functiont &goto_function=it->second; + if(!goto_function.body_available()) - { continue; - } + goto_programt &goto_program=goto_function.body; - // the unwinding continues until there is no loop in the function - while(true) - { - natural_loops_mutablet natural_loops(goto_program); - // if there is no loop anymore in the current function, - // then go to the next function for unwinding - if(natural_loops.loop_map.size()==0) - { - break; - } - typedef const natural_loops_mutablet::natural_loopt loopt; - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) - { - // save a copy of the loop guard - const exprt loop_guard=l_it->first->guard; + unwind(goto_program, unwind_set, k, unwind_strategy); + } +} - const loopt &loop=l_it->second; - assert(!loop.empty()); - goto_programt::targett loop_exit=get_loop_exit(loop); +/*******************************************************************\ - unwind(goto_program, l_it->first, loop_exit, k); +Function: show_log_json - } - } + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +// call after calling goto_functions.update()! +jsont goto_unwindt::unwind_logt::output_log_json() const +{ + json_objectt json_result; + json_arrayt &json_unwound=json_result["unwound"].make_array(); + + for(location_mapt::const_iterator it=location_map.begin(); + it!=location_map.end(); it++) + { + json_objectt &object=json_unwound.push_back().make_object(); + + goto_programt::const_targett target=it->first; + unsigned location_number=it->second; + + object["original_location_number"]=json_numbert(i2string( + location_number)); + object["new_location_number"]=json_numbert(i2string( + target->location_number)); } + + return json_result; } diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h index ac93496a842..bda09c566b7 100644 --- a/src/goto-instrument/unwind.h +++ b/src/goto-instrument/unwind.h @@ -1,31 +1,129 @@ /*******************************************************************\ -Module: loop unwinding +Module: Loop unwinding Author: Daniel Kroening, kroening@kroening.com + Daniel Poetzl \*******************************************************************/ -#ifndef CPROVER_UNWIND_H -#define CPROVER_UNWIND_H +#ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H +#define CPROVER_GOTO_INSTRUMENT_UNWIND_H +#include +#include +#include #include -void unwind( - goto_programt &goto_program, - goto_programt::targett loop_head, - goto_programt::targett loop_exit, - const unsigned k); - -void unwind( - goto_programt &goto_program, - goto_programt::targett loop_head, - goto_programt::targett loop_exit, - const unsigned k, - std::vector &iteration_points); - -void goto_unwind( - goto_functionst &goto_functions, - const unsigned k); +// -1: do not unwind loop +typedef std::map> unwind_sett; + +void parse_unwindset(const std::string &us, unwind_sett &unwind_set); + +class goto_unwindt +{ +public: + typedef enum { CONTINUE, PARTIAL, ASSERT, ASSUME } unwind_strategyt; + + // unwind loop + + void unwind( + goto_programt &goto_program, + const goto_programt::const_targett loop_head, + const goto_programt::const_targett loop_exit, + const unsigned k, // bound for given loop + const unwind_strategyt unwind_strategy); + + void unwind( + goto_programt &goto_program, + const goto_programt::const_targett loop_head, + const goto_programt::const_targett loop_exit, + const unsigned k, // bound for given loop + const unwind_strategyt unwind_strategy, + std::vector &iteration_points); + + // unwind function + + void unwind( + goto_programt &goto_program, + const unwind_sett &unwind_set, + const int k=-1, // -1: no global bound + const unwind_strategyt unwind_strategy=PARTIAL); + + // unwind all functions + + void operator()( + goto_functionst &goto_functions, + const unsigned k, // global bound + const unwind_strategyt unwind_strategy=PARTIAL) + { + const unwind_sett unwind_set; + operator()(goto_functions, unwind_set, (int)k, unwind_strategy); + } + + void operator()( + goto_functionst &goto_functions, + const unwind_sett &unwind_set, + const int k=-1, // -1: no global bound + const unwind_strategyt unwind_strategy=PARTIAL); + + // unwind log + + jsont output_log_json() const + { + return unwind_log.output_log_json(); + } + + // log + // - for each copied instruction the location number of the + // original instruction it came from + // - for each new instruction the location number of the loop head + // or backedge of the loop it is associated with + struct unwind_logt + { + // call after calling goto_functions.update()! + jsont output_log_json() const; + + // remove entries that refer to the given goto program + void cleanup(const goto_programt &goto_program) + { + forall_goto_program_instructions(it, goto_program) + location_map.erase(it); + } + + void insert( + const goto_programt::const_targett target, + const unsigned location_number) + { + auto r=location_map.insert(std::make_pair(target, location_number)); + assert(r.second); // did not exist yet + } + + typedef std::map location_mapt; + location_mapt location_map; + }; + + unwind_logt unwind_log; + +protected: + int get_k( + const irep_idt func, + const unsigned loop_id, + const int global_k, + const unwind_sett &unwind_set) const; + + // copy goto program segment and redirect internal edges + void copy_segment( + const goto_programt::const_targett start, + const goto_programt::const_targett end, // exclusive + goto_programt &goto_program); // result + + goto_programt::targett get_mutable( + goto_programt &goto_program, + const goto_programt::const_targett t) const + { + return goto_program.instructions.erase(t, t); + } +}; #endif diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 4de571933f7..02c421dca23 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -293,6 +293,13 @@ class goto_program_templatet { return instructions.insert(target, instructiont()); } + + //! Insertion before the given target + //! \return newly inserted location + inline targett insert_before(const_targett target) + { + return instructions.insert(target, instructiont()); + } //! Insertion after the given target //! \return newly inserted location @@ -322,6 +329,17 @@ class goto_program_templatet // BUG: The iterators to p-instructions are invalidated! } + //! Inserts the given program at the given location. + //! The program is destroyed. + inline void destructive_insert( + const_targett target, + goto_program_templatet &p) + { + instructions.splice(target, + p.instructions); + // BUG: The iterators to p-instructions are invalidated! + } + //! Adds an instruction at the end. //! \return The newly added instruction. inline targett add_instruction() diff --git a/src/util/Makefile b/src/util/Makefile index 5e11f3f1db4..2fddfa618bb 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -21,7 +21,8 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.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_expr.cpp + ssa_expr.cpp json_expr.cpp \ + string_utils.cpp INCLUDES= -I .. diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp new file mode 100644 index 00000000000..1c33e5aa654 --- /dev/null +++ b/src/util/string_utils.cpp @@ -0,0 +1,137 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include +#include + +#include "string_utils.h" + +/*******************************************************************\ + +Function: + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::string strip_string(const std::string &s) +{ + std::string::size_type n=s.length(); + + // find first non-space char + unsigned i; + for(i=0; i &result, + bool strip, + bool remove_empty) +{ + assert(result.empty()); + assert(!std::isspace(delim)); + + if(s.empty()) + { + result.push_back(""); + return; + } + + std::string::size_type n=s.length(); + assert(n>0); + + unsigned start=0; + unsigned i; + + for (i=0; i result; + + split_string(s, delim, result, strip); + if(result.size()!=2) + throw "split string did not generate exactly 2 parts"; + + left=result[0]; + right=result[1]; +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h new file mode 100644 index 00000000000..703fc359e82 --- /dev/null +++ b/src/util/string_utils.h @@ -0,0 +1,31 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_STRING_UTILS_H +#define CPROVER_UTIL_STRING_UTILS_H + +#include +#include + +std::string strip_string(const std::string &s); + +void split_string( + const std::string &s, + char delim, // must not be a whitespace character + std::vector &result, + bool strip=false, // strip whitespace from elements + bool remove_empty=false); // remove empty elements + +void split_string( + const std::string &s, + char delim, + std::string &left, + std::string &right, + bool strip=false); + +#endif diff --git a/unit/Makefile b/unit/Makefile index c26ba71b4f0..0b442445a0f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,6 +1,6 @@ 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 + smt2_parser.cpp wp.cpp string_utils.cpp INCLUDES= -I ../src/ @@ -55,3 +55,7 @@ smt2_parser$(EXEEXT): smt2_parser$(OBJEXT) wp$(EXEEXT): wp$(OBJEXT) $(LINKBIN) + +string_utils$(EXEEXT): string_utils$(OBJEXT) + $(LINKBIN) + diff --git a/unit/string_utils.cpp b/unit/string_utils.cpp new file mode 100644 index 00000000000..b02b1d24674 --- /dev/null +++ b/unit/string_utils.cpp @@ -0,0 +1,50 @@ +#include +#include +#include + +#include + +int main() +{ + assert(strip_string(" x y ")=="x y"); + + const std::string test=" a,, x , ,"; + + std::vector result; + split_string(test, ',', result, false, false); + assert(result.size()==5); + assert(result[0]==" a"); + assert(result[1]==""); + assert(result[2]==" x "); + assert(result[3]==" "); + assert(result[4]==""); + + result.clear(); + split_string(test, ',', result, true, false); + assert(result.size()==5); + assert(result[0]=="a"); + assert(result[1]==""); + assert(result[2]=="x"); + assert(result[3]==""); + assert(result[4]==""); + + result.clear(); + split_string(test, ',', result, false, true); + assert(result.size()==3); + assert(result[0]==" a"); + assert(result[1]==" x "); + assert(result[2]==" "); + + result.clear(); + split_string(test, ',', result, true, true); + assert(result.size()==2); + assert(result[0]=="a"); + assert(result[1]=="x"); + + std::string s1; + std::string s2; + split_string("a:b", ':', s1, s2, false); + assert(s1=="a"); + assert(s2=="b"); +} +