Skip to content

Commit 4cc60e9

Browse files
committed
r/w/rw_ok and pointer_in_range depend on deallocated and dead_object
The evaluation of these expressions depends on the specific values of __CPROVER_deallocated and __CPROVER_dead_object at the time the expression is used. Therefore, create new prophecy_* variants of these expressions to retain the properties expected of an expression (as opposed to a statement/function call). These prophecy_* expressions can safely be passed on to back-ends, be simplified, and do not need to be rewritten during instrumentation. For now, they are just handled by lowering the expressions (in the SAT and SMT back-ends). We may, in future, decide to have back-end specific (and possibly more efficient) handling of these.
1 parent 79186c4 commit 4cc60e9

File tree

20 files changed

+565
-9
lines changed

20 files changed

+565
-9
lines changed

regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE new-smt-backend
22
test.c
33
--malloc-may-fail --malloc-fail-null
4-
^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
4+
^\[free.precondition.\d+] line \d+ double free: SUCCESS$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$
77
^SIGNAL=0$

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.c
44
^EXIT=0$
55
^SIGNAL=0$
66
Checking assertions
7-
^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
7+
^\[free.precondition.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
88
--
99
Invariant check failed
1010
--

src/ansi-c/expr2c.cpp

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3572,6 +3572,26 @@ std::string expr2ct::convert_r_or_w_ok(const r_or_w_ok_exprt &src)
35723572
return dest;
35733573
}
35743574

3575+
std::string
3576+
expr2ct::convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src)
3577+
{
3578+
// we hide prophecy expressions in C-style output
3579+
std::string dest = src.id() == ID_prophecy_r_ok ? "R_OK"
3580+
: src.id() == ID_prophecy_w_ok ? "W_OK"
3581+
: "RW_OK";
3582+
3583+
dest += '(';
3584+
3585+
unsigned p;
3586+
dest += convert_with_precedence(src.pointer(), p);
3587+
dest += ", ";
3588+
dest += convert_with_precedence(src.size(), p);
3589+
3590+
dest += ')';
3591+
3592+
return dest;
3593+
}
3594+
35753595
std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
35763596
{
35773597
std::string dest = CPROVER_PREFIX "pointer_in_range";
@@ -3590,6 +3610,26 @@ std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
35903610
return dest;
35913611
}
35923612

3613+
std::string expr2ct::convert_prophecy_pointer_in_range(
3614+
const prophecy_pointer_in_range_exprt &src)
3615+
{
3616+
// we hide prophecy expressions in C-style output
3617+
std::string dest = CPROVER_PREFIX "pointer_in_range";
3618+
3619+
dest += '(';
3620+
3621+
unsigned p;
3622+
dest += convert_with_precedence(src.lower_bound(), p);
3623+
dest += ", ";
3624+
dest += convert_with_precedence(src.pointer(), p);
3625+
dest += ", ";
3626+
dest += convert_with_precedence(src.upper_bound(), p);
3627+
3628+
dest += ')';
3629+
3630+
return dest;
3631+
}
3632+
35933633
std::string expr2ct::convert_with_precedence(
35943634
const exprt &src,
35953635
unsigned &precedence)
@@ -4002,9 +4042,22 @@ std::string expr2ct::convert_with_precedence(
40024042
else if(src.id() == ID_r_ok || src.id() == ID_w_ok || src.id() == ID_rw_ok)
40034043
return convert_r_or_w_ok(to_r_or_w_ok_expr(src));
40044044

4045+
else if(
4046+
auto prophecy_r_or_w_ok =
4047+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(src))
4048+
{
4049+
return convert_prophecy_r_or_w_ok(*prophecy_r_or_w_ok);
4050+
}
4051+
40054052
else if(src.id() == ID_pointer_in_range)
40064053
return convert_pointer_in_range(to_pointer_in_range_expr(src));
40074054

4055+
else if(src.id() == ID_prophecy_pointer_in_range)
4056+
{
4057+
return convert_prophecy_pointer_in_range(
4058+
to_prophecy_pointer_in_range_expr(src));
4059+
}
4060+
40084061
auto function_string_opt = convert_function(src);
40094062
if(function_string_opt.has_value())
40104063
return *function_string_opt;

src/ansi-c/expr2c_class.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ class qualifierst;
2828
class namespacet;
2929
class r_or_w_ok_exprt;
3030
class pointer_in_range_exprt;
31+
class prophecy_r_or_w_ok_exprt;
32+
class prophecy_pointer_in_range_exprt;
3133

3234
class expr2ct
3335
{
@@ -285,7 +287,10 @@ class expr2ct
285287
std::string convert_bitreverse(const bitreverse_exprt &src);
286288

287289
std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src);
290+
std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src);
288291
std::string convert_pointer_in_range(const pointer_in_range_exprt &src);
292+
std::string
293+
convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src);
289294
};
290295

