Adds support for "checked:named-check" pragmas to avoid redudant instrumentation.

When several invocations to goto-instrument/cmbc are performed with named-check flags,
the same assertions were generated several times, and assertions generated by a check A
in some pass would be instrumented by a check B in some ulterior pass.

"checked" pragmas allow to keep track of which checks have been performed on which instructions
and are saved in the goto binaries, hence surviving across invocations of the tools.

The presente of a "checked" pragma for a given check on an instruction prevents future
invocations of the tools to generate again the assertions of that check.

We also tag all assertions generated by goto_check with "disable" pragmas to avoid
instrumenting instrumentation assertions in ulterior invocations of the tool.

Author: Remi Delmas

src/analyses/goto_check.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_check.h"
 
 #include <algorithm>
+#include <optional>
 
 #include <util/arith_tools.h>
 #include <util/array_name.h>
@@ -277,6 +278,23 @@ class goto_checkt
   bool enable_assumptions;
   bool enable_pointer_primitive_check;
 
+  /// Maps a named-check name to the corresponding boolean flag.
+  std::map<irep_idt, bool *> name_to_flag{
+    {"no-enum-check", &no_enum_check},
+    {"bounds-check", &enable_bounds_check},
+    {"pointer-check", &enable_pointer_check},
+    {"memory-leak-check", &enable_memory_leak_check},
+    {"div-by-zero-check", &enable_div_by_zero_check},
+    {"enum-range-check", &enable_enum_range_check},
+    {"signed-overflow-check", &enable_signed_overflow_check},
+    {"unsigned-overflow-check", &enable_unsigned_overflow_check},
+    {"pointer-overflow-check", &enable_pointer_overflow_check},
+    {"conversion-check", &enable_conversion_check},
+    {"undefined-shift-check", &enable_undefined_shift_check},
+    {"float-overflow-check", &enable_float_overflow_check},
+    {"nan-check", &enable_nan_check},
+    {"pointer-primitive-check", &enable_pointer_primitive_check}};
+
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
 
@@ -287,6 +305,35 @@ class goto_checkt
   allocationst allocations;
 
   irep_idt mode;
+
+  /// \brief Adds "checked" pragmas for all currently active named checks
+  /// on the given source location.
+  void add_active_named_check_pragmas(source_locationt &source_location);
+
+  /// \brief Adds "disable" pragmas for all named checks
+  /// on the given source location.
+  void add_all_disable_named_check_pragmas(source_locationt &source_location);
+
+  /// activation statuses for named checks
+  typedef enum
+  {
+    ENABLE,
+    DISABLE,
+    CHECKED
+  } check_statust;
+
+  /// optional (named-check, status) pair
+  typedef optionalt<std::pair<irep_idt, check_statust>> named_check_statust;
+
+  /// Matches a named-check string of the form
+  ///
+  /// ```
+  /// ("enable"|"disable"|"checked") ":" <named-check>
+  /// ```
+  ///
+  /// \returns a pair (name, status) if the match succeeds
+  /// and the name is known, nothing otherwise.
+  named_check_statust match_named_check(irep_idt named_check);
 };
 
 void goto_checkt::collect_allocations(
@@ -1575,6 +1622,8 @@ void goto_checkt::add_guarded_property(
     t->source_location_nonconst().set_comment(
       comment + " in " + source_expr_string);
     t->source_location_nonconst().set_property_class(property_class);
+
+    add_all_disable_named_check_pragmas(t->source_location_nonconst());
   }
 }
 
@@ -1877,11 +1926,24 @@ class flag_resett
         instruction.source_location().pretty());
     if(flag != new_value)
     {
-      flags_to_reset.emplace(&flag, flag);
+      flags_to_reset[&flag] = flag;
       flag = new_value;
     }
   }
 
+  /// \brief Sets the given flag to false, overriding any previous value.
+  ///
+  /// Contrary to \ref set_flag, does not trigger an INVARIANT
+  /// if the flag was already seen before.
+  void disable(bool &flag)
+  {
+    if(flag != false)
+    {
+      flags_to_reset[&flag] = flag;
+      flag = false;
+    }
+  }
+
   /// \brief Restore the values of all flags that have been
   /// modified via `set_flag`.
   ~flag_resett()
@@ -1917,63 +1979,40 @@ void goto_checkt::goto_check(
     goto_programt::instructiont &i=*it;
 
     flag_resett resetter(i);
+    std::list<bool *> already_checked;
     const auto &pragmas = i.source_location().get_pragmas();
     for(const auto &d : pragmas)
     {
-      if(d.first == "disable:bounds-check")
-        resetter.set_flag(enable_bounds_check, false, d.first);
-      else if(d.first == "disable:pointer-check")
-        resetter.set_flag(enable_pointer_check, false, d.first);
-      else if(d.first == "disable:memory-leak-check")
-        resetter.set_flag(enable_memory_leak_check, false, d.first);
-      else if(d.first == "disable:div-by-zero-check")
-        resetter.set_flag(enable_div_by_zero_check, false, d.first);
-      else if(d.first == "disable:enum-range-check")
-        resetter.set_flag(enable_enum_range_check, false, d.first);
-      else if(d.first == "disable:signed-overflow-check")
-        resetter.set_flag(enable_signed_overflow_check, false, d.first);
-      else if(d.first == "disable:unsigned-overflow-check")
-        resetter.set_flag(enable_unsigned_overflow_check, false, d.first);
-      else if(d.first == "disable:pointer-overflow-check")
-        resetter.set_flag(enable_pointer_overflow_check, false, d.first);
-      else if(d.first == "disable:float-overflow-check")
-        resetter.set_flag(enable_float_overflow_check, false, d.first);
-      else if(d.first == "disable:conversion-check")
-        resetter.set_flag(enable_conversion_check, false, d.first);
-      else if(d.first == "disable:undefined-shift-check")
-        resetter.set_flag(enable_undefined_shift_check, false, d.first);
-      else if(d.first == "disable:nan-check")
-        resetter.set_flag(enable_nan_check, false, d.first);
-      else if(d.first == "disable:pointer-primitive-check")
-        resetter.set_flag(enable_pointer_primitive_check, false, d.first);
-      else if(d.first == "enable:bounds-check")
-        resetter.set_flag(enable_bounds_check, true, d.first);
-      else if(d.first == "enable:pointer-check")
-        resetter.set_flag(enable_pointer_check, true, d.first);
-      else if(d.first == "enable:memory_leak-check")
-        resetter.set_flag(enable_memory_leak_check, true, d.first);
-      else if(d.first == "enable:div-by-zero-check")
-        resetter.set_flag(enable_div_by_zero_check, true, d.first);
-      else if(d.first == "enable:enum-range-check")
-        resetter.set_flag(enable_enum_range_check, true, d.first);
-      else if(d.first == "enable:signed-overflow-check")
-        resetter.set_flag(enable_signed_overflow_check, true, d.first);
-      else if(d.first == "enable:unsigned-overflow-check")
-        resetter.set_flag(enable_unsigned_overflow_check, true, d.first);
-      else if(d.first == "enable:pointer-overflow-check")
-        resetter.set_flag(enable_pointer_overflow_check, true, d.first);
-      else if(d.first == "enable:float-overflow-check")
-        resetter.set_flag(enable_float_overflow_check, true, d.first);
-      else if(d.first == "enable:conversion-check")
-        resetter.set_flag(enable_conversion_check, true, d.first);
-      else if(d.first == "enable:undefined-shift-check")
-        resetter.set_flag(enable_undefined_shift_check, true, d.first);
-      else if(d.first == "enable:nan-check")
-        resetter.set_flag(enable_nan_check, true, d.first);
-      else if(d.first == "enable:pointer-primitive-check")
-        resetter.set_flag(enable_pointer_primitive_check, true, d.first);
+      // match named-check related pragmas
+      auto parsed = match_named_check(d.first);
+      if(parsed.has_value())
+      {
+        auto named_check = parsed.value();
+        auto name = named_check.first;
+        auto status = named_check.second;
+        bool *flag = name_to_flag.find(name)->second;
+        switch(status)
+        {
+        case check_statust::ENABLE:
+          resetter.set_flag(*flag, true, name);
+          break;
+        case check_statust::DISABLE:
+          resetter.set_flag(*flag, false, name);
+          break;
+        case check_statust::CHECKED:
+          already_checked.push_back(flag);
+          break;
+        }
+      }
     }
 
+    // inhibit already checked checks
+    for(auto flag : already_checked)
+      resetter.disable(*flag);
+
+    // add checked pragmas for all active checks
+    add_active_named_check_pragmas(i.source_location_nonconst());
+
     new_code.clear();
 
     // we clear all recorded assertions if
@@ -2453,3 +2492,48 @@ void goto_check(
   const namespacet ns(goto_model.symbol_table);
   goto_check(ns, options, goto_model.goto_functions, message_handler);
 }
+
+void goto_checkt::add_active_named_check_pragmas(
+  source_locationt &source_location)
+{
+  for(auto it : name_to_flag)
+    if(*(it.second))
+      source_location.add_pragma("checked:" + id2string(it.first));
+}
+
+void goto_checkt::add_all_disable_named_check_pragmas(
+  source_locationt &source_location)
+{
+  for(auto it : name_to_flag)
+    source_location.add_pragma("disable:" + id2string(it.first));
+}
+
+goto_checkt::named_check_statust
+goto_checkt::match_named_check(irep_idt named_check)
+{
+  auto s = id2string(named_check);
+  auto status = check_statust::DISABLE;
+  if(s.find("enable:") == 0)
+  {
+    status = check_statust::ENABLE;
+  }
+  else if(s.find("disable:") == 0)
+  {
+    status = check_statust::DISABLE;
+  }
+  else if(s.find("checked:") == 0)
+  {
+    status = check_statust::CHECKED;
+  }
+  else
+  {
+    return {};
+  }
+
+  auto sep = s.find(":");
+  auto name = s.substr(sep + 1);
+  if(name_to_flag.find(name) == name_to_flag.end())
+    return {};
+
+  return std::pair<irep_idt, check_statust>{name, status};
+}