Fix invalid assumptions and invariants in GraphML witness generation

src/goto-programs/graphml_witness.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/find_symbols.h>
 #include <util/namespace.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
@@ -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;

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