src/clight/clightFromC.ml

   1 open Printf
   2
   3 open Cparser
   4 open Cparser.C
   5 open Cparser.Env
   6
   7 open Clight
   8
   9 (** Extract the type part of a type-annotated Clight expression. *)
  10
  11 let typeof e = match e with Expr(_,te) -> te
  12
  13 (** Natural alignment of a type, in bytes. *)
  14 let rec alignof = function
  15   | Tvoid -> 1
  16   | Tint (I8,_) -> 1
  17   | Tint (I16,_) -> 2
  18   | Tint (I32,_) -> 4
  19   | Tfloat F32 -> 4
  20   | Tfloat F64 -> 8
  21   | Tpointer _ -> 4
  22   | Tarray (t',n) -> alignof t'
  23   | Tfunction (_,_) -> 1
  24   | Tstruct (_,fld) -> alignof_fields fld
  25   | Tunion (_,fld) -> alignof_fields fld
  26   | Tcomp_ptr _ -> 4
  27 and alignof_fields = function
  28           | [] -> 1
  29           | (id,t)::f' -> max (alignof t) (alignof_fields f')
  30
  31 (** Size of a type, in bytes. *)
  32
  33 let align n amount =
  34   ((n + amount - 1) / amount) * amount
  35
  36 let rec sizeof t =
  37   match t with
  38     | Tvoid -> 1
  39     | Tint (I8,_) -> 1
  40     | Tint (I16,_) -> 2
  41     | Tint (I32,_) -> 4
  42     | Tfloat F32 -> 4
  43     | Tfloat F64 -> 8
  44     | Tpointer _ -> 4
  45     | Tarray (t',n) -> sizeof t' * max 1 n
  46     | Tfunction (_,_) -> 1
  47     | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t)
  48     | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t)
  49     | Tcomp_ptr _ -> 4
  50 and sizeof_struct fld pos =
  51   match fld with
  52     | [] -> pos
  53     | (id,t)::fld' -> sizeof_struct fld' (align pos (alignof t) + sizeof t)
  54 and sizeof_union = function
  55   | [] -> 0
  56   | (id,t)::fld' -> max (sizeof t) (sizeof_union fld')
  57
  58 (** Record the declarations of global variables and associate them
  59     with the corresponding atom. *)
  60
  61 let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103
  62
  63 (** Hooks -- overriden in machine-dependent CPragmas module *)
  64
  65 let process_pragma_hook = ref (fun (s: string) -> false)
  66 let define_variable_hook = ref (fun (id: AST.ident) (d: C.decl) -> ())
  67 let define_function_hook = ref (fun (id: AST.ident) (d: C.decl) -> ())
  68 let define_stringlit_hook = ref (fun (id: AST.ident) -> ())
  69
  70 (** ** Error handling *)
  71
  72 let currentLocation = ref Cutil.no_loc
  73
  74 let updateLoc l = currentLocation := l
  75
  76 let numErrors = ref 0
  77
  78 let error msg =
  79   incr numErrors;
  80   eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg
  81
  82 let unsupported msg =
  83   incr numErrors;
  84   eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg
  85
  86 let warning msg =
  87   eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg
  88
  89
  90 (** ** Functions used to handle string literals *)
  91
  92 let stringNum = ref 0   (* number of next global for string literals *)
  93 let stringTable = Hashtbl.create 47
  94
  95 let name_for_string_literal env s =
  96   try
  97     Hashtbl.find stringTable s
  98   with Not_found ->
  99     incr stringNum;
 100     let name = Printf.sprintf "__stringlit_%d" !stringNum in
 101     let id = name in
 102     Hashtbl.add decl_atom id
 103       (env, (C.Storage_static,
 104              Env.fresh_ident name,
 105              C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
 106              None));
 107     !define_stringlit_hook id;
 108     Hashtbl.add stringTable s id;
 109     id
 110
 111 let typeStringLiteral s =
 112   Tarray(Tint(I8, AST.Unsigned), String.length s + 1)
 113
 114 let global_for_string s id =
 115   let init = ref [] in
 116   let add_char c =
 117     init :=
 118        Init_int8(Char.code c)
 119        :: !init in
 120   add_char '\000';
 121   for i = String.length s - 1 downto 0 do add_char s.[i] done;
 122   ((id, !init), typeStringLiteral s)
 123
 124 let globals_for_strings globs =
 125   Hashtbl.fold
 126     (fun s id l -> global_for_string s id :: l)
 127     stringTable globs
 128
 129 (** ** Handling of stubs for variadic functions *)
 130
 131 let stub_function_table = Hashtbl.create 47
 132
 133 let register_stub_function name tres targs =
 134   let rec letters_of_type = function
 135     | [] -> []
 136     | Tfloat(_)::tl -> "f" :: letters_of_type tl
 137     | _::tl -> "i" :: letters_of_type tl in
 138   let stub_name =
 139     name ^ "$" ^ String.concat "" (letters_of_type targs) in
 140   try
 141     (stub_name, Hashtbl.find stub_function_table stub_name)
 142   with Not_found ->
 143     let rec types_of_types = function
 144       | [] -> []
 145       | Tfloat(_)::tl -> Tfloat(F64)::(types_of_types tl)
 146       | _::tl -> Tpointer(Tvoid)::(types_of_types tl) in
 147     let stub_type = Tfunction (types_of_types targs, tres) in
 148     Hashtbl.add stub_function_table stub_name stub_type;
 149     (stub_name, stub_type)
 150
 151 let declare_stub_function stub_name stub_type =
 152   match stub_type with
 153   | Tfunction(targs, tres) ->
 154       (stub_name,
 155                          External(stub_name, targs, tres))
 156   | _ -> assert false
 157
 158 let declare_stub_functions k =
 159   Hashtbl.fold
 160     (fun n i k -> declare_stub_function n i :: k)
 161                stub_function_table k
 162
 163 (** ** Translation functions *)
 164
 165 (** Constants *)
 166
 167 let convertInt n = Int64.to_int n
 168
 169 (** Types *)
 170
 171 let convertIkind = function
 172   | C.IBool -> unsupported "'_Bool' type"; (AST.Unsigned, I8)
 173   | C.IChar -> (AST.Unsigned, I8)
 174   | C.ISChar -> (AST.Signed, I8)
 175   | C.IUChar -> (AST.Unsigned, I8)
 176   | C.IInt -> (AST.Signed, I32)
 177   | C.IUInt -> (AST.Unsigned, I32)
 178   | C.IShort -> (AST.Signed, I16)
 179   | C.IUShort -> (AST.Unsigned, I16)
 180   | C.ILong -> (AST.Signed, I32)
 181   | C.IULong -> (AST.Unsigned, I32)
 182   | C.ILongLong ->
 183       if not !ClightFlags.option_flonglong then unsupported "'long long' type";
 184       (AST.Signed, I32)
 185   | C.IULongLong ->
 186       if not !ClightFlags.option_flonglong then unsupported "'unsigned long long' type";
 187       (AST.Unsigned, I32)
 188
 189 let convertFkind = function
 190   | C.FFloat -> F32
 191   | C.FDouble -> F64
 192   | C.FLongDouble ->
 193       if not !ClightFlags.option_flonglong then unsupported "'long double' type";
 194       F64
 195
 196 let convertTyp env t =
 197
 198   let rec convertTyp seen t =
 199     match Cutil.unroll env t with
 200     | C.TVoid a -> Tvoid
 201     | C.TInt(ik, a) ->
 202         let (sg, sz) = convertIkind ik in Tint(sz, sg)
 203     | C.TFloat(fk, a) ->
 204         Tfloat(convertFkind fk)
 205     | C.TPtr(C.TStruct(id, _), _) when List.mem id seen ->
 206         Tcomp_ptr("struct " ^ id.name)
 207     | C.TPtr(C.TUnion(id, _), _) when List.mem id seen ->
 208         Tcomp_ptr("union " ^ id.name)
 209     | C.TPtr(ty, a) ->
 210         Tpointer(convertTyp seen ty)
 211     | C.TArray(ty, None, a) ->
 212         (* Cparser verified that the type ty[] occurs only in
 213            contexts that are safe for Clight, so just treat as ty[0]. *)
 214         (* warning "array type of unspecified size"; *)
 215         Tarray(convertTyp seen ty, 0)
 216     | C.TArray(ty, Some sz, a) ->
 217         Tarray(convertTyp seen ty, convertInt sz )
 218     | C.TFun(tres, targs, va, a) ->
 219         if va then unsupported "variadic function type";
 220         if Cutil.is_composite_type env tres then
 221           unsupported "return type is a struct or union";
 222         Tfunction(begin match targs with
 223                   | None -> warning "un-prototyped function type"; []
 224                   | Some tl -> convertParams seen tl
 225                   end,
 226                   convertTyp seen tres)
 227     | C.TNamed _ ->
 228         assert false
 229     | C.TStruct(id, a) ->
 230         let flds =
 231           try
 232             convertFields (id :: seen) (Env.find_struct env id)
 233           with Env.Error e ->
 234             error (Env.error_message e); [] in
 235         Tstruct("struct " ^ id.name, flds)
 236     | C.TUnion(id, a) ->
 237         let flds =
 238           try
 239             convertFields (id :: seen) (Env.find_union env id)
 240           with Env.Error e ->
 241             error (Env.error_message e); [] in
 242         Tunion("union " ^ id.name, flds)
 243
 244   and convertParams seen = function
 245     | [] -> []
 246     | (id, ty) :: rem ->
 247         if Cutil.is_composite_type env ty then
 248           unsupported "function parameter of struct or union type";
 249         (convertTyp seen ty)::(convertParams seen rem)
 250
 251   and convertFields seen ci =
 252     convertFieldList seen ci.Env.ci_members
 253
 254   and convertFieldList seen = function
 255     | [] -> []
 256     | f :: fl ->
 257         if f.fld_bitfield <> None then
 258           unsupported "bit field in struct or union";
 259         (f.fld_name, convertTyp seen f.fld_typ)::(
 260               convertFieldList seen fl)
 261
 262   in convertTyp [] t
 263
 264 let rec convertTypList env = function
 265   | [] -> []
 266   | t1 :: tl -> (convertTyp env t1 )::( convertTypList env tl)
 267
 268 (** Expressions *)
 269
 270 let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed))
 271
 272 let rec convertExpr env e =
 273   let ty = convertTyp env e.etyp in
 274   match e.edesc with
 275   | C.EConst(C.CInt(i, _, _)) ->
 276       Expr(Econst_int( convertInt i), ty)
 277   | C.EConst(C.CFloat(f, _, _)) ->
 278       Expr(Econst_float f, ty)
 279   | C.EConst(C.CStr s) ->
 280       Expr(Evar(name_for_string_literal env s), typeStringLiteral s)
 281   | C.EConst(C.CWStr s) ->
 282       unsupported "wide string literal"; ezero
 283   | C.EConst(C.CEnum(id, i)) ->
 284       Expr(Econst_int(convertInt i), ty)
 285
 286   | C.ESizeof ty1 ->
 287       Expr(Esizeof(convertTyp env ty1), ty)
 288   | C.EVar id ->
 289       Expr(Evar(id.name), ty)
 290
 291   | C.EUnop(C.Oderef, e1) ->
 292       Expr(Ederef(convertExpr env e1), ty)
 293   | C.EUnop(C.Oaddrof, e1) ->
 294       Expr(Eaddrof(convertExpr env e1), ty)
 295   | C.EUnop(C.Odot id, e1) ->
 296       Expr(Efield(convertExpr env e1, id), ty)
 297   | C.EUnop(C.Oarrow id, e1) ->
 298       let e1' = convertExpr env e1 in
 299       let ty1 =
 300         match typeof e1' with
 301         | Tpointer t -> t
 302         | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
 303       Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
 304                    id), ty)
 305   | C.EUnop(C.Oplus, e1) ->
 306       convertExpr env e1
 307   | C.EUnop(C.Ominus, e1) ->
 308       Expr(Eunop(Oneg, convertExpr env e1), ty)
 309   | C.EUnop(C.Olognot, e1) ->
 310       Expr(Eunop(Onotbool, convertExpr env e1), ty)
 311   | C.EUnop(C.Onot, e1) ->
 312       Expr(Eunop(Onotint, convertExpr env e1), ty)
 313   | C.EUnop(_, _) ->
 314       unsupported "pre/post increment/decrement operator"; ezero
 315
 316   | C.EBinop(C.Oindex, e1, e2, _) ->
 317       Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2),
 318                        Tpointer ty)), ty)
 319   | C.EBinop(C.Ologand, e1, e2, _) ->
 320       Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
 321   | C.EBinop(C.Ologor, e1, e2, _) ->
 322       Expr(Eorbool(convertExpr env e1, convertExpr env e2), ty)
 323   | C.EBinop(op, e1, e2, _) ->
 324       let op' =
 325         match op with
 326         | C.Oadd -> Oadd
 327         | C.Osub -> Osub
 328         | C.Omul -> Omul
 329         | C.Odiv -> Odiv
 330         | C.Omod -> Omod
 331         | C.Oand -> Oand
 332         | C.Oor  -> Oor
 333         | C.Oxor -> Oxor
 334         | C.Oshl -> Oshl
 335         | C.Oshr -> Oshr
 336         | C.Oeq  -> Oeq
 337         | C.One  -> One
 338         | C.Olt  -> Olt
 339         | C.Ogt  -> Ogt
 340         | C.Ole  -> Ole
 341         | C.Oge  -> Oge
 342         | C.Ocomma -> unsupported "sequence operator"; Oadd
 343         | _ -> unsupported "assignment operator"; Oadd in
 344       Expr(Ebinop(op', convertExpr env e1, convertExpr env e2), ty)
 345   | C.EConditional(e1, e2, e3) ->
 346       Expr(Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3), ty)
 347   | C.ECast(ty1, e1) ->
 348       Expr(Ecast(convertTyp env ty1, convertExpr env e1), ty)
 349   | C.ECall _ ->
 350       unsupported "function call within expression"; ezero
 351
 352 (* Function calls *)
 353
 354 let rec projFunType env ty =
 355   match Cutil.unroll env ty with
 356   | TFun(res, args, vararg, attr) -> Some(res, vararg)
 357   | TPtr(ty', attr) -> projFunType env ty'
 358   | _ -> None
 359
 360 let convertFuncall env lhs fn args =
 361   match projFunType env fn.etyp with
 362   | None ->
 363       error "wrong type for function part of a call"; Sskip
 364   | Some(res, false) ->
 365       (* Non-variadic function *)
 366       Scall(lhs, convertExpr env fn, List.map (convertExpr env) args)
 367   | Some(res, true) ->
 368       (* Variadic function: generate a call to a stub function with
 369          the appropriate number and types of arguments.  Works only if
 370          the function expression e is a global variable. *)
 371       let fun_name =
 372         match fn with
 373         | {edesc = C.EVar id} when !ClightFlags.option_fvararg_calls ->
 374             (*warning "emulating call to variadic function"; *)
 375             id.name
 376         | _ ->
 377             unsupported "call to variadic function";
 378             "<error>" in
 379       let targs = convertTypList env (List.map (fun e -> e.etyp) args) in
 380       let tres = convertTyp env res in
 381       let (stub_fun_name, stub_fun_typ) =
 382         register_stub_function fun_name tres targs in
 383       Scall(lhs,
 384             Expr(Evar( stub_fun_name), stub_fun_typ),
 385             List.map (convertExpr env) args)
 386
 387 (* Handling of volatile *)
 388
 389 let is_volatile_access env e =
 390   List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp)
 391   && Cutil.is_lvalue env e
 392
 393 let volatile_fun_suffix_type ty =
 394   match ty with
 395   | Tint(I8, AST.Unsigned) -> ("int8unsigned", ty)
 396   | Tint(I8, AST.Signed) -> ("int8signed", ty)
 397   | Tint(I16, AST.Unsigned) -> ("int16unsigned", ty)
 398   | Tint(I16, AST.Signed) -> ("int16signed", ty)
 399   | Tint(I32, _) -> ("int32", Tint(I32, AST.Signed))
 400   | Tfloat F32 -> ("float32", ty)
 401   | Tfloat F64 -> ("float64", ty)
 402   | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ ->
 403       ("pointer", Tpointer Tvoid)
 404   | _ ->
 405       unsupported "operation on volatile struct or union"; ("", Tvoid)
 406
 407 let volatile_read_fun ty =
 408   let (suffix, ty') = volatile_fun_suffix_type ty in
 409   Expr(Evar( ("__builtin_volatile_read_" ^ suffix)),
 410        Tfunction((Tpointer Tvoid)::[], ty'))
 411
 412 let volatile_write_fun ty =
 413   let (suffix, ty') = volatile_fun_suffix_type ty in
 414   Expr(Evar( ("__builtin_volatile_write_" ^ suffix)),
 415        Tfunction((Tpointer Tvoid)::(ty'::[]), Tvoid))
 416
 417 (* Toplevel expression, argument of an Sdo *)
 418
 419 let convertTopExpr env e =
 420   match e.edesc with
 421   | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) ->
 422       convertFuncall env (Some (convertExpr env lhs)) fn args
 423   | C.EBinop(C.Oassign, lhs, rhs, _) ->
 424       if Cutil.is_composite_type env lhs.etyp then
 425         unsupported "assignment between structs or between unions";
 426       let lhs' = convertExpr env lhs
 427       and rhs' = convertExpr env rhs in
 428       begin match (is_volatile_access env lhs, is_volatile_access env rhs) with
 429       | true, true ->                   (* should not happen *)
 430           unsupported "volatile-to-volatile assignment";
 431           Sskip
 432       | false, true ->                  (* volatile read *)
 433           Scall(Some lhs',
 434                 volatile_read_fun (typeof rhs'),
 435                 [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ])
 436       | true, false ->                  (* volatile write *)
 437           Scall(None,
 438                 volatile_write_fun (typeof lhs'),
 439                 [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ])
 440       | false, false ->                 (* regular assignment *)
 441           Sassign(convertExpr env lhs, convertExpr env rhs)
 442       end
 443   | C.ECall(fn, args) ->
 444       convertFuncall env None fn args
 445   | _ ->
 446       unsupported "illegal toplevel expression"; Sskip
 447
 448 (* Separate the cases of a switch statement body *)
 449
 450 type switchlabel =
 451   | Case of C.exp
 452   | Default
 453
 454 type switchbody =
 455   | Label of switchlabel
 456   | Stmt of C.stmt
 457
 458 let rec flattenSwitch = function
 459   | {sdesc = C.Sseq(s1, s2)} ->
 460       flattenSwitch s1 @ flattenSwitch s2
 461   | {sdesc = C.Slabeled(C.Scase e, s1)} ->
 462       Label(Case e) :: flattenSwitch s1
 463   | {sdesc = C.Slabeled(C.Sdefault, s1)} ->
 464       Label Default :: flattenSwitch s1
 465   | s ->
 466       [Stmt s]
 467
 468 let rec groupSwitch = function
 469   | [] ->
 470       (Cutil.sskip, [])
 471   | Label case :: rem ->
 472       let (fst, cases) = groupSwitch rem in
 473       (Cutil.sskip, (case, fst) :: cases)
 474   | Stmt s :: rem ->
 475       let (fst, cases) = groupSwitch rem in
 476       (Cutil.sseq s.sloc s fst, cases)
 477
 478 (* Statement *)
 479
 480 let rec convertStmt env s =
 481   updateLoc s.sloc;
 482   match s.sdesc with
 483   | C.Sskip ->
 484       Sskip
 485   | C.Sdo e ->
 486       convertTopExpr env e
 487   | C.Sseq(s1, s2) ->
 488       Ssequence(convertStmt env s1, convertStmt env s2)
 489   | C.Sif(e, s1, s2) ->
 490       Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2)
 491   | C.Swhile(e, s1) ->
 492       Swhile(convertExpr env e, convertStmt env s1)
 493   | C.Sdowhile(s1, e) ->
 494       Sdowhile(convertExpr env e, convertStmt env s1)
 495   | C.Sfor(s1, e, s2, s3) ->
 496       Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2,
 497            convertStmt env s3)
 498   | C.Sbreak ->
 499       Sbreak
 500   | C.Scontinue ->
 501       Scontinue
 502   | C.Sswitch(e, s1) ->
 503       let (init, cases) = groupSwitch (flattenSwitch s1) in
 504       if cases = [] then
 505         unsupported "ill-formed 'switch' statement";
 506       if init.sdesc <> C.Sskip then
 507         warning "ignored code at beginning of 'switch'";
 508       Sswitch(convertExpr env e, convertSwitch env cases)
 509   | C.Slabeled(C.Slabel lbl, s1) ->
 510       Slabel( lbl, convertStmt env s1)
 511   | C.Slabeled(C.Scase _, _) ->
 512       unsupported "'case' outside of 'switch'"; Sskip
 513   | C.Slabeled(C.Sdefault, _) ->
 514       unsupported "'default' outside of 'switch'"; Sskip
 515   | C.Sgoto lbl ->
 516       Sgoto( lbl)
 517   | C.Sreturn None ->
 518       Sreturn None
 519   | C.Sreturn(Some e) ->
 520       Sreturn(Some(convertExpr env e))
 521   | C.Sblock _ ->
 522       unsupported "nested blocks"; Sskip
 523   | C.Sdecl _ ->
 524       unsupported "inner declarations"; Sskip
 525
 526 and convertSwitch env = function
 527   | [] ->
 528       LSdefault Sskip
 529   | [Default, s] ->
 530       LSdefault (convertStmt env s)
 531   | (Default, s) :: _ ->
 532       updateLoc s.sloc;
 533       unsupported "'default' case must occur last";
 534       LSdefault Sskip
 535   | (Case e, s) :: rem ->
 536       updateLoc s.sloc;
 537       let v =
 538         match Ceval.integer_expr env e with
 539         | None -> unsupported "'case' label is not a compile-time integer"; 0L
 540         | Some v -> v in
 541       LScase(convertInt v,
 542              convertStmt env s,
 543              convertSwitch env rem)
 544
 545 (** Function definitions *)
 546
 547 let convertFundef env fd =
 548   if Cutil.is_composite_type env fd.fd_ret then
 549     unsupported "function returning a struct or union";
 550   let ret =
 551     convertTyp env fd.fd_ret in
 552   let params =
 553     List.map
 554       (fun (id, ty) ->
 555         if Cutil.is_composite_type env ty then
 556           unsupported "function parameter of struct or union type";
 557         ( id.name, convertTyp env ty))
 558       fd.fd_params in
 559   let vars =
 560     List.map
 561       (fun (sto, id, ty, init) ->
 562         if sto = Storage_extern || sto = Storage_static then
 563           unsupported "'static' or 'extern' local variable";
 564         if init <> None then
 565           unsupported "initialized local variable";
 566         ( id.name, convertTyp env ty))
 567       fd.fd_locals in
 568   let body' = convertStmt env fd.fd_body in
 569   let id' =  fd.fd_name.name in
 570   let decl =
 571     (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in
 572   Hashtbl.add decl_atom id' (env, decl);
 573   !define_function_hook id' decl;
 574   (id',
 575    Internal {fn_return = ret; fn_params = params;
 576              fn_vars = vars; fn_body = body'})
 577
 578 (** External function declaration *)
 579
 580 let convertFundecl env (sto, id, ty, optinit) =
 581   match convertTyp env ty with
 582   | Tfunction(args, res) ->
 583       let id' =  id.name in
 584       (id', External(id', args, res))
 585   | _ ->
 586       assert false
 587
 588 (** Initializers *)
 589
 590 let init_data_of_string s =
 591   let id = ref [] in
 592   let enter_char c =
 593     let n = (Char.code c) in
 594     id := Init_int8 n :: !id in
 595   enter_char '\000';
 596   for i = String.length s - 1 downto 0 do enter_char s.[i] done;
 597   !id
 598
 599 let convertInit env ty init =
 600
 601   let k = ref []
 602   and pos = ref 0 in
 603   let emit size datum =
 604     k := datum :: !k;
 605     pos := !pos + size in
 606   let emit_space size =
 607     emit size (Init_space size) in
 608   let align size =
 609     let n = !pos land (size - 1) in
 610     if n > 0 then emit_space (size - n) in
 611   let check_align size =
 612     assert (!pos land (size - 1) = 0) in
 613
 614   let rec reduceInitExpr = function
 615     | { edesc = C.EVar id; etyp = ty } ->
 616         begin match Cutil.unroll env ty with
 617         | C.TArray _ | C.TFun _ -> Some id
 618         | _ -> None
 619         end
 620     | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id
 621     | {edesc = C.ECast(ty, e)} -> reduceInitExpr e
 622     | _ -> None in
 623
 624   let rec cvtInit ty = function
 625   | Init_single e ->
 626       begin match reduceInitExpr e with
 627       | Some id ->
 628           check_align 4;
 629           emit 4 (Init_addrof( id.name, 0))
 630       | None ->
 631       match Ceval.constant_expr env ty e with
 632       | Some(C.CInt(v, ik, _)) ->
 633           begin match convertIkind ik with
 634           | (_, I8) ->
 635               emit 1 (Init_int8(convertInt v))
 636           | (_, I16) ->
 637               check_align 2;
 638               emit 2 (Init_int16(convertInt v))
 639           | (_, I32) ->
 640               check_align 4;
 641               emit 4 (Init_int32(convertInt v))
 642           end
 643       | Some(C.CFloat(v, fk, _)) ->
 644           begin match convertFkind fk with
 645           | F32 ->
 646               check_align 4;
 647               emit 4 (Init_float32 v)
 648           | F64 ->
 649               check_align 8;
 650               emit 8 (Init_float64 v)
 651           end
 652       | Some(C.CStr s) ->
 653           check_align 4;
 654           let id = name_for_string_literal env s in
 655           emit 4 (Init_addrof(id, 0))
 656       | Some(C.CWStr _) ->
 657           unsupported "wide character strings"
 658       | Some(C.CEnum _) ->
 659           error "enum tag after constant folding"
 660       | None ->
 661           error "initializer is not a compile-time constant"
 662       end
 663   | Init_array il ->
 664       let ty_elt =
 665         match Cutil.unroll env ty with
 666         | C.TArray(t, _, _) -> t
 667         | _ -> error "array type expected in initializer"; C.TVoid [] in
 668       List.iter (cvtInit ty_elt) il
 669   | Init_struct(_, flds) ->
 670       cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds)
 671   | Init_union(_, fld, i) ->
 672       cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i))
 673
 674   and cvtFieldInit (fld, i) =
 675     let ty' = convertTyp env fld.fld_typ in
 676     let al = alignof ty' in
 677     align al;
 678     cvtInit fld.fld_typ i
 679
 680   and cvtPadToSizeof ty fn =
 681     let ty' = convertTyp env ty in
 682     let sz = sizeof ty' in
 683     let pos0 = !pos in
 684     fn();
 685     let pos1 = !pos in
 686     assert (pos1 <= pos0 + sz);
 687     if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1)
 688
 689   in cvtInit ty init; List.rev !k
 690
 691 (** Global variable *)
 692
 693 let convertGlobvar env (sto, id, ty, optinit as decl) =
 694   let id' =  id.name in
 695   let ty' = convertTyp env ty in
 696   let init' =
 697     match optinit with
 698     | None ->
 699         if sto = C.Storage_extern then [] else [Init_space(sizeof ty')]
 700     | Some i ->
 701         convertInit env ty i in
 702   Hashtbl.add decl_atom id' (env, decl);
 703   !define_variable_hook id' decl;
 704   ((id', init'), ty')
 705
 706 (** Convert a list of global declarations.
 707   Result is a pair [(funs, vars)] where [funs] are
 708   the function definitions (internal and external)
 709   and [vars] the variable declarations. *)
 710
 711 let rec convertGlobdecls env funs vars gl =
 712   match gl with
 713   | [] -> (List.rev funs, List.rev vars)
 714   | g :: gl' ->
 715       updateLoc g.gloc;
 716       match g.gdesc with
 717       | C.Gdecl((sto, id, ty, optinit) as d) ->
 718           (* Prototyped functions become external declarations.
 719              Variadic functions are skipped.
 720              Other types become variable declarations. *)
 721           begin match Cutil.unroll env ty with
 722           | TFun(_, Some _, false, _) ->
 723               convertGlobdecls env (convertFundecl env d :: funs) vars gl'
 724           | TFun(_, None, false, _) ->
 725               error "function declaration without prototype";
 726               convertGlobdecls env funs vars gl'
 727           | TFun(_, _, true, _) ->
 728               convertGlobdecls env funs vars gl'
 729           | _ ->
 730               convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
 731           end
 732       | C.Gfundef fd ->
 733           convertGlobdecls env (convertFundef env fd :: funs) vars gl'
 734       | C.Gcompositedecl _ | C.Gcompositedef _
 735       | C.Gtypedef _ | C.Genumdef _ ->
 736           (* typedefs are unrolled, structs are expanded inline, and
 737              enum tags are folded.  So we just skip their declarations. *)
 738           convertGlobdecls env funs vars gl'
 739       | C.Gpragma s ->
 740           if not (!process_pragma_hook s) then
 741             warning ("'#pragma " ^ s ^ "' directive ignored");
 742           convertGlobdecls env funs vars gl'
 743
 744 (** Build environment of typedefs and structs *)
 745
 746 let rec translEnv env = function
 747   | [] -> env
 748   | g :: gl ->
 749       let env' =
 750         match g.gdesc with
 751         | C.Gcompositedecl(su, id) ->
 752             Env.add_composite env id (Cutil.composite_info_decl env su)
 753         | C.Gcompositedef(su, id, fld) ->
 754             Env.add_composite env id (Cutil.composite_info_def env su fld)
 755         | C.Gtypedef(id, ty) ->
 756             Env.add_typedef env id ty
 757         | _ ->
 758             env in
 759       translEnv env' gl
 760
 761 (** Eliminate forward declarations of globals that are defined later. *)
 762
 763 module IdentSet = Set.Make(struct type t = C.ident let compare = compare end)
 764
 765 let cleanupGlobals p =
 766
 767   let rec clean defs accu = function
 768     | [] -> accu
 769     | g :: gl ->
 770         updateLoc g.gloc;
 771         match g.gdesc with
 772         | C.Gdecl(sto, id, ty, None) ->
 773             if IdentSet.mem id defs
 774             then clean defs accu gl
 775             else clean (IdentSet.add id defs) (g :: accu) gl
 776         | C.Gdecl(_, id, ty, _) ->
 777             if IdentSet.mem id defs then
 778               error ("multiple definitions of " ^ id.name);
 779             clean (IdentSet.add id defs) (g :: accu) gl
 780         | C.Gfundef fd ->
 781             if IdentSet.mem fd.fd_name defs then
 782               error ("multiple definitions of " ^ fd.fd_name.name);
 783             clean (IdentSet.add fd.fd_name defs) (g :: accu) gl
 784         | _ ->
 785             clean defs (g :: accu) gl
 786
 787   in clean IdentSet.empty [] (List.rev p)
 788
 789 (** Convert a [C.program] into a [Csyntax.program] *)
 790
 791 let convertProgram p =
 792   numErrors := 0;
 793   stringNum := 0;
 794   Hashtbl.clear decl_atom;
 795   Hashtbl.clear stringTable;
 796   Hashtbl.clear stub_function_table;
 797   (* Hack: externals are problematic for Cerco. TODO *)
 798   let p = (* Builtins.declarations() @ *) p in
 799   try
 800     let (funs1, vars1) =
 801       convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in
 802     let funs2 = declare_stub_functions funs1 in
 803     let main = if List.mem_assoc "main" funs2 then Some "main" else None in
 804     let vars2 = globals_for_strings vars1 in
 805     if !numErrors > 0
 806     then None
 807     else Some { prog_funct = funs2;
 808                 prog_vars = vars2;
 809                 prog_main = main }
 810   with Env.Error msg ->
 811     error (Env.error_message msg); None
 812
 813 (** ** Extracting information about global variables from their atom *)
 814
 815 let rec type_is_readonly env t =
 816   let a = Cutil.attributes_of_type env t in
 817   if List.mem C.AVolatile a then false else
 818   if List.mem C.AConst a then true else
 819   match Cutil.unroll env t with
 820   | C.TArray(t', _, _) -> type_is_readonly env t'
 821   | _ -> false
 822
 823 let atom_is_static a =
 824   try
 825     let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
 826     sto = C.Storage_static
 827   with Not_found ->
 828     false
 829
 830 let atom_is_readonly a =
 831   try
 832     let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
 833     type_is_readonly env ty
 834   with Not_found ->
 835     false
 836
 837 let atom_sizeof a =
 838   try
 839     let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
 840     Cutil.sizeof env ty
 841   with Not_found ->
 842     None
 843
 844 let atom_alignof a =
 845   try
 846     let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
 847     Cutil.alignof env ty
 848   with Not_found ->
 849     None
 850
 851 (** ** The builtin environment *)
 852
 853 open Builtins
 854
 855 let builtins_generic = {
 856   typedefs = [
 857     (* keeps GCC-specific headers happy, harmless for others *)
 858     "__builtin_va_list", C.TPtr(C.TVoid [], [])
 859   ];
 860   functions = [
 861     (* The volatile read/volatile write functions *)
 862     "__builtin_volatile_read_int8unsigned",
 863         (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
 864     "__builtin_volatile_read_int8signed",
 865         (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
 866     "__builtin_volatile_read_int16unsigned",
 867         (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
 868     "__builtin_volatile_read_int16signed",
 869         (TInt(IShort, []), [TPtr(TVoid [], [])], false);
 870     "__builtin_volatile_read_int32",
 871         (TInt(IInt, []), [TPtr(TVoid [], [])], false);
 872     "__builtin_volatile_read_float32",
 873         (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
 874     "__builtin_volatile_read_float64",
 875          (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
 876     "__builtin_volatile_read_pointer",
 877          (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
 878     "__builtin_volatile_write_int8unsigned",
 879         (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
 880     "__builtin_volatile_write_int8signed",
 881         (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
 882     "__builtin_volatile_write_int16unsigned",
 883         (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
 884     "__builtin_volatile_write_int16signed",
 885         (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
 886     "__builtin_volatile_write_int32",
 887         (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
 888     "__builtin_volatile_write_float32",
 889         (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
 890     "__builtin_volatile_write_float64",
 891          (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
 892     "__builtin_volatile_write_pointer",
 893          (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
 894   ]
 895 }
 896
 897 (* Add processor-dependent builtins *)
 898
 899 let builtins =
 900   { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
 901     functions = builtins_generic.functions @ CBuiltins.builtins.functions
 902   }