Merge pull request #7782 from qinheping/migrate_synthesizer_utils

CONTRACTS: Move some functions from `synthesizer_utils` to `contracts/utils`

Author: qinheping

src/goto-instrument/contracts/utils.cpp

@@ -23,6 +23,7 @@ Date: September 2021
 
 #include <goto-programs/cfg.h>
 
+#include <analyses/natural_loops.h>
 #include <ansi-c/c_expr.h>
 #include <langapi/language_util.h>
 
@@ -610,3 +611,130 @@ unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
   std::string result = str.substr(first_index, last_index - first_index);
   return std::stol(result);
 }
+
+goto_programt::const_targett get_loop_end_from_loop_head_and_content(
+  const goto_programt::const_targett &loop_head,
+  const loop_templatet<
+    goto_programt::const_targett,
+    goto_programt::target_less_than> &loop)
+{
+  goto_programt::const_targett loop_end = loop_head;
+  for(const auto &t : loop)
+  {
+    // an instruction is the loop end if it is a goto instruction
+    // and it jumps backward to the loop head
+    if(
+      t->is_goto() && t->get_target() == loop_head &&
+      t->location_number > loop_end->location_number)
+      loop_end = t;
+  }
+  INVARIANT(
+    loop_head != loop_end,
+    "Could not find end of the loop starting at: " +
+      loop_head->source_location().as_string());
+
+  return loop_end;
+}
+
+goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(
+  const goto_programt::targett &loop_head,
+  const loop_templatet<goto_programt::targett, goto_programt::target_less_than>
+    &loop)
+{
+  goto_programt::targett loop_end = loop_head;
+  for(const auto &t : loop)
+  {
+    // an instruction is the loop end if it is a goto instruction
+    // and it jumps backward to the loop head
+    if(
+      t->is_goto() && t->get_target() == loop_head &&
+      t->location_number > loop_end->location_number)
+      loop_end = t;
+  }
+  INVARIANT(
+    loop_head != loop_end,
+    "Could not find end of the loop starting at: " +
+      loop_head->source_location().as_string());
+
+  return loop_end;
+}
+
+goto_programt::targett get_loop_head_or_end(
+  const unsigned int target_loop_number,
+  goto_functiont &function,
+  bool finding_head)
+{
+  natural_loops_mutablet natural_loops(function.body);
+
+  // iterate over all natural loops to find the loop with `target_loop_number`
+  for(const auto &loop_p : natural_loops.loop_map)
+  {
+    const goto_programt::targett loop_head = loop_p.first;
+    goto_programt::targett loop_end =
+      get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second);
+    // check if the current loop is the target loop by comparing loop number
+    if(loop_end->loop_number == target_loop_number)
+    {
+      if(finding_head)
+        return loop_head;
+      else
+        return loop_end;
+    }
+  }
+
+  UNREACHABLE;
+}
+
+goto_programt::targett
+get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
+{
+  return get_loop_head_or_end(target_loop_number, function, false);
+}
+
+goto_programt::targett
+get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
+{
+  return get_loop_head_or_end(target_loop_number, function, true);
+}
+
+void annotate_invariants(
+  const invariant_mapt &invariant_map,
+  goto_modelt &goto_model)
+{
+  for(const auto &invariant_map_entry : invariant_map)
+  {
+    loop_idt loop_id = invariant_map_entry.first;
+    irep_idt function_id = loop_id.function_id;
+    unsigned int loop_number = loop_id.loop_number;
+
+    // get the last instruction of the target loop
+    auto &function = goto_model.goto_functions.function_map[function_id];
+    goto_programt::targett loop_end = get_loop_end(loop_number, function);
+
+    // annotate the invariant to the condition of `loop_end`
+    loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
+      invariant_map_entry.second;
+  }
+}
+
+void annotate_assigns(
+  const std::map<loop_idt, std::set<exprt>> &assigns_map,
+  goto_modelt &goto_model)
+{
+  for(const auto &assigns_map_entry : assigns_map)
+  {
+    loop_idt loop_id = assigns_map_entry.first;
+    irep_idt function_id = loop_id.function_id;
+    unsigned int loop_number = loop_id.loop_number;
+
+    // get the last instruction of the target loop
+    auto &function = goto_model.goto_functions.function_map[function_id];
+    goto_programt::targett loop_end = get_loop_end(loop_number, function);
+
+    exprt &condition = loop_end->condition_nonconst();
+    auto assigns = exprt(ID_target_list);
+    for(const auto &e : assigns_map_entry.second)
+      assigns.add_to_operands(e);
+    condition.add(ID_C_spec_assigns) = assigns;
+  }
+}

