Skip to content

Commit 9186b70

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 b34e991 commit 9186b70

File tree

3 files changed

+209
-0
lines changed

3 files changed

+209
-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_library.cpp \
2223
contracts/dynamic-frames/dfcc_is_fresh.cpp \
2324
contracts/dynamic-frames/dfcc_pointer_in_range.cpp \

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

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
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 &ptr =
81+
expr_try_dynamic_cast<dereference_exprt>(skip_typecast(expr)))
82+
{
83+
// normalise into `pointer + offset` and pattern match on the pointer
84+
const auto &base_ptr = pointer_arithmetict(*ptr).pointer;
85+
if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>(base_ptr))
86+
{
87+
// *(c ? true_case : false_case) => rec(*true_case); rec(*false_case)
88+
lhs_root_objects_rec(
89+
dereference_exprt(if_expr->true_case()), ns, log, dest);
90+
lhs_root_objects_rec(
91+
dereference_exprt(if_expr->false_case()), ns, log, dest);
92+
}
93+
else if(
94+
const auto &address_of_expr =
95+
expr_try_dynamic_cast<address_of_exprt>(base_ptr))
96+
{
97+
const exprt &object = skip_typecast(address_of_expr->object());
98+
if(const auto &index = expr_try_dynamic_cast<index_exprt>(object))
99+
{
100+
// *(&arr[idx]) => rec(arr)
101+
const exprt &arr = index->array();
102+
if(arr.id() == ID_array)
103+
{
104+
lhs_root_objects_rec(arr, ns, log, dest);
105+
}
106+
}
107+
else
108+
{
109+
// *(&object) => rec(object)
110+
lhs_root_objects_rec(object, ns, log, dest);
111+
}
112+
}
113+
else
114+
{
115+
// *(base_pointer) could not be simplified
116+
dest.insert(expr);
117+
}
118+
}
119+
else
120+
{
121+
// Stop here for anything else.
122+
dest.insert(expr);
123+
}
124+
}
125+
126+
std::unordered_set<exprt, irep_hash> dfcc_assignment_lhs_root_objects(
127+
const exprt &expr,
128+
const namespacet &ns,
129+
messaget &log)
130+
{
131+
std::unordered_set<exprt, irep_hash> result;
132+
lhs_root_objects_rec(expr, ns, log, result);
133+
return result;
134+
}
135+
136+
/// Translates object slice expressions found in assigns clause targets to
137+
/// dereference expressions, so that object_descriptor_exprt can be used to
138+
/// compute the base object expression.
139+
static exprt slice_op_to_deref(const exprt &expr)
140+
{
141+
if(can_cast_expr<side_effect_expr_function_callt>(expr))
142+
{
143+
auto function_call_expr = to_side_effect_expr_function_call(expr);
144+
auto function_expr = function_call_expr.function();
145+
INVARIANT(
146+
function_expr.id() == ID_symbol,
147+
"no function pointer calls in loop assigns clause targets");
148+
auto function_id = to_symbol_expr(function_expr).get_identifier();
149+
INVARIANT(
150+
function_id == CPROVER_PREFIX "assignable" ||
151+
function_id == CPROVER_PREFIX "object_whole" ||
152+
function_id == CPROVER_PREFIX "object_from" ||
153+
function_id == CPROVER_PREFIX "object_upto",
154+
"can only handle built-in function calls in assigns clause targets");
155+
return dereference_exprt(
156+
skip_typecast(function_call_expr.arguments().at(0)));
157+
}
158+
else
159+
{
160+
return expr;
161+
}
162+
}
163+
164+
std::unordered_set<exprt, irep_hash> dfcc_loop_assigns_target_root_object(
165+
const exprt &expr,
166+
const namespacet &ns,
167+
messaget &log)
168+
{
169+
return dfcc_assignment_lhs_root_objects(slice_op_to_deref(expr), ns, log);
170+
}

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
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 a loop assigns clause target
33+
/// expression.
34+
std::unordered_set<exprt, irep_hash> dfcc_loop_assigns_target_root_object(
35+
const exprt &expr,
36+
const namespacet &ns,
37+
messaget &log);
38+
#endif

0 commit comments

Comments
 (0)