Merge pull request #7628 from remi-delmas-3000/contracts-contract-mode

CONTRACTS: add loop contract mode enum and string conversion functions

Author: remi-delmas-3000

src/goto-instrument/Makefile

@@ -19,6 +19,8 @@ SRC = accelerate/accelerate.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
+      contracts/dynamic-frames/dfcc_contract_mode.cpp \
+      contracts/dynamic-frames/dfcc_loop_contract_mode.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_contract_mode.cpp

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking for function contracts
+
+Author: Remi Delmas, delmasrd@amazon.com
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_contract_mode.h"
+
+#include <util/invariant.h>
+
+std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
+{
+  switch(mode)
+  {
+  case dfcc_contract_modet::CHECK:
+    return "dfcc_contract_modet::CHECK";
+  case dfcc_contract_modet::REPLACE:
+    return "dfcc_contract_modet::REPLACE";
+  }
+  UNREACHABLE;
+}
+
+std::ostream &operator<<(std::ostream &os, const dfcc_contract_modet mode)
+{
+  os << dfcc_contract_mode_to_string(mode);
+  return os;
+}

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

@@ -13,11 +13,17 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_MODE_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_MODE_H
 
+#include <string>
+
 /// Enum type representing the contract checking and replacement modes.
 enum class dfcc_contract_modet
 {
   CHECK,
   REPLACE
 };
 
+std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode);
+
+std::ostream &operator<<(std::ostream &os, const dfcc_contract_modet mode);
+
 #endif

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

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking for function contracts
+
+Author: Remi Delmas, delmasrd@amazon.com
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_loop_contract_mode.h"
+
+#include <util/invariant.h>
+
+dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools(
+  bool apply_loop_contracts,
+  bool unwind_transformed_loops)
+{
+  if(apply_loop_contracts)
+  {
+    if(unwind_transformed_loops)
+    {
+      return dfcc_loop_contract_modet::APPLY_UNWIND;
+    }
+    else
+    {
+      return dfcc_loop_contract_modet::APPLY;
+    }
+  }
+  else
+  {
+    return dfcc_loop_contract_modet::NONE;
+  }
+}
+
+std::string
+dfcc_loop_contract_mode_to_string(const dfcc_loop_contract_modet mode)
+{
+  switch(mode)
+  {
+  case dfcc_loop_contract_modet::NONE:
+    return "dfcc_loop_contract_modet::NONE";
+  case dfcc_loop_contract_modet::APPLY:
+    return "dfcc_loop_contract_modet::APPLY";
+  case dfcc_loop_contract_modet::APPLY_UNWIND:
+    return "dfcc_loop_contract_modet::APPLY_UNWIND";
+  }
+  UNREACHABLE;
+}
+
+std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode)
+{
+  os << dfcc_loop_contract_mode_to_string(mode);
+  return os;
+}

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

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking for function contracts
+
+Author: Remi Delmas, delmasrd@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Enumeration representing the instrumentation mode for loop contracts.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H
+
+#include <string>
+
+/// Enumeration representing the instrumentation mode for loop contracts.
+enum class dfcc_loop_contract_modet
+{
+  /// Do not apply loop contracts
+  NONE,
+  /// Apply loop contracts
+  APPLY,
+  /// Apply loop contracts and unwind the resulting base + step encoding
+  APPLY_UNWIND
+};
+
+/// Generates an enum value from boolean flags for application and unwinding.
+dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools(
+  bool apply_loop_contracts,
+  bool unwind_transformed_loops);
+
+std::string dfcc_loop_contract_mode_to_string(dfcc_loop_contract_modet mode);
+
+std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode);
+
+#endif