Skip to content

Commit 41811ba

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 41811ba

File tree

4 files changed

+75
-92
lines changed

4 files changed

+75
-92
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,6 @@ Author: Daniel Kroening, [email protected]
2626
#include "goto_symex_can_forward_propagate.h"
2727
#include "symex_target_equation.h"
2828

29-
static void get_l1_name(exprt &expr);
30-
3129
goto_symex_statet::goto_symex_statet(
3230
const symex_targett::sourcet &_source,
3331
std::size_t max_field_sensitive_array_size,
@@ -123,20 +121,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
123121
else
124122
propagation.erase_if_exists(l1_identifier);
125123

126-
{
127-
// update value sets
128-
exprt l1_rhs(rhs);
129-
get_l1_name(l1_rhs);
130-
131-
const ssa_exprt l1_lhs = remove_level_2(lhs);
132-
if(run_validation_checks)
133-
{
134-
DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
135-
DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
136-
}
137-
138-
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
139-
}
124+
value_set.assign(lhs, rhs, ns, rhs_is_simplified, is_shared);
140125

141126
#ifdef DEBUG
142127
std::cout << "Assigning " << l1_identifier << '\n';
@@ -783,17 +768,6 @@ void goto_symex_statet::rename(
783768
l1_type_entry.first->second=type;
784769
}
785770

786-
static void get_l1_name(exprt &expr)
787-
{
788-
// do not reset the type !
789-
790-
if(is_ssa_expr(expr))
791-
to_ssa_expr(expr).remove_level_2();
792-
else
793-
Forall_operands(it, expr)
794-
get_l1_name(*it);
795-
}
796-
797771
/// Dumps the current state of symex, printing the function name and location
798772
/// number for each stack frame in the currently active thread.
799773
/// This is for use from the debugger or in debug code; please don't delete it

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: 68 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,13 @@ Author: Daniel Kroening, [email protected]
2323
#include <util/prefix.h>
2424
#include <util/range.h>
2525
#include <util/simplify_expr.h>
26+
#include <util/ssa_expr.h>
2627
#include <util/std_code.h>
2728
#include <util/symbol.h>
2829
#include <util/xml.h>
2930

3031
#ifdef DEBUG
31-
#include <iostream>
32-
#include <util/format_expr.h>
33-
#include <util/format_type.h>
32+
# include <iostream>
3433
#endif
3534

3635
#include "add_failed_symbols.h"
@@ -184,7 +183,7 @@ void value_sett::output(std::ostream &out, const std::string &indent) const
184183
stream << "<" << format(o) << ", ";
185184

186185
if(o_it->second)
187-
stream << *o_it->second;
186+
stream << format(*o_it->second);
188187
else
189188
stream << '*';
190189

@@ -261,7 +260,7 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
261260
od.object()=object;
262261

263262
if(it.second)
264-
od.offset() = from_integer(*it.second, c_index_type());
263+
od.offset() = *it.second;
265264

266265
od.type()=od.object().type();
267266

@@ -352,7 +351,7 @@ bool value_sett::eval_pointer_offset(
352351
it=object_map.begin();
353352
it!=object_map.end();
354353
it++)
355-
if(!it->second)
354+
if(!it->second || !it->second->is_constant())
356355
return false;
357356
else
358357
{
@@ -362,7 +361,8 @@ bool value_sett::eval_pointer_offset(
362361
if(!ptr_offset.has_value())
363362
return false;
364363

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

367367
if(mod && *ptr_offset != previous_offset)
368368
return false;
@@ -556,8 +556,11 @@ void value_sett::get_value_set_rec(
556556
}
557557
else if(expr.id()==ID_symbol)
558558
{
559-
auto entry_index = get_index_of_symbol(
560-
to_symbol_expr(expr).get_identifier(), expr.type(), suffix, ns);
559+
const symbol_exprt expr_l1 = is_ssa_expr(expr)
560+
? remove_level_2(to_ssa_expr(expr))
561+
: to_symbol_expr(expr);
562+
auto entry_index =
563+
get_index_of_symbol(expr_l1.get_identifier(), expr.type(), suffix, ns);
561564

562565
if(entry_index.has_value())
563566
make_union(dest, find_entry(*entry_index)->object_map);
@@ -623,7 +626,7 @@ void value_sett::get_value_set_rec(
623626
insert(
624627
dest,
625628
exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
626-
mp_integer{0});
629+
from_integer(0, c_index_type()));
627630
}
628631
else if(
629632
expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
@@ -655,7 +658,10 @@ void value_sett::get_value_set_rec(
655658

656659
if(op.is_zero())
657660
{
658-
insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
661+
insert(
662+
dest,
663+
exprt(ID_null_object, empty_typet{}),
664+
from_integer(0, c_index_type()));
659665
}
660666
else
661667
{
@@ -696,15 +702,14 @@ void value_sett::get_value_set_rec(
696702
throw expr.id_string()+" expected to have at least two operands";
697703

698704
object_mapt pointer_expr_set;
699-
std::optional<mp_integer> i;
705+
std::optional<exprt> additional_offset;
700706

701707
// special case for plus/minus and exactly one pointer
702708
std::optional<exprt> ptr_operand;
703709
if(
704710
expr.type().id() == ID_pointer &&
705711
(expr.id() == ID_plus || expr.id() == ID_minus))
706712
{
707-
bool non_const_offset = false;
708713
for(const auto &op : expr.operands())
709714
{
710715
if(op.type().id() == ID_pointer)
@@ -717,24 +722,20 @@ void value_sett::get_value_set_rec(
717722

718723
ptr_operand = op;
719724
}
720-
else if(!non_const_offset)
725+
else
721726
{
722-
auto offset = numeric_cast<mp_integer>(op);
723-
if(!offset.has_value())
724-
{
725-
i.reset();
726-
non_const_offset = true;
727-
}
727+
if(!additional_offset.has_value())
728+
additional_offset = op;
728729
else
729730
{
730-
if(!i.has_value())
731-
i = mp_integer{0};
732-
i = *i + *offset;
731+
additional_offset = plus_exprt{
732+
*additional_offset,
733+
typecast_exprt::conditional_cast(op, additional_offset->type())};
733734
}
734735
}
735736
}
736737

737-
if(ptr_operand.has_value() && i.has_value())
738+
if(ptr_operand.has_value() && additional_offset.has_value())
738739
{
739740
typet pointer_base_type =
740741
to_pointer_type(ptr_operand->type()).base_type();
@@ -745,18 +746,22 @@ void value_sett::get_value_set_rec(
745746

746747
if(!size.has_value() || (*size) == 0)
747748
{
748-
i.reset();
749+
additional_offset.reset();
749750
}
750751
else
751752
{
752-
*i *= *size;
753+
additional_offset = mult_exprt{
754+
*additional_offset, from_integer(*size, additional_offset->type())};
753755

754756
if(expr.id()==ID_minus)
755757
{
756758
DATA_INVARIANT(
757759
to_minus_expr(expr).lhs() == *ptr_operand,
758760
"unexpected subtraction of pointer from integer");
759-
i->negate();
761+
DATA_INVARIANT(
762+
additional_offset->type().id() != ID_unsignedbv,
763+
"offset type must support negation");
764+
additional_offset = unary_minus_exprt{*additional_offset};
760765
}
761766
}
762767
}
@@ -790,8 +795,15 @@ void value_sett::get_value_set_rec(
790795
offsett offset = it->second;
791796

792797
// adjust by offset
793-
if(offset && i.has_value())
794-
*offset += *i;
798+
if(offset && additional_offset.has_value())
799+
{
800+
offset = simplify_expr(
801+
plus_exprt{
802+
*offset,
803+
typecast_exprt::conditional_cast(
804+
*additional_offset, offset->type())},
805+
ns);
806+
}
795807
else
796808
offset.reset();
797809

@@ -871,7 +883,7 @@ void value_sett::get_value_set_rec(
871883
dynamic_object.set_instance(location_number);
872884
dynamic_object.valid()=true_exprt();
873885

874-
insert(dest, dynamic_object, mp_integer{0});
886+
insert(dest, dynamic_object, from_integer(0, c_index_type()));
875887
}
876888
else if(statement==ID_cpp_new ||
877889
statement==ID_cpp_new_array)
@@ -884,7 +896,7 @@ void value_sett::get_value_set_rec(
884896
dynamic_object.set_instance(location_number);
885897
dynamic_object.valid()=true_exprt();
886898

887-
insert(dest, dynamic_object, mp_integer{0});
899+
insert(dest, dynamic_object, from_integer(0, c_index_type()));
888900
}
889901
else
890902
insert(dest, exprt(ID_unknown, original_type));
@@ -1331,12 +1343,17 @@ void value_sett::get_reference_set_rec(
13311343
expr.id()==ID_string_constant ||
13321344
expr.id()==ID_array)
13331345
{
1346+
exprt l1_expr =
1347+
is_ssa_expr(expr) ? remove_level_2(to_ssa_expr(expr)) : expr;
1348+
13341349
if(
13351350
expr.type().id() == ID_array &&
13361351
to_array_type(expr.type()).element_type().id() == ID_array)
1337-
insert(dest, expr);
1352+
{
1353+
insert(dest, l1_expr);
1354+
}
13381355
else
1339-
insert(dest, expr, mp_integer{0});
1356+
insert(dest, l1_expr, from_integer(0, c_index_type()));
13401357

13411358
return;
13421359
}
@@ -1365,7 +1382,7 @@ void value_sett::get_reference_set_rec(
13651382

13661383
const index_exprt &index_expr=to_index_expr(expr);
13671384
const exprt &array=index_expr.array();
1368-
const exprt &offset=index_expr.index();
1385+
const exprt &index = index_expr.index();
13691386

13701387
DATA_INVARIANT(
13711388
array.type().id() == ID_array, "index takes array-typed operand");
@@ -1393,22 +1410,24 @@ void value_sett::get_reference_set_rec(
13931410
from_integer(0, c_index_type()));
13941411

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

1398-
if(offset.is_zero())
1399-
{
1400-
}
1401-
else if(i.has_value() && o)
1414+
if(!index.is_zero() && o.has_value())
14021415
{
14031416
auto size = pointer_offset_size(array_type.element_type(), ns);
14041417

14051418
if(!size.has_value() || *size == 0)
14061419
o.reset();
14071420
else
1408-
*o = *i * (*size);
1421+
{
1422+
o = simplify_expr(
1423+
plus_exprt{
1424+
*o,
1425+
typecast_exprt::conditional_cast(
1426+
mult_exprt{index, from_integer(*size, index.type())},
1427+
o->type())},
1428+
ns);
1429+
}
14091430
}
1410-
else
1411-
o.reset();
14121431

14131432
insert(dest, deref_index_expr, o);
14141433
}
@@ -1658,7 +1677,9 @@ void value_sett::assign_rec(
16581677

16591678
if(lhs.id()==ID_symbol)
16601679
{
1661-
const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
1680+
const symbol_exprt lhs_l1 =
1681+
is_ssa_expr(lhs) ? remove_level_2(to_ssa_expr(lhs)) : to_symbol_expr(lhs);
1682+
const irep_idt &identifier = lhs_l1.get_identifier();
16621683

16631684
update_entry(
16641685
entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets);
@@ -1864,8 +1885,11 @@ void value_sett::apply_code_rec(
18641885
(lhs_type.id() == ID_array &&
18651886
to_array_type(lhs_type).element_type().id() == ID_pointer))
18661887
{
1888+
const symbol_exprt lhs_l1 = is_ssa_expr(lhs)
1889+
? remove_level_2(to_ssa_expr(lhs))
1890+
: to_symbol_expr(lhs);
18671891
// assign the address of the failed object
1868-
if(auto failed = get_failed_symbol(to_symbol_expr(lhs), ns))
1892+
if(auto failed = get_failed_symbol(to_symbol_expr(lhs_l1), ns))
18691893
{
18701894
address_of_exprt address_of_expr(*failed, to_pointer_type(lhs.type()));
18711895
assign(lhs, address_of_expr, ns, false, false);

src/pointer-analysis/value_set.h

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

15-
#include <unordered_set>
16-
17-
#include <util/mp_arith.h>
1815
#include <util/reference_counting.h>
1916
#include <util/sharing_map.h>
2017

2118
#include "object_numbering.h"
2219
#include "value_sets.h"
2320

21+
#include <unordered_set>
22+
2423
class namespacet;
2524
class xmlt;
2625

@@ -76,9 +75,9 @@ class value_sett
7675
/// in value sets.
7776
static object_numberingt object_numbering;
7877

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;
78+
/// Represents the offset into an object: either some (possibly constant)
79+
/// expression, or an unknown value, represented by `!offset`.
80+
typedef std::optional<exprt> offsett;
8281

8382
/// Represents a set of expressions (`exprt` instances) with corresponding
8483
/// offsets (`offsett` instances). This is the RHS set of a single row of
@@ -140,20 +139,6 @@ class value_sett
140139
return insert(dest, object_numbering.number(src), offsett());
141140
}
142141

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-
157142
/// Adds a numbered expression and offset to an object map. If the
158143
/// destination map has an existing element for the same expression
159144
/// with a differing offset its offset is marked unknown.

0 commit comments

Comments
 (0)