[WIP] Filter generated assertions

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -475,7 +475,7 @@ void acceleration_utilst::ensure_no_overflows(scratch_programt &program)
 
   // goto_functionst::goto_functiont fn;
   // fn.body.instructions.swap(program.instructions);
-  // goto_check(ns, checker_options, fn);
+  // goto_check_c(ns, checker_options, fn);
   // fn.body.instructions.swap(program.instructions);
 
 #ifdef DEBUG

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1328,7 +1328,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   }
 
   // add generic checks, if needed
-  goto_check(options, goto_model, ui_message_handler);
+  goto_check_c(options, goto_model, ui_message_handler);
+  remove_disabled_checks(options, goto_model);
   transform_assertions_assumptions(options, goto_model);
 
   // check for uninitalized local variables

src/goto-programs/goto_check.cpp

@@ -12,45 +12,11 @@ Author: Daniel Kroening, [email protected]
 #include "goto_check.h"
 
 #include <util/options.h>
-#include <util/symbol.h>
+#include <util/prefix.h>
+#include <util/simplify_expr.h>
 
-#include <goto-programs/goto_model.h>
-#include <goto-programs/remove_skip.h>
-
-#include <ansi-c/goto_check_c.h>
-
-void goto_check(
-  const irep_idt &function_identifier,
-  goto_functionst::goto_functiont &goto_function,
-  const namespacet &ns,
-  const optionst &options,
-  message_handlert &message_handler)
-{
-  const auto &function_symbol = ns.lookup(function_identifier);
-
-  if(function_symbol.mode == ID_C)
-  {
-    goto_check_c(
-      function_identifier, goto_function, ns, options, message_handler);
-  }
-}
-
-void goto_check(
-  const namespacet &ns,
-  const optionst &options,
-  goto_functionst &goto_functions,
-  message_handlert &message_handler)
-{
-  goto_check_c(ns, options, goto_functions, message_handler);
-}
-
-void goto_check(
-  const optionst &options,
-  goto_modelt &goto_model,
-  message_handlert &message_handler)
-{
-  goto_check_c(options, goto_model, message_handler);
-}
+#include "goto_model.h"
+#include "remove_skip.h"
 
 static void transform_assertions_assumptions(
   goto_programt &goto_program,
@@ -132,3 +98,161 @@ void transform_assertions_assumptions(
     enable_built_in_assertions,
     enable_assumptions);
 }
