Skip to content

Commit 77dda3e

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 e2b42b8 commit 77dda3e

30 files changed

+123
-74
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
@@ -208,7 +208,8 @@ exprt java_bytecode_convert_methodt::variable(
208208
java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
209209
{
210210
typet t=java_type_from_char(type_char);
211-
const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
211+
const std::size_t number_int =
212+
numeric_cast_v<std::size_t>(to_constant_expr(arg));
212213
variablest &var_list=variables[number_int];
213214

214215
// search variable in list for correct frame / address if necessary
@@ -1334,15 +1335,17 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13341335
else if(statement=="goto" || statement=="goto_w")
13351336
{
13361337
PRECONDITION(op.empty() && results.empty());
1337-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1338+
const mp_integer number =
1339+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13381340
code_gotot code_goto(label(integer2string(number)));
13391341
c=code_goto;
13401342
}
13411343
else if(statement=="jsr" || statement=="jsr_w")
13421344
{
13431345
// As 'goto', except we must also push the subroutine return address:
13441346
PRECONDITION(op.empty() && results.size() == 1);
1345-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1347+
const mp_integer number =
1348+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
13461349
code_gotot code_goto(label(integer2string(number)));
13471350
c=code_goto;
13481351
results[0]=
@@ -1369,7 +1372,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13691372
else if(statement==patternt("?const"))
13701373
{
13711374
assert(results.size()==1);
1372-
results = convert_const(statement, arg0, results);
1375+
results = convert_const(statement, to_constant_expr(arg0), results);
13731376
}
13741377
else if(statement==patternt("?ipush"))
13751378
{
@@ -1382,7 +1385,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13821385
else if(statement==patternt("if_?cmp??"))
13831386
{
13841387
PRECONDITION(op.size() == 2 && results.empty());
1385-
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));
13861390
c = convert_if_cmp(
13871391
address_map, statement, op, number, i_it->source_location);
13881392
}
@@ -1399,19 +1403,22 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
13991403

14001404
INVARIANT(!id.empty(), "unexpected bytecode-if");
14011405
PRECONDITION(op.size() == 1 && results.empty());
1402-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1406+
const mp_integer number =
1407+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
14031408
c = convert_if(address_map, op, id, number, i_it->source_location);
14041409
}
14051410
else if(statement==patternt("ifnonnull"))
14061411
{
14071412
PRECONDITION(op.size() == 1 && results.empty());
1408-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1413+
const mp_integer number =
1414+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
14091415
c = convert_ifnonull(address_map, op, number, i_it->source_location);
14101416
}
14111417
else if(statement==patternt("ifnull"))
14121418
{
14131419
PRECONDITION(op.size() == 1 && results.empty());
1414-
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1420+
const mp_integer number =
1421+
numeric_cast_v<mp_integer>(to_constant_expr(arg0));
14151422
c = convert_ifnull(address_map, op, number, i_it->source_location);
14161423
}
14171424
else if(statement=="iinc")
@@ -1606,7 +1613,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
16061613
{
16071614
// The first argument is the type, the second argument is the number of
16081615
// dimensions. The size of each dimension is on the stack.
1609-
const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
1616+
const std::size_t dimension =
1617+
numeric_cast_v<std::size_t>(to_constant_expr(arg1));
16101618

16111619
op=pop(dimension);
16121620
assert(results.size()==1);
@@ -1930,7 +1938,8 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
19301938
{
19311939
if(is_label)
19321940
{
1933-
const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
1941+
const mp_integer number =
1942+
numeric_cast_v<mp_integer>(to_constant_expr(*a_it));
19341943
// The switch case does not contain any code, it just branches via a GOTO
19351944
// to the jump target of the tableswitch/lookupswitch case at
19361945
// hand. Therefore we consider this code to belong to the source bytecode
@@ -2039,7 +2048,7 @@ void java_bytecode_convert_methodt::convert_dup2_x2(
20392048

20402049
exprt::operandst &java_bytecode_convert_methodt::convert_const(
20412050
const irep_idt &statement,
2042-
const exprt &arg0,
2051+
const constant_exprt &arg0,
20432052
exprt::operandst &results) const
20442053
{
20452054
const char type_char = statement[0];
@@ -2059,7 +2068,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
20592068
value.from_integer(number);
20602069
}
20612070
else
2062-
value.from_expr(to_constant_expr(arg0));
2071+
value.from_expr(arg0);
20632072

20642073
results[0] = value.to_expr();
20652074
}

‎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
@@ -98,7 +98,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
9898
/// \return the corresponding index set
9999
std::set<exprt> full_index_set(const array_string_exprt &s)
100100
{
101-
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
101+
const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
102102
std::set<exprt> ret;
103103
for(mp_integer i = 0; i < n; ++i)
104104
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
@@ -858,7 +858,8 @@ exprt invariant_sett::get_constant(const exprt &expr) const
858858

859859
if(e.is_constant())
860860
{
861-
const mp_integer value = numeric_cast_v<mp_integer>(e);
861+
const mp_integer value =
862+
numeric_cast_v<mp_integer>(to_constant_expr(e));
862863

863864
if(expr.type().id()==ID_pointer)
864865
{

‎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
@@ -2170,7 +2170,7 @@ std::string expr2ct::convert_array(
21702170
if(it==--src.operands().end())
21712171
break;
21722172

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

21752175
if(last_was_hex)
21762176
{

‎src/cpp/cpp_typecheck_initializer.cpp

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

237-
const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
237+
const mp_integer size =
238+
numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
238239
CHECK_RETURN(size>=0);
239240

240241
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+
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
@@ -62,7 +62,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
6262
}
6363

6464
// Must have a finite size
65-
mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
65+
mp_integer array_size =
66+
numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
67+
6668
{
6769
// see if the index address is constant
6870
// 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_replication.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,14 @@ bvt boolbvt::convert_replication(const replication_exprt &expr)
1717
if(width==0)
1818
return conversion_failed(expr);
1919

20-
mp_integer times = numeric_cast_v<mp_integer>(expr.times());
20+
const auto &times = expr.times();
21+
22+
mp_integer times_int = numeric_cast_v<mp_integer>(times);
2123

2224
bvt bv;
2325
bv.resize(width);
2426

25-
const std::size_t u_times = numeric_cast_v<std::size_t>(times);
27+
const std::size_t u_times = numeric_cast_v<std::size_t>(times_int);
2628
const bvt &op = convert_bv(expr.op());
2729

2830
INVARIANT(

‎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

0 commit comments

Comments
 (0)