Merge pull request #48 from goblint/c11-generic

Add C11 generic support

Author: michael-schwarz

CHANGES

@@ -2,6 +2,7 @@
 * Add ends to locations, allowing for ranges.
 * Add additional expression locations to statements, etc.
 * Drop all support for MSVC
+* Add C11 `_Generic` support.
 
 ## Older versions
 

Makefile.in

@@ -190,7 +190,6 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "  alignof_fun: int;       (* Alignment of function *)" >> $@
 	@echo "  alignof_aligned: int;   (* Alignment of anything with the \"aligned\" attribute *)" >> $@
 	@echo "  char_is_unsigned: bool; (* Whether \"char\" is unsigned *)">> $@
-	@echo "  const_string_literals: bool; (* Whether string literals have const chars *)">> $@
 	@echo "  little_endian: bool; (* whether the machine is little endian *)">>$@
 	@echo "  __thread_is_keyword: bool; (* whether __thread is a keyword *)">>$@
 	@echo "  __builtin_va_list: bool; (* whether __builtin_va_list is builtin (gccism) *)">>$@
@@ -286,7 +285,7 @@ clean: $(CILLYDIR)/Makefile
 
 .PHONY: test
 test:
-	cd test; CC=@CC@ ./testcil -r --regrtest || { cat cil.log; exit 1; }
+	cd test; CC=@CC@ ./testcil -r --regrtest || { echo "Check test/cil.log for raw output"; exit 1; }
 
 ########################################################################
 

doc/cil.tex

@@ -1851,7 +1851,7 @@ \subsection{Specifying a machine model}
   short=2,2 int=4,4 long=8,8 long_long=8,8 pointer=8,8 enum=4,4
   float=4,4 double=8,8 long_double=16,16 void=1 bool=1,1 fun=1,1
   alignof_string=1 max_alignment=16 size_t=unsigned_long 
-  wchar_t=int char_signed=true const_string_literals=true 
+  wchar_t=int char_signed=true 
   big_endian=false __thread_is_keyword=true 
   __builtin_va_list=true underscore_name=true
 \end{verbatim}

src/check.ml

@@ -208,6 +208,7 @@ let typeSigIgnoreConst (t : typ) : typsig =
   let attrFilter (attr : attribute) : bool =
     match attr with
       | Attr ("const", []) -> false
+      | Attr ("pconst", []) -> false
       | _ -> true
   in
   typeSigWithAttrs (List.filter attrFilter) t

src/cil.ml

@@ -1276,8 +1276,8 @@ let charType = TInt(IChar, [])
 let boolType = TInt(IBool, [])
 
 let charPtrType = TPtr(charType,[])
-let charConstPtrType = TPtr(TInt(IChar, [Attr("const", [])]),[])
-let stringLiteralType = ref charPtrType
+let charConstPtrType = TPtr(TInt(IChar, [Attr("const", []); Attr("pconst", [])]),[])
+let stringLiteralType = charPtrType
 
 let voidPtrType = TPtr(voidType, [])
 let intPtrType = TPtr(intType, [])
@@ -1523,6 +1523,18 @@ let rec typeAttrs = function
   | TFun (_, _, _, a) -> a
   | TBuiltin_va_list a -> a
 
