From 1fb11297d5fdce7875f7fdf3141bb531c9045ec2 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Sun, 24 Feb 2019 23:26:18 +0000 Subject: [PATCH] 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(