source: driver/clightFromC.ml @ 2620

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

Sufficient hacking to run the extracted Clight semantics.

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