Skip to content

Commit 8fa0c36

Browse files
Remi Delmasqinheping
Remi Delmas
authored and
qinheping
committed
CONTRACTS: functions to compute root objects
Alternative implementation of `root_object` supporting ternary operators in assignment or call LHS expressions, and object slice expressions in assigns clause targets.
1 parent 47e6e92 commit 8fa0c36

File tree

3 files changed

+236
-0
lines changed

3 files changed

+236
-0
lines changed

‎src/goto-instrument/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ SRC = accelerate/accelerate.cpp \
2121
contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
2222
contracts/dynamic-frames/dfcc_contract_mode.cpp \
2323
contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \
24+
contracts/dynamic-frames/dfcc_root_object.cpp \
2425
contracts/dynamic-frames/dfcc_library.cpp \
2526
contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
2627
contracts/dynamic-frames/dfcc_is_fresh.cpp \

‎src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp

+188
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking
4+
5+
Author: Remi Delmas, [email protected]
6+
7+
Date: 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/message.h>
18+
#include <util/namespace.h>
19+
#include <util/pointer_expr.h>
20+
#include <util/std_code.h>
21+
22+
#include <goto-programs/pointer_arithmetic.h>
23+
24+
#include <langapi/language_util.h>
25+
26+
/// Recursively computes a set of root object expressions for \p expr.
27+
static void root_objects_rec(
28+
const exprt &expr,
29+
const namespacet &ns,
30+
messaget log,
31+
std::unordered_set<exprt, irep_hash> &dest)
32+
{
33+
if(expr.id() == ID_symbol)
34+
{
35+
dest.insert(expr);
36+
}
37+
else if(expr.id() == ID_index)
38+
{
39+
root_objects_rec(to_index_expr(expr).array(), ns, log, dest);
40+
}
41+
else if(expr.id() == ID_member)
42+
{
43+
const typet &type = to_member_expr(expr).struct_op().type();
44+
if(
45+
type.id() == ID_struct || type.id() == ID_struct_tag ||
46+
type.id() == ID_union || type.id() == ID_union_tag)
47+
{
48+
root_objects_rec(to_member_expr(expr).compound(), ns, log, dest);
49+
}
50+
else
51+
{
52+
throw unsupported_operation_exceptiont(
53+
"unexpected assignment to member of '" + type.id_string() + "'");
54+
}
55+
}
56+
else if(expr.id() == ID_if)
57+
{
58+
root_objects_rec(to_if_expr(expr).true_case(), ns, log, dest);
59+
root_objects_rec(to_if_expr(expr).false_case(), ns, log, dest);
60+
}
61+
else if(expr.id() == ID_typecast)
62+
{
63+
root_objects_rec(to_typecast_expr(expr).op(), ns, log, dest);
64+
}
65+
else if(
66+
expr.id() == ID_byte_extract_little_endian ||
67+
expr.id() == ID_byte_extract_big_endian)
68+
{
69+
root_objects_rec(to_byte_extract_expr(expr).op(), ns, log, dest);
70+
}
71+
else if(expr.id() == ID_complex_real)
72+
{
73+
root_objects_rec(to_complex_real_expr(expr).op(), ns, log, dest);
74+
}
75+
else if(expr.id() == ID_complex_imag)
76+
{
77+
root_objects_rec(to_complex_imag_expr(expr).op(), ns, log, dest);
78+
}
79+
else if(
80+
const auto &deref =
81+
expr_try_dynamic_cast<dereference_exprt>(skip_typecast(expr)))
82+
{
83+
// normalise the dereferenced pointer into `pointer + offset`, extract
84+
// pointer expression and try some simplifications
85+
const exprt &pointer = pointer_arithmetict(deref->pointer()).pointer;
86+
const source_locationt source_location = expr.source_location();
87+
if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>(pointer))
88+
{
89+
// split on disjunctions
90+
// *(c ? true_case : false_case) => rec(*true_case); rec(*false_case)
91+
dereference_exprt if_true(if_expr->true_case());
92+
if_true.add_source_location() = source_location;
93+
root_objects_rec(if_true, ns, log, dest);
94+
dereference_exprt if_false(if_expr->false_case());
95+
if_false.add_source_location() = source_location;
96+
root_objects_rec(if_false, ns, log, dest);
97+
}
98+
else if(
99+
const auto &address_of_expr =
100+
expr_try_dynamic_cast<address_of_exprt>(pointer))
101+
{
102+
const exprt &object = skip_typecast(address_of_expr->object());
103+
if(const auto &index = expr_try_dynamic_cast<index_exprt>(object))
104+
{
105+
// *(&arr[idx]) => rec(arr)
106+
const exprt &arr = index->array();
107+
if(arr.type().id() == ID_array)
108+
{
109+
root_objects_rec(arr, ns, log, dest);
110+
}
111+
}
112+
else
113+
{
114+
// *(&object) => rec(object)
115+
root_objects_rec(object, ns, log, dest);
116+
}
117+
}
118+
else
119+
{
120+
// simplify *(pointer + offset) to *pointer
121+
dereference_exprt base_pointer(pointer);
122+
base_pointer.add_source_location() = source_location;
123+
dest.insert(base_pointer);
124+
}
125+
}
126+
else
127+
{
128+
// Stop here for anything else.
129+
dest.insert(expr);
130+
}
131+
}
132+
133+
std::unordered_set<exprt, irep_hash> dfcc_assignment_lhs_root_objects(
134+
const exprt &lhs,
135+
const namespacet &ns,
136+
messaget &log)
137+
{
138+
std::unordered_set<exprt, irep_hash> result;
139+
root_objects_rec(lhs, ns, log, result);
140+
return result;
141+
}
142+
143+
/// Translates object slice expressions found in assigns clause targets to
144+
/// dereference expressions so that root objects can be computed.
145+
static exprt slice_op_to_deref(const exprt &expr)
146+
{
147+
if(can_cast_expr<side_effect_expr_function_callt>(expr))
148+
{
149+
auto function_call_expr = to_side_effect_expr_function_call(expr);
150+
auto function_expr = function_call_expr.function();
151+
INVARIANT(
152+
function_expr.id() == ID_symbol,
153+
"no function pointer calls in loop assigns clause targets");
154+
auto function_id = to_symbol_expr(function_expr).get_identifier();
155+
INVARIANT(
156+
function_id == CPROVER_PREFIX "assignable" ||
157+
function_id == CPROVER_PREFIX "object_whole" ||
158+
function_id == CPROVER_PREFIX "object_from" ||
159+
function_id == CPROVER_PREFIX "object_upto",
160+
"can only handle built-in function calls in assigns clause targets");
161+
return dereference_exprt(
162+
skip_typecast(function_call_expr.arguments().at(0)));
163+
}
164+
else
165+
{
166+
return expr;
167+
}
168+
}
169+
170+
std::unordered_set<exprt, irep_hash> dfcc_assigns_target_root_objects(
171+
const exprt &expr,
172+
const namespacet &ns,
173+
messaget &log)
174+
{
175+
return dfcc_assignment_lhs_root_objects(slice_op_to_deref(expr), ns, log);
176+
}
177+
178+
exprt dfcc_assigns_target_single_root_object(
179+
const exprt &expr,
180+
const namespacet &ns,
181+
messaget &log)
182+
{
183+
auto root_objects = dfcc_assigns_target_root_objects(expr, ns, log);
184+
PRECONDITION_WITH_DIAGNOSTICS(
185+
root_objects.size() == 1,
186+
"Expecting single root object for assigns clause target");
187+
return *root_objects.begin();
188+
}

