Get wf to accept unions for Fulminate

lib/check.ml

@@ -2436,7 +2436,11 @@ let record_tagdefs tagDefs =
   PmapM.iterM
     (fun tag def ->
        match def with
-       | Mu.UnionDef -> unsupported (Loc.other __LOC__) !^"todo: union types"
+       | Mu.UnionDef ->
+         if !Sym.executable_spec_enabled then
+           return ()
+         else
+           unsupported (Loc.other __LOC__) !^"todo: union types"
        | StructDef layout -> Global.add_struct_decl tag layout)
     tagDefs
 
@@ -2446,7 +2450,11 @@ let check_tagdefs tagDefs =
     (fun _tag def ->
        let open Memory in
        match def with
-       | Mu.UnionDef -> unsupported (Loc.other __LOC__) !^"todo: union types"
+       | Mu.UnionDef ->
+         if !Sym.executable_spec_enabled then
+           return ()
+         else
+           unsupported (Loc.other __LOC__) !^"todo: union types"
        | StructDef layout ->
          let@ _ =
            ListM.fold_rightM

lib/coreTypeChecks.ml

@@ -41,7 +41,13 @@ let check_against_core_bt core_bt cn_bt =
       let@ () = check_object_type (OTy_integer, param_t) in
       check_object_type (t, t2)
     | OTy_struct tag, BT.Struct tag2 when Sym.equal tag tag2 -> return ()
-    | OTy_union _tag, _ -> fail (Pp.string "unsupported: union types")
+    | (OTy_union _tag as core_obj_ty), bt ->
+      if !Sym.executable_spec_enabled then (
+        match bt with
+        | Map (_, Option MemByte) -> return ()
+        | _ -> mismatch (BTy_object core_obj_ty) bt)
+      else
+        fail (Pp.string "unsupported: union types")
     | OTy_floating, _ -> fail (Pp.string "unsupported: floats")
     | core_obj_ty, bt -> mismatch (BTy_object core_obj_ty) bt
   in

lib/core_to_mucore.ml

@@ -1488,7 +1488,11 @@ let normalise_tag_definition tag (loc, def) =
     ->
     unsupported loc !^"flexible array members"
   | StructDef (fields, None) -> return (Mu.StructDef (make_struct_decl loc fields tag))
-  | UnionDef _l -> unsupported loc !^"union types"
+  | UnionDef _l ->
+    if !Sym.executable_spec_enabled then
+      return Mu.UnionDef
+    else
+      unsupported loc !^"union types"
 
 
 let normalise_tag_definitions tagDefs =

lib/sctypes.ml

@@ -158,7 +158,7 @@ let rec to_ctype (ct_ : ctype) =
   Ctype ([], ct_)
 
 
-let rec of_ctype (Ctype.Ctype (_, ct_)) =
+let rec of_ctype (Ctype.Ctype (_, ct_) as ct) =
   let open Option in
   match ct_ with
   | Ctype.Void -> return Void
@@ -189,7 +189,13 @@ let rec of_ctype (Ctype.Ctype (_, ct_)) =
   | Ctype.Atomic _ -> None
   | Ctype.Struct s -> return (Struct s)
   | Byte -> return Byte
-  | Union _ -> fail
+  | Union _ ->
+    let int_of_ival iv = Z.to_int (Option.get (Mem.eval_integer_value iv)) in
+    let size = int_of_ival (Impl_mem.sizeof_ival ct) in
+    if !Sym.executable_spec_enabled then
+      return (Array (Byte, Some size))
+    else
+      fail
 
 
 let of_ctype_unsafe loc ct =

lib/wellTyped.ml

@@ -1735,16 +1735,33 @@ module BaseTyping = struct
         | PEapply_fun (fname, pes) ->
           let@ bt, pes = check_infer_apply_fun None fname pes pe in
           return (bt, PEapply_fun (fname, pes))
-        | PEconstrained _
-        | PEunion (_, _, _)
+        | PEconstrained _ -> todo ()
+        | PEunion (tag, member, pe) ->
+          if !Sym.executable_spec_enabled then (
+            (* todo: make this proper when CN actually supports unions *)
+            let ct = Option.get (Sctypes.of_ctype (CF.Ctype.Ctype ([], Union tag))) in
+            let@ () = WCT.is_ct loc ct in
+            let@ pe = infer_pexpr pe in
+            return (Memory.bt_of_sct ct, PEunion (tag, member, pe)))
+          else
+            fail
+              { loc; msg = Generic !^"unsupported: union types" } [@alert "-deprecated"]
         | PEmemberof (_, _, _)
         | PEconv_int (_, _)
         | PEconv_loaded_int (_, _)
         (* reaching these cases should be prevented by the `is_unreachable` used in
            inferring types of PEif *)
-        | PEerror (_, _)
-        | PEundef (_, _) ->
+        | PEerror (_, _) ->
           todo ()
+        | PEundef (loc, ub) ->
+          if !Sym.executable_spec_enabled then
+            (* in the case of a well-formedness check when labels are not inlined
+             *      run ret_label ( undef(<<UB088_reached_end_of_function>>)))
+             * we may need to infer an type for PEundef, which in the absence of
+             * polymorphism is arbitrarily to Unit below *)
+            return (Unit, PEundef (loc, ub))
+          else
+            todo ()
       in
       return (Pexpr (loc, annots, bty, pe_))
 
