Implemented review requests

Author: Remi Delmas

src/analyses/goto_check.cpp

@@ -280,7 +280,6 @@ class goto_checkt
 
   /// 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},
@@ -308,11 +307,12 @@ class goto_checkt
 
   /// \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);
+  void add_active_named_check_pragmas(source_locationt &source_location) const;
 
   /// \brief Adds "disable" pragmas for all named checks
   /// on the given source location.
-  void add_all_disable_named_check_pragmas(source_locationt &source_location);
+  void
+  add_all_disable_named_check_pragmas(source_locationt &source_location) const;
 
   /// activation statuses for named checks
   typedef enum
@@ -323,7 +323,7 @@ class goto_checkt
   } check_statust;
 
   /// optional (named-check, status) pair
-  typedef optionalt<std::pair<irep_idt, check_statust>> named_check_statust;
+  using named_check_statust = optionalt<std::pair<irep_idt, check_statust>>;
 
   /// Matches a named-check string of the form
   ///
@@ -333,7 +333,7 @@ class goto_checkt
   ///
   /// \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);
+  named_check_statust match_named_check(const irep_idt &named_check) const;
 };
 
 void goto_checkt::collect_allocations(
@@ -1897,11 +1897,13 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
     return {};
 }
 
-/// \brief Set a Boolean flag to a new value (via `set_flag`) and restore
-/// the previous value when the entire object goes out of scope.
+/// Allows to:
+/// - override a Boolean flag with a new value via `set_flag`
+/// - set a Boolean flag to false via `disable_flag`, such that
+///   previous `set_flag` are overridden and future `set_flag` are ignored.
 ///
-/// \remarks Calls to set_value are tracked to allow detecting doubles sets
-/// with different values and trigger an INVARIANT.
+/// A flag's initial value (before any `set_flag` or `disable_flag`) is restored
+/// when the entire object goes out of scope.
 class flag_resett
 {
 public:
@@ -1913,16 +1915,18 @@ class flag_resett
   /// \brief Store the current value of \p flag and
   /// then set its value to \p new_value.
   ///
-  /// \remarks an INVARIANT triggers iff the flag is set
-  /// more than once with different values.
+  /// - calling `set_flag` after `disable_flag` is a no-op
+  /// - calling `set_flag` twice triggers an INVARIANT
   void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
   {
-    bool seen = flags_to_reset.find(&flag) != flags_to_reset.end();
+    // make this a no-op if the flag is disabled
+    if(disabled_flags.find(&flag) != disabled_flags.end())
+      return;
+
+    // detect double sets
     INVARIANT(
-      !(seen && flag != new_value),
-      "Flag " + id2string(flag_name) +
-        " set twice with incompatible values "
-        " at \n" +
+      flags_to_reset.find(&flag) == flags_to_reset.end(),
+      "Flag " + id2string(flag_name) + " set twice at \n" +
         instruction.source_location().pretty());
     if(flag != new_value)
     {
@@ -1931,17 +1935,28 @@ class flag_resett
     }
   }
 
-  /// \brief Sets the given flag to false, overriding any previous value.
+  /// 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)
+  /// - calling `disable_flag` after `set_flag` overrides the set value
+  /// - calling `disable_flag` twice triggers an INVARIANT
+  void disable_flag(bool &flag, const irep_idt &flag_name)
   {
-    if(flag)
-    {
+    INVARIANT(
+      disabled_flags.find(&flag) == disabled_flags.end(),
+      "Flag " + id2string(flag_name) + " disabled twice at \n" +
+        instruction.source_location().pretty());
+
+    disabled_flags.insert(&flag);
+
+    // If the flag has not already been set,
+    // we store its current value in the reset map.
+    // Otherwise, the reset map already holds
+    // the initial value we want to reset it to, keep it as is.
+    if(flags_to_reset.find(&flag) == flags_to_reset.end())
       flags_to_reset[&flag] = flag;
-      flag = false;
-    }
+
+    // set the flag to false in all cases.
+    flag = false;
   }
 
   /// \brief Restore the values of all flags that have been
@@ -1955,6 +1970,7 @@ class flag_resett
 private:
   const goto_programt::instructiont &instruction;
   std::map<bool *, bool> flags_to_reset;
+  std::set<bool *> disabled_flags;
 };
 
 void goto_checkt::goto_check(
@@ -1979,15 +1995,14 @@ 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)
     {
       // match named-check related pragmas
-      auto parsed = match_named_check(d.first);
-      if(parsed.has_value())
+      auto matched = match_named_check(d.first);
+      if(matched.has_value())
       {
-        auto named_check = parsed.value();
+        auto named_check = matched.value();
         auto name = named_check.first;
         auto status = named_check.second;
         bool *flag = name_to_flag.find(name)->second;
@@ -2000,16 +2015,12 @@ void goto_checkt::goto_check(
           resetter.set_flag(*flag, false, name);
           break;
         case check_statust::CHECKED:
-          already_checked.push_back(flag);
+          resetter.disable_flag(*flag, name);
           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());
 
@@ -2494,46 +2505,44 @@ void goto_check(
 }
 
 void goto_checkt::add_active_named_check_pragmas(
-  source_locationt &source_location)
+  source_locationt &source_location) const
 {
-  for(auto it : name_to_flag)
-    if(*(it.second))
-      source_location.add_pragma("checked:" + id2string(it.first));
+  for(const auto &entry : name_to_flag)
+    if(*(entry.second))
+      source_location.add_pragma("checked:" + id2string(entry.first));
 }
 
 void goto_checkt::add_all_disable_named_check_pragmas(
-  source_locationt &source_location)
+  source_locationt &source_location) const
 {
-  for(auto it : name_to_flag)
-    source_location.add_pragma("disable:" + id2string(it.first));
+  for(const auto &entry : name_to_flag)
+    source_location.add_pragma("disable:" + id2string(entry.first));
 }
 
 goto_checkt::named_check_statust
-goto_checkt::match_named_check(irep_idt named_check)
+goto_checkt::match_named_check(const irep_idt &named_check) const
 {
   auto s = id2string(named_check);
-  auto status = check_statust::DISABLE;
-  if(s.find("enable:") == 0)
-  {
+  auto col = s.find(":");
+
+  if(col == std::string::npos)
+    return {}; // separator not found
+
+  auto name = s.substr(col + 1);
+
+  if(name_to_flag.find(name) == name_to_flag.end())
+    return {}; // name unknown
+
+  check_statust status;
+  if(!s.compare(0, 6, "enable"))
     status = check_statust::ENABLE;
-  }
-  else if(s.find("disable:") == 0)
-  {
+  else if(!s.compare(0, 7, "disable"))
     status = check_statust::DISABLE;
-  }
-  else if(s.find("checked:") == 0)
-  {
+  else if(!s.compare(0, 7, "checked"))
     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 {}; // prefix unknow
 
+  // success
   return std::pair<irep_idt, check_statust>{name, status};
 }