diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b3caeaa94f4..f312832dcfc 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -530,6 +530,11 @@ int cbmc_parse_optionst::doit() if(set_properties()) return CPROVER_EXIT_SET_PROPERTIES_FAILED; + if(cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::INVARIANT); + } + return bmct::do_language_agnostic_bmc( path_strategy_chooser, options, goto_model, ui_message_handler); } @@ -977,6 +982,8 @@ 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" + // NOLINTNEXTLINE(whitespace/line_length) + HELP_VALIDATE 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 f2fa3cfaa7e..f6727890244 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H -#include #include #include +#include +#include #include @@ -73,6 +74,7 @@ class optionst; OPT_FLUSH \ "(localize-faults)(localize-faults-method):" \ OPT_GOTO_TRACE \ + OPT_VALIDATE \ "(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-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index cc392a93697..dc7b8a1e55e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -406,6 +406,11 @@ int goto_analyzer_parse_optionst::doit() if(process_goto_program(options)) return CPROVER_EXIT_INTERNAL_ERROR; + if(cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::INVARIANT); + } + // show it? if(cmdline.isset("show-symbol-table")) { @@ -875,6 +880,7 @@ void goto_analyzer_parse_optionst::help() HELP_GOTO_CHECK "\n" "Other options:\n" + HELP_VALIDATE " --version show version and exit\n" HELP_FLUSH HELP_TIMESTAMP diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 9392ab2e7f8..ade410a4453 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -101,9 +101,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H -#include #include #include +#include +#include #include @@ -148,6 +149,7 @@ class optionst; "(show)(verify)(simplify):" \ "(location-sensitive)(concurrent)" \ "(no-simplify-slicing)" \ + OPT_VALIDATE \ // clang-format on class goto_analyzer_parse_optionst: diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b53b7503c11..f4b29d43e02 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -125,8 +125,27 @@ int goto_instrument_parse_optionst::doit() get_goto_program(); + { + const bool validate_only = cmdline.isset("validate-goto-binary"); + + if(validate_only || cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::EXCEPTION); + + if(validate_only) + { + return CPROVER_EXIT_SUCCESS; + } + } + } + instrument_goto_program(); + if(cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::INVARIANT); + } + { bool unwind_given=cmdline.isset("unwind"); bool unwindset_given=cmdline.isset("unwindset"); @@ -1572,6 +1591,10 @@ void goto_instrument_parse_optionst::help() " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*) " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*) " *and* used as a dereference operand\n" // NOLINT(*) + HELP_VALIDATE + // NOLINTNEXTLINE(whitespace/line_length) + " --validate-goto-binary check the well-formedness of the passed in goto\n" + " binary and then exit\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 747cdd7b22d..a5179302446 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H -#include #include #include +#include +#include #include #include @@ -101,6 +102,8 @@ Author: Daniel Kroening, kroening@kroening.com OPT_GOTO_PROGRAM_STATS \ "(show-local-safe-pointers)(show-safe-dereferences)" \ OPT_REPLACE_CALLS \ + "(validate-goto-binary)" \ + OPT_VALIDATE \ // empty last line // clang-format on diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index a1e8115747f..f9e1d7f99db 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -110,6 +110,16 @@ class goto_functiont parameter_identifiers = std::move(other.parameter_identifiers); return *this; } + + /// Check that the goto function is well-formed + /// + /// 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 + { + body.validate(ns, vm); + validate_full_type(type, ns, vm); + } }; 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 6e49f30af5c..a5fa9c0094f 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -117,6 +117,19 @@ class goto_functionst std::vector sorted() const; std::vector sorted(); + + /// Check that the goto functions are well-formed + /// + /// 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 + { + for(const auto &entry : function_map) + { + const goto_functiont &goto_function = entry.second; + goto_function.validate(ns, vm); + } + } }; #define Forall_goto_functions(it, functions) \ diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index aea03ae86da..d6b6c961b7c 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -89,6 +89,18 @@ class goto_modelt : public abstract_goto_modelt return goto_functions.function_map.find(id) != goto_functions.function_map.end(); } + + /// Check that the goto model is well-formed + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + void validate(const validation_modet vm) const + { + symbol_table.validate(); + + const namespacet ns(symbol_table); + goto_functions.validate(ns, 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..79a86c41d1d 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -668,6 +669,62 @@ bool goto_programt::instructiont::equals(const instructiont &other) const // clang-format on } +void goto_programt::instructiont::validate( + const namespacet &ns, + const validation_modet vm) const +{ + validate_full_code(code, ns, vm); + validate_full_expr(guard, ns, vm); + + switch(type) + { + case NO_INSTRUCTION_TYPE: + break; + case GOTO: + break; + case ASSUME: + break; + case ASSERT: + break; + case OTHER: + break; + case SKIP: + break; + case START_THREAD: + break; + case END_THREAD: + break; + case LOCATION: + break; + case END_FUNCTION: + break; + case ATOMIC_BEGIN: + break; + case ATOMIC_END: + break; + case RETURN: + break; + case ASSIGN: + DATA_CHECK( + code.get_statement() == ID_assign, + "assign instruction should contain an assign statement"); + DATA_CHECK(targets.empty(), "assign instruction should not have a target"); + break; + case DECL: + break; + case DEAD: + break; + case FUNCTION_CALL: + break; + case THROW: + break; + case CATCH: + break; + case INCOMPLETE_GOTO: + break; + } +} + bool goto_programt::equals(const goto_programt &other) const { if(instructions.size() != other.instructions.size()) diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 4499b7c3c6e..63f859b505d 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -20,10 +20,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include -#include #include +#include +#include + +enum class validation_modet; /// The type of an instruction in a GOTO program. enum goto_program_instruction_typet @@ -398,6 +400,12 @@ class goto_programt /// only be evaluated in the context of a goto_programt (see /// goto_programt::equals). bool equals(const instructiont &other) const; + + /// Check that the instruction is well-formed + /// + /// 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; }; // Never try to change this to vector-we mutate the list while iterating @@ -677,6 +685,18 @@ 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; + + /// Check that the goto program is well-formed + /// + /// 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 + { + for(const instructiont &ins : instructions) + { + ins.validate(ns, vm); + } + } }; /// Get control-flow successors of a given instruction. The instruction is diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 8cd410c97a8..bd3fbed6ec2 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -165,6 +165,11 @@ goto_modelt initialize_goto_model( goto_model.goto_functions, message_handler); + if(cmdline.isset("validate-goto-model")) + { + goto_model.validate(validation_modet::EXCEPTION); + } + // stupid hack config.set_object_bits_from_symbol_table( goto_model.symbol_table); diff --git a/src/util/Makefile b/src/util/Makefile index 7be29d060ed..6734fe7e701 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -96,6 +96,9 @@ SRC = arith_tools.cpp \ union_find.cpp \ union_find_replace.cpp \ unwrap_nested_exception.cpp \ + validate_code.cpp \ + validate_expressions.cpp \ + validate_types.cpp \ version.cpp \ xml.cpp \ xml_expr.cpp \ diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp index e88e8554455..29f850c1a7f 100644 --- a/src/util/exception_utils.cpp +++ b/src/util/exception_utils.cpp @@ -55,25 +55,23 @@ std::string deserialization_exceptiont::what() const } incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( - std::string message, - source_locationt source_location) - : message(std::move(message)), source_location(std::move(source_location)) + std::string message) + : message(std::move(message)) { + source_location.make_nil(); } std::string incorrect_goto_program_exceptiont::what() const { - if(source_location.is_nil()) - return message; - else - return message + " (at: " + source_location.as_string() + ")"; -} + std::string ret(message); -incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( - std::string message) - : message(std::move(message)) -{ - source_location.make_nil(); + if(!source_location.is_nil()) + ret += " (at: " + source_location.as_string() + ")"; + + if(!diagnostics.empty()) + ret += "\n" + diagnostics; + + return ret; } unsupported_operation_exceptiont::unsupported_operation_exceptiont( diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h index 98322e71eaa..90a15e51886 100644 --- a/src/util/exception_utils.h +++ b/src/util/exception_utils.h @@ -11,6 +11,7 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com #include +#include "invariant.h" #include "source_location.h" /// Base class for exceptions thrown in the cprover project. @@ -88,17 +89,54 @@ class deserialization_exceptiont : public cprover_exception_baset class incorrect_goto_program_exceptiont : public cprover_exception_baset { public: + explicit incorrect_goto_program_exceptiont(std::string message); + + template incorrect_goto_program_exceptiont( std::string message, - source_locationt source_location); - explicit incorrect_goto_program_exceptiont(std::string message); + Diagnostic &&diagnostic, + Diagnostics &&... diagnostics); + + template + incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location, + Diagnostics &&... diagnostics); + std::string what() const override; private: std::string message; source_locationt source_location; + + std::string diagnostics; }; +template +incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( + std::string message, + Diagnostic &&diagnostic, + Diagnostics &&... diagnostics) + : message(std::move(message)), + source_location(), + diagnostics(detail::assemble_diagnostics( + std::forward(diagnostic), + std::forward(diagnostics)...)) +{ +} + +template +incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location, + Diagnostics &&... diagnostics) + : message(std::move(message)), + source_location(std::move(source_location)), + diagnostics( + detail::assemble_diagnostics(std::forward(diagnostics)...)) +{ +} + /// Thrown when we encounter an instruction, parameters to an instruction etc. /// in a goto program that has some theoretically valid semantics, /// but that we don't presently have any support for. diff --git a/src/util/expr.h b/src/util/expr.h index ce9aa101e9b..96fbc98f8b1 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -10,6 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_EXPR_H #include "type.h" +#include "validate_expressions.h" +#include "validate_types.h" +#include "validation_mode.h" #include #include @@ -235,6 +238,63 @@ class exprt:public irept return static_cast(add(ID_C_source_location)); } + /// Check that the expression is well-formed (shallow checks only, i.e., + /// subexpressions and its type are not checked). + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding expressions. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + } + + /// Check that the expression is well-formed, assuming that its subexpressions + /// and type have all ready been checked for well-formedness. + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding expressions. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check_expr(expr, vm); + } + + /// Check that the expression is well-formed (full check, including checks + /// of all subexpressions and the type) + /// + /// Subclasses may override this function, though in most cases the provided + /// implementation should be sufficient. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate_full( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + // first check operands (if any) + for(const exprt &op : expr.operands()) + { + validate_full_expr(op, ns, vm); + } + + // type may be nil + const typet &t = expr.type(); + + validate_full_type(t, ns, vm); + + validate_expr(expr, ns, vm); + } + protected: exprt &add_expr(const irep_idt &name) { diff --git a/src/util/std_code.h b/src/util/std_code.h index 2de906428bd..a2996af8706 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -12,9 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "base_type.h" +#include "expr.h" #include "expr_cast.h" #include "invariant.h" #include "std_expr.h" +#include "validate.h" +#include "validate_code.h" /// Data structure for representing an arbitrary statement in a program. Every /// specific type of statement (e.g. block of statements, assignment, @@ -59,6 +63,53 @@ class codet:public exprt codet &last_statement(); const codet &last_statement() const; class code_blockt &make_block(); + + /// Check that the code statement is well-formed (shallow checks only, i.e., + /// enclosed statements, subexpressions, etc. are not checked) + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding types. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + } + + /// Check that the code statement is well-formed, assuming that all its + /// enclosed statements, subexpressions, etc. have all ready been checked for + /// well-formedness. + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding types. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check_code(code, vm); + } + + /// Check that the code statement is well-formed (full check, including checks + /// of all subexpressions) + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding types. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate_full( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check_code(code, vm); + } }; namespace detail // NOLINT @@ -236,6 +287,39 @@ class code_assignt:public codet { return op1(); } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + code.operands().size() == 2, "assignment must have two operands"); + } + + static void validate( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check(code, vm); + + DATA_CHECK( + base_type_eq(code.op0().type(), code.op1().type(), ns), + "lhs and rhs of assignment must have same type"); + } + + static void validate_full( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + for(const exprt &op : code.operands()) + { + validate_full_expr(op, ns, vm); + } + + validate(code, ns, vm); + } }; template<> inline bool can_cast_expr(const exprt &base) @@ -251,16 +335,14 @@ inline void validate_expr(const code_assignt & x) inline const code_assignt &to_code_assign(const codet &code) { PRECONDITION(code.get_statement() == ID_assign); - DATA_INVARIANT( - code.operands().size() == 2, "assignment must have two operands"); + code_assignt::check(code); return static_cast(code); } inline code_assignt &to_code_assign(codet &code) { PRECONDITION(code.get_statement() == ID_assign); - DATA_INVARIANT( - code.operands().size() == 2, "assignment must have two operands"); + code_assignt::check(code); return static_cast(code); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index aba92207c43..718dca71ebc 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file util/std_expr.h /// API to expression classes +#include "base_type.h" #include "expr_cast.h" #include "invariant.h" #include "mathematical_types.h" @@ -771,6 +772,22 @@ class binary_exprt:public exprt add_to_operands(_lhs, _rhs); } + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + expr.operands().size() == 2, "binary expression must have two operands"); + } + + static void validate( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + const exprt &op2() const = delete; exprt &op2() = delete; const exprt &op3() const = delete; @@ -826,6 +843,25 @@ class binary_predicate_exprt:public binary_exprt const exprt &_op1):binary_exprt(_op0, _id, _op1, bool_typet()) { } + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_exprt::check(expr, vm); + } + + static void validate( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_exprt::validate(expr, ns, vm); + + DATA_CHECK( + expr.type().id() == ID_bool, + "result of binary predicate expression should be of type bool"); + } }; /// \brief A base class for relations, i.e., binary predicates @@ -849,6 +885,26 @@ class binary_relation_exprt:public binary_predicate_exprt { } + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_predicate_exprt::check(expr, vm); + } + + static void validate( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_predicate_exprt::validate(expr, ns, vm); + + // check types + DATA_CHECK( + base_type_eq(expr.op0().type(), expr.op1().type(), ns), + "lhs and rhs of binary relation expression should have same type"); + } + exprt &lhs() { return op0(); @@ -1414,6 +1470,21 @@ class equal_exprt:public binary_relation_exprt binary_relation_exprt(_lhs, ID_equal, _rhs) { } + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_relation_exprt::check(expr, vm); + } + + static void validate( + const exprt &expr, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_relation_exprt::validate(expr, ns, vm); + } }; /// \brief Cast an exprt to an \ref equal_exprt @@ -1425,7 +1496,7 @@ class equal_exprt:public binary_relation_exprt inline const equal_exprt &to_equal_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_equal); - DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands"); + equal_exprt::check(expr); return static_cast(expr); } @@ -1433,7 +1504,7 @@ inline const equal_exprt &to_equal_expr(const exprt &expr) inline equal_exprt &to_equal_expr(exprt &expr) { PRECONDITION(expr.id()==ID_equal); - DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands"); + equal_exprt::check(expr); return static_cast(expr); } diff --git a/src/util/std_types.h b/src/util/std_types.h index ad93ff4838e..970549694be 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -14,9 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_STD_TYPES_H #include "expr.h" -#include "mp_arith.h" -#include "invariant.h" #include "expr_cast.h" +#include "invariant.h" +#include "mp_arith.h" +#include "validate.h" #include @@ -1143,6 +1144,13 @@ class bitvector_typet : public typet { set(ID_width, width); } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width"); + } }; /// Check whether a reference to a typet is a \ref bitvector_typet. @@ -1245,6 +1253,13 @@ class unsignedbv_typet:public bitvector_typet constant_exprt smallest_expr() const; constant_exprt zero_expr() const; constant_exprt largest_expr() const; + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + bitvector_typet::check(type, vm); + } }; /// Check whether a reference to a typet is a \ref unsignedbv_typet. @@ -1256,12 +1271,6 @@ inline bool can_cast_type(const typet &type) return type.id() == ID_unsignedbv; } -inline void validate_type(const unsignedbv_typet &type) -{ - DATA_INVARIANT( - !type.get(ID_width).empty(), "unsigned bitvector type must have width"); -} - /// \brief Cast a typet to an \ref unsignedbv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1273,18 +1282,16 @@ inline void validate_type(const unsignedbv_typet &type) inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) { PRECONDITION(can_cast_type(type)); - const unsignedbv_typet &ret = static_cast(type); - validate_type(ret); - return ret; + unsignedbv_typet::check(type); + return static_cast(type); } /// \copydoc to_unsignedbv_type(const typet &) inline unsignedbv_typet &to_unsignedbv_type(typet &type) { PRECONDITION(can_cast_type(type)); - unsignedbv_typet &ret = static_cast(type); - validate_type(ret); - return ret; + unsignedbv_typet::check(type); + return static_cast(type); } /// Fixed-width bit-vector with two's complement interpretation diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index fa2d3076da3..6d5725e47ed 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -109,6 +109,11 @@ class symbol_tablet : public symbol_table_baset { return iteratort(internal_symbols.end()); } + + /// Check that the symbol table is well-formed + void validate() const + { + } }; #endif // CPROVER_UTIL_SYMBOL_TABLE_H diff --git a/src/util/type.h b/src/util/type.h index e9806923692..55505258722 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -13,7 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_TYPE_H #define CPROVER_UTIL_TYPE_H +class namespacet; + #include "source_location.h" +#include "validate_types.h" +#include "validation_mode.h" /// The type of an expression, extends irept. Types may have subtypes. This is /// modeled with two subs named “subtype” (a single type) and “subtypes” @@ -74,6 +78,59 @@ class typet:public irept { return static_cast(find(name)); } + + /// Check that the type is well-formed (shallow checks only, i.e., subtypes + /// are not checked) + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding types. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + } + + /// Check that the type is well-formed, assuming that its subtypes have + /// already been checked for well-formedness. + /// + /// Subclasses may override this function to provide specific well-formedness + /// checks for the corresponding types. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate( + const typet &type, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check_type(type, vm); + } + + /// Check that the type is well-formed (full check, including checks of + /// subtypes) + /// + /// Subclasses may override this function, though in most cases the provided + /// implementation should be sufficient. + /// + /// The validation mode indicates whether well-formedness check failures are + /// reported via DATA_INVARIANT violations or exceptions. + static void validate_full( + const typet &type, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + // check subtypes + for(const irept &sub : type.get_sub()) + { + const typet &subtype = static_cast(sub); + validate_full_type(subtype, ns, vm); + } + + validate_type(type, ns, vm); + } }; /// Type with a single subtype. diff --git a/src/util/validate.h b/src/util/validate.h new file mode 100644 index 00000000000..eaf62c0576c --- /dev/null +++ b/src/util/validate.h @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Goto program validation macros + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_VALIDATE_H +#define CPROVER_UTIL_VALIDATE_H + +#include + +#include "exception_utils.h" +#include "validation_mode.h" + +/// This macro takes a condition which denotes a well-formedness criterion on +/// goto programs, expressions, instructions, etc. When invoking the macro, a +/// variable named `vm` of type `const validation_modet` should be in scope. It +/// indicates whether DATA_INVARIANT() is used to check the condition, or if an +/// exception is thrown when the condition does not hold. +#define DATA_CHECK(condition, message) \ + do \ + { \ + static_assert( \ + std::is_same::value, \ + "when invoking the macro DATA_CHECK(), a variable named `vm` of type " \ + "`const validation_modet` should be in scope which indicates the " \ + "validation mode (see `validate.h`"); \ + 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 \ + { \ + static_assert( \ + std::is_same::value, \ + "when invoking the macro DATA_CHECK_WITH_DIAGNOSTICS(), a variable " \ + "named `vm` of type `const validation_modet` should be in scope which " \ + "indicates the validation mode (see `validate.h`"); \ + 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, __VA_ARGS__); \ + break; \ + } \ + } while(0) + +#endif /* CPROVER_UTIL_VALIDATE_H */ diff --git a/src/util/validate_code.cpp b/src/util/validate_code.cpp new file mode 100644 index 00000000000..9123ad6680d --- /dev/null +++ b/src/util/validate_code.cpp @@ -0,0 +1,90 @@ +/*******************************************************************\ + +Module: Validate code + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include "validate_code.h" + +#ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS +#include +#endif + +#include "namespace.h" +#include "std_code.h" +#include "validate.h" +#include "validate_helpers.h" + +#define CALL_ON_CODE(code_type) \ + C()(code, std::forward(args)...) + +template