Decouple type conversion checks from arithmetic overflow

Type conversion has implementation-defined semantics, whereas integer
overflow is undefined behavior in C. Thus one my want to check only the
latter, in particular in SV-COMP.

Fixes #307

Author: tautschnig

src/analyses/goto_check.cpp

@@ -41,6 +41,7 @@ class goto_checkt
     enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check");
     enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check");
     enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check");
+    enable_conversion_check=_options.get_bool_option("conversion-check");
     enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check");
     enable_float_overflow_check=_options.get_bool_option("float-overflow-check");
     enable_simplify=_options.get_bool_option("simplify");
@@ -74,6 +75,7 @@ class goto_checkt
   void pointer_overflow_check(const exprt &expr, const guardt &guard);
   void pointer_validity_check(const dereference_exprt &expr, const guardt &guard);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
+  void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
   void nan_check(const exprt &expr, const guardt &guard);
 
@@ -105,6 +107,7 @@ class goto_checkt
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
   bool enable_pointer_overflow_check;
+  bool enable_conversion_check;
   bool enable_undefined_shift_check;
   bool enable_float_overflow_check;
   bool enable_simplify;
@@ -305,7 +308,7 @@ void goto_checkt::mod_by_zero_check(
 
 /*******************************************************************\
 
-Function: goto_checkt::integer_overflow_check
+Function: goto_checkt::conversion_check
 
   Inputs:
 
@@ -315,25 +318,20 @@ Function: goto_checkt::integer_overflow_check
 
 \*******************************************************************/
 
-void goto_checkt::integer_overflow_check(
+void goto_checkt::conversion_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_signed_overflow_check &&
-     !enable_unsigned_overflow_check)
+  if(!enable_conversion_check)
     return;
 
   // First, check type.
   const typet &type=ns.follow(expr.type());
 
-  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
-    return;
-
-  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
+  if(type.id()!=ID_signedbv &&
+     type.id()!=ID_unsignedbv)
     return;
 
-  // add overflow subgoal
-
   if(expr.id()==ID_typecast)
   {
     // conversion to signed int may overflow
@@ -493,10 +491,41 @@ void goto_checkt::integer_overflow_check(
           guard);
       }
     }
+  }
+}
 
+/*******************************************************************\
+
+Function: goto_checkt::integer_overflow_check
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void goto_checkt::integer_overflow_check(
+  const exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_signed_overflow_check &&
+     !enable_unsigned_overflow_check)
     return;
-  }
-  else if(expr.id()==ID_div)
+
+  // First, check type.
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
+    return;
+
+  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
+    return;
+
+  // add overflow subgoal
+
+  if(expr.id()==ID_div)
   {
     assert(expr.operands().size()==2);
 
@@ -1432,8 +1461,7 @@ void goto_checkt::check_rec(
   }
   else if(expr.id()==ID_plus || expr.id()==ID_minus ||
           expr.id()==ID_mult ||
-          expr.id()==ID_unary_minus ||
-          expr.id()==ID_typecast)
+          expr.id()==ID_unary_minus)
   {
     if(expr.type().id()==ID_signedbv ||
        expr.type().id()==ID_unsignedbv)
@@ -1454,6 +1482,8 @@ void goto_checkt::check_rec(
       pointer_overflow_check(expr, guard);
     }
   }
+  else if(expr.id()==ID_typecast)
+    conversion_check(expr, guard);
   else if(expr.id()==ID_le || expr.id()==ID_lt ||
           expr.id()==ID_ge || expr.id()==ID_gt)
     pointer_rel_check(expr, guard);

src/analyses/goto_check.h

@@ -32,7 +32,7 @@ void goto_check(
 #define GOTO_CHECK_OPTIONS \
   "(bounds-check)(pointer-check)(memory-leak-check)" \
   "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
-  "(pointer-overflow-check)(undefined-shift-check)" \
+  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
   "(float-overflow-check)(nan-check)"
 
 #define GOTO_CHECK_HELP \
@@ -43,6 +43,7 @@ void goto_check(
   " --signed-overflow-check      enable signed arithmetic over- and underflow checks\n" \
   " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n" \
   " --pointer-overflow-check     enable pointer arithmetic over- and underflow checks\n" \
+  " --conversion-check           check whether values can be represented after type cast\n" \
   " --undefined-shift-check      check shift greater than bit-width\n" \
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
@@ -55,6 +56,7 @@ void goto_check(
   options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \
   options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \
   options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \
+  options.set_option("conversion-check", cmdline.isset("conversion-check")); \
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \
   options.set_option("nan-check", cmdline.isset("nan-check"))