1 files changed, 741 insertions, 0 deletions

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
new file mode 100644
index 0000000..fcb0c7c
--- /dev/null
+++ b/cfrontend/C2Clight.ml
@@ -0,0 +1,741 @@
+open Printf
+
+open Cparser
+open Cparser.C
+open Cparser.Env
+
+open Camlcoq
+open AST
+open Csyntax
+
+(** Record the declarations of global variables and associate them
+    with the corresponding atom. *)
+
+let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103
+
+(** Hooks -- overriden in machine-dependent CPragmas module *)
+
+let process_pragma_hook = ref (fun (s: string) -> false)
+let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ())
+let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ())
+let define_stringlit_hook = ref (fun (id: ident) -> ())
+
+(** ** Error handling *)
+
+let currentLocation = ref Cutil.no_loc
+
+let updateLoc l = currentLocation := l
+
+let numErrors = ref 0
+
+let error msg =
+  incr numErrors;
+  eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg
+
+let unsupported msg =
+  incr numErrors;
+  eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg
+
+let warning msg =
+  eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg
+
+
+(** ** Functions used to handle string literals *)
+
+let stringNum = ref 0   (* number of next global for string literals *)
+let stringTable = Hashtbl.create 47
+
+let name_for_string_literal env s =
+  try
+    Hashtbl.find stringTable s
+  with Not_found ->
+    incr stringNum;
+    let name = Printf.sprintf "__stringlit_%d" !stringNum in
+    let id = intern_string name in
+    Hashtbl.add decl_atom id
+      (env, (C.Storage_static,
+             Env.fresh_ident name,
+             C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
+             None));
+    !define_stringlit_hook id;
+    Hashtbl.add stringTable s id;
+    id
+
+let typeStringLiteral s =
+  Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1)))
+
+let global_for_string s id =
+  let init = ref [] in
+  let add_char c =
+    init :=
+       AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c)))
+       :: !init in
+  add_char '\000';
+  for i = String.length s - 1 downto 0 do add_char s.[i] done;
+  Datatypes.Coq_pair(Datatypes.Coq_pair(id, !init), typeStringLiteral s)
+
+let globals_for_strings globs =
+  Hashtbl.fold
+    (fun s id l -> global_for_string s id :: l)
+    stringTable globs
+
+(** ** Handling of stubs for variadic functions *)
+
+let stub_function_table = Hashtbl.create 47
+
+let register_stub_function name tres targs =
+  let rec letters_of_type = function
+    | Tnil -> []
+    | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl
+    | Tcons(_, tl) -> "i" :: letters_of_type tl in
+  let stub_name =
+    name ^ "$" ^ String.concat "" (letters_of_type targs) in
+  try
+    (stub_name, Hashtbl.find stub_function_table stub_name)
+  with Not_found ->
+    let rec types_of_types = function
+      | Tnil -> Tnil
+      | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl)
+      | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in
+    let stub_type = Tfunction (types_of_types targs, tres) in
+    Hashtbl.add stub_function_table stub_name stub_type;
+    (stub_name, stub_type)
+
+let declare_stub_function stub_name stub_type =
+  match stub_type with
+  | Tfunction(targs, tres) ->
+      Datatypes.Coq_pair(intern_string stub_name,
+                         External(intern_string stub_name, targs, tres))
+  | _ -> assert false
+
+let declare_stub_functions k =
+  Hashtbl.fold (fun n i k -> declare_stub_function n i :: k)
+               stub_function_table k
+
+(** ** Translation functions *)
+
+(** Constants *)
+
+let convertInt n = coqint_of_camlint(Int64.to_int32 n)
+
+(** Types *)
+
+let convertIkind = function
+  | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8)
+  | C.IChar -> (Unsigned, I8)
+  | C.ISChar -> (Signed, I8)
+  | C.IUChar -> (Unsigned, I8)
+  | C.IInt -> (Signed, I32)
+  | C.IUInt -> (Unsigned, I32)
+  | C.IShort -> (Signed, I16)
+  | C.IUShort -> (Unsigned, I16)
+  | C.ILong -> (Signed, I32)
+  | C.IULong -> (Unsigned, I32)
+  | C.ILongLong -> 
+      if not !Clflags.option_flonglong then unsupported "'long long' type";
+      (Signed, I32)
+  | C.IULongLong ->
+      if not !Clflags.option_flonglong then unsupported "'unsigned long long' type";
+      (Unsigned, I32)
+
+let convertFkind = function
+  | C.FFloat -> F32
+  | C.FDouble -> F64
+  | C.FLongDouble ->
+      if not !Clflags.option_flonglong then unsupported "'long double' type";
+      F64
+
+let convertTyp env t =
+
+  let rec convertTyp seen t =
+    match Cutil.unroll env t with
+    | C.TVoid a -> Tvoid
+    | C.TInt(ik, a) ->
+        let (sg, sz) = convertIkind ik in Tint(sz, sg)
+    | C.TFloat(fk, a) ->
+        Tfloat(convertFkind fk)
+    | C.TPtr(C.TStruct(id, _), _) when List.mem id seen ->
+        Tcomp_ptr(intern_string ("struct " ^ id.name))
+    | C.TPtr(C.TUnion(id, _), _) when List.mem id seen ->
+        Tcomp_ptr(intern_string ("union " ^ id.name))
+    | C.TPtr(ty, a) ->
+        Tpointer(convertTyp seen ty)
+    | C.TArray(ty, None, a) ->
+        warning "array type of unspecified size";
+        Tarray(convertTyp seen ty, coqint_of_camlint 0l)
+    | C.TArray(ty, Some sz, a) ->
+        Tarray(convertTyp seen ty, convertInt sz)
+    | C.TFun(tres, targs, va, a) ->
+        if va then unsupported "variadic function type";
+        if Cutil.is_composite_type env tres then
+          unsupported "return type is a struct or union";
+        Tfunction(begin match targs with
+                  | None -> warning "un-prototyped function type"; Tnil
+                  | Some tl -> convertParams seen tl
+                  end,
+                  convertTyp seen tres)
+    | C.TNamed _ ->
+        assert false
+    | C.TStruct(id, a) ->
+        let flds =
+          try
+            convertFields (id :: seen) (Env.find_struct env id)
+          with Env.Error e ->
+            error (Env.error_message e); Fnil in
+        Tstruct(intern_string("struct " ^ id.name), flds)
+    | C.TUnion(id, a) ->
+        let flds =
+          try
+            convertFields (id :: seen) (Env.find_union env id)
+          with Env.Error e ->
+            error (Env.error_message e); Fnil in
+        Tunion(intern_string("union " ^ id.name), flds)
+
+  and convertParams seen = function
+    | [] -> Tnil
+    | (id, ty) :: rem ->
+        if Cutil.is_composite_type env ty then
+          unsupported "function parameter of struct or union type";
+        Tcons(convertTyp seen ty, convertParams seen rem)
+
+  and convertFields seen ci =
+    convertFieldList seen ci.Env.ci_members
+
+  and convertFieldList seen = function
+    | [] -> Fnil
+    | f :: fl ->
+        if f.fld_bitfield <> None then
+          unsupported "bit field in struct or union";
+        Fcons(intern_string f.fld_name, convertTyp seen f.fld_typ,
+              convertFieldList seen fl)
+
+  in convertTyp [] t
+
+let rec convertTypList env = function
+  | [] -> Tnil
+  | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl)
+
+(** Expressions *)
+
+let ezero = Expr(Econst_int(coqint_of_camlint 0l), Tint(I32, Signed))
+
+let rec convertExpr env e =
+  let ty = convertTyp env e.etyp in
+  match e.edesc with
+  | C.EConst(C.CInt(i, _, _)) ->
+      Expr(Econst_int(convertInt i), ty)
+  | C.EConst(C.CFloat(f, _, _)) ->
+      Expr(Econst_float f, ty)
+  | C.EConst(C.CStr s) ->
+      Expr(Evar(name_for_string_literal env s), typeStringLiteral s)
+  | C.EConst(C.CWStr s) ->
+      unsupported "wide string literal"; ezero
+  | C.EConst(C.CEnum(id, i)) ->
+      Expr(Econst_int(convertInt i), ty)
+
+  | C.ESizeof ty1 ->
+      Expr(Esizeof(convertTyp env ty1), ty)
+  | C.EVar id ->
+      Expr(Evar(intern_string id.name), ty)
+
+  | C.EUnop(C.Oderef, e1) ->
+      Expr(Ederef(convertExpr env e1), ty)
+  | C.EUnop(C.Oaddrof, e1) ->
+      Expr(Eaddrof(convertExpr env e1), ty)
+  | C.EUnop(C.Odot id, e1) ->
+      Expr(Efield(convertExpr env e1, intern_string id), ty)
+  | C.EUnop(C.Oarrow id, e1) ->
+      let e1' = convertExpr env e1 in
+      let ty1 =
+        match typeof e1' with
+        | Tpointer t -> t
+        | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
+      Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
+                  intern_string id), ty)
+  | C.EUnop(C.Oplus, e1) ->
+      convertExpr env e1
+  | C.EUnop(C.Ominus, e1) ->
+      Expr(Eunop(Oneg, convertExpr env e1), ty)
+  | C.EUnop(C.Olognot, e1) ->
+      Expr(Eunop(Onotbool, convertExpr env e1), ty)
+  | C.EUnop(C.Onot, e1) ->
+      Expr(Eunop(Onotint, convertExpr env e1), ty)
+  | C.EUnop(_, _) ->
+      unsupported "pre/post increment/decrement operator"; ezero
+
+  | C.EBinop(C.Oindex, e1, e2, _) ->
+      Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2),
+                       Tpointer ty)), ty)
+  | C.EBinop(C.Ologand, e1, e2, _) ->
+      Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
+  | C.EBinop(C.Ologor, e1, e2, _) ->
+      Expr(Eorbool(convertExpr env e1, convertExpr env e2), ty)
+  | C.EBinop(op, e1, e2, _) ->
+      let op' =
+        match op with
+        | C.Oadd -> Oadd
+        | C.Osub -> Osub
+        | C.Omul -> Omul
+        | C.Odiv -> Odiv
+        | C.Omod -> Omod
+        | C.Oand -> Oand
+        | C.Oor  -> Oor
+        | C.Oxor -> Oxor
+        | C.Oshl -> Oshl
+        | C.Oshr -> Oshr
+        | C.Oeq  -> Oeq
+        | C.One  -> One
+        | C.Olt  -> Olt
+        | C.Ogt  -> Ogt
+        | C.Ole  -> Ole
+        | C.Oge  -> Oge
+        | C.Ocomma -> unsupported "sequence operator"; Oadd
+        | _ -> unsupported "assignment operator"; Oadd in
+      Expr(Ebinop(op', convertExpr env e1, convertExpr env e2), ty)
+  | C.EConditional(e1, e2, e3) ->
+      Expr(Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3), ty)
+  | C.ECast(ty1, e1) ->
+      Expr(Ecast(convertTyp env ty1, convertExpr env e1), ty)
+  | C.ECall _ ->
+      unsupported "function call within expression"; ezero
+
+(* Function calls *)
+
+let rec projFunType env ty =
+  match Cutil.unroll env ty with
+  | TFun(res, args, vararg, attr) -> Some(res, vararg)
+  | TPtr(ty', attr) -> projFunType env ty'
+  | _ -> None
+
+let convertFuncall env lhs fn args =
+  let lhs' =
+    match lhs with None -> None | Some e -> Some(convertExpr env e) in
+  match projFunType env fn.etyp with
+  | None ->
+      error "wrong type for function part of a call"; Sskip
+  | Some(res, false) ->
+      (* Non-variadic function *)
+      Scall(lhs', convertExpr env fn, List.map (convertExpr env) args)
+  | Some(res, true) ->
+      (* Variadic function: generate a call to a stub function with
+         the appropriate number and types of arguments.  Works only if
+         the function expression e is a global variable. *)
+      let fun_name =
+        match fn with
+        | {edesc = C.EVar id} when !Clflags.option_fvararg_calls ->
+            warning "emulating call to variadic function";
+            id.name
+        | _ ->
+            unsupported "call to variadic function";
+            "" in
+      let targs = convertTypList env (List.map (fun e -> e.etyp) args) in
+      let tres = convertTyp env res in
+      let (stub_fun_name, stub_fun_typ) =
+        register_stub_function fun_name tres targs in
+      Scall(lhs',
+            Expr(Evar(intern_string stub_fun_name), stub_fun_typ),
+            List.map (convertExpr env) args)
+
+(* Toplevel expression, argument of an Sdo *)
+
+let convertTopExpr env e =
+  match e.edesc with
+  | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) ->
+      convertFuncall env (Some lhs) fn args
+  | C.EBinop(C.Oassign, lhs, rhs, _) ->
+      Sassign(convertExpr env lhs, convertExpr env rhs)
+  | C.ECall(fn, args) ->
+      convertFuncall env None fn args
+  | _ ->
+      unsupported "illegal toplevel expression"; Sskip
+
+(* Separate the cases of a switch statement body *)
+
+type switchlabel =
+  | Case of C.exp
+  | Default
+
+type switchbody = 
+  | Label of switchlabel
+  | Stmt of C.stmt
+
+let rec flattenSwitch = function
+  | {sdesc = C.Sseq(s1, s2)} ->
+      flattenSwitch s1 @ flattenSwitch s2
+  | {sdesc = C.Slabeled(C.Scase e, s1)} ->
+      Label(Case e) :: flattenSwitch s1
+  | {sdesc = C.Slabeled(C.Sdefault, s1)} ->
+      Label Default :: flattenSwitch s1
+  | s ->
+      [Stmt s]
+
+let rec groupSwitch = function
+  | [] ->
+      (Cutil.sskip, [])
+  | Label case :: rem ->
+      let (fst, cases) = groupSwitch rem in
+      (Cutil.sskip, (case, fst) :: cases)
+  | Stmt s :: rem ->
+      let (fst, cases) = groupSwitch rem in
+      (Cutil.sseq s.sloc s fst, cases)
+
+(* Statement *)
+
+let rec convertStmt env s =
+  updateLoc s.sloc;
+  match s.sdesc with
+  | C.Sskip ->
+      Sskip
+  | C.Sdo e ->
+      convertTopExpr env e
+  | C.Sseq(s1, s2) ->
+      Ssequence(convertStmt env s1, convertStmt env s2)
+  | C.Sif(e, s1, s2) ->
+      Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2)
+  | C.Swhile(e, s1) ->
+      Swhile(convertExpr env e, convertStmt env s1)
+  | C.Sdowhile(s1, e) ->
+      Sdowhile(convertExpr env e, convertStmt env s1)
+  | C.Sfor(s1, e, s2, s3) ->
+      Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2,
+           convertStmt env s3)
+  | C.Sbreak ->
+      Sbreak
+  | C.Scontinue ->
+      Scontinue
+  | C.Sswitch(e, s1) ->
+      let (init, cases) = groupSwitch (flattenSwitch s1) in
+      if cases = [] then
+        unsupported "ill-formed 'switch' statement";
+      if init.sdesc <> C.Sskip then
+        warning "ignored code at beginning of 'switch'";
+      Sswitch(convertExpr env e, convertSwitch env cases)
+  | C.Slabeled(C.Slabel lbl, s1) ->
+      Slabel(intern_string lbl, convertStmt env s1)
+  | C.Slabeled(C.Scase _, _) ->
+      unsupported "'case' outside of 'switch'"; Sskip
+  | C.Slabeled(C.Sdefault, _) ->
+      unsupported "'default' outside of 'switch'"; Sskip
+  | C.Sgoto lbl ->
+      Sgoto(intern_string lbl)
+  | C.Sreturn None ->
+      Sreturn None
+  | C.Sreturn(Some e) ->
+      Sreturn(Some(convertExpr env e))
+  | C.Sblock _ ->
+      unsupported "nested blocks"; Sskip
+  | C.Sdecl _ ->
+      unsupported "inner declarations"; Sskip
+
+and convertSwitch env = function
+  | [] ->
+      LSdefault Sskip
+  | [Default, s] ->
+      LSdefault (convertStmt env s)
+  | (Default, s) :: _ ->
+      updateLoc s.sloc;
+      unsupported "'default' case must occur last";
+      LSdefault Sskip
+  | (Case e, s) :: rem ->
+      updateLoc s.sloc;
+      let v =
+        match Ceval.integer_expr env e with
+        | None -> unsupported "'case' label is not a compile-time integer"; 0L
+        | Some v -> v in
+      LScase(convertInt v,
+             convertStmt env s,
+             convertSwitch env rem)
+
+(** Function definitions *)
+
+let convertFundef env fd =
+  if Cutil.is_composite_type env fd.fd_ret then
+    unsupported "function returning a struct or union";
+  let ret =
+    convertTyp env fd.fd_ret in
+  let params =
+    List.map
+      (fun (id, ty) ->
+        if Cutil.is_composite_type env ty then
+          unsupported "function parameter of struct or union type";
+        Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+      fd.fd_params in
+  let vars =
+    List.map
+      (fun (sto, id, ty, init) ->
+        if sto = Storage_extern || sto = Storage_static then
+          unsupported "'static' or 'extern' local variable";
+        if init <> None then
+          unsupported "initialized local variable";
+        Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+      fd.fd_locals in
+  let body' = convertStmt env fd.fd_body in
+  let id' = intern_string fd.fd_name.name in
+  let decl =
+    (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in
+  Hashtbl.add decl_atom id' (env, decl);
+  !define_function_hook id' decl;
+  Datatypes.Coq_pair(id',
+                     Internal {fn_return = ret; fn_params = params;
+                               fn_vars = vars; fn_body = body'})
+
+(** External function declaration *)
+
+let convertFundecl env (sto, id, ty, optinit) =
+  match convertTyp env ty with
+  | Tfunction(args, res) ->
+      let id' = intern_string id.name in
+      Datatypes.Coq_pair(id', External(id', args, res))
+  | _ ->
+      assert false
+
+(** Initializers *)
+
+let init_data_of_string s =
+  let id = ref [] in
+  let enter_char c =
+    let n = coqint_of_camlint(Int32.of_int(Char.code c)) in
+    id := Init_int8 n :: !id in
+  enter_char '\000';
+  for i = String.length s - 1 downto 0 do enter_char s.[i] done;
+  !id
+
+let convertInit env ty init =
+
+  let k = ref []
+  and pos = ref 0 in
+  let emit size datum =
+    k := datum :: !k;
+    pos := !pos + size in
+  let emit_space size =
+    emit size (Init_space (z_of_camlint (Int32.of_int size))) in
+  let align size =
+    let n = !pos land (size - 1) in
+    if n > 0 then emit_space (size - n) in
+  let check_align size =
+    assert (!pos land (size - 1) = 0) in
+
+  let rec reduceInitExpr = function
+    | { edesc = C.EVar id; etyp = ty } ->
+        begin match Cutil.unroll env ty with
+        | C.TArray _ | C.TFun _ -> Some id
+        | _ -> None
+        end
+    | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id
+    | {edesc = C.ECast(ty, e)} -> reduceInitExpr e
+    | _ -> None in
+
+  let rec cvtInit ty = function
+  | Init_single e ->
+      begin match reduceInitExpr e with
+      | Some id ->
+          check_align 4;
+          emit 4 (Init_addrof(intern_string id.name, coqint_of_camlint 0l))
+      | None ->
+      match Ceval.constant_expr env ty e with
+      | Some(C.CInt(v, ik, _)) ->
+          begin match convertIkind ik with
+          | (_, I8) ->
+              emit 1 (Init_int8(convertInt v))
+          | (_, I16) ->
+              check_align 2;
+              emit 2 (Init_int16(convertInt v))
+          | (_, I32) ->
+              check_align 4;
+              emit 4 (Init_int32(convertInt v))
+          end
+      | Some(C.CFloat(v, fk, _)) ->
+          begin match convertFkind fk with
+          | F32 ->
+              check_align 4;
+              emit 4 (Init_float32 v)
+          | F64 ->
+              check_align 8;
+              emit 8 (Init_float64 v)
+          end
+      | Some(C.CStr s) ->
+          check_align 4;
+          let id = name_for_string_literal env s in
+          emit 4 (Init_addrof(id, coqint_of_camlint 0l))
+      | Some(C.CWStr _) ->
+          unsupported "wide character strings"
+      | Some(C.CEnum _) ->
+          error "enum tag after constant folding"
+      | None ->
+          error "initializer is not a compile-time constant"
+      end
+  | Init_array il ->
+      let ty_elt =
+        match Cutil.unroll env ty with
+        | C.TArray(t, _, _) -> t
+        | _ -> error "array type expected in initializer"; C.TVoid [] in
+      List.iter (cvtInit ty_elt) il
+  | Init_struct(_, flds) ->
+      cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds)
+  | Init_union(_, fld, i) ->
+      cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i))
+
+  and cvtFieldInit (fld, i) =
+    let ty' = convertTyp env fld.fld_typ in
+    let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in
+    align al;
+    cvtInit fld.fld_typ i
+
+  and cvtPadToSizeof ty fn =
+    let ty' = convertTyp env ty in
+    let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in
+    let pos0 = !pos in
+    fn();
+    let pos1 = !pos in
+    assert (pos1 <= pos0 + sz);
+    if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1)
+
+  in cvtInit ty init; List.rev !k
+
+(** Global variable *)
+
+let convertGlobvar env (sto, id, ty, optinit as decl) =
+  let id' = intern_string id.name in
+  let ty' = convertTyp env ty in 
+  let init' =
+    match optinit with
+    | None ->
+        if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')]
+    | Some i ->
+        convertInit env ty i in
+  Hashtbl.add decl_atom id' (env, decl);
+  !define_variable_hook id' decl;
+  Datatypes.Coq_pair(Datatypes.Coq_pair(id', init'), ty')
+
+(** Convert a list of global declarations.
+  Result is a pair [(funs, vars)] where [funs] are 
+  the function definitions (internal and external)
+  and [vars] the variable declarations. *)
+
+let rec convertGlobdecls env funs vars gl =
+  match gl with
+  | [] -> (List.rev funs, List.rev vars)
+  | g :: gl' ->
+      updateLoc g.gloc;
+      match g.gdesc with
+      | C.Gdecl((sto, id, ty, optinit) as d) ->
+          (* Prototyped functions become external declarations.
+             Variadic functions are skipped.
+             Other types become variable declarations. *)
+          begin match Cutil.unroll env ty with
+          | TFun(_, Some _, false, _) ->
+              convertGlobdecls env (convertFundecl env d :: funs) vars gl'
+          | TFun(_, None, false, _) ->
+              error "function declaration without prototype";
+              convertGlobdecls env funs vars gl'
+          | TFun(_, _, true, _) ->
+              convertGlobdecls env funs vars gl'
+          | _ ->
+              convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
+          end
+      | C.Gfundef fd ->
+          convertGlobdecls env (convertFundef env fd :: funs) vars gl'
+      | C.Gcompositedecl _ | C.Gcompositedef _
+      | C.Gtypedef _ | C.Genumdef _ ->
+          (* typedefs are unrolled, structs are expanded inline, and
+             enum tags are folded.  So we just skip their declarations. *)
+          convertGlobdecls env funs vars gl'
+      | C.Gpragma s ->
+          if not (!process_pragma_hook s) then
+            warning ("'#pragma " ^ s ^ "' directive ignored");
+          convertGlobdecls env funs vars gl'
+
+(** Build environment of typedefs and structs *)
+
+let rec translEnv env = function
+  | [] -> env
+  | g :: gl ->
+      let env' =
+        match g.gdesc with
+        | C.Gcompositedecl(su, id) ->
+            Env.add_composite env id
+              {ci_kind = su; ci_incomplete = true;  ci_members = []}
+        | C.Gcompositedef(su, id, fld) ->
+            Env.add_composite env id
+              {ci_kind = su; ci_incomplete = false;  ci_members = fld}
+        | C.Gtypedef(id, ty) ->
+            Env.add_typedef env id ty
+        | _ ->
+            env in
+      translEnv env' gl
+
+(** Eliminate forward declarations of globals that are defined later. *)
+
+module IdentSet = Set.Make(struct type t = C.ident let compare = compare end)
+
+let cleanupGlobals p =
+  
+  let rec clean defs accu = function
+    | [] -> accu
+    | g :: gl ->
+        updateLoc g.gloc;
+        match g.gdesc with
+        | C.Gdecl(sto, id, ty, None) ->
+            if IdentSet.mem id defs
+            then clean defs accu gl
+            else clean (IdentSet.add id defs) (g :: accu) gl
+        | C.Gdecl(_, id, ty, _) ->
+            if IdentSet.mem id defs then
+              error ("multiple definitions of " ^ id.name);
+            clean (IdentSet.add id defs) (g :: accu) gl
+        | C.Gfundef fd ->
+            if IdentSet.mem fd.fd_name defs then
+              error ("multiple definitions of " ^ fd.fd_name.name);
+            clean (IdentSet.add fd.fd_name defs) (g :: accu) gl
+        | _ ->
+            clean defs (g :: accu) gl
+
+  in clean IdentSet.empty [] (List.rev p)
+
+(** Convert a [C.program] into a [Csyntax.program] *)
+
+let convertProgram p =
+  numErrors := 0;
+  stringNum := 0;
+  Hashtbl.clear decl_atom;
+  Hashtbl.clear stringTable;
+  Hashtbl.clear stub_function_table;
+  try
+    let (funs1, vars1) =
+      convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in
+    let funs2 = declare_stub_functions funs1 in
+    let vars2 = globals_for_strings vars1 in
+    if !numErrors > 0
+    then None
+    else Some { AST.prog_funct = funs2;
+                AST.prog_vars = vars2;
+                AST.prog_main = intern_string "main" }
+  with Env.Error msg ->
+    error (Env.error_message msg); None
+
+(** ** Extracting information about global variables from their atom *)
+
+let type_is_readonly env t =
+  let a = Cutil.attributes_of_type env t in
+  if List.mem C.AVolatile a then false else
+  if List.mem C.AConst a then true else
+  match Cutil.unroll env t with
+  | C.TArray(ty, _, _) ->
+      let a' = Cutil.attributes_of_type env ty in
+      List.mem C.AConst a' && not (List.mem C.AVolatile a')
+  | _ ->
+      false
+
+let atom_is_static a =
+  try
+    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
+    sto = C.Storage_static
+  with Not_found ->
+    false
+
+let atom_is_readonly a =
+  try
+    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
+    type_is_readonly env ty
+  with Not_found ->
+    false