Fix narrowing conversions seen by test-gen

jbmc/src/java_bytecode/java_types.h

@@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 #include <set>
 
-#include <util/type.h>
-#include <util/std_types.h>
 #include <util/c_types.h>
+#include <util/narrow.h>
 #include <util/optional.h>
 #include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/type.h>
 
 class java_annotationt : public irept
 {
@@ -750,7 +751,7 @@ inline const optionalt<size_t> java_generics_get_index_for_subtype(
     return {};
   }
 
-  return std::distance(gen_types.cbegin(), iter);
+  return narrow_cast<size_t>(std::distance(gen_types.cbegin(), iter));
 }
 
 void get_dependencies_from_generic_parameters(

src/goto-symex/symex_target_equation.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/invariant.h>
 #include <util/merge_irep.h>
+#include <util/narrow.h>
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_trace.h>
@@ -351,18 +352,18 @@ class symex_target_equationt:public symex_targett
 
   std::size_t count_assertions() const
   {
-    return std::count_if(
+    return narrow_cast<std::size_t>(std::count_if(
       SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
         return step.is_assert();
-      });
+      }));
   }
 
   std::size_t count_ignored_SSA_steps() const
   {
-    return std::count_if(
+    return narrow_cast<std::size_t>(std::count_if(
       SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
         return step.ignore;
-      });
+      }));
   }
 
   typedef std::list<SSA_stept> SSA_stepst;

src/solvers/prop/literal.h

@@ -10,8 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_PROP_LITERAL_H
 #define CPROVER_SOLVERS_PROP_LITERAL_H
 
-#include <vector>
 #include <iosfwd>
+#include <util/narrow.h>
+#include <vector>
 
 // a pair of a variable number and a sign, encoded as follows:
 //
@@ -115,7 +116,7 @@ class literalt
   //
   int dimacs() const
   {
-    int result=var_no();
+    int result = narrow_cast<int>(var_no());
 
     if(sign())
       result=-result;
@@ -128,7 +129,7 @@ class literalt
     bool sign=d<0;
     if(sign)
       d=-d;
-    set(d, sign);
+    set(narrow_cast<unsigned>(d), sign);
   }
 
   void clear()

src/util/expr_iterator.h

@@ -188,8 +188,7 @@ class depth_iterator_baset
       auto &operands = expr->operands();
       // Get iterators into the operands of the new expr corresponding to the
       // ones into the operands of the old expr
-      const auto i=operands.size()-(state.end-state.it);
-      const auto it=operands.begin()+i;
+      const auto it = operands.end() - (state.end - state.it);
       state.expr = *expr;
       state.it=it;
       state.end=operands.end();

src/util/narrow.h

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Narrowing conversion functions
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_NARROW_H
+#define CPROVER_UTIL_NARROW_H
+
+#include <type_traits>
+
+#include "invariant.h"
+
+/// Alias for static_cast intended to be used for numeric casting
+/// Rationale: Easier to grep than static_cast
+template <typename output_type, typename input_type>
+output_type narrow_cast(input_type value)
+{
+  static_assert(
+    std::is_arithmetic<input_type>::value &&
+      std::is_arithmetic<output_type>::value,
+    "narrow_cast is intended only for numeric conversions");
+  return static_cast<output_type>(value);
+}
+
+/// Run-time checked narrowing cast. Raises an invariant if the input
+/// value cannot be converted to the output value without data loss
+///
+/// Template accepts a single argument - the return type. Input type
+/// is deduced from the function argument and shouldn't be specified
+template <typename output_type, typename input_type>
+output_type narrow(input_type input)
+{
+  const auto output = static_cast<output_type>(input);
+  INVARIANT(static_cast<input_type>(output) == input, "Data loss detected");
+  return output;
+}
+
+#endif // CPROVER_UTIL_NARROW_H

src/util/std_expr.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr_cast.h"
 #include "invariant.h"
 #include "std_types.h"
+#include <util/narrow.h>
 
 /// An expression without operands
 class nullary_exprt : public exprt
@@ -544,7 +545,7 @@ class bswap_exprt: public unary_exprt
 
   void set_bits_per_byte(std::size_t bits_per_byte)
   {
-    set(ID_bits_per_byte, bits_per_byte);
+    set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
   }
 };
 
@@ -1756,7 +1757,7 @@ class union_exprt:public unary_exprt
 
   void set_component_number(std::size_t component_number)
   {
-    set(ID_component_number, component_number);
+    set(ID_component_number, narrow_cast<long long>(component_number));
   }
 };
 

src/util/std_types.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "invariant.h"
 #include "mp_arith.h"
 #include "validate.h"
+#include <util/narrow.h>
 
 #include <unordered_map>
 
@@ -1122,7 +1123,7 @@ class bitvector_typet : public typet
 
   void set_width(std::size_t width)
   {
-    set(ID_width, width);
+    set(ID_width, narrow_cast<long long>(width));
   }
 
   static void check(
@@ -1351,7 +1352,7 @@ class fixedbv_typet:public bitvector_typet
 
   void set_integer_bits(std::size_t b)
   {
-    set(ID_integer_bits, b);
+    set(ID_integer_bits, narrow_cast<long long>(b));
   }
 };
 
@@ -1413,7 +1414,7 @@ class floatbv_typet:public bitvector_typet
 
   void set_f(std::size_t b)
   {
-    set(ID_f, b);
+    set(ID_f, narrow_cast<long long>(b));
   }
 };