diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8412b99da8c..bc5ba49f251 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 c8ace68078c..a8b61c0f21f 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_function.h b/src/goto-programs/goto_function.h index a1e8115747f..e52b5d581a3 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -110,6 +110,11 @@ class goto_functiont parameter_identifiers = std::move(other.parameter_identifiers); return *this; } + + void validate(const symbol_tablet &table, const validation_modet &vm) const + { + return body.validate(table, vm); + } }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 80c14205968..fca679fa7b2 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "abstract_goto_model.h" #include "goto_functions.h" @@ -95,6 +96,18 @@ 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) + { + it->second.validate(symbol_table, vm); + } + } }; /// Class providing the abstract GOTO model interface onto an unrelated diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 310e85c6d46..c11f3b4a16f 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -668,6 +669,61 @@ bool goto_programt::instructiont::equals(const instructiont &other) const // clang-format on } +void goto_programt::instructiont::validate( + const symbol_tablet &table, + const validation_modet &vm) const +{ + namespacet ns(table); + std::vector> type_collector; + + auto type_finder = [&](const exprt &e) { + if(e.id() == ID_symbol) + { + auto symbol_expr = to_symbol_expr(e); + const auto &symbol_id = symbol_expr.get_identifier(); + + if(table.has_symbol(symbol_id)) + DATA_CHECK_WITH_DIAGNOSTICS( + base_type_eq( + symbol_expr.type(), table.lookup_ref(symbol_id).type, ns), + id2string(symbol_id) + " type inconsistency\n" + + "goto program type: " + symbol_expr.type().id_string() + "\n " + + "symbol table type: " + + table.lookup_ref(symbol_id).type.id_string(), + source_location); + } + }; + + switch(type) + { + case GOTO: + case ASSUME: + case ASSERT: + guard.visit(type_finder); + break; + case ASSIGN: + case DECL: + case DEAD: + case FUNCTION_CALL: + code.visit(type_finder); + break; + case OTHER: + case SKIP: + case LOCATION: + case END_FUNCTION: + case START_THREAD: + case END_THREAD: + case ATOMIC_BEGIN: + case ATOMIC_END: + case RETURN: + case THROW: + case CATCH: + case NO_INSTRUCTION_TYPE: + case INCOMPLETE_GOTO: + break; + } +} + bool goto_programt::equals(const goto_programt &other) const { if(instructions.size() != other.instructions.size()) @@ -699,6 +755,16 @@ bool goto_programt::equals(const goto_programt &other) const return true; } +void goto_programt::validate( + const symbol_tablet &table, + const validation_modet &vm) const +{ + forall_goto_program_instructions(it, (*this)) + { + it->validate(table, vm); + } +} + /// Outputs a string representation of a `goto_program_instruction_typet` std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t) { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 4499b7c3c6e..9f75fc58c84 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include /// The type of an instruction in a GOTO program. enum goto_program_instruction_typet @@ -398,6 +399,12 @@ class goto_programt /// only be evaluated in the context of a goto_programt (see /// goto_programt::equals). bool equals(const instructiont &other) const; + + /// Iterate over code and guard and collect inconsistencies with symbol + /// table. + /// \param table the symbol table + /// \param vm validation mode + void validate(const symbol_tablet &table, const validation_modet &vm) const; }; // Never try to change this to vector-we mutate the list while iterating @@ -677,6 +684,8 @@ class goto_programt /// the same number of instructions, each pair of instructions compares equal, /// and relative jumps have the same distance. bool equals(const goto_programt &other) const; + + void validate(const symbol_tablet &table, const validation_modet &vm) const; }; /// Get control-flow successors of a given instruction. The instruction is diff --git a/src/util/expr.cpp b/src/util/expr.cpp index a800ea15be0..5ac79acbf2c 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -322,6 +322,24 @@ void exprt::visit(const_expr_visitort &visitor) const } } +void exprt::visit(const std::function &f) const +{ + std::stack stack; + + stack.push(this); + + while(!stack.empty()) + { + const exprt &expr = *stack.top(); + stack.pop(); + + f(expr); + + forall_operands(it, expr) + stack.push(&(*it)); + } +} + depth_iteratort exprt::depth_begin() { return depth_iteratort(*this); } depth_iteratort exprt::depth_end() diff --git a/src/util/expr.h b/src/util/expr.h index a89cc19a630..5b0d8deb2fe 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 @@ -224,6 +225,7 @@ class exprt:public irept public: void visit(class expr_visitort &visitor); void visit(class const_expr_visitort &visitor) const; + void visit(const std::function &f) const; depth_iteratort depth_begin(); depth_iteratort depth_end(); 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..34406d9796f 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_program_symbol_type_table_consistency.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ path_strategies.cpp \ diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp new file mode 100644 index 00000000000..538f6efe069 --- /dev/null +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -0,0 +1,68 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of consistent program/table pair (type-wise)", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one assertion") + { + symbol_tablet symbol_table; + const typet type1 = signedbv_typet(32); + const typet type2 = signedbv_typet(64); + symbolt symbol; + irep_idt symbol_name = "a"; + symbol.name = symbol_name; + symbol_exprt varx(symbol_name, type1); + + exprt val10 = from_integer(10, type1); + binary_relation_exprt x_le_10(varx, ID_le, val10); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::ASSERT); + instructions.back().make_assertion(x_le_10); + + WHEN("Symbol table has the right symbol type") + { + symbol.type = type1; + symbol_table.insert(symbol); + + THEN("The consistency check succeeds") + { + goto_function.validate(symbol_table, validation_modet::INVARIANT); + + REQUIRE(true); + } + } + + WHEN("Symbol table has the wrong symbol type") + { + symbol.type = type2; + symbol_table.insert(symbol); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.validate(symbol_table, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +}