Preliminary support for gcc-style __attribute__ over types

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 168 insertions, 135 deletions

diff --git a/cparser/.depend b/cparser/.depend
index 9f12718..d2338ef 100644
--- a/cparser/.depend
+++ b/cparser/.depend
@@ -1,81 +1,86 @@
-AddCasts.cmi: C.cmi 
-Bitfields.cmi: C.cmi 
-Builtins.cmi: Env.cmi C.cmi 
-Ceval.cmi: Env.cmi C.cmi 
-Cleanup.cmi: C.cmi 
-C.cmi: 
-Cprint.cmi: C.cmi 
-Cutil.cmi: Env.cmi C.cmi 
-Elab.cmi: C.cmi 
-Env.cmi: C.cmi 
-Errors.cmi: 
-GCC.cmi: Builtins.cmi 
-Lexer.cmi: Parser.cmi 
-Machine.cmi: 
-Parse_aux.cmi: 
-Parse.cmi: C.cmi 
-Parser.cmi: Cabs.cmo 
-Rename.cmi: C.cmi 
-SimplExpr.cmi: C.cmi 
-StructAssign.cmi: C.cmi 
-StructByValue.cmi: C.cmi 
-Transform.cmi: Env.cmi C.cmi 
-Unblock.cmi: C.cmi 
-AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi 
-AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi 
-Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi 
-Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi 
-Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi 
-Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi 
-Cabshelper.cmo: Cabs.cmo 
-Cabshelper.cmx: Cabs.cmx 
-Cabs.cmo: 
-Cabs.cmx: 
-Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi 
-Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi 
-Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi 
-Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi 
-Cprint.cmo: C.cmi Cprint.cmi 
-Cprint.cmx: C.cmi Cprint.cmi 
-Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi 
-Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi 
+AddCasts.cmi: C.cmi
+Bitfields.cmi: C.cmi
+Builtins.cmi: Env.cmi C.cmi
+Ceval.cmi: Env.cmi C.cmi
+Cleanup.cmi: C.cmi
+C.cmi:
+Cprint.cmi: C.cmi
+Cutil.cmi: Env.cmi C.cmi
+Elab.cmi: C.cmi
+Env.cmi: C.cmi
+Errors.cmi:
+GCC.cmi: Builtins.cmi
+Lexer.cmi: Parser.cmi
+Machine.cmi:
+PackedStructs.cmi: C.cmi
+Parse_aux.cmi:
+Parse.cmi: C.cmi
+Parser.cmi: Cabs.cmo
+Rename.cmi: C.cmi
+SimplExpr.cmi: C.cmi
+StructAssign.cmi: C.cmi
+StructByValue.cmi: C.cmi
+Transform.cmi: Env.cmi C.cmi
+Unblock.cmi: C.cmi
+AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi
+AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi
+Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi
+Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi
+Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi
+Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi
+Cabshelper.cmo: Cabs.cmo
+Cabshelper.cmx: Cabs.cmx
+Cabs.cmo:
+Cabs.cmx:
+Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi
+Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi
+Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi
+Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi
+Cprint.cmo: C.cmi Cprint.cmi
+Cprint.cmx: C.cmi Cprint.cmi
+Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi
+Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi
 Elab.cmo: Parser.cmi Machine.cmi Lexer.cmi Errors.cmi Env.cmi Cutil.cmi \
     Cprint.cmi Cleanup.cmi Ceval.cmi Cabshelper.cmo Cabs.cmo C.cmi \
-    Builtins.cmi Elab.cmi 
+    Builtins.cmi Elab.cmi
 Elab.cmx: Parser.cmx Machine.cmx Lexer.cmx Errors.cmx Env.cmx Cutil.cmx \
     Cprint.cmx Cleanup.cmx Ceval.cmx Cabshelper.cmx Cabs.cmx C.cmi \
-    Builtins.cmx Elab.cmi 
-Env.cmo: C.cmi Env.cmi 
-Env.cmx: C.cmi Env.cmi 
-Errors.cmo: Errors.cmi 
-Errors.cmx: Errors.cmi 
-GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi 
-GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi 
-Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi 
-Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi 
-Machine.cmo: Machine.cmi 
-Machine.cmx: Machine.cmi 
-Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi 
-Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx 
-Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi 
-Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi 
+    Builtins.cmx Elab.cmi
+Env.cmo: C.cmi Env.cmi
+Env.cmx: C.cmi Env.cmi
+Errors.cmo: Errors.cmi
+Errors.cmx: Errors.cmi
+GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi
+GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi
+Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi
+Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi
+Machine.cmo: Machine.cmi
+Machine.cmx: Machine.cmi
+Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi
+Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx
+PackedStructs.cmo: Errors.cmi Env.cmi Cutil.cmi C.cmi Builtins.cmi \
+    PackedStructs.cmi
+PackedStructs.cmx: Errors.cmx Env.cmx Cutil.cmx C.cmi Builtins.cmx \
+    PackedStructs.cmi
+Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi
+Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi
 Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplExpr.cmi \
