Skip to content

Commit 5d136c4

Browse files
committed
Value set: lift offset from numeric constants to expressions
We can safely track arbitrary expressions as pointer offsets rather than limit ourselves to just constant offsets (and then treating all other expressions as "unknown").
1 parent f1faa61 commit 5d136c4

File tree

3 files changed

+53
-57
lines changed

3 files changed

+53
-57
lines changed

src/goto-symex/shadow_memory_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -981,7 +981,7 @@ normalize(const object_descriptor_exprt &expr, const namespacet &ns)
981981
{
982982
return expr;
983983
}
984-
if(expr.offset().id() == ID_unknown)
984+
if(!expr.offset().is_constant())
985985
{
986986
return expr;
987987
}

src/pointer-analysis/value_set.cpp

Lines changed: 49 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,7 @@ Author: Daniel Kroening, [email protected]
2828
#include <util/xml.h>
2929

3030
#ifdef DEBUG
31-
#include <iostream>
32-
#include <util/format_expr.h>
33-
#include <util/format_type.h>
31+
# include <iostream>
3432
#endif
3533

3634
#include "add_failed_symbols.h"
@@ -184,7 +182,7 @@ void value_sett::output(std::ostream &out, const std::string &indent) const
184182
stream << "<" << format(o) << ", ";
185183

186184
if(o_it->second)
187-
stream << *o_it->second;
185+
stream << format(*o_it->second);
188186
else
189187
stream << '*';
190188

@@ -261,7 +259,7 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
261259
od.object()=object;
262260

263261
if(it.second)
264-
od.offset() = from_integer(*it.second, c_index_type());
262+
od.offset() = *it.second;
265263

266264
od.type()=od.object().type();
267265

