source: driver/clightFromC.ml @ 2769

Last change on this file since 2769 was 2758, checked in by campbell, 7 years ago

Adapt prototype's Clight printer.
Doesn't use cost map yet.

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