diff --git a/regression/cbmc-cover/block-coverage-report2/test.desc b/regression/cbmc-cover/block-coverage-report2/test.desc index 82ca670a358..87f86152050 100644 --- a/regression/cbmc-cover/block-coverage-report2/test.desc +++ b/regression/cbmc-cover/block-coverage-report2/test.desc @@ -4,7 +4,7 @@ main.c block 1 \(lines main.c:main:13,14\): SATISFIED block 2 \(lines main.c:main:15\): SATISFIED block 3 \(lines main.c:main:17,18\): SATISFIED -block 4 \(lines main.c:main:18,19\): SATISFIED +block 4 \(lines main.c:main:19\): SATISFIED block 5 \(lines main.c:main:20\): SATISFIED block 6 \(lines main.c:main:15,21,22\): SATISFIED block 7 \(lines main.c:main:24,25\): SATISFIED diff --git a/regression/cbmc/reachability-slice-interproc3/test.desc b/regression/cbmc/reachability-slice-interproc3/test.desc index 66f6ca60700..ccf9d04e679 100644 --- a/regression/cbmc/reachability-slice-interproc3/test.desc +++ b/regression/cbmc/reachability-slice-interproc3/test.desc @@ -3,6 +3,6 @@ main.c --reachability-slice-fb --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ -ASSIGN main#return_value := 1 +SET RETURN VALUE 1$ -- ^warning: ignoring diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 70319de4204..0ba91129038 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -388,6 +389,7 @@ int goto_analyzer_parse_optionst::doit() // Preserve backwards compatibility in processing options.set_option("partial-inline", true); options.set_option("rewrite-union", false); + options.set_option("remove-returns", true); if(process_goto_program(options)) return CPROVER_EXIT_INTERNAL_ERROR; diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 34c5f42de38..cf18e2f9f2b 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -13,6 +13,7 @@ Date: April 2017 #include "mm_io.h" +#include #include #include #include @@ -35,6 +36,7 @@ void collect_deref_expr( void mm_io( const exprt &mm_io_r, + const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns) @@ -60,21 +62,20 @@ void mm_io( source_locationt source_location = it->source_location(); const code_typet &ct=to_code_type(mm_io_r.type()); - irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier(); - auto return_value = return_value_symbol(identifier, ns); - if_exprt if_expr(integer_address(d.pointer()), return_value, d); + if_exprt if_expr(integer_address(d.pointer()), mm_io_r_value, d); replace_expr(d, if_expr, a_rhs); const typet &pt=ct.parameters()[0].type(); const typet &st=ct.parameters()[1].type(); auto size_opt = size_of_expr(d.type(), ns); CHECK_RETURN(size_opt.has_value()); - const code_function_callt fc( + auto call = goto_programt::make_function_call( + mm_io_r_value, mm_io_r, {typecast_exprt(d.pointer(), pt), - typecast_exprt(size_opt.value(), st)}); - goto_function.body.insert_before_swap(it); - *it = goto_programt::make_function_call(fc, source_location); + typecast_exprt(size_opt.value(), st)}, + source_location); + goto_function.body.insert_before_swap(it, call); it++; } } @@ -105,26 +106,37 @@ void mm_io( } } -void mm_io( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions) { const namespacet ns(symbol_table); - exprt mm_io_r=nil_exprt(), mm_io_w=nil_exprt(); + exprt mm_io_r = nil_exprt(), mm_io_r_value = nil_exprt(), + mm_io_w = nil_exprt(); irep_idt id_r=CPROVER_PREFIX "mm_io_r"; irep_idt id_w=CPROVER_PREFIX "mm_io_w"; auto maybe_symbol=symbol_table.lookup(id_r); if(maybe_symbol) + { mm_io_r=maybe_symbol->symbol_expr(); + const auto &value_symbol = get_fresh_aux_symbol( + to_code_type(mm_io_r.type()).return_type(), + id2string(id_r) + "$value", + id2string(id_r) + "$value", + maybe_symbol->location, + maybe_symbol->mode, + symbol_table); + + mm_io_r_value = value_symbol.symbol_expr(); + } + maybe_symbol=symbol_table.lookup(id_w); if(maybe_symbol) mm_io_w=maybe_symbol->symbol_expr(); for(auto & f : goto_functions.function_map) - mm_io(mm_io_r, mm_io_w, f.second, ns); + mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns); } void mm_io(goto_modelt &model) diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 68121ab9335..5154290ff38 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -58,9 +58,16 @@ bool process_goto_program( } // remove returns, gcc vectors, complex - remove_returns(goto_model); + if( + options.get_bool_option("remove-returns") || + options.get_bool_option("string-abstraction")) + { + remove_returns(goto_model); + } + remove_vector(goto_model); remove_complex(goto_model); + if(options.get_bool_option("rewrite-union")) rewrite_union(goto_model); diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index a2ff3a33da5..7fc772b1b7d 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -14,7 +14,6 @@ Date: Oct 2018 #include #include "goto_functions.h" -#include "remove_returns.h" namespace { @@ -38,18 +37,6 @@ class validate_goto_modelt /// Check that no function calls via function pointer are present void function_pointer_calls_removed(); - /// Check returns have been removed - /// - /// Calls via function pointer must have been removed already when - /// removing returns, thus enabling this check also enables the check - /// that all calls via function pointer have been removed - /// - /// Sub-checks are: - /// - no return statements in any of the functions - /// - lhs of every \ref code_function_callt instruction is nil - /// - all return types are void (of both calls and functions themselves) - void check_returns_removed(); - /// Check that for all: /// -# functions that are called or /// -# functions of which the address is taken @@ -74,19 +61,11 @@ validate_goto_modelt::validate_goto_modelt( if(validation_options.entry_point_exists) entry_point_exists(); - /// NB function pointer calls must have been removed before removing - /// returns - so 'check_returns_removed' also enables - // 'function_pointer_calls_removed' - if( - validation_options.function_pointer_calls_removed || - validation_options.check_returns_removed) + if(validation_options.function_pointer_calls_removed) { function_pointer_calls_removed(); } - if(validation_options.check_returns_removed) - check_returns_removed(); - if(validation_options.check_called_functions) check_called_functions(); } @@ -116,30 +95,6 @@ void validate_goto_modelt::function_pointer_calls_removed() } } -void validate_goto_modelt::check_returns_removed() -{ - for(const auto &fun : function_map) - { - const goto_functiont &goto_function = fun.second; - - for(const auto &instr : goto_function.body.instructions) - { - DATA_CHECK( - vm, - !instr.is_set_return_value(), - "no SET_RETURN_VALUE instructions should be present"); - - if(instr.is_function_call()) - { - DATA_CHECK( - vm, - !does_function_call_return(instr), - "function call lhs return should be nil"); - } - } - } -} - void validate_goto_modelt::check_called_functions() { auto test_for_function_address = diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index d9670e644bd..0047bc9acd9 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -31,6 +31,7 @@ SRC = auto_objects.cpp \ symex_goto.cpp \ symex_main.cpp \ symex_other.cpp \ + symex_set_return_value.cpp \ symex_start_thread.cpp \ symex_target.cpp \ symex_target_equation.cpp \ diff --git a/src/goto-symex/frame.h b/src/goto-symex/frame.h index e0f55196af1..d80f8b3f9b4 100644 --- a/src/goto-symex/frame.h +++ b/src/goto-symex/frame.h @@ -14,6 +14,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "goto_state.h" #include "symex_target.h" + #include /// Stack frames -- these are used for function calls and for exceptions @@ -30,7 +31,8 @@ struct framet std::vector parameter_names; guardt guard_at_function_start; goto_programt::const_targett end_of_function; - exprt return_value = nil_exprt(); + exprt call_lhs = nil_exprt(); // cleaned, but not renamed + optionalt return_value_symbol; // not renamed bool hidden_function = false; symex_level1t old_level1; diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 2e45e803fb3..c7fb2d37abe 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -303,6 +303,10 @@ class goto_symext /// Symbolically execute a GOTO instruction in the context of unreachable code /// \param state: Symbolic execution state for current instruction void symex_unreachable_goto(statet &state); + /// Symbolically execute a SET_RETURN_VALUE instruction + /// \param state: Symbolic execution state for current instruction + /// \param return_value: The value to be returned + void symex_set_return_value(statet &state, const exprt &return_value); /// Symbolically execute a START_THREAD instruction /// \param state: Symbolic execution state for current instruction virtual void symex_start_thread(statet &state); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 9e00e5d201d..53f601e0b16 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -332,11 +332,33 @@ void goto_symext::symex_function_call_post_clean( // assign actuals to formal parameters parameter_assignments(identifier, goto_function, state, cleaned_arguments); - frame.end_of_function=--goto_function.body.instructions.end(); - frame.return_value = cleaned_lhs; + frame.call_lhs = cleaned_lhs; + frame.end_of_function = --goto_function.body.instructions.end(); frame.function_identifier=identifier; frame.hidden_function = goto_function.is_hidden(); + // set up the 'return value symbol' when needed + if(frame.call_lhs.is_not_nil()) + { + irep_idt return_value_symbol_identifier = + "goto_symex::return_value::" + id2string(identifier); + + if(!state.symbol_table.has_symbol(return_value_symbol_identifier)) + { + const symbolt &function_symbol = ns.lookup(identifier); + auxiliary_symbolt + new_symbol; // these are thread-local and have dynamic lifetime + new_symbol.base_name = "return_value"; + new_symbol.name = return_value_symbol_identifier; + new_symbol.type = to_code_type(function_symbol.type).return_type(); + new_symbol.mode = function_symbol.mode; + state.symbol_table.add(new_symbol); + } + + frame.return_value_symbol = + ns.lookup(return_value_symbol_identifier).symbol_expr(); + } + const framet &p_frame = state.call_stack().previous_frame(); for(const auto &pair : p_frame.loop_iterations) { @@ -405,14 +427,33 @@ static void pop_frame( /// do function call by inlining void goto_symext::symex_end_of_function(statet &state) { + PRECONDITION(!state.call_stack().empty()); + const bool hidden = state.call_stack().top().hidden_function; // first record the return target.function_return( state.guard.as_expr(), state.source.function_id, state.source, hidden); - // then get rid of the frame + // before we drop the frame, remember the call LHS + // and the return value symbol, if any + auto call_lhs = state.call_stack().top().call_lhs; + auto return_value_symbol = state.call_stack().top().return_value_symbol; + + // now get rid of the frame pop_frame(state, path_storage, symex_config.doing_path_exploration); + + // after dropping the frame, assign the return value, if any + if(state.reachable && call_lhs.is_not_nil()) + { + DATA_INVARIANT( + return_value_symbol.has_value(), + "must have return value symbol when assigning call lhs"); + // the type of the call lhs and the return type might not match + auto casted_return_value = typecast_exprt::conditional_cast( + return_value_symbol.value(), call_lhs.type()); + symex_assign(state, call_lhs, casted_return_value); + } } /// Preserves locality of parameters of a given function by applying L1 diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 36cd1b1a55b..697779db366 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -661,8 +661,9 @@ void goto_symext::execute_next_instruction( break; case SET_RETURN_VALUE: - // This case should have been removed by return-value removal - UNREACHABLE; + if(state.reachable) + symex_set_return_value(state, instruction.return_value()); + symex_transition(state); break; case ASSIGN: diff --git a/src/goto-symex/symex_set_return_value.cpp b/src/goto-symex/symex_set_return_value.cpp new file mode 100644 index 00000000000..c0cbc28e83d --- /dev/null +++ b/src/goto-symex/symex_set_return_value.cpp @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: Symbolic Execution of ANSI-C + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Symbolic Execution of ANSI-C + +#include "goto_symex.h" + +void goto_symext::symex_set_return_value( + statet &state, + const exprt &return_value) +{ + // we must be inside a function that was called + PRECONDITION(!state.call_stack().empty()); + + framet &frame = state.call_stack().top(); + if(frame.return_value_symbol.has_value()) + { + symex_assign(state, frame.return_value_symbol.value(), return_value); + } +} diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 6c35b8e3868..48fa3053e32 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -185,48 +185,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") } } - WHEN("not all returns have been removed - a function call lhs is not nil") - { - // int h(); - symbolt h; - h.name = "h"; - h.mode = ID_C; - h.type = code_typet({}, signed_int_type()); - h.value = code_blockt{}; - goto_model.symbol_table.add(h); - - // the lhs is non-nil - code_function_callt function_call{from_integer(1, signed_int_type()), - h.symbol_expr(), - code_function_callt::argumentst{}}; - symbolt k; - k.name = "k"; - k.mode = ID_C; - k.type = code_typet({}, empty_typet{}); - - code_blockt k_body{{function_call}}; - k.value = k_body; - - goto_model.symbol_table.add(k); - - THEN("fail!") - { - goto_convert(goto_model, null_message_handler); - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_returns_removed = true; - - REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), - incorrect_goto_program_exceptiont); - } - } - WHEN("all returns have been removed") { THEN("true!")