Detect repeated contract enforcement in goto-instrument

goto-instrument must detect when it is being invoked again when contract
enforcement has already been run as only one contract can be enforced at
a time.

Fixes: #7830

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -14,6 +14,7 @@ Date: February 2016
 #include "contracts.h"
 
 #include <util/c_types.h>
+#include <util/exception_utils.h>
 #include <util/format_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/mathematical_expr.h>
@@ -1199,16 +1200,25 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
 
 void code_contractst::enforce_contract(const irep_idt &function)
 {
-  // Add statements to the source function
-  // to ensure assigns clause is respected.
-  check_frame_conditions_function(function);
-
   // Rename source function
   std::stringstream ss;
   ss << CPROVER_PREFIX << "contracts_original_" << function;
   const irep_idt mangled(ss.str());
   const irep_idt original(function);
 
+  // Check if contract enforcement has already been applied to this function
+  if(symbol_table.has_symbol(mangled))
+  {
+    throw invalid_input_exceptiont(
+      "Contract enforcement has already been applied to function '" +
+      id2string(function) +
+      "'.\nOnly one contract may be enforced at a time per function.");
+  }
+
+  // Add statements to the source function
+  // to ensure assigns clause is respected.
+  check_frame_conditions_function(function);
+
   auto old_function = goto_functions.function_map.find(original);
   INVARIANT(
     old_function != goto_functions.function_map.end(),

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

@@ -171,6 +171,13 @@ dfcct::dfcct(
 
 void dfcct::check_transform_goto_model_preconditions()
 {
+  // Check if contract enforcement has already been applied
+  const irep_idt dfcc_map_name = "__dfcc_instrumented_functions";
+  PRECONDITION_WITH_DIAGNOSTICS(
+    !goto_model.symbol_table.has_symbol(dfcc_map_name),
+    "Contract enforcement has already been applied to this binary.\n"
+    "Only one contract may be enforced at a time.");
+
   // check that harness function exists
   PRECONDITION_WITH_DIAGNOSTICS(
     dfcc_utilst::function_symbol_with_body_exists(goto_model, harness_id),