Skip to content

Commit ca225ec

Browse files
tautschnigtautschnig
committed
boolbv_width: distinguish zero from unknown size
Use optionalt to distinguish types of known-zero size from those with unknown size, which previously had the default value of zero. This makes it possible to support index expressions over zero bitwidth arrays without mistaking the situation for an unknown size. (There is not really anything wrong in having empty bitvectors, which we otherwise already support (as of e021eef).)
1 parent 15d60af commit ca225ec

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+602
-344
lines changed

‎regression/cbmc/dynamic_sizeof1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-z3-smt-backend
22
main.c
33

44
^EXIT=0$

‎regression/cbmc/vla1/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
1-
CORE
1+
CORE broken-cprover-smt-backend
22
main.c
33

44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
^warning: ignoring
9+
--
10+
The SMT back-end does not correctly support structs with non-constant size,
11+
unless named data types are used (as is the case with Z3).

‎src/solvers/flattening/boolbv.cpp

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,11 @@ bvt boolbvt::conversion_failed(const exprt &expr)
8585
ignoring(expr);
8686

8787
// try to make it free bits
88-
std::size_t width=boolbv_width(expr.type());
89-
return prop.new_variables(width);
88+
// TODO we likely end up in this path when an earlier call to boolbv_width
89+
// failed
90+
const auto &width_opt = boolbv_width(expr.type());
91+
CHECK_RETURN(width_opt.has_value());
92+
return prop.new_variables(*width_opt);
9093
}
9194

9295
/// Converts an expression into its gate-level representation and returns a
@@ -234,11 +237,12 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
234237

235238
bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
236239
{
237-
std::size_t width=boolbv_width(expr.type());
238-
239-
if(width==0)
240+
const auto &width_opt = boolbv_width(expr.type());
241+
if(!width_opt.has_value())
240242
return conversion_failed(expr);
241243

244+
const std::size_t width = *width_opt;
245+
242246
const exprt &array_size = expr.type().size();
243247

244248
const auto size = numeric_cast<mp_integer>(array_size);
@@ -276,7 +280,9 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
276280
bvt boolbvt::convert_symbol(const exprt &expr)
277281
{
278282
const typet &type=expr.type();
279-
std::size_t width=boolbv_width(type);
283+
const auto &width_opt = boolbv_width(type);
284+
CHECK_RETURN(width_opt.has_value());
285+
const std::size_t width = *width_opt;
280286

281287
const irep_idt &identifier = expr.get(ID_identifier);
282288
CHECK_RETURN(!identifier.empty());
@@ -304,7 +310,9 @@ bvt boolbvt::convert_function_application(
304310
functions.record(expr);
305311

306312
// make it free bits
307-
return prop.new_variables(boolbv_width(expr.type()));
313+
const auto &width_opt = boolbv_width(expr.type());
314+
CHECK_RETURN(width_opt.has_value());
315+
return prop.new_variables(*width_opt);
308316
}
309317

310318

@@ -515,12 +523,12 @@ bool boolbvt::is_unbounded_array(const typet &type) const
515523
if(unbounded_array==unbounded_arrayt::U_ALL)
516524
return true;
517525

518-
const std::size_t size = boolbv_width(type);
519-
if(size == 0)
526+
const auto &size_opt = boolbv_width(type);
527+
if(!size_opt.has_value())
520528
return true;
521529

522530
if(unbounded_array==unbounded_arrayt::U_AUTO)
523-
if(size > MAX_FLATTENED_ARRAY_SIZE)
531+
if(*size_opt > MAX_FLATTENED_ARRAY_SIZE)
524532
return true;
525533

526534
return false;
@@ -564,7 +572,9 @@ boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src)
564572
for(const auto &comp : components)
565573
{
566574
dest.push_back(offset);
567-
offset += boolbv_width(comp.type());
575+
const auto &comp_width_opt = boolbv_width(comp.type());
576+
CHECK_RETURN(comp_width_opt.has_value());
577+
offset += *comp_width_opt;
568578
}
569579
return dest;
570580
}

‎src/solvers/flattening/boolbv.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ class boolbvt:public arrayst
9898
return map;
9999
}
100100

101-
virtual std::size_t boolbv_width(const typet &type) const
101+
virtual optionalt<std::size_t> boolbv_width(const typet &type) const
102102
{
103103
return bv_width(type);
104104
}

‎src/solvers/flattening/boolbv_abs.cpp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,6 @@ Author: Daniel Kroening, [email protected]
1616

1717
bvt boolbvt::convert_abs(const abs_exprt &expr)
1818
{
19-
const std::size_t width = boolbv_width(expr.type());
20-
21-
if(width==0)
22-
return conversion_failed(expr);
23-
2419
const bvt &op_bv=convert_bv(expr.op());
2520

2621
if(expr.op().type()!=expr.type())

‎src/solvers/flattening/boolbv_add_sub.cpp

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,12 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
3030
type.id()!=ID_vector)
3131
return conversion_failed(expr);
3232

