Skip to content

Commit b511a1a

Browse files
author
Daniel Kroening
committed
simplify_byte_extract and simplify_byte_update now have new interface
This improves memory safety.
1 parent ab071ae commit b511a1a

File tree

2 files changed

+80
-91
lines changed

2 files changed

+80
-91
lines changed

src/util/simplify_expr.cpp

Lines changed: 78 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -1872,17 +1872,19 @@ optionalt<std::reference_wrapper<const array_exprt>>
18721872
return optionalt<std::reference_wrapper<const array_exprt>>(char_seq);
18731873
}
18741874

1875-
bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
1875+
simplify_exprt::resultt<>
1876+
simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
18761877
{
18771878
// lift up any ID_if on the object
18781879
if(expr.op().id()==ID_if)
18791880
{
18801881
if_exprt if_expr=lift_if(expr, 0);
1881-
simplify_byte_extract(to_byte_extract_expr(if_expr.true_case()));
1882-
simplify_byte_extract(to_byte_extract_expr(if_expr.false_case()));
1882+
if_expr.true_case() =
1883+
simplify_byte_extract(to_byte_extract_expr(if_expr.true_case()));
1884+
if_expr.false_case() =
1885+
simplify_byte_extract(to_byte_extract_expr(if_expr.false_case()));
18831886
simplify_if(if_expr);
1884-
expr.swap(if_expr);
1885-
return false;
1887+
return std::move(if_expr);
18861888
}
18871889

18881890
const auto el_size = pointer_offset_bits(expr.type(), ns);
@@ -1891,15 +1893,14 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
18911893
// byte_extract(root, offset1+offset2)
18921894
if(expr.op().id()==expr.id())
18931895
{
1894-
expr.offset()=plus_exprt(
1895-
to_byte_extract_expr(expr.op()).offset(),
1896-
expr.offset());
1897-
simplify_plus(expr.offset());
1896+
auto tmp = expr;
18981897

1899-
expr.op()=to_byte_extract_expr(expr.op()).op();
1900-
simplify_byte_extract(expr);
1898+
tmp.offset() =
1899+
plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset());
1900+
simplify_plus(tmp.offset());
19011901

1902-
return false;
1902+
tmp.op() = to_byte_extract_expr(expr.op()).op();
1903+
return changed(simplify_byte_extract(tmp)); // recursive call
19031904
}
19041905

19051906
// byte_extract(byte_update(root, offset, value), offset) =>
@@ -1915,28 +1916,24 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
19151916

19161917
if(expr.type() == op_byte_update.value().type())
19171918
{
1918-
exprt tmp = op_byte_update.value();
1919-
expr.swap(tmp);
1920-
1921-
return false;
1919+
return op_byte_update.value();
19221920
}
19231921
else if(
19241922
el_size.has_value() &&
19251923
*el_size <= pointer_offset_bits(op_byte_update.value().type(), ns))
19261924
{
1927-
expr.op() = op_byte_update.value();
1928-
expr.offset()=from_integer(0, expr.offset().type());
1925+
auto tmp = expr;
1926+
tmp.op() = op_byte_update.value();
1927+
tmp.offset() = from_integer(0, expr.offset().type());
19291928

1930-
simplify_byte_extract(expr);
1931-
1932-
return false;
1929+
return changed(simplify_byte_extract(tmp)); // recursive call
19331930
}
19341931
}
19351932

19361933
// the following require a constant offset
19371934
auto offset = numeric_cast<mp_integer>(expr.offset());
19381935
if(!offset.has_value() || *offset < 0)
1939-
return true;
1936+
return unchanged(expr);
19401937

19411938
// don't do any of the following if endianness doesn't match, as
19421939
// bytes need to be swapped
@@ -1945,25 +1942,19 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
19451942
// byte extract of full object is object
19461943
if(expr.type() == expr.op().type())
19471944
{
1948-
exprt tmp = expr.op();
1949-
expr.swap(tmp);
1950-
1951-
return false;
1945+
return expr.op();
19521946
}
19531947
else if(
19541948
expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
19551949
{
1956-
typecast_exprt tc(expr.op(), expr.type());
1957-
expr.swap(tc);
1958-
1959-
return false;
1950+
return typecast_exprt(expr.op(), expr.type());
19601951
}
19611952
}
19621953

19631954
// no proper simplification for expr.type()==void
19641955
// or types of unknown size
19651956
if(!el_size.has_value() || *el_size == 0)
1966-
return true;
1957+
return unchanged(expr);
19671958

19681959
if(expr.op().id()==ID_array_of &&
19691960
to_array_of_expr(expr.op()).op().id()==ID_constant)
@@ -1973,7 +1964,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
19731964
byte_extract_id()==ID_byte_extract_little_endian);
19741965

