From 5f17951ff21e62ae4433f1e25c5849c8e567b573 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 15 Mar 2022 19:44:41 +0100
Subject: [PATCH] [kernel] Fixes link issue for typedef'd struct
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
The issue was introduced in 8fa891ecc8397e6724. Apparently
`Mergecil.union` has some interesting side effects even if one of the
field list is empty 🤔
---
src/kernel_internals/typing/mergecil.ml | 213 +++++++++---------
tests/syntax/oracle/typedef_struct.res.oracle | 25 ++
tests/syntax/typedef_struct.i | 19 ++
tests/syntax/typedef_struct_2.i | 5 +
4 files changed, 155 insertions(+), 107 deletions(-)
create mode 100644 tests/syntax/oracle/typedef_struct.res.oracle
create mode 100644 tests/syntax/typedef_struct.i
create mode 100644 tests/syntax/typedef_struct_2.i
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 8b515e1324e..a120eb377d9 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1191,113 +1191,112 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
let oldfidx = oldcinode.nfidx in
let ci = cinode.ndata in
let fidx = cinode.nfidx in
-
- match oldci.cfields, ci.cfields with
- | _, None -> () (* new struct is not defined, just keep using the old one *)
- | None, Some fields ->
- (* old struct is not defined, but new one is. Use its fields. *)
- oldci.cfields <- Some fields
- | Some oldfields, Some fields ->
- let old_len = List.length oldfields in
- let len = List.length fields in
- if old_len <> len then begin
- let curLoc = CurrentLoc.get () in (* d_global blows this away.. *)
- CurrentLoc.set curLoc;
- let aggregate_name = if cstruct then "struct" else "union" in
- let msg = Printf.sprintf
- "different number of fields in %s %s and %s %s: %d != %d."
- aggregate_name oldci.cname aggregate_name ci.cname
- old_len len
- in
- raise (Failure msg)
- end;
- (* We check that they are defined in the same way. While doing this there
- * might be recursion and we have to watch for going into an infinite
- * loop. So we add the assumption that they are equal *)
- let newrep, undo = union oldcinode cinode in
- (* We check the fields but watch for Failure. We only do the check when
- * the lengths are the same. Due to the code above this the other
- * possibility is that one of the length is 0, in which case we reuse the
- * old compinfo. *)
- begin
- try
- (* must_check_offsets indicates that composite type attributes are
- different, which may impact field offsets *)
- let mustCheckOffsets =
- if equal_attributes_for_merge ci.cattr oldci.cattr then false
- else if equalModuloPackedAlign ci.cattr oldci.cattr then true
- else raise
- (Failure
- (let attrs = drop_attributes_for_merge ci.cattr in
- let oldattrs = drop_attributes_for_merge oldci.cattr in
- (* we do not use Cil_datatype.Attributes.pretty because it
- may not print some relevant attributes *)
- let pp_attrs =
- Pretty_utils.pp_list ~sep:", " Printer.pp_attribute
- in
- Format.asprintf
- "different/incompatible composite type attributes: \
- [%a] vs [%a]"
- pp_attrs attrs pp_attrs oldattrs))
- in
- List.iter2
- (fun oldf f ->
- checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
- (* Make sure the types are compatible *)
- (* Note: 6.2.7 §1 states that the names of the fields
- should be the same.
- We do not force this for now, but could do it. *)
- let newtype =
- combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
- in
- (* Change the type in the representative *)
- oldf.ftype <- newtype)
- oldfields fields
- with Failure reason ->
- (* Our assumption was wrong. Forget the isomorphism *)
- undo ();
- let fields_old =
- Format.asprintf "%a"
- Cil_printer.pp_global
- (GCompTag(oldci, Cil_datatype.Location.unknown))
- in
- let fields =
- Format.asprintf "%a"
- Cil_printer.pp_global
- (GCompTag(ci, Cil_datatype.Location.unknown))
- in
- let fullname_old = compFullName oldci in
- let fullname = compFullName ci in
- let msg =
- match fullname_old = fullname,
- fields_old = fields (* Could also use a special comparison *)
- with
- true, true ->
- Format.asprintf
- "Definitions of %s are not isomorphic. Reason follows:@\n@?%s"
- fullname_old reason
- | false, true ->
- Format.asprintf
- "%s and %s are not isomorphic. Reason follows:@\n@?%s"
- fullname_old fullname reason
- | true, false ->
- Format.asprintf
- "Definitions of %s are not isomorphic. \
- Reason follows:@\n@?%s@\n@?%s@?%s"
- fullname_old reason
- fields_old fields
- | false, false ->
- Format.asprintf
- "%s and %s are not isomorphic. \
- Reason follows:@\n@?%s@\n@?%s@?%s"
- fullname_old fullname reason
- fields_old fields
- in
- raise (Failure msg)
- end;
- (* We get here when we succeeded checking that they are equal, or one of
- * them was empty *)
- newrep.ndata.cattr <- addAttributes oldci.cattr ci.cattr
+ (* We check that they are defined in the same way. While doing this there
+ * might be recursion and we have to watch for going into an infinite
+ * loop. So we add the assumption that they are equal *)
+ let newrep, undo = union oldcinode cinode in
+ (match oldci.cfields, ci.cfields with
+ | _, None -> () (* new struct is not defined, just keep using the old one *)
+ | None, Some fields ->
+ (* old struct is not defined, but new one is. Use its fields. *)
+ oldci.cfields <- Some fields
+ | Some oldfields, Some fields ->
+ let old_len = List.length oldfields in
+ let len = List.length fields in
+ if old_len <> len then begin
+ let curLoc = CurrentLoc.get () in (* d_global blows this away.. *)
+ CurrentLoc.set curLoc;
+ let aggregate_name = if cstruct then "struct" else "union" in
+ let msg = Printf.sprintf
+ "different number of fields in %s %s and %s %s: %d != %d."
+ aggregate_name oldci.cname aggregate_name ci.cname
+ old_len len
+ in
+ raise (Failure msg)
+ end;
+ (* We check the fields but watch for Failure. We only do the check when
+ * the lengths are the same. Due to the code above this the other
+ * possibility is that one of the length is 0, in which case we reuse the
+ * old compinfo. *)
+ begin
+ try
+ (* must_check_offsets indicates that composite type attributes are
+ different, which may impact field offsets *)
+ let mustCheckOffsets =
+ if equal_attributes_for_merge ci.cattr oldci.cattr then false
+ else if equalModuloPackedAlign ci.cattr oldci.cattr then true
+ else raise
+ (Failure
+ (let attrs = drop_attributes_for_merge ci.cattr in
+ let oldattrs = drop_attributes_for_merge oldci.cattr in
+ (* we do not use Cil_datatype.Attributes.pretty because it
+ may not print some relevant attributes *)
+ let pp_attrs =
+ Pretty_utils.pp_list ~sep:", " Printer.pp_attribute
+ in
+ Format.asprintf
+ "different/incompatible composite type attributes: \
+ [%a] vs [%a]"
+ pp_attrs attrs pp_attrs oldattrs))
+ in
+ List.iter2
+ (fun oldf f ->
+ checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
+ (* Make sure the types are compatible *)
+ (* Note: 6.2.7 §1 states that the names of the fields
+ should be the same.
+ We do not force this for now, but could do it. *)
+ let newtype =
+ combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
+ in
+ (* Change the type in the representative *)
+ oldf.ftype <- newtype)
+ oldfields fields
+ with Failure reason ->
+ (* Our assumption was wrong. Forget the isomorphism *)
+ undo ();
+ let fields_old =
+ Format.asprintf "%a"
+ Cil_printer.pp_global
+ (GCompTag(oldci, Cil_datatype.Location.unknown))
+ in
+ let fields =
+ Format.asprintf "%a"
+ Cil_printer.pp_global
+ (GCompTag(ci, Cil_datatype.Location.unknown))
+ in
+ let fullname_old = compFullName oldci in
+ let fullname = compFullName ci in
+ let msg =
+ match fullname_old = fullname,
+ fields_old = fields (* Could also use a special comparison *)
+ with
+ true, true ->
+ Format.asprintf
+ "Definitions of %s are not isomorphic. Reason follows:@\n@?%s"
+ fullname_old reason
+ | false, true ->
+ Format.asprintf
+ "%s and %s are not isomorphic. Reason follows:@\n@?%s"
+ fullname_old fullname reason
+ | true, false ->
+ Format.asprintf
+ "Definitions of %s are not isomorphic. \
+ Reason follows:@\n@?%s@\n@?%s@?%s"
+ fullname_old reason
+ fields_old fields
+ | false, false ->
+ Format.asprintf
+ "%s and %s are not isomorphic. \
+ Reason follows:@\n@?%s@\n@?%s@?%s"
+ fullname_old fullname reason
+ fields_old fields
+ in
+ raise (Failure msg)
+ end);
+ (* We get here when we succeeded checking that they are equal, or one of
+ * them was empty *)
+ newrep.ndata.cattr <- addAttributes oldci.cattr ci.cattr
end
(* Match two enuminfos and throw a Failure if they do not match *)
diff --git a/tests/syntax/oracle/typedef_struct.res.oracle b/tests/syntax/oracle/typedef_struct.res.oracle
new file mode 100644
index 00000000000..8beec1c4be5
--- /dev/null
+++ b/tests/syntax/oracle/typedef_struct.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing typedef_struct_2.i (no preprocessing)
+[kernel] Parsing typedef_struct.i (no preprocessing)
+[kernel] Parsing typedef_struct_2.i (no preprocessing)
+/* Generated by Frama-C */
+typedef struct foo foo;
+struct foo {
+ int y ;
+};
+foo *f(int x);
+
+extern foo *alloc(void);
+
+foo *f(int x)
+{
+ foo *__retres;
+ foo *f_0 = alloc();
+ if (f_0->y == x) {
+ __retres = (foo *)0;
+ goto return_label;
+ }
+ __retres = f_0;
+ return_label: return __retres;
+}
+
+
diff --git a/tests/syntax/typedef_struct.i b/tests/syntax/typedef_struct.i
new file mode 100644
index 00000000000..f376bbaa6a2
--- /dev/null
+++ b/tests/syntax/typedef_struct.i
@@ -0,0 +1,19 @@
+/* run.config
+OPT: %{dep:typedef_struct_2.i} @PTEST_FILE@ %{dep:typedef_struct_2.i} -print
+*/
+typedef struct foo foo;
+extern foo *alloc(void);
+
+foo* f(int x);
+
+struct foo
+{
+ int y;
+};
+
+foo* f(int x)
+{
+ foo* f = alloc();
+ if (f->y == x) return 0;
+ return f;
+ }
diff --git a/tests/syntax/typedef_struct_2.i b/tests/syntax/typedef_struct_2.i
new file mode 100644
index 00000000000..507ac9cd505
--- /dev/null
+++ b/tests/syntax/typedef_struct_2.i
@@ -0,0 +1,5 @@
+/* run.config
+ DONTRUN: main test is in typedef_struct.i
+*/
+typedef struct foo foo;
+foo* f(int);
--
GitLab