33-
std::size_t width=boolbv_width(type);
34-
35-
if(width==0)
33+
const auto &width_opt = boolbv_width(type);
34+
if(!width_opt.has_value())
3635
return conversion_failed(expr);
3736

37+
const std::size_t width = *width_opt;
38+
3839
const exprt::operandst &operands=expr.operands();
3940

4041
DATA_INVARIANT(
@@ -73,8 +74,10 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
7374

7475
if(type.id()==ID_vector || type.id()==ID_complex)
7576
{
76-
std::size_t sub_width =
77+
const auto &sub_width_opt =
7778
boolbv_width(to_type_with_subtype(type).subtype());
79+
CHECK_RETURN(sub_width_opt.has_value());
80+
const std::size_t sub_width = *sub_width_opt;
7881

7982
INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
8083
INVARIANT(
@@ -158,11 +161,12 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
158161
return conversion_failed(expr);
159162
}
160163

161-
std::size_t width = boolbv_width(type);
162-
163-
if(width == 0)
164+
const auto &width_opt = boolbv_width(type);
165+
if(!width_opt.has_value())
164166
return conversion_failed(expr);
165167

168+
const std::size_t width = *width_opt;
169+
166170
DATA_INVARIANT(
167171
expr.lhs().type() == type && expr.rhs().type() == type,
168172
"saturating add/sub with mixed types:\n" + expr.pretty());
@@ -184,7 +188,10 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
184188
if(type.id() != ID_vector && type.id() != ID_complex)
185189
return bv_utils.saturating_add_sub(bv, op, subtract, rep);
186190

187-
std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
191+
const auto &sub_width_opt =
192+
boolbv_width(to_type_with_subtype(type).subtype());
193+
CHECK_RETURN(sub_width_opt.has_value());
194+
const std::size_t sub_width = *sub_width_opt;
188195

189196
INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
190197
INVARIANT(

‎src/solvers/flattening/boolbv_array.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,10 @@ Author: Daniel Kroening, [email protected]
1515
/// Return an empty vector if the width is zero or the array has no elements.
1616
bvt boolbvt::convert_array(const exprt &expr)
1717
{
18-
const std::size_t width = boolbv_width(expr.type());
18+
const auto &width_opt = boolbv_width(expr.type());
19+
CHECK_RETURN(width_opt.has_value());
20+
const std::size_t width = *width_opt;
21+
1922
const exprt::operandst &operands = expr.operands();
2023

2124
if(operands.empty() && width == 0)

‎src/solvers/flattening/boolbv_array_of.cpp

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -23,17 +23,13 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
2323
if(is_unbounded_array(array_type))
2424
return conversion_failed(expr);
2525

26-
std::size_t width=boolbv_width(array_type);
26+
const auto &width_opt = boolbv_width(array_type);
27+
if(!width_opt.has_value())
28+
return conversion_failed(expr);
29+
else if(*width_opt == 0)
30+
return bvt{};
2731

28-
if(width==0)
29-
{
30-
// A zero-length array is acceptable;
31-
// an element with unknown size is not.
32-
if(boolbv_width(array_type.element_type()) == 0)
33-
return conversion_failed(expr);
34-
else
35-
return bvt();
36-
}
32+
const std::size_t width = *width_opt;
3733

3834
const exprt &array_size=array_type.size();
3935

‎src/solvers/flattening/boolbv_bitreverse.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,12 @@ Author: Michael Tautschnig
1212

1313
bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr)
1414
{
15-
const std::size_t width = boolbv_width(expr.type());
16-
if(width == 0)
15+
const auto &width_opt = boolbv_width(expr.type());
16+
if(!width_opt.has_value())
1717
return conversion_failed(expr);
1818

19+
const std::size_t width = *width_opt;
20+
1921
bvt bv = convert_bv(expr.op(), width);
2022

2123
std::reverse(bv.begin(), bv.end());

‎src/solvers/flattening/boolbv_bitwise.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,12 @@ Author: Daniel Kroening, [email protected]
1212

1313
bvt boolbvt::convert_bitwise(const exprt &expr)
1414
{
15-
const std::size_t width = boolbv_width(expr.type());
16-
if(width==0)
15+
const auto &width_opt = boolbv_width(expr.type());
16+
if(!width_opt.has_value())
1717
return conversion_failed(expr);
1818

19+
const std::size_t width = *width_opt;
20+
1921
if(expr.id()==ID_bitnot)
2022
{
2123
const exprt &op = to_bitnot_expr(expr).op();

‎src/solvers/flattening/boolbv_bswap.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,11 @@ Author: Michael Tautschnig
1212

1313
bvt boolbvt::convert_bswap(const bswap_exprt &expr)
1414
{
15-
const std::size_t width = boolbv_width(expr.type());
15+
const auto &width_opt = boolbv_width(expr.type());
16+
if(!width_opt.has_value())
17+
return conversion_failed(expr);
18+
19+
const std::size_t width = *width_opt;
1620

1721
// width must be multiple of bytes
1822
const std::size_t byte_bits = expr.get_bits_per_byte();

‎src/solvers/flattening/boolbv_byte_extract.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,11 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
4141
return convert_bv(lower_byte_extract(expr, ns));
4242
}
4343

44-
const std::size_t width = boolbv_width(expr.type());
44+
const auto &width_opt = boolbv_width(expr.type());
45+
if(!width_opt.has_value())
46+
return conversion_failed(expr);
47+
48+
const std::size_t width = *width_opt;
4549

4650
// special treatment for bit-fields and big-endian:
4751
// we need byte granularity

‎src/solvers/flattening/boolbv_case.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,12 @@ bvt boolbvt::convert_case(const exprt &expr)
1616

1717
const std::vector<exprt> &operands=expr.operands();
1818

19-
std::size_t width=boolbv_width(expr.type());
20-
21-
if(width==0)
19+
const auto &width_opt = boolbv_width(expr.type());
20+
if(!width_opt.has_value())
2221
return conversion_failed(expr);
2322

23+
const std::size_t width = *width_opt;
24+
2425
// make it free variables
2526
bvt bv = prop.new_variables(width);
2627

‎src/solvers/flattening/boolbv_complex.cpp

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,12 @@ Author: Daniel Kroening, [email protected]
1212

1313
bvt boolbvt::convert_complex(const complex_exprt &expr)
1414
{
15-
std::size_t width=boolbv_width(expr.type());
16-
17-
if(width==0)
15+
const auto &width_opt = boolbv_width(expr.type());
16+
if(!width_opt.has_value())
1817
return conversion_failed(expr);
1918

19+
const std::size_t width = *width_opt;
20+
2021
DATA_INVARIANT(
2122
expr.type().id() == ID_complex,
2223
"complex expression shall have complex type");
@@ -39,11 +40,12 @@ bvt boolbvt::convert_complex(const complex_exprt &expr)
3940

4041
bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
4142
{
42-
std::size_t width=boolbv_width(expr.type());
43-
44-
if(width==0)
43+
const auto &width_opt = boolbv_width(expr.type());
44+
if(!width_opt.has_value())
4545
return conversion_failed(expr);
4646

47+
const std::size_t width = *width_opt;
48+
4749
bvt bv = convert_bv(expr.op(), width * 2);
4850

4951
bv.resize(width); // chop
@@ -53,11 +55,12 @@ bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
5355

5456
bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)
5557
{
56-
std::size_t width=boolbv_width(expr.type());
57-
58-
if(width==0)
58+
const auto &width_opt = boolbv_width(expr.type());
59+
if(!width_opt.has_value())
5960
return conversion_failed(expr);
6061

62+
const std::size_t width = *width_opt;
63+
6164
bvt bv = convert_bv(expr.op(), width * 2);
6265

6366
bv.erase(bv.begin(), bv.begin()+width);

‎src/solvers/flattening/boolbv_concatenation.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,12 @@ Author: Daniel Kroening, [email protected]
1313

1414
bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
1515
{
16-
std::size_t width=boolbv_width(expr.type());
17-
18-
if(width==0)
16+
const auto &width_opt = boolbv_width(expr.type());
17+
if(!width_opt.has_value())
1918
return conversion_failed(expr);
2019

20+
const std::size_t width = *width_opt;
21+
2122
const exprt::operandst &operands=expr.operands();
2223

2324
DATA_INVARIANT(

‎src/solvers/flattening/boolbv_cond.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,12 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
1414
{
1515
const exprt::operandst &operands=expr.operands();
1616

17-
std::size_t width=boolbv_width(expr.type());
18-
19-
if(width==0)
17+
const auto &width_opt = boolbv_width(expr.type());
18+
if(!width_opt.has_value())
2019
return conversion_failed(expr);
2120

21+
const std::size_t width = *width_opt;
22+
2223
bvt bv;
2324

2425
DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");

‎src/solvers/flattening/boolbv_constant.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,12 @@ Author: Daniel Kroening, [email protected]
1212

1313
bvt boolbvt::convert_constant(const constant_exprt &expr)
1414
{
15-
std::size_t width=boolbv_width(expr.type());
16-
17-
if(width==0)
15+
const auto &width_opt = boolbv_width(expr.type());
16+
if(!width_opt.has_value())
1817
return conversion_failed(expr);
1918

19+
const std::size_t width = *width_opt;
20+
2021
bvt bv;
2122
bv.resize(width);
2223

‎src/solvers/flattening/boolbv_constraint_select_one.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,12 @@ bvt boolbvt::convert_constraint_select_one(const exprt &expr)
2626

2727
if(prop.has_set_to())
2828
{
29-
std::size_t width=boolbv_width(expr.type());
29+
const auto &width_opt = boolbv_width(expr.type());
30+
if(!width_opt.has_value())
31+
return conversion_failed(expr);
32+
33+
const std::size_t width = *width_opt;
34+
3035
bv=prop.new_variables(width);
3136

3237
bvt b;

0 commit comments

Comments
 (0)