-    Rename.cmi Errors.cmi Elab.cmi Bitfields.cmi AddCasts.cmi Parse.cmi 
+    Rename.cmi Errors.cmi Elab.cmi Bitfields.cmi AddCasts.cmi Parse.cmi
 Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplExpr.cmx \
-    Rename.cmx Errors.cmx Elab.cmx Bitfields.cmx AddCasts.cmx Parse.cmi 
-Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi 
-Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi 
-Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi 
-Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi 
-SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi 
-SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi 
-StructAssign.cmo: Transform.cmi Errors.cmi Env.cmi Cutil.cmi C.cmi \
-    StructAssign.cmi 
-StructAssign.cmx: Transform.cmx Errors.cmx Env.cmx Cutil.cmx C.cmi \
-    StructAssign.cmi 
-StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi 
-StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi 
-Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi 
-Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi 
-Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi 
-Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi 
+    Rename.cmx Errors.cmx Elab.cmx Bitfields.cmx AddCasts.cmx Parse.cmi
+Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi
+Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi
+Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi
+Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi
+SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi
+SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi
+StructAssign.cmo: Transform.cmi Machine.cmi Errors.cmi Env.cmi Cutil.cmi \
+    C.cmi StructAssign.cmi
+StructAssign.cmx: Transform.cmx Machine.cmx Errors.cmx Env.cmx Cutil.cmx \
+    C.cmi StructAssign.cmi
+StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi
+StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi
+Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi
+Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi
+Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi
+Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi
diff --git a/cparser/C.mli b/cparser/C.mli
index d477acd..9d5a7d7 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -61,7 +61,16 @@ type constant =
 
 (** Attributes *)
 
-type attribute = AConst | AVolatile | ARestrict
+type attr_arg =
+  | AIdent of string
+  | AInt of int64
+  | AString of string
+
+type attribute = 
+  | AConst
+  | AVolatile
+  | ARestrict
+  | Attr of string * attr_arg list
 
 type attributes = attribute list
 
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 7d8f2b3..3d023a8 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -31,10 +31,72 @@ let ident pp i =
   then fprintf pp "%s$%d" i.name i.stamp
   else fprintf pp "%s" i.name
 
+let const pp = function
+  | CInt(v, ik, s) ->
+      if s <> "" then
+        fprintf pp "%s" s
+      else begin
+        fprintf pp "%Ld" v;
+        match ik with
+        | IULongLong -> fprintf pp "ULL"
+        | ILongLong -> fprintf pp "LL"
+        | IULong -> fprintf pp "UL"
+        | ILong -> fprintf pp "L"
+        | IUInt -> fprintf pp "U"
+        | _ -> ()
+      end
+  | CFloat(v, fk, s) ->
+      if s <> "" then
+        fprintf pp "%s" s
+      else begin
+        fprintf pp "%.18g" v;
+        match fk with
+        | FFloat -> fprintf pp "F"
+        | FLongDouble -> fprintf pp "L"
+        | _ -> ()
+      end
+  | CStr s ->
+      fprintf pp "\"";
+      for i = 0 to String.length s - 1 do
+        match s.[i] with
+        | '\009' -> fprintf pp "\\t"
+        | '\010' -> fprintf pp "\\n"
+        | '\013' -> fprintf pp "\\r"
+        | '\"'   -> fprintf pp "\\\""
+        | '\\'   -> fprintf pp "\\\\"
+        | c ->
+            if c >= ' ' && c <= '~'
+            then fprintf pp "%c" c
+            else fprintf pp "\\%03o" (Char.code c)
+      done;
+      fprintf pp "\""
+  | CWStr l ->
+      fprintf pp "L\"";
+      List.iter
+        (fun c ->
+          if c >= 32L && c <= 126L && c <> 34L && c <>92L
+          then fprintf pp "%c" (Char.chr (Int64.to_int c))
+          else fprintf pp "\" \"\\x%02Lx\" \"" c)
+        l;      
+      fprintf pp "\""
+  | CEnum(id, v) ->
+      ident pp id
+
+let attr_arg pp = function
+  | AIdent s -> fprintf pp "%s" s
+  | AInt n -> fprintf pp "%Ld" n
+  | AString s -> const pp (CStr s)
+
 let attribute pp = function
   | AConst -> fprintf pp "const"
   | AVolatile -> fprintf pp "volatile"
   | ARestrict -> fprintf pp "restrict"
