From 5fddbcdcd1a47153ba5beb2e05bf0b669d19d331 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Wed, 21 Nov 2018 09:37:56 +0000 Subject: [PATCH 01/13] Validation checks for Goto Programs There are several checks, implemented with separate methods, and some flagged as optional. NB use of validate_goto_model(*this, vm) in goto_functions.h is to avoid circular inclusion as function_mapt is a nested type and so cannot be forward declared. --- src/cbmc/cbmc_parse_options.cpp | 23 +- .../goto_analyzer_parse_options.cpp | 4 +- .../goto_instrument_parse_options.cpp | 33 +- src/goto-programs/Makefile | 1 + src/goto-programs/goto_functions.h | 7 +- src/goto-programs/goto_model.h | 6 +- src/goto-programs/initialize_goto_model.cpp | 3 +- src/goto-programs/validate_goto_model.cpp | 251 ++++++++++ src/goto-programs/validate_goto_model.h | 62 +++ unit/Makefile | 1 + unit/goto-programs/goto_program_validate.cpp | 429 ++++++++++++++++++ 11 files changed, 793 insertions(+), 27 deletions(-) create mode 100644 src/goto-programs/validate_goto_model.cpp create mode 100644 src/goto-programs/validate_goto_model.h create mode 100644 unit/goto-programs/goto_program_validate.cpp diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 43b24793e1f..55e1d1675ae 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -46,6 +46,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include +#include +#include #include #include #include @@ -53,24 +57,23 @@ 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 @@ -550,7 +553,13 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model_validation_optionst goto_model_validation_options; + goto_model_validation_options.function_pointer_calls_removed = true; + goto_model_validation_options.check_returns_removed = true; + goto_model_validation_options.check_called_functions = true; + goto_model_validation_options.check_last_instruction = true; + goto_model.validate( + validation_modet::INVARIANT, goto_model_validation_options); } if( diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 68266c0fe8d..5c05391c6e7 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,8 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate( + validation_modet::INVARIANT, goto_model_validation_optionst{}); } // show it? diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 840b395ad9a..4b45a25cf4e 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 @@ -134,7 +135,8 @@ int goto_instrument_parse_optionst::doit() if(validate_only || cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::EXCEPTION); + goto_model.validate( + validation_modet::EXCEPTION, goto_model_validation_optionst{}); if(validate_only) { @@ -147,7 +149,8 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate( + validation_modet::INVARIANT, goto_model_validation_optionst{}); } { 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/goto_functions.h b/src/goto-programs/goto_functions.h index 4cc922ec5bf..3ec0f23d8a5 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -16,6 +16,7 @@ Date: June 2003 #include "goto_function.h" +#include "validate_goto_model.h" #include /// A collection of goto functions @@ -111,8 +112,12 @@ class goto_functionst /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const namespacet &ns, const validation_modet vm) const + void validate( + const namespacet &ns, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) const { + validate_goto_model(*this, vm, goto_model_validation_options); for(const auto &entry : function_map) { const goto_functiont &goto_function = entry.second; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index a640dc5885f..5dc3dcc0268 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -94,12 +94,14 @@ 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, + const goto_model_validation_optionst &goto_model_validation_options) const override { symbol_table.validate(vm); const namespacet ns(symbol_table); - goto_functions.validate(ns, vm); + goto_functions.validate(ns, vm, goto_model_validation_options); } }; diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index bda9c4cf3a0..80565fb688a 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -194,7 +194,8 @@ goto_modelt initialize_goto_model( if(options.is_set("validate-goto-model")) { - goto_model.validate(validation_modet::EXCEPTION); + goto_model.validate( + validation_modet::EXCEPTION, goto_model_validation_optionst{}); } // stupid hack diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp new file mode 100644 index 00000000000..a855ea10ba7 --- /dev/null +++ b/src/goto-programs/validate_goto_model.cpp @@ -0,0 +1,251 @@ +/*******************************************************************\ + +Module: Validate Goto Programs + +Author: Diffblue + +Date: Oct 2018 + +\*******************************************************************/ +#include "validate_goto_model.h" + +#include + +#include "goto_functions.h" +#include + +class validate_goto_modelt +{ +public: + using function_mapt = goto_functionst::function_mapt; + + validate_goto_modelt( + const goto_functionst &goto_functions, + const validation_modet vm) + : vm{vm}, function_map{goto_functions.function_map} + { + } + + void + do_goto_program_checks(goto_model_validation_optionst validation_options); + +private: + /// Check the goto_program has an entry point + /// + /// NB goto-cc -c will generate goto-programs without entry-points + /// until they are linked. + void entry_point_exists(); + + /// Check that no functions calls via function pointer are present + void function_pointer_calls_removed(); + + /// Check returns have been removed + /// + /// NB Calls via function pointer must have been removed already when + /// removing returns, thus enabling this check also should enable 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 + /// 1. functions that are called or + /// 2. functions of which the address is taken, + /// a corresponding entry exists in the function_map + void check_called_functions(); + + /// Check that goto-programs that have a body end with an END_FUNCTION + /// instruction. + /// + /// NB 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_last_instruction(); + + /// Check both + /// 1. every instruction \"code\" field, has a non nil source location" + /// 2. every instruction source_location field is nil + /// NB this check is not expected to pass until setting these locations is + /// patched up. + void check_sourcecode_location(); + + const validation_modet vm; + const function_mapt &function_map; + const goto_model_validation_optionst validation_options; +}; + +void validate_goto_modelt::do_goto_program_checks( + goto_model_validation_optionst validation_options) +{ + if(validation_options.entry_point_exists) + entry_point_exists(); + + if(validation_options.check_last_instruction) + check_last_instruction(); + + /// 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(); + + if(validation_options.check_sourcecode_location) + check_sourcecode_location(); +} + +void validate_goto_modelt::entry_point_exists() +{ + DATA_CHECK( + 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(auto &instr : fun.second.body.instructions) + { + if(instr.is_function_call()) + { + const code_function_callt &function_call = + to_code_function_call(instr.code); + DATA_CHECK( + 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; + DATA_CHECK( + goto_function.type.return_type().id() == ID_empty, + "functions must have empty return type"); + + for(const auto &instr : goto_function.body.instructions) + { + DATA_CHECK( + !instr.is_return(), "no return instructions should be present"); + + if(instr.is_function_call()) + { + const auto &function_call = to_code_function_call(instr.code); + DATA_CHECK( + function_call.lhs().is_nil(), "function call return should be nil"); + + const auto &callee = to_code_type(function_call.function().type()); + DATA_CHECK(callee.return_type().id() == ID_empty, ""); + } + } + } +} + +void validate_goto_modelt::check_called_functions() +{ + class test_for_function_addresst : public const_expr_visitort + { + public: + std::set identifiers; + + void operator()(const exprt &expr) override + { + if(expr.id() == ID_address_of) + { + const exprt &pointee = to_address_of_expr(expr).object(); + if(pointee.id() == ID_symbol) + identifiers.insert(to_symbol_expr(pointee).get_identifier()); + } + } + + void clear() + { + identifiers.clear(); + } + } test_for_function_address; + + for(const auto &fun : function_map) + { + for(auto &instr : fun.second.body.instructions) + { + if(instr.is_function_call()) + { + const auto &function_call = to_code_function_call(instr.code); + const irep_idt &identifier = + to_symbol_expr(function_call.function()).get_identifier(); + + DATA_CHECK( + function_map.find(identifier) != function_map.end(), + "every function call callee must be in the function map"); + } + + const exprt &src{instr.code}; + src.visit(test_for_function_address); + if(!test_for_function_address.identifiers.empty()) + { + for(auto &identifier : test_for_function_address.identifiers) + DATA_CHECK( + function_map.find(identifier) != function_map.end(), + "every function whose address is taken must be in the " + "function map"); + } + test_for_function_address.clear(); + } + } +} + +void validate_goto_modelt::check_last_instruction() +{ + for(const auto &fun : function_map) + { + if(fun.second.body_available()) + { + DATA_CHECK( + fun.second.body.instructions.back().is_end_function(), + "last instruction should be of end function type"); + } + } +} + +void validate_goto_modelt::check_sourcecode_location() +{ + // Assumption is that if every instruction is checked - then there is no + // need to check targets. + for(const auto &fun : function_map) + { + for(auto &instr : fun.second.body.instructions) + { + DATA_CHECK( + instr.code.source_location().is_not_nil(), + "each instruction \"code\" field, must have non nil source location"); + + DATA_CHECK( + instr.source_location.is_not_nil(), + "each instruction source location must not be nil"); + } + } +} + +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}.do_goto_program_checks( + 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..828346e5069 --- /dev/null +++ b/src/goto-programs/validate_goto_model.h @@ -0,0 +1,62 @@ +/*******************************************************************\ + +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 + +struct goto_model_validation_optionst +{ + bool entry_point_exists; + bool function_pointer_calls_removed; + bool check_returns_removed; + bool check_called_functions; + bool check_last_instruction; + bool check_sourcecode_location; + + goto_model_validation_optionst() + : entry_point_exists{true}, + function_pointer_calls_removed{false}, + check_returns_removed{false}, + check_called_functions{false}, + check_last_instruction{false}, + check_sourcecode_location{false} + { + } + + void disable_all_checks() + { + entry_point_exists = false; + function_pointer_calls_removed = false; + check_returns_removed = false; + check_called_functions = false; + check_last_instruction = false; + check_sourcecode_location = false; + } + + void enable_all_checks() + { + entry_point_exists = true; + function_pointer_calls_removed = true; + check_returns_removed = true; + check_called_functions = true; + check_last_instruction = true; + check_sourcecode_location = true; + } +}; + +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_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp new file mode 100644 index 00000000000..d0749331091 --- /dev/null +++ b/unit/goto-programs/goto_program_validate.cpp @@ -0,0 +1,429 @@ +/*******************************************************************\ + + Module: Unit tests for goto program validation + + Author: Diffblue Ltd. + + Date: Oct 2018 + +\*******************************************************************/ + +/// \file +/// Unit tests for goto program validation + +#include +#include + +#include +#include + +#include +#include +#include +#include + +namespace +{ +code_function_callt make_void_call(const symbol_exprt &function) +{ + code_function_callt ret; + ret.function() = function; + return ret; +} + +void validate( + const goto_functionst &goto_functions, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) +{ + validate_goto_model(goto_functions, vm, goto_model_validation_options); +} + +bool test_for_pass( + goto_modelt &goto_model, + const goto_model_validation_optionst goto_model_validation_options) +{ + validate( + goto_model.goto_functions, + validation_modet::INVARIANT, + goto_model_validation_options); + return true; +} + +bool test_for_failure( + goto_modelt &goto_model, + const goto_model_validation_optionst goto_model_validation_options) +{ + bool caught{false}; + try + { + validate( + goto_model.goto_functions, + validation_modet::EXCEPTION, + goto_model_validation_options); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + return caught; +} +} // namespace + +SCENARIO("validate goto program") +{ + 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; + f_body.copy_to_operands(code_declt(x.symbol_expr())); + f_body.copy_to_operands( + 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; + g_body.copy_to_operands(code_declt(y.symbol_expr())); + g_body.copy_to_operands( + 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({}, void_typet()); + + code_blockt entry_point_body; + entry_point_body.copy_to_operands(code_declt(z.symbol_expr())); + entry_point_body.copy_to_operands( + code_assignt(z.symbol_expr(), from_integer(3, signed_int_type()))); + + entry_point_body.copy_to_operands( + code_assignt(fn_ptr.symbol_expr(), address_of_exprt{f.symbol_expr()})); + entry_point_body.copy_to_operands(make_void_call(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; + validation_options.disable_all_checks(); + validation_options.entry_point_exists = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + WHEN("the goto program has an entry point") + { + goto_convert(goto_model, null_message_handler); + THEN("pass!") + { + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.entry_point_exists = true; + REQUIRE(test_for_pass(goto_model, 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; + function_call.function() = dereference_exprt( + fn_ptr.symbol_expr(), pointer_typet(code_typet{{}, empty_typet()}, 64)); + + code_blockt k_body; + k_body.copy_to_operands(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; + validation_options.disable_all_checks(); + validation_options.function_pointer_calls_removed = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + 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; + validation_options.disable_all_checks(); + validation_options.function_pointer_calls_removed = true; + REQUIRE(test_for_pass(goto_model, validation_options)); + } + } + + /// check_returns_removed() + WHEN( + "not all returns have been removed - a function has return type " + "non-empty") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find("f"); + it->second.type.return_type() = signedbv_typet{32}; + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_returns_removed = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + 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(); + instruction.function = "g"; // if this is not set will fail id test + + 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; + validation_options.disable_all_checks(); + validation_options.check_returns_removed = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + 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({}, void_typet{}); + h.value = code_blockt{}; + goto_model.symbol_table.add(h); + + symbolt k; + k.name = "k"; + k.mode = ID_C; + k.type = code_typet({}, empty_typet()); + code_blockt k_body; + + // the lhs is non-nil + code_function_callt function_call{from_integer(1, signed_int_type()), + h.symbol_expr(), + code_function_callt::argumentst{}}; + + k_body.copy_to_operands(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; + validation_options.disable_all_checks(); + validation_options.check_returns_removed = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + WHEN("all returns have been removed") + { + THEN("true!") + { + goto_convert(goto_model, null_message_handler); + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_returns_removed = true; + REQUIRE(test_for_pass(goto_model, 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; + validation_options.disable_all_checks(); + validation_options.check_called_functions = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + 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; + validation_options.disable_all_checks(); + validation_options.check_called_functions = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + 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; + validation_options.disable_all_checks(); + validation_options.check_called_functions = true; + REQUIRE(test_for_pass(goto_model, 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_map = goto_model.goto_functions.function_map; + auto it = function_map.find("f"); + it->second.body.instructions.erase( + std::prev(it->second.body.instructions.end())); + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_last_instruction = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + WHEN("the last instruction of a function is always an end function") + { + THEN("pass!") + { + goto_convert(goto_model, null_message_handler); + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_last_instruction = true; + REQUIRE(test_for_pass(goto_model, validation_options)); + } + } + + WHEN("an instruction \"code\" field, has a non nil source location") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find("f"); + + auto source_location = + it->second.body.instructions.front().code.source_location(); + source_location.make_nil(); + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_sourcecode_location = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } + + WHEN("an instruction source_location field is nil") + { + THEN("fail!") + { + goto_convert(goto_model, null_message_handler); + auto &function_map = goto_model.goto_functions.function_map; + auto it = function_map.find("f"); + + auto source_location = + it->second.body.instructions.front().source_location; + source_location.make_nil(); + + goto_model_validation_optionst validation_options; + validation_options.disable_all_checks(); + validation_options.check_sourcecode_location = true; + REQUIRE(test_for_failure(goto_model, validation_options)); + } + } +} From 8bd353cceb98a4e95d8f4a685817a66e30254054 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Sun, 16 Dec 2018 11:58:35 +0000 Subject: [PATCH 02/13] Use unnamed namespace for validate_goto_modelt The overall pattern here is a global function that instantiates a utility class for a specific purpose (not a general utility class). This clarifies that separation of concerns. Class 'validate_goto_modelt' does not need to be globally visible. --- src/goto-programs/validate_goto_model.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index a855ea10ba7..18a61793c0e 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -14,6 +14,8 @@ Date: Oct 2018 #include "goto_functions.h" #include +namespace +{ class validate_goto_modelt { public: @@ -76,6 +78,7 @@ class validate_goto_modelt const function_mapt &function_map; const goto_model_validation_optionst validation_options; }; +} // namespace void validate_goto_modelt::do_goto_program_checks( goto_model_validation_optionst validation_options) From 2ec4b8364ffce2e96a3bf9330147f8645ca03945 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Sun, 16 Dec 2018 11:49:01 +0000 Subject: [PATCH 03/13] Add additional 'vm' argument to DATA_CHECK --- src/goto-programs/validate_goto_model.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 18a61793c0e..d9f8db2ce84 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -110,6 +110,7 @@ void validate_goto_modelt::do_goto_program_checks( 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"); } @@ -125,6 +126,7 @@ void validate_goto_modelt::function_pointer_calls_removed() const code_function_callt &function_call = to_code_function_call(instr.code); DATA_CHECK( + vm, function_call.function().id() == ID_symbol, "no calls via function pointer should be present"); } @@ -138,22 +140,25 @@ void validate_goto_modelt::check_returns_removed() { const goto_functiont &goto_function = fun.second; DATA_CHECK( + vm, goto_function.type.return_type().id() == ID_empty, "functions must have empty return type"); for(const auto &instr : goto_function.body.instructions) { DATA_CHECK( - !instr.is_return(), "no return instructions should be present"); + vm, !instr.is_return(), "no return instructions should be present"); if(instr.is_function_call()) { const auto &function_call = to_code_function_call(instr.code); DATA_CHECK( - function_call.lhs().is_nil(), "function call return should be nil"); + vm, + function_call.lhs().is_nil(), + "function call return should be nil"); const auto &callee = to_code_type(function_call.function().type()); - DATA_CHECK(callee.return_type().id() == ID_empty, ""); + DATA_CHECK(vm, callee.return_type().id() == ID_empty, ""); } } } @@ -193,6 +198,7 @@ void validate_goto_modelt::check_called_functions() 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"); } @@ -203,6 +209,7 @@ void validate_goto_modelt::check_called_functions() { for(auto &identifier : test_for_function_address.identifiers) DATA_CHECK( + vm, function_map.find(identifier) != function_map.end(), "every function whose address is taken must be in the " "function map"); @@ -219,6 +226,7 @@ void validate_goto_modelt::check_last_instruction() if(fun.second.body_available()) { DATA_CHECK( + vm, fun.second.body.instructions.back().is_end_function(), "last instruction should be of end function type"); } @@ -234,10 +242,12 @@ void validate_goto_modelt::check_sourcecode_location() for(auto &instr : fun.second.body.instructions) { DATA_CHECK( + vm, instr.code.source_location().is_not_nil(), "each instruction \"code\" field, must have non nil source location"); DATA_CHECK( + vm, instr.source_location.is_not_nil(), "each instruction source location must not be nil"); } From 4cd976f983a0b01bdd98fd661298ce2ecd3af0c0 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Tue, 18 Dec 2018 16:33:34 +0000 Subject: [PATCH 04/13] Improved function call check --- src/goto-programs/validate_goto_model.cpp | 41 ++++++++++++----------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index d9f8db2ce84..48f001f28ec 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -169,28 +169,40 @@ void validate_goto_modelt::check_called_functions() class test_for_function_addresst : public const_expr_visitort { public: - std::set identifiers; - + 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 exprt &pointee = to_address_of_expr(expr).object(); + const auto &pointee = to_address_of_expr(expr).object(); if(pointee.id() == ID_symbol) - identifiers.insert(to_symbol_expr(pointee).get_identifier()); + { + 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"); + } } } - void clear() - { - identifiers.clear(); - } - } test_for_function_address; + 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(auto &instr : fun.second.body.instructions) { + // check functions that are called if(instr.is_function_call()) { const auto &function_call = to_code_function_call(instr.code); @@ -203,18 +215,9 @@ void validate_goto_modelt::check_called_functions() "every function call callee must be in the function map"); } + // check functions of which the address is taken const exprt &src{instr.code}; src.visit(test_for_function_address); - if(!test_for_function_address.identifiers.empty()) - { - for(auto &identifier : test_for_function_address.identifiers) - DATA_CHECK( - vm, - function_map.find(identifier) != function_map.end(), - "every function whose address is taken must be in the " - "function map"); - } - test_for_function_address.clear(); } } } From a3b55130ff023fdbb4e055e5fdb5b47fba50240f Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Tue, 18 Dec 2018 16:34:00 +0000 Subject: [PATCH 05/13] Use catch exception macros --- unit/goto-programs/goto_program_validate.cpp | 163 +++++++++---------- 1 file changed, 80 insertions(+), 83 deletions(-) diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index d0749331091..2363f7f3af1 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -30,44 +30,6 @@ code_function_callt make_void_call(const symbol_exprt &function) ret.function() = function; return ret; } - -void validate( - const goto_functionst &goto_functions, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) -{ - validate_goto_model(goto_functions, vm, goto_model_validation_options); -} - -bool test_for_pass( - goto_modelt &goto_model, - const goto_model_validation_optionst goto_model_validation_options) -{ - validate( - goto_model.goto_functions, - validation_modet::INVARIANT, - goto_model_validation_options); - return true; -} - -bool test_for_failure( - goto_modelt &goto_model, - const goto_model_validation_optionst goto_model_validation_options) -{ - bool caught{false}; - try - { - validate( - goto_model.goto_functions, - validation_modet::EXCEPTION, - goto_model_validation_options); - } - catch(incorrect_goto_program_exceptiont &e) - { - caught = true; - } - return caught; -} } // namespace SCENARIO("validate goto program") @@ -153,10 +115,13 @@ SCENARIO("validate goto program") THEN("fail!") { - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.entry_point_exists = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -165,10 +130,11 @@ SCENARIO("validate goto program") goto_convert(goto_model, null_message_handler); THEN("pass!") { - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.entry_point_exists = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -195,10 +161,13 @@ SCENARIO("validate goto program") goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.function_pointer_calls_removed = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -208,10 +177,11 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.function_pointer_calls_removed = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -228,10 +198,13 @@ SCENARIO("validate goto program") auto it = function_map.find("f"); it->second.type.return_type() = signedbv_typet{32}; - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_returns_removed = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -252,10 +225,13 @@ SCENARIO("validate goto program") auto &instructions = it->second.body.instructions; instructions.insert(instructions.begin(), instruction); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_returns_removed = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -287,10 +263,13 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_returns_removed = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -300,10 +279,11 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_returns_removed = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -319,10 +299,13 @@ SCENARIO("validate goto program") auto it = function_map.find("g"); function_map.erase(it); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_called_functions = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -336,10 +319,13 @@ SCENARIO("validate goto program") auto it = function_map.find("f"); function_map.erase(it); // f is no longer in function map - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_called_functions = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -351,10 +337,11 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_called_functions = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -369,10 +356,13 @@ SCENARIO("validate goto program") it->second.body.instructions.erase( std::prev(it->second.body.instructions.end())); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_last_instruction = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -382,10 +372,11 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_last_instruction = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -401,10 +392,13 @@ SCENARIO("validate goto program") it->second.body.instructions.front().code.source_location(); source_location.make_nil(); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_sourcecode_location = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -420,10 +414,13 @@ SCENARIO("validate goto program") it->second.body.instructions.front().source_location; source_location.make_nil(); - goto_model_validation_optionst validation_options; - validation_options.disable_all_checks(); validation_options.check_sourcecode_location = true; - REQUIRE(test_for_failure(goto_model, validation_options)); + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } } From 6cc09c9d4b8e72a568777c4cd9f0bd47dade8595 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Tue, 18 Dec 2018 20:16:32 +0000 Subject: [PATCH 06/13] Add boolean constructor to options structure --- src/goto-programs/validate_goto_model.h | 24 ++++++-------------- unit/goto-programs/goto_program_validate.cpp | 15 ++++++++++++ 2 files changed, 22 insertions(+), 17 deletions(-) diff --git a/src/goto-programs/validate_goto_model.h b/src/goto-programs/validate_goto_model.h index 828346e5069..92e635dfe3d 100644 --- a/src/goto-programs/validate_goto_model.h +++ b/src/goto-programs/validate_goto_model.h @@ -31,24 +31,14 @@ struct goto_model_validation_optionst { } - void disable_all_checks() + goto_model_validation_optionst(bool options_value) + : entry_point_exists{options_value}, + function_pointer_calls_removed{options_value}, + check_returns_removed{options_value}, + check_called_functions{options_value}, + check_last_instruction{options_value}, + check_sourcecode_location{options_value} { - entry_point_exists = false; - function_pointer_calls_removed = false; - check_returns_removed = false; - check_called_functions = false; - check_last_instruction = false; - check_sourcecode_location = false; - } - - void enable_all_checks() - { - entry_point_exists = true; - function_pointer_calls_removed = true; - check_returns_removed = true; - check_called_functions = true; - check_last_instruction = true; - check_sourcecode_location = true; } }; diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 2363f7f3af1..34d415643f2 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -115,6 +115,7 @@ SCENARIO("validate goto program") THEN("fail!") { + goto_model_validation_optionst validation_options{false}; validation_options.entry_point_exists = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -130,6 +131,7 @@ SCENARIO("validate goto program") goto_convert(goto_model, null_message_handler); THEN("pass!") { + goto_model_validation_optionst validation_options{false}; validation_options.entry_point_exists = true; REQUIRE_NOTHROW(validate_goto_model( goto_model.goto_functions, @@ -161,6 +163,7 @@ SCENARIO("validate goto program") goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.function_pointer_calls_removed = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -177,6 +180,7 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.function_pointer_calls_removed = true; REQUIRE_NOTHROW(validate_goto_model( goto_model.goto_functions, @@ -198,6 +202,7 @@ SCENARIO("validate goto program") auto it = function_map.find("f"); it->second.type.return_type() = signedbv_typet{32}; + goto_model_validation_optionst validation_options{false}; validation_options.check_returns_removed = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -225,6 +230,7 @@ SCENARIO("validate goto program") auto &instructions = it->second.body.instructions; instructions.insert(instructions.begin(), instruction); + goto_model_validation_optionst validation_options{false}; validation_options.check_returns_removed = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -263,6 +269,7 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.check_returns_removed = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -279,6 +286,7 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.check_returns_removed = true; REQUIRE_NOTHROW(validate_goto_model( goto_model.goto_functions, @@ -299,6 +307,7 @@ SCENARIO("validate goto program") auto it = function_map.find("g"); function_map.erase(it); + goto_model_validation_optionst validation_options{false}; validation_options.check_called_functions = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -319,6 +328,7 @@ SCENARIO("validate goto program") auto it = function_map.find("f"); function_map.erase(it); // f is no longer in function map + goto_model_validation_optionst validation_options{false}; validation_options.check_called_functions = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -337,6 +347,7 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.check_called_functions = true; REQUIRE_NOTHROW(validate_goto_model( goto_model.goto_functions, @@ -356,6 +367,7 @@ SCENARIO("validate goto program") it->second.body.instructions.erase( std::prev(it->second.body.instructions.end())); + goto_model_validation_optionst validation_options{false}; validation_options.check_last_instruction = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -372,6 +384,7 @@ SCENARIO("validate goto program") { goto_convert(goto_model, null_message_handler); + goto_model_validation_optionst validation_options{false}; validation_options.check_last_instruction = true; REQUIRE_NOTHROW(validate_goto_model( goto_model.goto_functions, @@ -392,6 +405,7 @@ SCENARIO("validate goto program") it->second.body.instructions.front().code.source_location(); source_location.make_nil(); + goto_model_validation_optionst validation_options{false}; validation_options.check_sourcecode_location = true; REQUIRE_THROWS_AS( validate_goto_model( @@ -414,6 +428,7 @@ SCENARIO("validate goto program") it->second.body.instructions.front().source_location; source_location.make_nil(); + goto_model_validation_optionst validation_options{false}; validation_options.check_sourcecode_location = true; REQUIRE_THROWS_AS( validate_goto_model( From ca1116608b2dc36311502fd7ac0e3e4f6aeec92e Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Thu, 20 Dec 2018 12:55:46 +0000 Subject: [PATCH 07/13] Add options structure to unit tests --- .../goto_model_function_type_consistency.cpp | 7 +++++-- unit/goto-programs/goto_program_assume.cpp | 8 ++++++-- unit/goto-programs/goto_program_dead.cpp | 8 ++++++-- unit/goto-programs/goto_program_declaration.cpp | 8 ++++++-- unit/goto-programs/goto_program_function_call.cpp | 8 ++++++-- unit/goto-programs/goto_program_goto_target.cpp | 12 ++++++++---- .../goto_program_symbol_type_table_consistency.cpp | 12 ++++++++---- .../goto-programs/goto_program_table_consistency.cpp | 8 ++++++-- 8 files changed, 51 insertions(+), 20 deletions(-) diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index e5ee11fd696..6f29148d830 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,8 @@ SCENARIO( goto_model.goto_functions.function_map[function_symbol.name].type = fun_type1; + goto_model_validation_optionst validation_options{false}; + WHEN("Symbol table has the right type") { function_symbol.type = fun_type1; @@ -41,7 +44,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 +58,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_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index dc0f1db2d5d..b8705a84261 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include +#include SCENARIO( "Validation of well-formed assert/assume codes", @@ -40,11 +41,14 @@ SCENARIO( namespacet ns(symbol_table); instructions.back() = goto_programt::make_assertion(x_le_10); + goto_model_validation_optionst validation_options; + WHEN("Instruction has no targets") { THEN("The consistency check succeeds") { - goto_function.body.validate(ns, validation_modet::INVARIANT); + goto_function.body.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -55,7 +59,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION), + goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 7b591e892ed..0e8e4d6560c 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include +#include SCENARIO( "Validation of well-formed symbol removing codes", @@ -36,6 +37,8 @@ SCENARIO( instructions.emplace_back(goto_programt::make_dead(var_a)); symbol_table.insert(fun_symbol); + goto_model_validation_optionst validation_options; + WHEN("Removing known symbol") { symbol_table.insert(var_symbol); @@ -43,7 +46,8 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate(ns, validation_modet::INVARIANT); + goto_function.body.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -55,7 +59,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION), + goto_function.body.validate(ns, 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..a1ebd69ed06 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include @@ -36,6 +37,8 @@ SCENARIO( instructions.emplace_back(goto_programt::make_decl(var_a)); symbol_table.insert(fun_symbol); + goto_model_validation_optionst validation_options; + WHEN("Declaring known symbol") { symbol_table.insert(var_symbol); @@ -43,7 +46,8 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate(ns, validation_modet::INVARIANT); + goto_function.body.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -55,7 +59,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION), + goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index cb923f87cbf..76e95fdf6f6 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include +#include SCENARIO( "Validation of well-formed function call codes", @@ -50,6 +51,8 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); + goto_model_validation_optionst validation_options; + WHEN("Return type matches") { code_function_callt function_call(var_a, fun_foo, {}); @@ -58,7 +61,8 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate(ns, validation_modet::INVARIANT); + goto_function.body.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -71,7 +75,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION), + goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index ebc9a571018..45b13193627 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -8,9 +8,10 @@ Author: Diffblue Ltd. #include -#include - #include +#include + +#include SCENARIO( "Validation of well-formed goto codes", @@ -43,12 +44,15 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); + goto_model_validation_optionst validation_options; + WHEN("Target is a target") { instructions.front().target_number = 1; THEN("The consistency check succeeds") { - goto_function.body.validate(ns, validation_modet::INVARIANT); + goto_function.body.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -58,7 +62,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION), + goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } 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..8cc33e30439 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -10,8 +10,9 @@ Author: Diffblue Ltd. #include -#include - +#include +#include + SCENARIO( "Validation of consistent program/table pair (type-wise)", "[core][goto-programs][validate]") @@ -36,6 +37,8 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_programt::make_assertion(x_le_10)); + goto_model_validation_optionst validation_options; + symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol type") { @@ -45,7 +48,8 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.validate(ns, validation_modet::INVARIANT); + goto_function.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } @@ -60,7 +64,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate(ns, validation_modet::EXCEPTION), + goto_function.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index 64663a8360b..25e3699978e 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -11,6 +11,7 @@ Author: Diffblue Ltd. #include #include +#include SCENARIO( "Validation of consistent program/table pair", @@ -35,6 +36,8 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_programt::make_assertion(x_le_10)); + goto_model_validation_optionst validation_options; + symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol") { @@ -43,7 +46,8 @@ SCENARIO( const namespacet ns(symbol_table); THEN("The consistency check succeeds") { - goto_function.validate(ns, validation_modet::INVARIANT); + goto_function.validate( + ns, validation_modet::INVARIANT, validation_options); REQUIRE(true); } } @@ -53,7 +57,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate(ns, validation_modet::EXCEPTION), + goto_function.validate(ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } From ab3cb608d58df811897ef4090cb76051836a7b4a Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Fri, 21 Dec 2018 09:17:32 +0000 Subject: [PATCH 08/13] Adjustments for new location of program checks --- src/cbmc/cbmc_parse_options.cpp | 9 +- src/goto-programs/abstract_goto_model.h | 5 +- src/goto-programs/goto_function.cpp | 18 +- src/goto-programs/goto_function.h | 6 +- src/goto-programs/goto_functions.h | 2 +- src/goto-programs/goto_model.h | 6 +- src/goto-programs/goto_program.cpp | 22 ++- src/goto-programs/goto_program.h | 14 +- src/goto-programs/lazy_goto_model.h | 6 +- src/goto-programs/validate_goto_model.cpp | 62 +------ src/goto-programs/validate_goto_model.h | 9 +- unit/Makefile | 1 + .../goto_model_function_type_consistency.cpp | 5 +- .../goto_program_instruction.cpp | 110 ++++++++++++ ..._program_symbol_type_table_consistency.cpp | 10 ++ .../goto_program_table_consistency.cpp | 7 + unit/goto-programs/goto_program_validate.cpp | 169 ++++++------------ 17 files changed, 259 insertions(+), 202 deletions(-) create mode 100644 unit/goto-programs/goto_program_instruction.cpp diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 55e1d1675ae..c62e5f424f9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -553,11 +553,10 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model_validation_optionst goto_model_validation_options; - goto_model_validation_options.function_pointer_calls_removed = true; - goto_model_validation_options.check_returns_removed = true; - goto_model_validation_options.check_called_functions = true; - goto_model_validation_options.check_last_instruction = true; + goto_model_validation_optionst goto_model_validation_options{true}; + // this option is temporarily disabled until all source locations + // are reliably set correctly + goto_model_validation_options.check_source_location = false; goto_model.validate( validation_modet::INVARIANT, goto_model_validation_options); } diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h index 25243c8f5eb..33b9ea8379a 100644 --- a/src/goto-programs/abstract_goto_model.h +++ b/src/goto-programs/abstract_goto_model.h @@ -54,7 +54,10 @@ 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..e5b182803a0 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -33,10 +33,21 @@ void get_local_identifiers( /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. -void goto_functiont::validate(const namespacet &ns, const validation_modet vm) - const +void goto_functiont::validate( + const namespacet &ns, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) const { - body.validate(ns, vm); + // 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, goto_model_validation_options); find_symbols_sett typetags; find_type_symbols(type, typetags); @@ -61,3 +72,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm) validate_full_type(type, ns, vm); } + diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index 90ef0d7879c..240895fc87b 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -21,6 +21,7 @@ Date: May 2018 #include #include "goto_program.h" +#include "validate_goto_model.h" /// A goto function, consisting of function type (see #type), function body (see /// #body), and parameter identifiers (see #parameter_identifiers). @@ -119,7 +120,10 @@ class goto_functiont /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const namespacet &ns, const validation_modet vm) const; + void validate( + const namespacet &ns, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) const; }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 3ec0f23d8a5..cc0ef26c65c 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -153,7 +153,7 @@ class goto_functionst ++it; } - goto_function.validate(ns, vm); + goto_function.validate(ns, vm, goto_model_validation_options); } } }; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 5dc3dcc0268..d49fa3a42c9 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -144,12 +144,14 @@ 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); const namespacet ns(symbol_table); - goto_functions.validate(ns, vm); + goto_functions.validate(ns, vm, goto_model_validation_options); } private: diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index a26c6096c1c..babf64e1daa 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -674,7 +674,8 @@ bool goto_programt::instructiont::equals(const instructiont &other) const void goto_programt::instructiont::validate( const namespacet &ns, - const validation_modet vm) const + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) const { validate_full_code(code, ns, vm); validate_full_expr(guard, ns, vm); @@ -776,6 +777,25 @@ void goto_programt::instructiont::validate( } }; + if(goto_model_validation_options.check_source_location) + { + DATA_CHECK( + vm, + source_location.is_not_nil(), + "each instruction source location must not be nil"); + + DATA_CHECK( + vm, + code.source_location().is_not_nil(), + "each instruction \"code\" field, must have non nil source location"); + + DATA_CHECK( + vm, + source_location == code.source_location(), + "instruction source location and" + " instruction \"code\" field source location must be the same"); + } + const symbolt *table_symbol; switch(type) { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 71f73fe050a..3ae3ab5aaa1 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "validate_goto_model.h" #include #include #include @@ -554,7 +555,11 @@ class goto_programt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const namespacet &ns, const validation_modet vm) const; + void validate( + const namespacet &ns, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) + const; /// Apply given transformer to all expressions; no return value /// means no change needed. @@ -814,11 +819,14 @@ class goto_programt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate(const namespacet &ns, const validation_modet vm) const + void validate( + const namespacet &ns, + const validation_modet vm, + const goto_model_validation_optionst &goto_model_validation_options) const { for(const instructiont &ins : instructions) { - ins.validate(ns, vm); + ins.validate(ns, vm, goto_model_validation_options); } } diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index d62b477c838..39e9392469b 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -247,9 +247,11 @@ 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, + const goto_model_validation_optionst &goto_model_validation_options) 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 index 48f001f28ec..dc70d55bd1e 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -59,24 +59,8 @@ class validate_goto_modelt /// a corresponding entry exists in the function_map void check_called_functions(); - /// Check that goto-programs that have a body end with an END_FUNCTION - /// instruction. - /// - /// NB 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_last_instruction(); - - /// Check both - /// 1. every instruction \"code\" field, has a non nil source location" - /// 2. every instruction source_location field is nil - /// NB this check is not expected to pass until setting these locations is - /// patched up. - void check_sourcecode_location(); - const validation_modet vm; const function_mapt &function_map; - const goto_model_validation_optionst validation_options; }; } // namespace @@ -86,9 +70,6 @@ void validate_goto_modelt::do_goto_program_checks( if(validation_options.entry_point_exists) entry_point_exists(); - if(validation_options.check_last_instruction) - check_last_instruction(); - /// NB function pointer calls must have been removed before removing /// returns - so 'check_returns_removed' also enables // 'function_pointer_calls_removed' @@ -102,9 +83,6 @@ void validate_goto_modelt::do_goto_program_checks( if(validation_options.check_called_functions) check_called_functions(); - - if(validation_options.check_sourcecode_location) - check_sourcecode_location(); } void validate_goto_modelt::entry_point_exists() @@ -158,7 +136,10 @@ void validate_goto_modelt::check_returns_removed() "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, ""); + DATA_CHECK( + vm, + callee.return_type().id() == ID_empty, + "called function must have empty return type"); } } } @@ -222,41 +203,6 @@ void validate_goto_modelt::check_called_functions() } } -void validate_goto_modelt::check_last_instruction() -{ - for(const auto &fun : function_map) - { - if(fun.second.body_available()) - { - DATA_CHECK( - vm, - fun.second.body.instructions.back().is_end_function(), - "last instruction should be of end function type"); - } - } -} - -void validate_goto_modelt::check_sourcecode_location() -{ - // Assumption is that if every instruction is checked - then there is no - // need to check targets. - for(const auto &fun : function_map) - { - for(auto &instr : fun.second.body.instructions) - { - DATA_CHECK( - vm, - instr.code.source_location().is_not_nil(), - "each instruction \"code\" field, must have non nil source location"); - - DATA_CHECK( - vm, - instr.source_location.is_not_nil(), - "each instruction source location must not be nil"); - } - } -} - void validate_goto_model( const goto_functionst &goto_functions, const validation_modet vm, diff --git a/src/goto-programs/validate_goto_model.h b/src/goto-programs/validate_goto_model.h index 92e635dfe3d..0e0e31be515 100644 --- a/src/goto-programs/validate_goto_model.h +++ b/src/goto-programs/validate_goto_model.h @@ -18,16 +18,14 @@ struct goto_model_validation_optionst bool function_pointer_calls_removed; bool check_returns_removed; bool check_called_functions; - bool check_last_instruction; - bool check_sourcecode_location; + bool check_source_location; goto_model_validation_optionst() : entry_point_exists{true}, function_pointer_calls_removed{false}, check_returns_removed{false}, check_called_functions{false}, - check_last_instruction{false}, - check_sourcecode_location{false} + check_source_location{false} { } @@ -36,8 +34,7 @@ struct goto_model_validation_optionst function_pointer_calls_removed{options_value}, check_returns_removed{options_value}, check_called_functions{options_value}, - check_last_instruction{options_value}, - check_sourcecode_location{options_value} + check_source_location{options_value} { } }; diff --git a/unit/Makefile b/unit/Makefile index edcc5199021..c9025f9a32c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -22,6 +22,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_declaration.cpp \ goto-programs/goto_program_function_call.cpp \ goto-programs/goto_program_goto_target.cpp \ + goto-programs/goto_program_instruction.cpp \ goto-programs/goto_program_symbol_type_table_consistency.cpp \ goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_program_validate.cpp \ diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index 6f29148d830..beb33aa56d7 100644 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -35,7 +35,10 @@ SCENARIO( goto_model.goto_functions.function_map[function_symbol.name].type = fun_type1; - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options; + // required as this test has no entry point, but calls the top-level + // 'goto_model.validate()' + validation_options.entry_point_exists = false; WHEN("Symbol table has the right type") { diff --git a/unit/goto-programs/goto_program_instruction.cpp b/unit/goto-programs/goto_program_instruction.cpp new file mode 100644 index 00000000000..2424c3eb967 --- /dev/null +++ b/unit/goto-programs/goto_program_instruction.cpp @@ -0,0 +1,110 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include +#include + +#include +#include + +SCENARIO( + "Validation of well-formed instruction", + "[core][goto-programs][validate]") +{ + GIVEN("A function with one instruction") + { + symbol_tablet symbol_table; + symbolt fun_symbol; + irep_idt fun_name = "foo"; + fun_symbol.name = fun_name; + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + + goto_programt::instructiont instruction; + instruction.make_end_function(); + instructions.push_back(instruction); + instructions.back().function = fun_name; // if not set will fail id test + instructions.back().source_location.id("id_any_valid_id"); + + codet instruction_code_field; + static_cast(instruction_code_field) + .add_source_location() + .id("id_any_valid_id"); + instructions.back().code = instruction_code_field; + + symbol_table.insert(fun_symbol); + namespacet ns(symbol_table); + + WHEN("the source locations are set and identical") + { + goto_model_validation_optionst validation_options{false}; + validation_options.check_source_location = true; + + THEN("The consistency check succeeds") + { + REQUIRE_NOTHROW(goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options)); + } + } + + WHEN("the source location is not set") + { + instructions.back().source_location.make_nil(); + + goto_model_validation_optionst validation_options{false}; + validation_options.check_source_location = true; + + THEN("The consistency check fails") + { + REQUIRE_THROWS_AS( + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN("the 'code' source location is not set") + { + auto &expr = static_cast(instructions.back().code); + expr.add_source_location().make_nil(); + + goto_model_validation_optionst validation_options{false}; + validation_options.check_source_location = true; + + THEN("The consistency check fails") + { + REQUIRE_THROWS_AS( + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), + incorrect_goto_program_exceptiont); + } + } + + WHEN("the source locations are not the same") + { + instructions.back().source_location.id("id_any_valid_id_1"); + + auto &expr = static_cast(instructions.back().code); + expr.add_source_location().id("id_any_valid_id_2"); + + goto_model_validation_optionst validation_options{false}; + validation_options.check_source_location = true; + + THEN("The consistency check fails") + { + REQUIRE_THROWS_AS( + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), + incorrect_goto_program_exceptiont); + } + } + } +} 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 8cc33e30439..51b02d80fbf 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -37,7 +37,17 @@ 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); + instructions.back().function = function_symbol.name; + goto_model_validation_optionst validation_options; + // required as this test has no entry point, but calls the top-level + // 'goto_model.validate()' + validation_options.entry_point_exists = false; 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 25e3699978e..c4c860e921a 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -36,6 +36,13 @@ 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); + instructions.back().function = function_symbol.name; + goto_model_validation_optionst validation_options; symbol_table.insert(function_symbol); diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 34d415643f2..7ef1f9b4e7e 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -30,9 +30,33 @@ code_function_callt make_void_call(const symbol_exprt &function) ret.function() = function; return ret; } + +bool test_for_fail( + goto_modelt &goto_model, + goto_model_validation_optionst &validation_options) +{ + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); + return true; +} + +bool test_for_pass( + goto_modelt &goto_model, + goto_model_validation_optionst &validation_options) +{ + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); + return true; +} } // namespace -SCENARIO("validate goto program") +SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_modelt goto_model; @@ -117,12 +141,7 @@ SCENARIO("validate goto program") { goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -133,10 +152,7 @@ SCENARIO("validate goto program") { goto_model_validation_optionst validation_options{false}; validation_options.entry_point_exists = true; - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); + REQUIRE(test_for_pass(goto_model, validation_options)); } } @@ -165,12 +181,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -182,10 +193,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{false}; validation_options.function_pointer_calls_removed = true; - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); + REQUIRE(test_for_pass(goto_model, validation_options)); } } @@ -204,12 +212,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -232,12 +235,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -271,12 +269,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -288,10 +281,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{false}; validation_options.check_returns_removed = true; - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); + REQUIRE(test_for_pass(goto_model, validation_options)); } } @@ -309,12 +299,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -330,12 +315,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{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); + REQUIRE(test_for_fail(goto_model, validation_options)); } } @@ -349,10 +329,7 @@ SCENARIO("validate goto program") goto_model_validation_optionst validation_options{false}; validation_options.check_called_functions = true; - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); + REQUIRE(test_for_pass(goto_model, validation_options)); } } @@ -362,18 +339,18 @@ SCENARIO("validate goto program") THEN("fail!") { goto_convert(goto_model, null_message_handler); - auto &function_map = goto_model.goto_functions.function_map; - auto it = function_map.find("f"); - it->second.body.instructions.erase( - std::prev(it->second.body.instructions.end())); + auto &function_f = goto_model.goto_functions.function_map["f"]; + function_f.body.instructions.erase( + std::prev(function_f.body.instructions.end())); + // goto_function.validate checks by default (if a function has a body) + // that the last instruction of a function body marks the function's end. goto_model_validation_optionst validation_options{false}; - validation_options.check_last_instruction = true; + namespacet ns(goto_model.symbol_table); + REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), + function_f.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } @@ -383,59 +360,15 @@ SCENARIO("validate goto program") THEN("pass!") { goto_convert(goto_model, null_message_handler); + auto &function_f = goto_model.goto_functions.function_map["f"]; + // goto_function.validate checks by default (if a function has a body) + // that the last instruction of a function body marks the function's end. goto_model_validation_optionst validation_options{false}; - validation_options.check_last_instruction = true; - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); - } - } - - WHEN("an instruction \"code\" field, has a non nil source location") - { - THEN("fail!") - { - goto_convert(goto_model, null_message_handler); - auto &function_map = goto_model.goto_functions.function_map; - auto it = function_map.find("f"); - - auto source_location = - it->second.body.instructions.front().code.source_location(); - source_location.make_nil(); - - goto_model_validation_optionst validation_options{false}; - validation_options.check_sourcecode_location = true; - REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), - incorrect_goto_program_exceptiont); - } - } - - WHEN("an instruction source_location field is nil") - { - THEN("fail!") - { - goto_convert(goto_model, null_message_handler); - auto &function_map = goto_model.goto_functions.function_map; - auto it = function_map.find("f"); - - auto source_location = - it->second.body.instructions.front().source_location; - source_location.make_nil(); + namespacet ns(goto_model.symbol_table); - goto_model_validation_optionst validation_options{false}; - validation_options.check_sourcecode_location = true; - REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), - incorrect_goto_program_exceptiont); + REQUIRE_NOTHROW(function_f.validate( + ns, validation_modet::EXCEPTION, validation_options)); } } } From 1fb11297d5fdce7875f7fdf3141bb531c9045ec2 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Sun, 24 Feb 2019 23:26:18 +0000 Subject: [PATCH 09/13] Rebase and address review comments --- jbmc/src/jbmc/jbmc_parse_options.cpp | 10 +- src/cbmc/cbmc_parse_options.cpp | 20 +- .../goto_analyzer_parse_options.cpp | 4 +- src/goto-cc/compile.cpp | 6 +- .../goto_instrument_parse_options.cpp | 10 +- src/goto-programs/abstract_goto_model.h | 3 +- src/goto-programs/goto_function.cpp | 1 - src/goto-programs/goto_functions.h | 2 - src/goto-programs/goto_model.h | 19 +- src/goto-programs/goto_program.cpp | 6 +- src/goto-programs/initialize_goto_model.cpp | 8 +- src/goto-programs/lazy_goto_model.h | 3 +- src/goto-programs/validate_goto_model.cpp | 59 +++-- src/goto-programs/validate_goto_model.h | 47 ++-- .../goto_model_function_type_consistency.cpp | 5 +- unit/goto-programs/goto_program_assume.cpp | 8 +- unit/goto-programs/goto_program_dead.cpp | 8 +- .../goto_program_declaration.cpp | 8 +- .../goto_program_function_call.cpp | 8 +- .../goto_program_goto_target.cpp | 8 +- .../goto_program_instruction.cpp | 26 +- ..._program_symbol_type_table_consistency.cpp | 15 +- .../goto_program_table_consistency.cpp | 9 +- unit/goto-programs/goto_program_validate.cpp | 231 +++++++++++------- 24 files changed, 328 insertions(+), 196 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 03d24c1ae65..82078bba24b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -550,7 +550,10 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate(validation_modet::INVARIANT); + goto_model.validate( + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } if( @@ -691,7 +694,10 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - lazy_goto_model.validate(validation_modet::INVARIANT); + lazy_goto_model.validate( + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } // 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 c62e5f424f9..cbfd52ece9d 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -46,10 +46,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include #include #include #include @@ -60,9 +56,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include -#include -#include #include #include #include @@ -75,6 +68,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include +#include +#include + #include #include @@ -553,12 +551,10 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model_validation_optionst goto_model_validation_options{true}; - // this option is temporarily disabled until all source locations - // are reliably set correctly - goto_model_validation_options.check_source_location = false; goto_model.validate( - validation_modet::INVARIANT, goto_model_validation_options); + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } if( diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 5c05391c6e7..fac6080cbe6 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -407,7 +407,9 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { goto_model.validate( - validation_modet::INVARIANT, goto_model_validation_optionst{}); + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } // show it? diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3b8c6983ce0..285810b101b 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,10 @@ 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( + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } 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 4b45a25cf4e..9a64ec8c906 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -28,12 +28,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include #include #include +#include #include #include #include @@ -136,7 +136,9 @@ int goto_instrument_parse_optionst::doit() if(validate_only || cmdline.isset("validate-goto-model")) { goto_model.validate( - validation_modet::EXCEPTION, goto_model_validation_optionst{}); + validation_modet::EXCEPTION, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); if(validate_only) { @@ -150,7 +152,9 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { goto_model.validate( - validation_modet::INVARIANT, goto_model_validation_optionst{}); + validation_modet::INVARIANT, + goto_model_validation_optionst{ + goto_model_validation_optionst::set_optionst::all_true}); } { diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h index 33b9ea8379a..5d06fa1b750 100644 --- a/src/goto-programs/abstract_goto_model.h +++ b/src/goto-programs/abstract_goto_model.h @@ -57,7 +57,8 @@ class abstract_goto_modelt // 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; + 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 e5b182803a0..ab1b7f13970 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -72,4 +72,3 @@ void goto_functiont::validate( validate_full_type(type, ns, vm); } - diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index cc0ef26c65c..ab779cfe405 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -16,7 +16,6 @@ Date: June 2003 #include "goto_function.h" -#include "validate_goto_model.h" #include /// A collection of goto functions @@ -117,7 +116,6 @@ class goto_functionst const validation_modet vm, const goto_model_validation_optionst &goto_model_validation_options) const { - validate_goto_model(*this, vm, goto_model_validation_options); for(const auto &entry : function_map) { const goto_functiont &goto_function = entry.second; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index d49fa3a42c9..a0a5e4f6624 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. @@ -96,10 +97,16 @@ class goto_modelt : public abstract_goto_modelt /// reported via DATA_INVARIANT violations or exceptions. void validate( const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const override + 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, goto_model_validation_options); } @@ -146,12 +153,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt /// reported via DATA_INVARIANT violations or exceptions. void validate( const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const override + 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, goto_model_validation_options); + goto_functions.validate(ns, vm, goto_model_validation_options); } private: diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index babf64e1daa..c615029a98d 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -777,6 +777,8 @@ void goto_programt::instructiont::validate( } }; + // this option is always set to false until all source locations + // are reliably set correctly (future work) if(goto_model_validation_options.check_source_location) { DATA_CHECK( @@ -787,13 +789,13 @@ void goto_programt::instructiont::validate( DATA_CHECK( vm, code.source_location().is_not_nil(), - "each instruction \"code\" field, must have non nil source location"); + "each instruction code field, must have non nil source location"); DATA_CHECK( vm, source_location == code.source_location(), "instruction source location and" - " instruction \"code\" field source location must be the same"); + " instruction code field source location must be the same"); } const symbolt *table_symbol; diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 80565fb688a..df31058f6f1 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -194,8 +194,14 @@ goto_modelt initialize_goto_model( if(options.is_set("validate-goto-model")) { + goto_model_validation_optionst goto_model_validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + + // temporarily disabled until regression tests fixed + goto_model_validation_options.entry_point_exists = false; + goto_model.validate( - validation_modet::EXCEPTION, goto_model_validation_optionst{}); + 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 39e9392469b..871179d11cd 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -249,7 +249,8 @@ class lazy_goto_modelt : public abstract_goto_modelt /// reported via DATA_INVARIANT violations or exceptions. void validate( const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const override + const goto_model_validation_optionst &goto_model_validation_options) + const override { goto_model->validate(vm, goto_model_validation_options); } diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index dc70d55bd1e..9f2f057f043 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -1,5 +1,4 @@ /*******************************************************************\ - Module: Validate Goto Programs Author: Diffblue @@ -7,13 +6,15 @@ Author: Diffblue Date: Oct 2018 \*******************************************************************/ + #include "validate_goto_model.h" #include -#include "goto_functions.h" #include +#include "goto_functions.h" + namespace { class validate_goto_modelt @@ -23,28 +24,23 @@ class validate_goto_modelt validate_goto_modelt( const goto_functionst &goto_functions, - const validation_modet vm) - : vm{vm}, function_map{goto_functions.function_map} - { - } - - void - do_goto_program_checks(goto_model_validation_optionst validation_options); + const validation_modet vm, + const goto_model_validation_optionst goto_model_validation_options); private: /// Check the goto_program has an entry point /// - /// NB goto-cc -c will generate goto-programs without entry-points + /// goto-cc -c will generate goto-programs without entry-points /// until they are linked. void entry_point_exists(); - /// Check that no functions calls via function pointer are present + /// Check that no function calls via function pointer are present void function_pointer_calls_removed(); /// Check returns have been removed /// - /// NB Calls via function pointer must have been removed already when - /// removing returns, thus enabling this check also should enable the check + /// 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: @@ -53,19 +49,26 @@ class validate_goto_modelt /// - all return types are void (of both calls and functions themselves) void check_returns_removed(); - /// Check that for all - /// 1. functions that are called or - /// 2. functions of which the address is taken, + /// 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; }; -} // namespace -void validate_goto_modelt::do_goto_program_checks( - goto_model_validation_optionst validation_options) +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(); @@ -76,7 +79,9 @@ void validate_goto_modelt::do_goto_program_checks( 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(); @@ -97,7 +102,7 @@ void validate_goto_modelt::function_pointer_calls_removed() { for(const auto &fun : function_map) { - for(auto &instr : fun.second.body.instructions) + for(const auto &instr : fun.second.body.instructions) { if(instr.is_function_call()) { @@ -156,14 +161,17 @@ void validate_goto_modelt::check_called_functions() : 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) + + 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(), @@ -181,7 +189,7 @@ void validate_goto_modelt::check_called_functions() for(const auto &fun : function_map) { - for(auto &instr : fun.second.body.instructions) + for(const auto &instr : fun.second.body.instructions) { // check functions that are called if(instr.is_function_call()) @@ -197,17 +205,18 @@ void validate_goto_modelt::check_called_functions() } // check functions of which the address is taken - const exprt &src{instr.code}; + 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}.do_goto_program_checks( - 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 index 0e0e31be515..925fb87bd29 100644 --- a/src/goto-programs/validate_goto_model.h +++ b/src/goto-programs/validate_goto_model.h @@ -1,5 +1,4 @@ /*******************************************************************\ - Module: Validate Goto Programs Author: Diffblue @@ -7,35 +6,55 @@ Author: Diffblue Date: Oct 2018 \*******************************************************************/ + #ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H #define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H #include -struct goto_model_validation_optionst +class goto_model_validation_optionst final { +public: bool entry_point_exists; bool function_pointer_calls_removed; bool check_returns_removed; bool check_called_functions; bool check_source_location; - goto_model_validation_optionst() - : entry_point_exists{true}, - function_pointer_calls_removed{false}, - check_returns_removed{false}, - check_called_functions{false}, - check_source_location{false} +private: + void set_all_flags(bool options_value) { + // temporarily disabled until adjustments made for regression tests that + // have no entry point(e.g. testing json-ui warnings when there + // is no entry point) + entry_point_exists = false; + function_pointer_calls_removed = options_value; + check_returns_removed = options_value; + check_called_functions = options_value; + + // this option is temporarily disabled until all source locations + // are reliably set correctly + check_source_location = false; } - goto_model_validation_optionst(bool options_value) - : entry_point_exists{options_value}, - function_pointer_calls_removed{options_value}, - check_returns_removed{options_value}, - check_called_functions{options_value}, - check_source_location{options_value} +public: + 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; + } } }; diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index beb33aa56d7..8443886d2ca 100644 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -35,10 +35,13 @@ SCENARIO( goto_model.goto_functions.function_map[function_symbol.name].type = fun_type1; - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; // required as this test has no entry point, but calls the top-level // 'goto_model.validate()' validation_options.entry_point_exists = false; + validation_options.function_pointer_calls_removed = true; + validation_options.check_called_functions = true; WHEN("Symbol table has the right type") { diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index b8705a84261..29945656736 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -41,7 +41,10 @@ SCENARIO( namespacet ns(symbol_table); instructions.back() = goto_programt::make_assertion(x_le_10); - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; WHEN("Instruction has no targets") { @@ -59,7 +62,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 0e8e4d6560c..015cd9d75d2 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -37,7 +37,10 @@ SCENARIO( instructions.emplace_back(goto_programt::make_dead(var_a)); symbol_table.insert(fun_symbol); - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; WHEN("Removing known symbol") { @@ -59,7 +62,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate( + ns, 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 a1ebd69ed06..588817f0151 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -37,7 +37,10 @@ SCENARIO( instructions.emplace_back(goto_programt::make_decl(var_a)); symbol_table.insert(fun_symbol); - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; WHEN("Declaring known symbol") { @@ -59,7 +62,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index 76e95fdf6f6..e59a4b85850 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -51,7 +51,10 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; WHEN("Return type matches") { @@ -75,7 +78,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index 45b13193627..fc19c07be17 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -44,7 +44,10 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; WHEN("Target is a target") { @@ -62,7 +65,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_instruction.cpp b/unit/goto-programs/goto_program_instruction.cpp index 2424c3eb967..e15d64a2645 100644 --- a/unit/goto-programs/goto_program_instruction.cpp +++ b/unit/goto-programs/goto_program_instruction.cpp @@ -1,14 +1,13 @@ /*******************************************************************\ + Module: Unit tests for goto_program::validate - Module: Unit tests for goto_program::validate + Author: Diffblue Ltd. - Author: Diffblue Ltd. - - \*******************************************************************/ +\*******************************************************************/ #include #include -#include +#include #include #include @@ -31,7 +30,6 @@ SCENARIO( goto_programt::instructiont instruction; instruction.make_end_function(); instructions.push_back(instruction); - instructions.back().function = fun_name; // if not set will fail id test instructions.back().source_location.id("id_any_valid_id"); codet instruction_code_field; @@ -45,7 +43,9 @@ SCENARIO( WHEN("the source locations are set and identical") { - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_source_location = true; THEN("The consistency check succeeds") @@ -59,7 +59,9 @@ SCENARIO( { instructions.back().source_location.make_nil(); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_source_location = true; THEN("The consistency check fails") @@ -76,7 +78,9 @@ SCENARIO( auto &expr = static_cast(instructions.back().code); expr.add_source_location().make_nil(); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_source_location = true; THEN("The consistency check fails") @@ -95,7 +99,9 @@ SCENARIO( auto &expr = static_cast(instructions.back().code); expr.add_source_location().id("id_any_valid_id_2"); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_source_location = true; THEN("The consistency check fails") 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 51b02d80fbf..1c1ac1cbfa9 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -10,9 +10,9 @@ Author: Diffblue Ltd. #include -#include +#include #include - + SCENARIO( "Validation of consistent program/table pair (type-wise)", "[core][goto-programs][validate]") @@ -42,12 +42,10 @@ SCENARIO( goto_programt::instructiont end_function_instruction; end_function_instruction.make_end_function(); instructions.push_back(end_function_instruction); - instructions.back().function = function_symbol.name; - goto_model_validation_optionst validation_options; - // required as this test has no entry point, but calls the top-level - // 'goto_model.validate()' - validation_options.entry_point_exists = false; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.function_pointer_calls_removed = true; symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol type") @@ -74,7 +72,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index c4c860e921a..5bba951df89 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -41,9 +41,11 @@ SCENARIO( goto_programt::instructiont end_function_instruction; end_function_instruction.make_end_function(); instructions.push_back(end_function_instruction); - instructions.back().function = function_symbol.name; - goto_model_validation_optionst validation_options; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst::set_optionst::all_false}; + validation_options.entry_point_exists = true; + validation_options.function_pointer_calls_removed = true; symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol") @@ -64,7 +66,8 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate(ns, validation_modet::EXCEPTION, validation_options), + goto_function.validate( + ns, validation_modet::EXCEPTION, validation_options), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 7ef1f9b4e7e..023c6b57a7e 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -1,6 +1,5 @@ /*******************************************************************\ - - Module: Unit tests for goto program validation + Module: Unit tests for goto_program::validate Author: Diffblue Ltd. @@ -11,7 +10,8 @@ /// \file /// Unit tests for goto program validation -#include +#include + #include #include @@ -22,40 +22,6 @@ #include #include -namespace -{ -code_function_callt make_void_call(const symbol_exprt &function) -{ - code_function_callt ret; - ret.function() = function; - return ret; -} - -bool test_for_fail( - goto_modelt &goto_model, - goto_model_validation_optionst &validation_options) -{ - REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), - incorrect_goto_program_exceptiont); - return true; -} - -bool test_for_pass( - goto_modelt &goto_model, - goto_model_validation_optionst &validation_options) -{ - REQUIRE_NOTHROW(validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options)); - return true; -} -} // namespace - SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_modelt goto_model; @@ -71,11 +37,10 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") 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()))}}; - code_blockt f_body; - f_body.copy_to_operands(code_declt(x.symbol_expr())); - f_body.copy_to_operands( - code_assignt(x.symbol_expr(), from_integer(1, signed_int_type()))); f.value = f_body; goto_model.symbol_table.add(f); @@ -91,10 +56,10 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") g.mode = ID_C; g.type = code_typet({}, empty_typet()); - code_blockt g_body; - g_body.copy_to_operands(code_declt(y.symbol_expr())); - g_body.copy_to_operands( - code_assignt(y.symbol_expr(), from_integer(2, signed_int_type()))); + 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); @@ -107,6 +72,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") 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); @@ -114,16 +80,12 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") symbolt entry_point; entry_point.name = goto_functionst::entry_point(); entry_point.mode = ID_C; - entry_point.type = code_typet({}, void_typet()); - - code_blockt entry_point_body; - entry_point_body.copy_to_operands(code_declt(z.symbol_expr())); - entry_point_body.copy_to_operands( - code_assignt(z.symbol_expr(), from_integer(3, signed_int_type()))); - - entry_point_body.copy_to_operands( - code_assignt(fn_ptr.symbol_expr(), address_of_exprt{f.symbol_expr()})); - entry_point_body.copy_to_operands(make_void_call(g.symbol_expr())); + 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); @@ -139,9 +101,16 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") THEN("fail!") { - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; validation_options.entry_point_exists = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -150,9 +119,15 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") goto_convert(goto_model, null_message_handler); THEN("pass!") { - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.entry_point_exists = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -165,23 +140,29 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") symbolt k; k.name = "k"; k.mode = ID_C; - k.type = code_typet({}, empty_typet()); // void return, take no params + k.type = code_typet({}, empty_typet{}); // void return, take no params - code_function_callt function_call; - function_call.function() = dereference_exprt( - fn_ptr.symbol_expr(), pointer_typet(code_typet{{}, empty_typet()}, 64)); + code_function_callt function_call{ + dereference_exprt{fn_ptr.symbol_expr(), + pointer_typet(code_typet{{}, empty_typet{}}, 64)}}; - code_blockt k_body; - k_body.copy_to_operands(function_call); + 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{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.function_pointer_calls_removed = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -191,9 +172,15 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.function_pointer_calls_removed = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -210,9 +197,17 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") auto it = function_map.find("f"); it->second.type.return_type() = signedbv_typet{32}; - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_returns_removed = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -226,16 +221,23 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") goto_programt::instructiont instruction; instruction.make_return(); - instruction.function = "g"; // if this is not set will fail id test 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{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_returns_removed = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -244,32 +246,39 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") symbolt h; h.name = "h"; h.mode = ID_C; - h.type = code_typet({}, void_typet{}); + h.type = code_typet({}, empty_typet{}); h.value = code_blockt{}; goto_model.symbol_table.add(h); - symbolt k; - k.name = "k"; - k.mode = ID_C; - k.type = code_typet({}, empty_typet()); - code_blockt k_body; - // 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{}); - k_body.copy_to_operands(function_call); + 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{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_returns_removed = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -279,9 +288,15 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_returns_removed = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -297,9 +312,17 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") auto it = function_map.find("g"); function_map.erase(it); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_called_functions = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -313,9 +336,17 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") auto it = function_map.find("f"); function_map.erase(it); // f is no longer in function map - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_called_functions = true; - REQUIRE(test_for_fail(goto_model, validation_options)); + + REQUIRE_THROWS_AS( + validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options), + incorrect_goto_program_exceptiont); } } @@ -327,9 +358,15 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_convert(goto_model, null_message_handler); - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + validation_options.check_called_functions = true; - REQUIRE(test_for_pass(goto_model, validation_options)); + + REQUIRE_NOTHROW(validate_goto_model( + goto_model.goto_functions, + validation_modet::EXCEPTION, + validation_options)); } } @@ -345,7 +382,9 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") // goto_function.validate checks by default (if a function has a body) // that the last instruction of a function body marks the function's end. - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + namespacet ns(goto_model.symbol_table); REQUIRE_THROWS_AS( @@ -364,7 +403,9 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") // goto_function.validate checks by default (if a function has a body) // that the last instruction of a function body marks the function's end. - goto_model_validation_optionst validation_options{false}; + goto_model_validation_optionst validation_options{ + goto_model_validation_optionst ::set_optionst::all_false}; + namespacet ns(goto_model.symbol_table); REQUIRE_NOTHROW(function_f.validate( From 971c788ae09258fad916e2acef54104190cc22aa Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Thu, 28 Feb 2019 13:44:59 +0000 Subject: [PATCH 10/13] Address review comments - Kroening Removed previously disabled checks: Not every instruction has a code member - so removed checks that both instruction sourcelocation and code sourcelocation are set and identical Remove also remaining check that every instruction have a non-nil sourcelocation as this would have to be optional (if enabled fails many regression tests). This also simplifies considerably the overall validation pass (removes much passing around of the options structure). Removes check on function return type - this will be preserved (#4266) goto_model::validate now has default parameters. Minor fixes. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 10 +- src/cbmc/cbmc_parse_options.cpp | 5 +- .../goto_analyzer_parse_options.cpp | 5 +- src/goto-cc/compile.cpp | 5 +- .../goto_instrument_parse_options.cpp | 10 +- src/goto-programs/abstract_goto_model.h | 1 + src/goto-programs/goto_function.cpp | 5 +- src/goto-programs/goto_function.h | 4 +- src/goto-programs/goto_functions.h | 5 +- src/goto-programs/goto_model.h | 10 +- src/goto-programs/goto_program.cpp | 24 +--- src/goto-programs/goto_program.h | 14 +-- src/goto-programs/initialize_goto_model.cpp | 3 - src/goto-programs/lazy_goto_model.h | 6 +- src/goto-programs/validate_goto_model.cpp | 11 +- src/goto-programs/validate_goto_model.h | 23 ++-- unit/Makefile | 1 - unit/goto-programs/goto_program_assume.cpp | 12 +- unit/goto-programs/goto_program_dead.cpp | 12 +- .../goto_program_declaration.cpp | 12 +- .../goto_program_function_call.cpp | 12 +- .../goto_program_goto_target.cpp | 12 +- .../goto_program_instruction.cpp | 116 ------------------ ..._program_symbol_type_table_consistency.cpp | 13 +- .../goto_program_table_consistency.cpp | 10 +- unit/goto-programs/goto_program_validate.cpp | 40 +----- 26 files changed, 56 insertions(+), 325 deletions(-) delete mode 100644 unit/goto-programs/goto_program_instruction.cpp diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 82078bba24b..ad226c0499a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -550,10 +550,7 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + goto_model.validate(); } if( @@ -694,10 +691,7 @@ int jbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - lazy_goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + 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 cbfd52ece9d..368edf04e33 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -551,10 +551,7 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + 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 fac6080cbe6..492c859c88d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -406,10 +406,7 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + goto_model.validate(); } // show it? diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 285810b101b..fa29a36bdf8 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -547,10 +547,7 @@ bool compilet::write_bin_object_file( if(validate_goto_model) { status() << "Validating goto model" << eom; - src_goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + 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 9a64ec8c906..516be63d660 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -135,10 +135,7 @@ int goto_instrument_parse_optionst::doit() if(validate_only || cmdline.isset("validate-goto-model")) { - goto_model.validate( - validation_modet::EXCEPTION, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + goto_model.validate(validation_modet::EXCEPTION); if(validate_only) { @@ -151,10 +148,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("validate-goto-model")) { - goto_model.validate( - validation_modet::INVARIANT, - goto_model_validation_optionst{ - goto_model_validation_optionst::set_optionst::all_true}); + goto_model.validate(); } { diff --git a/src/goto-programs/abstract_goto_model.h b/src/goto-programs/abstract_goto_model.h index 5d06fa1b750..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 diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index ab1b7f13970..1844d35b5af 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -35,8 +35,7 @@ void get_local_identifiers( /// reported via DATA_INVARIANT violations or exceptions. void goto_functiont::validate( const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const + const validation_modet vm) const { // function body must end with an END_FUNCTION instruction if(body_available()) @@ -47,7 +46,7 @@ void goto_functiont::validate( "last instruction should be of end function type"); } - body.validate(ns, vm, goto_model_validation_options); + body.validate(ns, vm); find_symbols_sett typetags; find_type_symbols(type, typetags); diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index 240895fc87b..955f2f1d75c 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -21,7 +21,6 @@ Date: May 2018 #include #include "goto_program.h" -#include "validate_goto_model.h" /// A goto function, consisting of function type (see #type), function body (see /// #body), and parameter identifiers (see #parameter_identifiers). @@ -122,8 +121,7 @@ class goto_functiont /// reported via DATA_INVARIANT violations or exceptions. void validate( const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const; + const validation_modet vm) const; }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index ab779cfe405..4bb62fb8f4c 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -113,8 +113,7 @@ class goto_functionst /// reported via DATA_INVARIANT violations or exceptions. void validate( const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const + const validation_modet vm) const { for(const auto &entry : function_map) { @@ -151,7 +150,7 @@ class goto_functionst ++it; } - goto_function.validate(ns, vm, goto_model_validation_options); + goto_function.validate(ns, vm); } } }; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index a0a5e4f6624..52631d121a9 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -96,9 +96,9 @@ 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 goto_model_validation_optionst &goto_model_validation_options) - const override + 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); @@ -108,7 +108,7 @@ class goto_modelt : public abstract_goto_modelt validate_goto_model(goto_functions, vm, goto_model_validation_options); const namespacet ns(symbol_table); - goto_functions.validate(ns, vm, goto_model_validation_options); + goto_functions.validate(ns, vm); } }; @@ -164,7 +164,7 @@ class wrapper_goto_modelt : public abstract_goto_modelt validate_goto_model(goto_functions, vm, goto_model_validation_options); const namespacet ns(symbol_table); - goto_functions.validate(ns, vm, goto_model_validation_options); + goto_functions.validate(ns, vm); } private: diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index c615029a98d..a26c6096c1c 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -674,8 +674,7 @@ bool goto_programt::instructiont::equals(const instructiont &other) const void goto_programt::instructiont::validate( const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const + const validation_modet vm) const { validate_full_code(code, ns, vm); validate_full_expr(guard, ns, vm); @@ -777,27 +776,6 @@ void goto_programt::instructiont::validate( } }; - // this option is always set to false until all source locations - // are reliably set correctly (future work) - if(goto_model_validation_options.check_source_location) - { - DATA_CHECK( - vm, - source_location.is_not_nil(), - "each instruction source location must not be nil"); - - DATA_CHECK( - vm, - code.source_location().is_not_nil(), - "each instruction code field, must have non nil source location"); - - DATA_CHECK( - vm, - source_location == code.source_location(), - "instruction source location and" - " instruction code field source location must be the same"); - } - const symbolt *table_symbol; switch(type) { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 3ae3ab5aaa1..71f73fe050a 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "validate_goto_model.h" #include #include #include @@ -555,11 +554,7 @@ class goto_programt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate( - const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) - const; + void validate(const namespacet &ns, const validation_modet vm) const; /// Apply given transformer to all expressions; no return value /// means no change needed. @@ -819,14 +814,11 @@ class goto_programt /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate( - const namespacet &ns, - const validation_modet vm, - const goto_model_validation_optionst &goto_model_validation_options) const + void validate(const namespacet &ns, const validation_modet vm) const { for(const instructiont &ins : instructions) { - ins.validate(ns, vm, goto_model_validation_options); + ins.validate(ns, vm); } } diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index df31058f6f1..67d291631c6 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -197,9 +197,6 @@ goto_modelt initialize_goto_model( goto_model_validation_optionst goto_model_validation_options{ goto_model_validation_optionst ::set_optionst::all_false}; - // temporarily disabled until regression tests fixed - goto_model_validation_options.entry_point_exists = false; - goto_model.validate( validation_modet::INVARIANT, goto_model_validation_options); } diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 871179d11cd..1979064c5da 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -248,9 +248,9 @@ 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 goto_model_validation_optionst &goto_model_validation_options) - const override + 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_validation_options); } diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 9f2f057f043..2f3d42480e6 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -106,8 +106,7 @@ void validate_goto_modelt::function_pointer_calls_removed() { if(instr.is_function_call()) { - const code_function_callt &function_call = - to_code_function_call(instr.code); + const code_function_callt &function_call = instr.get_function_call(); DATA_CHECK( vm, function_call.function().id() == ID_symbol, @@ -122,10 +121,6 @@ void validate_goto_modelt::check_returns_removed() for(const auto &fun : function_map) { const goto_functiont &goto_function = fun.second; - DATA_CHECK( - vm, - goto_function.type.return_type().id() == ID_empty, - "functions must have empty return type"); for(const auto &instr : goto_function.body.instructions) { @@ -134,7 +129,7 @@ void validate_goto_modelt::check_returns_removed() if(instr.is_function_call()) { - const auto &function_call = to_code_function_call(instr.code); + const auto &function_call = instr.get_function_call(); DATA_CHECK( vm, function_call.lhs().is_nil(), @@ -194,7 +189,7 @@ void validate_goto_modelt::check_called_functions() // check functions that are called if(instr.is_function_call()) { - const auto &function_call = to_code_function_call(instr.code); + const auto &function_call = instr.get_function_call(); const irep_idt &identifier = to_symbol_expr(function_call.function()).get_identifier(); diff --git a/src/goto-programs/validate_goto_model.h b/src/goto-programs/validate_goto_model.h index 925fb87bd29..d521bd893f4 100644 --- a/src/goto-programs/validate_goto_model.h +++ b/src/goto-programs/validate_goto_model.h @@ -15,29 +15,26 @@ Date: Oct 2018 class goto_model_validation_optionst final { public: - bool entry_point_exists; - bool function_pointer_calls_removed; - bool check_returns_removed; - bool check_called_functions; - bool check_source_location; + // 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) { - // temporarily disabled until adjustments made for regression tests that - // have no entry point(e.g. testing json-ui warnings when there - // is no entry point) - entry_point_exists = false; + entry_point_exists = options_value; function_pointer_calls_removed = options_value; check_returns_removed = options_value; check_called_functions = options_value; - - // this option is temporarily disabled until all source locations - // are reliably set correctly - check_source_location = false; } public: + goto_model_validation_optionst() = default; + enum class set_optionst { all_true, diff --git a/unit/Makefile b/unit/Makefile index c9025f9a32c..edcc5199021 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -22,7 +22,6 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_declaration.cpp \ goto-programs/goto_program_function_call.cpp \ goto-programs/goto_program_goto_target.cpp \ - goto-programs/goto_program_instruction.cpp \ goto-programs/goto_program_symbol_type_table_consistency.cpp \ goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_program_validate.cpp \ diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index 29945656736..dc0f1db2d5d 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include SCENARIO( "Validation of well-formed assert/assume codes", @@ -41,17 +40,11 @@ SCENARIO( namespacet ns(symbol_table); instructions.back() = goto_programt::make_assertion(x_le_10); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - WHEN("Instruction has no targets") { THEN("The consistency check succeeds") { - goto_function.body.validate( - ns, validation_modet::INVARIANT, validation_options); + goto_function.body.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -62,8 +55,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 015cd9d75d2..7b591e892ed 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include SCENARIO( "Validation of well-formed symbol removing codes", @@ -37,11 +36,6 @@ SCENARIO( instructions.emplace_back(goto_programt::make_dead(var_a)); symbol_table.insert(fun_symbol); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - WHEN("Removing known symbol") { symbol_table.insert(var_symbol); @@ -49,8 +43,7 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate( - ns, validation_modet::INVARIANT, validation_options); + goto_function.body.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -62,8 +55,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index 588817f0151..19fed687358 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -9,7 +9,6 @@ Author: Diffblue Ltd. #include #include -#include #include @@ -37,11 +36,6 @@ SCENARIO( instructions.emplace_back(goto_programt::make_decl(var_a)); symbol_table.insert(fun_symbol); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - WHEN("Declaring known symbol") { symbol_table.insert(var_symbol); @@ -49,8 +43,7 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate( - ns, validation_modet::INVARIANT, validation_options); + goto_function.body.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -62,8 +55,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index e59a4b85850..cb923f87cbf 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include SCENARIO( "Validation of well-formed function call codes", @@ -51,11 +50,6 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - WHEN("Return type matches") { code_function_callt function_call(var_a, fun_foo, {}); @@ -64,8 +58,7 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.body.validate( - ns, validation_modet::INVARIANT, validation_options); + goto_function.body.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -78,8 +71,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index fc19c07be17..2e9ddddddc7 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -9,7 +9,6 @@ Author: Diffblue Ltd. #include #include -#include #include @@ -44,18 +43,12 @@ SCENARIO( symbol_table.insert(fun_symbol); namespacet ns(symbol_table); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - WHEN("Target is a target") { instructions.front().target_number = 1; THEN("The consistency check succeeds") { - goto_function.body.validate( - ns, validation_modet::INVARIANT, validation_options); + goto_function.body.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -65,8 +58,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), + goto_function.body.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_instruction.cpp b/unit/goto-programs/goto_program_instruction.cpp deleted file mode 100644 index e15d64a2645..00000000000 --- a/unit/goto-programs/goto_program_instruction.cpp +++ /dev/null @@ -1,116 +0,0 @@ -/*******************************************************************\ - Module: Unit tests for goto_program::validate - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include -#include -#include -#include - -#include -#include - -SCENARIO( - "Validation of well-formed instruction", - "[core][goto-programs][validate]") -{ - GIVEN("A function with one instruction") - { - symbol_tablet symbol_table; - symbolt fun_symbol; - irep_idt fun_name = "foo"; - fun_symbol.name = fun_name; - - goto_functiont goto_function; - auto &instructions = goto_function.body.instructions; - - goto_programt::instructiont instruction; - instruction.make_end_function(); - instructions.push_back(instruction); - instructions.back().source_location.id("id_any_valid_id"); - - codet instruction_code_field; - static_cast(instruction_code_field) - .add_source_location() - .id("id_any_valid_id"); - instructions.back().code = instruction_code_field; - - symbol_table.insert(fun_symbol); - namespacet ns(symbol_table); - - WHEN("the source locations are set and identical") - { - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_source_location = true; - - THEN("The consistency check succeeds") - { - REQUIRE_NOTHROW(goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options)); - } - } - - WHEN("the source location is not set") - { - instructions.back().source_location.make_nil(); - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_source_location = true; - - THEN("The consistency check fails") - { - REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), - incorrect_goto_program_exceptiont); - } - } - - WHEN("the 'code' source location is not set") - { - auto &expr = static_cast(instructions.back().code); - expr.add_source_location().make_nil(); - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_source_location = true; - - THEN("The consistency check fails") - { - REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), - incorrect_goto_program_exceptiont); - } - } - - WHEN("the source locations are not the same") - { - instructions.back().source_location.id("id_any_valid_id_1"); - - auto &expr = static_cast(instructions.back().code); - expr.add_source_location().id("id_any_valid_id_2"); - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_source_location = true; - - THEN("The consistency check fails") - { - REQUIRE_THROWS_AS( - goto_function.body.validate( - ns, validation_modet::EXCEPTION, validation_options), - incorrect_goto_program_exceptiont); - } - } - } -} 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 1c1ac1cbfa9..313fa58b9d1 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include SCENARIO( "Validation of consistent program/table pair (type-wise)", @@ -39,14 +38,10 @@ SCENARIO( // 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(); + goto_programt::instructiont end_function_instruction = + goto_programt::make_end_function(); instructions.push_back(end_function_instruction); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.function_pointer_calls_removed = true; - symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol type") { @@ -57,7 +52,7 @@ SCENARIO( THEN("The consistency check succeeds") { goto_function.validate( - ns, validation_modet::INVARIANT, validation_options); + ns, validation_modet::INVARIANT); REQUIRE(true); } @@ -73,7 +68,7 @@ SCENARIO( { REQUIRE_THROWS_AS( goto_function.validate( - ns, validation_modet::EXCEPTION, validation_options), + ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index 5bba951df89..2055d2a4cf5 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include SCENARIO( "Validation of consistent program/table pair", @@ -42,11 +41,6 @@ SCENARIO( end_function_instruction.make_end_function(); instructions.push_back(end_function_instruction); - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - validation_options.entry_point_exists = true; - validation_options.function_pointer_calls_removed = true; - symbol_table.insert(function_symbol); WHEN("Symbol table has the right symbol") { @@ -56,7 +50,7 @@ SCENARIO( THEN("The consistency check succeeds") { goto_function.validate( - ns, validation_modet::INVARIANT, validation_options); + ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -67,7 +61,7 @@ SCENARIO( { REQUIRE_THROWS_AS( goto_function.validate( - ns, validation_modet::EXCEPTION, validation_options), + ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 023c6b57a7e..088462a6a50 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -185,32 +185,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") } /// check_returns_removed() - WHEN( - "not all returns have been removed - a function has return type " - "non-empty") - { - THEN("fail!") - { - goto_convert(goto_model, null_message_handler); - - auto &function_map = goto_model.goto_functions.function_map; - auto it = function_map.find("f"); - it->second.type.return_type() = signedbv_typet{32}; - - 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 - an instruction is of type " "'return'") @@ -380,16 +354,11 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") function_f.body.instructions.erase( std::prev(function_f.body.instructions.end())); - // goto_function.validate checks by default (if a function has a body) - // that the last instruction of a function body marks the function's end. - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - namespacet ns(goto_model.symbol_table); REQUIRE_THROWS_AS( function_f.validate( - ns, validation_modet::EXCEPTION, validation_options), + ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } @@ -401,15 +370,10 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") goto_convert(goto_model, null_message_handler); auto &function_f = goto_model.goto_functions.function_map["f"]; - // goto_function.validate checks by default (if a function has a body) - // that the last instruction of a function body marks the function's end. - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - namespacet ns(goto_model.symbol_table); REQUIRE_NOTHROW(function_f.validate( - ns, validation_modet::EXCEPTION, validation_options)); + ns, validation_modet::EXCEPTION)); } } } From b5b1f64a2b755753f868a020df8c11cd7e8a5e50 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Fri, 1 Mar 2019 14:50:02 +0000 Subject: [PATCH 11/13] Address review comments - Kroening Removed previously disabled checks: Not every instruction has a code member - so removed checks that both instruction sourcelocation and code sourcelocation are set and identical Remove also remaining check that every instruction have a non-nil sourcelocation as this would have to be optional (if enabled fails many regression tests). This also simplifies considerably the overall validation pass (removes much passing around of the options structure). Removes check on function return type - this will be preserved (#4266) goto_model::validate now has default parameters. Minor fixes. --- src/goto-programs/goto_function.cpp | 5 ++--- src/goto-programs/goto_function.h | 4 +--- src/goto-programs/goto_functions.h | 4 +--- .../goto_program_symbol_type_table_consistency.cpp | 6 ++---- unit/goto-programs/goto_program_table_consistency.cpp | 6 ++---- unit/goto-programs/goto_program_validate.cpp | 6 ++---- 6 files changed, 10 insertions(+), 21 deletions(-) diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index 1844d35b5af..3d86edcded8 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -33,9 +33,8 @@ void get_local_identifiers( /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. -void goto_functiont::validate( - const namespacet &ns, - const validation_modet vm) const +void goto_functiont::validate(const namespacet &ns, const validation_modet vm) + const { // function body must end with an END_FUNCTION instruction if(body_available()) diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index 955f2f1d75c..90ef0d7879c 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -119,9 +119,7 @@ class goto_functiont /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate( - const namespacet &ns, - const validation_modet vm) const; + void validate(const namespacet &ns, const validation_modet vm) const; }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 4bb62fb8f4c..4cc922ec5bf 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -111,9 +111,7 @@ class goto_functionst /// /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. - void validate( - const namespacet &ns, - const validation_modet vm) const + void validate(const namespacet &ns, const validation_modet vm) const { for(const auto &entry : function_map) { 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 313fa58b9d1..9487fc5fd5c 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -51,8 +51,7 @@ SCENARIO( THEN("The consistency check succeeds") { - goto_function.validate( - ns, validation_modet::INVARIANT); + goto_function.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } @@ -67,8 +66,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate( - ns, validation_modet::EXCEPTION), + goto_function.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index 2055d2a4cf5..001d2e44e95 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -49,8 +49,7 @@ SCENARIO( const namespacet ns(symbol_table); THEN("The consistency check succeeds") { - goto_function.validate( - ns, validation_modet::INVARIANT); + goto_function.validate(ns, validation_modet::INVARIANT); REQUIRE(true); } } @@ -60,8 +59,7 @@ SCENARIO( THEN("The consistency check fails") { REQUIRE_THROWS_AS( - goto_function.validate( - ns, validation_modet::EXCEPTION), + goto_function.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 088462a6a50..0ab1e70d1fa 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -357,8 +357,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") namespacet ns(goto_model.symbol_table); REQUIRE_THROWS_AS( - function_f.validate( - ns, validation_modet::EXCEPTION), + function_f.validate(ns, validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } } @@ -372,8 +371,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") namespacet ns(goto_model.symbol_table); - REQUIRE_NOTHROW(function_f.validate( - ns, validation_modet::EXCEPTION)); + REQUIRE_NOTHROW(function_f.validate(ns, validation_modet::EXCEPTION)); } } } From a1de5dc259a445d5ef6fd9229fae681ff8dc73e2 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Fri, 1 Mar 2019 07:51:13 +0000 Subject: [PATCH 12/13] Remove extraneous goto-program checks in unit tests. Although additional checks may hold, they have their own unit tests and it is these tests that should fail when these checks fail. --- unit/goto-programs/goto_model_function_type_consistency.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index 8443886d2ca..d88e617850c 100644 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -37,11 +37,6 @@ SCENARIO( goto_model_validation_optionst validation_options{ goto_model_validation_optionst::set_optionst::all_false}; - // required as this test has no entry point, but calls the top-level - // 'goto_model.validate()' - validation_options.entry_point_exists = false; - validation_options.function_pointer_calls_removed = true; - validation_options.check_called_functions = true; WHEN("Symbol table has the right type") { From 6ba2cf43b4d9c634fea4fe0ed6ccb48753a867b8 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Fri, 1 Mar 2019 13:04:50 +0000 Subject: [PATCH 13/13] Reorder unit test headers for consistency. --- unit/goto-programs/goto_program_declaration.cpp | 4 ++-- unit/goto-programs/goto_program_goto_target.cpp | 4 ++-- unit/goto-programs/goto_program_validate.cpp | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) 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_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index 2e9ddddddc7..ebc9a571018 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -8,10 +8,10 @@ Author: Diffblue Ltd. #include -#include - #include +#include + SCENARIO( "Validation of well-formed goto codes", "[core][goto-programs][validate]") diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 0ab1e70d1fa..6e67e6ccdc5 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -14,14 +14,14 @@ #include -#include -#include - #include #include #include #include +#include +#include + SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { goto_modelt goto_model;