@@ -352,7 +350,7 @@ bool value_sett::eval_pointer_offset(
352350
it=object_map.begin();
353351
it!=object_map.end();
354352
it++)
355-
if(!it->second)
353+
if(!it->second || !it->second->is_constant())
356354
return false;
357355
else
358356
{
@@ -362,7 +360,8 @@ bool value_sett::eval_pointer_offset(
362360
if(!ptr_offset.has_value())
363361
return false;
364362

365-
*ptr_offset += *it->second;
363+
*ptr_offset +=
364+
numeric_cast_v<mp_integer>(to_constant_expr(*it->second));
366365

367366
if(mod && *ptr_offset != previous_offset)
368367
return false;
@@ -623,7 +622,7 @@ void value_sett::get_value_set_rec(
623622
insert(
624623
dest,
625624
exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
626-
mp_integer{0});
625+
from_integer(0, c_index_type()));
627626
}
628627
else if(
629628
expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
@@ -655,7 +654,10 @@ void value_sett::get_value_set_rec(
655654

656655
if(op.is_zero())
657656
{
658-
insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
657+
insert(
658+
dest,
659+
exprt(ID_null_object, empty_typet{}),
660+
from_integer(0, c_index_type()));
659661
}
660662
else
661663
{
@@ -696,15 +698,14 @@ void value_sett::get_value_set_rec(
696698
throw expr.id_string()+" expected to have at least two operands";
697699

698700
object_mapt pointer_expr_set;
699-
std::optional<mp_integer> i;
701+
std::optional<exprt> additional_offset;
700702

701703
// special case for plus/minus and exactly one pointer
702704
std::optional<exprt> ptr_operand;
703705
if(
704706
expr.type().id() == ID_pointer &&
705707
(expr.id() == ID_plus || expr.id() == ID_minus))
706708
{
707-
bool non_const_offset = false;
708709
for(const auto &op : expr.operands())
709710
{
710711
if(op.type().id() == ID_pointer)
@@ -717,24 +718,20 @@ void value_sett::get_value_set_rec(
717718

718719
ptr_operand = op;
719720
}
720-
else if(!non_const_offset)
721+
else
721722
{
722-
auto offset = numeric_cast<mp_integer>(op);
723-
if(!offset.has_value())
724-
{
725-
i.reset();
726-
non_const_offset = true;
727-
}
723+
if(!additional_offset.has_value())
724+
additional_offset = op;
728725
else
729726
{
730-
if(!i.has_value())
731-
i = mp_integer{0};
732-
i = *i + *offset;
727+
additional_offset = plus_exprt{
728+
*additional_offset,
729+
typecast_exprt::conditional_cast(op, additional_offset->type())};
733730
}
734731
}
735732
}
736733

737-
if(ptr_operand.has_value() && i.has_value())
734+
if(ptr_operand.has_value() && additional_offset.has_value())
738735
{
739736
typet pointer_base_type =
740737
to_pointer_type(ptr_operand->type()).base_type();
@@ -745,18 +742,22 @@ void value_sett::get_value_set_rec(
745742

746743
if(!size.has_value() || (*size) == 0)
747744
{
748-
i.reset();
745+
additional_offset.reset();
749746
}
750747
else
751748
{
752-
*i *= *size;
749+
additional_offset = mult_exprt{
750+
*additional_offset, from_integer(*size, additional_offset->type())};
753751

754752
if(expr.id()==ID_minus)
755753
{
756754
DATA_INVARIANT(
757755
to_minus_expr(expr).lhs() == *ptr_operand,
758756
"unexpected subtraction of pointer from integer");
759-
i->negate();
757+
DATA_INVARIANT(
758+
additional_offset->type().id() != ID_unsignedbv,
759+
"offset type must support negation");
760+
additional_offset = unary_minus_exprt{*additional_offset};
760761
}
761762
}
762763
}
@@ -790,8 +791,15 @@ void value_sett::get_value_set_rec(
790791
offsett offset = it->second;
791792

792793
// adjust by offset
793-
if(offset && i.has_value())
794-
*offset += *i;
794+
if(offset && additional_offset.has_value())
795+
{
796+
offset = simplify_expr(
797+
plus_exprt{
798+
*offset,
799+
typecast_exprt::conditional_cast(
800+
*additional_offset, offset->type())},
801+
ns);
802+
}
795803
else
796804
offset.reset();
797805

@@ -871,7 +879,7 @@ void value_sett::get_value_set_rec(
871879
dynamic_object.set_instance(location_number);
872880
dynamic_object.valid()=true_exprt();
873881

874-
insert(dest, dynamic_object, mp_integer{0});
882+
insert(dest, dynamic_object, from_integer(0, c_index_type()));
875883
}
876884
else if(statement==ID_cpp_new ||
877885
statement==ID_cpp_new_array)
@@ -884,7 +892,7 @@ void value_sett::get_value_set_rec(
884892
dynamic_object.set_instance(location_number);
885893
dynamic_object.valid()=true_exprt();
886894

887-
insert(dest, dynamic_object, mp_integer{0});
895+
insert(dest, dynamic_object, from_integer(0, c_index_type()));
888896
}
889897
else
890898
insert(dest, exprt(ID_unknown, original_type));
@@ -1336,7 +1344,7 @@ void value_sett::get_reference_set_rec(
13361344
to_array_type(expr.type()).element_type().id() == ID_array)
13371345
insert(dest, expr);
13381346
else
1339-
insert(dest, expr, mp_integer{0});
1347+
insert(dest, expr, from_integer(0, c_index_type()));
13401348

13411349
return;
13421350
}
@@ -1365,7 +1373,7 @@ void value_sett::get_reference_set_rec(
13651373

13661374
const index_exprt &index_expr=to_index_expr(expr);
13671375
const exprt &array=index_expr.array();
1368-
const exprt &offset=index_expr.index();
1376+
const exprt &index = index_expr.index();
13691377

13701378
DATA_INVARIANT(
13711379
array.type().id() == ID_array, "index takes array-typed operand");
@@ -1393,22 +1401,24 @@ void value_sett::get_reference_set_rec(
13931401
from_integer(0, c_index_type()));
13941402

13951403
offsett o = a_it->second;
1396-
const auto i = numeric_cast<mp_integer>(offset);
13971404

1398-
if(offset.is_zero())
1399-
{
1400-
}
1401-
else if(i.has_value() && o)
1405+
if(!index.is_zero() && o.has_value())
14021406
{
14031407
auto size = pointer_offset_size(array_type.element_type(), ns);
14041408

14051409
if(!size.has_value() || *size == 0)
14061410
o.reset();
14071411
else
1408-
*o = *i * (*size);
1412+
{
1413+
o = simplify_expr(
1414+
plus_exprt{
1415+
*o,
1416+
typecast_exprt::conditional_cast(
1417+
mult_exprt{index, from_integer(*size, index.type())},
1418+
o->type())},
1419+
ns);
1420+
}
14091421
}
1410-
else
1411-
o.reset();
14121422

14131423
insert(dest, deref_index_expr, o);
14141424
}

src/pointer-analysis/value_set.h

Lines changed: 3 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,9 @@ class value_sett
7676
/// in value sets.
7777
static object_numberingt object_numbering;
7878

79-
/// Represents the offset into an object: either a unique integer offset,
80-
/// or an unknown value, represented by `!offset`.
81-
typedef std::optional<mp_integer> offsett;
79+
/// Represents the offset into an object: either some (possibly constant)
80+
/// expression, or an unknown value, represented by `!offset`.
81+
typedef std::optional<exprt> offsett;
8282

8383
/// Represents a set of expressions (`exprt` instances) with corresponding
8484
/// offsets (`offsett` instances). This is the RHS set of a single row of
@@ -140,20 +140,6 @@ class value_sett
140140
return insert(dest, object_numbering.number(src), offsett());
141141
}
142142

143-
/// Adds an expression to an object map, with known offset. If the
144-
/// destination map has an existing element for the same expression
145-
/// with a differing offset its offset is marked unknown.
146-
/// \param dest: object map to update
147-
/// \param src: expression to add
148-
/// \param offset_value: offset into `src`
149-
bool insert(
150-
object_mapt &dest,
151-
const exprt &src,
152-
const mp_integer &offset_value) const
153-
{
154-
return insert(dest, object_numbering.number(src), offsett(offset_value));
155-
}
156-
157143
/// Adds a numbered expression and offset to an object map. If the
158144
/// destination map has an existing element for the same expression
159145
/// with a differing offset its offset is marked unknown.

0 commit comments

Comments
 (0)