[WIP] Filter generated assertions

This changes C/C++ goto checks to be generated at compile time, and
filtered-out based on command-line options at analysis time.

Author: tautschnig

src/ansi-c/goto_check_c.cpp

@@ -72,6 +72,7 @@ class goto_check_ct
     enable_simplify = _options.get_bool_option("simplify");
     enable_nan_check = _options.get_bool_option("nan-check");
     retain_trivial = _options.get_bool_option("retain-trivial-checks");
+    // TODO: the following aren't C specific
     enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
     enable_assertions = _options.get_bool_option("assertions");
     enable_built_in_assertions =
@@ -1511,6 +1512,7 @@ void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)
   if(!enable_bounds_check)
     return;
 
+  // TODO: get rid of this
   if(
     expr.find(ID_C_bounds_check).is_not_nil() &&
     !expr.get_bool(ID_C_bounds_check))
@@ -2181,6 +2183,7 @@ void goto_check_ct::goto_check(
         const notequal_exprt not_eq_null(
           pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
 
+        // TODO this is unconditional
         add_guarded_property(
           not_eq_null,
           "throwing null",

src/goto-programs/goto_check.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/goto_check_c.h>
 
+#include "remove_skip.h"
+
 void goto_check(
   const irep_idt &function_identifier,
   goto_functionst::goto_functiont &goto_function,
@@ -47,3 +49,140 @@ void goto_check(
 {
   goto_check_c(options, goto_model, message_handler);
 }
+
+void remove_disabled_checks(
+  const optionst &options,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  // done
+  const bool enable_bounds_check = options.get_bool_option("bounds-check");
+  const bool enable_pointer_check = options.get_bool_option("pointer-check");
+  // done
+  const bool enable_memory_leak_check = options.get_bool_option("memory-leak-check");
+  // done
+  const bool enable_div_by_zero_check = options.get_bool_option("div-by-zero-check");
+  // done
+  const bool enable_enum_range_check = options.get_bool_option("enum-range-check");
+  const bool enable_signed_overflow_check = options.get_bool_option("signed-overflow-check");
+  const bool enable_unsigned_overflow_check = options.get_bool_option("unsigned-overflow-check");
+  const bool enable_pointer_overflow_check = options.get_bool_option("pointer-overflow-check");
+  const bool enable_conversion_check = options.get_bool_option("conversion-check");
+  // done
+  const bool enable_undefined_shift_check = options.get_bool_option("undefined-shift-check");
+  const bool enable_float_overflow_check = options.get_bool_option("float-overflow-check");
+  // done
+  const bool enable_nan_check = options.get_bool_option("nan-check");
+  const bool enable_assert_to_assume = options.get_bool_option("assert-to-assume");
+  const bool enable_assertions = options.get_bool_option("assertions");
+  const bool enable_built_in_assertions = options.get_bool_option("built-in-assertions");
+  const bool enable_assumptions = options.get_bool_option("assumptions");
+  // done
+  const bool error_labels = options.get_list_option("error-label");
+  // done
+  const bool enable_pointer_primitive_check = options.get_bool_option("pointer-primitive-check");
+
+  const bool enable_simplify = options.get_bool_option("simplify");
+  const bool retain_trivial = options.get_bool_option("retain-trivial-checks");
+
+  for(auto &entry : goto_model.goto_functions.function_map)
+  {
+    bool changed = false;
+
+    for(auto &instruction : entry.second.body.instructions)
+    {
+      if(instruction.is_assign())
+      {
+        if(!enable_pointer_check && !enable_pointer_primitive_check &&
+          instruction.get_assign_lhs().id() == ID_symbol &&
+           to_symbol_expr(instruction.get_assign_lhs()).get_identifier() == CPROVER_PREFIX "dead_object")
+        {
+        instruction->make_skip(), changed = true;
+        }
+      }
+      else if(!instruction.is_assert())
+        continue;
+
+      const irep_idt &property_class = instruction.get_property_class();
+
+      if(!error_labels && property_class == "error label")
+        instruction->make_skip(), changed = true;
+      else if(!enable_div_by_zero_check && property_class == "division-by-zero")
+      {
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_enum_range_check && property_class == "enum-range-check")
+        instruction->make_skip(), changed = true;
+      else if(!enable_undefined_shift_check && property_class == "undefined-shift")
+        instruction->make_skip(), changed = true;
+      else if(!enable_signed_overflow_check && property_class == "overflow")
+      {
+        // "result of signed mod is not representable"
+        "arithmetic overflow on signed division",
+        "arithmetic overflow on signed unary minus",
+        "arithmetic overflow on signed shl",
+        "arithmetic overflow on signed " + expr.id_string(),
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_unsigned_overflow_check && property_class == "overflow")
+      {
+        "arithmetic overflow on unsigned unary minus",
+        "arithmetic overflow on unsigned " + expr.id_string(),
+      }
+      else if(!enable_float_overflow_check && property_class == "overflow")
+      {
+        "arithmetic overflow on floating-point typecast",
+        "arithmetic overflow on floating-point division",
+        "arithmetic overflow on floating-point " + kind,
+      }
+      else if(!enable_conversion_check && property_class == "overflow")
+      {
+        // "arithmetic overflow on signed type conversion"
+          "arithmetic overflow on unsigned to signed type conversion",
+          "arithmetic overflow on float to signed integer type conversion",
+          "arithmetic overflow on signed to unsigned type conversion",
+          "arithmetic overflow on unsigned to unsigned type conversion",
+          "arithmetic overflow on float to unsigned integer type conversion",
+      }
+      else if(!enable_nan_check && property_class == "NaN")
+      {
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_pointer_check && property_class == "pointer")
+      {
+      }
+      else if(!enable_pointer_check && property_class == "pointer arithmetic")
+      {
+      }
+      else if(!enable_pointer_check && property_class == "pointer dereference")
+      {
+      }
+      else if(!enable_pointer_overflow_check && property_class == "overflow")
+      {
+        // same as signed/unsigned overflow
+      }
+      else if(!enable_pointer_overflow_check && property_class == "pointer arithmetic")
+      {
+      }
+      else if(!enable_pointer_primitive_check && property_class == "pointer primitives")
+      {
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_bounds_check && property_class == "array bounds")
+      {
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_bounds_check && property_class == "bit count")
+      {
+        instruction->make_skip(), changed = true;
+      }
+      else if(!enable_memory_leak_check && property_class == "memory-leak")
+      {
+        instruction->make_skip(), changed = true;
+      }
+    }
+
+    if(changed)
+      remove_skip(entry.second.body);
+  }
+}

src/goto-programs/goto_check.h

@@ -34,4 +34,7 @@ void goto_check(
 
 void goto_check(const optionst &, goto_modelt &, message_handlert &);
 
+void remove_disabled_checks(
+  const optionst &, goto_modelt &, message_handlert &);
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H