source: Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml @ 489

Last change on this file since 489 was 489, checked in by campbell, 9 years ago

Pointer fixes for the temporary version of the compiler that can output matita
terms.

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