Skip to content

Commit 23af75f

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#4479 from owen-jones-diffblue/fix/disambiguate-two-exprts-with-same-id
disambiguate two exprts with same ID
2 parents d9694d5 + a9774ca commit 23af75f

15 files changed

+92
-60
lines changed

‎regression/goto-instrument/slice19/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--full-slice
44
^EXIT=0$

‎src/analyses/goto_check.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1129,18 +1129,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
11291129

11301130
if(flags.is_unknown())
11311131
{
1132-
conditions.push_back(conditiont(
1133-
not_exprt(invalid_pointer(address)),
1134-
"pointer invalid"));
1132+
conditions.push_back(conditiont{
1133+
not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
11351134
}
11361135

11371136
if(flags.is_uninitialized())
11381137
{
1139-
conditions.push_back(conditiont(
1140-
or_exprt(
1141-
in_bounds_of_some_explicit_allocation,
1142-
not_exprt(invalid_pointer(address))),
1143-
"pointer uninitialized"));
1138+
conditions.push_back(
1139+
conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
1140+
not_exprt{is_invalid_pointer_exprt{address}}},
1141+
"pointer uninitialized"});
11441142
}
11451143

11461144
if(flags.is_unknown() || flags.is_dynamic_heap())

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2095,16 +2095,16 @@ exprt c_typecheck_baset::do_special_functions(
20952095

20962096
return std::move(get_may_expr);
20972097
}
2098-
else if(identifier==CPROVER_PREFIX "invalid_pointer")
2098+
else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
20992099
{
21002100
if(expr.arguments().size()!=1)
21012101
{
21022102
error().source_location = f_op.source_location();
2103-
error() << "invalid_pointer expects one operand" << eom;
2103+
error() << "is_invalid_pointer expects one operand" << eom;
21042104
throw 0;
21052105
}
21062106

2107-
exprt same_object_expr = invalid_pointer(expr.arguments().front());
2107+
exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
21082108
same_object_expr.add_source_location()=source_location;
21092109

21102110
return same_object_expr;
@@ -2165,11 +2165,10 @@ exprt c_typecheck_baset::do_special_functions(
21652165
throw 0;
21662166
}
21672167

2168-
exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
2169-
dynamic_object_expr.operands()=expr.arguments();
2170-
dynamic_object_expr.add_source_location()=source_location;
2168+
exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
2169+
is_dynamic_object_expr.add_source_location() = source_location;
21712170

2172-
return dynamic_object_expr;
2171+
return is_dynamic_object_expr;
21732172
}
21742173
else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
21752174
{

‎src/ansi-c/cprover_builtin_headers.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
55
void __CPROVER_havoc_object(void *);
66
__CPROVER_bool __CPROVER_equal();
77
__CPROVER_bool __CPROVER_same_object(const void *, const void *);
8-
__CPROVER_bool __CPROVER_invalid_pointer(const void *);
8+
__CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
99
__CPROVER_bool __CPROVER_is_zero_string(const void *);
1010
__CPROVER_size_t __CPROVER_zero_string_length(const void *);
1111
__CPROVER_size_t __CPROVER_buffer_size(const void *);

‎src/ansi-c/expr2c.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3426,8 +3426,8 @@ std::string expr2ct::convert_with_precedence(
34263426
else if(src.id() == ID_w_ok)
34273427
return convert_function(src, "W_OK", precedence = 16);
34283428

3429-
else if(src.id()==ID_invalid_pointer)
3430-
return convert_function(src, "INVALID-POINTER", precedence=16);
3429+
else if(src.id() == ID_is_invalid_pointer)
3430+
return convert_function(src, "IS_INVALID_POINTER", precedence = 16);
34313431

34323432
else if(src.id()==ID_good_pointer)
34333433
return convert_function(src, "GOOD_POINTER", precedence=16);
@@ -3482,12 +3482,12 @@ std::string expr2ct::convert_with_precedence(
34823482
else if(src.id()=="pointer_cons")
34833483
return convert_function(src, "POINTER_CONS", precedence=16);
34843484

3485-
else if(src.id()==ID_invalid_pointer)
3485+
else if(src.id() == ID_is_invalid_pointer)
34863486
return convert_function(
3487-
src, CPROVER_PREFIX "invalid_pointer", precedence = 16);
3487+
src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16);
34883488

3489-
else if(src.id()==ID_dynamic_object)
3490-
return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
3489+
else if(src.id() == ID_is_dynamic_object)
3490+
return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16);
34913491

34923492
else if(src.id()=="is_zero_string")
34933493
return convert_function(src, "IS_ZERO_STRING", precedence=16);

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
2020

2121
const exprt::operandst &operands=expr.operands();
2222

23-
if(expr.id()==ID_invalid_pointer)
23+
if(expr.id() == ID_is_invalid_pointer)
2424
{
2525
if(operands.size()==1 &&
2626
operands[0].type().id()==ID_pointer)
@@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
4545
}
4646
}
4747
}
48-
else if(expr.id()==ID_dynamic_object)
48+
else if(expr.id() == ID_is_dynamic_object)
4949
{
5050
if(operands.size()==1 &&
5151
operands[0].type().id()==ID_pointer)
@@ -728,7 +728,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
728728
void bv_pointerst::do_postponed(
729729
const postponedt &postponed)
730730
{
731-
if(postponed.expr.id() == ID_dynamic_object)
731+
if(postponed.expr.id() == ID_is_dynamic_object)
732732
{
733733
const pointer_logict::objectst &objects=
734734
pointer_logic.objects;

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1316,11 +1316,11 @@ void smt2_convt::convert_expr(const exprt &expr)
13161316
if(ext>0)
13171317
out << ")"; // zero_extend
13181318
}
1319-
else if(expr.id() == ID_dynamic_object)
1319+
else if(expr.id() == ID_is_dynamic_object)
13201320
{
13211321
convert_is_dynamic_object(expr);
13221322
}
1323-
else if(expr.id()==ID_invalid_pointer)
1323+
else if(expr.id() == ID_is_invalid_pointer)
13241324
{
13251325
DATA_INVARIANT(
13261326
expr.operands().size() == 1,

‎src/util/irep_ids.def

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,7 @@ IREP_ID_ONE(invalid)
217217
IREP_ID_TWO(C_invalid_object, #invalid_object)
218218
IREP_ID_ONE(pointer_offset)
219219
IREP_ID_ONE(pointer_object)
220-
IREP_ID_TWO(invalid_pointer, invalid-pointer)
220+
IREP_ID_ONE(is_invalid_pointer)
221221
IREP_ID_ONE(ieee_float_equal)
222222
IREP_ID_ONE(ieee_float_notequal)
223223
IREP_ID_ONE(isnan)
@@ -446,6 +446,7 @@ IREP_ID_TWO(overflow_minus, overflow--)
446446
IREP_ID_TWO(overflow_mult, overflow-*)
447447
IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
448448
IREP_ID_ONE(object_descriptor)
449+
IREP_ID_ONE(is_dynamic_object)
449450
IREP_ID_ONE(dynamic_object)
450451
IREP_ID_TWO(C_dynamic, #dynamic)
451452
IREP_ID_ONE(object_size)

‎src/util/pointer_predicates.cpp

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns)
7070

7171
exprt dynamic_object(const exprt &pointer)
7272
{
73-
exprt dynamic_expr(ID_dynamic_object, bool_typet());
73+
exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
7474
dynamic_expr.copy_to_operands(pointer);
7575
return dynamic_expr;
7676
}
@@ -105,7 +105,7 @@ exprt good_pointer_def(
105105

106106
const not_exprt not_null(null_pointer(pointer));
107107

108-
const not_exprt not_invalid(invalid_pointer(pointer));
108+
const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
109109

110110
const or_exprt bad_other(
111111
object_lower_bound(pointer, nil_exprt()),
@@ -139,11 +139,6 @@ exprt null_pointer(const exprt &pointer)
139139
return same_object(pointer, null_pointer);
140140
}
141141

142-
exprt invalid_pointer(const exprt &pointer)
143-
{
144-
return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
145-
}
146-
147142
exprt dynamic_object_lower_bound(
148143
const exprt &pointer,
149144
const exprt &offset)

‎src/util/pointer_predicates.h

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,9 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_UTIL_POINTER_PREDICATES_H
1313
#define CPROVER_UTIL_POINTER_PREDICATES_H
1414

15-
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
15+
#include "std_expr.h"
1616

17-
class exprt;
18-
class namespacet;
19-
class typet;
17+
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
2018

2119
exprt same_object(const exprt &p1, const exprt &p2);
2220
exprt deallocated(const exprt &pointer, const namespacet &);
@@ -32,7 +30,6 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &);
3230
exprt null_object(const exprt &pointer);
3331
exprt null_pointer(const exprt &pointer);
3432
exprt integer_address(const exprt &pointer);
35-
exprt invalid_pointer(const exprt &pointer);
3633
exprt dynamic_object_lower_bound(
3734
const exprt &pointer,
3835
const exprt &offset);
@@ -47,4 +44,13 @@ exprt object_upper_bound(
4744
const exprt &pointer,
4845
const exprt &access_size);
4946

47+
class is_invalid_pointer_exprt : public unary_predicate_exprt
48+
{
49+
public:
50+
explicit is_invalid_pointer_exprt(exprt pointer)
51+
: unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
52+
{
53+
}
54+
};
55+
5056
#endif // CPROVER_UTIL_POINTER_PREDICATES_H

‎src/util/simplify_expr.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2403,12 +2403,12 @@ bool simplify_exprt::simplify_node(exprt &expr)
24032403
result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
24042404
else if(expr.id()==ID_pointer_object)
24052405
result=simplify_pointer_object(expr) && result;
2406-
else if(expr.id() == ID_dynamic_object)
2406+
else if(expr.id() == ID_is_dynamic_object)
24072407
{
2408-
result = simplify_dynamic_object(expr) && result;
2408+
result = simplify_is_dynamic_object(expr) && result;
24092409
}
2410-
else if(expr.id()==ID_invalid_pointer)
2411-
result=simplify_invalid_pointer(expr) && result;
2410+
else if(expr.id() == ID_is_invalid_pointer)
2411+
result = simplify_is_invalid_pointer(expr) && result;
24122412
else if(expr.id()==ID_object_size)
24132413
result=simplify_object_size(expr) && result;
24142414
else if(expr.id()==ID_good_pointer)

‎src/util/simplify_expr_class.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,8 +96,8 @@ class simplify_exprt
9696
bool simplify_pointer_object(exprt &expr);
9797
bool simplify_object_size(exprt &expr);
9898
bool simplify_dynamic_size(exprt &expr);
99-
bool simplify_dynamic_object(exprt &expr);
100-
bool simplify_invalid_pointer(exprt &expr);
99+
bool simplify_is_dynamic_object(exprt &expr);
100+
bool simplify_is_invalid_pointer(exprt &expr);
101101
bool simplify_same_object(exprt &expr);
102102
bool simplify_good_pointer(exprt &expr);
103103
bool simplify_object(exprt &expr);

‎src/util/simplify_expr_int.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1686,7 +1686,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
16861686
{
16871687
if(
16881688
expr.op0().op0().id() == ID_symbol ||
1689-
expr.op0().op0().id() == ID_dynamic_object ||
1689+
expr.op0().op0().id() == ID_is_dynamic_object ||
16901690
expr.op0().op0().id() == ID_member ||
16911691
expr.op0().op0().id() == ID_index ||
16921692
expr.op0().op0().id() == ID_string_constant)
@@ -1701,11 +1701,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
17011701
expr.op0().op0().id()==ID_address_of &&
17021702
expr.op0().op0().operands().size()==1)
17031703
{
1704-
if(expr.op0().op0().op0().id()==ID_symbol ||
1705-
expr.op0().op0().op0().id()==ID_dynamic_object ||
1706-
expr.op0().op0().op0().id()==ID_member ||
1707-
expr.op0().op0().op0().id()==ID_index ||
1708-
expr.op0().op0().op0().id()==ID_string_constant)
1704+
if(
1705+
expr.op0().op0().op0().id() == ID_symbol ||
1706+
expr.op0().op0().op0().id() == ID_is_dynamic_object ||
1707+
expr.op0().op0().op0().id() == ID_member ||
1708+
expr.op0().op0().op0().id() == ID_index ||
1709+
expr.op0().op0().op0().id() == ID_string_constant)
17091710
{
17101711
expr=false_exprt();
17111712
return false;

‎src/util/simplify_expr_pointer.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -468,7 +468,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
468468
{
469469
if(
470470
op.operands().size() != 1 ||
471-
(op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object &&
471+
(op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object &&
472472
op.op0().id() != ID_string_constant))
473473
{
474474
return true;
@@ -515,18 +515,18 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
515515
return result;
516516
}
517517

518-
bool simplify_exprt::simplify_dynamic_object(exprt &expr)
518+
bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
519519
{
520-
if(expr.operands().size()!=1)
521-
return true;
520+
// This should hold as a result of the expr ID being is_dynamic_object.
521+
PRECONDITION(expr.operands().size() == 1);
522522

523523
exprt &op=expr.op0();
524524

525525
if(op.id()==ID_if && op.operands().size()==3)
526526
{
527527
if_exprt if_expr=lift_if(expr, 0);
528-
simplify_dynamic_object(if_expr.true_case());
529-
simplify_dynamic_object(if_expr.false_case());
528+
simplify_is_dynamic_object(if_expr.true_case());
529+
simplify_is_dynamic_object(if_expr.false_case());
530530
simplify_if(if_expr);
531531
expr.swap(if_expr);
532532

@@ -571,7 +571,7 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
571571
return result;
572572
}
573573

574-
bool simplify_exprt::simplify_invalid_pointer(exprt &expr)
574+
bool simplify_exprt::simplify_is_invalid_pointer(exprt &expr)
575575
{
576576
if(expr.operands().size()!=1)
577577
return true;

‎src/util/std_expr.h

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2103,6 +2103,38 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
21032103
return ret;
21042104
}
21052105

2106+
/// Evaluates to true if the operand is a pointer to a dynamic object.
2107+
class is_dynamic_object_exprt : public unary_predicate_exprt
2108+
{
2109+
public:
2110+
is_dynamic_object_exprt() : unary_predicate_exprt(ID_is_dynamic_object)
2111+
{
2112+
}
2113+
2114+
explicit is_dynamic_object_exprt(const exprt &op)
2115+
: unary_predicate_exprt(ID_is_dynamic_object, op)
2116+
{
2117+
}
2118+
};
2119+
2120+
inline const is_dynamic_object_exprt &
2121+
to_is_dynamic_object_expr(const exprt &expr)
2122+
{
2123+
PRECONDITION(expr.id() == ID_is_dynamic_object);
2124+
DATA_INVARIANT(
2125+
expr.operands().size() == 1, "is_dynamic_object must have one operand");
2126+
return static_cast<const is_dynamic_object_exprt &>(expr);
2127+
}
2128+
2129+
/// \copydoc to_is_dynamic_object_expr(const exprt &)
2130+
/// \ingroup gr_std_expr
2131+
inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
2132+
{
2133+
PRECONDITION(expr.id() == ID_is_dynamic_object);
2134+
DATA_INVARIANT(
2135+
expr.operands().size() == 1, "is_dynamic_object must have one operand");
2136+
return static_cast<is_dynamic_object_exprt &>(expr);
2137+
}
21062138

21072139
/// \brief Semantic type conversion
21082140
class typecast_exprt:public unary_exprt

0 commit comments

Comments
 (0)