291296
#endif // CPROVER_ANSI_C_EXPR2C_CLASS_H

src/ansi-c/goto_check_c.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1444,6 +1444,8 @@ void goto_check_ct::pointer_primitive_check(
14441444
const exprt pointer =
14451445
(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
14461446
? to_r_or_w_ok_expr(expr).pointer()
1447+
: can_cast_expr<prophecy_r_or_w_ok_exprt>(expr)
1448+
? to_prophecy_r_or_w_ok_expr(expr).pointer()
14471449
: to_unary_expr(expr).op();
14481450

14491451
CHECK_RETURN(pointer.type().id() == ID_pointer);
@@ -1484,6 +1486,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr)
14841486
// will equally be non-deterministic.
14851487
return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
14861488
expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1489+
can_cast_expr<prophecy_r_or_w_ok_exprt>(expr) ||
14871490
expr.id() == ID_is_dynamic_object;
14881491
}
14891492

src/cprover/state_encoding.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -294,6 +294,20 @@ exprt state_encodingt::evaluate_expr_rec(
294294
: ID_state_rw_ok;
295295
return ternary_exprt(new_id, state, pointer, size, what.type());
296296
}
297+
else if(
298+
const auto r_or_w_ok_expr =
299+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(what))
300+
{
301+
// we replace prophecy expressions by our state
302+
auto pointer =
303+
evaluate_expr_rec(loc, state, r_or_w_ok_expr->pointer(), bound_symbols);
304+
auto size =
305+
evaluate_expr_rec(loc, state, r_or_w_ok_expr->size(), bound_symbols);
306+
auto new_id = what.id() == ID_prophecy_r_ok ? ID_state_r_ok
307+
: what.id() == ID_prophecy_w_ok ? ID_state_w_ok
308+
: ID_state_rw_ok;
309+
return ternary_exprt(new_id, state, pointer, size, what.type());
310+
}
297311
else if(what.id() == ID_is_cstring)
298312
{
299313
// we need to add the state

src/goto-instrument/contracts/instrument_spec_assigns.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -644,9 +644,13 @@ exprt instrument_spec_assignst::target_validity_expr(
644644
// (or is NULL if we allow it explicitly).
645645
// This assertion will be falsified whenever `start_address` is invalid or
646646
// not of the right size (or is NULL if we do not allow it explicitly).
647-
auto result =
648-
or_exprt{not_exprt{car.condition()},
649-
w_ok_exprt{car.target_start_address(), car.target_size()}};
647+
symbol_exprt deallocated =
648+
ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
649+
symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
650+
auto result = or_exprt{
651+
not_exprt{car.condition()},
652+
prophecy_w_ok_exprt{
653+
car.target_start_address(), car.target_size(), deallocated, dead}};
650654

651655
if(allow_null_target)
652656
result.add_to_operands(null_object(car.target_start_address()));

src/goto-instrument/contracts/utils.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,11 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
178178
const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
179179
CHECK_RETURN(size_of_expr_opt.has_value());
180180

181-
validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
181+
symbol_exprt deallocated =
182+
ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
183+
symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
184+
validity_checks.push_back(prophecy_r_ok_exprt{
185+
deref->pointer(), *size_of_expr_opt, deallocated, dead});
182186
}
183187

184188
for(const auto &op : expr.operands())

src/goto-programs/builtin_functions.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -669,7 +669,10 @@ void goto_convertt::do_havoc_slice(
669669
// char nondet_contents[argument[1]];
670670
// __CPROVER_array_replace(p, nondet_contents);
671671

672-
r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
672+
symbol_exprt deallocated =
673+
ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
674+
symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
675+
prophecy_w_ok_exprt ok_expr{arguments[0], arguments[1], deallocated, dead};
673676
ok_expr.add_source_location() = source_location;
674677
source_locationt annotated_location = source_location;
675678
annotated_location.set("user-provided", false);

src/goto-programs/goto_clean_expr.cpp

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "goto_convert_class.h"
1313

14+
#include <util/cprover_prefix.h>
1415
#include <util/expr_util.h>
1516
#include <util/fresh_symbol.h>
1617
#include <util/pointer_expr.h>
@@ -73,6 +74,15 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
7374
return true;
7475
}
7576

77+
// Rewrite rw_ok and pointer_in_range front-end expressions into ones
78+
// including prophecy expressions.
79+
if(
80+
can_cast_expr<r_or_w_ok_exprt>(expr) ||
81+
can_cast_expr<pointer_in_range_exprt>(expr))
82+
{
83+
return true;
84+
}
85+
7686
// We can't flatten quantified expressions by introducing new literals for
7787
// conditional expressions. This is because the body of the quantified
7888
// may refer to bound variables, which are not visible outside the scope
@@ -436,6 +446,32 @@ void goto_convertt::clean_expr(
436446
expr.operands().size() == 1, "ID_compound_literal has a single operand");
437447
expr = to_unary_expr(expr).op();
438448
}
449+
else if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(expr))
450+
{
451+
const auto &id = expr.id();
452+
expr =
453+
prophecy_r_or_w_ok_exprt{
454+
id == ID_r_ok ? ID_prophecy_r_ok
455+
: id == ID_w_ok ? ID_prophecy_w_ok
456+
: ID_prophecy_rw_ok,
457+
r_or_w_ok->pointer(),
458+
r_or_w_ok->size(),
459+
ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
460+
ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
461+
.with_source_location<exprt>(expr);
462+
}
463+
else if(
464+
auto pointer_in_range = expr_try_dynamic_cast<pointer_in_range_exprt>(expr))
465+
{
466+
expr =
467+
prophecy_pointer_in_range_exprt{
468+
pointer_in_range->lower_bound(),
469+
pointer_in_range->pointer(),
470+
pointer_in_range->upper_bound(),
471+
ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
472+
ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
473+
.with_source_location<exprt>(expr);
474+
}
439475
}
440476

441477
void goto_convertt::clean_expr_address_of(

src/solvers/flattening/bv_pointers.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/pointer_expr.h>
1919
#include <util/pointer_offset_size.h>
2020
#include <util/pointer_predicates.h>
21+
#include <util/simplify_expr.h>
2122

2223
/// Map bytes according to the configured endianness. The key difference to
2324
/// endianness_mapt is that bv_endianness_mapt is aware of the bit-level
@@ -204,6 +205,18 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
204205
bv_utilst::representationt::UNSIGNED));
205206
}
206207
}
208+
else if(
209+
auto prophecy_r_or_w_ok =
210+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
211+
{
212+
return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns));
213+
}
214+
else if(
215+
auto prophecy_pointer_in_range =
216+
expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
217+
{
218+
return convert(simplify_expr(prophecy_pointer_in_range->lower(ns), ns));
219+
}
207220

208221
return SUB::convert_rest(expr);
209222
}

