From 9f8e2a28fcc9d4eaa58df6a5ca400bfcd88e48a9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Mar 2021 17:32:11 +0100
Subject: [PATCH] [typing] Take into account tentative defs when merging
 globals

A tentative def turned into 0-initialization can't be merged with
an explicit definition from another translation unit.
---
 src/kernel_internals/typing/frontc.ml         |  1 -
 src/kernel_internals/typing/mergecil.ml       | 15 +---
 .../oracle/tentative_definition.0.res.oracle  | 10 +++
 .../oracle/tentative_definition.1.res.oracle  | 11 +++
 .../oracle/tentative_definition.2.res.oracle  | 12 +++
 .../oracle/tentative_definition.3.res.oracle  | 12 +++
 .../oracle/tentative_definition.4.res.oracle  | 10 +++
 .../oracle/tentative_definition.5.res.oracle  |  6 ++
 .../oracle/tentative_definition.6.res.oracle  |  6 ++
 .../oracle/tentative_definition.7.res.oracle  |  6 ++
 .../oracle/tentative_definition.8.res.oracle  |  6 ++
 .../oracle/tentative_definition.9.res.oracle  |  6 ++
 tests/syntax/tentative_definition.c           | 77 +++++++++++++++++++
 tests/syntax/tentative_definition_aux.c       | 64 +++++++++++++++
 14 files changed, 230 insertions(+), 12 deletions(-)
 create mode 100644 tests/syntax/oracle/tentative_definition.0.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.1.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.2.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.3.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.4.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.5.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.6.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.7.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.8.res.oracle
 create mode 100644 tests/syntax/oracle/tentative_definition.9.res.oracle
 create mode 100644 tests/syntax/tentative_definition.c
 create mode 100644 tests/syntax/tentative_definition_aux.c

diff --git a/src/kernel_internals/typing/frontc.ml b/src/kernel_internals/typing/frontc.ml
index de9fec4dfc3..aac0b990d40 100644
--- a/src/kernel_internals/typing/frontc.ml
+++ b/src/kernel_internals/typing/frontc.ml
@@ -41,7 +41,6 @@
 (*                          et Automatique).                                *)
 (****************************************************************************)
 
