From 1587505146db43d0174268f0e2512f36e04c4b1d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 16 Feb 2017 15:29:37 +0000 Subject: [PATCH] Fix an issue in is_threadedt where the is_threaded property was not propagated back to function call sites --- .../goto-instrument/is-threaded1/main.c | 25 ++++++++++ .../goto-instrument/is-threaded1/test.desc | 7 +++ src/analyses/is_threaded.cpp | 49 ++++++++----------- .../goto_instrument_parse_options.cpp | 26 ++++++++++ .../goto_instrument_parse_options.h | 3 +- 5 files changed, 81 insertions(+), 29 deletions(-) create mode 100644 regression/goto-instrument/is-threaded1/main.c create mode 100644 regression/goto-instrument/is-threaded1/test.desc diff --git a/regression/goto-instrument/is-threaded1/main.c b/regression/goto-instrument/is-threaded1/main.c new file mode 100644 index 00000000000..875af72fec0 --- /dev/null +++ b/regression/goto-instrument/is-threaded1/main.c @@ -0,0 +1,25 @@ + +int x; + +void func2() +{ + x = 3; +} + +void func1() +{ + x = 1; + func2(); + x = 2; +} + +int main() +{ + x = 4; + __CPROVER_ASYNC_0: + func1(); + x = 5; + + return 0; +} + diff --git a/regression/goto-instrument/is-threaded1/test.desc b/regression/goto-instrument/is-threaded1/test.desc new file mode 100644 index 00000000000..a9bc6080e8d --- /dev/null +++ b/regression/goto-instrument/is-threaded1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--show-threaded +activate-multi-line-match +x = 2;\nIs threaded: True +-- +^warning: ignoring diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 812041903f0..905cd6b91ac 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -15,41 +15,33 @@ class is_threaded_domaint:public ai_domain_baset { public: bool reachable; - bool has_spawn; bool is_threaded; - inline is_threaded_domaint(): + is_threaded_domaint(): reachable(false), - has_spawn(false), is_threaded(false) { // this is bottom } - inline bool merge( + bool merge( const is_threaded_domaint &src, locationt from, locationt to) { + // assert(src.reachable); + + if(!src.reachable) + return false; + bool old_reachable=reachable; - if(src.reachable) - reachable=true; - - bool old_h_s=has_spawn; - if(src.has_spawn && - (from->is_end_function() || - from->function==to->function)) - has_spawn=true; - - bool old_i_t=is_threaded; - if(has_spawn || - (src.is_threaded && - !from->is_end_function())) - is_threaded=true; + bool old_is_threaded=is_threaded; + + reachable=true; + is_threaded|=src.is_threaded; return old_reachable!=reachable || - old_i_t!=is_threaded || - old_h_s!=has_spawn; + old_is_threaded!=is_threaded; } void transform( @@ -58,30 +50,31 @@ class is_threaded_domaint:public ai_domain_baset ai_baset &ai, const namespacet &ns) final { + // assert(reachable); + if(!reachable) return; - if(from->is_start_thread() || - to->is_end_thread()) - { - has_spawn=true; + + if(from->is_start_thread()) is_threaded=true; - } } void make_bottom() final { - reachable=has_spawn=is_threaded=false; + reachable=false; + is_threaded=false; } void make_top() final { - reachable=has_spawn=is_threaded=true; + reachable=true; + is_threaded=true; } void make_entry() final { reachable=true; - has_spawn=is_threaded=false; + is_threaded=false; } }; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 857c590fe65..3cbbac3a55b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -52,6 +52,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -246,6 +247,31 @@ int goto_instrument_parse_optionst::doit() } } + if(cmdline.isset("show-threaded")) + { + namespacet ns(symbol_table); + + is_threadedt is_threaded(goto_functions); + + forall_goto_functions(f_it, goto_functions) + { + std::cout << "////" << std::endl; + std::cout << "//// Function: " << f_it->first << std::endl; + std::cout << "////" << std::endl; + std::cout << std::endl; + + const goto_programt &goto_program=f_it->second.body; + + forall_goto_program_instructions(i_it, goto_program) + { + goto_program.output_instruction(ns, "", std::cout, i_it); + std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False") + << std::endl; + std::cout << std::endl; + } + } + } + if(cmdline.isset("show-value-sets")) { do_indirect_call_and_rtti_removal(); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1d74bd94dbf..1db5f0bdb4d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -67,7 +67,8 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" + "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ + "(show-threaded)" class goto_instrument_parse_optionst: public parse_options_baset,