‎src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h

+47
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking
4+
5+
Author: Remi Delmas, [email protected]
6+
7+
Date: March 2023
8+
9+
\*******************************************************************/
10+
11+
/// \file
12+
/// Utility functions that compute root object expressions for assigns clause
13+
/// targets and LHS expressions.
14+
15+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
16+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
17+
18+
#include <util/irep.h>
19+
20+
#include <unordered_set>
21+
22+
class exprt;
23+
class namespacet;
24+
class messaget;
25+
26+
/// Computes a set of root object expressions for an assignment left hand side
27+
/// expression.
28+
std::unordered_set<exprt, irep_hash> dfcc_assignment_lhs_root_objects(
29+
const exprt &lhs,
30+
const namespacet &ns,
31+
messaget &log);
32+
33+
/// Computes a set of root object expressions for an assigns clause target
34+
/// expression that may contain disjunctions.
35+
std::unordered_set<exprt, irep_hash> dfcc_assigns_target_root_objects(
36+
const exprt &expr,
37+
const namespacet &ns,
38+
messaget &log);
39+
40+
/// Computes a single root object expressions for an assigns clause target that
41+
/// is expected not to contain disjunctions. Fails if the expression contains
42+
/// disjunctions.
43+
exprt dfcc_assigns_target_single_root_object(
44+
const exprt &expr,
45+
const namespacet &ns,
46+
messaget &log);
47+
#endif

0 commit comments

Comments
 (0)