@@ -2346,44 +2363,47 @@ module BaseTyping = struct
           let bts = List.map bt_of_expr es in
           return (Tuple bts, Eunseq es)
         | Erun (l, pes) ->
-          (* copying from check.ml *)
-          let@ lt, _lkind =
-            match Sym.Map.find_opt l label_context with
-            | None ->
-              fail
-                { loc;
-                  msg =
-                    Generic (!^"undefined code label" ^/^ Sym.pp l) [@alert "-deprecated"]
-                }
-            | Some (lt, lkind, _) -> return (lt, lkind)
-          in
-          let@ pes =
-            let wrong_number_computational_args () =
-              let has = List.length pes in
-              let expect = AT.count_computational lt in
-              fail { loc; msg = Number_arguments { type_ = `Computational; has; expect } }
-            in
-            let wrong_number_ghost_args () =
-              let has = 0 in
-              let expect = AT.count_ghost lt in
-              fail { loc; msg = Number_arguments { type_ = `Ghost; has; expect } }
-            in
-            let rec check_args acc_pes lt pes =
-              Pp.debug 1 (lazy (Pp.item __FUNCTION__ (AT.pp (fun _ -> Pp.empty) lt)));
-              match (lt, pes) with
-              | AT.Computational ((_s, bt), _info, lt'), pe :: pes' ->
-                let@ pe = check_pexpr bt pe in
-                check_args (acc_pes @ [ pe ]) lt' pes'
-              | AT.L _lat, [] -> return acc_pes
-              | AT.Computational _, [] | AT.L _, _ :: _ ->
-                wrong_number_computational_args ()
-              | AT.Ghost _, _ -> wrong_number_ghost_args ()
-            in
-            (* TODO: fix duplication wrt Check.check_expr, cf.
+          (match Sym.Map.find_opt l label_context with
+           | None ->
+             if !Sym.executable_spec_enabled then
+               let@ pes = ListM.mapM infer_pexpr pes in
+               return (Unit, Erun (l, pes))
+             else (* copying from check.ml *)
+               fail
+                 { loc;
+                   msg =
+                     Generic (!^"undefined code label" ^/^ Sym.pp l)
+                     [@alert "-deprecated"]
+                 }
+           | Some (lt, _lkind, _) ->
+             let@ pes =
+               let wrong_number_computational_args () =
+                 let has = List.length pes in
+                 let expect = AT.count_computational lt in
+                 fail
+                   { loc; msg = Number_arguments { type_ = `Computational; has; expect } }
+               in
+               let wrong_number_ghost_args () =
+                 let has = 0 in
+                 let expect = AT.count_ghost lt in
+                 fail { loc; msg = Number_arguments { type_ = `Ghost; has; expect } }
+               in
+               let rec check_args acc_pes lt pes =
+                 Pp.debug 1 (lazy (Pp.item __FUNCTION__ (AT.pp (fun _ -> Pp.empty) lt)));
+                 match (lt, pes) with
+                 | AT.Computational ((_s, bt), _info, lt'), pe :: pes' ->
+                   let@ pe = check_pexpr bt pe in
+                   check_args (acc_pes @ [ pe ]) lt' pes'
+                 | AT.L _lat, [] -> return acc_pes
+                 | AT.Computational _, [] | AT.L _, _ :: _ ->
+                   wrong_number_computational_args ()
+                 | AT.Ghost _, _ -> wrong_number_ghost_args ()
+               in
+               (* TODO: fix duplication wrt Check.check_expr, cf.
                      https://github.com/rems-project/cn/issues/210 *)
-            check_args [] lt pes
-          in
-          return (Unit, Erun (l, pes))
+               check_args [] lt pes
+             in
+             return (Unit, Erun (l, pes)))
         | CN_progs (surfaceprog, cnprogs) ->
           let@ cnprogs = ListM.mapM (check_cnprog check_cn_statement) cnprogs in
           return (Unit, CN_progs (surfaceprog, cnprogs))

tests/cn/unsupported_union.error.c.verify

@@ -1,4 +1 @@
-return code: 2
-tests/cn/unsupported_union.error.c:1:1: error: unsupported union types
-union union_test {
-~~~~~~^~~~~~~~~~~~ 
+return code: 0