Skip to content

Commit ea0523d

Browse files
tautschnigtautschnig
committed
Configure bits_per_byte in byte_extract/byte_update expression
Semantically evaluating a byte_extract/byte_update expression requires knowledge of the number of bits that a byte is composed of. This, however, is a configuration parameter known to the front-end that created the expression in the first place. The back-end should not need to consult configuration information to evaluate the expression.
1 parent a8cfa6f commit ea0523d

24 files changed

+384
-168
lines changed

‎jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ Author: Diffblue Ltd.
1717
#include <util/byte_operators.h>
1818
#include <util/pointer_expr.h>
1919

20+
#include <climits>
21+
2022
TEST_CASE("java trace validation", "[core][java_trace_validation]")
2123
{
2224
const exprt plain_expr = exprt();
@@ -33,9 +35,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
3335
index_exprt(valid_symbol_expr, valid_constant);
3436
const index_exprt index_plain = index_exprt(exprt(), exprt());
3537
const byte_extract_exprt byte_little_endian = byte_extract_exprt(
36-
ID_byte_extract_little_endian, exprt(), exprt(), typet());
37-
const byte_extract_exprt byte_big_endian =
38-
byte_extract_exprt(ID_byte_extract_big_endian, exprt(), exprt(), typet());
38+
ID_byte_extract_little_endian, exprt(), exprt(), CHAR_BIT, typet());
39+
const byte_extract_exprt byte_big_endian = byte_extract_exprt(
40+
ID_byte_extract_big_endian, exprt(), exprt(), CHAR_BIT, typet());
3941
const address_of_exprt valid_address = address_of_exprt(valid_symbol_expr);
4042
const address_of_exprt invalid_address = address_of_exprt(exprt());
4143
const struct_exprt struct_plain =

‎scripts/expected_doxygen_warnings.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes
2323
warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
2424
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
2525
warning: Included by graph for 'c_types.h' not generated, too many nodes (144), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
26-
warning: Included by graph for 'config.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
26+
warning: Included by graph for 'config.h' not generated, too many nodes (84), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
2727
warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
2828
warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
2929
warning: Included by graph for 'expr_util.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

‎src/analyses/goto_rw.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ void rw_range_sett::get_objects_byte_extract(
157157
get_objects_rec(mode, be.op(), -1, size);
158158
else
159159
{
160-
*index *= 8;
160+
*index *= be.get_bits_per_byte();
161161
if(*index >= *pointer_offset_bits(be.op().type(), ns))
162162
return;
163163

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -542,8 +542,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
542542

543543
if(current_symbol.is_static_lifetime)
544544
{
545-
byte_update_exprt byte_update{
546-
byte_update_id(), *dest, from_integer(0, index_type()), *zero};
545+
byte_update_exprt byte_update{byte_update_id(),
546+
*dest,
547+
from_integer(0, index_type()),
548+
*zero,
549+
config.ansi_c.char_width};
547550
byte_update.add_source_location() = value.source_location();
548551
*dest = std::move(byte_update);
549552
dest = &(to_byte_update_expr(*dest).op2());

‎src/goto-programs/rewrite_union.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/arith_tools.h>
1515
#include <util/byte_operators.h>
1616
#include <util/c_types.h>
17+
#include <util/config.h>
1718
#include <util/pointer_expr.h>
1819
#include <util/std_code.h>
1920
#include <util/std_expr.h>
@@ -84,7 +85,8 @@ void rewrite_union(exprt &expr)
8485
if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
8586
{
8687
exprt offset=from_integer(0, index_type());
87-
byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
88+
byte_extract_exprt tmp(
89+
byte_extract_id(), op, offset, config.ansi_c.char_width, expr.type());
8890
expr=tmp;
8991
}
9092
}
@@ -94,7 +96,11 @@ void rewrite_union(exprt &expr)
9496
exprt offset=from_integer(0, index_type());
9597
side_effect_expr_nondett nondet(expr.type(), expr.source_location());
9698
byte_update_exprt tmp(
97-
byte_update_id(), nondet, offset, union_expr.op());
99+
byte_update_id(),
100+
nondet,
101+
offset,
102+
union_expr.op(),
103+
config.ansi_c.char_width);
98104
expr=tmp;
99105
}
100106
}

‎src/goto-symex/symex_assign.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
1111

1212
#include "symex_assign.h"
1313

14-
#include "expr_skeleton.h"
15-
#include "goto_symex.h"
16-
#include "goto_symex_state.h"
1714
#include <util/byte_operators.h>
1815
#include <util/expr_util.h>
1916
#include <util/format_expr.h>
2017

