numeric_cast_v(expr) now requires constant_expr

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);
   }

src/goto-programs/interpreter.cpp

@@ -498,7 +498,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      count = numeric_cast_v<mp_integer>(size_expr);
+      count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     }
 
     // Retrieve the value for each member in the array
@@ -567,7 +567,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      count = numeric_cast_v<mp_integer>(size_expr);
+      count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     }
 
     // Retrieve the value for each member in the array
@@ -1026,7 +1026,7 @@ mp_integer interpretert::get_size(const typet &type)
     {
       // Go via the binary representation to reproduce any
       // overflow behaviour.
-      exprt size_const=from_integer(i[0], size_expr.type());
+      const constant_exprt size_const = from_integer(i[0], size_expr.type());
       const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
       return subtype_size*size_mp;
     }

src/goto-programs/remove_vector.cpp

@@ -92,7 +92,7 @@ static void remove_vector(exprt &expr)
       array_typet array_type=to_array_type(expr.type());
 
       const mp_integer dimension =
-        numeric_cast_v<mp_integer>(array_type.size());
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
       const typet subtype=array_type.subtype();
       // do component-wise:
@@ -119,7 +119,7 @@ static void remove_vector(exprt &expr)
       array_typet array_type=to_array_type(expr.type());
 
       const mp_integer dimension =
-        numeric_cast_v<mp_integer>(array_type.size());
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
       const typet subtype=array_type.subtype();
       // do component-wise:
@@ -150,7 +150,8 @@ static void remove_vector(exprt &expr)
         // (vector-type) x ==> { x, x, ..., x }
         remove_vector(expr.type());
         array_typet array_type = to_array_type(expr.type());
-        const auto dimension = numeric_cast_v<std::size_t>(array_type.size());
+        const auto dimension =
+          numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
         exprt casted_op =
           typecast_exprt::conditional_cast(op, array_type.subtype());
         expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);

src/solvers/flattening/boolbv.cpp

@@ -72,9 +72,13 @@ bool boolbvt::literal(
       std::size_t element_width=boolbv_width(index_expr.type());
       CHECK_RETURN(element_width != 0);
 
-      mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
+      const auto &index = index_expr.index();
+      PRECONDITION(index.id() == ID_constant);
+      mp_integer index_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(index));
 
-      std::size_t offset = numeric_cast_v<std::size_t>(index * element_width);
+      std::size_t offset =
+        numeric_cast_v<std::size_t>(index_int * element_width);
 
       return literal(index_expr.array(), bit+offset, dest);
     }

src/solvers/flattening/boolbv_extractbit.cpp

@@ -19,11 +19,13 @@ Author: Daniel Kroening, [email protected]
 literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
 {
   const bvt &src_bv = convert_bv(expr.src());
+  const auto &index = expr.index();
 
   // constant?
-  if(expr.index().is_constant())
+  if(index.is_constant())
   {
-    mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
+    mp_integer index_as_integer =
+      numeric_cast_v<mp_integer>(to_constant_expr(index));
 
     if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
@@ -42,7 +44,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
   else
   {
     std::size_t src_bv_width = boolbv_width(expr.src().type());
-    std::size_t index_bv_width = boolbv_width(expr.index().type());
+    std::size_t index_bv_width = boolbv_width(index.type());
 
     if(src_bv_width == 0 || index_bv_width == 0)
       return SUB::convert_rest(expr);
@@ -52,7 +54,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     unsignedbv_typet index_type(index_width);
 
     equal_exprt equality(
-      typecast_exprt::conditional_cast(expr.index(), index_type), exprt());
+      typecast_exprt::conditional_cast(index, index_type), exprt());
 
     if(prop.has_set_to())
     {

src/solvers/flattening/boolbv_index.cpp

@@ -61,7 +61,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     }
 
     // Must have a finite size
-    mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
+    mp_integer array_size =
+      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+
     {
       // see if the index address is constant
       // many of these are compacted by simplify_expr

src/solvers/flattening/boolbv_quantifier.cpp

@@ -87,8 +87,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
         continue;
       if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
       {
-        exprt over_expr=x.op1();
+        const constant_exprt &over_expr = to_constant_expr(x.op1());
+
         mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
+
         /**
          * Due to the ''simplify'',
          * 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)
         continue;
       if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
       {
-        exprt over_expr=y.op1();
+        const constant_exprt &over_expr = to_constant_expr(y.op1());
         mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
         over_i-=1;
         res=from_integer(over_i, y.op1().type());
@@ -149,8 +151,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
   if(min_i.is_false() || max_i.is_false())
     return nullopt;
 
-  mp_integer lb = numeric_cast_v<mp_integer>(min_i);
-  mp_integer ub = numeric_cast_v<mp_integer>(max_i);
+  mp_integer lb = numeric_cast_v<mp_integer>(to_constant_expr(min_i));
+  mp_integer ub = numeric_cast_v<mp_integer>(to_constant_expr(max_i));
 
   if(lb>ub)
     return nullopt;

src/solvers/flattening/boolbv_shift.cpp

@@ -47,11 +47,12 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   else
     UNREACHABLE;
 
-  // we allow a constant as shift distance
+  // we optimise for the special case where the shift distance
+  // is a constant
 
   if(expr.op1().is_constant())
   {
-    mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
+    mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
 
     std::size_t distance;
 

src/solvers/flattening/boolbv_update.cpp

@@ -74,13 +74,18 @@ void boolbvt::convert_update_rec(
     bvt index_bv=convert_bv(designator.op0());
 
     const array_typet &array_type=to_array_type(type);
-
     const typet &subtype = array_type.subtype();
+    const exprt &size_expr = array_type.size();
 
     std::size_t element_size=boolbv_width(subtype);
 
+    DATA_INVARIANT(
+      size_expr.id() == ID_constant,
+      "array in update expression should be constant-sized");
+
     // iterate over array
-    const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
+    const std::size_t size =
+      numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
     bvt tmp_bv=bv;