From 712f3cbae6bfd3c6f6cc40d44f438aa0affcd371 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 18 Dec 2012 07:54:35 +0000
Subject: Support for inline assembly (asm statements). cparser: add primitive
 support for enum types. bitfield emulation: for bitfields with enum type,
 choose signed/unsigned as appropriate

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2C.ml  | 23 +++++++++++++++++++++--
 cfrontend/Cexec.v |  7 +++++++
 2 files changed, 28 insertions(+), 2 deletions(-)

(limited to 'cfrontend')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2cdcc03..aa9eca0 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -293,6 +293,9 @@ let convertTyp env t =
           with Env.Error e ->
             error (Env.error_message e); Fnil in
         Tunion(intern_string("union " ^ id.name), flds, convertAttr a)
+    | C.TEnum(id, a) ->
+        let (sg, sz) = convertIkind Cutil.enum_ikind in
+        Tint(sz, sg, convertAttr a)
 
   and convertParams seen = function
     | [] -> Tnil
@@ -332,6 +335,12 @@ let first_class_value env ty =
   | C.TInt((C.ILongLong|C.IULongLong), _) -> false
   | _ -> true
 
+let supported_return_type env ty =
+  match Cutil.unroll env ty with
+  | C.TInt((C.ILongLong|C.IULongLong), _) -> false
+  | C.TStruct _  | C.TUnion _ -> false
+  | _ -> true
+
 (** Floating point constants *)
 
 let z_of_str hex str fst =
@@ -499,6 +508,8 @@ let rec convertExpr env e =
   | C.EConditional(e1, e2, e3) ->
       Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty)
   | C.ECast(ty1, e1) ->
+      if not (first_class_value env ty1) then
+        unsupported ("cast to type " ^ string_of_type ty1);
       Ecast(convertExpr env e1, convertTyp env ty1)
 
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
@@ -527,6 +538,8 @@ let rec convertExpr env e =
       make_builtin_memcpy (convertExprList env args)
 
   | C.ECall(fn, args) ->
+      if not (supported_return_type env e.etyp) then
+        unsupported ("function returning a result of type " ^ string_of_type e.etyp);
       match projFunType env fn.etyp with
       | None ->
           error "wrong type for function part of a call"; ezero
@@ -660,6 +673,10 @@ let rec convertStmt env s =
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
       unsupported "inner declarations"; Sskip
+  | C.Sasm txt ->
+      if not !Clflags.option_finline_asm then
+        unsupported "inline 'asm' statement (consider adding option -finline-asm)";
+      Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid))
 
 and convertSwitch env = function
   | [] ->
@@ -820,7 +837,7 @@ let rec convertGlobdecls env res gl =
           | TFun(_, Some _, false, _) ->
               convertGlobdecls env (convertFundecl env d :: res) gl'
           | TFun(_, None, false, _) ->
-              error "function declaration without prototype";
+              error ("'" ^ id.name ^ "' is declared without a function prototype");
               convertGlobdecls env res gl'
           | TFun(_, _, true, _) ->
               convertGlobdecls env res gl'
@@ -842,7 +859,7 @@ let rec convertGlobdecls env res gl =
             warning ("'#pragma " ^ s ^ "' directive ignored");
           convertGlobdecls env res gl'
 
-(** Build environment of typedefs and structs *)
+(** Build environment of typedefs, structs, unions and enums *)
 
 let rec translEnv env = function
   | [] -> env
@@ -855,6 +872,8 @@ let rec translEnv env = function
             Env.add_composite env id (Cutil.composite_info_def env su attr fld)
         | C.Gtypedef(id, ty) ->
             Env.add_typedef env id ty
+        | C.Genumdef(id, attr, members) ->
+            Env.add_enum env id {ei_members = members; ei_attr = attr}
         | _ ->
             env in
       translEnv env' gl
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b6ea1e0..c768118 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -506,6 +506,7 @@ Definition do_external (ef: external_function):
   | EF_memcpy sz al => do_ef_memcpy sz al
   | EF_annot text targs => do_ef_annot text targs
   | EF_annot_val text targ => do_ef_annot_val text targ
+  | EF_inline_asm text => do_ef_annot text nil
   end.
 
 Lemma do_ef_external_sound:
@@ -575,6 +576,10 @@ Proof with try congruence.
   unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. 
   split. constructor. apply eventval_of_val_sound; auto.
   econstructor. constructor; eauto. constructor.
+(* EF_inline_asm *)
+  unfold do_ef_annot. destruct vargs; simpl... mydestr. 
+  split. constructor. constructor. 
+  econstructor. constructor; eauto. constructor.
 Qed.
 
 Lemma do_ef_external_complete:
@@ -633,6 +638,8 @@ Proof.
 (* EF_annot_val *)
   inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. 
   rewrite (eventval_of_val_complete _ _ _ H1). auto.
+(* EF_inline_asm *)
+  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. inv H1. simpl. auto.
 Qed.
 
 (** * Reduction of expressions *)
-- 
cgit v1.2.3