Skip to content

Commit d11f7a2

Browse files
author
Remi Delmas
committed
CONTRACTS: functions to compute root objects
Alternative implementation of `root_object` supporting ternary operators in assignemtn or call LHS expressions, and object slice expressions in assigns clause targets.
1 parent 193b2fd commit d11f7a2

File tree

3 files changed

+237
-0
lines changed

3 files changed

+237
-0
lines changed

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
1818
call_sequences.cpp \
1919
contracts/contracts.cpp \
2020
contracts/dynamic-frames/dfcc_utils.cpp \
21+
contracts/dynamic-frames/dfcc_root_object.cpp \
2122
contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
2223
contracts/dynamic-frames/dfcc_contract_mode.cpp \
2324
contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \

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

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
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 an assignment lhs.
27+
static void lhs_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+
lhs_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+
lhs_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+
lhs_root_objects_rec(to_if_expr(expr).true_case(), ns, log, dest);
59+
lhs_root_objects_rec(to_if_expr(expr).false_case(), ns, log, dest);
60+
}
61+
else if(expr.id() == ID_typecast)
62+
{
63+
lhs_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+
lhs_root_objects_rec(to_byte_extract_expr(expr).op(), ns, log, dest);
70+
}
71+
else if(expr.id() == ID_complex_real)
72+
{
73+
lhs_root_objects_rec(to_complex_real_expr(expr).op(), ns, log, dest);
74+
}
75+
else if(expr.id() == ID_complex_imag)
76+
{
77+
lhs_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+
lhs_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+
lhs_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+
lhs_root_objects_rec(arr, ns, log, dest);
110+
}
111+
}
112+
else
113+
{
114+
// *(&object) => rec(object)
115+
lhs_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 &expr,
135+
const namespacet &ns,
136+
messaget &log)
137+
{
138+
std::unordered_set<exprt, irep_hash> result;
139+
lhs_root_objects_rec(expr, ns, log, result);
140+
return result;
141+
}
142+
143+
/// Translates object slice expressions found in assigns clause targets to
144+
/// dereference expressions, so that object_descriptor_exprt can be used to
145+
/// compute the base object expression.
146+
static exprt slice_op_to_deref(const exprt &expr)
147+
{
148+
if(can_cast_expr<side_effect_expr_function_callt>(expr))
149+
{
150+
auto function_call_expr = to_side_effect_expr_function_call(expr);
151+
auto function_expr = function_call_expr.function();
152+
INVARIANT(
153+
function_expr.id() == ID_symbol,
154+
"no function pointer calls in loop assigns clause targets");
155+
auto function_id = to_symbol_expr(function_expr).get_identifier();
156+
INVARIANT(
157+
function_id == CPROVER_PREFIX "assignable" ||
158+
function_id == CPROVER_PREFIX "object_whole" ||
159+
function_id == CPROVER_PREFIX "object_from" ||
160+
function_id == CPROVER_PREFIX "object_upto",
161+
"can only handle built-in function calls in assigns clause targets");
162+
return dereference_exprt(
163+
skip_typecast(function_call_expr.arguments().at(0)));
164+
}
165+
else
166+
{
167+
return expr;
168+
}
169+
}
170+
171+
std::unordered_set<exprt, irep_hash> dfcc_assigns_target_root_objects(
172+
const exprt &expr,
173+
const namespacet &ns,
174+
messaget &log)
175+
{
176+
return dfcc_assignment_lhs_root_objects(slice_op_to_deref(expr), ns, log);
177+
}
178+
179+
exprt dfcc_assigns_target_single_root_object(
180+
const exprt &expr,
181+
const namespacet &ns,
182+
messaget &log)
183+
{
184+
auto root_objects =
185+
dfcc_assignment_lhs_root_objects(slice_op_to_deref(expr), ns, log);
186+
PRECONDITION_WITH_DIAGNOSTICS(
187+
root_objects.size() == 1,
188+
"Expecting single root object for assigns clause target");
189+
return *root_objects.begin();
190+
}

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

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
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 lhs expression.
27+
std::unordered_set<exprt, irep_hash> dfcc_assignment_lhs_root_objects(
28+
const exprt &lhs,
29+
const namespacet &ns,
30+
messaget &log);
31+
32+
/// Computes a set of root object expressions for an assigns clause target
33+
/// expression that may contain disjunctions.
34+
std::unordered_set<exprt, irep_hash> dfcc_assigns_target_root_objects(
35+
const exprt &expr,
36+
const namespacet &ns,
37+
messaget &log);
38+
39+
/// Computes a single root object expressions for an assigns clause target that
40+
/// is expected not to contain disjunctions. Fails if the exprssion contains
41+
/// disjunctions.
42+
exprt dfcc_assigns_target_single_root_object(
43+
const exprt &expr,
44+
const namespacet &ns,
45+
messaget &log);
46+
#endif

0 commit comments

Comments
 (0)