- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include "goto-programs/goto_binary_reader.h"#include <util/base/stack_budget.h>#include "irep2/irep2_expr.h"#include <util/lang/c_builtins.h>#include <util/lang/c_sizeof.h>#include <util/lang/c_typecast.h>#include <util/lang/c_types.h>#include <util/lang/exception_specification.h>#include <util/lang/python_types.h>#include <util/irep/std_code.h>#include <util/config/config.h>#include <irep2/irep2_utils.h>#include <util/message/format.h>#include <util/arith/arith_tools.h>#include <util/irep/migrate.h>#include <util/symtab/namespace.h>#include <set>#include <util/base/prefix.h>#include <util/irep/pad_names.h>#include <util/expr/string_constant.h>#include <util/expr/type_byte_size.h>#include <unordered_map>Typedefs | |
| using | back_cachet |
| Legacy forms of migrated aggregate types, keyed on node identity. | |
Functions | |
| expr2tc | invoke_intrinsic (const std::string &name, const typet &type, const std::vector< exprt > &args) |
| An ESBMC intrinsic invoked from an expression position, as a sideeffect2t of allockind::function_call carrying the call's result type. | |
| static void | restore_padding_flag (struct_union_typet::componentt &component) |
| static struct_union_typet::componentst | migrate_components_back (const std::vector< type2tc > &members, const std::vector< irep_idt > &names, const std::vector< irep_idt > &pretty_names, const std::vector< irep_idt > &base_names) |
| static code_typet::argumentst | migrate_arguments_back (const code_type2t &ref2) |
| const BigInt & | binary2bigint (irep_idt binary, bool is_signed) |
| static expr2tc | fixup_containerof_in_sizeof (const expr2tc &_expr) |
| static unsigned | get_pragma_unroll (const exprt &expr) |
| static pointer_ref_kindt | pointer_ref_kind (const typet &type) |
| static BigInt | explicit_alignment (const typet &type) |
| An explicit alignas in bytes, or zero when the record has none. | |
| static bool | migrates_to_empty (const typet &type) |
| Type ids that carry no storage and so migrate to the empty type: an unset or nil id; an ellipsis, which is not a type at all; clang's BoundMember, the type of obj.
| |
| static std::vector< irep_idt > | struct_bases (const typet &type) |
| static irep_idt | ctor_dtor_marker (const typet &ret) |
| static void | migrate_exception_spec (const typet &type, irep_idt &kind, std::vector< irep_idt > &types, std::vector< type2tc > &decl) |
| static std::vector< expr2tc > | migrate_arg_defaults (const code_typet::argumentst &old_args) |
| static type2tc | migrate_type0 (const typet &type) |
| type2tc | migrate_type (const typet &type) |
| type2tc | migrate_symbol_type (const symbolt &sym) |
| void | migrate_symbol_value (const symbolt &sym, expr2tc &dest) |
| void | set_symbol_type (symbolt &sym, const type2tc &t) |
| expr2tc | symbol_expr2tc (const symbolt &sym) |
| expr2tc | side_effect_function_call2tc (const type2tc &return_type, const expr2tc &function, const std::vector< expr2tc > &arguments) |
| static const typet & | decide_on_expr_type (const exprt &side1, const exprt &side2) |
| static exprt | splice_expr (const exprt &expr) |
| static void | splice_expr (const exprt &expr, expr2tc &new_expr_ref) |
| static void | promote_complex_operand (const type2tc &t, expr2tc &op) |
| Clang does not cast a binary operator's real operand to complex – it hands over double + _Complex double and leaves the promotion to the consumer, so clang_c_adjust's complex lowering pairs the real with a zero imaginary part before anything migrates. | |
| static void | decay_array_operand (expr2tc &op) |
| C11 6.3.2.1p3. | |
| static void | convert_operand_pair (const exprt &expr, expr2tc &arg1, expr2tc &arg2) |
| static bool | handle_introspection_expr (const exprt &expr, expr2tc &new_expr_ref) |
| expr2tc | sym_name_to_symbol (const irep_idt &init, const type2tc &type) |
| static expr2tc | migrate_sizeof (const exprt &expr) |
| sizeof(T): op0 (a type_exprt) carries the measured type T, op1 the eagerly-computed byte-size value. | |
| static expr2tc | migrate_builtin_va_arg (const exprt &expr) |
| clang_c_adjust::adjust_builtin_va_arg lowers this to a __ESBMC_va_arg call, and IREP2 has no builtin_va_arg kind – so under –clang-c-irep2-adjust-only the node would die before anything could rewrite it. | |
| static expr2tc | migrate_rounding_mode (const exprt &expr) |
| The rounding mode a legacy ieee_* node carries. | |
| static bool | migrate_ieee_arith_2op (const exprt &expr, expr2tc &new_expr_ref) |
| The two-operand IEEE nodes migrate identically: an n-ary irep splices into nested binaries, and the rounding mode comes from the irep's attribute when it carries one. | |
| static void | coerce_ternary_branch (expr2tc &branch, const type2tc &type) |
| Bring one ternary branch to the ternary's own type. | |
| static expr2tc | coerce_to_type (const expr2tc &e, const type2tc &type) |
| static expr2tc | migrate_pointer_ok (const exprt &expr) |
| _CPROVER{r,w,rw}_ok(p, n): the n bytes from p lie inside one live object. | |
| static const exprt & | cpp_new_size (const exprt &expr) |
| cpp_new[] hides the array size in a size field. | |
| static bool | migrate_before_dispatch (const exprt &expr, expr2tc &new_expr_ref) |
| The two forms recognised before the id dispatch below: a nil expression, and a node carrying a #derived_to_base marker. | |
| static bool | migrate_right_shift (const exprt &expr, expr2tc &new_expr_ref) |
| The right-shift family. | |
| static void | migrate_cpp_delete (const exprt &expr, std::vector< expr2tc > &args) |
| static void | migrate_cpp_new (const exprt &expr, expr2tc &thesize, std::vector< expr2tc > &args) |
| static void | wrap_padded_union_member (const type2tc &type, const irep_idt &component, std::vector< expr2tc > &members) |
| static bool | is_all_zero_bytes (const expr2tc &e) |
| static expr2tc | union_member_update (const type2tc &type, const expr2tc &source, const expr2tc &offs, const expr2tc &update) |
| static expr2tc | byte_update_bytes (const type2tc &type, expr2tc result, const expr2tc &offs, const expr2tc &update, bool big_endian) |
| static expr2tc | migrate_byte_update (const type2tc &type, const expr2tc &source, const expr2tc &offs, const expr2tc &update, bool big_endian) |
| void | migrate_expr (const exprt &expr, expr2tc &new_expr_ref) |
| void | migrate_type_back_cache_clear () |
| static void | migrate_struct_bases_back (const struct_type2t &ref, typet &type) |
| static void | migrate_ctor_dtor_marker_back (const code_type2t &ref, code_typet &code) |
| static void | migrate_exception_spec_back (const code_type2t &ref, code_typet &code) |
| static typet | migrate_type_back_uncached (const type2tc &ref) |
| typet | migrate_type_back (const type2tc &ref) |
| static void | restore_type_comments (typet &t, bool constant_qualified, const irep_idt &cpp_type) |
| #constant and #cpp_type are comment fields: writing them when unset still inserts the key, which the printer then reads back as a qualifier or a spelling (§158). | |
| static void | set_implicit_flag (exprt &e, bool implicit) |
| static const char * | back_sideeffect_statement (sideeffect2t::allockind kind) |
| static void | back_sideeffect_cpp_delete (const sideeffect2t &ref2, exprt &theexpr) |
| static void | back_sideeffect_cpp_new (const sideeffect2t &ref2, exprt &theexpr) |
| static void | back_sideeffect_operands (const sideeffect2t &ref2, exprt &theexpr) |
| static exprt | back_sideeffect (const expr2tc &ref) |
| static exprt | with_cformat (exprt e, const irep_idt &cformat) |
| Restores #cformat only when there is one: it is a comment field, but an empty one still makes c_expr2string prefer it over deriving the text, so it would print nothing at all (§63). | |
| static exprt | migrate_expr_back_dispatch (const expr2tc &ref) |
| exprt | migrate_expr_back (const expr2tc &ref) |
| static exprt | back_typecast (const typecast2t &ref2) |
| A cast's legacy form, with the base-conversion markers the adjust passes dispatch on. | |
| static exprt | migrate_expr_back_rest6 (const expr2tc &ref) |
| static exprt | migrate_expr_back_rest5 (const expr2tc &ref) |
| static exprt | migrate_expr_back_rest4 (const expr2tc &ref) |
| static exprt | migrate_expr_back_rest3 (const expr2tc &ref) |
| static exprt | migrate_expr_back_rest2 (const expr2tc &ref) |
| void | migrate_census (const contextt &context) |
| Migrate every symbol's type, and its value where it has one, and report what could not be represented. | |
Variables | |
| const namespacet * | migrate_namespace_lookup = nullptr |
| static std::map< irep_idt, BigInt > | bin2int_map_signed |
| static std::map< irep_idt, BigInt > | bin2int_map_unsigned |
| static std::mutex | bin2int_map_signed_mutex |
| static std::mutex | bin2int_map_unsigned_mutex |
| static back_cachet | back_cache |
| static constexpr size_t | back_cache_capacity = 4096 |
| using back_cachet |
Legacy forms of migrated aggregate types, keyed on node identity.
Identity keying is sound because the entry pins the type2tc, so the node cannot be freed and its address reused, and irep_container is copy-on-write: a node the cache references detaches on write rather than mutating in place. migrate_type_back() reads no globals, so the legacy form is a pure function of the node – unlike the forward direction, which reads config and migrate_namespace_lookup, so this key scheme must not be copied to it. The pinned type2tc keeps the key valid; the typet is the memoised result.
|
static |
|
static |
|
static |
|
static |
|
static |
A cast's legacy form, with the base-conversion markers the adjust passes dispatch on.
A same-type cast carrying #derived_to_base is the wrapper migrate_expr builds for a marker on a node that is not a cast, so the marker goes back on the node itself rather than leaving an identity cast behind.
|
static |
Bring one ternary branch to the ternary's own type.
C11 6.3.2.1p3: an array operand converts to a pointer to its first element. That is not a cast of the array object, and the frontend's own conversion (c_typecastt::do_typecast) spells it &a[0]; coerced as a plain typecast the node reaches the encoder as typecast(array, pointer) and aborts it.
cpp_new[] hides the array size in a size field.
The frontend stores it under "size" (size_irep); the pipeline later mirrors it into "#size" (cmt_size). Under –irep2-bodies the body is migrated before that mirroring runs, so "#size" is still empty – read "size" then, or the size is silently dropped. A present-but-empty irep is a third state is_not_nil() reports as present, so the choice is made on the id.
|
static |
C11 6.3.2.1p3.
clang_c_convert drops CK_ArrayToPointerDecay and leaves clang_c_adjust to insert the &a[0], so an expression migrated before that pass – which –clang-c-irep2-adjust-only does – still carries the array, and add2t/sub2t assert on it (esbmc/esbmc#4715).
An explicit alignas in bytes, or zero when the record has none.
It travels as an alignment sub-irep and add_padding reads it back to size a record's trailing pad (docs/roadmap/scope-clang-cpp-irep2.md §7.4).
|
static |
|
inline |
An ESBMC intrinsic invoked from an expression position, as a sideeffect2t of allockind::function_call carrying the call's result type.
It has to be an expression node, not a code_function_call2t: the latter is void-typed, and an enclosing arithmetic constructor asserts on an operand whose type is not its own – CBMC serialises object_size under +, so the abort landed while the binary was still being read, long before lift_call_expressions() gets a chance to hoist the call out (#7410).
|
static |
|
static |
The two forms recognised before the id dispatch below: a nil expression, and a node carrying a #derived_to_base marker.
That marker names whichever node is being converted, and that is almost never a cast: over regression/esbmc-cpp it lands on a symbol 32474 times and on a typecast 58. IREP2 has nowhere to hang a flag on an arbitrary node, so it becomes a same-type typecast2t around it – the identity – which back_typecast unwraps. Dropping it loses the base displacement and silently proves false assertions (docs/roadmap/scope-clang-cpp-irep2.md §3.12).
clang_c_adjust::adjust_builtin_va_arg lowers this to a __ESBMC_va_arg call, and IREP2 has no builtin_va_arg kind – so under –clang-c-irep2-adjust-only the node would die before anything could rewrite it.
The lowering is a pure function of the node's type and operand, which migration may compute (§72, §80). The callee symbol is declared by clang_c_adjust_irep2::declare_implicit_callee, and goto_convert's __ESBMC_va_arg arm (builtin_functions.cpp) enforces the one-argument contract and settles the operand's final shape. The normal pipeline adjusts first and never reaches this function.
|
static |
| void migrate_census | ( | const contextt & | context | ) |
Migrate every symbol's type, and its value where it has one, and report what could not be represented.
Migration signals failure by throwing a std::string, so each symbol is wrapped: one unrepresentable construct names itself and the walk continues, which is what makes this a census rather than a bisection. Walks the whole linked context, operational models included, which is the set goto_convert migrates anyway.
Frontend-agnostic on purpose: clang-cpp and solidity share one definition, so a census taken on either is the same measurement (docs/roadmap/scope-solidity-irep2.md §3, step S.2).
|
static |
|
static |
|
static |
|
static |
|
static |
The two-operand IEEE nodes migrate identically: an n-ary irep splices into nested binaries, and the rounding mode comes from the irep's attribute when it carries one.
False when expr is not one of them.
_CPROVER{r,w,rw}_ok(p, n): the n bytes from p lie inside one live object.
Migrating these to true made every assertion over them pass vacuously – CBMC refutes __CPROVER_r_ok(malloc(8), 16) and ESBMC proved it. ESBMC draws no read/write distinction (it models no read-only storage), so all three get the same encoding.
The right-shift family.
lshr and ashr name their kind; the Solidity converter also emits a kind-less shr for >>, and IREP2 has no node for it. clang_c_adjust resolves that one by the left operand's signedness before anything migrates, but –clang-cpp-irep2-adjust-only replaces that pass, so the resolution belongs here (docs/roadmap/scope-solidity-irep2.md §7.21). The three are extracted together because migrate_expr is over the complexity gate: an arm added inline fails it.
The rounding mode a legacy ieee_* node carries.
The frontends leave it implicit on most of them, in which case it is the global symbol.
sizeof(T): op0 (a type_exprt) carries the measured type T, op1 the eagerly-computed byte-size value.
Both become reflected sizeof2t fields, replacing the legacy sizeof-type side channel (esbmc/esbmc#5337).
|
static |
| void migrate_type_back_cache_clear | ( | ) |
Type ids that carry no storage and so migrate to the empty type: an unset or nil id; an ellipsis, which is not a type at all; clang's BoundMember, the type of obj.
*pmf before it is called, which is a placeholder rather than storage – clang_c_adjust::adjust_ptr_mem replaces the whole node with the member function, and a ptr_mem2t typed empty is exactly that placeholder, a pointer-to-*data*-member selection carrying the member's own type (docs/roadmap/scope-clang-cpp-irep2.md §7.5); and the return types of a destructor and of a constructor, which is a void method on an existing object rather than something that returns a value.
|
static |
Clang does not cast a binary operator's real operand to complex – it hands over double + _Complex double and leaves the promotion to the consumer, so clang_c_adjust's complex lowering pairs the real with a zero imaginary part before anything migrates.
Under –clang-c-irep2-adjust-only that pass does not run and the mixed node reaches the arith constructors, whose width assertion fires before clang_c_adjust_irep2 can lower it. The promotion is a pure function of the node's type and the operand, so migration may do it (§80).
|
static |
#constant and #cpp_type are comment fields: writing them when unset still inserts the key, which the printer then reads back as a qualifier or a spelling (§158).
| expr2tc side_effect_function_call2tc | ( | const type2tc & | return_type, |
| const expr2tc & | function, | ||
| const std::vector< expr2tc > & | arguments ) |
|
static |
Restores #cformat only when there is one: it is a comment field, but an empty one still makes c_expr2string prefer it over deriving the text, so it would print nothing at all (§63).
|
static |
|
thread_localstatic |
|
staticconstexpr |
|
static |
|
static |
|
thread_local |
1.15.0