Merge pull request #7693 from tautschnig/cleanup/nesting-graph-loopt

Cleanup the API of dfcc_loop_nesting_grapht

Author: tautschnig

src/analyses/loop_analysis.h

@@ -13,7 +13,7 @@ Author: Diffblue Ltd
 #ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
 #define CPROVER_ANALYSES_LOOP_ANALYSIS_H
 
-#include <memory>
+#include <goto-programs/goto_model.h>
 
 template <class T>
 class loop_analysist;

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

@@ -522,16 +522,15 @@ dfcc_cfg_infot::dfcc_cfg_infot(
   : function_id(function_id),
     goto_function(goto_function),
     top_level_write_set(top_level_write_set),
-    log(message_handler),
     ns(symbol_table)
 {
   dfcc_loop_nesting_grapht loop_nesting_graph;
   goto_programt &goto_program = goto_function.body;
-  messaget log(message_handler);
   if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
   {
+    messaget log(message_handler);
     dfcc_check_loop_normal_form(goto_program, log);
-    loop_nesting_graph = build_loop_nesting_graph(goto_program, log);
+    loop_nesting_graph = build_loop_nesting_graph(goto_program);
 
     const auto head = check_inner_loops_have_contracts(loop_nesting_graph);
     if(head.has_value())

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

@@ -17,7 +17,6 @@ Date: March 2023
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
 
-#include <util/message.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -33,6 +32,7 @@ Date: March 2023
 class dfcc_utilst;
 class dfcc_libraryt;
 class goto_functiont;
+class message_handlert;
 
 /// \brief Describes a single loop for the purpose of DFCC loop contract
 /// instrumentation.
@@ -297,7 +297,6 @@ class dfcc_cfg_infot
   const irep_idt &function_id;
   goto_functiont &goto_function;
   const exprt &top_level_write_set;
-  messaget log;
   const namespacet ns;
 
   /// True iff \p id is in the valid range for a loop id or is equal to

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

@@ -12,20 +12,18 @@ Date: March 2023
 
 #include "dfcc_loop_nesting_graph.h"
 
-#include <util/invariant.h>
-#include <util/message.h>
+#include <analyses/natural_loops.h>
 
 dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
   const goto_programt::targett &head,
   const goto_programt::targett &latch,
-  const loopt &instructions)
+  const loop_templatet<goto_programt::targett> &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)
+dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
 {
   natural_loops_mutablet natural_loops(goto_program);
   dfcc_loop_nesting_grapht loop_nesting_graph;

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

@@ -18,7 +18,7 @@ Date: March 2023
 
 #include <util/graph.h>
 
-#include <goto-instrument/loop_utils.h>
+#include <analyses/loop_analysis.h>
 
 class messaget;
 
@@ -29,7 +29,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
   dfcc_loop_nesting_graph_nodet(
     const goto_programt::targett &head,
     const goto_programt::targett &latch,
-    const loopt &instructions);
+    const loop_templatet<goto_programt::targett> &instructions);
 
   /// Loop head instruction
   goto_programt::targett head;
@@ -38,7 +38,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
   goto_programt::targett latch;
 
   /// Set of loop instructions
-  loopt instructions;
+  loop_templatet<goto_programt::targett> instructions;
 };
 
 typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
@@ -47,6 +47,6 @@ typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
 /// 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);
+dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);
+
 #endif