CONTRACTS: loop info tagging utility functions

Utility functions for loop contracts instrumentation,
allowing to tag GOTO instructions with loop identifiers
and loop instruction type.

Author: Remi Delmas

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_tags.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \

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

@@ -0,0 +1,130 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_loop_tags.h"
+
+#define ID_LOOP_ID "loop-id"
+#define ID_LOOP_HEAD "loop-head"
+#define ID_LOOP_BODY "loop-body"
+#define ID_LOOP_LATCH "loop-latch"
+#define ID_LOOP_EXITING "loop-exiting"
+#define ID_LOOP_TOP_LEVEL "loop-top-level"
+
+void dfcc_set_loop_id(
+  goto_programt::instructiont &instruction,
+  const std::size_t loop_id)
+{
+  instruction.source_location_nonconst().set(ID_LOOP_ID, loop_id);
+}
+
+optionalt<std::size_t>
+dfcc_get_loop_id(const goto_programt::instructiont &instruction)
+{
+  if(instruction.source_location().get(ID_LOOP_ID).empty())
+    return {};
+
+  return instruction.source_location().get_size_t(ID_LOOP_ID);
+}
+
+bool dfcc_has_loop_id(
+  const goto_programt::instructiont &instruction,
+  std::size_t loop_id)
+{
+  auto loop_id_opt = dfcc_get_loop_id(instruction);
+  return loop_id_opt.has_value() && loop_id_opt.value() == loop_id;
+}
+
+static void
+dfcc_set_loop_tag(goto_programt::instructiont &instruction, const irep_idt &tag)
+{
+  instruction.source_location_nonconst().set(tag, true);
+}
+
+static bool has_loop_tag(
+  const goto_programt::instructiont &instruction,
+  const irep_idt &tag)
+{
+  return instruction.source_location().get_bool(tag);
+}
+
+void dfcc_set_loop_head(goto_programt::instructiont &instruction)
+{
+  dfcc_set_loop_tag(instruction, ID_LOOP_HEAD);
+}
+
+bool dfcc_is_loop_head(const goto_programt::instructiont &instruction)
+{
+  return has_loop_tag(instruction, ID_LOOP_HEAD);
+}
+
+void dfcc_set_loop_body(goto_programt::instructiont &instruction)
+{
+  dfcc_set_loop_tag(instruction, ID_LOOP_BODY);
+}
+
+bool dfcc_is_loop_body(const goto_programt::instructiont &instruction)
+{
+  return has_loop_tag(instruction, ID_LOOP_BODY);
+}
+
+void dfcc_set_loop_exiting(goto_programt::instructiont &instruction)
+{
+  dfcc_set_loop_tag(instruction, ID_LOOP_EXITING);
+}
+
+bool dfcc_is_loop_exiting(const goto_programt::instructiont &instruction)
+{
+  return has_loop_tag(instruction, ID_LOOP_EXITING);
+}
+
+void dfcc_set_loop_latch(goto_programt::instructiont &instruction)
+{
+  dfcc_set_loop_tag(instruction, ID_LOOP_LATCH);
+}
+
+bool dfcc_is_loop_latch(const goto_programt::instructiont &instruction)
+{
+  return has_loop_tag(instruction, ID_LOOP_LATCH);
+}
+
+void dfcc_set_loop_top_level(goto_programt::instructiont &instruction)
+{
+  dfcc_set_loop_tag(instruction, ID_LOOP_TOP_LEVEL);
+}
+
+bool dfcc_is_loop_top_level(const goto_programt::instructiont &instruction)
+{
+  return has_loop_tag(instruction, ID_LOOP_TOP_LEVEL);
+}
+
+void dfcc_remove_loop_tags(goto_programt &goto_program)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    dfcc_remove_loop_tags(instruction);
+  }
+}
+
+void dfcc_remove_loop_tags(goto_programt::instructiont &instruction)
+{
+  dfcc_remove_loop_tags(instruction.source_location_nonconst());
+}
+
+void dfcc_remove_loop_tags(source_locationt &source_location)
+{
+  source_location.remove(ID_LOOP_ID);
+  source_location.remove(ID_LOOP_HEAD);
+  source_location.remove(ID_LOOP_BODY);
+  source_location.remove(ID_LOOP_EXITING);
+  source_location.remove(ID_LOOP_LATCH);
+  source_location.remove(ID_LOOP_TOP_LEVEL);
+}

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

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+/// Functions that allow to tag GOTO instructions with loop identifiers and
+/// loop instruction type: head, body, exiting, latch.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
+
+#include <goto-programs/goto_program.h>
+
+void dfcc_set_loop_id(
+  goto_programt::instructiont &instruction,
+  std::size_t loop_id);
+
+bool dfcc_has_loop_id(
+  const goto_programt::instructiont &instruction,
+  std::size_t loop_id);
+
+optionalt<std::size_t>
+dfcc_get_loop_id(const goto_programt::instructiont &instruction);
+
+void dfcc_set_loop_head(goto_programt::instructiont &instruction);
+bool dfcc_is_loop_head(const goto_programt::instructiont &instruction);
+
+void dfcc_set_loop_body(goto_programt::instructiont &instruction);
+bool dfcc_is_loop_body(const goto_programt::instructiont &instruction);
+
+void dfcc_set_loop_exiting(goto_programt::instructiont &instruction);
+bool dfcc_is_loop_exiting(const goto_programt::instructiont &instruction);
+
+void dfcc_set_loop_latch(goto_programt::instructiont &instruction);
+bool dfcc_is_loop_latch(const goto_programt::instructiont &instruction);
+
+void dfcc_set_loop_top_level(goto_programt::instructiont &instruction);
+bool dfcc_is_loop_top_level(const goto_programt::instructiont &instruction);
+
+void dfcc_remove_loop_tags(goto_programt &goto_program);
+void dfcc_remove_loop_tags(goto_programt::instructiont &instruction);
+void dfcc_remove_loop_tags(source_locationt &source_location);
+#endif