src/solvers/smt2/smt2_conv.cpp

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4864,6 +4864,30 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr)
48644864
!has_byte_operator(lowered_expr),
48654865
"lower_byte_operators should remove all byte operators");
48664866

4867+
// Perform rewrites that may introduce new symbols
4868+
for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4869+
it != itend;) // no ++it
4870+
{
4871+
if(
4872+
auto prophecy_r_or_w_ok =
4873+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(*it))
4874+
{
4875+
exprt lowered = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
4876+
it.mutate() = lowered;
4877+
it.next_sibling_or_parent();
4878+
}
4879+
else if(
4880+
auto prophecy_pointer_in_range =
4881+
expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(*it))
4882+
{
4883+
exprt lowered = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
4884+
it.mutate() = lowered;
4885+
it.next_sibling_or_parent();
4886+
}
4887+
else
4888+
++it;
4889+
}
4890+
48674891
// Now create symbols for all composite expressions present in lowered_expr:
48684892
find_symbols(lowered_expr);
48694893

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1463,6 +1463,24 @@ static smt_termt convert_expr_to_smt(
14631463
count_trailing_zeros.pretty());
14641464
}
14651465

1466+
static smt_termt convert_expr_to_smt(
1467+
const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok,
1468+
const sub_expression_mapt &converted)
1469+
{
1470+
UNIMPLEMENTED_FEATURE(
1471+
"Generation of SMT formula for r/w/rw ok expression: " +
1472+
prophecy_r_or_w_ok.pretty());
1473+
}
1474+
1475+
static smt_termt convert_expr_to_smt(
1476+
const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range,
1477+
const sub_expression_mapt &converted)
1478+
{
1479+
UNIMPLEMENTED_FEATURE(
1480+
"Generation of SMT formula for pointer-in-range expression: " +
1481+
prophecy_pointer_in_range.pretty());
1482+
}
1483+
14661484
static smt_termt dispatch_expr_to_smt_conversion(
14671485
const exprt &expr,
14681486
const sub_expression_mapt &converted,
@@ -1798,6 +1816,18 @@ static smt_termt dispatch_expr_to_smt_conversion(
17981816
{
17991817
return convert_expr_to_smt(*count_trailing_zeros, converted);
18001818
}
1819+
if(
1820+
const auto prophecy_r_or_w_ok =
1821+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
1822+
{
1823+
return convert_expr_to_smt(*prophecy_r_or_w_ok, converted);
1824+
}
1825+
if(
1826+
const auto prophecy_pointer_in_range =
1827+
expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
1828+
{
1829+
return convert_expr_to_smt(*prophecy_pointer_in_range, converted);
1830+
}
18011831

18021832
UNIMPLEMENTED_FEATURE(
18031833
"Generation of SMT formula for unknown kind of expression: " +

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
#include <util/namespace.h>
88
#include <util/nodiscard.h>
99
#include <util/range.h>
10+
#include <util/simplify_expr.h>
1011
#include <util/std_expr.h>
1112
#include <util/string_constant.h>
1213
#include <util/symbol.h>
@@ -273,6 +274,25 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
273274
solver_process->send(is_dynamic_object_function.declaration);
274275
}
275276

277+
static exprt lower_rw_ok_pointer_in_range(exprt expr, const namespacet &ns)
278+
{
279+
expr.visit_pre([&ns](exprt &expr) {
280+
if(
281+
auto prophecy_r_or_w_ok =
282+
expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
283+
{
284+
expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
285+
}
286+
else if(
287+
auto prophecy_pointer_in_range =
288+
expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
289+
{
290+
expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
291+
}
292+
});
293+
return expr;
294+
}
295+
276296
void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
277297
const exprt &in_expr)
278298
{
@@ -623,8 +643,9 @@ void smt2_incremental_decision_proceduret::define_object_properties()
623643

624644
exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
625645
{
626-
const exprt lowered = struct_encoding.encode(
627-
lower_enum(lower_byte_operators(expression, ns), ns));
646+
const exprt lowered = struct_encoding.encode(lower_enum(
647+
lower_byte_operators(lower_rw_ok_pointer_in_range(expression, ns), ns),
648+
ns));
628649
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
629650
if(lowered != expression)
630651
debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;

0 commit comments

Comments
 (0)