move functions to utils.cpp

Author: Remi Delmas

src/goto-instrument/contracts/contracts.cpp

@@ -40,7 +40,6 @@ Date: February 2016
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
-#include <util/simplify_expr.h>
 #include <util/std_code.h>
 
 #include "memory_predicates.h"
@@ -1175,13 +1174,13 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     "Recursive functions found during inlining");
 
   // clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
-  simplify_gotos(goto_program);
+  simplify_gotos(goto_program, ns);
 
   // restore internal coherence in the programs
   goto_functions.update();
 
   INVARIANT(
-    is_loop_free(goto_program),
+    is_loop_free(goto_program, ns, log),
     "Loops remain in function '" + id2string(function) +
       "', assigns clause checking instrumentation cannot be applied.");
 
@@ -1212,10 +1211,10 @@ void code_contractst::check_frame_conditions(
     if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end())
       continue;
 
-    if(skip_parameter_assigns && is_parameter_assign(instruction_it))
+    if(skip_parameter_assigns && is_parameter_assign(instruction_it, ns))
       continue;
 
-    if(is_auxiliary_decl_dead_or_assign(instruction_it))
+    if(is_auxiliary_decl_dead_or_assign(instruction_it, ns))
       continue;
 
     // Do not instrument this instruction again in the future,
@@ -1605,107 +1604,3 @@ bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
   }
   return fail;
 }
-
-bool code_contractst::is_parameter_assign(
-  const goto_programt::targett &instruction_it)
-{
-  optionalt<symbol_exprt> sym = {};
-
-  // extract symbol
-  if(instruction_it->is_assign())
-  {
-    const auto &lhs = instruction_it->assign_lhs();
-    if(can_cast_expr<symbol_exprt>(lhs))
-      sym = to_symbol_expr(lhs);
-  }
-
-  // check condition
-  if(sym.has_value())
-    return ns.lookup(sym.value().get_identifier()).is_parameter;
-
-  return false;
-}
-
-bool code_contractst::is_auxiliary_decl_dead_or_assign(
-  const goto_programt::targett &instruction_it)
-{
-  optionalt<symbol_exprt> sym = {};
-
-  // extract symbol
-  if(instruction_it->is_decl())
-    sym = instruction_it->decl_symbol();
-  else if(instruction_it->is_dead())
-    sym = instruction_it->dead_symbol();
-  else if(instruction_it->is_assign())
-  {
-    const auto &lhs = instruction_it->assign_lhs();
-    if(can_cast_expr<symbol_exprt>(lhs))
-      sym = to_symbol_expr(lhs);
-  }
-
-  // check condition
-  if(sym.has_value())
-    return ns.lookup(sym.value().get_identifier()).is_auxiliary;
-
-  return false;
-}
-
-void code_contractst::simplify_gotos(goto_programt &goto_program)
-{
-  for(auto &instruction : goto_program.instructions)
-  {
-    if(instruction.is_goto())
-    {
-      const auto &condition = instruction.get_condition();
-      const auto &simplified = simplify_expr(condition, ns);
-      if(simplified.is_false())
-        instruction.turn_into_skip();
-    }
-  }
-}
-
-bool code_contractst::is_loop_free(const goto_programt &goto_program)
-{
-  // create cfg from instruction list
-  cfg_baset<empty_cfg_nodet> cfg;
-  cfg(goto_program);
-
-  // check that all nodes are there
-  INVARIANT(
-    goto_program.instructions.size() == cfg.size(),
-    "Instruction list vs CFG size mismatch.");
-
-  // compute SCCs
-  std::vector<node_indext> node_to_scc(cfg.size(), -1);
-  auto nof_sccs = cfg.SCCs(node_to_scc);
-
-  // compute size of each SCC
-  std::vector<int> scc_size(nof_sccs, 0);
-  for(auto scc : node_to_scc)
-  {
-    INVARIANT(
-      0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
-    scc_size[scc]++;
-  }
-
-  // check they are all of size 1
-  for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
-  {
-    auto size = scc_size[scc_id];
-    if(size > 1)
-    {
-      log.error() << "Found CFG SCC with size " << size << messaget::eom;
-      for(const auto &node_id : node_to_scc)
-      {
-        if(node_to_scc[node_id] == scc_id)
-        {
-          const auto &pc = cfg[node_id].PC;
-          goto_program.output_instruction(ns, "", log.error(), *pc);
-          log.error() << messaget::eom;
-        }
-      }
-      return false;
-    }
-  }
-  return true;
-}

src/goto-instrument/contracts/contracts.h

@@ -213,23 +213,6 @@ class code_contractst
     source_locationt location,
     const irep_idt &mode);
 
-private:
-  /// Returns true iff the instruction is a `DECL x`, `DEAD x`,
-  /// or `ASSIGN x := expr` where `x` has the `is_parameter` flag set.
-  bool is_parameter_assign(const goto_programt::targett &instruction_it);
-
-  /// Returns true iff the instruction is a `DECL x`, `DEAD x`,
-  /// or `ASSIGN x := expr` where `x` has the `is_auxiliary` flag set.
-  bool is_auxiliary_decl_dead_or_assign(
-    const goto_programt::targett &instruction_it);
-
-  /// Turns goto instructions `IF cond GOTO label` where the condition
-  /// statically simplifies to `false` into SKIP instructions.
-  void simplify_gotos(goto_programt &goto_program);
-
-  /// Returns true iff the given program is loop-free,
-  /// i.e. if each SCC of its CFG contains a single element.
-  bool is_loop_free(const goto_programt &goto_program);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H

src/goto-instrument/contracts/utils.cpp

@@ -10,9 +10,13 @@ Date: September 2021
 
 #include "utils.h"
 
+#include <goto-programs/cfg.h>
 #include <util/fresh_symbol.h>
+#include <util/graph.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 goto_programt::instructiont &
 add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
@@ -163,3 +167,113 @@ void disable_pointer_checks(source_locationt &source_location)
   source_location.add_pragma("disable:pointer-primitive-check");
   source_location.add_pragma("disable:pointer-overflow-check");
 }
+
+bool is_parameter_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns)
+{
+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_parameter;
+
+  return false;
+}
+
+bool is_auxiliary_decl_dead_or_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns)
+{
+  optionalt<symbol_exprt> sym = {};
+
+  // extract symbol
+  if(instruction_it->is_decl())
+    sym = instruction_it->decl_symbol();
+  else if(instruction_it->is_dead())
+    sym = instruction_it->dead_symbol();
+  else if(instruction_it->is_assign())
+  {
+    const auto &lhs = instruction_it->assign_lhs();
+    if(can_cast_expr<symbol_exprt>(lhs))
+      sym = to_symbol_expr(lhs);
+  }
+
+  // check condition
+  if(sym.has_value())
+    return ns.lookup(sym.value().get_identifier()).is_auxiliary;
+
+  return false;
+}
+
+void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_goto())
+    {
+      const auto &condition = instruction.get_condition();
+      const auto &simplified = simplify_expr(condition, ns);
+      if(simplified.is_false())
+        instruction.turn_into_skip();
+    }
+  }
+}
+
+bool is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log)
+{
+  // create cfg from instruction list
+  cfg_baset<empty_cfg_nodet> cfg;
+  cfg(goto_program);
+
+  // check that all nodes are there
+  INVARIANT(
+    goto_program.instructions.size() == cfg.size(),
+    "Instruction list vs CFG size mismatch.");
+
+  // compute SCCs
+  using idxt = graph_nodet<empty_cfg_nodet>::node_indext;
+  std::vector<idxt> node_to_scc(cfg.size(), -1);
+  auto nof_sccs = cfg.SCCs(node_to_scc);
+
+  // compute size of each SCC
+  std::vector<int> scc_size(nof_sccs, 0);
+  for(auto scc : node_to_scc)
+  {
+    INVARIANT(
+      0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
+    scc_size[scc]++;
+  }
+
+  // check they are all of size 1
+  for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
+  {
+    auto size = scc_size[scc_id];
+    if(size > 1)
+    {
+      log.error() << "Found CFG SCC with size " << size << messaget::eom;
+      for(const auto &node_id : node_to_scc)
+      {
+        if(node_to_scc[node_id] == scc_id)
+        {
+          const auto &pc = cfg[node_id].PC;
+          goto_program.output_instruction(ns, "", log.error(), *pc);
+          log.error() << messaget::eom;
+        }
+      }
+      return false;
+    }
+  }
+  return true;
+}

src/goto-instrument/contracts/utils.h

@@ -17,6 +17,8 @@ Date: September 2021
 
 #include <goto-programs/goto_model.h>
 
+#include <util/message.h>
+
 #define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
 
 /// \brief A class that overrides the low-level havocing functions in the base
@@ -125,4 +127,27 @@ const symbolt &new_tmp_symbol(
 /// Add disable pragmas for all pointer checks on the given location
 void disable_pointer_checks(source_locationt &source_location);
 
+/// Returns true iff the instruction is a `DECL x`, `DEAD x`,
+/// or `ASSIGN x := expr` where `x` has the `is_parameter` flag set.
+bool is_parameter_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns);
+
+/// Returns true iff the instruction is a `DECL x`, `DEAD x`,
+/// or `ASSIGN x := expr` where `x` has the `is_auxiliary` flag set.
+bool is_auxiliary_decl_dead_or_assign(
+  const goto_programt::targett &instruction_it,
+  namespacet &ns);
+
+/// Turns goto instructions `IF cond GOTO label` where the condition
+/// statically simplifies to `false` into SKIP instructions.
+void simplify_gotos(goto_programt &goto_program, namespacet &ns);
+
+/// Returns true iff the given program is loop-free,
+/// i.e. if each SCC of its CFG contains a single element.
+bool is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H