+  | Attr(name, []) -> fprintf pp "__attribute__((%s))" name
+  | Attr(name, arg1 :: args) ->
+      fprintf pp "__attribute__((%s(" name;
+      attr_arg pp arg1;
+      List.iter (fun aa -> fprintf pp ", %a" attr_arg aa) args;
+      fprintf pp ")))"
 
 let attributes pp = function
   | [] -> ()
@@ -114,57 +176,6 @@ let rec dcl pp ty n =
 let typ pp ty =
   dcl pp ty (fun _ -> ())
 
-let const pp = function
-  | CInt(v, ik, s) ->
-      if s <> "" then
-        fprintf pp "%s" s
-      else begin
-        fprintf pp "%Ld" v;
-        match ik with
-        | IULongLong -> fprintf pp "ULL"
-        | ILongLong -> fprintf pp "LL"
-        | IULong -> fprintf pp "UL"
-        | ILong -> fprintf pp "L"
-        | IUInt -> fprintf pp "U"
-        | _ -> ()
-      end
-  | CFloat(v, fk, s) ->
-      if s <> "" then
-        fprintf pp "%s" s
-      else begin
-        fprintf pp "%.18g" v;
-        match fk with
-        | FFloat -> fprintf pp "F"
-        | FLongDouble -> fprintf pp "L"
-        | _ -> ()
-      end
-  | CStr s ->
-      fprintf pp "\"";
-      for i = 0 to String.length s - 1 do
-        match s.[i] with
-        | '\009' -> fprintf pp "\\t"
-        | '\010' -> fprintf pp "\\n"
-        | '\013' -> fprintf pp "\\r"
-        | '\"'   -> fprintf pp "\\\""
-        | '\\'   -> fprintf pp "\\\\"
-        | c ->
-            if c >= ' ' && c <= '~'
-            then fprintf pp "%c" c
-            else fprintf pp "\\%03o" (Char.code c)
-      done;
-      fprintf pp "\""
-  | CWStr l ->
-      fprintf pp "L\"";
-      List.iter
-        (fun c ->
-          if c >= 32L && c <= 126L && c <> 34L && c <>92L
-          then fprintf pp "%c" (Char.chr (Int64.to_int c))
-          else fprintf pp "\" \"\\x%02Lx\" \"" c)
-        l;      
-      fprintf pp "\""
-  | CEnum(id, v) ->
-      ident pp id
-
 type associativity = LtoR | RtoL | NA
 
 let precedence = function               (* H&S section 7.2 *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 7204508..9a4639f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -255,13 +255,25 @@ let elab_constant loc = function
 
 (* Elaboration of attributes *)
 
+exception Wrong_attr_arg
+
+let elab_attr_arg loc = function
+  | VARIABLE v -> AIdent v
+  | CONSTANT(CONST_STRING s) -> AString s
+  | CONSTANT(CONST_INT s) ->
+      let (v, _) = elab_int_constant loc s in AInt v
+  | _ -> raise Wrong_attr_arg
+
 let elab_attribute loc = function
   | ("const", []) -> Some AConst
   | ("restrict", []) -> Some ARestrict
   | ("volatile", []) -> Some AVolatile
   | (name, args) -> 
-      (* warning loc "ignoring '%s' attribute" name; *)
-      None
+      try
+        Some (Attr(name, List.map (elab_attr_arg loc) args))
+      with Wrong_attr_arg ->
+        warning loc "cannot parse '%s' attribute, ignored" name;
+        None
 
 let rec elab_attributes loc = function
   | [] -> []
diff --git a/cparser/Makefile b/cparser/Makefile
index 837bda8..59d4b47 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -31,13 +31,13 @@ install:
 	cp -p Cparser.cmi cparser.cma cparser.cmxa cparser.a libcparser.a dllcparser.so $(LIBDIR)
 
 cparser: $(COBJS) $(NOBJS) Main.cmx
-	$(OCAMLOPT) -o cparser $(COBJS) $(NOBJS) Main.cmx
+	$(OCAMLOPT) -o cparser str.cmxa $(COBJS) $(NOBJS) Main.cmx
 
 clean::
 	rm -f cparser
 
 cparser.byte: $(COBJS) $(BOBJS) Main.cmo
-	$(OCAMLC) -custom -o cparser.byte $(COBJS) $(BOBJS) Main.cmo
+	$(OCAMLC) -custom -o cparser.byte str.cma $(COBJS) $(BOBJS) Main.cmo
 
 clean::
 	rm -f cparser
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index b7f57f3..911d613 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -49,10 +49,6 @@ let program
     ?(typedef = fun env id ty -> ty)
     p =
 
-(* In all transformations of interest so far, the environment is used only
-   for its type definitions and struct/union definitions,
-   so we do not update it for other definitions. *)
-
   let rec transf_globdecls env accu = function
   | [] -> List.rev accu
   | g :: gl ->