Add C11 generic to Cabs and CIL

Partially cherry-picked from ad69b97.

Author: coslu

src/cil.ml

@@ -277,6 +277,7 @@ and typ =
 
   | TBuiltin_va_list of attributes
             (** This is the same as the gcc's type with the same name *)
+  | TDefault
 
 (** Various kinds of integers *)
 and ikind =
@@ -537,6 +538,7 @@ and exp =
                           * It is not printed. Given an lval of type
                           * [TArray(T)] produces an expression of type
                           * [TPtr(T)]. *)
+  | Generic of exp * ((typ * exp) list)
 
 
 (** Literal constants *)
@@ -1526,6 +1528,7 @@ let rec typeAttrs = function
   | TEnum (enum, a) -> addAttributes enum.eattr a
   | TFun (_, _, _, a) -> a
   | TBuiltin_va_list a -> a
+  | TDefault -> []
 
 
 let setTypeAttrs t a =
@@ -1540,6 +1543,7 @@ let setTypeAttrs t a =
   | TEnum (enum, _) -> TEnum (enum, a)
   | TFun (r, args, v, _) -> TFun(r,args,v,a)
   | TBuiltin_va_list _ -> TBuiltin_va_list a
+  | TDefault -> TDefault
 
 
 let typeAddAttributes a0 t =
@@ -1562,6 +1566,7 @@ begin
       | TComp (comp, a) -> TComp (comp, add a)
       | TNamed (t, a) -> TNamed (t, add a)
       | TBuiltin_va_list a -> TBuiltin_va_list (add a)
+      | TDefault -> TDefault
 end
 
 let typeRemoveAttributes (anl: string list) t =
@@ -1577,6 +1582,7 @@ let typeRemoveAttributes (anl: string list) t =
   | TComp (comp, a) -> TComp (comp, drop a)
   | TNamed (t, a) -> TNamed (t, drop a)
   | TBuiltin_va_list a -> TBuiltin_va_list (drop a)
+  | TDefault -> TDefault
 
 let unrollType (t: typ) : typ =
   let rec withAttrs (al: attributes) (t: typ) : typ =
@@ -1857,6 +1863,7 @@ let getParenthLevel (e: exp) =
 
   | Lval(Var _, NoOffset) -> 0        (* Plain variables *)
   | Const _ -> 0                        (* Constants *)
+  | Generic _ -> 0 (*TODO*)
 
 
 let getParenthLevelAttrParam (a: attrparam) =
@@ -1953,6 +1960,7 @@ let rec typeOf (e: exp) : typ =
         TArray (t,_, a) -> TPtr(t, a)
      | _ -> E.s (E.bug "typeOf: StartOf on a non-array")
   end
+  | Generic (e, lst) -> match lst with (t, e1) :: rest -> typeOf e1 | _ -> voidType (* TODO: implement properly *)
 
 and typeOfInit (i: init) : typ =
   match i with
@@ -2242,6 +2250,7 @@ let rec alignOf_int t =
 
     | TFun _ as t -> raise (SizeOfError ("function", t))
     | TVoid _ as t -> raise (SizeOfError ("void", t))
+    | TDefault -> raise (SizeOfError ("default", t))
   in
   match filterAttributes "aligned" (typeAttrs t) with
     [] ->
@@ -2554,6 +2563,7 @@ and bitsSizeOf t =
       0
 
   | TFun _ -> raise (SizeOfError ("function", t))
+  | TDefault -> raise (SizeOfError("default", t))
 
 
 and addTrailing nrbits roundto =
@@ -2821,6 +2831,8 @@ let rec isConstant = function
   | AddrOf (Mem e, off) | StartOf(Mem e, off)
         -> isConstant e && isConstantOffset off
   | AddrOfLabel _ -> true
+  | Generic _ -> false (*TODO*)
+
 and isConstantOffset = function
     NoOffset -> true
   | Field(fi, off) -> isConstantOffset off
@@ -3524,6 +3536,14 @@ class defaultCilPrinterClass : cilPrinter = object (self)
 
     | StartOf(lv) -> self#pLval () lv
 