18+
#include "expr_skeleton.h"
19+
#include "goto_symex.h"
20+
#include "goto_symex_state.h"
21+
2122
// We can either use with_exprt or update_exprt when building expressions that
2223
// modify components of an array or a struct. Set USE_UPDATE to use
2324
// update_exprt.
@@ -377,7 +378,8 @@ void symex_assignt::assign_byte_extract(
377378
else
378379
UNREACHABLE;
379380

380-
const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
381+
const byte_update_exprt new_rhs{
382+
byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
381383
const expr_skeletont new_skeleton =
382384
full_lhs.compose(expr_skeletont::remove_op0(lhs));
383385
assign_rec(lhs.op(), new_skeleton, new_rhs, guard);

‎src/goto-symex/symex_clean_expr.cpp

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/arith_tools.h>
1515
#include <util/byte_operators.h>
1616
#include <util/c_types.h>
17+
#include <util/config.h>
1718
#include <util/expr_iterator.h>
1819
#include <util/nodiscard.h>
1920
#include <util/pointer_offset_size.h>
@@ -46,6 +47,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
4647
byte_extract_id(),
4748
if_expr.false_case(),
4849
from_integer(0, index_type()),
50+
config.ansi_c.char_width,
4951
if_expr.true_case().type());
5052

5153
if_expr.false_case().swap(be);
@@ -95,6 +97,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
9597
byte_extract_id(),
9698
expr,
9799
from_integer(0, index_type()),
100+
config.ansi_c.char_width,
98101
array_typet(char_type(), array_size.value()));
99102
}
100103

@@ -123,12 +126,12 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
123126

124127
array_typet new_array_type(subtype, new_size);
125128

126-
expr =
127-
byte_extract_exprt(
128-
byte_extract_id(),
129-
expr,
130-
ode.offset(),
131-
new_array_type);
129+
expr = byte_extract_exprt(
130+
byte_extract_id(),
131+
expr,
132+
ode.offset(),
133+
config.ansi_c.char_width,
134+
new_array_type);
132135
}
133136
}
134137
}

‎src/goto-symex/symex_dereference.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/arith_tools.h>
1515
#include <util/byte_operators.h>
1616
#include <util/c_types.h>
17+
#include <util/config.h>
1718
#include <util/exception_utils.h>
1819
#include <util/expr_iterator.h>
1920
#include <util/expr_util.h>
@@ -96,7 +97,11 @@ exprt goto_symext::address_arithmetic(
9697
ode.build(expr, ns);
9798

9899
const byte_extract_exprt be(
99-
byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
100+
byte_extract_id(),
101+
ode.root_object(),
102+
ode.offset(),
103+
config.ansi_c.char_width,
104+
expr.type());
100105

101106
// recursive call
102107
result = address_arithmetic(be, state, keep_array);
@@ -155,6 +160,7 @@ exprt goto_symext::address_arithmetic(
155160
byte_extract_id(),
156161
to_ssa_expr(expr).get_l1_object(),
157162
from_integer(offset, index_type()),
163+
config.ansi_c.char_width,
158164
expr.type());
159165

160166
result = address_arithmetic(be, state, keep_array);

‎src/goto-symex/symex_function_call.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <util/arith_tools.h>
1616
#include <util/byte_operators.h>
1717
#include <util/c_types.h>
18+
#include <util/config.h>
1819
#include <util/exception_utils.h>
1920
#include <util/fresh_symbol.h>
2021
#include <util/invariant.h>
@@ -113,6 +114,7 @@ void goto_symext::parameter_assignments(
113114
byte_extract_id(),
114115
rhs,
115116
from_integer(0, index_type()),
117+
config.ansi_c.char_width,
116118
parameter_type);
117119
}
118120
// clang-format on

‎src/goto-symex/symex_other.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
1414
#include <util/arith_tools.h>
1515
#include <util/byte_operators.h>
1616
#include <util/c_types.h>
17+
#include <util/config.h>
1718
#include <util/pointer_offset_size.h>
1819

1920
void goto_symext::havoc_rec(
@@ -148,6 +149,7 @@ void goto_symext::symex_other(
148149
byte_extract_id(),
149150
src_array,
150151
from_integer(0, index_type()),
152+
config.ansi_c.char_width,
151153
dest_array.type());
152154
src_array.swap(be);
153155
do_simplify(src_array);
@@ -159,6 +161,7 @@ void goto_symext::symex_other(
159161
byte_extract_id(),
160162
dest_array,
161163
from_integer(0, index_type()),
164+
config.ansi_c.char_width,
162165
src_array.type());
163166
dest_array.swap(be);
164167
do_simplify(dest_array);
@@ -200,6 +203,7 @@ void goto_symext::symex_other(
200203
byte_extract_id(),
201204
array_expr,
202205
from_integer(0, index_type()),
206+
config.ansi_c.char_width,
203207
array_typet(char_type(), array_size.value()));
204208
}
205209

