From f7cc40cefc8e3258c91fa7c456db3392b8cf45c6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Dec 2025 11:49:15 +0000 Subject: [PATCH] Fix invalid assumptions and invariants in GraphML witness generation - Remove assumptions with `__CPROVER_initialize` scope - Filter out assumptions for internal variables of external functions - Remove assumptions referencing out-of-scope local variables Co-authored-by: Kiro autonomous agent Fixes: #5264 --- src/goto-programs/graphml_witness.cpp | 132 ++++++++++++++++++++++---- src/xmllang/graphml.cpp | 10 +- 2 files changed, 119 insertions(+), 23 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 239922a2ab3..de63c417c5e 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include #include @@ -274,6 +275,64 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) return false; } +/// Check if a function is external (has no body or is marked extern) +static bool +is_function_extern(const namespacet &ns, const irep_idt &function_id) +{ + const symbolt *symbol_ptr = nullptr; + if(ns.lookup(function_id, symbol_ptr)) + return false; // symbol not found + + // Check if the symbol is marked as extern + if(symbol_ptr->is_extern) + return true; + + // Check if it's a function type but has no value (no body) + if(symbol_ptr->type.id() == ID_code && symbol_ptr->value.is_nil()) + return true; + + return false; +} + +/// Check if all symbols in an expression are in scope for a given function +static bool all_symbols_in_scope( + const namespacet &ns, + const exprt &expr, + const irep_idt &function_id) +{ + // Get all symbols in the expression + find_symbols_sett symbols; + find_symbols(expr, symbols); + + for(const auto &symbol_id : symbols) + { + // Skip CPROVER internal symbols - they're "global" + if(id2string(symbol_id).find(CPROVER_PREFIX) != std::string::npos) + continue; + + const symbolt *symbol_ptr = nullptr; + if(ns.lookup(symbol_id, symbol_ptr)) + continue; // symbol not found, skip + + // Check if it's a local variable (contains "::") + std::string symbol_str = id2string(symbol_id); + std::string::size_type scope_sep = symbol_str.find("::"); + + if(scope_sep != std::string::npos) + { + // Extract the function part of the identifier + std::string symbol_function = symbol_str.substr(0, scope_sep); + + // Check if it matches the expected function scope + if(symbol_function != id2string(function_id)) + return false; // Variable from different function scope + } + // Global variables (no ::) are always in scope + } + + return true; +} + /// counterexample witness void graphml_witnesst::operator()(const goto_tracet &goto_trace) { @@ -460,30 +519,44 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) to_multi_ary_expr(it->full_lhs_value).op0().get(ID_value)), "INVALID-"))) { - xmlt &val = edge.new_element("data"); - val.set_attribute("key", "assumption"); + // Check if this is from an external function or has out-of-scope vars + const bool is_extern = is_function_extern(ns, it->function_id); code_assignt assign{it->full_lhs, it->full_lhs_value}; - val.data = convert_assign_rec(lhs_id, assign); + const bool all_in_scope = + all_symbols_in_scope(ns, assign.lhs(), it->function_id) && + all_symbols_in_scope(ns, assign.rhs(), it->function_id); - if(!it->function_id.empty()) + // Skip assumptions for external functions or out-of-scope variables + if(!is_extern && all_in_scope) { - xmlt &val_s = edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - irep_idt function_id = it->function_id; - const symbolt *symbol_ptr = nullptr; - if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter) + xmlt &val = edge.new_element("data"); + val.set_attribute("key", "assumption"); + + val.data = convert_assign_rec(lhs_id, assign); + + // Only add assumption.scope if function_id is not __CPROVER_initialize + if( + !it->function_id.empty() && + it->function_id != "__CPROVER_initialize") { - function_id = lhs_id.substr(0, lhs_id.find("::")); + xmlt &val_s = edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + irep_idt function_id = it->function_id; + const symbolt *symbol_ptr = nullptr; + if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter) + { + function_id = lhs_id.substr(0, lhs_id.find("::")); + } + val_s.data = id2string(function_id); } - val_s.data = id2string(function_id); - } - if(has_prefix(val.data, "\\result =")) - { - xmlt &val_f = edge.new_element("data"); - val_f.set_attribute("key", "assumption.resultfunction"); - val_f.data = id2string(it->function_id); + if(has_prefix(val.data, "\\result =")) + { + xmlt &val_f = edge.new_element("data"); + val_f.set_attribute("key", "assumption.resultfunction"); + val_f.data = id2string(it->function_id); + } } } } @@ -636,10 +709,29 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) { irep_idt identifier = it->ssa_lhs.get_object_name(); - graphml[to].has_invariant = true; + // Check if this is from an external function or has out-of-scope vars + const bool is_extern = is_function_extern(ns, it->source.function_id); + code_assignt assign(it->ssa_lhs, it->ssa_rhs); - graphml[to].invariant = convert_assign_rec(identifier, assign); - graphml[to].invariant_scope = id2string(it->source.function_id); + const bool all_in_scope = + all_symbols_in_scope(ns, assign.lhs(), it->source.function_id) && + all_symbols_in_scope(ns, assign.rhs(), it->source.function_id); + + // Skip invariants for external functions or out-of-scope variables + if(!is_extern && all_in_scope) + { + graphml[to].has_invariant = true; + graphml[to].invariant = convert_assign_rec(identifier, assign); + + // Only add invariant.scope if function_id is not empty and not __CPROVER_initialize + if( + !it->source.function_id.empty() && + it->source.function_id != "__CPROVER_initialize") + { + graphml[to].invariant_scope = id2string(it->source.function_id); + } + // else: leave invariant_scope empty for __CPROVER_initialize or empty function_id + } } graphml[to].in[from].xml_node = edge; diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 0df4bf16267..4a6b66346ab 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -531,9 +531,13 @@ bool write_graphml(const graphmlt &src, std::ostream &os) val.set_attribute("key", "invariant"); val.data=n.invariant; - xmlt &val_s=node.new_element("data"); - val_s.set_attribute("key", "invariant.scope"); - val_s.data=n.invariant_scope; + // Only add invariant.scope if it's not empty + if(!n.invariant_scope.empty()) + { + xmlt &val_s = node.new_element("data"); + val_s.set_attribute("key", "invariant.scope"); + val_s.data = n.invariant_scope; + } } for(graphmlt::edgest::const_iterator