+(** [typeAttrs], which doesn't add inner attributes. *)
+let typeAttrsOuter = function
+  | TVoid a -> a
+  | TInt (_, a) -> a
+  | TFloat (_, a) -> a
+  | TNamed (_, a) -> a
+  | TPtr (_, a) -> a
+  | TArray (_, _, a) -> a
+  | TComp (_, a) -> a
+  | TEnum (_, a) -> a
+  | TFun (_, _, _, a) -> a
+  | TBuiltin_va_list a -> a
 
 let setTypeAttrs t a =
   match t with
@@ -1574,6 +1586,19 @@ let typeRemoveAttributes (anl: string list) t =
   | TNamed (t, a) -> TNamed (t, drop a)
   | TBuiltin_va_list a -> TBuiltin_va_list (drop a)
 
+(** Partition attributes into type qualifiers and non type qualifiers. *)
+let partitionQualifierAttributes al =
+  List.partition (function
+      | Attr (("const" | "volatile" | "restrict"), []) -> true
+      | _ -> false
+    ) al
+
+(** Remove top-level type qualifiers from type. *)
+let removeOuterQualifierAttributes t =
+  let a = typeAttrsOuter t in
+  let (_, a') = partitionQualifierAttributes a in
+  setTypeAttrs t a'
+
 let unrollType (t: typ) : typ =
   let rec withAttrs (al: attributes) (t: typ) : typ =
     match t with
@@ -1910,7 +1935,7 @@ let rec typeOf (e: exp) : typ =
     (* The type of a string is a pointer to characters ! The only case when
      * you would want it to be an array is as an argument to sizeof, but we
      * have SizeOfStr for that *)
-  | Const(CStr s) -> !stringLiteralType
+  | Const(CStr s) -> stringLiteralType
 
   | Const(CWStr s) -> TPtr(!wcharType,[])
 
@@ -2149,11 +2174,7 @@ let rec getInteger (e:exp) : cilint option =
       let mkInt ik n = Some (fst (truncateCilint ik n)) in
       match unrollType t, getInteger e with
       | TInt (ik, _), Some n -> mkInt ik n
-      | TPtr _, Some n -> begin
-	  match !upointType with
-	    TInt (ik, _) -> mkInt ik n
-	  | _ -> raise (Failure "pointer size unknown")
-        end
+      (* "integer constant expressions" may not cast to ptr *)
       | TEnum (ei, _), Some n -> mkInt ei.ekind n
       | TFloat _, v -> v
       | _, _ -> None
@@ -2671,9 +2692,12 @@ let isArrayType t =
 
 (** 6.3.2.3 subsection 3
  *  An integer constant expr with value 0, or such an expr cast to void *, is called a null pointer constant. *)
-let isNullPtrConstant = function
-  | CastE(TPtr(TVoid _,_), e) -> isZero @@ constFold true e
-  | e -> isZero @@ constFold true e
+let isNullPtrConstant e =
+  let rec isNullPtrConstant = function
+    | CastE (TPtr (TVoid [], []), e) -> isNullPtrConstant e (* no qualifiers allowed on void or ptr *)
+    | e -> isZero e
+  in
+  isNullPtrConstant (constFold true e)
 
 let rec isConstant = function
   | Const _ -> true
@@ -2798,7 +2822,7 @@ let initGccBuiltins () : unit =
   let ulongLongType = TInt(IULongLong, []) in
   let floatType = TFloat(FFloat, []) in
   let longDoubleType = TFloat (FLongDouble, []) in
-  let voidConstPtrType = TPtr(TVoid [Attr ("const", [])], []) in
+  let voidConstPtrType = TPtr(TVoid [Attr ("const", []); Attr ("pconst", [])], []) in
   let sizeType = !typeOfSizeOf in
   let v4sfType = TFloat (FFloat,[Attr("__vector_size__", [AInt 16])]) in
 
@@ -4176,7 +4200,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
 
     | TArray (elemt, lo, a) ->
         (* ignore the const attribute for arrays *)
-        let a' = dropAttributes [ "const" ] a in
+        let a' = dropAttributes [ "pconst" ] a in
         let name' =
           if a' == [] then name else
           if nameOpt == None then printAttributes a' else
@@ -4241,7 +4265,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
   method pAttr (Attr(an, args): attribute) : doc * bool =
     (* Recognize and take care of some known cases *)
     match an, args with
-      "const", [] -> text "const", false
+      "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
+    | "pconst", [] -> text "const", false (* pconst means print const *)
           (* Put the aconst inside the attribute list *)
     | "complex", [] when !c99Mode -> text "_Complex", false
     | "complex", [] -> text "__complex__", false
@@ -4805,7 +4830,7 @@ let makeVarinfo global name ?init typ =
     { vname = name;
       vid   = newVID ();
       vglob = global;
-      vtype = if global then typ else typeRemoveAttributes ["const"] typ;
+      vtype = if global then typ else typeRemoveAttributes ["pconst"] typ;
       vdecl = lu;
       vinit = {init=init};
       vinline = false;
@@ -6712,11 +6737,6 @@ let initCIL () =
         Some machine -> M.theMachine := machine
       | None -> M.theMachine := M.gcc
     end;
-    (* Pick type for string literals *)
-    stringLiteralType := if !M.theMachine.M.const_string_literals then
-      charConstPtrType
-    else
-      charPtrType;
     (* Find the right ikind given the size *)
     let findIkindSz (unsigned: bool) (sz: int) : ikind =
       try

src/cil.mli

@@ -1332,6 +1332,9 @@ val charType: typ
 (** char * *)
 val charPtrType: typ
 
+(** Type of string literals *)
+val stringLiteralType: typ
+
 (** wchar_t (depends on architecture) and is set when you call
  * {!Cil.initCIL}. *)
 val wcharKind: ikind ref
@@ -1799,6 +1802,9 @@ val hasAttribute: string -> attributes -> bool
     of the type structure, in case of composite, enumeration and named types *)
 val typeAttrs: typ -> attribute list
 
+(** [typeAttrs], which doesn't add inner attributes. *)
+val typeAttrsOuter: typ -> attribute list
+
 val setTypeAttrs: typ -> attributes -> typ (* Resets the attributes *)
 
 
@@ -1811,6 +1817,13 @@ val typeAddAttributes: attribute list -> typ -> typ
 val typeRemoveAttributes: string list -> typ -> typ
 
 
+(** Partition attributes into type qualifiers and non type qualifiers. *)
+val partitionQualifierAttributes: attribute list -> attribute list * attribute list
+
+(** Remove top-level type qualifiers from type. *)
+val removeOuterQualifierAttributes: typ -> typ
+
+
 (** Convert an expression into an attrparam, if possible. Otherwise raise
     NotAnAttrParam with the offending subexpression *)
 val expToAttrParam: exp -> attrparam

src/frontc/cabs.ml

@@ -83,6 +83,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 (** "default" in generic associations *)
 
 and storage =
     NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
@@ -280,6 +281,7 @@ and expression =
   | MEMBEROFPTR of expression * string
   | GNU_BODY of block
   | EXPR_PATTERN of string     (* pattern variable, and name *)
+  | GENERIC of expression * (((specifier * decl_type) * expression) list)
 
 and constant =
   | CONST_INT of string   (* the textual representation *)

src/frontc/cabs2cil.ml

@@ -603,11 +603,7 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo =
  * a struct we must recursively strip the "const" from fields and array
  * elements. *)
 let rec stripConstLocalType (t: typ) : typ =
-  let dc a =
-    if hasAttribute "const" a then
-      dropAttribute "const" a
-    else a
-  in
+  let dc = dropAttribute "pconst" in
   match t with
   | TPtr (bt, a) ->
       (* We want to be able to detect by pointer equality if the type has
@@ -1570,7 +1566,16 @@ type combineWhat =
  * that are known to be equal *)
 let isomorphicStructs : (string * string, bool) H.t = H.create 15
 
+(** Construct the composite type of [oldt] and [t] if they are compatible.
+    Raise [Failure] if they are incompatible. *)
 let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
+  let (oldq, olda) = partitionQualifierAttributes (typeAttrsOuter oldt) in
+  let (q, a) = partitionQualifierAttributes (typeAttrsOuter t) in
+  if oldq <> q then
+    raise (Failure "different type qualifiers")
+  else if q <> [] then
+    cabsTypeAddAttributes q (combineTypes what (setTypeAttrs oldt olda) (setTypeAttrs t a))
+  else
   match oldt, t with
   | TVoid olda, TVoid a -> TVoid (cabsAddAttributes olda a)
   | TInt (oldik, olda), TInt (ik, a) ->
@@ -1743,7 +1748,7 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
                    combineTypes
                      (if what = CombineFundef then
                        CombineFunarg else CombineOther)
-                     ot' at
+                     (removeOuterQualifierAttributes ot') (removeOuterQualifierAttributes at)
                  in
                  let a = addAttributes oa aa in
                  (n, t, a))
@@ -1883,19 +1888,33 @@ let conditionalConversion (t2: typ) (t3: typ) (e2: exp option) (e3:exp) : typ =
         arithmeticConversion t2 t3
     | TComp (comp2,_), TComp (comp3,_), _
           when comp2.ckey = comp3.ckey -> t2
-    | TPtr(_, _), TPtr(TVoid _, _), _ ->
-      if isNullPtrConstant e3 then t2 else t3
-    | TPtr(TVoid _, _), TPtr(_, _), Some e2' ->
-      if isNullPtrConstant e2' then t3 else t2
+    | TVoid [], TVoid [], _ -> TVoid [] (* TODO: what about qualifiers? standard says nothing *)
+    | TPtr(_, _), _, _ when isNullPtrConstant e3 -> t2
+    | _, TPtr(_, _), Some e2' when isNullPtrConstant e2' -> t3
+    | TPtr(b2, _), TPtr(TVoid _ as b3, _), _
+    | TPtr(TVoid _ as b2, _), TPtr(b3, _), _ ->
+        let a2 = typeAttrsOuter b2 in
+        let a3 = typeAttrsOuter b3 in
+        let (q2, _) = partitionQualifierAttributes a2 in
+        let (q3, _) = partitionQualifierAttributes a3 in
+        let q = cabsAddAttributes q2 q3 in
+        TPtr (TVoid q, [])
     | TPtr _, TPtr _, _ when Util.equals (typeSig t2) (typeSig t3) -> t2
-    | TPtr _, TInt _, _  -> t2 (* most likely comparison with int constant 0, if it isn't it would not be valid C *)
-    | TInt _, TPtr _, _ -> t3 (* most likely comparison with int constant 0, if it isn't it would not be valid C *)
+    | TPtr _, TInt _, _  -> t2 (* not "null pointer constant", not allowed by standard, works in gcc/clang with warning *)
+    | TInt _, TPtr _, _ -> t3 (* not "null pointer constant", not allowed by standard, works in gcc/clang with warning *)
 
           (* When we compare two pointers of different type, we combine them
            * using the same algorithm when combining multiple declarations of
            * a global *)
-    | (TPtr _) as t2', (TPtr _ as t3'), _ -> begin
-        try combineTypes CombineOther t2' t3'
+    | TPtr (b2, _), TPtr (b3, _), _ -> begin
+        try
+          let a2 = typeAttrsOuter b2 in
+          let a3 = typeAttrsOuter b3 in
+          let (q2, a2') = partitionQualifierAttributes a2 in
+          let (q3, a3') = partitionQualifierAttributes a3 in
+          let b = combineTypes CombineOther (setTypeAttrs b2 a2') (setTypeAttrs b2 a3') in
+          let q = cabsAddAttributes q2 q3 in
+          TPtr (cabsTypeAddAttributes q b, [])
         with Failure msg -> begin
           ignore (warn "A.QUESTION: %a does not match %a (%s)"
                     d_type (unrollType t2) d_type (unrollType t3) msg);
@@ -2443,6 +2462,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] -> E.s (error "Default outside generic associations")
     | [A.Tnamed n] -> begin
         if n = "__builtin_va_list" &&
           !Machdep.theMachine.Machdep.__builtin_va_list then begin
@@ -2629,7 +2649,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
   match src with
   | [] -> []
-  | CV_CONST    :: tl -> ("const",[])    :: (convertCVtoAttr tl)
+  | CV_CONST    :: tl -> ("const",[]) :: ("pconst",[])    :: (convertCVtoAttr tl)
   | CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
   | CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
   | CV_COMPLEX  :: tl -> ("complex",[]) ::  (convertCVtoAttr tl)
@@ -4798,6 +4818,35 @@ 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 (e, al) ->
+        let is_default = function
+          | ([SpecType Tdefault], JUSTBASE) -> true (* exactly matches cparser *)
+          | _ -> false
+        in
+        let (al_default, al_nondefault) = List.partition (fun (at, _) -> is_default at) al in
+
+        let typ_compatible t1 t2 =
+          match combineTypes CombineOther t1 t2 with (* combineTypes does "compatible types" check *)
+          | _ -> true
+          | exception (Failure _) -> false
+        in
+        let (_, _, e_typ) = doExp false e (AExp None) in (* doExp with AExp handles array and function types for "lvalue conversions" (AType would not!) *)
+        let e_typ = removeOuterQualifierAttributes e_typ in (* removeOuterQualifierAttributes handles qualifiers for "lvalue conversions" *)
+        let al_compatible = List.filter (fun ((ast, adt), _) -> typ_compatible e_typ (doOnlyType ast adt)) al_nondefault in
+
+        (* TODO: error when multiple compatible associations or defaults even when unused? *)
+
+        begin match al_compatible with
+          | [(_, ae)] -> doExp false ae (AExp None)
+          | [] ->
+            begin match al_default with
+              | [(_, ae)] -> doExp false ae (AExp None)
+              | [] -> E.s (error "No compatible associations or default in generic")
+              | _ -> E.s (error "Multiple defaults in generic")
+            end
+          | _ -> E.s (error "Multiple compatible associations in generic")
+        end
+
   with e when continueOnError -> begin
     (*ignore (E.log "error in doExp (%s)" (Printexc.to_string e));*)
     E.hadErrors := true;

src/frontc/cabsvisit.ml

@@ -526,6 +526,17 @@ and childrenExpression vis e =
       let b' = visitCabsBlock vis b in
       if b' != b then GNU_BODY b' else e
   | EXPR_PATTERN _ -> e
+  | GENERIC (e1, al) ->
+      let e1' = ve e1 in
+      let al' = mapNoCopy (fun (((ast, adt), ae) as a) ->
+          let ast' = visitCabsSpecifier vis ast in
+          let adt' = visitCabsDeclType vis false adt in
+          let ae' = ve ae in
+          if ast' != ast || adt' != adt || ae' != ae then ((ast', adt'), ae') else a
+        ) al
+      in
+      if e1' != e1 || al' != al then GENERIC (e1', al') else e
+
 
 and visitCabsInitExpression vis (ie: init_expression) : init_expression =
   doVisit vis vis#vinitexpr childrenInitExpression ie

src/frontc/clexer.mll

@@ -211,6 +211,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