+    | Generic(e, lst) -> 
+        let rec print_generic_exp l doc =
+          match l with
+          | [] -> doc
+          | (t, e1) :: rest -> print_generic_exp rest (doc ++ text ", " ++ (self#pType None () t) ++ text ":" ++ self#pExp () e1)
+        in
+        text "_Generic(" ++ self#pExp () e ++ print_generic_exp lst nil ++ text ")"
+
   (* Print an expression, given the precedence of the context in which it
    * appears. *)
   method private pExpPrec (contextprec: int) () (e: exp) =
@@ -4460,6 +4480,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
        ++ self#pAttrs () a
         ++ text " "
         ++ name
+  | TDefault -> text "default"
 
 
   (**** PRINTING ATTRIBUTES *********)
@@ -4795,6 +4816,7 @@ class plainCilPrinterClass =
        end
    | TBuiltin_va_list a ->
        dprintf "TBuiltin_va_list(%a)" self#pAttrs a
+   | TDefault -> dprintf "TDefault"
 
 
   (* Some plain pretty-printers. Unlike the above these expose all the
@@ -4873,6 +4895,13 @@ class plainCilPrinterClass =
   | StartOf lv -> dprintf "StartOf(%a)" self#pLval lv
   | AddrOf (lv) -> dprintf "AddrOf(%a)" self#pLval lv
   | AddrOfLabel (sref) -> dprintf "AddrOfLabel(%a)" self#pStmt !sref
+  | Generic(e, lst) -> 
+      let rec print_generic_exp l doc =
+        match l with
+        | [] -> doc
+        | (t, e1) :: rest -> print_generic_exp rest (doc ++ text "," ++ (self#pType None () t) ++ text ":" ++ self#pExp () e1)
+      in
+      text "_Generic(" ++ self#pExp () e ++ text "," ++ print_generic_exp lst nil
 
 
 
@@ -5386,6 +5415,8 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
   | StartOf lv ->
       let lv' = vLval lv in
       if lv' != lv then StartOf lv' else e
+  | Generic(e, lst) -> e (*TODO*)
+
 
 and visitCilInit (vis: cilVisitor) (forglob: varinfo)
                  (atoff: offset) (i: init) : init =
@@ -6170,6 +6201,7 @@ let rec typeSigWithAttrs ?(ignoreSign=false) doattr t =
       TSFun(typeSig rt, (Util.list_map_opt (fun (_, atype, _) -> (typeSig atype)) args), isva, doattr a)
   | TNamed(t, a) -> typeSigAddAttrs (doattr a) (typeSig t.ttype)
   | TBuiltin_va_list al -> TSBase (TBuiltin_va_list (doattr al))
+  | TDefault -> TSBase (TDefault)
 
 let typeSig t =
   typeSigWithAttrs (fun al -> al) t

src/cil.mli

@@ -242,6 +242,7 @@ and typ =
 
   | TBuiltin_va_list of attributes
             (** This is the same as the gcc's type with the same name *)
+  | TDefault
 
 (**
  There are a number of functions for querying the kind of a type. These are
@@ -631,6 +632,7 @@ and exp =
      * not sure which one to use. In C this operation is implicit, the
      * [StartOf] operator is not printed. We have it in CIL because it makes
      * the typing rules simpler. *)
+  | Generic of exp * ((typ * exp) list)
 
 (** {b Constants.} *)
 

src/frontc/cabs.ml

@@ -80,6 +80,7 @@ type typeSpecifier = (* Merge all specifiers into one type *)
   | Tenum of string * enum_item list option * attribute list
   | TtypeofE of expression                      (* GCC __typeof__ *)
   | TtypeofT of specifier * decl_type       (* GCC __typeof__ *)
+  | Tdefault
 
 and storage =
     NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
@@ -281,6 +282,7 @@ and expression =
   | MEMBEROFPTR of expression * string
   | GNU_BODY of block
   | EXPR_PATTERN of string     (* pattern variable, and name *)
+  | GENERIC of expression * ((specifier * expression) list)
 
 and constant =
   | CONST_INT of string   (* the textual representation *)

src/frontc/cabs2cil.ml

@@ -1569,6 +1569,7 @@ let cabsTypeAddAttributes a0 t =
           | TComp (comp, a) -> TComp (comp, addA0To a)
           | TNamed (t, a) -> TNamed (t, addA0To a)
           | TBuiltin_va_list a -> TBuiltin_va_list (addA0To a)
+          | TDefault -> TDefault
   end
 
 
@@ -2458,6 +2459,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
     | [A.Tfloat128] -> TFloat(FLongDouble, []) (* TODO: Correct? *)
 
      (* Now the other type specifiers *)
+    | [A.Tdefault] -> TDefault
     | [A.Tnamed n] -> begin
         if n = "__builtin_va_list" &&
           !Machdep.theMachine.Machdep.__builtin_va_list then begin
@@ -4844,6 +4846,26 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
 
     | A.EXPR_PATTERN _ -> E.s (E.bug "EXPR_PATTERN in cabs2cil input")
 
+    | A.GENERIC (expr, lst) -> 
+        let get_exp tupel = match tupel with _, e, _ -> e in
+        let exp = get_exp (doExp false expr (AExp None)) in
+        let rec make_cil_list cabs_l cil_l = match cabs_l with 
+          | [] -> cil_l
+          | (s, e) :: rest -> make_cil_list rest (((doOnlyType s JUSTBASE),get_exp (doExp false e (AExp None))) :: cil_l) 
+        in
+        let cil_list = make_cil_list lst [] in
+        let exp_typ = typeOf exp in
+        let default_typ = ref voidType in
+        let typ = 
+          let rec get_typ l = match l with 
+            | (TDefault, e) :: rest -> default_typ := typeOf e; get_typ rest
+            | (t, e) :: rest -> if t = exp_typ then typeOf e else get_typ rest
+            | [] -> !default_typ
+          in
+          get_typ cil_list
+        in
+        finishExp empty (Generic(exp, (make_cil_list lst []))) typ
+
   with e when continueOnError -> begin
     (*ignore (E.log "error in doExp (%s)" (Printexc.to_string e));*)
     E.hadErrors := true;

src/frontc/cabsvisit.ml

@@ -538,6 +538,7 @@ and childrenExpression vis e =
       let b' = visitCabsBlock vis b in
       if b' != b then GNU_BODY b' else e
   | EXPR_PATTERN _ -> e
+  | GENERIC _ -> e (*TODO*)
 
 and visitCabsInitExpression vis (ie: init_expression) : init_expression =
   doVisit vis vis#vinitexpr childrenInitExpression ie

src/frontc/clexer.mll

@@ -225,6 +225,7 @@ let init_lexicon _ =
                          THREAD loc
                        else
                          IDENT ("__thread", loc));
+      ("_Generic", fun loc -> GENERIC loc);
     ]
 
 (* Mark an identifier as a type name. The old mapping is preserved and will

src/frontc/cparser.mly

@@ -257,6 +257,7 @@ let transformOffsetOf (speclist, dtype) member =
 %token EOF
 %token<Cabs.cabsloc> CHAR INT BOOL DOUBLE FLOAT VOID INT64 INT32
 %token<Cabs.cabsloc> INT128 FLOAT128 COMPLEX /* C99 */
+%token<Cabs.cabsloc> GENERIC /* C11 */
 %token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
 %token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
 %token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
@@ -475,8 +476,19 @@ primary_expression:                     /*(* 6.5.1. *)*/
      /*(* Next is Scott's transformer *)*/
 |               AT_EXPR LPAREN IDENT RPAREN         /* expression pattern variable */
                          { EXPR_PATTERN(fst $3), $1 }
+|   GENERIC LPAREN assignment_expression COMMA generic_assoc_list RPAREN {GENERIC ((fst $3), $5), $1}
 ;
 
+/* (specifier, expression) list */
+generic_assoc_list: 
+| generic_association {[$1]}
+| generic_assoc_list COMMA generic_association {$3 :: $1}
+
+/* specifier, expression */
+generic_association:
+| type_name COLON assignment_expression {fst $1, fst $3}
+| DEFAULT COLON assignment_expression {[SpecType(Tdefault)], fst $3}
+
 postfix_expression:                     /*(* 6.5.2 *)*/
 |               primary_expression
                         { $1 }