From 8558e891962d1603ec9a82633cee1d21f077213b Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Tue, 9 Oct 2018 09:41:57 +0100 Subject: [PATCH 1/5] Function type consistency between goto programs and symbol table A simple iteration over goto-functions to check that it's base type is the same as the one stored in the symbol table. --- src/cbmc/cbmc_parse_options.cpp | 4 ++++ src/goto-programs/goto_model.h | 25 ++++++++++++++++++++++++- 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a6a18c77057..4a7efc48785 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -515,6 +515,10 @@ int cbmc_parse_optionst::doit() if(get_goto_program_ret!=-1) return get_goto_program_ret; + INVARIANT( + !goto_model.check_internal_invariants(*this), + "goto program internal invariants failed"); + if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 80c14205968..e04334a48d2 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,27 @@ 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 msg message instance to collect errors + /// \return true if any violation was found + bool check_internal_invariants(messaget &msg) const + { + bool found_violation = false; + namespacet ns(symbol_table); + forall_goto_functions(it, goto_functions) + { + if(!base_type_eq( + it->second.type, symbol_table.lookup_ref(it->first).type, ns)) + { + msg.error() << "error" << messaget::eom; + found_violation = true; + } + } + + return found_violation; + } }; /// Class providing the abstract GOTO model interface onto an unrelated From 150cf46d1a04b50d066293b5224e109ef072190e Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Tue, 9 Oct 2018 11:05:37 +0100 Subject: [PATCH 2/5] Better error message Now reports the id of violating function and the two inconsistent types. --- src/goto-programs/goto_model.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index e04334a48d2..3c0f538e8d8 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -111,7 +111,13 @@ class goto_modelt : public abstract_goto_modelt if(!base_type_eq( it->second.type, symbol_table.lookup_ref(it->first).type, ns)) { - msg.error() << "error" << messaget::eom; + msg.error() << id2string(it->first) << " type inconsistency\n" + << "goto program type: " << it->second.type.id_string() + << "\nsymbol table type: " + << symbol_table.lookup_ref(it->first).type.id_string() + << messaget::eom; + + msg.error() << "" << messaget::eom; found_violation = true; } } From 7dd2aa54189f6f3dd58dd3336ed9daee33b23fa2 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 8 Oct 2018 15:01:39 +0100 Subject: [PATCH 3/5] Add macros for goto model validation --- src/util/validate.h | 61 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/util/validate.h 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 */ From 43052d570a1c86daaf5084e22ed34f71df3b4b8c Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Wed, 10 Oct 2018 14:30:32 +0100 Subject: [PATCH 4/5] Reworked based on PR #3123 Using DATA_CHECK instead of calling error handling directly. --- src/cbmc/cbmc_parse_options.cpp | 11 +++++++---- src/cbmc/cbmc_parse_options.h | 1 + src/goto-programs/goto_model.h | 28 +++++++++------------------- src/util/expr.h | 1 + 4 files changed, 18 insertions(+), 23 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 4a7efc48785..0d585382514 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -515,10 +515,6 @@ int cbmc_parse_optionst::doit() if(get_goto_program_ret!=-1) return get_goto_program_ret; - INVARIANT( - !goto_model.check_internal_invariants(*this), - "goto program internal invariants failed"); - if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { @@ -530,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); } @@ -976,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 3c0f538e8d8..6c33dc6580b 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -100,29 +100,19 @@ class goto_modelt : public abstract_goto_modelt /// Iterates over the functions inside the goto model and checks invariants /// in all of them. Prints out error message collected. - /// \param msg message instance to collect errors - /// \return true if any violation was found - bool check_internal_invariants(messaget &msg) const + /// \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 { - bool found_violation = false; - namespacet ns(symbol_table); forall_goto_functions(it, goto_functions) { - if(!base_type_eq( - it->second.type, symbol_table.lookup_ref(it->first).type, ns)) - { - msg.error() << id2string(it->first) << " type inconsistency\n" - << "goto program type: " << it->second.type.id_string() - << "\nsymbol table type: " - << symbol_table.lookup_ref(it->first).type.id_string() - << messaget::eom; - - msg.error() << "" << messaget::eom; - found_violation = true; - } + 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()); } - - return found_violation; } }; 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 From 00357ff365bccb68cf4395653ead5b2f95d50c13 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 11 Oct 2018 15:10:05 +0100 Subject: [PATCH 5/5] Added unit test for wrong type in table Builds a goto model with one function and checks that: 1) with the right type in the table the validation succeeds, 2) with the wrong type the validation fails. --- unit/Makefile | 1 + .../goto_model_function_type_consistency.cpp | 69 +++++++++++++++++++ 2 files changed, 70 insertions(+) create mode 100644 unit/goto-programs/goto_model_function_type_consistency.cpp 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); + } + } + } +}