Merge pull request #6687 from tautschnig/cleanup/assertions-assumptions-filter

goto_check_ct: Transforming assertions and assumptions is language-agnostic

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -703,13 +703,7 @@ void janalyzer_parse_optionst::process_goto_function(
 
   remove_returns(function, function_is_stub);
 
-  // add generic checks
-  goto_check(
-    function.get_function_id(),
-    function.get_goto_function(),
-    ns,
-    options,
-    ui_message_handler);
+  transform_assertions_assumptions(options, function.get_goto_function().body);
 }
 
 bool janalyzer_parse_optionst::can_generate_function_body(const irep_idt &name)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -11,27 +11,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "jbmc_parse_options.h"
 
-#include <cstdlib> // exit()
-#include <iostream>
-#include <memory>
-
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
 #include <util/version.h>
 #include <util/xml.h>
 
-#include <langapi/language.h>
-
-#include <ansi-c/ansi_c_language.h>
-
-#include <goto-checker/all_properties_verifier.h>
-#include <goto-checker/all_properties_verifier_with_fault_localization.h>
-#include <goto-checker/all_properties_verifier_with_trace_storage.h>
-#include <goto-checker/stop_on_fail_verifier.h>
-#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
-
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -45,18 +31,17 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
 
+#include <analyses/goto_check.h>
+#include <ansi-c/ansi_c_language.h>
+#include <goto-checker/all_properties_verifier.h>
+#include <goto-checker/all_properties_verifier_with_fault_localization.h>
+#include <goto-checker/all_properties_verifier_with_trace_storage.h>
+#include <goto-checker/stop_on_fail_verifier.h>
+#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/reachability_slicer.h>
-
 #include <goto-symex/path_storage.h>
-
-#include <linking/static_lifetime_init.h>
-
-#include <pointer-analysis/add_failed_symbols.h>
-
-#include <langapi/mode.h>
-
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_multi_path_symex_checker.h>
@@ -69,6 +54,14 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/remove_java_new.h>
 #include <java_bytecode/replace_java_nondet.h>
 #include <java_bytecode/simple_method_stubbing.h>
+#include <langapi/language.h>
+#include <langapi/mode.h>
+#include <linking/static_lifetime_init.h>
+#include <pointer-analysis/add_failed_symbols.h>
+
+#include <cstdlib> // exit()
+#include <iostream>
+#include <memory>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
   : parse_options_baset(
@@ -717,13 +710,7 @@ void jbmc_parse_optionst::process_goto_function(
       ui_message_handler);
   }
 
