From 4c36fcb770cf8e45bb6a23c8a176f61c1fbfd605 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 08:33:22 +0000 Subject: Better emulation of long long as a struct. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1500 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 65 +++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 50 insertions(+), 15 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6649a2c8..26815a10 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -242,25 +242,29 @@ let convertIkind = function | C.IUShort -> (Unsigned, I16) | C.ILong -> (Signed, I32) | C.IULong -> (Unsigned, I32) - | C.ILongLong -> - if not !Clflags.option_flonglong then unsupported "'long long' type"; - (Signed, I32) - | C.IULongLong -> - if not !Clflags.option_flonglong then unsupported "'unsigned long long' type"; - (Unsigned, I32) + (* Special-cased in convertTyp below *) + | C.ILongLong -> unsupported "'long long' type"; (Signed, I32) + | C.IULongLong -> unsupported "'unsigned long long' type"; (Unsigned, I32) let convertFkind = function | C.FFloat -> F32 | C.FDouble -> F64 - | C.FLongDouble -> - if not !Clflags.option_flonglong then unsupported "'long double' type"; - F64 + | C.FLongDouble -> unsupported "'long double' type"; F64 + +let int64_struct = + let ty = Tint(I32,Unsigned) in + Tstruct(intern_string "struct __int64", + if Memdataaux.big_endian + then Fcons(intern_string "hi", ty, Fcons(intern_string "lo", ty, Fnil)) + else Fcons(intern_string "lo", ty, Fcons(intern_string "hi", ty, Fnil))) let convertTyp env t = let rec convertTyp seen t = match Cutil.unroll env t with | C.TVoid a -> Tvoid + | C.TInt((C.ILongLong|C.IULongLong), a) when !Clflags.option_flonglong -> + int64_struct | C.TInt(ik, a) -> let (sg, sz) = convertIkind ik in Tint(sz, sg) | C.TFloat(fk, a) -> @@ -334,6 +338,20 @@ let rec projFunType env ty = | TPtr(ty', attr) -> projFunType env ty' | _ -> None +let string_of_type ty = + let b = Buffer.create 20 in + let fb = Format.formatter_of_buffer b in + Cprint.typ fb ty; + Format.pp_print_flush fb (); + Buffer.contents b + +let first_class_value env ty = + match Cutil.unroll env ty with + | C.TInt((C.ILongLong|C.IULongLong), _) -> false + | C.TStruct _ -> false + | C.TUnion _ -> false + | _ -> true + (* Handling of volatile *) let is_volatile_access env e = @@ -368,6 +386,12 @@ let volatile_write_fun ty = let ezero = Eval(Vint(coqint_of_camlint 0l), Tint(I32, Signed)) +let check_assignop msg env e = + if not (first_class_value env e.etyp) then + unsupported (msg ^ " on a l-value of type " ^ string_of_type e.etyp); + if is_volatile_access env e then + unsupported (msg ^ " on a volatile l-value") + let rec convertExpr env e = let ty = convertTyp env e.etyp in match e.edesc with @@ -375,6 +399,8 @@ let rec convertExpr env e = | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in + if not (first_class_value env e.etyp) then + unsupported ("r-value of type " ^ string_of_type e.etyp); if is_volatile_access env e then Ecall(volatile_read_fun (typeof l), Econs(Eaddrof(l, Tpointer(typeof l)), Enil), @@ -407,12 +433,16 @@ let rec convertExpr env e = | C.EUnop(C.Oaddrof, e1) -> Eaddrof(convertLvalue env e1, ty) | C.EUnop(C.Opreincr, e1) -> + check_assignop "pre-increment" env e1; coq_Epreincr Incr (convertLvalue env e1) ty | C.EUnop(C.Opredecr, e1) -> + check_assignop "pre-decrement" env e1; coq_Epreincr Decr (convertLvalue env e1) ty | C.EUnop(C.Opostincr, e1) -> + check_assignop "post-increment" env e1; Epostincr(Incr, convertLvalue env e1, ty) | C.EUnop(C.Opostdecr, e1) -> + check_assignop "post-decrement" env e1; Epostincr(Decr, convertLvalue env e1, ty) | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor| @@ -441,8 +471,8 @@ let rec convertExpr env e = | C.EBinop(C.Oassign, e1, e2, _) -> let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in - if Cutil.is_composite_type env e1.etyp then - unsupported "assignment between structs or between unions"; + if not (first_class_value env e1.etyp) then + unsupported ("assignment to a l-value of type " ^ string_of_type e1.etyp); if is_volatile_access env e1 then Ecall(volatile_write_fun (typeof e1'), Econs(Eaddrof(e1', Tpointer(typeof e1')), Econs(e2', Enil)), @@ -469,10 +499,8 @@ let rec convertExpr env e = | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in - if is_volatile_access env e1 then - (error "assign-op to volatile not supported"; ezero) - else - Eassignop(op', e1', e2', tyres, ty) + check_assignop "assignment-operation" env e1; + Eassignop(op', e1', e2', tyres, ty) | C.EBinop(C.Ocomma, e1, e2, _) -> Ecomma(convertExpr env e1, convertExpr env e2, ty) | C.EBinop(C.Ologand, e1, e2, _) -> @@ -955,6 +983,13 @@ let atom_is_static a = with Not_found -> false +let atom_is_extern a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + sto = C.Storage_extern + with Not_found -> + false + let atom_is_readonly a = try let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in -- cgit