Linking: structural-equivalence-aware type comparison

regression/ansi-c/linking_conflicts2/test.desc

@@ -3,6 +3,6 @@ main.c
 other.c
 ^EXIT=(64|1)$
 ^SIGNAL=0$
-^\S+\.c(:\d+:\d+|\(\d+\)): error: conflicting function declarations 'foo'$
+^\S+\.c(:\d+:\d+|\(\d+\)): error: duplicate definition of function 'foo'$
 --
 ^warning: ignoring

regression/cbmc/Linking10/main.c

@@ -0,0 +1,16 @@
+// TU1: struct A is incomplete, struct B is complete
+struct A;
+struct B
+{
+  int y;
+};
+
+void f(struct A *a, struct B *b);
+
+int main()
+{
+  struct B b;
+  b.y = 10;
+  f((struct A *)0, &b);
+  return 0;
+}

regression/cbmc/Linking10/module.c

@@ -0,0 +1,16 @@
+// TU2: struct A is complete, struct B is incomplete
+// Param 1 (struct A *): old=incomplete, new=complete -> set_to_new=true
+// Param 2 (struct B *): old=complete, new=incomplete -> set_to_new=false
+// Without |= accumulation, replace would be false (from param 2),
+// losing the replacement needed for param 1.
+struct A
+{
+  int x;
+};
+struct B;
+
+void f(struct A *a, struct B *b)
+{
+  if(a)
+    __CPROVER_assert(a->x == 0, "a->x accessible");
+}

regression/cbmc/Linking10/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+module.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Test that the replace flag is accumulated (|=) across function parameters
+during linking. Param 1 has incomplete-to-complete struct (set_to_new=true),
+param 2 has complete-to-incomplete struct (set_to_new=false). Without |=,
+the replace flag from param 1 would be lost.

regression/cbmc/Linking11/main.c

@@ -0,0 +1,16 @@
+// TU1: struct S with member 'x'
+struct S
+{
+  int x;
+};
+
+// Function declared here, defined in module.c with a different struct S
+int g(struct S *p);
+
+int main()
+{
+  struct S s;
+  s.x = 42;
+  __CPROVER_assert(g(&s) == 42, "g returns s.x");
+  return 0;
+}

regression/cbmc/Linking11/module.c

@@ -0,0 +1,16 @@
+// TU2: a different struct S (with members x and y)
+// During linking, this struct S will be renamed because it conflicts
+// with TU1's struct S. The parameter type of g must be updated to
+// refer to TU1's struct S.
+struct S
+{
+  int x;
+  int y;
+};
+
+// Declaration matching TU1's g — parameter type refers to this TU's struct S,
+// which will be renamed during linking.
+int g(struct S *p)
+{
+  return p->x;
+}

regression/cbmc/Linking11/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+module.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Test that struct tags in function parameter types are properly updated during
+linking when the tag is renamed due to a conflict between translation units.

regression/cbmc/Linking12/main.c

@@ -0,0 +1,45 @@
+// Regression test for structural-equivalence-aware linker.
+//
+// Two translation units share the same C type `struct S`, but the irept
+// representations of `S` differ at the byte level because the inner type
+// `struct Inner` is COMPLETE in this TU and INCOMPLETE in module.c.
+// CBMC's compile-time canonicalisation bakes that completion state into
+// any anonymous-tag identifiers that transitively reference Inner; the
+// linker used to flag this as a "conflicting function declarations" warning
+// and produce 'pointer parameter types differ between declaration and
+// definition' diagnostics.
+//
+// With the structural-equivalence-aware needs_renaming_type / duplicate_
+// type_symbol pair, the linker recognises the two `struct S` types as the
+// same C type and merges them silently.
+
+struct Inner
+{
+  int payload;
+};
+
+struct S
+{
+  // Anonymous union whose synthetic tag identifier serializes Inner's
+  // completion state, making the byte-level encoding of S differ between
+  // this TU (Inner complete here) and module.c (Inner forward-declared
+  // there).
+  union
+  {
+    struct Inner *via_struct;
+    int *via_int;
+  } u;
+  int sentinel;
+};
+
+int read_sentinel(struct S *p);
+
+int main(void)
+{
+  struct Inner inner = {7};
+  struct S s;
+  s.u.via_struct = &inner;
+  s.sentinel = 42;
+  __CPROVER_assert(read_sentinel(&s) == 42, "sentinel survived linking");
+  return 0;
+}

regression/cbmc/Linking12/module.c

@@ -0,0 +1,21 @@
+// Translation unit where `struct Inner` is only forward-declared.
+// This makes anonymous-tag identifiers inside `struct S` serialize
+// differently from main.c's view, exercising the structural-equivalence
+// path of the linker.
+
+struct Inner;
+
+struct S
+{
+  union
+  {
+    struct Inner *via_struct;
+    int *via_int;
+  } u;
+  int sentinel;
+};
+
+int read_sentinel(struct S *p)
+{
+  return p->sentinel;
+}

regression/cbmc/Linking12/test.desc

@@ -0,0 +1,21 @@
+CORE
+main.c
+module.c --validate-goto-model --validate-ssa-equation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^.*conflicting (function|pointer parameter types|return types).*$
+^.*unexpected difference between type symbols.*$
+--
+Two translation units describe the same C type `struct S`, but the
+byte-level irept encoding differs because the inner type `struct Inner`
+is COMPLETE in main.c and INCOMPLETE in module.c.  Type-name
+canonicalisation propagates the completion state into anonymous-tag
+identifiers nested inside `struct S`, so the linker used to see the
+types as different and flag the function declaration as conflicting.
+
+The structural-equivalence-aware linker recognises the two types as
+the same C type, allows the link to succeed silently, and produces a
+goto model that passes --validate-goto-model.