diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a6a18c77057..0d585382514 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -526,6 +526,12 @@ int cbmc_parse_optionst::doit() if(set_properties()) return CPROVER_EXIT_SET_PROPERTIES_FAILED; + if(cmdline.isset("validate-goto-model")) + { + namespacet ns(goto_model.symbol_table); + goto_model.validate(ns, validation_modet::INVARIANT); + } + return bmct::do_language_agnostic_bmc( path_strategy_chooser, options, goto_model, ui_message_handler); } @@ -972,6 +978,7 @@ void cbmc_parse_optionst::help() " --xml-ui use XML-formatted output\n" " --xml-interface bi-directional XML interface\n" " --json-ui use JSON-formatted output\n" + " --validate-goto-model enables additional well-formedness checks on the goto program\n" // NOLINT(*) HELP_GOTO_TRACE HELP_FLUSH " --verbosity # verbosity level\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index fcc207ffb20..b1e11bea75b 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -72,6 +72,7 @@ class optionst; OPT_FLUSH \ "(localize-faults)(localize-faults-method):" \ OPT_GOTO_TRACE \ + "(validate-goto-model)" \ "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 80c14205968..6c33dc6580b 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -12,8 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H -#include +#include #include +#include +#include #include "abstract_goto_model.h" #include "goto_functions.h" @@ -95,6 +97,23 @@ class goto_modelt : public abstract_goto_modelt return goto_functions.function_map.find(id) != goto_functions.function_map.end(); } + + /// Iterates over the functions inside the goto model and checks invariants + /// in all of them. Prints out error message collected. + /// \param ns namespace for the environment + /// \param vm validation mode to be used for error reporting + void validate(const namespacet &ns, const validation_modet &vm) const + { + forall_goto_functions(it, goto_functions) + { + DATA_CHECK( + base_type_eq( + it->second.type, symbol_table.lookup_ref(it->first).type, ns), + id2string(it->first) + " type inconsistency\ngoto program type: " + + it->second.type.id_string() + "\nsymbol table type: " + + symbol_table.lookup_ref(it->first).type.id_string()); + } + } }; /// Class providing the abstract GOTO model interface onto an unrelated diff --git a/src/util/expr.h b/src/util/expr.h index a89cc19a630..fcd57275aed 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_EXPR_H #include "type.h" +#include "validate.h" #include #include diff --git a/src/util/validate.h b/src/util/validate.h new file mode 100644 index 00000000000..fc6082ea396 --- /dev/null +++ b/src/util/validate.h @@ -0,0 +1,61 @@ +/*******************************************************************\ + +Module: Goto program validation + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_VALIDATE_H +#define CPROVER_UTIL_VALIDATE_H + +#include + +#include "exception_utils.h" +#include "invariant.h" +#include "irep.h" + +enum class validation_modet +{ + INVARIANT, + EXCEPTION +}; + +#define GET_FIRST(A, ...) A + +/// This macro takes a condition which denotes a well-formedness criterion on +/// goto programs, expressions, instructions, etc. Based on the value of the +/// variable vm (the validation mode), it either uses DATA_INVARIANT() to check +/// those conditions, or throws an exception when a condition does not hold. +#define DATA_CHECK(condition, message) \ + do \ + { \ + switch(vm) \ + { \ + case validation_modet::INVARIANT: \ + DATA_INVARIANT(condition, message); \ + break; \ + case validation_modet::EXCEPTION: \ + if(!(condition)) \ + throw incorrect_goto_program_exceptiont(message); \ + break; \ + } \ + } while(0) + +#define DATA_CHECK_WITH_DIAGNOSTICS(condition, message, ...) \ + do \ + { \ + switch(vm) \ + { \ + case validation_modet::INVARIANT: \ + DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__); \ + break; \ + case validation_modet::EXCEPTION: \ + if(!(condition)) \ + throw incorrect_goto_program_exceptiont( \ + message, GET_FIRST(__VA_ARGS__, dummy)); \ + break; \ + } \ + } while(0) + +#endif /* CPROVER_UTIL_VALIDATE_H */ diff --git a/unit/Makefile b/unit/Makefile index 261393bd89e..2412c7ab562 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -15,6 +15,7 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ goto-programs/goto_trace_output.cpp \ + goto-programs/goto_model_function_type_consistency.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ path_strategies.cpp \ diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp new file mode 100644 index 00000000000..458370da898 --- /dev/null +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -0,0 +1,69 @@ +/*******************************************************************\ + + Module: Unit tests for goto_model::validate + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of consistent program/table pair (function type)", + "[core][goto-programs][validate]") +{ + GIVEN("A model with one function") + { + const typet type1 = signedbv_typet(32); + const typet type2 = signedbv_typet(64); + code_typet fun_type1({}, type1); + code_typet fun_type2({}, type2); + + symbolt function_symbol; + irep_idt function_symbol_name = "foo"; + function_symbol.name = function_symbol_name; + + goto_modelt goto_model; + goto_model.goto_functions.function_map[function_symbol.name] = + goto_functiont(); + goto_model.goto_functions.function_map[function_symbol.name].type = + fun_type1; + + WHEN("Symbol table has the right type") + { + function_symbol.type = fun_type1; + goto_model.symbol_table.insert(function_symbol); + namespacet ns(goto_model.symbol_table); + + THEN("The consistency check succeeds") + { + goto_model.validate(ns, validation_modet::INVARIANT); + + REQUIRE(true); + } + } + + WHEN("Symbol table has the wrong type") + { + function_symbol.type = fun_type2; + goto_model.symbol_table.insert(function_symbol); + namespacet ns(goto_model.symbol_table); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_model.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +}