Skip to content

Commit a5944a7

Browse files
author
Daniel Kroening
committed
numeric_cast_v(expr) now requires constant_expr
This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.
1 parent 02e508e commit a5944a7

29 files changed

+120
-73
lines changed

‎jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,8 @@ static const std::string get_thread_block_identifier(
8686
{
8787
PRECONDITION(f_code.arguments().size() == 1);
8888
const exprt &expr = f_code.arguments()[0];
89-
const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
89+
const mp_integer lbl_id =
90+
numeric_cast_v<mp_integer>(to_constant_expr(expr.op0()));
9091
return integer2string(lbl_id);
9192
}
9293

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 21 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,8 @@ exprt java_bytecode_convert_methodt::variable(
183183
java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
184184
{
185185
typet t=java_type_from_char(type_char);
186-
const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
186+
const std::size_t number_int =
187+
numeric_cast_v<std::size_t>(to_constant_expr(arg));
187188
variablest &var_list=variables[number_int];
188189

189190
// search variable in list for correct frame / address if necessary
@@ -1309,15 +1310,17 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13091310
else if(statement=="goto" || statement=="goto_w")
13101311
{
13111312
PRECONDITION(op.empty() && results.empty());
1312-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1313+
const mp_integer number =
1314+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13131315
code_gotot code_goto(label(integer2string(number)));
13141316
c=code_goto;
13151317
}
13161318
else if(statement=="jsr" || statement=="jsr_w")
13171319
{
13181320
// As 'goto', except we must also push the subroutine return address:
13191321
PRECONDITION(op.empty() && results.size() == 1);
1320-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1322+
const mp_integer number =
1323+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13211324
code_gotot code_goto(label(integer2string(number)));
13221325
c=code_goto;
13231326
results[0]=
@@ -1344,7 +1347,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13441347
else if(statement==patternt("?const"))
13451348
{
13461349
assert(results.size()==1);
1347-
results = convert_const(statement, arg0, results);
1350+
results = convert_const(statement, to_constant_expr(arg0), results);
13481351
}
13491352
else if(statement==patternt("?ipush"))
13501353
{
@@ -1357,7 +1360,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13571360
else if(statement==patternt("if_?cmp??"))
13581361
{
13591362
PRECONDITION(op.size() == 2 && results.empty());
1360-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1363+
const mp_integer number =
1364+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13611365
c = convert_if_cmp(
13621366
address_map, statement, op, number, i_it->source_location);
13631367
}
@@ -1374,19 +1378,22 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13741378

13751379
INVARIANT(!id.empty(), "unexpected bytecode-if");
13761380
PRECONDITION(op.size() == 1 && results.empty());
1377-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1381+
const mp_integer number =
1382+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13781383
c = convert_if(address_map, op, id, number, i_it->source_location);
13791384
}
13801385
else if(statement==patternt("ifnonnull"))
13811386
{
13821387
PRECONDITION(op.size() == 1 && results.empty());
1383-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1388+
const mp_integer number =
1389+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13841390
c = convert_ifnonull(address_map, op, number, i_it->source_location);
13851391
}
13861392
else if(statement==patternt("ifnull"))
13871393
{
13881394
PRECONDITION(op.size() == 1 && results.empty());
1389-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1395+
const mp_integer number =
1396+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13901397
c = convert_ifnull(address_map, op, number, i_it->source_location);
13911398
}
13921399
else if(statement=="iinc")
@@ -1581,7 +1588,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
15811588
{
15821589
// The first argument is the type, the second argument is the number of
15831590
// dimensions. The size of each dimension is on the stack.
1584-
const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
1591+
const std::size_t dimension =
1592+
numeric_cast_v<std::size_t>(to_constant_expr(arg1));
15851593

15861594
op=pop(dimension);
15871595
assert(results.size()==1);
@@ -1905,7 +1913,8 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
19051913
{
19061914
if(is_label)
19071915
{
1908-
const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
1916+
const mp_integer number =
1917+
numeric_cast_v<mp_integer>(to_constant_expr(*a_it));
19091918
// The switch case does not contain any code, it just branches via a GOTO
19101919
// to the jump target of the tableswitch/lookupswitch case at
19111920
// hand. Therefore we consider this code to belong to the source bytecode
@@ -2014,7 +2023,7 @@ void java_bytecode_convert_methodt::convert_dup2_x2(
20142023

20152024
exprt::operandst &java_bytecode_convert_methodt::convert_const(
20162025
const irep_idt &statement,
2017-
const exprt &arg0,
2026+
const constant_exprt &arg0,
20182027
exprt::operandst &results) const
20192028
{
20202029
const char type_char = statement[0];
@@ -2034,7 +2043,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
20342043
value.from_integer(number);
20352044
}
20362045
else
2037-
value.from_expr(to_constant_expr(arg0));
2046+
value.from_expr(arg0);
20382047

20392048
results[0] = value.to_expr();
20402049
}

‎jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -487,7 +487,7 @@ class java_bytecode_convert_methodt:public messaget
487487

488488
exprt::operandst &convert_const(
489489
const irep_idt &statement,
490-
const exprt &arg0,
490+
const constant_exprt &arg0,
491491
exprt::operandst &results) const;
492492

493493
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results);

‎jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
9999
/// \return the corresponding index set
100100
std::set<exprt> full_index_set(const array_string_exprt &s)
101101
{
102-
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
102+
const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
103103
std::set<exprt> ret;
104104
for(mp_integer i = 0; i < n; ++i)
105105
ret.insert(from_integer(i));

‎src/analyses/interval_domain.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,7 @@ void interval_domaint::assume_rec(
254254

255255
if(is_int(lhs.type()) && is_int(rhs.type()))
256256
{
257-
mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
257+
mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(rhs));
258258
if(id==ID_lt)
259259
--tmp;
260260
integer_intervalt &ii=int_map[lhs_identifier];
@@ -279,7 +279,7 @@ void interval_domaint::assume_rec(
279279

280280
if(is_int(lhs.type()) && is_int(rhs.type()))
281281
{
282-
mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
282+
mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(lhs));
283283
if(id==ID_lt)
284284
++tmp;
285285
integer_intervalt &ii=int_map[rhs_identifier];

‎src/analyses/invariant_set.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -850,7 +850,8 @@ exprt invariant_sett::get_constant(const exprt &expr) const
850850

851851
if(e.is_constant())
852852
{
853-
const mp_integer value = numeric_cast_v<mp_integer>(e);
853+
const mp_integer value =
854+
numeric_cast_v<mp_integer>(to_constant_expr(e));
854855

855856
if(expr.type().id()==ID_pointer)
856857
{

‎src/ansi-c/c_nondet_symbol_factory.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,9 @@ void symbol_factoryt::gen_nondet_array_init(
155155
const recursion_sett &recursion_set)
156156
{
157157
auto const &array_type = to_array_type(expr.type());
158-
auto const array_size = numeric_cast_v<size_t>(array_type.size());
158+
const auto &size = array_type.size();
159+
PRECONDITION(size.id() == ID_constant);
160+
auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
159161
DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
160162
for(size_t index = 0; index < array_size; ++index)
161163
{

‎src/ansi-c/expr2c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2172,7 +2172,7 @@ std::string expr2ct::convert_array(
21722172
if(it==--src.operands().end())
21732173
break;
21742174

2175-
const unsigned int ch = numeric_cast_v<unsigned>(*it);
2175+
const unsigned int ch = numeric_cast_v<unsigned>(to_constant_expr(*it));
21762176

21772177
if(last_was_hex)
21782178
{

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,8 @@ void cpp_typecheckt::zero_initializer(
231231
if(size_expr.id()==ID_infinity)
232232
return; // don't initialize
233233

234-
const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
234+
const mp_integer size =
235+
numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
235236
CHECK_RETURN(size>=0);
236237

237238
exprt::operandst empty_operands;

‎src/goto-instrument/accelerate/polynomial.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ void polynomialt::from_expr(const exprt &expr)
139139
else if(expr.id()==ID_constant)
140140
{
141141
monomialt monomial;
142-
monomial.coeff = numeric_cast_v<int>(expr);
142+
monomial.coeff = numeric_cast_v<int>(to_constant_expr(expr));
143143

144144
monomials.push_back(monomial);
145145
}

‎src/goto-programs/interpreter.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -498,7 +498,7 @@ exprt interpretert::get_value(
498498
}
499499
else
500500
{
501-
count = numeric_cast_v<mp_integer>(size_expr);
501+
count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
502502
}
503503

504504
// Retrieve the value for each member in the array
@@ -567,7 +567,7 @@ exprt interpretert::get_value(
567567
}
568568
else
569569
{
570-
count = numeric_cast_v<mp_integer>(size_expr);
570+
count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
571571
}
572572

573573
// Retrieve the value for each member in the array
@@ -1026,7 +1026,7 @@ mp_integer interpretert::get_size(const typet &type)
10261026
{
10271027
// Go via the binary representation to reproduce any
10281028
// overflow behaviour.
1029-
exprt size_const=from_integer(i[0], size_expr.type());
1029+
const constant_exprt size_const = from_integer(i[0], size_expr.type());
10301030
const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
10311031
return subtype_size*size_mp;
10321032
}

‎src/goto-programs/remove_vector.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ static void remove_vector(exprt &expr)
9292
array_typet array_type=to_array_type(expr.type());
9393

9494
const mp_integer dimension =
95-
numeric_cast_v<mp_integer>(array_type.size());
95+
numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
9696

9797
const typet subtype=array_type.subtype();
9898
// do component-wise:
@@ -119,7 +119,7 @@ static void remove_vector(exprt &expr)
119119
array_typet array_type=to_array_type(expr.type());
120120

121121
const mp_integer dimension =
122-
numeric_cast_v<mp_integer>(array_type.size());
122+
numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
123123

124124
const typet subtype=array_type.subtype();
125125
// do component-wise:
@@ -150,7 +150,8 @@ static void remove_vector(exprt &expr)
150150
// (vector-type) x ==> { x, x, ..., x }
151151
remove_vector(expr.type());
152152
array_typet array_type = to_array_type(expr.type());
153-
const auto dimension = numeric_cast_v<std::size_t>(array_type.size());
153+
const auto dimension =
154+
numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
154155
exprt casted_op =
155156
typecast_exprt::conditional_cast(op, array_type.subtype());
156157
expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);

‎src/solvers/flattening/boolbv.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,9 +72,13 @@ bool boolbvt::literal(
7272
std::size_t element_width=boolbv_width(index_expr.type());
7373
CHECK_RETURN(element_width != 0);
7474

75-
mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
75+
const auto &index = index_expr.index();
76+
PRECONDITION(index.id() == ID_constant);
77+
mp_integer index_int =
78+
numeric_cast_v<mp_integer>(to_constant_expr(index));
7679

77-
std::size_t offset = numeric_cast_v<std::size_t>(index * element_width);
80+
std::size_t offset =
81+
numeric_cast_v<std::size_t>(index_int * element_width);
7882

7983
return literal(index_expr.array(), bit+offset, dest);
8084
}

‎src/solvers/flattening/boolbv_extractbit.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,13 @@ Author: Daniel Kroening, [email protected]
1919
literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
2020
{
2121
const bvt &src_bv = convert_bv(expr.src());
22+
const auto &index = expr.index();
2223

2324
// constant?
24-
if(expr.index().is_constant())
25+
if(index.is_constant())
2526
{
26-
mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
27+
mp_integer index_as_integer =
28+
numeric_cast_v<mp_integer>(to_constant_expr(index));
2729

2830
if(index_as_integer < 0 || index_as_integer >= src_bv.size())
2931
return prop.new_variable(); // out of range!
@@ -42,7 +44,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
4244
else
4345
{
4446
std::size_t src_bv_width = boolbv_width(expr.src().type());
45-
std::size_t index_bv_width = boolbv_width(expr.index().type());
47+
std::size_t index_bv_width = boolbv_width(index.type());
4648

4749
if(src_bv_width == 0 || index_bv_width == 0)
4850
return SUB::convert_rest(expr);
@@ -52,7 +54,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
5254
unsignedbv_typet index_type(index_width);
5355

5456
equal_exprt equality(
55-
typecast_exprt::conditional_cast(expr.index(), index_type), exprt());
57+
typecast_exprt::conditional_cast(index, index_type), exprt());
5658

5759
if(prop.has_set_to())
5860
{

‎src/solvers/flattening/boolbv_index.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
6161
}
6262

6363
// Must have a finite size
64-
mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
64+
mp_integer array_size =
65+
numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
66+
6567
{
6668
// see if the index address is constant
6769
// many of these are compacted by simplify_expr

‎src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -87,8 +87,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
8787
continue;
8888
if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
8989
{
90-
exprt over_expr=x.op1();
90+
const constant_exprt &over_expr = to_constant_expr(x.op1());
91+
9192
mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
93+
9294
/**
9395
* Due to the ''simplify'',
9496
* the ''over_i'' value we obtain here is not the exact
@@ -115,7 +117,7 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
115117
continue;
116118
if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
117119
{
118-
exprt over_expr=y.op1();
120+
const constant_exprt &over_expr = to_constant_expr(y.op1());
119121
mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
120122
over_i-=1;
121123
res=from_integer(over_i, y.op1().type());
@@ -149,8 +151,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
149151
if(min_i.is_false() || max_i.is_false())
150152
return nullopt;
151153

152-
mp_integer lb = numeric_cast_v<mp_integer>(min_i);
153-
mp_integer ub = numeric_cast_v<mp_integer>(max_i);
154+
mp_integer lb = numeric_cast_v<mp_integer>(to_constant_expr(min_i));
155+
mp_integer ub = numeric_cast_v<mp_integer>(to_constant_expr(max_i));
154156

155157
if(lb>ub)
156158
return nullopt;

‎src/solvers/flattening/boolbv_shift.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,11 +47,12 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
4747
else
4848
UNREACHABLE;
4949

50-
// we allow a constant as shift distance
50+
// we optimise for the special case where the shift distance
51+
// is a constant
5152

5253
if(expr.op1().is_constant())
5354
{
54-
mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
55+
mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
5556

5657
std::size_t distance;
5758

‎src/solvers/flattening/boolbv_update.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -74,13 +74,18 @@ void boolbvt::convert_update_rec(
7474
bvt index_bv=convert_bv(designator.op0());
7575

7676
const array_typet &array_type=to_array_type(type);
77-
7877
const typet &subtype = array_type.subtype();
78+
const exprt &size_expr = array_type.size();
7979

8080
std::size_t element_size=boolbv_width(subtype);
8181

82+
DATA_INVARIANT(
83+
size_expr.id() == ID_constant,
84+
"array in update expression should be constant-sized");
85+
8286
// iterate over array
83-
const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
87+
const std::size_t size =
88+
numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
8489

8590
bvt tmp_bv=bv;
8691

0 commit comments

Comments
 (0)