src/goto-instrument/contracts/utils.h

@@ -14,6 +14,7 @@ Date: September 2021
 #include <goto-programs/goto_convert_class.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/loop_ids.h>
 
 #include <goto-instrument/havoc_utils.h>
 
@@ -24,6 +25,10 @@ Date: September 2021
 #define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"
 #define INIT_INVARIANT "__init_invariant"
 
+template <class T, typename C>
+class loop_templatet;
+typedef std::map<loop_idt, exprt> invariant_mapt;
+
 /// Class that allows to clean expressions of side effects and to generate
 /// havoc_slice expressions.
 class cleanert : public goto_convertt
@@ -271,4 +276,45 @@ bool is_assignment_to_instrumented_variable(
 /// Convert the suffix digits right after `prefix` of `str` into unsigned.
 unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix);
 
+/// Find the goto instruction of `loop` that jumps to `loop_head`
+goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(
+  const goto_programt::targett &loop_head,
+  const loop_templatet<goto_programt::targett, goto_programt::target_less_than>
+    &loop);
+
+goto_programt::const_targett get_loop_end_from_loop_head_and_content(
+  const goto_programt::const_targett &loop_head,
+  const loop_templatet<
+    goto_programt::const_targett,
+    goto_programt::target_less_than> &loop);
+
+/// Return loop head if `finding_head` is true,
+/// Otherwise return loop end.
+goto_programt::targett get_loop_head_or_end(
+  const unsigned int loop_number,
+  goto_functiont &function,
+  bool finding_head);
+
+/// Find and return the last instruction of the natural loop with
+/// `loop_number` in `function`. loop_end -> loop_head
+goto_programt::targett
+get_loop_end(const unsigned int loop_number, goto_functiont &function);
+
+/// Find and return the first instruction of the natural loop with
+/// `loop_number` in `function`. loop_end -> loop_head
+goto_programt::targett
+get_loop_head(const unsigned int loop_number, goto_functiont &function);
+
+/// Annotate the invariants in `invariant_map` to their corresponding
+/// loops. Corresponding loops are specified by keys of `invariant_map`
+void annotate_invariants(
+  const invariant_mapt &invariant_map,
+  goto_modelt &goto_model);
+
+/// Annotate the assigns in `assigns_map` to their corresponding
+/// loops. Corresponding loops are specified by keys of `assigns_map`
+void annotate_assigns(
+  const std::map<loop_idt, std::set<exprt>> &assigns_map,
+  goto_modelt &goto_model);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H

src/goto-synthesizer/synthesizer_utils.cpp

@@ -8,139 +8,6 @@ Author: Qinheping Hu
 
 #include "synthesizer_utils.h"
 
