source: driver/clightFromC.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 31.4 KB
Line 
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
126let idGenerator = ref (Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag)
127let idTable = Hashtbl.create 47
128let symTable = Hashtbl.create 47
129let make_id s =
130  try
131    Hashtbl.find idTable s
132  with Not_found ->
133    let { Extracted.Types.fst = id; Extracted.Types.snd = g} = Extracted.Identifiers.fresh Extracted.PreIdentifiers.SymbolTag !idGenerator in
134    idGenerator := g;
135    Hashtbl.add idTable s id;
136    Hashtbl.add symTable id s;
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  -> One
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;
861  idGenerator := Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag;
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.