clightFromC.ml

   1 (* Based on the prototype --- expect some obsolete definitions to be present *)
   2
   3 open Printf
   4
   5 open Cparser
   6 open Cparser.C
   7 open Cparser.Env
   8
   9 open Extracted.Csyntax
  10 open Extracted.AST
  11 open Extracted.Vector
  12 open Extracted.BitVector
  13
  14 (* Integer conversion *)
  15
  16 let rec convertIntNat n =
  17   if n = 0 then Extracted.Nat.O else Extracted.Nat.S (convertIntNat (n-1))
  18
  19 let rec convertInt64Nat n =
  20   if n = Int64.zero then Extracted.Nat.O else Extracted.Nat.S (convertInt64Nat (Int64.pred n))
  21
  22 let convertBool = function
  23 | true -> Extracted.Bool.True
  24 | false -> Extracted.Bool.False
  25
  26 let 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
  31 let 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
  36 let typeof e = match e with Expr(_,te) -> te
  37
  38 (** Natural alignment of a type, in bytes. *)
  39 let 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
  52 and 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
  58 let align n amount =
  59   ((n + amount - 1) / amount) * amount
  60
  61 let 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
  68 let 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
  82 and 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)
  86 and 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
  93 let decl_atom : (ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103
  94
  95 (** Hooks -- overriden in machine-dependent CPragmas module *)
  96
  97 let process_pragma_hook = ref (fun (s: string) -> false)
  98 let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ())
  99 let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ())
 100 let define_stringlit_hook = ref (fun (id: ident) -> ())
 101
 102 (** ** Error handling *)
 103
 104 let currentLocation = ref Cutil.no_loc
 105
 106 let updateLoc l = currentLocation := l
 107
 108 let numErrors = ref 0
 109
 110 let error msg =
 111   incr numErrors;
 112   eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg
 113
 114 let unsupported msg =
 115   incr numErrors;
 116   eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg
 117
 118 let 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
 126 let idGenerator = ref (Extracted.Identifiers.new_universe Extracted.PreIdentifiers.SymbolTag)
 127 let idTable = Hashtbl.create 47
 128 let symTable = Hashtbl.create 47
 129 let 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
 141 let stringNum = ref 0   (* number of next global for string literals *)
 142 let stringTable = Hashtbl.create 47
 143
 144 let 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
 160 let typeStringLiteral s =
 161   Tarray(Tint(I8, Unsigned), convertIntNat (String.length s + 1))
 162
 163 let 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
 173 let 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
 180 let stub_function_table = Hashtbl.create 47
 181
 182 let 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
 200 let 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
 207 let 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
 220 let 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 (*
 239 let 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
 247 let 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
 315 let rec convertTypList env = function
 316   | [] -> Tnil
 317   | t1 :: tl -> Tcons (convertTyp env t1, convertTypList env tl)
 318
 319 (** Expressions *)
 320
 321 let ezero = Expr(Econst_int(I32, zero (convertIntNat 32)), Tint(I32, Signed))
 322
 323 let is_pointer = function
 324 | Tpointer _ -> true
 325 | _ -> false
 326
 327 let 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
 413 let 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
 419 let rec convertList l =
 420   match l with
 421   | [] -> Extracted.List.Nil
 422   | h::t -> Extracted.List.Cons (h,convertList t)
 423
 424 let 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
 453 let is_volatile_access env e =
 454   List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp)
 455   && Cutil.is_lvalue env e
 456
 457 let 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
 471 let 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
 476 let 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
 483 let 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
 514 type switchlabel =
 515   | Case of C.exp
 516   | Default
 517
 518 type switchbody =
 519   | Label of switchlabel
 520   | Stmt of C.stmt
 521
 522 let 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
 532 let 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
 544 let 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
 592 and 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
 614 let convertProd (x,y) = {Extracted.Types.fst = x; Extracted.Types.snd = y}
 615
 616 let 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
 649 let 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
 659 let 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
 668 let 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
 769 let 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
 787 let 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
 822 let 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
 839 module IdentSet = Set.Make(struct type t = C.ident let compare = compare end)
 840
 841 let 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
 867 let 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
 871 let 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
 897 let 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
 905 let 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
 912 let 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
 919 let 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
 926 let 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
 935 open Builtins
 936
 937 let 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
 981 let builtins =
 982   { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
 983     functions = builtins_generic.functions @ CBuiltins.builtins.functions
 984   }
 985