source: driver/clightFromC.ml @ 3368

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

Some null handling in conversion from CIL.

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