From 6520856e1f6e425da1bd2b144ecc968993ff2bcb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 25 Mar 2020 18:05:46 +0100
Subject: [PATCH] [Instantiate] Ignore nested unions in memset

---
 src/plugins/instantiate/string/memset.ml      | 16 ++++---
 .../tests/string/memset_nested_union.c        | 11 +++++
 .../oracle/memset_nested_union.res.oracle     | 45 +++++++++++++++++++
 3 files changed, 67 insertions(+), 5 deletions(-)
 create mode 100644 src/plugins/instantiate/tests/string/memset_nested_union.c
 create mode 100644 src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle

diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 7c2bc6ce40c..d597bd3a452 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -183,13 +183,19 @@ let memset_value e =
   | Const(CInt64(ni, _, _)) when Integer.equal ni ff -> Some 255
   | _ -> None
 
-let is_union_type = function
-  | TComp({ cstruct = false }, _, _) -> true
+let rec contains_union_type t =
+  match Cil.unrollType t with
+  | TComp({ cstruct = false }, _, _) ->
+    true
+  | TComp({ cfields = fields }, _, _) ->
+    List.exists contains_union_type (List.map (fun f -> f.ftype) fields)
+  | TArray(t, _, _, _) ->
+    contains_union_type t
   | _ -> false
 
 let well_typed_call _ret = function
   | [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
-  | [ ptr ; _ ; _ ] when is_union_type (type_from_arg ptr) -> false
+  | [ ptr ; _ ; _ ] when contains_union_type (type_from_arg ptr) -> false
   | [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
   | [ _ ; value ; _ ] ->
     begin match memset_value value with
@@ -201,7 +207,7 @@ let well_typed_call _ret = function
 let key_from_call _ret = function
   | [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) ->
     (type_from_arg ptr), None
-  | [ ptr ; value ; _ ] when not (is_union_type (type_from_arg ptr)) ->
+  | [ ptr ; value ; _ ] when not (contains_union_type (type_from_arg ptr)) ->
     (type_from_arg ptr), (memset_value value)
   | _ -> failwith "Call to Memset.key_from_call on an ill-typed call"
 
@@ -226,7 +232,7 @@ let generate_prototype = function
     let name = function_name ^ "_" ^ (string_of_typ t) in
     let fun_type = char_prototype t in
     name, fun_type
-  | t, Some x when not (is_union_type t) && (x = 0 || x = 255) ->
+  | t, Some x when not (contains_union_type t) && (x = 0 || x = 255) ->
     let ext = if x = 0 then "_0" else if x = 255 then "_FF" else assert false in
     let name = function_name ^ "_" ^ (string_of_typ t) ^ ext in
     let fun_type = non_char_prototype t in
diff --git a/src/plugins/instantiate/tests/string/memset_nested_union.c b/src/plugins/instantiate/tests/string/memset_nested_union.c
new file mode 100644
index 00000000000..ea236b94e15
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/memset_nested_union.c
@@ -0,0 +1,11 @@
+#include <string.h>
+
+union U {
+  int x ;
+  unsigned y ;
+};
+struct X { union U u ; };
+void test() {
+  struct X x;
+  memset(&x, 0, sizeof(x));
+}
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
new file mode 100644
index 00000000000..99b6125cfd4
--- /dev/null
+++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
@@ -0,0 +1,45 @@
+[kernel] Parsing tests/string/memset_nested_union.c (with preprocessing)
+[instantiate] tests/string/memset_nested_union.c:10: Warning: 
+  Ignore call: not well typed
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+union U {
+   int x ;
+   unsigned int y ;
+};
+struct X {
+   union U u ;
+};
+void test(void)
+{
+  struct X x;
+  memset((void *)(& x),0,sizeof(x));
+  return;
+}
+
+
+[kernel] Parsing tests/string/result/memset_nested_union.c (with preprocessing)
+[kernel] Parsing tests/string/memset_nested_union.c (with preprocessing)
+[kernel] tests/string/memset_nested_union.c:8: Warning: 
+  dropping duplicate def'n of func test at tests/string/memset_nested_union.c:8 in favor of that at tests/string/result/memset_nested_union.c:12
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
+union U {
+   int x ;
+   unsigned int y ;
+};
+struct X {
+   union U u ;
+};
+void test(void)
+{
+  struct X x;
+  memset((void *)(& x),0,sizeof(x));
+  return;
+}
+
+
-- 
GitLab