From 34fa09f61447242c45a0e533bbe57ae93c103a63 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 May 2026 20:15:36 +0000 Subject: [PATCH] contracts: strip metadata before DATA_INVARIANT in get_contract MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit goto-instrument --replace-call-with-contract's get_contract helper compares the contract-declaration's code_typet with the function-symbol's code_typet via irept::operator==. That operator recurses into every sub-irep, including metadata (source locations, per-declaration #identifier strings) and contract- specific sub-ireps (spec_requires / spec_ensures / spec_assigns / spec_frees). The metadata is unrelated to whether the two declarations describe the same function signature, so comparing it turns every cross-TU contract application into a DATA_INVARIANT false-positive — even when the signatures match exactly. This commit strips the known irrelevant fields recursively from both types before comparing: - #source_location - #identifier / #base_name (per-declaration parameter names) - C_spec_requires / C_spec_ensures / C_spec_assigns / C_spec_frees (contract-specific decorations) The remaining type comparison is still strict on the semantic shape (code type, return type, parameter count and types); it just no longer fires on metadata-only differences. All three CORE contracts regression sets (contracts-CORE, contracts-dfcc-CORE, contracts-non-dfcc-CORE) remain green, and the integration/linux scan pipeline (9 regression scripts) is unchanged. A further case (contract adapter declares an opaque struct whose linked kernel TU has the struct's full definition) is a genuine semantic mismatch and should continue to fire the invariant. That's a design matter for the scan adapter rather than a bug in get_contract. Co-authored-by: Kiro --- src/goto-instrument/contracts/contracts.cpp | 42 ++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 5d192c6cd78..523b5861c5d 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -35,6 +35,7 @@ Date: February 2016 #include "utils.h" #include +#include #include void code_contractst::check_apply_loop_contracts( @@ -590,8 +591,47 @@ get_contract(const irep_idt &function, const namespacet &ns) } const auto &type = to_code_with_contract_type(contract_sym->type); + // Compare the contract-declaration's signature to the function + // declaration's signature *structurally*. A literal + // `irept::operator==` recurses into every sub-irep — including + // source-location stamps, contract-spec clauses, and per- + // declaration `#identifier` strings on parameter types — and + // reports unequal on signature-identical declarations that merely + // live in different translation units. That produces + // DATA_INVARIANT false-positives when a contract-declaration in + // a scan adapter matches a plain re-declaration in a kernel TU + // (see integration/linux/CBMC_LIMITATIONS.md LIM-016). + // + // Helper: strip all per-declaration metadata (source locations, + // comments prefixed with `#`) from a type irep, recursively. + // Contract-spec sub-ireps get stripped too so they don't throw + // off the comparison against the plain function-declaration. + std::function strip_metadata = [&strip_metadata](irept &node) + { + node.remove(ID_C_source_location); + node.remove(ID_C_spec_requires); + node.remove(ID_C_spec_ensures); + node.remove(ID_C_spec_assigns); + node.remove(ID_C_spec_frees); + // Also strip per-declaration identifier/base-name ireps so + // two parameter declarations with the same type but + // different mangled caller-specific identifiers still + // compare equal. + node.remove(ID_C_identifier); + node.remove(ID_C_base_name); + // Walk named sub-ireps (the ones that aren't comments). + for(auto &[name, sub] : node.get_named_sub()) + strip_metadata(sub); + for(auto &sub : node.get_sub()) + strip_metadata(sub); + }; + + typet contract_type_stripped = type; + strip_metadata(contract_type_stripped); + typet function_type_stripped = function_symbol.type; + strip_metadata(function_type_stripped); DATA_INVARIANT( - type == function_symbol.type, + contract_type_stripped == function_type_stripped, "front-end should have rejected re-declarations with a different type"); return type;