Cleanup of *-check options handling, refined options for SV-COMP

src/aa-symex/symex_parseoptions.cpp

@@ -28,8 +28,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -112,47 +110,8 @@ void symex_parseoptionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.getval("unwindset"));
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -811,13 +770,7 @@ void symex_parseoptionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"

src/aa-symex/symex_parseoptions.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 #include "path_search.h"
 
 class goto_functionst;
@@ -23,8 +25,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(unwind):" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \

src/analyses/goto_check.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/pointer_predicates.h>
 #include <util/cprover_prefix.h>
+#include <util/options.h>
 
 #include "local_bitvector_analysis.h"
 #include "goto_check.h"
@@ -39,6 +40,8 @@ class goto_checkt
     enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
     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");
@@ -72,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);
 
@@ -102,6 +106,8 @@ class goto_checkt
   bool enable_div_by_zero_check;
   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;
@@ -302,7 +308,7 @@ void goto_checkt::mod_by_zero_check(
 
 /*******************************************************************\
 
-Function: goto_checkt::integer_overflow_check
+Function: goto_checkt::conversion_check
 
   Inputs:
 
@@ -312,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
@@ -490,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);
 
@@ -898,7 +930,7 @@ void goto_checkt::pointer_overflow_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_pointer_check)
+  if(!enable_pointer_overflow_check)
     return;
 
   if(expr.id()==ID_plus ||
@@ -1429,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)
@@ -1451,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

@@ -9,12 +9,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 
-#include <util/namespace.h>
-#include <util/options.h>
-
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
+class namespacet;
+class optionst;
+
 void goto_check(
   const namespacet &ns,
   const optionst &options,
@@ -29,4 +29,36 @@ void goto_check(
   const optionst &options,
   goto_modelt &goto_model);
 
+#define GOTO_CHECK_OPTIONS \
+  "(bounds-check)(pointer-check)(memory-leak-check)" \
+  "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
+  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
+  "(float-overflow-check)(nan-check)"
+
+#define GOTO_CHECK_HELP \
+  " --bounds-check               enable array bounds checks\n" \
+  " --pointer-check              enable pointer checks\n" \
+  " --memory-leak-check          enable memory leak checks\n" \
+  " --div-by-zero-check          enable division by zero checks\n" \
+  " --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" \
+
+#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \
+  options.set_option("bounds-check", cmdline.isset("bounds-check")); \
+  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
+  options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
+  options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-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"))
+
 #endif

src/cbmc/cbmc_parse_options.cpp

@@ -46,8 +46,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <pointer-analysis/add_failed_symbols.h>
 
-#include <analyses/goto_check.h>
-
 #include <langapi/mode.h>
 
 #include "cbmc_solvers.h"
@@ -218,53 +216,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("propagation", true);
 
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
+  // all checks supported by goto_check
+  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1137,14 +1090,7 @@ void cbmc_parse_optionst::help()
     " --show-goto-functions        show goto program\n"
     "\n"
     "Program instrumentation options:\n"
-    " --bounds-check               enable array bounds checks\n"
-    " --div-by-zero-check          enable division by zero checks\n"
-    " --pointer-check              enable pointer checks\n"
-    " --memory-leak-check          enable memory leak checks\n"
-    " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
-    " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
-    " --float-overflow-check       check floating-point for +/-Inf\n"
-    " --nan-check                  check floating-point for NaN\n"
+    GOTO_CHECK_HELP
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"

src/cbmc/cbmc_parse_options.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_ui.h>
 
+#include <analyses/goto_check.h>
+
 #include "xml_interface.h"
 
 class bmct;
@@ -28,8 +30,7 @@ class optionst;
   "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
   "(classpath):(cp):(main-class):" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
-  "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \
+  GOTO_CHECK_OPTIONS \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \