diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.h b/jbmc/src/java_bytecode/character_refine_preprocess.h index 7fb1578134d..8e7dd44e5eb 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.h +++ b/jbmc/src/java_bytecode/character_refine_preprocess.h @@ -20,8 +20,9 @@ Date: March 2017 #ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H #define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H -#include +#include #include +#include #include diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp index 109db7c9315..61d3aa4048d 100644 --- a/jbmc/src/java_bytecode/code_with_references.cpp +++ b/jbmc/src/java_bytecode/code_with_references.cpp @@ -8,7 +8,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "code_with_references.h" #include "java_types.h" + #include +#include codet allocate_array( const exprt &expr, diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp index 50863dae548..8dab3198699 100644 --- a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp +++ b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp @@ -14,6 +14,7 @@ Author: Diffblue Ltd. #include #include +#include #include #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index eec8d47676b..de8b7872edb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -12,6 +12,7 @@ Date: June 2017 #include #include +#include #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp index 1222ec68e86..652fc2d6713 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_typecheck.h" -#include +#include void java_bytecode_typecheckt::typecheck_code(codet &code) { diff --git a/jbmc/src/java_bytecode/lift_clinit_calls.cpp b/jbmc/src/java_bytecode/lift_clinit_calls.cpp index 80ca2af795d..64f5d0b70e5 100644 --- a/jbmc/src/java_bytecode/lift_clinit_calls.cpp +++ b/jbmc/src/java_bytecode/lift_clinit_calls.cpp @@ -13,6 +13,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h index d708c09c719..c1ff2860014 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.h +++ b/jbmc/unit/java-testing-utils/require_goto_statements.h @@ -9,8 +9,8 @@ Author: Diffblue Ltd. /// \file /// Utilties for inspecting goto functions +#include #include -#include #include diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp index 18b18692cd9..c490d4b3792 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp @@ -7,14 +7,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com \*******************************************************************/ #include - #include #include #include #include + #include #include + #include +#include #include #include diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp index e3f6558c722..7fcd2001cf0 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp @@ -16,6 +16,7 @@ Author: Diffblue Ltd. #include #include +#include #include #include diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index bfb49377621..386943e029c 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index b65fdc0a078..aa44d7dbbfa 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index fcc98022150..513f8969bfa 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index ffedc861002..10d761075fe 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 4a343a2fc01..8135dd5f585 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" +#include #include bool cpp_typecheckt::find_dtor(const symbolt &symbol) const diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 228a7673baa..4d37932b849 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include #include diff --git a/src/goto-instrument/object_id.cpp b/src/goto-instrument/object_id.cpp index b0dc0f2351f..ea754793ab5 100644 --- a/src/goto-instrument/object_id.cpp +++ b/src/goto-instrument/object_id.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "object_id.h" +#include #include -#include enum class get_modet { LHS_R, LHS_W, READ }; diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp index bb298d9cd3b..31e9de7fa86 100644 --- a/src/goto-programs/destructor.cpp +++ b/src/goto-programs/destructor.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" +#include #include -#include code_function_callt get_destructor( const namespacet &ns, diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 329062b63b6..9032dfb1229 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,10 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include -#include enum class validation_modet; diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index 4287eb3f1b8..76502d2ce7c 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com // #include +#include #include -#include #include diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index d0b630b1fe8..e65b18eeb03 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -11,6 +11,7 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_convert.h" +#include #include #include diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 97fa3adc292..5d12ecbc6ac 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -12,8 +12,8 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_typecheck.h" #include +#include #include -#include #include #include "expr2jsil.h" diff --git a/src/jsil/parser.y b/src/jsil/parser.y index 227fa8c51bd..a0d72b31924 100644 --- a/src/jsil/parser.y +++ b/src/jsil/parser.y @@ -11,7 +11,7 @@ extern char *yyjsiltext; #define YYSTYPE unsigned #define YYSTYPE_IS_TRIVIAL 1 -#include +#include #include #include "jsil_y.tab.h" diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index a6ce0d83e5d..4ce9c006c9c 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index fc46539ae57..73e406a5cc5 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include #include @@ -23,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{}; diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index 071a68e021f..753555cd911 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -13,6 +13,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "converters/statement_list_types.h" #include +#include #include #include #include diff --git a/src/util/allocate_objects.h b/src/util/allocate_objects.h index 7ac1976c7ae..09a0a737596 100644 --- a/src/util/allocate_objects.h +++ b/src/util/allocate_objects.h @@ -9,9 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H #define CPROVER_UTIL_ALLOCATE_OBJECTS_H +#include "goto_instruction_code.h" #include "namespace.h" #include "source_location.h" -#include "std_code.h" /// Selects the kind of objects allocated enum class lifetimet diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 41b0f202218..5d6273c6e80 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -14,12 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "byte_operators.h" #include "format_type.h" +#include "goto_instruction_code.h" #include "ieee_float.h" #include "mathematical_expr.h" #include "mp_arith.h" #include "pointer_expr.h" #include "prefix.h" -#include "std_code.h" #include "string_utils.h" #include diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h new file mode 100644 index 00000000000..9b3ec65ffbe --- /dev/null +++ b/src/util/goto_instruction_code.h @@ -0,0 +1,522 @@ +/*******************************************************************\ + +Module: Data structures representing instructions in a GOTO program + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H +#define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H + +#include "std_code.h" + +/// A \ref codet representing an assignment in the program. +/// For example, if an expression `e1` is represented as an \ref exprt `expr1` +/// and an expression `e2` is represented as an \ref exprt `expr2`, the +/// assignment `e1 = e2;` can be represented as `code_assignt(expr1, expr2)`. +class code_assignt : public codet +{ +public: + code_assignt() : codet(ID_assign) + { + operands().resize(2); + } + + code_assignt(exprt lhs, exprt rhs) + : codet(ID_assign, {std::move(lhs), std::move(rhs)}) + { + } + + code_assignt(exprt lhs, exprt rhs, source_locationt loc) + : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc)) + { + } + + exprt &lhs() + { + return op0(); + } + + exprt &rhs() + { + return op1(); + } + + const exprt &lhs() const + { + return op0(); + } + + const exprt &rhs() const + { + return op1(); + } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, code.operands().size() == 2, "assignment must have two operands"); + } + + static void validate( + const codet &code, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(code, vm); + + DATA_CHECK( + vm, + code.op0().type() == code.op1().type(), + "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); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assign); +} + +inline void validate_expr(const code_assignt &x) +{ + code_assignt::check(x); +} + +inline const code_assignt &to_code_assign(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_assign); + code_assignt::check(code); + return static_cast(code); +} + +inline code_assignt &to_code_assign(codet &code) +{ + PRECONDITION(code.get_statement() == ID_assign); + code_assignt::check(code); + return static_cast(code); +} + +/// A \ref codet representing the removal of a local variable going out of +/// scope. +class code_deadt : public codet +{ +public: + explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)}) + { + } + + symbol_exprt &symbol() + { + return static_cast(op0()); + } + + const symbol_exprt &symbol() const + { + return static_cast(op0()); + } + + const irep_idt &get_identifier() const + { + return symbol().get_identifier(); + } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + code.operands().size() == 1, + "removal (code_deadt) must have one operand"); + DATA_CHECK( + vm, + code.op0().id() == ID_symbol, + "removing a non-symbol: " + id2string(code.op0().id()) + "from scope"); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_dead); +} + +inline void validate_expr(const code_deadt &x) +{ + code_deadt::check(x); +} + +inline const code_deadt &to_code_dead(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_dead); + code_deadt::check(code); + return static_cast(code); +} + +inline code_deadt &to_code_dead(codet &code) +{ + PRECONDITION(code.get_statement() == ID_dead); + code_deadt::check(code); + return static_cast(code); +} + +/// \ref codet representation of a function call statement. +/// The function call statement has three operands. +/// The first is the expression that is used to store the return value. +/// The second is the function called. +/// The third is a vector of argument values. +class code_function_callt : public codet +{ +public: + explicit code_function_callt(exprt _function) + : codet( + ID_function_call, + {nil_exprt(), std::move(_function), exprt(ID_arguments)}) + { + } + + typedef exprt::operandst argumentst; + + code_function_callt(exprt _lhs, exprt _function, argumentst _arguments) + : codet( + ID_function_call, + {std::move(_lhs), std::move(_function), exprt(ID_arguments)}) + { + arguments() = std::move(_arguments); + } + + code_function_callt(exprt _function, argumentst _arguments) + : code_function_callt(std::move(_function)) + { + arguments() = std::move(_arguments); + } + + exprt &lhs() + { + return op0(); + } + + const exprt &lhs() const + { + return op0(); + } + + exprt &function() + { + return op1(); + } + + const exprt &function() const + { + return op1(); + } + + argumentst &arguments() + { + return op2().operands(); + } + + const argumentst &arguments() const + { + return op2().operands(); + } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + code.operands().size() == 3, + "function calls must have three operands:\n1) expression to store the " + "returned values\n2) the function being called\n3) the vector of " + "arguments"); + } + + static void validate( + const codet &code, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(code, vm); + + if(code.op0().id() != ID_nil) + DATA_CHECK( + vm, + code.op0().type() == to_code_type(code.op1().type()).return_type(), + "function returns expression of wrong 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); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_function_call); +} + +inline void validate_expr(const code_function_callt &x) +{ + code_function_callt::check(x); +} + +inline const code_function_callt &to_code_function_call(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_function_call); + code_function_callt::check(code); + return static_cast(code); +} + +inline code_function_callt &to_code_function_call(codet &code) +{ + PRECONDITION(code.get_statement() == ID_function_call); + code_function_callt::check(code); + return static_cast(code); +} + +/// An assumption, which must hold in subsequent code. +class code_assumet : public codet +{ +public: + explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)}) + { + } + + const exprt &assumption() const + { + return op0(); + } + + exprt &assumption() + { + return op0(); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assume); +} + +inline void validate_expr(const code_assumet &x) +{ + validate_operands(x, 1, "assume must have one operand"); +} + +inline const code_assumet &to_code_assume(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_assume); + const code_assumet &ret = static_cast(code); + validate_expr(ret); + return ret; +} + +inline code_assumet &to_code_assume(codet &code) +{ + PRECONDITION(code.get_statement() == ID_assume); + code_assumet &ret = static_cast(code); + validate_expr(ret); + return ret; +} + +/// A non-fatal assertion, which checks a condition then permits execution to +/// continue. +class code_assertt : public codet +{ +public: + explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)}) + { + } + + const exprt &assertion() const + { + return op0(); + } + + exprt &assertion() + { + return op0(); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assert); +} + +inline void validate_expr(const code_assertt &x) +{ + validate_operands(x, 1, "assert must have one operand"); +} + +inline const code_assertt &to_code_assert(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_assert); + const code_assertt &ret = static_cast(code); + validate_expr(ret); + return ret; +} + +inline code_assertt &to_code_assert(codet &code) +{ + PRECONDITION(code.get_statement() == ID_assert); + code_assertt &ret = static_cast(code); + validate_expr(ret); + return ret; +} + +/// A `codet` representing the declaration that an input of a particular +/// description has a value which corresponds to the value of a given expression +/// (or expressions). +/// When working with the C front end, calls to the `__CPROVER_input` intrinsic +/// can be added to the input code in order add instructions of this type to the +/// goto program. +/// The first argument is expected to be a C string denoting the input +/// identifier. The second argument is the expression for the input value. +class code_inputt : public codet +{ +public: + /// This constructor is for support of calls to `__CPROVER_input` in user + /// code. Where the first first argument is a description which may be any + /// `const char *` and one or more corresponding expression arguments follow. + explicit code_inputt( + std::vector arguments, + optionalt location = {}); + + /// This constructor is intended for generating input instructions as part of + /// synthetic entry point code, rather than as part of user code. + /// \param description: This is used to construct an expression for a pointer + /// to a string constant containing the description text. This expression + /// is then used as the first argument. + /// \param expression: This expression corresponds to a value which should be + /// recorded as an input. + /// \param location: A location to associate with this instruction. + code_inputt( + const irep_idt &description, + exprt expression, + optionalt location = {}); + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT); +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_input); +} + +inline void validate_expr(const code_inputt &input) +{ + code_inputt::check(input); +} + +/// A `codet` representing the declaration that an output of a particular +/// description has a value which corresponds to the value of a given expression +/// (or expressions). +/// When working with the C front end, calls to the `__CPROVER_output` intrinsic +/// can be added to the input code in order add instructions of this type to the +/// goto program. +/// The first argument is expected to be a C string denoting the output +/// identifier. The second argument is the expression for the output value. +class code_outputt : public codet +{ +public: + /// This constructor is for support of calls to `__CPROVER_output` in user + /// code. Where the first first argument is a description which may be any + /// `const char *` and one or more corresponding expression arguments follow. + explicit code_outputt( + std::vector arguments, + optionalt location = {}); + + /// This constructor is intended for generating output instructions as part of + /// synthetic entry point code, rather than as part of user code. + /// \param description: This is used to construct an expression for a pointer + /// to a string constant containing the description text. + /// \param expression: This expression corresponds to a value which should be + /// recorded as an output. + /// \param location: A location to associate with this instruction. + code_outputt( + const irep_idt &description, + exprt expression, + optionalt location = {}); + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT); +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_output); +} + +inline void validate_expr(const code_outputt &output) +{ + code_outputt::check(output); +} + +#endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index 5790b827498..4246ee996f0 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "c_types.h" +#include "goto_instruction_code.h" #include "pointer_expr.h" #include "string_constant.h" diff --git a/src/util/std_code.h b/src/util/std_code.h index a8555272fbc..04aaa27d53d 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -285,113 +285,6 @@ template<> inline bool can_cast_expr(const exprt &base) // there is no to_code_skip, so no validate_expr is provided for code_skipt -/// A \ref codet representing an assignment in the program. -/// For example, if an expression `e1` is represented as an \ref exprt `expr1` -/// and an expression `e2` is represented as an \ref exprt `expr2`, the -/// assignment `e1 = e2;` can be represented as `code_assignt(expr1, expr2)`. -class code_assignt:public codet -{ -public: - code_assignt():codet(ID_assign) - { - operands().resize(2); - } - - code_assignt(exprt lhs, exprt rhs) - : codet(ID_assign, {std::move(lhs), std::move(rhs)}) - { - } - - code_assignt(exprt lhs, exprt rhs, source_locationt loc) - : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc)) - { - } - - exprt &lhs() - { - return op0(); - } - - exprt &rhs() - { - return op1(); - } - - const exprt &lhs() const - { - return op0(); - } - - const exprt &rhs() const - { - return op1(); - } - - static void check( - const codet &code, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, code.operands().size() == 2, "assignment must have two operands"); - } - - static void validate( - const codet &code, - const namespacet &, - const validation_modet vm = validation_modet::INVARIANT) - { - check(code, vm); - - DATA_CHECK( - vm, - code.op0().type() == code.op1().type(), - "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); - } - -protected: - using codet::op0; - using codet::op1; - using codet::op2; - using codet::op3; -}; - -template<> inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_assign); -} - -inline void validate_expr(const code_assignt & x) -{ - code_assignt::check(x); -} - -inline const code_assignt &to_code_assign(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_assign); - code_assignt::check(code); - return static_cast(code); -} - -inline code_assignt &to_code_assign(codet &code) -{ - PRECONDITION(code.get_statement() == ID_assign); - code_assignt::check(code); - return static_cast(code); -} - /// A `codet` representing the declaration of a local variable. /// For example, if a variable (symbol) `x` is represented as a /// \ref symbol_exprt `sym`, then the declaration of this variable can be @@ -491,271 +384,6 @@ inline code_declt &to_code_decl(codet &code) return static_cast(code); } -/// A \ref codet representing the removal of a local variable going out of -/// scope. -class code_deadt:public codet -{ -public: - explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)}) - { - } - - symbol_exprt &symbol() - { - return static_cast(op0()); - } - - const symbol_exprt &symbol() const - { - return static_cast(op0()); - } - - const irep_idt &get_identifier() const - { - return symbol().get_identifier(); - } - - static void check( - const codet &code, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, - code.operands().size() == 1, - "removal (code_deadt) must have one operand"); - DATA_CHECK( - vm, - code.op0().id() == ID_symbol, - "removing a non-symbol: " + id2string(code.op0().id()) + "from scope"); - } - -protected: - using codet::op0; - using codet::op1; - using codet::op2; - using codet::op3; -}; - -template<> inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_dead); -} - -inline void validate_expr(const code_deadt &x) -{ - code_deadt::check(x); -} - -inline const code_deadt &to_code_dead(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_dead); - code_deadt::check(code); - return static_cast(code); -} - -inline code_deadt &to_code_dead(codet &code) -{ - PRECONDITION(code.get_statement() == ID_dead); - code_deadt::check(code); - return static_cast(code); -} - -/// An assumption, which must hold in subsequent code. -class code_assumet:public codet -{ -public: - explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)}) - { - } - - const exprt &assumption() const - { - return op0(); - } - - exprt &assumption() - { - return op0(); - } - -protected: - using codet::op0; - using codet::op1; - using codet::op2; - using codet::op3; -}; - -template<> inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_assume); -} - -inline void validate_expr(const code_assumet &x) -{ - validate_operands(x, 1, "assume must have one operand"); -} - -inline const code_assumet &to_code_assume(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_assume); - const code_assumet &ret = static_cast(code); - validate_expr(ret); - return ret; -} - -inline code_assumet &to_code_assume(codet &code) -{ - PRECONDITION(code.get_statement() == ID_assume); - code_assumet &ret = static_cast(code); - validate_expr(ret); - return ret; -} - -/// A non-fatal assertion, which checks a condition then permits execution to -/// continue. -class code_assertt:public codet -{ -public: - explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)}) - { - } - - const exprt &assertion() const - { - return op0(); - } - - exprt &assertion() - { - return op0(); - } - -protected: - using codet::op0; - using codet::op1; - using codet::op2; - using codet::op3; -}; - -template<> inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_assert); -} - -inline void validate_expr(const code_assertt &x) -{ - validate_operands(x, 1, "assert must have one operand"); -} - -inline const code_assertt &to_code_assert(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_assert); - const code_assertt &ret = static_cast(code); - validate_expr(ret); - return ret; -} - -inline code_assertt &to_code_assert(codet &code) -{ - PRECONDITION(code.get_statement() == ID_assert); - code_assertt &ret = static_cast(code); - validate_expr(ret); - return ret; -} - -/// A `codet` representing the declaration that an input of a particular -/// description has a value which corresponds to the value of a given expression -/// (or expressions). -/// When working with the C front end, calls to the `__CPROVER_input` intrinsic -/// can be added to the input code in order add instructions of this type to the -/// goto program. -/// The first argument is expected to be a C string denoting the input -/// identifier. The second argument is the expression for the input value. -class code_inputt : public codet -{ -public: - /// This constructor is for support of calls to `__CPROVER_input` in user - /// code. Where the first first argument is a description which may be any - /// `const char *` and one or more corresponding expression arguments follow. - explicit code_inputt( - std::vector arguments, - optionalt location = {}); - - /// This constructor is intended for generating input instructions as part of - /// synthetic entry point code, rather than as part of user code. - /// \param description: This is used to construct an expression for a pointer - /// to a string constant containing the description text. This expression - /// is then used as the first argument. - /// \param expression: This expression corresponds to a value which should be - /// recorded as an input. - /// \param location: A location to associate with this instruction. - code_inputt( - const irep_idt &description, - exprt expression, - optionalt location = {}); - - static void check( - const codet &code, - const validation_modet vm = validation_modet::INVARIANT); -}; - -template <> -inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_input); -} - -inline void validate_expr(const code_inputt &input) -{ - code_inputt::check(input); -} - -/// A `codet` representing the declaration that an output of a particular -/// description has a value which corresponds to the value of a given expression -/// (or expressions). -/// When working with the C front end, calls to the `__CPROVER_output` intrinsic -/// can be added to the input code in order add instructions of this type to the -/// goto program. -/// The first argument is expected to be a C string denoting the output -/// identifier. The second argument is the expression for the output value. -class code_outputt : public codet -{ -public: - /// This constructor is for support of calls to `__CPROVER_output` in user - /// code. Where the first first argument is a description which may be any - /// `const char *` and one or more corresponding expression arguments follow. - explicit code_outputt( - std::vector arguments, - optionalt location = {}); - - /// This constructor is intended for generating output instructions as part of - /// synthetic entry point code, rather than as part of user code. - /// \param description: This is used to construct an expression for a pointer - /// to a string constant containing the description text. - /// \param expression: This expression corresponds to a value which should be - /// recorded as an output. - /// \param location: A location to associate with this instruction. - code_outputt( - const irep_idt &description, - exprt expression, - optionalt location = {}); - - static void check( - const codet &code, - const validation_modet vm = validation_modet::INVARIANT); -}; - -template <> -inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_output); -} - -inline void validate_expr(const code_outputt &output) -{ - code_outputt::check(output); -} - /// Create a fatal assertion, which checks a condition and then halts if it does /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. /// @@ -1204,137 +832,6 @@ inline code_gotot &to_code_goto(codet &code) return ret; } -/// \ref codet representation of a function call statement. -/// The function call statement has three operands. -/// The first is the expression that is used to store the return value. -/// The second is the function called. -/// The third is a vector of argument values. -class code_function_callt:public codet -{ -public: - explicit code_function_callt(exprt _function) - : codet( - ID_function_call, - {nil_exprt(), std::move(_function), exprt(ID_arguments)}) - { - } - - typedef exprt::operandst argumentst; - - code_function_callt(exprt _lhs, exprt _function, argumentst _arguments) - : codet( - ID_function_call, - {std::move(_lhs), std::move(_function), exprt(ID_arguments)}) - { - arguments() = std::move(_arguments); - } - - code_function_callt(exprt _function, argumentst _arguments) - : code_function_callt(std::move(_function)) - { - arguments() = std::move(_arguments); - } - - exprt &lhs() - { - return op0(); - } - - const exprt &lhs() const - { - return op0(); - } - - exprt &function() - { - return op1(); - } - - const exprt &function() const - { - return op1(); - } - - argumentst &arguments() - { - return op2().operands(); - } - - const argumentst &arguments() const - { - return op2().operands(); - } - - static void check( - const codet &code, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, - code.operands().size() == 3, - "function calls must have three operands:\n1) expression to store the " - "returned values\n2) the function being called\n3) the vector of " - "arguments"); - } - - static void validate( - const codet &code, - const namespacet &, - const validation_modet vm = validation_modet::INVARIANT) - { - check(code, vm); - - if(code.op0().id() != ID_nil) - DATA_CHECK( - vm, - code.op0().type() == to_code_type(code.op1().type()).return_type(), - "function returns expression of wrong 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); - } - -protected: - using codet::op0; - using codet::op1; - using codet::op2; - using codet::op3; -}; - -template<> inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_function_call); -} - -inline void validate_expr(const code_function_callt &x) -{ - code_function_callt::check(x); -} - -inline const code_function_callt &to_code_function_call(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_function_call); - code_function_callt::check(code); - return static_cast(code); -} - -inline code_function_callt &to_code_function_call(codet &code) -{ - PRECONDITION(code.get_statement() == ID_function_call); - code_function_callt::check(code); - return static_cast(code); -} - /// \ref codet representation of a "return from a function" statement. class code_returnt:public codet { diff --git a/src/util/validate_code.cpp b/src/util/validate_code.cpp index aa3517ebca8..758e8a50a77 100644 --- a/src/util/validate_code.cpp +++ b/src/util/validate_code.cpp @@ -12,6 +12,7 @@ Author: Daniel Poetzl #include #endif +#include "goto_instruction_code.h" #include "std_code.h" #include "validate_helpers.h"