-#include <util/optional.h>
-
-#include <analyses/natural_loops.h>
-#include <goto-instrument/contracts/utils.h>
-#include <goto-instrument/havoc_utils.h>
-
-goto_programt::const_targett get_loop_end_from_loop_head_and_content(
-  const goto_programt::const_targett &loop_head,
-  const loop_templatet<
-    goto_programt::const_targett,
-    goto_programt::target_less_than> &loop)
-{
-  goto_programt::const_targett loop_end = loop_head;
-  for(const auto &t : loop)
-  {
-    // an instruction is the loop end if it is a goto instruction
-    // and it jumps backward to the loop head
-    if(
-      t->is_goto() && t->get_target() == loop_head &&
-      t->location_number > loop_end->location_number)
-      loop_end = t;
-  }
-  INVARIANT(
-    loop_head != loop_end,
-    "Could not find end of the loop starting at: " +
-      loop_head->source_location().as_string());
-
-  return loop_end;
-}
-
-goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(
-  const goto_programt::targett &loop_head,
-  const loop_templatet<goto_programt::targett, goto_programt::target_less_than>
-    &loop)
-{
-  goto_programt::targett loop_end = loop_head;
-  for(const auto &t : loop)
-  {
-    // an instruction is the loop end if it is a goto instruction
-    // and it jumps backward to the loop head
-    if(
-      t->is_goto() && t->get_target() == loop_head &&
-      t->location_number > loop_end->location_number)
-      loop_end = t;
-  }
-  INVARIANT(
-    loop_head != loop_end,
-    "Could not find end of the loop starting at: " +
-      loop_head->source_location().as_string());
-
-  return loop_end;
-}
-
-goto_programt::targett get_loop_head_or_end(
-  const unsigned int target_loop_number,
-  goto_functiont &function,
-  bool finding_head)
-{
-  natural_loops_mutablet natural_loops(function.body);
-
-  // iterate over all natural loops to find the loop with `target_loop_number`
-  for(const auto &loop_p : natural_loops.loop_map)
-  {
-    const goto_programt::targett loop_head = loop_p.first;
-    goto_programt::targett loop_end =
-      get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second);
-    // check if the current loop is the target loop by comparing loop number
-    if(loop_end->loop_number == target_loop_number)
-    {
-      if(finding_head)
-        return loop_head;
-      else
-        return loop_end;
-    }
-  }
-
-  UNREACHABLE;
-}
-
-goto_programt::targett
-get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
-{
-  return get_loop_head_or_end(target_loop_number, function, false);
-}
-
-goto_programt::targett
-get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
-{
-  return get_loop_head_or_end(target_loop_number, function, true);
-}
-
-void annotate_invariants(
-  const invariant_mapt &invariant_map,
-  goto_modelt &goto_model)
-{
-  for(const auto &invariant_map_entry : invariant_map)
-  {
-    loop_idt loop_id = invariant_map_entry.first;
-    irep_idt function_id = loop_id.function_id;
-    unsigned int loop_number = loop_id.loop_number;
-
-    // get the last instruction of the target loop
-    auto &function = goto_model.goto_functions.function_map[function_id];
-    goto_programt::targett loop_end = get_loop_end(loop_number, function);
-
-    // annotate the invariant to the condition of `loop_end`
-    loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
-      invariant_map_entry.second;
-  }
-}
-
-void annotate_assigns(
-  const std::map<loop_idt, std::set<exprt>> &assigns_map,
-  goto_modelt &goto_model)
-{
-  for(const auto &assigns_map_entry : assigns_map)
-  {
-    loop_idt loop_id = assigns_map_entry.first;
-    irep_idt function_id = loop_id.function_id;
-    unsigned int loop_number = loop_id.loop_number;
-
-    // get the last instruction of the target loop
-    auto &function = goto_model.goto_functions.function_map[function_id];
-    goto_programt::targett loop_end = get_loop_end(loop_number, function);
-
-    exprt &condition = loop_end->condition_nonconst();
-    auto assigns = exprt(ID_target_list);
-    for(const auto &e : assigns_map_entry.second)
-      assigns.add_to_operands(e);
-    condition.add(ID_C_spec_assigns) = assigns;
-  }
-}
-
 invariant_mapt combine_in_and_post_invariant_clauses(
   const invariant_mapt &in_clauses,
   const invariant_mapt &post_clauses,