19751966
if(!const_bits_opt.has_value())
1976-
return true;
1967+
return unchanged(expr);
19771968

19781969
std::string const_bits=const_bits_opt.value();
19791970

@@ -1992,22 +1983,20 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
19921983
el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian);
19931984

19941985
if(tmp.has_value())
1995-
{
1996-
expr.swap(*tmp);
1997-
return false;
1998-
}
1986+
return std::move(*tmp);
19991987
}
20001988

20011989
// in some cases we even handle non-const array_of
20021990
if(
20031991
expr.op().id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
20041992
*el_size <= pointer_offset_bits(expr.op().op0().type(), ns))
20051993
{
2006-
expr.op()=index_exprt(expr.op(), expr.offset());
2007-
expr.offset()=from_integer(0, expr.offset().type());
2008-
simplify_rec(expr);
1994+
auto tmp = expr;
1995+
tmp.op() = index_exprt(expr.op(), expr.offset());
1996+
tmp.offset() = from_integer(0, expr.offset().type());
1997+
simplify_rec(tmp);
20091998

2010-
return false;
1999+
return std::move(tmp);
20112000
}
20122001

20132002
// extract bits of a constant
@@ -2044,42 +2033,37 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
20442033
bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian);
20452034

20462035
if(tmp.has_value())
2047-
{
2048-
expr.swap(*tmp);
2049-
2050-
return false;
2051-
}
2036+
return std::move(*tmp);
20522037
}
20532038

20542039
// try to refine it down to extracting from a member or an index in an array
20552040
auto subexpr =
20562041
get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
20572042
if(!subexpr.has_value() || subexpr.value() == expr)
2058-
return true;
2043+
return unchanged(expr);
20592044

20602045
simplify_rec(subexpr.value());
2061-
expr.swap(subexpr.value());
2062-
return false;
2046+
return subexpr.value();
20632047
}
20642048

2065-
bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
2049+
simplify_exprt::resultt<>
2050+
simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
20662051
{
2067-
const byte_update_exprt &expr_const = expr;
20682052
// byte_update(byte_update(root, offset, value), offset, value2) =>
20692053
// byte_update(root, offset, value2)
20702054
if(
2071-
expr_const.id() == expr_const.op().id() &&
2072-
expr_const.offset() == to_byte_update_expr(expr_const.op()).offset() &&
2073-
expr_const.value().type() ==
2074-
to_byte_update_expr(expr_const.op()).value().type())
2055+
expr.id() == expr.op().id() &&
2056+
expr.offset() == to_byte_update_expr(expr.op()).offset() &&
2057+
expr.value().type() == to_byte_update_expr(expr.op()).value().type())
20752058
{
2076-
expr.set_op(expr_const.op().op0());
2077-
return false;
2059+
auto tmp = expr;
2060+
tmp.set_op(expr.op().op0());
2061+
return std::move(tmp);
20782062
}
20792063

2080-
const exprt &root = expr_const.op();
2081-
const exprt &offset = expr_const.offset();
2082-
const exprt &value = expr_const.value();
2064+
const exprt &root = expr.op();
2065+
const exprt &offset = expr.offset();
2066+
const exprt &value = expr.value();
20832067
const auto val_size = pointer_offset_bits(value.type(), ns);
20842068
const auto root_size = pointer_offset_bits(root.type(), ns);
20852069

@@ -2094,10 +2078,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
20942078
ID_byte_extract_big_endian,
20952079
value, offset, expr.type());
20962080

2097-
simplify_byte_extract(be);
2098-
expr.swap(be);
2099-
2100-
return false;
2081+
return changed(simplify_byte_extract(be));
21012082
}
21022083

21032084
/*
@@ -2109,7 +2090,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
21092090
*/
21102091

21112092
if(expr.id()!=ID_byte_update_little_endian)
2112-
return true;
2093+
return unchanged(expr);
21132094