-
 (* Signal that we are in MS VC mode *) (* BY: never called *)
 let setMSVCMode () =
   Cprint.msvcMode := true
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 7fe064e19d7..0da9d5eabce 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2759,20 +2759,13 @@ let oneFilePass2 (f: file) =
               (H.find emittedVarDefn vi'.vname) in
             (* previously defined; same initializer? *)
             if (equalInitOpts prevInitOpt init.init)
-            || (init.init = None) then (
+            then (
               false  (* do not emit *)
             )
-            else if prevInitOpt = None then (
-              (* The previous occurrence was only a tentative defn. Now,
-                 we have a real one. Set the correct value in the table,
-                 and tell that we need to change the previous into GVarDecl
-              *)
-              H.replace emittedVarDefn vi'.vname(vi',init.init,l);
-              replaceTentativeDefn:=true;
-              true
-            )
             else (
-              (* Both GVars have initializers. *)
+              (* Both GVars have initializers. Note that None in this
+                 context means a tentative definition turned into
+                 a default 0-initialization. *)
               Kernel.error ~current:true
                 "global var %s at %a has different initializer than %a"
                 vi'.vname
diff --git a/tests/syntax/oracle/tentative_definition.0.res.oracle b/tests/syntax/oracle/tentative_definition.0.res.oracle
new file mode 100644
index 00000000000..373498b824a
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.0.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x = 1;
+int main(void)
+{
+  return x;
+}
+
+
diff --git a/tests/syntax/oracle/tentative_definition.1.res.oracle b/tests/syntax/oracle/tentative_definition.1.res.oracle
new file mode 100644
index 00000000000..95d3d686b39
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.1.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+extern int x;
+
+int main(void)
+{
+  return x;
+}
+
+
diff --git a/tests/syntax/oracle/tentative_definition.2.res.oracle b/tests/syntax/oracle/tentative_definition.2.res.oracle
new file mode 100644
index 00000000000..db0e058c1f0
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.2.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+
+int main(void)
+{
+  return x;
+}
+
+int x = 2;
+
diff --git a/tests/syntax/oracle/tentative_definition.3.res.oracle b/tests/syntax/oracle/tentative_definition.3.res.oracle
new file mode 100644
index 00000000000..c4ca3ded89c
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.3.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+
+int main(void)
+{
+  return x;
+}
+
+int x;
+
diff --git a/tests/syntax/oracle/tentative_definition.4.res.oracle b/tests/syntax/oracle/tentative_definition.4.res.oracle
new file mode 100644
index 00000000000..b50717c0eef
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.4.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+int main(void)
+{
+  return x;
+}
+
+
diff --git a/tests/syntax/oracle/tentative_definition.5.res.oracle b/tests/syntax/oracle/tentative_definition.5.res.oracle
new file mode 100644
index 00000000000..14316d7a790
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.5.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/tentative_definition.6.res.oracle b/tests/syntax/oracle/tentative_definition.6.res.oracle
new file mode 100644
index 00000000000..14316d7a790
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.6.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/tentative_definition.7.res.oracle b/tests/syntax/oracle/tentative_definition.7.res.oracle
new file mode 100644
index 00000000000..14316d7a790
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.7.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/tentative_definition.8.res.oracle b/tests/syntax/oracle/tentative_definition.8.res.oracle
new file mode 100644
index 00000000000..14316d7a790
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.8.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/tentative_definition.9.res.oracle b/tests/syntax/oracle/tentative_definition.9.res.oracle
new file mode 100644
index 00000000000..14316d7a790
--- /dev/null
+++ b/tests/syntax/oracle/tentative_definition.9.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/tentative_definition.c (with preprocessing)
+[kernel] Parsing tests/syntax/tentative_definition_aux.c (with preprocessing)
+[kernel] tests/syntax/tentative_definition_aux.c:64: User Error: 
+  global var x at tests/syntax/tentative_definition_aux.c:64 has different initializer than tests/syntax/tentative_definition.c:75
+[kernel] User Error: error encountered during linking
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/tentative_definition.c b/tests/syntax/tentative_definition.c
new file mode 100644
index 00000000000..2d8e8726590
--- /dev/null
+++ b/tests/syntax/tentative_definition.c
@@ -0,0 +1,77 @@
+/* run.config*
+OPT: -cpp-extra-args="-DEEDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DEENN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENND" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENNN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNNN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+EXIT: 1
+OPT: -cpp-extra-args="-DEEDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DENDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNDD" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+OPT: -cpp-extra-args="-DNNDN" @PTEST_DIR@/@PTEST_NAME@_aux.c -print
+*/
+
+// OK (one global defined to 1)
+#ifdef EEDN
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef EENN
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK (one global, initialized to 2)
+#ifdef ENND
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef ENNN
+#define LINKAGE_1 extern
+#define DEF_1
+#endif
+
+// OK-ish (two defs to 0)
+#ifdef NNNN
+#define LINKAGE_1
+#define DEF_1
+#endif
+
+// KO (two conflicting defs)
+#ifdef EEDD
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDD
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDN
+#define LINKAGE_1 extern
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDD
+#define LINKAGE_1
+#define DEF_1 = 1
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDN
+#define LINKAGE_1
+#define DEF_1 = 1
+#endif
+
+LINKAGE_1 int x DEF_1;
+
+int main() { return x; }
diff --git a/tests/syntax/tentative_definition_aux.c b/tests/syntax/tentative_definition_aux.c
new file mode 100644
index 00000000000..3a94c22d140
--- /dev/null
+++ b/tests/syntax/tentative_definition_aux.c
@@ -0,0 +1,64 @@
+/* run.config*
+DONTRUN: primary test in tentative_definition.c
+*/
+
+#ifdef EEDN
+#define LINKAGE_2 extern
+#define DEF_2
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef EENN
+#define LINKAGE_2 extern
+#define DEF_2
+#endif
+
+// OK (one global, initialized to 2)
+#ifdef ENND
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// OK (one global, 0-initialized)
+#ifdef ENNN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// OK-ish (two defs to 0)
+#ifdef NNNN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// KO (two conflicting defs)
+#ifdef EEDD
+#define LINKAGE_2 extern
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDD
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef ENDN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDD
+#define LINKAGE_2
+#define DEF_2 = 2
+#endif
+
+// KO (two conflicting defs)
+#ifdef NNDN
+#define LINKAGE_2
+#define DEF_2
+#endif
+
+LINKAGE_2 int x DEF_2;
-- 
GitLab