diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cil2Csyntax.ml | 992 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 501 |
2 files changed, 1493 insertions, 0 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml new file mode 100644 index 00000000..41fe1d4f --- /dev/null +++ b/cfrontend/Cil2Csyntax.ml @@ -0,0 +1,992 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Thomas Moniot, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(************************************************************************** +CIL -> CabsCoq translator +**************************************************************************) + +open Cil +open CList +open Camlcoq +open AST +open Csyntax + + + + +module type TypeSpecifierTranslator = + sig + val convertIkind: Cil.ikind -> (intsize * signedness) option + val convertFkind: Cil.fkind -> floatsize option + end + + + + + +module Make(TS: TypeSpecifierTranslator) = struct +(*-----------------------------------------------------------------------*) + + +(** Pre-defined constants *) +let constInt32 = Tint (I32, Signed) +let constInt32uns = Tint (I32, Unsigned) +let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32) + + +(** Global variables *) +let currentLocation = ref Cil.locUnknown +let currentGlobalPrefix = ref "" +let stringNum = ref 0 (* number of next global for string literals *) +let stringTable = Hashtbl.create 47 + +(** ** Functions related to [struct]s and [union]s *) + +(* Unroll recursion in struct or union types: + substitute [Tcomp_ptr id] by [Tpointer compty] in [ty]. *) + +let unrollType id compty ty = + let rec unrType ty = + match ty with + | Tvoid -> ty + | Tint(sz, sg) -> ty + | Tfloat sz -> ty + | Tpointer ty -> Tpointer (unrType ty) + | Tarray(ty, sz) -> Tarray (unrType ty, sz) + | Tfunction(args, res) -> Tfunction(unrTypelist args, unrType res) + | Tstruct(id', fld) -> + if id' = id then ty else Tstruct(id', unrFieldlist fld) + | Tunion(id', fld) -> + if id' = id then ty else Tunion(id', unrFieldlist fld) + | Tcomp_ptr id' -> + if id' = id then Tpointer compty else ty + and unrTypelist = function + | Tnil -> Tnil + | Tcons(hd, tl) -> Tcons(unrType hd, unrTypelist tl) + and unrFieldlist = function + | Fnil -> Fnil + | Fcons(id, ty, tl) -> Fcons(id, unrType ty, unrFieldlist tl) + in unrType ty + +(* Return the type of a [struct] field *) +let rec getFieldType f = function + | Fnil -> raise Not_found + | Fcons(idf, t, rem) -> if idf = f then t else getFieldType f rem + +(** ** Some functions over lists *) + +(** Keep the elements in a list from [elt] (included) to the end + (used for the translation of the [switch] statement) *) +let rec keepFrom elt = function + | [] -> [] + | (x :: l) as l' -> if x == elt then l' else keepFrom elt l + +(** Keep the elements in a list before [elt'] (excluded) + (used for the translation of the [switch] statement) *) +let rec keepUntil elt' = function + | [] -> [] + | x :: l -> if x == elt' then [] else x :: (keepUntil elt' l) + +(** Keep the elements in a list from [elt] (included) to [elt'] (excluded) + (used for the translation of the [switch] statement) *) +let keepBetween elt elt' l = + keepUntil elt' (keepFrom elt l) + +(** ** Functions used to handle locations *) + +(** Update the current location *) +let updateLoc loc = + currentLocation := loc + +(** Convert the current location into a string *) +let currentLoc() = + match !currentLocation with { line=l; file=f } -> + f ^ ":" ^ (if l = -1 then "?" else string_of_int l) ^ ": " + +(** Exception raised when an unsupported feature is encountered *) +exception Unsupported of string +let unsupported msg = + raise (Unsupported(currentLoc() ^ "Unsupported C feature: " ^ msg)) + +(** Exception raised when an internal error is encountered *) +exception Internal_error of string +let internal_error msg = + raise (Internal_error(currentLoc() ^ "Internal error: " ^ msg)) + +(** Warning messages *) +let warning msg = + prerr_string (currentLoc()); + prerr_string "Warning: "; + prerr_endline msg + +(** ** Functions used to handle string literals *) +let name_for_string_literal s = + try + Hashtbl.find stringTable s + with Not_found -> + incr stringNum; + let symbol_name = + Printf.sprintf "_%s__stringlit_%d" + !currentGlobalPrefix !stringNum in + let symbol_ident = intern_string symbol_name in + Hashtbl.add stringTable s symbol_ident; + symbol_ident + +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 + +(** ** Generation of temporary variable names *) + +let current_function = ref (None: Cil.fundec option) + +let make_temp typ = + match !current_function with + | None -> assert false + | Some f -> + let v = Cil.makeTempVar f typ in + intern_string v.vname + +(** Detect and report GCC's __builtin_ functions *) + +let check_builtin s = + let b = "__builtin_" in + if String.length s >= String.length b + && String.sub s 0 (String.length b) = b + then unsupported ("GCC `" ^ s ^ "' built-in function") + +(** ** Translation functions *) + +(** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) +let convertIkind ik = + match TS.convertIkind ik with + | Some p -> p + | None -> unsupported "integer type specifier" + + +(** Convert a [Cil.fkind] into a [floatsize] *) +let convertFkind fk = + match TS.convertFkind fk with + | Some fs -> fs + | None -> unsupported "floating-point type specifier" + + +(** Convert a [Cil.constant] into a [CabsCoq.expr] *) +let rec convertConstant = function + | CInt64 (i64, _, _) -> + let i = coqint_of_camlint (Int64.to_int32 i64) in + Expr (Econst_int i, constInt32) + | CStr s -> + let symb = name_for_string_literal s in + Expr (Evar symb, typeStringLiteral s) + | CWStr _ -> + unsupported "wide string literal" + | CChr c -> + let i = coqint_of_camlint (Int32.of_int (Char.code c)) in + Expr (Econst_int i, constInt32) + | CReal (f, _, _) -> + Expr (Econst_float f, Tfloat F64) + | (CEnum (exp, str, enumInfo)) as enum -> + (* do constant folding on an enum constant *) + let e = Cil.constFold false (Const enum) in + convertExp e + + +(** Convert a [Cil.UnOp] into a [CabsCoq.expr] + ([t] is the type of the result of applying [uop] to [e]) *) +and convertUnop uop e t = + let e' = convertExp e in + let t' = convertTyp t in + let uop' = match uop with + | Neg -> Eunop (Oneg, e') + | BNot -> Eunop (Onotint, e') + | LNot -> Eunop (Onotbool, e') + in + Expr (uop', t') + + +(** Convert a [Cil.BinOp] into a [CabsCoq.expr] + ([t] is the type of the result of applying [bop] to [(e1, e2)], every + arithmetic conversion being made explicit by CIL for both arguments] *) +and convertBinop bop e1 e2 t = + let e1' = convertExp e1 in + let e2' = convertExp e2 in + let t' = convertTyp t in + let bop' = match bop with + | PlusA -> Ebinop (Oadd, e1', e2') + | PlusPI -> Ebinop (Oadd, e1', e2') + | IndexPI -> Ebinop (Oadd, e1', e2') + | MinusA -> Ebinop (Osub, e1', e2') + | MinusPI -> Ebinop (Osub, e1', e2') + | MinusPP -> Ebinop (Osub, e1', e2') + | Mult -> Ebinop (Omul, e1', e2') + | Div -> Ebinop (Odiv, e1', e2') + | Mod -> Ebinop (Omod, e1', e2') + | Shiftlt -> Ebinop (Oshl, e1', e2') + | Shiftrt -> Ebinop (Oshr, e1', e2') + | Lt -> Ebinop (Olt, e1', e2') + | Gt -> Ebinop (Ogt, e1', e2') + | Le -> Ebinop (Ole, e1', e2') + | Ge -> Ebinop (Oge, e1', e2') + | Eq -> Ebinop (Oeq, e1', e2') + | Ne -> Ebinop (One, e1', e2') + | BAnd -> Ebinop (Oand, e1', e2') + | BXor -> Ebinop (Oxor, e1', e2') + | BOr -> Ebinop (Oor, e1', e2') + | LAnd -> Eandbool (e1', e2') + | LOr -> Eorbool (e1', e2') + in + Expr (bop', t') + + +(** Test if two types are compatible + (in order to cast one of the types to the other) *) +and compatibleTypes t1 t2 = true +(* + let isArithmeticType = function + | Tint _ | Tfloat _ -> true + | _ -> false + in + let isPointerType = function + | Tpointer _ | Tarray _ -> true + | _ -> false + in + (t1 = t2) + || (isArithmeticType t1 && isArithmeticType t2) + || match (t1, t2) with + | (Tpointer Tvoid, t) | (t, Tpointer Tvoid) -> isPointerType t + | (Tint _, t) | (t, Tint _) -> isPointerType t + | _ -> false +*) + + +(** Convert a [Cil.CastE] into a [CabsCoq.expr] + (fail if the cast is illegal) *) +and processCast t e = + let t' = convertTyp t in + let te = convertTyp (Cil.typeOf e) in + if compatibleTypes t' te then + let e' = convertExp e in + Expr (Ecast (t', e'), t') + else internal_error "processCast: illegal cast" + + +(** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *) +and processParamsE = function + | [] -> [] + | e :: l -> + let (Expr (_, t)) as e' = convertExp e in + match t with + | Tstruct _ | Tunion _ -> + unsupported "function parameter of struct or union type" + | _ -> e' :: processParamsE l + + +(** Convert a [Cil.exp] into a [CabsCoq.expr] *) +and convertExp = function + | Const c -> + convertConstant c + | Lval lv -> + convertLval lv + | SizeOf t -> + Expr (Esizeof (convertTyp t), constInt32uns) + | SizeOfE e -> + let ty = convertTyp (Cil.typeOf e) in + Expr (Esizeof ty, constInt32uns) + | SizeOfStr str -> + let n = coqint_of_camlint (Int32.of_int(String.length str)) in + Expr (Econst_int n, constInt32uns) + | AlignOf t -> + unsupported "GCC `alignof' construct" + | AlignOfE e -> + unsupported "GCC `alignof' construct" + | UnOp (uop, e, t) -> + convertUnop uop e t + | BinOp (bop, e1, e2, t) -> + convertBinop bop e1 e2 t + | CastE (t, e) -> + processCast t e + | AddrOf lv -> + let (Expr (_, t)) as e = convertLval lv in + Expr (Eaddrof e, Tpointer t) + | StartOf lv -> + (* convert an array into a pointer to the beginning of the array *) + match Cil.unrollType (Cil.typeOfLval lv) with + | TArray (t, _, _) -> + let t' = convertTyp t in + let tPtr = Tpointer t' in + let e = convertLval lv in + (* array A of type T replaced by (T* )A *) + Expr (Ecast (tPtr, e), tPtr) + | _ -> internal_error "convertExp: StartOf applied to a \ + lvalue whose type is not an array" + + +(** Convert a [Cil.lval] into a [CabsCoq.expression] *) +and convertLval lv = + (* convert the offset of the lvalue *) + let rec processOffset ((Expr (_, t)) as e) = function + | NoOffset -> e + | Field (f, ofs) -> + begin match t with + | Tstruct(id, fList) -> + begin try + let idf = intern_string f.fname in + let t' = unrollType id t (getFieldType idf fList) in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + internal_error "processOffset: no such struct field" + end + | Tunion(id, fList) -> + begin try + let idf = intern_string f.fname in + let t' = unrollType id t (getFieldType idf fList) in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + internal_error "processOffset: no such union field" + end + | _ -> + internal_error "processOffset: Field on a non-struct nor union" + end + | Index (e', ofs) -> + match t with + | Tarray (t', _) -> + let e'' = Ederef(Expr (Ebinop(Oadd, e, convertExp e'), t)) in + processOffset (Expr (e'', t')) ofs + | _ -> internal_error "processOffset: Index on a non-array" + in + (* convert the lvalue *) + match lv with + | (Var v, ofs) -> + check_builtin v.vname; + let id = intern_string v.vname in + processOffset (Expr (Evar id, convertTyp v.vtype)) ofs + | (Mem e, ofs) -> + match Cil.unrollType (Cil.typeOf e) with + | TPtr (t, _) -> let e' = Ederef (convertExp e) in + processOffset (Expr (e', convertTyp t)) ofs + | _ -> internal_error "convertLval: Mem on a non-pointer" + + +(** Convert a [(Cil.string * Cil.typ * Cil.attributes)] list + into a [typelist] *) +and processParamsT convert = function + | [] -> Tnil + | (_, t, _) :: l -> + let t' = convert t in + match t' with + | Tstruct _ | Tunion _ -> + unsupported "function parameter of struct or union type" + | _ -> Tcons (t', processParamsT convert l) + + +(** Convert a [Cil.typ] into a [coq_type] *) +and convertTypGen env = function + | TVoid _ -> Tvoid + | TInt (k, _) -> let (x, y) = convertIkind k in Tint (x, y) + | TFloat (k, _) -> Tfloat (convertFkind k) + | TPtr (TComp(c, _), _) when List.mem c.ckey env -> + Tcomp_ptr (intern_string (Cil.compFullName c)) + | TPtr (t, _) -> Tpointer (convertTypGen env t) + | TArray (t, eOpt, _) -> + begin match eOpt with + | None -> + warning "array type of unspecified size"; + Tarray (convertTypGen env t, coqint_of_camlint 0l) + | Some e -> + match Cil.constFold true e with + | Const (CInt64 (i64, _, _)) -> + Tarray (convertTypGen env t, + coqint_of_camlint (Int64.to_int32 i64)) + | _ -> unsupported "size of array type not an integer constant" + end + | TFun (t, argListOpt, vArg, _) -> + if vArg then unsupported "variadic function type"; + let argList = + match argListOpt with + | None -> unsupported "un-prototyped function type" + | Some l -> l + in + let t' = convertTypGen env t in + begin match t' with + | Tstruct _ | Tunion _ -> + unsupported "return type is a struct or union" + | _ -> Tfunction (processParamsT (convertTypGen env) argList, t') + end + | TNamed (tinfo, _) -> convertTypGen env tinfo.ttype + | TComp (c, _) -> + let rec convertFieldList = function + | [] -> Fnil + | {fname=str; ftype=t} :: rem -> + let idf = intern_string str in + let t' = convertTypGen (c.ckey :: env) t in + Fcons(idf, t', convertFieldList rem) in + let fList = convertFieldList c.cfields in + let id = intern_string (Cil.compFullName c) in + if c.cstruct then Tstruct(id, fList) else Tunion(id, fList) + | TEnum _ -> constInt32 (* enum constants are integers *) + | TBuiltin_va_list _ -> unsupported "GCC `builtin va_list' type" + +and convertTyp ty = convertTypGen [] ty + +(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] *) +let convertVarinfo v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (id, convertTyp v.vtype) + + +(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] + (fail if the variable is of type struct or union) *) +let convertVarinfoParam v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + let t' = convertTyp v.vtype in + match t' with + | Tstruct _ | Tunion _ -> + unsupported "function parameter of struct or union type" + | _ -> Datatypes.Coq_pair (id, t') + + +(** Convert a [Cil.exp] which has a function type into a [CabsCoq.expr] + (used only to translate function calls) *) +let convertExpFuncall e eList = + match typeOf e with + | TFun (res, argListOpt, vArg, _) -> + begin match argListOpt, vArg with + | Some argList, false -> + (* Prototyped, non-variadic function *) + if List.length argList <> List.length eList then + internal_error "convertExpFuncall: wrong number of arguments"; + (convertExp e, processParamsE eList) + | _, _ -> + (* Variadic or unprototyped 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 params = processParamsE eList in + let fun_name = + match e with + | Lval(Var v, NoOffset) -> + warning "working around a call to a variadic function"; + v.vname + | _ -> + unsupported "call to variadic function" in + let rec typeOfExprList = function + | [] -> Tnil + | Expr (_, ty) :: rem -> Tcons (ty, typeOfExprList rem) in + let targs = typeOfExprList params in + let tres = convertTyp res in + let (stub_fun_name, stub_fun_typ) = + register_stub_function fun_name tres targs in + (Expr(Evar(intern_string stub_fun_name), stub_fun_typ), + params) + end + | _ -> internal_error "convertExpFuncall: not a function" + +(** Auxiliaries for function calls *) + +let makeFuncall1 tyfun (Expr(_, tlhs) as elhs) efun eargs = + match tyfun with + | TFun (t, _, _, _) -> + let tres = convertTyp t in + if tlhs = tres then + Scall(Datatypes.Some elhs, efun, eargs) + else begin + let tmp = make_temp t in + let elhs' = Expr(Evar tmp, tres) in + Ssequence(Scall(Datatypes.Some elhs', efun, eargs), + Sassign(elhs, Expr(Ecast(tlhs, elhs'), tlhs))) + end + | _ -> internal_error "wrong type for function in call" + +let makeFuncall2 tyfun tylhs elhs efun eargs = + match elhs with + | Expr(Evar _, _) -> + makeFuncall1 tyfun elhs efun eargs + | Expr(_, tlhs) -> + let tmp = make_temp tylhs in + let elhs' = Expr(Evar tmp, tlhs) in + Ssequence(makeFuncall1 tyfun elhs' efun eargs, + Sassign(elhs, elhs')) + + +(** Convert a [Cil.instr list] into a [CabsCoq.statement] *) +let rec processInstrList l = + (* convert an instruction *) + let convertInstr = function + | Set (lv, e, loc) -> + updateLoc(loc); + begin match convertTyp (Cil.typeOf e) with + | Tstruct _ | Tunion _ -> unsupported "struct or union assignment" + | t -> Sassign (convertLval lv, convertExp e) + end + | Call (None, e, eList, loc) -> + updateLoc(loc); + let (efun, params) = convertExpFuncall e eList in + Scall(Datatypes.None, efun, params) + | Call (Some lv, e, eList, loc) -> + updateLoc(loc); + let (efun, params) = convertExpFuncall e eList in + makeFuncall2 (Cil.typeOf e) (Cil.typeOfLval lv) (convertLval lv) efun params + | Asm (_, _, _, _, _, loc) -> + updateLoc(loc); + unsupported "inline assembly" + in + (* convert a list of instructions *) + match l with + | [] -> Sskip + | [s] -> convertInstr s + | s :: l -> + let cs = convertInstr s in + let cl = processInstrList l in + Ssequence (cs, cl) + + +(** Convert a [Cil.stmt list] into a [CabsCoq.statement] *) +let rec processStmtList = function + | [] -> Sskip + | [s] -> convertStmt s + | s :: l -> + let cs = convertStmt s in + let cl = processStmtList l in + Ssequence (cs, cl) + + +(** Return the list of the constant expressions in a label list + (return [None] if this is the default case) + (fail if the constant expression is not of type integer) *) +and getCaseList lblList = + match lblList with + | [] -> Some [] + | Label (_, loc, _) :: l -> updateLoc(loc); getCaseList l + | Default loc :: _ -> updateLoc(loc); None + | Case (e, loc) :: l -> + updateLoc(loc); + begin match convertExp e with + | Expr (Econst_int n, _) -> + begin match getCaseList l with + | None -> None + | Some cl -> Some (n :: cl) + end + | _ -> internal_error "getCaseList: case label does not \ + reduce to an integer constant" + end + + +(** Convert a list of integers into a [CabsCoq.lblStatementList] *) +and processCaseList cl s lrem = + match cl with + | [] -> internal_error "processCaseList: syntax error in switch statement" + | [n] -> LScase (n, s, lrem) + | n1 :: l -> LScase (n1, Sskip, processCaseList l s lrem) + + +(** Convert a [Cil.stmt list] which is the body of a Switch structure + into a [CabsCoq.lblStatementList] + (Pre-condition: all the Case labels are supposed to be at the same level, + ie. no nested structures) *) +and processLblStmtList switchBody = function + | [] -> LSdefault Sskip + | [ls] -> + let s = processStmtList (keepFrom ls switchBody) in + begin match getCaseList ls.labels with + | None -> LSdefault s + | Some cl -> processCaseList cl s (LSdefault Sskip) + end + | ls :: ((ls' :: _) as l) -> + if ls.labels = ls'.labels then processLblStmtList switchBody l + else + begin match getCaseList ls.labels with + | None -> unsupported "default case is not at the end of this `switch' statement" + | Some cl -> + let s = processStmtList (keepBetween ls ls' switchBody) in + let lrem = processLblStmtList switchBody l in + processCaseList cl s lrem + end + + +(** Convert a [Cil.stmt] into a [CabsCoq.statement] *) +and convertStmt s = + match s.skind with + | Instr iList -> processInstrList iList + | Return (eOpt, loc) -> + updateLoc(loc); + let eOpt' = match eOpt with + | None -> Datatypes.None + | Some e -> Datatypes.Some (convertExp e) + in + Sreturn eOpt' + | Goto (_, loc) -> + updateLoc(loc); + unsupported "`goto' statement" + | Break loc -> + updateLoc(loc); + Sbreak + | Continue loc -> + updateLoc(loc); + Scontinue + | If (e, b1, b2, loc) -> + updateLoc(loc); + let e1 = processStmtList b1.bstmts in + let e2 = processStmtList b2.bstmts in + Sifthenelse (convertExp e, e1, e2) + | Switch (e, b, l, loc) -> + updateLoc(loc); + Sswitch (convertExp e, processLblStmtList b.bstmts l) + | While (e, b, loc) -> + updateLoc(loc); + Swhile (convertExp e, processStmtList b.bstmts) + | DoWhile (e, b, loc) -> + updateLoc(loc); + Sdowhile (convertExp e, processStmtList b.bstmts) + | For (bInit, e, bIter, b, loc) -> + updateLoc(loc); + let sInit = processStmtList bInit.bstmts in + let e' = convertExp e in + let sIter = processStmtList bIter.bstmts in + Sfor (sInit, e', sIter, processStmtList b.bstmts) + | Block b -> processStmtList b.bstmts + | TryFinally (_, _, loc) -> + updateLoc(loc); + unsupported "`try'...`finally' statement" + | TryExcept (_, _, _, loc) -> + updateLoc(loc); + unsupported "`try'...`except' statement" + +(** Convert a [Cil.GFun] into a pair [(ident * coq_fundecl)] *) +let convertGFun fdec = + current_function := Some fdec; + let v = fdec.svar in + let ret = match v.vtype with + | TFun (t, _, vArg, _) -> + if vArg then unsupported "variadic function"; + begin match convertTyp t with + | Tstruct _ | Tunion _ -> + unsupported "return value of struct or union type" + | t' -> t' + end + | _ -> internal_error "convertGFun: incorrect function type" + in + let s = processStmtList fdec.sbody.bstmts in (* function body -- do it first because of generated temps *) + let args = List.map convertVarinfoParam fdec.sformals in (* parameters*) + let varList = List.map convertVarinfo fdec.slocals in (* local vars *) + if v.vname = "main" then begin + match ret with + | Tint(_, _) -> () + | _ -> updateLoc v.vdecl; + unsupported "the return type of main() must be an integer type" + end; + current_function := None; + Datatypes.Coq_pair + (intern_string v.vname, + Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s }) + +(** Auxiliary for [convertInit] *) + +let rec initDataLen accu = function + | [] -> accu + | i1 :: il -> + let sz = match i1 with + | Init_int8 _ -> 1l + | Init_int16 _ -> 2l + | Init_int32 _ -> 4l + | Init_float32 _ -> 4l + | Init_float64 _ -> 8l + | Init_space n -> camlint_of_z n + | Init_pointer _ -> 4l in + initDataLen (Int32.add sz accu) il + +(** Convert a [Cil.init] into a list of [AST.init_data] prepended to + the given list [k]. Result is in reverse order. *) + +(* Cil.constFold does not reduce floating-point operations. + We treat here those that appear naturally in initializers. *) + +type init_constant = + | ICint of int64 * intsize + | ICfloat of float * floatsize + | ICstring of string + | ICnone + +let rec extract_constant e = + match e with + | Const (CInt64(n, ikind, _)) -> + ICint(n, fst (convertIkind ikind)) + | Const (CReal(n, fkind, _)) -> + ICfloat(n, convertFkind fkind) + | Const (CStr s) -> + ICstring s + | CastE (ty, e1) -> + begin match extract_constant e1, convertTyp ty with + | ICfloat(n, _), Tfloat sz -> + ICfloat(n, sz) + | ICint(n, _), Tfloat sz -> + ICfloat(Int64.to_float n, sz) + | ICint(n, sz), Tpointer _ -> + ICint(n, sz) + | ICstring s, (Tint _ | Tpointer _) -> + ICstring s + | _, _ -> + ICnone + end + | UnOp (Neg, e1, _) -> + begin match extract_constant e1 with + | ICfloat(n, sz) -> ICfloat(-. n, sz) + | _ -> ICnone + end + | _ -> ICnone + +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 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 check_align size = + assert (!pos land (size - 1) = 0) in + let align size = + let n = !pos land (size - 1) in + if n > 0 then emit_space (size - n) in + + let rec cvtInit init = + match init with + | SingleInit e -> + begin match extract_constant(Cil.constFold true e) with + | ICint(n, I8) -> + let n' = coqint_of_camlint (Int64.to_int32 n) in + emit 1 (Init_int8 n') + | ICint(n, I16) -> + check_align 2; + let n' = coqint_of_camlint (Int64.to_int32 n) in + emit 2 (Init_int16 n') + | ICint(n, I32) -> + check_align 4; + let n' = coqint_of_camlint (Int64.to_int32 n) in + emit 4 (Init_int32 n') + | ICfloat(n, F32) -> + check_align 4; + emit 4 (Init_float32 n) + | ICfloat(n, F64) -> + check_align 8; + emit 8 (Init_float64 n) + | ICstring s -> + check_align 4; + emit 4 (Init_pointer(init_data_of_string s)) + | ICnone -> + unsupported "this kind of expression is not supported in global initializers" + end + | CompoundInit(ty, data) -> + let ty' = convertTyp ty in + let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in + let pos0 = !pos in + Cil.foldLeftCompoundAll + ~doinit: cvtCompoundInit + ~ct: ty + ~initl: data + ~acc: (); + let pos1 = !pos in + assert (pos1 <= pos0 + sz); + if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1) + + and cvtCompoundInit ofs init ty () = + let ty' = convertTyp ty in + let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in + align al; + cvtInit init + + in cvtInit init; CList.rev !k + +(** Convert a [Cil.initinfo] into a list of [AST.init_data] *) + +let convertInitInfo ty info = + match info.init with + | None -> + [ Init_space(Csyntax.sizeof (convertTyp ty)) ] + | Some init -> + convertInit init + +(** Convert a [Cil.GVar] into a global variable definition *) + +let convertGVar v i = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i), + convertTyp v.vtype) + + +(** Convert a [Cil.GVarDecl] into a global variable declaration *) + +let convertExtVar v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (Datatypes.Coq_pair(id, []), + convertTyp v.vtype) + +(** Convert a [Cil.GVarDecl] into an external function declaration *) + +let convertExtFun v = + updateLoc(v.vdecl); + match convertTyp v.vtype with + | Tfunction(args, res) -> + let id = intern_string v.vname in + Datatypes.Coq_pair (id, External(id, args, res)) + | _ -> + assert false + +(** Convert a [Cil.global list] into a pair whose first component, + of type [(ident * coq_function) coqlist], represents the definitions of the + functions and the second component, of type [(ident * coq_type) coqlist], + the definitions of the global variables of the program *) +let rec processGlobals = function + | [] -> ([], []) + | g :: l -> + match g with + | GType _ -> processGlobals l (* typedefs are unrolled... *) + | GCompTag _ -> processGlobals l + | GCompTagDecl _ -> processGlobals l + | GEnumTag _ -> processGlobals l (* enum constants are folded... *) + | GEnumTagDecl _ -> processGlobals l + | GVarDecl (v, loc) -> + updateLoc(loc); + (* Functions become external declarations, + variadic and unprototyped functions are skipped, + variables become uninitialized variables *) + begin match Cil.unrollType v.vtype with + | TFun (tres, Some targs, false, _) -> + let fn = convertExtFun v in + let (fList, vList) = processGlobals l in + (fn :: fList, vList) + | TFun (tres, _, _, _) -> + processGlobals l + | _ -> + let var = convertExtVar v in + let (fList, vList) = processGlobals l in + (fList, var :: vList) + end + | GVar (v, init, loc) -> + updateLoc(loc); + let var = convertGVar v init in + let (fList, vList) = processGlobals l in + (fList, var :: vList) + | GFun (fdec, loc) -> + updateLoc(loc); + let fn = convertGFun fdec in + let (fList, vList) = processGlobals l in + (fn :: fList, vList) + | GAsm (_, loc) -> + updateLoc(loc); + unsupported "inline assembly" + | GPragma (_, loc) -> + updateLoc(loc); + warning "#pragma directive ignored"; + processGlobals l + | GText _ -> processGlobals l (* comments are ignored *) + +(** Eliminate forward declarations of globals that are defined later *) + +let cleanupGlobals globs = + let defined = + List.fold_right + (fun g def -> + match g with GVar (v, init, loc) -> v.vname :: def + | GFun (fdec, loc) -> fdec.svar.vname :: def + | _ -> def) + globs [] in + List.filter + (function GVarDecl(v, loc) -> not(List.mem v.vname defined) + | g -> true) + globs + +(** Convert a [Cil.file] into a [CabsCoq.program] *) +let convertFile f = + currentGlobalPrefix := + Filename.chop_extension (Filename.basename f.fileName); + stringNum := 0; + Hashtbl.clear stringTable; + Hashtbl.clear stub_function_table; + let (funList, defList) = processGlobals (cleanupGlobals f.globals) in + let funList' = declare_stub_functions funList in + let funList'' = match f.globinit with + | Some fdec -> convertGFun fdec :: funList' + | None -> funList' in + let defList' = globals_for_strings defList in + { AST.prog_funct = funList''; + AST.prog_vars = defList'; + AST.prog_main = intern_string "main" } + + +(*-----------------------------------------------------------------------*) +end + diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml new file mode 100644 index 00000000..bb25339a --- /dev/null +++ b/cfrontend/PrintCsyntax.ml @@ -0,0 +1,501 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printer for Csyntax *) + +open Format +open Camlcoq +open CList +open Datatypes +open AST +open Csyntax + +let name_unop = function + | Onotbool -> "!" + | Onotint -> "~" + | Oneg -> "-" + + +let name_binop = function + | Oadd -> "+" + | Osub -> "-" + | Omul -> "*" + | Odiv -> "/" + | Omod -> "%" + | Oand -> "&" + | Oor -> "|" + | Oxor -> "^" + | Oshl -> "<<" + | Oshr -> ">>" + | Oeq -> "==" + | One -> "!=" + | Olt -> "<" + | Ogt -> ">" + | Ole -> "<=" + | Oge -> ">=" + +let name_inttype sz sg = + match sz, sg with + | I8, Signed -> "signed char" + | I8, Unsigned -> "unsigned char" + | I16, Signed -> "short" + | I16, Unsigned -> "unsigned short" + | I32, Signed -> "int" + | I32, Unsigned -> "unsigned int" + +let name_floattype sz = + match sz with + | F32 -> "float" + | F64 -> "double" + +(* Collecting the names and fields of structs and unions *) + +module StructUnionSet = Set.Make(struct + type t = string * fieldlist + let compare (n1, _ : t) (n2, _ : t) = compare n1 n2 +end) + +let struct_unions = ref StructUnionSet.empty + +let register_struct_union id fld = + struct_unions := StructUnionSet.add (extern_atom id, fld) !struct_unions + +(* Declarator (identifier + type) *) + +let name_optid id = + if id = "" then "" else " " ^ id + +let parenthesize_if_pointer id = + if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id + +let rec name_cdecl id ty = + match ty with + | Tvoid -> + "void" ^ name_optid id + | Tint(sz, sg) -> + name_inttype sz sg ^ name_optid id + | Tfloat sz -> + name_floattype sz ^ name_optid id + | Tpointer t -> + name_cdecl ("*" ^ id) t + | Tarray(t, n) -> + name_cdecl + (sprintf "%s[%ld]" (parenthesize_if_pointer id) (camlint_of_coqint n)) + t + | Tfunction(args, res) -> + let b = Buffer.create 20 in + if id = "" + then Buffer.add_string b "(*)" + else Buffer.add_string b (parenthesize_if_pointer id); + Buffer.add_char b '('; + begin match args with + | Tnil -> + Buffer.add_string b "void" + | _ -> + let rec add_args first = function + | Tnil -> () + | Tcons(t1, tl) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl "" t1); + add_args false tl in + add_args true args + end; + Buffer.add_char b ')'; + name_cdecl (Buffer.contents b) res + | Tstruct(name, fld) -> + extern_atom name ^ name_optid id + | Tunion(name, fld) -> + extern_atom name ^ name_optid id + | Tcomp_ptr name -> + extern_atom name ^ " *" ^ id + +(* Type *) + +let name_type ty = name_cdecl "" ty + +(* Expressions *) + +let parenthesis_level (Expr (e, ty)) = + match e with + | Econst_int _ -> 0 + | Econst_float _ -> 0 + | Evar _ -> 0 + | Eunop(_, _) -> 30 + | Ederef _ -> 20 + | Eaddrof _ -> 30 + | Ebinop(op, _, _) -> + begin match op with + | Oand | Oor | Oxor -> 75 + | Oeq | One | Olt | Ogt | Ole | Oge -> 70 + | Oadd | Osub | Oshl | Oshr -> 60 + | Omul | Odiv | Omod -> 40 + end + | Ecast _ -> 30 + | Econdition(_, _, _) -> 80 + | Eandbool(_, _) -> 80 + | Eorbool(_, _) -> 80 + | Esizeof _ -> 20 + | Efield _ -> 20 + +let rec print_expr p (Expr (eb, ty) as e) = + let level = parenthesis_level e in + match eb with + | Econst_int n -> + fprintf p "%ld" (camlint_of_coqint n) + | Econst_float f -> + fprintf p "%F" f + | Evar id -> + fprintf p "%s" (extern_atom id) + | Eunop(op, e1) -> + fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1) + | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) -> + fprintf p "@[<hov 2>%a@,[%a]@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Ederef (Expr (Efield(e1, id), _)) -> + fprintf p "%a->%s" print_expr_prec (level, e1) (extern_atom id) + | Ederef e -> + fprintf p "*%a" print_expr_prec (level, e) + | Eaddrof e -> + fprintf p "&%a" print_expr_prec (level, e) + | Ebinop(op, e1, e2) -> + fprintf p "@[<hov 0>%a@ %s %a@]" + print_expr_prec (level, e1) + (name_binop op) + print_expr_prec (level, e2) + | Ecast(ty, e1) -> + fprintf p "@[<hov 2>(%s)@,%a@]" + (name_type ty) + print_expr_prec (level, e1) + | Econdition(e1, e2, e3) -> + fprintf p "@[<hov 0>%a@ ? %a@ : %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + print_expr_prec (level, e3) + | Eandbool(e1, e2) -> + fprintf p "@[<hov 0>%a@ && %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Eorbool(e1, e2) -> + fprintf p "@[<hov 0>%a@ || %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Esizeof ty -> + fprintf p "sizeof(%s)" (name_type ty) + | Efield(e1, id) -> + fprintf p "%a.%s" print_expr_prec (level, e1) (extern_atom id) + +and print_expr_prec p (context_prec, e) = + let this_prec = parenthesis_level e in + if this_prec >= context_prec + then fprintf p "(%a)" print_expr e + else print_expr p e + +let rec print_expr_list p (first, el) = + match el with + | [] -> () + | e1 :: et -> + if not first then fprintf p ",@ "; + print_expr p e1; + print_expr_list p (false, et) + +let rec print_stmt p s = + match s with + | Sskip -> + fprintf p "/*skip*/;" + | Sassign(e1, e2) -> + fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2 + | Scall(None, e1, el) -> + fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]" + print_expr e1 + print_expr_list (true, el) + | Scall(Some lhs, e1, el) -> + fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]" + print_expr lhs + print_expr e1 + print_expr_list (true, el) + | Ssequence(s1, s2) -> + fprintf p "%a@ %a" print_stmt s1 print_stmt s2 + | Sifthenelse(e, s1, Sskip) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Swhile(e, s) -> + fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s + | Sdowhile(e, s) -> + fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]" + print_stmt s + print_expr e + | Sfor(s_init, e, s_iter, s_body) -> + fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" + print_stmt_for s_init + print_expr e + print_stmt_for s_iter + print_stmt s_body + | Sbreak -> + fprintf p "break;" + | Scontinue -> + fprintf p "continue;" + | Sswitch(e, cases) -> + fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_cases cases + | Sreturn None -> + fprintf p "return;" + | Sreturn (Some e) -> + fprintf p "return %a;" print_expr e + +and print_cases p cases = + match cases with + | LSdefault Sskip -> + () + | LSdefault s -> + fprintf p "@[<v 2>default:@ %a@]" print_stmt s + | LScase(lbl, Sskip, rem) -> + fprintf p "case %ld:@ %a" + (camlint_of_coqint lbl) + print_cases rem + | LScase(lbl, s, rem) -> + fprintf p "@[<v 2>case %ld:@ %a@]@ %a" + (camlint_of_coqint lbl) + print_stmt s + print_cases rem + +and print_stmt_for p s = + match s with + | Sskip -> + fprintf p "/*nothing*/" + | Sassign(e1, e2) -> + fprintf p "%a = %a" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2 + | Scall(None, e1, el) -> + fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@]" + print_expr e1 + print_expr_list (true, el) + | Scall(Some lhs, e1, el) -> + fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]" + print_expr lhs + print_expr e1 + print_expr_list (true, el) + | _ -> + fprintf p "({ %a })" print_stmt s + +let name_function_parameters fun_name params = + let b = Buffer.create 20 in + Buffer.add_string b fun_name; + Buffer.add_char b '('; + begin match params with + | [] -> + Buffer.add_string b "void" + | _ -> + let rec add_params first = function + | [] -> () + | Coq_pair(id, ty) :: rem -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl (extern_atom id) ty); + add_params false rem in + add_params true params + end; + Buffer.add_char b ')'; + Buffer.contents b + +let print_function p id f = + fprintf p "%s@ " + (name_cdecl (name_function_parameters (extern_atom id) + f.fn_params) + f.fn_return); + fprintf p "@[<v 2>{@ "; + List.iter + (fun (Coq_pair(id, ty)) -> + fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) + f.fn_vars; + print_stmt p f.fn_body; + fprintf p "@;<0 -2>}@]@ @ " + +let print_fundef p (Coq_pair(id, fd)) = + match fd with + | External(_, args, res) -> + fprintf p "extern %s;@ @ " + (name_cdecl (extern_atom id) (Tfunction(args, res))) + | Internal f -> + print_function p id f + +let string_of_init id = + try + let s = String.create (List.length id) in + let i = ref 0 in + List.iter + (function + | Init_int8 n -> + s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n)); + incr i + | _ -> raise Not_found) + id; + Some s + with Not_found -> None + +let print_escaped_string p s = + fprintf p "\""; + for i = 0 to String.length s - 1 do + match s.[i] with + | ('\"' | '\\') as c -> fprintf p "\\%c" c + | '\n' -> fprintf p "\\n" + | '\t' -> fprintf p "\\t" + | '\r' -> fprintf p "\\r" + | c -> if c >= ' ' && c <= '~' + then fprintf p "%c" c + else fprintf p "\\x%02x" (Char.code c) + done; + fprintf p "\"" + +let print_init p = function + | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_float32 n -> fprintf p "%F,@ " n + | Init_float64 n -> fprintf p "%F,@ " n + | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n) + | Init_pointer id -> + match string_of_init id with + | None -> fprintf p "/* pointer to other init*/,@ " + | Some s -> fprintf p "%a,@ " print_escaped_string s + +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = + match init with + | [] -> + fprintf p "extern %s;@ @ " + (name_cdecl (extern_atom id) ty) + | [Init_space _] -> + fprintf p "%s;@ @ " + (name_cdecl (extern_atom id) ty) + | _ -> + fprintf p "@[<hov 2>%s = {@ " + (name_cdecl (extern_atom id) ty); + List.iter (print_init p) init; + fprintf p "};@]@ @ " + +(* Collect struct and union types *) + +let rec collect_type = function + | Tvoid -> () + | Tint(sz, sg) -> () + | Tfloat sz -> () + | Tpointer t -> collect_type t + | Tarray(t, n) -> collect_type t + | Tfunction(args, res) -> collect_type_list args; collect_type res + | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld + | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld + | Tcomp_ptr _ -> () + +and collect_type_list = function + | Tnil -> () + | Tcons(hd, tl) -> collect_type hd; collect_type_list tl + +and collect_fields = function + | Fnil -> () + | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl + +let rec collect_expr (Expr(ed, ty)) = + match ed with + | Econst_int n -> () + | Econst_float f -> () + | Evar id -> () + | Eunop(op, e1) -> collect_expr e1 + | Ederef e -> collect_expr e + | Eaddrof e -> collect_expr e + | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2 + | Ecast(ty, e1) -> collect_type ty; collect_expr e1 + | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3 + | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2 + | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2 + | Esizeof ty -> collect_type ty + | Efield(e1, id) -> collect_expr e1 + +let rec collect_expr_list = function + | [] -> () + | hd :: tl -> collect_expr hd; collect_expr_list tl + +let rec collect_stmt = function + | Sskip -> () + | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 + | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el + | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el + | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 + | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 + | Swhile(e, s) -> collect_expr e; collect_stmt s + | Sdowhile(e, s) -> collect_stmt s; collect_expr e + | Sfor(s_init, e, s_iter, s_body) -> + collect_stmt s_init; collect_expr e; + collect_stmt s_iter; collect_stmt s_body + | Sbreak -> () + | Scontinue -> () + | Sswitch(e, cases) -> collect_expr e; collect_cases cases + | Sreturn None -> () + | Sreturn (Some e) -> collect_expr e + +and collect_cases = function + | LSdefault s -> collect_stmt s + | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem + +let collect_function f = + collect_type f.fn_return; + List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; + List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars; + collect_stmt f.fn_body + +let collect_fundef (Coq_pair(id, fd)) = + match fd with + | External(_, args, res) -> collect_type_list args; collect_type res + | Internal f -> collect_function f + +let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) = + collect_type ty + +let collect_program p = + List.iter collect_globvar p.prog_vars; + List.iter collect_fundef p.prog_funct + +let declare_struct_or_union p (name, fld) = + fprintf p "%s;@ @ " name + +let print_struct_or_union p (name, fld) = + fprintf p "@[<v 2>%s {" name; + let rec print_fields = function + | Fnil -> () + | Fcons(id, ty, rem) -> + fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); + print_fields rem in + print_fields fld; + fprintf p "@;<0 -2>};@]@ " + +let print_program p prog = + struct_unions := StructUnionSet.empty; + collect_program prog; + fprintf p "@[<v 0>"; + StructUnionSet.iter (declare_struct_or_union p) !struct_unions; + StructUnionSet.iter (print_struct_or_union p) !struct_unions; + List.iter (print_globvar p) prog.prog_vars; + List.iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + + |