Merge pull request #7631 from remi-delmas-3000/contracts-loop-nesting-graph

CONTRACTS: represent loop nesting structure as a graph

Author: remi-delmas-3000

src/goto-instrument/Makefile

@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
       call_sequences.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
+      contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \

src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp

@@ -0,0 +1,86 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_loop_nesting_graph.h"
+
+#include <util/invariant.h>
+#include <util/message.h>
+
+dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
+  const goto_programt::targett &head,
+  const goto_programt::targett &latch,
+  const loopt &instructions)
+  : head(head), latch(latch), instructions(instructions)
+{
+}
+
+/// \pre Loop normal form properties must hold.
+dfcc_loop_nesting_grapht
+build_loop_nesting_graph(goto_programt &goto_program, messaget &log)
+{
+  natural_loops_mutablet natural_loops(goto_program);
+  dfcc_loop_nesting_grapht loop_nesting_graph;
+  // Add a node per natural loop
+  for(auto &loop : natural_loops.loop_map)
+  {
+    auto loop_head = loop.first;
+    auto &loop_instructions = loop.second;
+
+    if(loop_instructions.size() <= 1)
+    {
+      // ignore single instruction loops of the form
+      // LOOP: goto LOOP;
+      continue;
+    }
+
+    // Find the instruction that jumps back to `loop_head` and has the
+    // highest GOTO location number, define it as the latch.
+    auto loop_latch = loop_head;
+    for(const auto &t : loop_instructions)
+    {
+      if(
+        t->is_goto() && t->get_target() == loop_head &&
+        t->location_number > loop_latch->location_number)
+        loop_latch = t;
+    }
+
+    DATA_INVARIANT(loop_latch != loop_head, "Natural loop latch is found");
+
+    loop_nesting_graph.add_node(loop_head, loop_latch, loop_instructions);
+  }
+
+  // Add edges to the graph, pointing from inner loop to outer loops.
+  // An `inner` will be considered nested in `outer` iff both its head
+  // and latch instructions are instructions of `outer`.
+  for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
+  {
+    const auto &outer_instructions = loop_nesting_graph[outer].instructions;
+
+    for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
+    {
+      if(inner == outer)
+        continue;
+
+      if(outer_instructions.contains(loop_nesting_graph[inner].head))
+      {
+        loop_nesting_graph.add_edge(inner, outer);
+      }
+    }
+  }
+
+  auto topsorted_size = loop_nesting_graph.topsort().size();
+  INVARIANT(
+    topsorted_size == loop_nesting_graph.size(),
+    "loop_nesting_graph must be acyclic");
+
+  return loop_nesting_graph;
+}

src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+/// Builds a graph describing how loops are nested in a GOTO program.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H
+
+#include <util/graph.h>
+
+#include <goto-instrument/loop_utils.h>
+
+class messaget;
+
+/// A graph node that stores information about a natural loop.
+struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
+{
+public:
+  dfcc_loop_nesting_graph_nodet(
+    const goto_programt::targett &head,
+    const goto_programt::targett &latch,
+    const loopt &instructions);
+
+  /// Loop head instruction
+  goto_programt::targett head;
+
+  /// Loop latch instruction
+  goto_programt::targett latch;
+
+  /// Set of loop instructions
+  loopt instructions;
+};
+
+typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
+
+/// \brief Builds a graph instance describing the nesting structure of natural
+/// loops in the given \p goto_program.
+/// A loop is considered nested in an outer loop if its head and its latch are
+/// both found in the instructions of the outer loop.
+dfcc_loop_nesting_grapht
+build_loop_nesting_graph(goto_programt &goto_program, messaget &log);
+#endif