21142095
if(value.id()==ID_with)
21152096
{
@@ -2123,9 +2104,9 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
21232104
root and offset of update and extract
21242105
are the same */
21252106
if(!(root==extract.op()))
2126-
return true;
2107+
return unchanged(expr);
21272108
if(!(offset==extract.offset()))
2128-
return true;
2109+
return unchanged(expr);
21292110

21302111
const typet &tp=ns.follow(with.type());
21312112
if(tp.id()==ID_struct)
@@ -2149,10 +2130,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
21492130
plus_exprt new_offset(offset, compo_offset);
21502131
simplify_node(new_offset);
21512132
exprt new_value(with.new_value());
2152-
expr.set_offset(std::move(new_offset));
2153-
expr.set_value(std::move(new_value));
2154-
simplify_byte_update(expr); // do this recursively
2155-
return false;
2133+
auto tmp = expr;
2134+
tmp.set_offset(std::move(new_offset));
2135+
tmp.set_value(std::move(new_value));
2136+
return changed(simplify_byte_update(tmp)); // recursive call
21562137
}
21572138
}
21582139
}
@@ -2176,10 +2157,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
21762157
plus_exprt new_offset(offset, index_offset);
21772158
simplify_node(new_offset);
21782159
exprt new_value(with.new_value());
2179-
expr.set_offset(std::move(new_offset));
2180-
expr.set_value(std::move(new_value));
2181-
simplify_byte_update(expr); // do this recursively
2182-
return false;
2160+
auto tmp = expr;
2161+
tmp.set_offset(std::move(new_offset));
2162+
tmp.set_value(std::move(new_value));
2163+
return changed(simplify_byte_update(tmp)); // recursive call
21832164
}
21842165
}
21852166
}
@@ -2188,13 +2169,13 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
21882169
// the following require a constant offset
21892170
const auto offset_int = numeric_cast<mp_integer>(offset);
21902171
if(!offset_int.has_value() || *offset_int < 0)
2191-
return true;
2172+
return unchanged(expr);
21922173

21932174
const typet &op_type=ns.follow(root.type());
21942175

21952176
// size must be known
21962177
if(!val_size.has_value() || *val_size == 0)
2197-
return true;
2178+
return unchanged(expr);
21982179

21992180
// Are we updating (parts of) a struct? Do individual member updates
22002181
// instead, unless there are non-byte-sized bit fields
@@ -2287,17 +2268,13 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
22872268
if(result_expr.is_not_nil())
22882269
{
22892270
simplify_rec(result_expr);
2290-
expr.swap(result_expr);
2291-
2292-
return false;
2271+
return result_expr;
22932272
}
22942273

22952274
if(result_expr.is_not_nil())
22962275
{
22972276
simplify_rec(result_expr);
2298-
expr.swap(result_expr);
2299-
2300-
return false;
2277+
return result_expr;
23012278
}
23022279
}
23032280

@@ -2310,7 +2287,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
23102287
if(!el_size.has_value() || *el_size == 0 ||
23112288
(*el_size) % 8 != 0 || (*val_size) % 8 != 0)
23122289
{
2313-
return true;
2290+
return unchanged(expr);
23142291
}
23152292

23162293
exprt result=root;
@@ -2350,12 +2327,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
23502327
m_offset_bits += *el_size;
23512328
}
23522329

2353-
expr.swap(result);
2354-
2355-
return false;
2330+
return std::move(result);
23562331
}
23572332

2358-
return true;
2333+
return unchanged(expr);
23592334
}
23602335

23612336
bool simplify_exprt::simplify_complex(exprt &expr)
@@ -2451,10 +2426,24 @@ bool simplify_exprt::simplify_node(exprt &expr)
24512426
no_change = simplify_member(expr) && no_change;
24522427
else if(expr.id()==ID_byte_update_little_endian ||
24532428
expr.id()==ID_byte_update_big_endian)
2454-
no_change = simplify_byte_update(to_byte_update_expr(expr)) && no_change;
2429+
{
2430+
auto r = simplify_byte_update(to_byte_update_expr(expr));
2431+
if(r.has_changed())
2432+
{
2433+
no_change = false;
2434+
expr = r.expr;
2435+
}
2436+
}
24552437
else if(expr.id()==ID_byte_extract_little_endian ||
24562438
expr.id()==ID_byte_extract_big_endian)
2457-
no_change = simplify_byte_extract(to_byte_extract_expr(expr)) && no_change;
2439+
{
2440+
auto r = simplify_byte_extract(to_byte_extract_expr(expr));
2441+
if(r.has_changed())
2442+
{
2443+
no_change = false;
2444+
expr = r.expr;
2445+
}
2446+
}
24582447
else if(expr.id()==ID_pointer_object)
24592448
no_change = simplify_pointer_object(expr) && no_change;
24602449
else if(expr.id() == ID_is_dynamic_object)

src/util/simplify_expr_class.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -140,8 +140,8 @@ class simplify_exprt
140140
bool simplify_update(exprt &expr);
141141
bool simplify_index(exprt &expr);
142142
bool simplify_member(exprt &expr);
143-
bool simplify_byte_update(byte_update_exprt &expr);
144-
bool simplify_byte_extract(byte_extract_exprt &expr);
143+
resultt<> simplify_byte_update(const byte_update_exprt &);
144+
resultt<> simplify_byte_extract(const byte_extract_exprt &);
145145
bool simplify_pointer_object(exprt &expr);
146146
bool simplify_object_size(exprt &expr);
147147
bool simplify_dynamic_size(exprt &expr);

0 commit comments

Comments
 (0)