-  // add generic checks
-  goto_check_java(
-    function.get_function_id(),
-    function.get_goto_function(),
-    ns,
-    options,
-    ui_message_handler);
+  transform_assertions_assumptions(options, function.get_goto_function().body);
 
   // Replace Java new side effects
   remove_java_new(

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -11,9 +11,6 @@ Author: Peter Schrammel
 
 #include "jdiff_parse_options.h"
 
-#include <cstdlib> // exit()
-#include <iostream>
-
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
@@ -31,15 +28,18 @@ Author: Peter Schrammel
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 
+#include <analyses/goto_check.h>
+#include <goto-diff/change_impact.h>
+#include <goto-diff/unified_diff.h>
 #include <goto-instrument/cover.h>
-
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 
 #include "java_syntactic_diff.h"
-#include <goto-diff/change_impact.h>
-#include <goto-diff/unified_diff.h>
+
+#include <cstdlib> // exit()
+#include <iostream>
 
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(
@@ -190,9 +190,7 @@ bool jdiff_parse_optionst::process_goto_program(
   // remove returns
   remove_returns(goto_model);
 
-  // add generic checks
-  log.status() << "Generic Property Instrumentation" << messaget::eom;
-  goto_check_java(options, goto_model, ui_message_handler);
+  transform_assertions_assumptions(options, goto_model);
 
   // checks don't know about adjusted float expressions
   adjust_float_expressions(goto_model);

src/analyses/goto_check.cpp

@@ -11,10 +11,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_check.h"
 
-#include "goto_check_c.h"
-
+#include <util/options.h>
 #include <util/symbol.h>
 
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_skip.h>
+
+#include "goto_check_c.h"
+
 void goto_check(
   const irep_idt &function_identifier,
   goto_functionst::goto_functiont &goto_function,
@@ -47,3 +51,84 @@ void goto_check(
 {
   goto_check_c(options, goto_model, message_handler);
 }
+
+static void transform_assertions_assumptions(
+  goto_programt &goto_program,
+  bool enable_assertions,
+  bool enable_built_in_assertions,
+  bool enable_assumptions)
+{
+  bool did_something = false;
+
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_assert())
+    {
+      bool is_user_provided =
+        instruction.source_location().get_bool("user-provided");
+
+      if(
+        (is_user_provided && !enable_assertions &&
+         instruction.source_location().get_property_class() != "error label") ||
+        (!is_user_provided && !enable_built_in_assertions))
+      {
+        instruction.turn_into_skip();
+        did_something = true;
+      }
+    }
+    else if(instruction.is_assume())
+    {
+      if(!enable_assumptions)
+      {
+        instruction.turn_into_skip();
+        did_something = true;
+      }
+    }
+  }
+
+  if(did_something)
+    remove_skip(goto_program);
+}
+
+void transform_assertions_assumptions(
+  const optionst &options,
+  goto_modelt &goto_model)
+{
+  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");
+
+  // check whether there could possibly be anything to do
+  if(enable_assertions && enable_built_in_assertions && enable_assumptions)
+    return;
+
+  for(auto &entry : goto_model.goto_functions.function_map)
+  {
+    transform_assertions_assumptions(
+      entry.second.body,
+      enable_assertions,
+      enable_built_in_assertions,
+      enable_assumptions);
+  }
+}
+
+void transform_assertions_assumptions(
+  const optionst &options,
+  goto_programt &goto_program)
+{
+  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");
+
+  // check whether there could possibly be anything to do
+  if(enable_assertions && enable_built_in_assertions && enable_assumptions)
+    return;
+
+  transform_assertions_assumptions(
+    goto_program,
+    enable_assertions,
+    enable_built_in_assertions,
+    enable_assumptions);
+}

src/analyses/goto_check.h

@@ -34,4 +34,18 @@ void goto_check(
 
 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
+/// false in \p options.
+void transform_assertions_assumptions(
+  const optionst &options,
+  goto_modelt &goto_model);
+
+/// Handle the options "assertions", "built-in-assertions", "assumptions" to
+/// remove assertions and assumptions in \p goto_program when these are set to
+/// false in \p options.
+void transform_assertions_assumptions(
+  const optionst &options,
+  goto_programt &goto_program);
+
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H

src/analyses/goto_check_c.cpp

@@ -74,10 +74,6 @@ class goto_check_ct
     enable_nan_check = _options.get_bool_option("nan-check");
     retain_trivial = _options.get_bool_option("retain-trivial-checks");
     enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
-    enable_assertions = _options.get_bool_option("assertions");
-    enable_built_in_assertions =
-      _options.get_bool_option("built-in-assertions");
-    enable_assumptions = _options.get_bool_option("assumptions");
     error_labels = _options.get_list_option("error-label");
     enable_pointer_primitive_check =
       _options.get_bool_option("pointer-primitive-check");
@@ -274,9 +270,6 @@ class goto_check_ct
   bool enable_nan_check;
   bool retain_trivial;
   bool enable_assert_to_assume;
-  bool enable_assertions;
-  bool enable_built_in_assertions;
-  bool enable_assumptions;
   bool enable_pointer_primitive_check;
 
   /// Maps a named-check name to the corresponding boolean flag.
@@ -2173,27 +2166,6 @@ void goto_check_ct::goto_check(
       // this has no successor
       assertions.clear();
     }
-    else if(i.is_assert())
-    {
-      bool is_user_provided = i.source_location().get_bool("user-provided");
-
-      if(
-        (is_user_provided && !enable_assertions &&
-         i.source_location().get_property_class() != "error label") ||
-        (!is_user_provided && !enable_built_in_assertions))
-      {
-        i.turn_into_skip();
-        did_something = true;
-      }
-    }
-    else if(i.is_assume())
-    {
-      if(!enable_assumptions)
-      {
-        i.turn_into_skip();
-        did_something = true;
-      }
-    }
     else if(i.is_dead())
     {
       if(enable_pointer_check || enable_pointer_primitive_check)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1331,6 +1331,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // add generic checks, if needed
   goto_check(options, goto_model, ui_message_handler);
+  transform_assertions_assumptions(options, goto_model);
 
   // check for uninitalized local variables
   if(cmdline.isset("uninitialized-check"))

src/goto-programs/process_goto_program.cpp

@@ -74,6 +74,7 @@ bool process_goto_program(
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
   goto_check(options, goto_model, log.get_message_handler());
+  transform_assertions_assumptions(options, goto_model);
 
   // checks don't know about adjusted float expressions
   adjust_float_expressions(goto_model);