From 698be3d57aa816df2861141a204d88641f770445 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Oct 2021 13:04:36 +0100 Subject: [PATCH 1/3] move codet into separate header file The codet class is currently shared between the front-end code classes and the classes that represent goto-instructions. This commit moves this class into a separate header file so it can be consumed by both without including everything else. --- src/util/std_code.h | 149 +---------------------------------- src/util/std_code_base.h | 162 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 163 insertions(+), 148 deletions(-) create mode 100644 src/util/std_code_base.h diff --git a/src/util/std_code.h b/src/util/std_code.h index 9a2e6c74841..c19fdca005a 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -12,155 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "expr_cast.h" -#include "invariant.h" +#include "std_code_base.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, -/// if-then-else statement...) is represented by a subtype of `codet`. -/// `codet`s are represented to be subtypes of \ref exprt since statements can -/// occur in an expression context in C: for example, the assignment `x = y;` -/// is an expression with return value `y`. For other types of statements in an -/// expression context, see e.g. -/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html. -/// To distinguish a `codet` from other [exprts](\ref exprt), we set its -/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of -/// `codet`, we use a named sub `ID_statement`. -class codet:public exprt -{ -public: - /// \param statement: Specifies the type of the `codet` to be constructed, - /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a - /// \ref code_frontend_assignt. - explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet()) - { - set_statement(statement); - } - - codet(const irep_idt &statement, source_locationt loc) - : exprt(ID_code, empty_typet(), std::move(loc)) - { - set_statement(statement); - } - - /// \param statement: Specifies the type of the `codet` to be constructed, - /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a - /// \ref code_frontend_assignt. - /// \param _op: any operands to be added - explicit codet(const irep_idt &statement, operandst _op) : codet(statement) - { - operands() = std::move(_op); - } - - codet(const irep_idt &statement, operandst op, source_locationt loc) - : codet(statement, std::move(loc)) - { - operands() = std::move(op); - } - - void set_statement(const irep_idt &statement) - { - set(ID_statement, statement); - } - - const irep_idt &get_statement() const - { - return get(ID_statement); - } - - codet &first_statement(); - const codet &first_statement() const; - codet &last_statement(); - const codet &last_statement() const; - - /// 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 &, const validation_modet) - { - } - - /// 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 &, - 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 &, - const validation_modet vm = validation_modet::INVARIANT) - { - check_code(code, vm); - } - - using exprt::op0; - using exprt::op1; - using exprt::op2; - using exprt::op3; -}; - -namespace detail // NOLINT -{ - -template -inline bool can_cast_code_impl(const exprt &expr, const Tag &tag) -{ - if(const auto ptr = expr_try_dynamic_cast(expr)) - { - return ptr->get_statement() == tag; - } - return false; -} - -} // namespace detail - -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_code; -} - -// to_code has no validation other than checking the id(), so no validate_expr -// is provided for codet - -inline const codet &to_code(const exprt &expr) -{ - PRECONDITION(expr.id() == ID_code); - return static_cast(expr); -} - -inline codet &to_code(exprt &expr) -{ - PRECONDITION(expr.id() == ID_code); - return static_cast(expr); -} /// A \ref codet representing an assignment in the program. /// For example, if an expression `e1` is represented as an \ref exprt `expr1` diff --git a/src/util/std_code_base.h b/src/util/std_code_base.h new file mode 100644 index 00000000000..55282af4951 --- /dev/null +++ b/src/util/std_code_base.h @@ -0,0 +1,162 @@ +/*******************************************************************\ + +Module: Data structures representing statements in a program + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_STD_CODE_BASE_H +#define CPROVER_UTIL_STD_CODE_BASE_H + +#include "expr_cast.h" +#include "invariant.h" +#include "std_types.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, +/// if-then-else statement...) is represented by a subtype of `codet`. +/// `codet`s are represented to be subtypes of \ref exprt since statements can +/// occur in an expression context in C: for example, the assignment `x = y;` +/// is an expression with return value `y`. For other types of statements in an +/// expression context, see e.g. +/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html. +/// To distinguish a `codet` from other [exprts](\ref exprt), we set its +/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of +/// `codet`, we use a named sub `ID_statement`. +class codet : public exprt +{ +public: + /// \param statement: Specifies the type of the `codet` to be constructed, + /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a + /// \ref code_frontend_assignt. + explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet()) + { + set_statement(statement); + } + + codet(const irep_idt &statement, source_locationt loc) + : exprt(ID_code, empty_typet(), std::move(loc)) + { + set_statement(statement); + } + + /// \param statement: Specifies the type of the `codet` to be constructed, + /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a + /// \ref code_frontend_assignt. + /// \param _op: any operands to be added + explicit codet(const irep_idt &statement, operandst _op) : codet(statement) + { + operands() = std::move(_op); + } + + codet(const irep_idt &statement, operandst op, source_locationt loc) + : codet(statement, std::move(loc)) + { + operands() = std::move(op); + } + + void set_statement(const irep_idt &statement) + { + set(ID_statement, statement); + } + + const irep_idt &get_statement() const + { + return get(ID_statement); + } + + codet &first_statement(); + const codet &first_statement() const; + codet &last_statement(); + const codet &last_statement() const; + + /// 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 &, const validation_modet) + { + } + + /// 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 &, + 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 &, + const validation_modet vm = validation_modet::INVARIANT) + { + check_code(code, vm); + } + + using exprt::op0; + using exprt::op1; + using exprt::op2; + using exprt::op3; +}; + +namespace detail // NOLINT +{ +template +inline bool can_cast_code_impl(const exprt &expr, const Tag &tag) +{ + if(const auto ptr = expr_try_dynamic_cast(expr)) + { + return ptr->get_statement() == tag; + } + return false; +} + +} // namespace detail + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_code; +} + +// to_code has no validation other than checking the id(), so no validate_expr +// is provided for codet + +inline const codet &to_code(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_code); + return static_cast(expr); +} + +inline codet &to_code(exprt &expr) +{ + PRECONDITION(expr.id() == ID_code); + return static_cast(expr); +} + +#endif // CPROVER_UTIL_STD_CODE_BASE_H From 60c9fe5d6f621e61dee9642f466512e3b7a19bcd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Oct 2021 13:20:57 +0100 Subject: [PATCH 2/3] move code_declt to goto_instruction_code.h After introducing code_frontend_declt, code_declt is now used exclusively by goto instructions, and thus belongs into goto_instruction_code.h. --- .../create_array_with_type_intrinsic.cpp | 2 +- src/util/goto_instruction_code.h | 65 +++++++++++++++++++ src/util/std_code.h | 65 ------------------- 3 files changed, 66 insertions(+), 66 deletions(-) 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 e895d7d7d7a..008eb5a429d 100644 --- a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp +++ b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp @@ -75,7 +75,7 @@ codet create_array_with_type_body( code_blockt code_block; // Declare new_array temporary: - code_block.add(code_declt(new_array_symbol_expr)); + code_block.add(code_frontend_declt(new_array_symbol_expr)); // new_array = new Object[length]; side_effect_exprt new_array_expr{ diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h index c5e33176668..25f4b13ce72 100644 --- a/src/util/goto_instruction_code.h +++ b/src/util/goto_instruction_code.h @@ -189,6 +189,71 @@ inline code_deadt &to_code_dead(codet &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 +/// represented as `code_declt(sym)`. +class code_declt : public codet +{ +public: + explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {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, "declaration must have one operand"); + DATA_CHECK( + vm, + code.op0().id() == ID_symbol, + "declaring a non-symbol: " + + id2string(to_symbol_expr(code.op0()).get_identifier())); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_decl); +} + +inline void validate_expr(const code_declt &x) +{ + code_declt::check(x); +} + +inline const code_declt &to_code_decl(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_decl); + code_declt::check(code); + return static_cast(code); +} + +inline code_declt &to_code_decl(codet &code) +{ + PRECONDITION(code.get_statement() == ID_decl); + code_declt::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. diff --git a/src/util/std_code.h b/src/util/std_code.h index c19fdca005a..990a125b0e4 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -352,71 +352,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 `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 -/// represented as `code_declt(sym)`. -class code_declt:public codet -{ -public: - explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {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, "declaration must have one operand"); - DATA_CHECK( - vm, - code.op0().id() == ID_symbol, - "declaring a non-symbol: " + - id2string(to_symbol_expr(code.op0()).get_identifier())); - } -}; - -template <> -inline bool can_cast_expr(const exprt &base) -{ - return detail::can_cast_code_impl(base, ID_decl); -} - -inline void validate_expr(const code_declt &x) -{ - code_declt::check(x); -} - -inline const code_declt &to_code_decl(const codet &code) -{ - PRECONDITION(code.get_statement() == ID_decl); - code_declt::check(code); - return static_cast(code); -} - -inline code_declt &to_code_decl(codet &code) -{ - PRECONDITION(code.get_statement() == ID_decl); - code_declt::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 From 47a327718d5086b44a3d746ec730fa38e4d6a96c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 20 Oct 2021 13:50:08 +0100 Subject: [PATCH 3/3] introduce code_frontend_returnt This splits the classes that represent return statements in the frontends and the return instructions in goto instructions. They differ in semantics and in the invariants that they maintain. The goto instruction variant always has a return value. The constructors for creating that class without return value are removed. --- .../create_array_with_type_intrinsic.cpp | 2 +- .../java_bytecode_convert_method.cpp | 4 +- .../java_static_initializers.cpp | 7 ++- src/ansi-c/c_typecheck_base.h | 2 +- src/ansi-c/c_typecheck_code.cpp | 4 +- src/ansi-c/expr2c.cpp | 2 +- src/cpp/cpp_typecheck_compound_type.cpp | 4 +- src/cpp/parse.cpp | 2 +- src/goto-harness/recursive_initialization.cpp | 6 +- src/goto-instrument/contracts/contracts.cpp | 5 +- src/goto-programs/goto_convert.cpp | 9 +-- src/goto-programs/goto_convert_class.h | 2 +- src/jsil/jsil_parse_tree.cpp | 2 +- src/jsil/jsil_typecheck.cpp | 4 +- src/jsil/jsil_typecheck.h | 4 +- src/pointer-analysis/value_set.cpp | 9 +-- src/pointer-analysis/value_set_fi.cpp | 9 +-- src/util/goto_instruction_code.h | 57 +++++++++++++++++++ src/util/std_code.h | 25 ++++---- unit/goto-programs/goto_program_validate.cpp | 29 ---------- 20 files changed, 107 insertions(+), 81 deletions(-) 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 008eb5a429d..4477488b6c1 100644 --- a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp +++ b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp @@ -105,7 +105,7 @@ codet create_array_with_type_body( new_array_element_classid, old_array_element_classid)); // return new_array - code_block.add(code_returnt(new_array_symbol_expr)); + code_block.add(code_frontend_returnt(new_array_symbol_expr)); return std::move(code_block); } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 0a215a111c5..c68372823e8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1361,7 +1361,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) else if(bytecode == BC_return) { PRECONDITION(op.empty() && results.empty()); - c=code_returnt(); + c = code_frontend_returnt(); } else if(bytecode == patternt("?return")) { @@ -1370,7 +1370,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) PRECONDITION(op.size() == 1 && results.empty()); const exprt r = typecast_exprt::conditional_cast(op[0], method_return_type); - c=code_returnt(r); + c = code_frontend_returnt(r); } else if(bytecode == patternt("?astore")) { diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 2bb7d17b206..5e97df5a83f 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -590,7 +590,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( gen_clinit_eqexpr( clinit_thread_local_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE), - code_returnt()); + code_frontend_returnt()); function_body.add(std::move(conditional)); } @@ -651,7 +651,8 @@ code_blockt get_thread_safe_clinit_wrapper_body( // if(init_complete) return; { - code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt()); + code_ifthenelset conditional( + init_complete.symbol_expr(), code_frontend_returnt()); function_body.add(std::move(conditional)); } @@ -696,7 +697,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( gen_clinit_assign( clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE)); function_body.add(atomic_end); - function_body.add(code_returnt()); + function_body.add(code_frontend_returnt()); } return function_body; diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index a79aedae124..405940c81fe 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -139,7 +139,7 @@ class c_typecheck_baset: virtual void typecheck_gcc_computed_goto(codet &code); virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &); virtual void typecheck_gcc_local_label(codet &code); - virtual void typecheck_return(code_returnt &code); + virtual void typecheck_return(code_frontend_returnt &); virtual void typecheck_switch(codet &code); virtual void typecheck_while(code_whilet &code); virtual void typecheck_dowhile(code_dowhilet &code); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index ea180d4c5d3..7e46443a18f 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code) else if(statement==ID_continue) typecheck_continue(code); else if(statement==ID_return) - typecheck_return(to_code_return(code)); + typecheck_return(to_code_frontend_return(code)); else if(statement==ID_decl) typecheck_decl(code); else if(statement==ID_assign) @@ -643,7 +643,7 @@ void c_typecheck_baset::typecheck_start_thread(codet &code) typecheck_code(to_code(code.op0())); } -void c_typecheck_baset::typecheck_return(code_returnt &code) +void c_typecheck_baset::typecheck_return(code_frontend_returnt &code) { if(code.has_return_value()) { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 08224545c6a..ec245bfae89 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2680,7 +2680,7 @@ std::string expr2ct::convert_code_return( std::string dest=indent_str(indent); dest+="return"; - if(to_code_return(src).has_return_value()) + if(to_code_frontend_return(src).has_return_value()) dest+=" "+convert(src.op0()); dest+=';'; diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 700bc221c2c..e7c40d9d4b4 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -688,8 +688,8 @@ void cpp_typecheckt::typecheck_compound_declarator( { expr_call.type()=to_code_type(component.type()).return_type(); - func_symb.value = code_blockt{ - {code_returnt(already_typechecked_exprt{std::move(expr_call)})}}; + func_symb.value = code_blockt{{code_frontend_returnt( + already_typechecked_exprt{std::move(expr_call)})}}; } else { diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 7220976c641..0c2d629e00d 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -7350,7 +7350,7 @@ optionalt Parser::rStatement() lex.get_token(tk1); - code_returnt statement; + code_frontend_returnt statement; set_location(statement, tk1); if(lex.LookAhead(0)==';') diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index f9f75fc12ad..ce16ab6c6cf 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -239,7 +239,7 @@ code_blockt build_null_pointer(const symbol_exprt &result_symbol) const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)}; const code_assignt assign_null{dereference_exprt{result_symbol}, nullptr_expr}; - return code_blockt{{assign_null, code_returnt{}}}; + return code_blockt{{assign_null, code_frontend_returnt{}}}; } code_blockt recursive_initializationt::build_constructor_body( @@ -688,7 +688,7 @@ code_blockt recursive_initializationt::build_pointer_constructor( null_pointer_exprt nullptr_expr{pointer_type(type.subtype())}; const code_assignt assign_null{dereference_exprt{result}, nullptr_expr}; - code_blockt null_and_return{{assign_null, code_returnt{}}}; + code_blockt null_and_return{{assign_null, code_frontend_returnt{}}}; body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return}); const auto should_recurse_nondet = @@ -1034,7 +1034,7 @@ code_blockt recursive_initializationt::build_function_pointer_constructor( auto const condition = equal_exprt{ function_pointer_selector, from_integer(function_pointer_index, function_pointer_selector.type())}; - auto const then = code_blockt{{assign, code_returnt{}}}; + auto const then = code_blockt{{assign, code_frontend_returnt{}}}; body.add(code_ifthenelset{condition, then}); } else diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index b5e89c0063c..ce88275457b 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1074,7 +1074,7 @@ void code_contractst::add_contract_check( replace_symbolt common_replace; // decl ret - code_returnt return_stmt; + optionalt return_stmt; if(code_type.return_type() != empty_typet()) { symbol_exprt r = new_tmp_symbol( @@ -1178,7 +1178,8 @@ void code_contractst::add_contract_check( if(code_type.return_type() != empty_typet()) { - check.add(goto_programt::make_return(return_stmt, skip->source_location())); + check.add( + goto_programt::make_return(return_stmt.value(), skip->source_location())); } // prepend the new code to dest diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index e3b13f66a2d..3ff25835a38 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -470,7 +470,7 @@ void goto_convertt::convert( else if(statement==ID_break) convert_break(to_code_break(code), dest, mode); else if(statement==ID_return) - convert_return(to_code_return(code), dest, mode); + convert_return(to_code_frontend_return(code), dest, mode); else if(statement==ID_continue) convert_continue(to_code_continue(code), dest, mode); else if(statement==ID_goto) @@ -1258,7 +1258,7 @@ void goto_convertt::convert_break( } void goto_convertt::convert_return( - const code_returnt &code, + const code_frontend_returnt &code, goto_programt &dest, const irep_idt &mode) { @@ -1273,7 +1273,7 @@ void goto_convertt::convert_return( "return takes none or one operand", code.find_source_location()); - code_returnt new_code(code); + code_frontend_returnt new_code(code); if(new_code.has_return_value()) { @@ -1297,7 +1297,8 @@ void goto_convertt::convert_return( new_code.find_source_location()); // Now add a return node to set the return value. - dest.add(goto_programt::make_return(new_code, new_code.source_location())); + dest.add(goto_programt::make_return( + to_code_return(new_code), new_code.source_location())); } else { diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 54050055f2e..fc3554c5fb1 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -267,7 +267,7 @@ class goto_convertt:public messaget goto_programt &dest, const irep_idt &mode); void convert_return( - const code_returnt &code, + const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode); void convert_continue( diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp index 7d97b72651d..99f0bb68934 100644 --- a/src/jsil/jsil_parse_tree.cpp +++ b/src/jsil/jsil_parse_tree.cpp @@ -66,7 +66,7 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const static_cast(find(ID_value)))); irept returns(find(ID_return)); - code_returnt r(symbol_exprt::typeless(returns.get(ID_value))); + code_frontend_returnt r(symbol_exprt::typeless(returns.get(ID_value))); irept throws(find(ID_throw)); side_effect_expr_throwt t( diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 5d12ecbc6ac..997c939bd5f 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -637,7 +637,7 @@ void jsil_typecheckt::typecheck_code(codet &code) if(statement==ID_function_call) typecheck_function_call(to_code_function_call(code)); else if(statement==ID_return) - typecheck_return(to_code_return(code)); + typecheck_return(to_code_frontend_return(code)); else if(statement==ID_expression) { if(code.operands().size()!=1) @@ -678,7 +678,7 @@ void jsil_typecheckt::typecheck_code(codet &code) } } -void jsil_typecheckt::typecheck_return(code_returnt &code) +void jsil_typecheckt::typecheck_return(code_frontend_returnt &code) { if(code.has_return_value()) typecheck_expr(code.return_value()); diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h index 4d66240758a..64b2e362b5a 100644 --- a/src/jsil/jsil_typecheck.h +++ b/src/jsil/jsil_typecheck.h @@ -20,7 +20,7 @@ Author: Michael Tautschnig, tautschn@amazon.com class code_assignt; class code_function_callt; class code_ifthenelset; -class code_returnt; +class code_frontend_returnt; class code_try_catcht; class codet; class message_handlert; @@ -89,7 +89,7 @@ class jsil_typecheckt:public typecheckt void typecheck_expr_main(exprt &expr); void typecheck_code(codet &code); void typecheck_function_call(code_function_callt &function_call); - void typecheck_return(code_returnt &code); + void typecheck_return(code_frontend_returnt &); void typecheck_block(codet &code); void typecheck_ifthenelse(code_ifthenelset &code); void typecheck_assign(code_assignt &code); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 6554aa9132e..1767fde029c 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1582,12 +1582,9 @@ void value_sett::apply_code_rec( { const code_returnt &code_return = to_code_return(code); // this is turned into an assignment - if(code_return.has_return_value()) - { - symbol_exprt lhs( - "value_set::return_value", code_return.return_value().type()); - assign(lhs, code_return.return_value(), ns, false, false); - } + symbol_exprt lhs( + "value_set::return_value", code_return.return_value().type()); + assign(lhs, code_return.return_value(), ns, false, false); } else if(statement==ID_array_set) { diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 73e406a5cc5..d4d960a5a6b 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1378,12 +1378,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns) { const code_returnt &code_return = to_code_return(code); // this is turned into an assignment - if(code_return.has_return_value()) - { - std::string rvs="value_set::return_value"+std::to_string(from_function); - symbol_exprt lhs(rvs, code_return.return_value().type()); - assign(lhs, code_return.return_value(), ns); - } + std::string rvs = "value_set::return_value" + std::to_string(from_function); + symbol_exprt lhs(rvs, code_return.return_value().type()); + assign(lhs, code_return.return_value(), ns); } else if(statement==ID_fence) { diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h index 25f4b13ce72..d02fa3ae328 100644 --- a/src/util/goto_instruction_code.h +++ b/src/util/goto_instruction_code.h @@ -479,4 +479,61 @@ inline void validate_expr(const code_outputt &output) code_outputt::check(output); } +/// \ref codet representation of a "return from a function" statement. +class code_returnt : public codet +{ +public: + explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)}) + { + } + + const exprt &return_value() const + { + return op0(); + } + + exprt &return_value() + { + return op0(); + } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand"); + } + +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_return); +} + +inline void validate_expr(const code_returnt &x) +{ + code_returnt::check(x); +} + +inline const code_returnt &to_code_return(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_return); + code_returnt::check(code); + return static_cast(code); +} + +inline code_returnt &to_code_return(codet &code) +{ + PRECONDITION(code.get_statement() == ID_return); + code_returnt::check(code); + return static_cast(code); +} + #endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H diff --git a/src/util/std_code.h b/src/util/std_code.h index 990a125b0e4..991ce23dd75 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -902,14 +902,14 @@ inline code_gotot &to_code_goto(codet &code) } /// \ref codet representation of a "return from a function" statement. -class code_returnt:public codet +class code_frontend_returnt : public codet { public: - code_returnt() : codet(ID_return, {nil_exprt()}) + code_frontend_returnt() : codet(ID_return, {nil_exprt()}) { } - explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)}) + explicit code_frontend_returnt(exprt _op) : codet(ID_return, {std::move(_op)}) { } @@ -942,28 +942,29 @@ class code_returnt:public codet using codet::op3; }; -template<> inline bool can_cast_expr(const exprt &base) +template <> +inline bool can_cast_expr(const exprt &base) { return detail::can_cast_code_impl(base, ID_return); } -inline void validate_expr(const code_returnt &x) +inline void validate_expr(const code_frontend_returnt &x) { - code_returnt::check(x); + code_frontend_returnt::check(x); } -inline const code_returnt &to_code_return(const codet &code) +inline const code_frontend_returnt &to_code_frontend_return(const codet &code) { PRECONDITION(code.get_statement() == ID_return); - code_returnt::check(code); - return static_cast(code); + code_frontend_returnt::check(code); + return static_cast(code); } -inline code_returnt &to_code_return(codet &code) +inline code_frontend_returnt &to_code_frontend_return(codet &code) { PRECONDITION(code.get_statement() == ID_return); - code_returnt::check(code); - return static_cast(code); + code_frontend_returnt::check(code); + return static_cast(code); } /// \ref codet representation of a label for branch targets. diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 58fc65bb691..6c35b8e3868 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -185,35 +185,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") } } - /// check_returns_removed() - WHEN( - "not all returns have been removed - an instruction is of type " - "'return'") - { - THEN("fail!") - { - goto_convert(goto_model, null_message_handler); - - auto &function_map = goto_model.goto_functions.function_map; - auto it = function_map.find("g"); - auto &instructions = it->second.body.instructions; - instructions.insert( - instructions.begin(), goto_programt::make_return(code_returnt())); - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst ::set_optionst::all_false}; - - validation_options.check_returns_removed = true; - - REQUIRE_THROWS_AS( - validate_goto_model( - goto_model.goto_functions, - validation_modet::EXCEPTION, - validation_options), - incorrect_goto_program_exceptiont); - } - } - WHEN("not all returns have been removed - a function call lhs is not nil") { // int h();