diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 03d24c1ae65..ad226c0499a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -550,7 +550,7 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate(); } if( @@ -691,7 +691,7 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - lazy_goto_model.validate(validation_modet::INVARIANT); + lazy_goto_model.validate(); } // Provide show-goto-functions and similar dump functions after symex diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 43b24793e1f..368edf04e33 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -53,24 +53,25 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include -#include -#include -#include #include +#include +#include #include #include #include -#include #include +#include #include #include +#include -#include +#include #include #include -#include +#include #include @@ -550,7 +551,7 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate(); } if( diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 68266c0fe8d..492c859c88d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -405,7 +406,7 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate(); } // show it? diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3b8c6983ce0..fa29a36bdf8 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -35,6 +35,7 @@ Date: June 2006 #include #include #include +#include #include #include @@ -546,7 +547,7 @@ bool compilet::write_bin_object_file( if(validate_goto_model) { status() << "Validating goto model" << eom; - src_goto_model.validate(validation_modet::INVARIANT); + src_goto_model.validate(); } statistics() << "Writing binary format object `" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 840b395ad9a..516be63d660 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -25,25 +25,26 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include #include -#include -#include -#include -#include #include -#include -#include -#include #include +#include +#include +#include +#include +#include #include +#include #include -#include -#include +#include +#include +#include #include +#include +#include +#include +#include +#include #include #include @@ -147,7 +148,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate(); } { diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index d25bfe32d70..c66e8a4c837 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -64,6 +64,7 @@ SRC = adjust_float_expressions.cpp \ string_abstraction.cpp \ string_instrumentation.cpp \ system_library_symbols.cpp \ + validate_goto_model.cpp \ vcd_goto_trace.cpp \ wp.cpp \ write_goto_binary.cpp \ diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h index 25243c8f5eb..856c5cff284 100644 --- a/src/goto-programs/abstract_goto_model.h +++ b/src/goto-programs/abstract_goto_model.h @@ -13,6 +13,7 @@ Author: Diffblue Ltd. #define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H #include "goto_functions.h" +#include "validate_goto_model.h" #include /// Abstract interface to eager or lazy GOTO models @@ -54,7 +55,11 @@ class abstract_goto_modelt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - virtual void validate(const validation_modet vm) const = 0; + // virtual void validate(const validation_modet vm) const = 0; + virtual void validate( + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) + const = 0; }; #endif diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index 99fd01e1b33..3d86edcded8 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -36,6 +36,15 @@ void get_local_identifiers( void goto_functiont::validate(const namespacet &ns, const validation_modet vm) const { + // function body must end with an END_FUNCTION instruction + if(body_available()) + { + DATA_CHECK( + vm, + body.instructions.back().is_end_function(), + "last instruction should be of end function type"); + } + body.validate(ns, vm); find_symbols_sett typetags; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index a640dc5885f..52631d121a9 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "abstract_goto_model.h" #include "goto_functions.h" +#include "validate_goto_model.h" // A model is a pair consisting of a symbol table // and the CFGs for the functions. @@ -94,10 +95,18 @@ class goto_modelt : public abstract_goto_modelt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const validation_modet vm) const override + void validate( + const validation_modet vm = validation_modet::INVARIANT, + const goto_model_validation_optionst &goto_model_validation_options = + goto_model_validation_optionst{}) const override { symbol_table.validate(vm); + // Does a number of checks at the function_mapt level to ensure the + // goto_program is well formed. Does not call any validate methods + // (at the goto_functiont level or below) + validate_goto_model(goto_functions, vm, goto_model_validation_options); + const namespacet ns(symbol_table); goto_functions.validate(ns, vm); } @@ -142,10 +151,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const validation_modet vm) const override + void validate( + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) + const override { symbol_table.validate(vm); + // Does a number of checks at the function_mapt level to ensure the + // goto_program is well formed. Does not call any validate methods + // (at the goto_functiont level or below) + validate_goto_model(goto_functions, vm, goto_model_validation_options); + const namespacet ns(symbol_table); goto_functions.validate(ns, vm); } diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index bda9c4cf3a0..67d291631c6 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -194,7 +194,11 @@ goto_modelt initialize_goto_model( if(options.is_set("validate-goto-model")) { - goto_model.validate(validation_modet::EXCEPTION); + goto_model_validation_optionst goto_model_validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + goto_model.validate( + validation_modet::INVARIANT, goto_model_validation_options); } // stupid hack diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index d62b477c838..1979064c5da 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -247,9 +247,12 @@ class lazy_goto_modelt : public abstract_goto_modelt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const validation_modet vm) const override + void validate( + const validation_modet vm = validation_modet::INVARIANT, + const goto_model_validation_optionst &goto_model_validation_options = + goto_model_validation_optionst{}) const override { - goto_model->validate(vm); + goto_model->validate(vm, goto_model_validation_options); } private: diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp new file mode 100644 index 00000000000..2f3d42480e6 --- /dev/null +++ b/src/goto-programs/validate_goto_model.cpp @@ -0,0 +1,217 @@ +/*******************************************************************\ +Module: Validate Goto Programs + +Author: Diffblue + +Date: Oct 2018 + +\*******************************************************************/ + +#include "validate_goto_model.h" + +#include + +#include + +#include "goto_functions.h" + +namespace +{ +class validate_goto_modelt +{ +public: + using function_mapt = goto_functionst::function_mapt; + + validate_goto_modelt( + const goto_functionst &goto_functions, + const validation_modet vm, + const goto_model_validation_optionst goto_model_validation_options); + +private: + /// Check the goto_program has an entry point + /// + /// goto-cc -c will generate goto-programs without entry-points + /// until they are linked. + void entry_point_exists(); + + /// 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 + /// . + /// a corresponding entry exists in the function_map + /// + /// Functions that are only declared and not used will not appear in the + /// function map. Functions that are declared only and used to e.g. + /// initialise a function pointer will have no body. + void check_called_functions(); + + const validation_modet vm; + const function_mapt &function_map; +}; + +validate_goto_modelt::validate_goto_modelt( + const goto_functionst &goto_functions, + const validation_modet vm, + const goto_model_validation_optionst validation_options) + : vm{vm}, function_map{goto_functions.function_map} +{ + 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) + { + function_pointer_calls_removed(); + } + + if(validation_options.check_returns_removed) + check_returns_removed(); + + if(validation_options.check_called_functions) + check_called_functions(); +} + +void validate_goto_modelt::entry_point_exists() +{ + DATA_CHECK( + vm, + function_map.find(goto_functionst::entry_point()) != function_map.end(), + "an entry point must exist"); +} + +void validate_goto_modelt::function_pointer_calls_removed() +{ + for(const auto &fun : function_map) + { + for(const auto &instr : fun.second.body.instructions) + { + if(instr.is_function_call()) + { + const code_function_callt &function_call = instr.get_function_call(); + DATA_CHECK( + vm, + function_call.function().id() == ID_symbol, + "no calls via function pointer should be present"); + } + } + } +} + +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_return(), "no return instructions should be present"); + + if(instr.is_function_call()) + { + const auto &function_call = instr.get_function_call(); + DATA_CHECK( + vm, + function_call.lhs().is_nil(), + "function call return should be nil"); + + const auto &callee = to_code_type(function_call.function().type()); + DATA_CHECK( + vm, + callee.return_type().id() == ID_empty, + "called function must have empty return type"); + } + } + } +} + +void validate_goto_modelt::check_called_functions() +{ + class test_for_function_addresst : public const_expr_visitort + { + public: + test_for_function_addresst( + const function_mapt &function_map, + const validation_modet &vm) + : function_map{function_map}, vm{vm} + { + } + + void operator()(const exprt &expr) override + { + if(expr.id() == ID_address_of) + { + const auto &pointee = to_address_of_expr(expr).object(); + + if(pointee.id() == ID_symbol && pointee.type().id() == ID_code) + { + const auto &identifier = to_symbol_expr(pointee).get_identifier(); + + DATA_CHECK( + vm, + function_map.find(identifier) != function_map.end(), + "every function whose address is taken must be in the " + "function map"); + } + } + } + + private: + const function_mapt &function_map; + const validation_modet &vm; + }; + test_for_function_addresst test_for_function_address(function_map, vm); + + for(const auto &fun : function_map) + { + for(const auto &instr : fun.second.body.instructions) + { + // check functions that are called + if(instr.is_function_call()) + { + const auto &function_call = instr.get_function_call(); + const irep_idt &identifier = + to_symbol_expr(function_call.function()).get_identifier(); + + DATA_CHECK( + vm, + function_map.find(identifier) != function_map.end(), + "every function call callee must be in the function map"); + } + + // check functions of which the address is taken + const auto &src = static_cast(instr.code); + src.visit(test_for_function_address); + } + } +} + +} // namespace + +void validate_goto_model( + const goto_functionst &goto_functions, + const validation_modet vm, + const goto_model_validation_optionst validation_options) +{ + validate_goto_modelt{goto_functions, vm, validation_options}; +} diff --git a/src/goto-programs/validate_goto_model.h b/src/goto-programs/validate_goto_model.h new file mode 100644 index 00000000000..d521bd893f4 --- /dev/null +++ b/src/goto-programs/validate_goto_model.h @@ -0,0 +1,65 @@ +/*******************************************************************\ +Module: Validate Goto Programs + +Author: Diffblue + +Date: Oct 2018 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H +#define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H + +#include + +class goto_model_validation_optionst final +{ +public: + // this check is disabled by default (not all goto programs + // have an entry point) + bool entry_point_exists = false; + + bool function_pointer_calls_removed = true; + bool check_returns_removed = true; + bool check_called_functions = true; + +private: + void set_all_flags(bool options_value) + { + entry_point_exists = options_value; + function_pointer_calls_removed = options_value; + check_returns_removed = options_value; + check_called_functions = options_value; + } + +public: + goto_model_validation_optionst() = default; + + enum class set_optionst + { + all_true, + all_false + }; + + explicit goto_model_validation_optionst(set_optionst flag_option) + { + switch(flag_option) + { + case set_optionst::all_true: + set_all_flags(true); + break; + case set_optionst::all_false: + set_all_flags(false); + break; + } + } +}; + +class goto_functionst; + +void validate_goto_model( + const goto_functionst &goto_functions, + const validation_modet vm, + const goto_model_validation_optionst validation_options); + +#endif // CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H diff --git a/unit/Makefile b/unit/Makefile index 26de90c719b..edcc5199021 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -24,6 +24,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_goto_target.cpp \ goto-programs/goto_program_symbol_type_table_consistency.cpp \ goto-programs/goto_program_table_consistency.cpp \ + goto-programs/goto_program_validate.cpp \ goto-programs/goto_trace_output.cpp \ goto-programs/xml_expr.cpp \ goto-symex/ssa_equation.cpp \ diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index e5ee11fd696..d88e617850c 100644 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include +#include SCENARIO( "Validation of consistent program/table pair (function type)", @@ -34,6 +35,9 @@ SCENARIO( goto_model.goto_functions.function_map[function_symbol.name].type = fun_type1; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + WHEN("Symbol table has the right type") { function_symbol.type = fun_type1; @@ -41,7 +45,7 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate(validation_modet::INVARIANT, validation_options); REQUIRE(true); } @@ -55,7 +59,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_model.validate(validation_modet::EXCEPTION), + goto_model.validate(validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index 19fed687358..48ed91b0521 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -8,10 +8,10 @@ Author: Diffblue Ltd. #include -#include - #include +#include + SCENARIO( "Validation of well-formed declaration codes", "[core][goto-programs][validate]") diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp index dd5081431ad..9487fc5fd5c 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -36,6 +36,12 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_programt::make_assertion(x_le_10)); + // required as goto_function.validate checks (if a function has a body) that + // the last instruction of a function body marks the function's end. + goto_programt::instructiont end_function_instruction = + goto_programt::make_end_function(); + instructions.push_back(end_function_instruction); + symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol type") { diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index 64663a8360b..001d2e44e95 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -35,6 +35,12 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_programt::make_assertion(x_le_10)); + // required as goto_function.validate checks (if a function has a body) that + // the last instruction of a function body marks the function's end. + goto_programt::instructiont end_function_instruction; + end_function_instruction.make_end_function(); + instructions.push_back(end_function_instruction); + symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol") { diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp new file mode 100644 index 00000000000..6e67e6ccdc5 --- /dev/null +++ b/unit/goto-programs/goto_program_validate.cpp @@ -0,0 +1,377 @@ +/*******************************************************************\ + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + Date: Oct 2018 + +\*******************************************************************/ + +/// \file +/// Unit tests for goto program validation + +#include + +#include + +#include +#include +#include +#include + +#include +#include + +SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") +{ + goto_modelt goto_model; + + // void f(){int x = 1;} + symbolt x; + x.name = "x"; + x.mode = ID_C; + x.type = signed_int_type(); + goto_model.symbol_table.add(x); + + symbolt f; + f.name = "f"; + f.mode = ID_C; + f.type = code_typet({}, empty_typet()); // void rtn, take no params + code_blockt f_body{ + {code_declt(x.symbol_expr()), + code_assignt(x.symbol_expr(), from_integer(1, signed_int_type()))}}; + + f.value = f_body; + goto_model.symbol_table.add(f); + + // void g(){int y = 2;} + symbolt y; + y.name = "y"; + y.mode = ID_C; + y.type = signed_int_type(); + goto_model.symbol_table.add(y); + + symbolt g; + g.name = "g"; + g.mode = ID_C; + g.type = code_typet({}, empty_typet()); + + code_blockt g_body{ + {code_declt{y.symbol_expr()}, + code_assignt{y.symbol_expr(), from_integer(2, signed_int_type())}}}; + + g.value = g_body; + goto_model.symbol_table.add(g); + + symbolt z; + z.name = "z"; + z.mode = ID_C; + z.type = signed_int_type(); + goto_model.symbol_table.add(z); + + symbolt fn_ptr; + fn_ptr.name = "fn_ptr"; + fn_ptr.mode = ID_C; + + // pointer to fn call + fn_ptr.type = pointer_typet(code_typet{{}, empty_typet()}, 64); + goto_model.symbol_table.add(fn_ptr); + + symbolt entry_point; + entry_point.name = goto_functionst::entry_point(); + entry_point.mode = ID_C; + entry_point.type = code_typet({}, empty_typet{}); + code_blockt entry_point_body{ + {code_declt{z.symbol_expr()}, + code_assignt{z.symbol_expr(), from_integer(3, signed_int_type())}, + code_assignt{fn_ptr.symbol_expr(), address_of_exprt{f.symbol_expr()}}, + code_function_callt{g.symbol_expr()}}}; + + entry_point.value = entry_point_body; + goto_model.symbol_table.add(entry_point); + + /// check entry_point_exists() + WHEN("the goto program has no entry point") + { + goto_convert(goto_model, null_message_handler); + + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find(goto_functionst::entry_point()); + function_map.erase(it); + + THEN("fail!") + { + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.entry_point_exists = true; + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN("the goto program has an entry point") + { + goto_convert(goto_model, null_message_handler); + THEN("pass!") + { + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.entry_point_exists = true; + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); + } + } + + /// check function_pointer_calls_removed() + WHEN("not all function calls via fn pointer have been removed") + { + THEN("fail!") + { + // introduce function k that has a function pointer call; + symbolt k; + k.name = "k"; + k.mode = ID_C; + k.type = code_typet({}, empty_typet{}); // void return, take no params + + code_function_callt function_call{ + dereference_exprt{fn_ptr.symbol_expr(), + pointer_typet(code_typet{{}, empty_typet{}}, 64)}}; + + code_blockt k_body{{function_call}}; + k.value = k_body; + + goto_model.symbol_table.add(k); + goto_convert(goto_model, null_message_handler); + + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.function_pointer_calls_removed = true; + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN("all function calls via fn pointer have been removed") + { + THEN("pass!") + { + goto_convert(goto_model, null_message_handler); + + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.function_pointer_calls_removed = true; + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); + } + } + + /// check_returns_removed() + WHEN( + "not all returns have been removed - an instruction is of type " + "'return'") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + + goto_programt::instructiont instruction; + instruction.make_return(); + + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find("g"); + auto &instructions = it->second.body.instructions; + instructions.insert(instructions.begin(), instruction); + + 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("not all returns have been removed - a function call lhs is not nil") + { + symbolt h; + h.name = "h"; + h.mode = ID_C; + h.type = code_typet({}, empty_typet{}); + 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!") + { + 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_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); + } + } + + /// check_called_functions() + WHEN("not every function call is in the function map") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + + auto &function_map = goto_model.goto_functions.function_map; + // the entry point has a call to g() + auto it = function_map.find("g"); + function_map.erase(it); + + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.check_called_functions = true; + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN("not every function whose address is taken is in the function map") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + // the address of f is taken in the entry point function + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find("f"); + function_map.erase(it); // f is no longer in function map + + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.check_called_functions = true; + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN( + "all functions calls and that of every function whose address is " + "taken are in the function map") + { + THEN("true!") + { + goto_convert(goto_model, null_message_handler); + + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + validation_options.check_called_functions = true; + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); + } + } + + /// check_last_instruction() + WHEN("the last instruction of a function is not an end function") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + auto &function_f = goto_model.goto_functions.function_map["f"]; + function_f.body.instructions.erase( + std::prev(function_f.body.instructions.end())); + + namespacet ns(goto_model.symbol_table); + + REQUIRE_THROWS_AS( + function_f.validate(ns, validation_modet::EXCEPTION), + incorrect_goto_program_exceptiont); + } + } + + WHEN("the last instruction of a function is always an end function") + { + THEN("pass!") + { + goto_convert(goto_model, null_message_handler); + auto &function_f = goto_model.goto_functions.function_map["f"]; + + namespacet ns(goto_model.symbol_table); + + REQUIRE_NOTHROW(function_f.validate(ns, validation_modet::EXCEPTION)); + } + } +}