Skip to content

Commit 23af75f

Browse files
author
owen-jones-diffblue
authored
Merge pull request #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

0 commit comments

Comments
 (0)