‎src/pointer-analysis/value_set_dereference.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -534,6 +534,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
534534
byte_extract_id(),
535535
symbol_expr,
536536
pointer_offset(pointer_expr),
537+
config.ansi_c.char_width,
537538
dereference_type);
538539
result.pointer = address_of_exprt{result.value};
539540
}
@@ -768,7 +769,8 @@ bool value_set_dereferencet::memory_model_bytes(
768769
else
769770
{
770771
// no, use 'byte_extract'
771-
result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
772+
result = byte_extract_exprt(
773+
byte_extract_id(), value, offset, config.ansi_c.char_width, to_type);
772774
}
773775

774776
value=result;

‎src/solvers/flattening/boolbv_byte_extract.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -49,11 +49,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
4949
#if 0
5050
if(expr.id()==ID_byte_extract_big_endian &&
5151
expr.type().id()==ID_c_bit_field &&
52-
(width%8)!=0)
52+
(width%expr.get_bits_per_byte())!=0)
5353
{
5454
byte_extract_exprt tmp=expr;
5555
// round up
56-
to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
56+
to_c_bit_field_type(tmp.type()).set_width(
57+
width+expr.get_bits_per_byte()-width%expr.get_bits_per_byte());
5758
convert_byte_extract(tmp, bv);
5859
bv.resize(width); // chop down
5960
return;
@@ -87,6 +88,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
8788
expr.id(),
8889
o.root_object(),
8990
plus_exprt(o.offset(), expr.offset()),
91+
expr.get_bits_per_byte(),
9092
expr.type());
9193

9294
return convert_bv(be);
@@ -108,11 +110,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
108110
bv.resize(width);
109111

110112
// see if the byte number is constant
111-
unsigned byte_width=8;
112-
113113
if(index.has_value())
114114
{
115-
const mp_integer offset = *index * byte_width;
115+
const mp_integer offset = *index * expr.get_bits_per_byte();
116116

117117
for(std::size_t i=0; i<width; i++)
118118
// out of bounds?
@@ -123,7 +123,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
123123
}
124124
else
125125
{
126-
std::size_t bytes=op_bv.size()/byte_width;
126+
std::size_t bytes = op_bv.size() / expr.get_bits_per_byte();
127127

128128
if(prop.has_set_to())
129129
{
@@ -141,7 +141,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
141141

142142
for(std::size_t i=0; i<bytes; i++)
143143
{
144-
std::size_t offset=i*byte_width;
144+
std::size_t offset = i * expr.get_bits_per_byte();
145145

146146
for(std::size_t j=0; j<width; j++)
147147
if(offset+j<op_bv.size())
@@ -164,7 +164,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
164164
literalt e =
165165
convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
166166

167-
std::size_t offset=i*byte_width;
167+
std::size_t offset = i * expr.get_bits_per_byte();
168168

169169
for(std::size_t j=0; j<width; j++)
170170
{

‎src/solvers/flattening/boolbv_byte_update.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
3939

4040
const bvt &value_bv=convert_bv(value);
4141
std::size_t update_width=value_bv.size();
42-
std::size_t byte_width=8;
42+
std::size_t byte_width = expr.get_bits_per_byte();
4343

4444
if(update_width>bv.size())
4545
update_width=bv.size();
@@ -50,7 +50,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
5050
if(index.has_value())
5151
{
5252
// yes!
53-
const mp_integer offset = *index * 8;
53+
const mp_integer offset = *index * byte_width;
5454

5555
if(offset+update_width>mp_integer(bv.size()) || offset<0)
5656
{

‎src/solvers/flattening/boolbv_index.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
1111
#include <algorithm>
1212

1313
#include <util/arith_tools.h>
14+
#include <util/config.h>
1415
#include <util/cprover_prefix.h>
1516
#include <util/pointer_expr.h>
1617
#include <util/pointer_offset_size.h>
@@ -347,7 +348,11 @@ bvt boolbvt::convert_index(
347348
ns);
348349

349350
byte_extract_exprt be(
350-
byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
351+
byte_extract_id(),
352+
o.root_object(),
353+
new_offset,
354+
config.ansi_c.char_width,
355+
array_type.subtype());
351356

352357
return convert_bv(be);
353358
}

0 commit comments

Comments
 (0)