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.

Author: kroening

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -86,7 +86,8 @@ static const std::string get_thread_block_identifier(
 {
   PRECONDITION(f_code.arguments().size() == 1);
   const exprt &expr = f_code.arguments()[0];
-  const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
+  const mp_integer lbl_id =
+    numeric_cast_v<mp_integer>(to_constant_expr(expr.op0()));
   return integer2string(lbl_id);
 }
 

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -183,7 +183,8 @@ exprt java_bytecode_convert_methodt::variable(
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
   typet t=java_type_from_char(type_char);
-  const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
+  const std::size_t number_int =
+    numeric_cast_v<std::size_t>(to_constant_expr(arg));
   variablest &var_list=variables[number_int];
 
   // search variable in list for correct frame / address if necessary
@@ -1309,15 +1310,17 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       PRECONDITION(op.empty() && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
     else if(statement=="jsr" || statement=="jsr_w")
     {
       // As 'goto', except we must also push the subroutine return address:
       PRECONDITION(op.empty() && results.size() == 1);
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
@@ -1344,7 +1347,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?const"))
     {
       assert(results.size()==1);
-      results = convert_const(statement, arg0, results);
+      results = convert_const(statement, to_constant_expr(arg0), results);
     }
     else if(statement==patternt("?ipush"))
     {
@@ -1357,7 +1360,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("if_?cmp??"))
     {
       PRECONDITION(op.size() == 2 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_if_cmp(
         address_map, statement, op, number, i_it->source_location);
     }
@@ -1374,19 +1378,22 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
       INVARIANT(!id.empty(), "unexpected bytecode-if");
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_if(address_map, op, id, number, i_it->source_location);
     }
     else if(statement==patternt("ifnonnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_ifnonull(address_map, op, number, i_it->source_location);
     }
     else if(statement==patternt("ifnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_ifnull(address_map, op, number, i_it->source_location);
     }
     else if(statement=="iinc")
@@ -1581,7 +1588,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       // The first argument is the type, the second argument is the number of
       // dimensions.  The size of each dimension is on the stack.
-      const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
+      const std::size_t dimension =
+        numeric_cast_v<std::size_t>(to_constant_expr(arg1));
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1905,7 +1913,8 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   {
     if(is_label)
     {
-      const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(*a_it));
       // The switch case does not contain any code, it just branches via a GOTO
       // to the jump target of the tableswitch/lookupswitch case at
       // hand. Therefore we consider this code to belong to the source bytecode
@@ -2014,7 +2023,7 @@ void java_bytecode_convert_methodt::convert_dup2_x2(
 
 exprt::operandst &java_bytecode_convert_methodt::convert_const(
   const irep_idt &statement,
-  const exprt &arg0,
+  const constant_exprt &arg0,
   exprt::operandst &results) const
 {
   const char type_char = statement[0];
@@ -2034,7 +2043,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
       value.from_integer(number);
     }
     else
-      value.from_expr(to_constant_expr(arg0));
+      value.from_expr(arg0);
 
     results[0] = value.to_expr();
   }

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -487,7 +487,7 @@ class java_bytecode_convert_methodt:public messaget
 
   exprt::operandst &convert_const(
     const irep_idt &statement,
-    const exprt &arg0,
+    const constant_exprt &arg0,
     exprt::operandst &results) const;
 
   void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results);

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

@@ -99,7 +99,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
 /// \return the corresponding index set
 std::set<exprt> full_index_set(const array_string_exprt &s)
 {
-  const mp_integer n = numeric_cast_v<mp_integer>(s.length());
+  const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
   std::set<exprt> ret;
   for(mp_integer i = 0; i < n; ++i)
     ret.insert(from_integer(i));

src/analyses/interval_domain.cpp

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

src/analyses/invariant_set.cpp

@@ -850,7 +850,8 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
         if(e.is_constant())
         {
-          const mp_integer value = numeric_cast_v<mp_integer>(e);
+          const mp_integer value =
+            numeric_cast_v<mp_integer>(to_constant_expr(e));
 
           if(expr.type().id()==ID_pointer)
           {

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -155,7 +155,9 @@ void symbol_factoryt::gen_nondet_array_init(
   const recursion_sett &recursion_set)
 {
   auto const &array_type = to_array_type(expr.type());
-  auto const array_size = numeric_cast_v<size_t>(array_type.size());
+  const auto &size = array_type.size();
+  PRECONDITION(size.id() == ID_constant);
+  auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
   DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
   for(size_t index = 0; index < array_size; ++index)
   {

src/ansi-c/expr2c.cpp

@@ -2172,7 +2172,7 @@ std::string expr2ct::convert_array(
       if(it==--src.operands().end())
         break;
 
-      const unsigned int ch = numeric_cast_v<unsigned>(*it);
+      const unsigned int ch = numeric_cast_v<unsigned>(to_constant_expr(*it));
 
       if(last_was_hex)
       {

src/cpp/cpp_typecheck_initializer.cpp

@@ -231,7 +231,8 @@ void cpp_typecheckt::zero_initializer(
     if(size_expr.id()==ID_infinity)
       return; // don't initialize
 
-    const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
+    const mp_integer size =
+      numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;

src/goto-instrument/accelerate/polynomial.cpp

@@ -139,7 +139,7 @@ void polynomialt::from_expr(const exprt &expr)
   else if(expr.id()==ID_constant)
   {
     monomialt monomial;
-    monomial.coeff = numeric_cast_v<int>(expr);
+    monomial.coeff = numeric_cast_v<int>(to_constant_expr(expr));
 
     monomials.push_back(monomial);
   }