From 6f45e4502698bb0715976a8f366a267816274398 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 21:10:13 +0100 Subject: [PATCH] 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 --- src/goto-instrument/contracts/contracts.cpp | 18 ++++++++++++++---- .../contracts/dynamic-frames/dfcc.cpp | 7 +++++++ 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 046bc714e97..04d9beef9fc 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -14,6 +14,7 @@ Date: February 2016 #include "contracts.h" #include +#include #include #include #include @@ -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(), diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 1403b04f403..03982924804 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/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),