CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_root_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: March 2023
8
9\*******************************************************************/
10
11#include "dfcc_root_object.h"
12
13#include <util/byte_operators.h>
14#include <util/cprover_prefix.h>
15#include <util/expr.h>
16#include <util/expr_util.h>
17#include <util/pointer_expr.h>
18#include <util/std_code.h>
19
21
23static void
24root_objects_rec(const exprt &expr, std::unordered_set<exprt, irep_hash> &dest)
25{
26 if(expr.id() == ID_symbol)
27 {
28 dest.insert(expr);
29 }
30 else if(expr.id() == ID_index)
31 {
32 root_objects_rec(to_index_expr(expr).array(), dest);
33 }
34 else if(expr.id() == ID_member)
35 {
36 const typet &type = to_member_expr(expr).struct_op().type();
38 type.id() == ID_struct || type.id() == ID_struct_tag ||
39 type.id() == ID_union || type.id() == ID_union_tag,
40 "unexpected assignment to member of '" + type.id_string() + "'");
41 root_objects_rec(to_member_expr(expr).compound(), dest);
42 }
43 else if(expr.id() == ID_if)
44 {
45 root_objects_rec(to_if_expr(expr).true_case(), dest);
46 root_objects_rec(to_if_expr(expr).false_case(), dest);
47 }
48 else if(expr.id() == ID_typecast)
49 {
50 root_objects_rec(to_typecast_expr(expr).op(), dest);
51 }
52 else if(
55 {
56 root_objects_rec(to_byte_extract_expr(expr).op(), dest);
57 }
58 else if(expr.id() == ID_complex_real)
59 {
60 root_objects_rec(to_complex_real_expr(expr).op(), dest);
61 }
62 else if(expr.id() == ID_complex_imag)
63 {
64 root_objects_rec(to_complex_imag_expr(expr).op(), dest);
65 }
66 else if(const auto &deref = expr_try_dynamic_cast<dereference_exprt>(expr))
67 {
68 // normalise the dereferenced pointer into `pointer + offset`, extract
69 // pointer expression and try some simplifications
70 const exprt &pointer = pointer_arithmetict(deref->pointer()).pointer;
71 const source_locationt source_location = expr.source_location();
72 if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>(pointer))
73 {
74 // split on disjunctions
75 // *(c ? true_case : false_case) => rec(*true_case); rec(*false_case)
76 dereference_exprt if_true(if_expr->true_case());
77 if_true.add_source_location() = source_location;
79 dereference_exprt if_false(if_expr->false_case());
80 if_false.add_source_location() = source_location;
82 }
83 else if(
84 const auto &address_of_expr =
86 {
87 // *(&object + offset) => rec(object)
89 }
90 else
91 {
92 // simplify *(pointer + offset) to *pointer and stop here
93 dereference_exprt deref(pointer);
94 deref.add_source_location() = source_location;
95 dest.insert(deref);
96 }
97 }
98 else
99 {
100 // Stop here for anything else.
101 dest.insert(expr);
102 }
103}
104
107static exprt slice_op_to_deref(const exprt &expr)
108{
109 if(
110 const auto &function_call_expr =
112 {
113 auto function_expr = function_call_expr->function();
114 INVARIANT(
115 function_expr.id() == ID_symbol,
116 "no function pointer calls in loop assigns clause targets");
117 auto function_id = to_symbol_expr(function_expr).get_identifier();
118 INVARIANT(
119 function_id == CPROVER_PREFIX "assignable" ||
120 function_id == CPROVER_PREFIX "object_whole" ||
121 function_id == CPROVER_PREFIX "object_from" ||
122 function_id == CPROVER_PREFIX "object_upto",
123 "can only handle built-in function calls in assigns clause targets");
124 return dereference_exprt(
125 skip_typecast(function_call_expr->arguments().at(0)));
126 }
127 else
128 {
129 return expr;
130 }
131}
132
133std::unordered_set<exprt, irep_hash> dfcc_root_objects(const exprt &expr)
134{
135 std::unordered_set<exprt, irep_hash> result;
136 root_objects_rec(slice_op_to_deref(expr), result);
137 return result;
138}
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:231
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
static exprt slice_op_to_deref(const exprt &expr)
Translates object slice expressions found in assigns clause targets to dereference expressions so tha...
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
static void root_objects_rec(const exprt &expr, std::unordered_set< exprt, irep_hash > &dest)
Recursively computes a set of root object expressions for expr.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
API to expression classes for Pointers.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272