Fix three-way-merge to be field-sensitive with --vsd-structs every-field

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/main.c

@@ -0,0 +1,40 @@
+#include <assert.h>
+
+struct s
+{
+  int x;
+  int y;
+};
+
+struct s global;
+int alsoGlobal;
+
+void f00(void)
+{
+  global.x = 0;
+}
+
+int main(int argc, char **argv)
+{
+  global.x = 1;
+  global.y = 1;
+  alsoGlobal = 1;
+
+  f00();
+
+  assert(global.x == 0);
+  assert(global.y == 1);
+  assert(alsoGlobal == 1);
+
+  global.x = 2;
+  global.y = 2;
+  alsoGlobal = 2;
+
+  f00();
+
+  assert(global.x == 0);
+  assert(global.y == 2);
+  assert(alsoGlobal == 2);
+
+  return 0;
+}

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --vsd --three-way-merge --vsd-structs every-field
+^\[main.assertion.1\] line \d+ assertion global.x == 0: SUCCESS$
+^\[main.assertion.2\] line \d+ assertion global.y == 1: SUCCESS$
+^\[main.assertion.3\] line \d+ assertion alsoGlobal == 1: SUCCESS$
+^\[main.assertion.4\] line \d+ assertion global.x == 0: SUCCESS$
+^\[main.assertion.5\] line \d+ assertion global.y == 2: SUCCESS$
+^\[main.assertion.6\] line \d+ assertion alsoGlobal == 2: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -13,6 +13,7 @@ Date: April 2016
 #include <util/cprover_prefix.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/std_expr.h>
 #include <util/symbol_table_base.h>
 
 #include <algorithm>
@@ -416,6 +417,90 @@ bool variable_sensitivity_domaint::ignore_function_call_transform(
          ignored_internal_function.cend();
 }
 
+// Helper function to recursively collect all modified sub-paths within an
+// object
+static void collect_modified_paths(
+  const abstract_object_pointert &start_value,
+  const abstract_object_pointert &end_value,
+  const exprt &base_expr,
+  std::vector<exprt> &modified_paths,
+  const abstract_environmentt &env,
+  const namespacet &ns)
+{
+  // If the objects themselves are different at this level
+  if(start_value->has_been_modified(end_value))
+  {
+    // Check if this is a struct or array that we should descend into
+    const typet &obj_type = start_value->type();
+
+    if(obj_type.id() == ID_struct || obj_type.id() == ID_struct_tag)
+    {
+      // Get the struct type
+      const struct_typet &struct_type =
+        obj_type.id() == ID_struct
+          ? to_struct_type(obj_type)
+          : ns.follow_tag(to_struct_tag_type(obj_type));
+
+      // Track if any field was modified
+      bool any_field_modified = false;
+
+      // Check each field
+      for(const auto &component : struct_type.components())
+      {
+        member_exprt member_expr(
+          base_expr, component.get_name(), component.type());
+
+        abstract_object_pointert start_field =
+          start_value->expression_transform(
+            member_expr, {start_value}, env, ns);
+        abstract_object_pointert end_field =
+          end_value->expression_transform(member_expr, {end_value}, env, ns);
+
+        // Recursively check if this field was modified
+        if(start_field->has_been_modified(end_field))
+        {
+          any_field_modified = true;
+
+          // Check if this field is also a struct/array - if so, descend
+          // recursively
+          const typet &field_type = start_field->type();
+          if(
+            field_type.id() == ID_struct || field_type.id() == ID_struct_tag ||
+            field_type.id() == ID_array)
+          {
+            // Recursively descend
+            collect_modified_paths(
+              start_field, end_field, member_expr, modified_paths, env, ns);
+          }
+          else
+          {
+            // It's a leaf field (not struct/array), add it
+            modified_paths.push_back(member_expr);
+          }
+        }
+      }
+
+      // If no field-specific modifications were found but the struct was marked
+      // as modified, fall back to updating the whole struct
+      if(!any_field_modified)
+      {
+        modified_paths.push_back(base_expr);
+      }
+    }
+    else if(obj_type.id() == ID_array)
+    {
+      // For arrays, we can't enumerate all possible indices
+      // So we fall back to marking the entire array as modified
+      modified_paths.push_back(base_expr);
+    }
+    else
+    {
+      // It's a simple value type that was modified
+      modified_paths.push_back(base_expr);
+    }
+  }
+}
+
 void variable_sensitivity_domaint::merge_three_way_function_return(
   const ai_domain_baset &function_start,
   const ai_domain_baset &function_end,
@@ -431,19 +516,42 @@ void variable_sensitivity_domaint::merge_three_way_function_return(
     abstract_environmentt::modified_symbols(
       cast_function_start.abstract_state, cast_function_end.abstract_state);
 
-  std::vector<symbol_exprt> modified_symbols;
-  modified_symbols.reserve(modified_symbol_names.size());
-  std::transform(
-    modified_symbol_names.begin(),
-    modified_symbol_names.end(),
-    std::back_inserter(modified_symbols),
-    [&ns](const irep_idt &id) { return ns.lookup(id).symbol_expr(); });
-
-  for(const auto &symbol : modified_symbols)
+  for(const auto &symbol_name : modified_symbol_names)
   {
-    abstract_object_pointert value =
+    symbol_exprt symbol = ns.lookup(symbol_name).symbol_expr();
+
+    abstract_object_pointert function_start_value =
+      cast_function_start.abstract_state.eval(symbol, ns);
+    abstract_object_pointert function_end_value =
       cast_function_end.abstract_state.eval(symbol, ns);
-    abstract_state.assign(symbol, value, ns);
+
+    // Collect all modified sub-paths (fields/elements) within this symbol
+    std::vector<exprt> modified_paths;
+    collect_modified_paths(
+      function_start_value,
+      function_end_value,
+      symbol,
+      modified_paths,
+      cast_function_start.abstract_state,
+      ns);
+
+    // Apply updates only for the modified paths
+    if(modified_paths.empty())
+    {
+      // No specific sub-paths found, update the whole symbol
+      // This happens for non-struct/non-array types
+      abstract_state.assign(symbol, function_end_value, ns);
+    }
+    else
+    {
+      // Update only the modified sub-paths
+      for(const auto &path : modified_paths)
+      {
+        abstract_object_pointert value =
+          cast_function_end.abstract_state.eval(path, ns);
+        abstract_state.assign(path, value, ns);
+      }
+    }
   }
 
   return;