From 49333eb248c2dba3eaf4ccce8c1bbd95bf5c83a0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 May 2018 11:13:32 +0000 Subject: [PATCH 1/2] Make restore_returns handle simplified programs The static simplifier may have removed useless goto statements, leaving programs in a form not previously expected by restore_returns, while it actually is still safe to use restore_returns on those. --- src/goto-programs/remove_returns.cpp | 33 ++-------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 5257c83ea0a..71d2761dc5c 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -352,38 +352,9 @@ bool remove_returnst::restore_returns( continue; // replace "fkt#return_value=x;" by "return x;" - code_returnt return_code(assign.rhs()); - - // the assignment might be a goto target - i_it->make_skip(); - i_it++; - - while(!i_it->is_goto() && !i_it->is_end_function()) - { - INVARIANT( - i_it->is_dead(), - "only dead statements should appear between " - "a return and the next goto or function end"); - i_it++; - } - - if(i_it->is_goto()) - { - INVARIANT( - i_it->get_target()->is_end_function(), - "GOTO following return should target end of function"); - } - else - { - INVARIANT( - i_it->is_end_function(), - "control-flow after assigning return value should lead directly " - "to end of function"); - i_it=goto_program.instructions.insert(i_it, *i_it); - } - + const exprt rhs = assign.rhs(); i_it->make_return(); - i_it->code=return_code; + i_it->code = code_returnt(rhs); } } From fc02e8ffd04e5c5eee19bae0adf69f64e062a897 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 May 2018 09:48:52 +0000 Subject: [PATCH 2/2] Restore returns before writing the simplified binary The static simplifier should not alter types of symbols. Doing so would cause conflicts if later attempting to link additional functions such as the C library as the types no longer match. --- src/goto-analyzer/static_simplifier.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 08e29037c70..ebda62896dd 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -12,6 +12,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include #include #include #include @@ -169,6 +170,10 @@ bool static_simplifier( goto_model.goto_functions.update(); } + // restore return types before writing the binary + restore_returns(goto_model); + goto_model.goto_functions.update(); + m.status() << "Writing goto binary" << messaget::eom; return write_goto_binary(out, ns.get_symbol_table(),