+
+void remove_disabled_checks(const optionst &options, goto_modelt &goto_model)
+{
+  // properties to keep
+  const bool enable_bounds_check = options.get_bool_option("bounds-check");
+  const bool enable_conversion_check =
+    options.get_bool_option("conversion-check");
+  const bool enable_div_by_zero_check =
+    options.get_bool_option("div-by-zero-check");
+  const bool enable_enum_range_check =
+    options.get_bool_option("enum-range-check");
+  const bool enable_float_overflow_check =
+    options.get_bool_option("float-overflow-check");
+  const bool enable_memory_leak_check =
+    options.get_bool_option("memory-leak-check");
+  const bool enable_nan_check = options.get_bool_option("nan-check");
+  const bool enable_pointer_check = options.get_bool_option("pointer-check");
+  const bool enable_pointer_overflow_check =
+    options.get_bool_option("pointer-overflow-check");
+  const bool enable_pointer_primitive_check =
+    options.get_bool_option("pointer-primitive-check");
+  const bool enable_signed_overflow_check =
+    options.get_bool_option("signed-overflow-check");
+  const bool enable_undefined_shift_check =
+    options.get_bool_option("undefined-shift-check");
+  const bool enable_unsigned_overflow_check =
+    options.get_bool_option("unsigned-overflow-check");
+  const auto error_labels = options.get_list_option("error-label");
+
+  // transformations retained on properties
+  // const bool enable_simplify = options.get_bool_option("simplify");
+  const bool enable_assert_to_assume =
+    options.get_bool_option("assert-to-assume");
+  // const bool retain_trivial = options.get_bool_option("retain-trivial-checks");
+
+  const std::unordered_map<irep_idt, bool> should_skip = {
+    {"NaN", !enable_nan_check},
+    {"array bounds", !enable_bounds_check},
+    {"bit count", !enable_bounds_check},
+    {"division-by-zero", !enable_div_by_zero_check},
+    {"enum-range-check", !enable_enum_range_check},
+    {"error label", error_labels.empty()}, // further evaluation is necessary
+    {"memory-leak", !enable_memory_leak_check},
+    {"overflow", false}, // further evaluation is necessary
+    {"pointer arithmetic",
+     !enable_pointer_check && !enable_pointer_overflow_check},
+    {"pointer dereference", !enable_pointer_check},
+    {"pointer primitives", !enable_pointer_primitive_check},
+    {"pointer", !enable_pointer_check},
+    {"undefined-shift", !enable_undefined_shift_check}};
+
+  const namespacet ns(goto_model.symbol_table);
+
+  for(auto &entry : goto_model.goto_functions.function_map)
+  {
+    bool added_skip = false;
+
+    for(auto &instruction : entry.second.body.instructions)
+    {
+      // TODO: we may have other code using __CPROVER_dead_object and therefore
+      // cannot easily remove these assignments
+#if 0
+      if(
+        instruction.is_assign() && !enable_pointer_check &&
+        !enable_pointer_primitive_check &&
+        instruction.assign_lhs().id() == ID_symbol &&
+        to_symbol_expr(instruction.assign_lhs()).get_identifier() ==
+          CPROVER_PREFIX "dead_object")
+      {
+        instruction.turn_into_skip();
+        added_skip = true;
+        continue;
+      }
+      else
+#endif
+      if(!instruction.is_assert())
+        continue;
+
+      const irep_idt &property_class =
+        instruction.source_location().get_property_class();
+      auto entry_it = should_skip.find(property_class);
+      bool skip = entry_it != should_skip.end() && entry_it->second;
+
+      if(!skip && property_class == "error label")
+      {
+        const std::string comment =
+          id2string(instruction.source_location().get_comment());
+        skip = true;
+        for(const auto &l : error_labels)
+        {
+          if(comment == std::string("error label " + l))
+          {
+            skip = false;
+            break;
+          }
+        }
+      }
+      else if(!skip && property_class == "overflow")
+      {
+        const std::string comment =
+          id2string(instruction.source_location().get_comment());
+        if(has_prefix(comment, "result of signed mod is not representable"))
+          skip = !enable_signed_overflow_check;
+        else if(has_prefix(comment, "arithmetic overflow on "))
+        {
+          const std::string op = comment.substr(23);
+          if(has_prefix(op, "floating-point "))
+            skip = !enable_float_overflow_check;
+          else if(
+            has_prefix(op, "signed type ") || has_prefix(op, "float to ") ||
+            has_prefix(op, "signed to ") || has_prefix(op, "unsigned to "))
+          {
+            skip = !enable_conversion_check;
+          }
+          else if(has_prefix(op, "signed "))
+          {
+            // TODO: some of these checks may also have been generated via
+            // enable_pointer_overflow_check
+            skip = !enable_signed_overflow_check;
+          }
+          else if(has_prefix(op, "unsigned "))
+          {
+            // TODO: some of these checks may also have been generated via
+            // enable_pointer_overflow_check
+            skip = !enable_unsigned_overflow_check;
+          }
+        }
+      }
+
+      if(skip)
+      {
+        instruction.turn_into_skip();
+        added_skip = true;
+      }
+      else
+      {
+        if(enable_assert_to_assume)
+          instruction.turn_into_assume();
+
+          // TODO: the following would also simplify assertions not generated by
+          // goto_check_c
+#if 0
+        if(enable_simplify)
+          simplify(instruction.guard, ns);
+
+        if(!retain_trivial && instruction.guard.is_true())
+        {
+          instruction.turn_into_skip();
+          added_skip = true;
+        }
+#endif
+      }
+    }
+
+    if(added_skip)
+      remove_skip(entry.second.body);
+  }
+}

src/goto-programs/goto_check.h

@@ -12,27 +12,9 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 
-#include "goto_functions.h"
-
 class goto_modelt;
-class namespacet;
+class goto_programt;
 class optionst;
-class message_handlert;
-
-void goto_check(
-  const namespacet &,
-  const optionst &,
-  goto_functionst &,
-  message_handlert &);
-
-void goto_check(
-  const irep_idt &function_identifier,
-  goto_functionst::goto_functiont &,
-  const namespacet &,
-  const optionst &,
-  message_handlert &);
-
-void goto_check(const optionst &, goto_modelt &, message_handlert &);
 
 /// Handle the options "assertions", "built-in-assertions", "assumptions" to
 /// remove assertions and assumptions in \p goto_model when these are set to
@@ -48,4 +30,6 @@ void transform_assertions_assumptions(
   const optionst &options,
   goto_programt &goto_program);
 
+void remove_disabled_checks(const optionst &, goto_modelt &);
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H

src/goto-programs/process_goto_program.cpp

@@ -27,6 +27,8 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
+#include <ansi-c/goto_check_c.h>
+
 #include "goto_check.h"
 
 bool process_goto_program(
@@ -73,7 +75,8 @@ bool process_goto_program(
 
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
-  goto_check(options, goto_model, log.get_message_handler());
+  goto_check_c(options, goto_model, log.get_message_handler());
+  remove_disabled_checks(options, goto_model);
   transform_assertions_assumptions(options, goto_model);
 
   // checks don't know about adjusted float expressions