|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Data structures representing statements in a program |
| 4 | +
|
| 5 | +Author: Daniel Kroening, kroening@kroening.com |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#ifndef CPROVER_UTIL_STD_CODE_BASE_H |
| 10 | +#define CPROVER_UTIL_STD_CODE_BASE_H |
| 11 | + |
| 12 | +#include "expr_cast.h" |
| 13 | +#include "invariant.h" |
| 14 | +#include "std_types.h" |
| 15 | +#include "validate.h" |
| 16 | +#include "validate_code.h" |
| 17 | + |
| 18 | +/// Data structure for representing an arbitrary statement in a program. Every |
| 19 | +/// specific type of statement (e.g. block of statements, assignment, |
| 20 | +/// if-then-else statement...) is represented by a subtype of `codet`. |
| 21 | +/// `codet`s are represented to be subtypes of \ref exprt since statements can |
| 22 | +/// occur in an expression context in C: for example, the assignment `x = y;` |
| 23 | +/// is an expression with return value `y`. For other types of statements in an |
| 24 | +/// expression context, see e.g. |
| 25 | +/// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html. |
| 26 | +/// To distinguish a `codet` from other [exprts](\ref exprt), we set its |
| 27 | +/// [id()](\ref irept::id) to `ID_code`. To distinguish different types of |
| 28 | +/// `codet`, we use a named sub `ID_statement`. |
| 29 | +class codet : public exprt |
| 30 | +{ |
| 31 | +public: |
| 32 | + /// \param statement: Specifies the type of the `codet` to be constructed, |
| 33 | + /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a |
| 34 | + /// \ref code_frontend_assignt. |
| 35 | + explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet()) |
| 36 | + { |
| 37 | + set_statement(statement); |
| 38 | + } |
| 39 | + |
| 40 | + codet(const irep_idt &statement, source_locationt loc) |
| 41 | + : exprt(ID_code, empty_typet(), std::move(loc)) |
| 42 | + { |
| 43 | + set_statement(statement); |
| 44 | + } |
| 45 | + |
| 46 | + /// \param statement: Specifies the type of the `codet` to be constructed, |
| 47 | + /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a |
| 48 | + /// \ref code_frontend_assignt. |
| 49 | + /// \param _op: any operands to be added |
| 50 | + explicit codet(const irep_idt &statement, operandst _op) : codet(statement) |
| 51 | + { |
| 52 | + operands() = std::move(_op); |
| 53 | + } |
| 54 | + |
| 55 | + codet(const irep_idt &statement, operandst op, source_locationt loc) |
| 56 | + : codet(statement, std::move(loc)) |
| 57 | + { |
| 58 | + operands() = std::move(op); |
| 59 | + } |
| 60 | + |
| 61 | + void set_statement(const irep_idt &statement) |
| 62 | + { |
| 63 | + set(ID_statement, statement); |
| 64 | + } |
| 65 | + |
| 66 | + const irep_idt &get_statement() const |
| 67 | + { |
| 68 | + return get(ID_statement); |
| 69 | + } |
| 70 | + |
| 71 | + codet &first_statement(); |
| 72 | + const codet &first_statement() const; |
| 73 | + codet &last_statement(); |
| 74 | + const codet &last_statement() const; |
| 75 | + |
| 76 | + /// Check that the code statement is well-formed (shallow checks only, i.e., |
| 77 | + /// enclosed statements, subexpressions, etc. are not checked) |
| 78 | + /// |
| 79 | + /// Subclasses may override this function to provide specific well-formedness |
| 80 | + /// checks for the corresponding types. |
| 81 | + /// |
| 82 | + /// The validation mode indicates whether well-formedness check failures are |
| 83 | + /// reported via DATA_INVARIANT violations or exceptions. |
| 84 | + static void check(const codet &, const validation_modet) |
| 85 | + { |
| 86 | + } |
| 87 | + |
| 88 | + /// Check that the code statement is well-formed, assuming that all its |
| 89 | + /// enclosed statements, subexpressions, etc. have all ready been checked for |
| 90 | + /// well-formedness. |
| 91 | + /// |
| 92 | + /// Subclasses may override this function to provide specific well-formedness |
| 93 | + /// checks for the corresponding types. |
| 94 | + /// |
| 95 | + /// The validation mode indicates whether well-formedness check failures are |
| 96 | + /// reported via DATA_INVARIANT violations or exceptions. |
| 97 | + static void validate( |
| 98 | + const codet &code, |
| 99 | + const namespacet &, |
| 100 | + const validation_modet vm = validation_modet::INVARIANT) |
| 101 | + { |
| 102 | + check_code(code, vm); |
| 103 | + } |
| 104 | + |
| 105 | + /// Check that the code statement is well-formed (full check, including checks |
| 106 | + /// of all subexpressions) |
| 107 | + /// |
| 108 | + /// Subclasses may override this function to provide specific well-formedness |
| 109 | + /// checks for the corresponding types. |
| 110 | + /// |
| 111 | + /// The validation mode indicates whether well-formedness check failures are |
| 112 | + /// reported via DATA_INVARIANT violations or exceptions. |
| 113 | + static void validate_full( |
| 114 | + const codet &code, |
| 115 | + const namespacet &, |
| 116 | + const validation_modet vm = validation_modet::INVARIANT) |
| 117 | + { |
| 118 | + check_code(code, vm); |
| 119 | + } |
| 120 | + |
| 121 | + using exprt::op0; |
| 122 | + using exprt::op1; |
| 123 | + using exprt::op2; |
| 124 | + using exprt::op3; |
| 125 | +}; |
| 126 | + |
| 127 | +namespace detail // NOLINT |
| 128 | +{ |
| 129 | +template <typename Tag> |
| 130 | +inline bool can_cast_code_impl(const exprt &expr, const Tag &tag) |
| 131 | +{ |
| 132 | + if(const auto ptr = expr_try_dynamic_cast<codet>(expr)) |
| 133 | + { |
| 134 | + return ptr->get_statement() == tag; |
| 135 | + } |
| 136 | + return false; |
| 137 | +} |
| 138 | + |
| 139 | +} // namespace detail |
| 140 | + |
| 141 | +template <> |
| 142 | +inline bool can_cast_expr<codet>(const exprt &base) |
| 143 | +{ |
| 144 | + return base.id() == ID_code; |
| 145 | +} |
| 146 | + |
| 147 | +// to_code has no validation other than checking the id(), so no validate_expr |
| 148 | +// is provided for codet |
| 149 | + |
| 150 | +inline const codet &to_code(const exprt &expr) |
| 151 | +{ |
| 152 | + PRECONDITION(expr.id() == ID_code); |
| 153 | + return static_cast<const codet &>(expr); |
| 154 | +} |
| 155 | + |
| 156 | +inline codet &to_code(exprt &expr) |
| 157 | +{ |
| 158 | + PRECONDITION(expr.id() == ID_code); |
| 159 | + return static_cast<codet &>(expr); |
| 160 | +} |
| 161 | + |
| 162 | +#endif // CPROVER_UTIL_STD_CODE_BASE_H |
0 commit comments