From 593ce3f7c5647e284cd2fdc3dd3ed41be9563982 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 7 Sep 2006 15:30:24 +0000 Subject: Integration du front-end CIL developpe par Thomas Moniot git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/Camlcoq.ml | 4 +- caml/Cil2Csyntax.ml | 863 +++++++++++++++++++++++++++++++++++++++++++++++++++ caml/Main2.ml | 144 ++++++++- caml/PrintCsyntax.ml | 434 ++++++++++++++++++++++++++ 4 files changed, 1433 insertions(+), 12 deletions(-) create mode 100644 caml/Cil2Csyntax.ml create mode 100644 caml/PrintCsyntax.ml (limited to 'caml') diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index b0bb4ff9..ab111c11 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -31,8 +31,8 @@ let rec positive_of_camlint n = if n = 0l then assert false else if n = 1l then Coq_xH else if Int32.logand n 1l = 0l - then Coq_xO (positive_of_camlint (Int32.shift_right n 1)) - else Coq_xI (positive_of_camlint (Int32.shift_right n 1)) + then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1)) + else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1)) let z_of_camlint n = if n = 0l then Z0 else diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml new file mode 100644 index 00000000..74bf0eb2 --- /dev/null +++ b/caml/Cil2Csyntax.ml @@ -0,0 +1,863 @@ +(************************************************************************** +CIL -> CabsCoq translator +**************************************************************************) + +open Cil +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 +(*-----------------------------------------------------------------------*) + + +(** Exception raised when an unsupported feature is encountered *) +exception Unsupported of string + + +(** Pre-defined constants *) +let constInt32 = Tint (I32, Signed) +let constInt32uns = Tint (I32, Unsigned) +let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32) + + +(** Identifiers for struct and union fields *) +let fieldTable = Hashtbl.create 47 (* hash-table *) +let fieldNum = ref Int32.one (* identifier of the next field *) + + +(** Other global variables *) +let currentLocation = ref Cil.locUnknown +let mainFound = ref false +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 *) + +(** Return a unique integer corresponding to a [struct] field *) +let ident_of_string str = + try Hashtbl.find fieldTable str + with Not_found -> let id = positive_of_camlint !fieldNum in + Hashtbl.add fieldTable str id; + fieldNum := Int32.succ !fieldNum; + id + +(* 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 *) + +(** Apply [f] to each element of the OCaml list [l] + and build a Coq list with the results returned by [f] *) +let rec map_coqlist f l = match l with + | [] -> CList.Coq_nil + | a :: b -> CList.Coq_cons (f a, map_coqlist f b) + +(** 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) + +(** Reverse-append over Coq lists *) + +let rec revappend l1 l2 = + match l1 with + | CList.Coq_nil -> l2 + | CList.Coq_cons(hd, tl) -> revappend tl (CList.Coq_cons (hd, l2)) + +(** ** 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) ^ ": " + +(** ** 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 CList.Coq_nil in + let add_char c = + init := CList.Coq_cons( + 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 -> CList.Coq_cons(global_for_string s id, l)) + stringTable globs + +(** ** Translation functions *) + +(** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) +let convertIkind ik = + match TS.convertIkind ik with + | Some p -> p + | None -> raise (Unsupported (currentLoc() ^ "integer type specifier")) + + +(** Convert a [Cil.fkind] into a [floatsize] *) +let convertFkind fk = + match TS.convertFkind fk with + | Some fs -> fs + | None -> raise (Unsupported + (currentLoc() ^ "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 _ -> + raise (Unsupported (currentLoc() ^ "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 failwith (currentLoc() ^ "processCast: illegal cast") + + +(** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *) +and processParamsE = function + | [] -> Enil + | e :: l -> + let (Expr (_, t)) as e' = convertExp e in + match t with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> Econs (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 -> raise (Unsupported + (currentLoc() ^ "size of a string literal")) + | AlignOf t -> raise (Unsupported + (currentLoc() ^ "GCC alignment directive")) + | AlignOfE e -> raise (Unsupported + (currentLoc() ^ "GCC alignment directive")) + | 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) +(* + (* array A replaced by &(A[0]) *) + Expr (Eaddrof (Expr (Eindex (e, const0), t')), tPtr) +*) + | _ -> failwith (currentLoc() ^ "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 fList -> + begin try + let idf = ident_of_string f.fname in + let t' = getFieldType idf fList in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + failwith (currentLoc() ^ "processOffset: no such struct field") + end + | Tunion fList -> + begin try + let idf = ident_of_string f.fname in + let t' = getFieldType idf fList in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + failwith (currentLoc() ^ "processOffset: no such union field") + end + | _ -> failwith + (currentLoc() ^ "processOffset: Field on a non-struct nor union") + end + | Index (e', ofs) -> + match t with + | Tarray (t', _) -> let e'' = Eindex (e, convertExp e') in + processOffset (Expr (e'', t')) ofs + | _ -> failwith + (currentLoc() ^ "processOffset: Index on a non-array") + in + (* convert the lvalue *) + match lv with + | (Var v, ofs) -> + 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 + | _ -> failwith + (currentLoc() ^ "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 _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> Tcons (t', processParamsT convert l) + + +(** Convert a [Cil.typ] into a [coq_type] *) +and convertTyp = function + | TVoid _ -> Tvoid + | TInt (k, _) -> let (x,y) = convertIkind k in Tint (x, y) + | TFloat (k, _) -> Tfloat (convertFkind k) + | TPtr (t, _) -> Tpointer (convertTyp t) + | TArray (t, eOpt, _) -> + begin match eOpt with + | Some (Const (CInt64 (i64, _, _))) -> + Tarray (convertTyp t, coqint_of_camlint (Int64.to_int32 i64)) + | Some _ -> raise (Unsupported + (currentLoc() ^ "size of array type not an integer constant")) + | None -> raise (Unsupported + (currentLoc() ^ "array type of unspecified size")) + end + | TFun (t, argListOpt, vArg, _) -> + (* Treat unprototyped functions as 0-argument functions, + and treat variadic functions as fixed-arity functions. + We will get type mismatches at applications, which we + compensate by casting the function type to the type + derived from the types of the actual arguments. *) + let argList = + match argListOpt with + | None -> [] + | Some l -> l + in + let t' = convertTyp t in + begin match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | _ -> Tfunction (processParamsT convertTyp argList, t') + end + | TNamed (tinfo, _) -> convertTyp tinfo.ttype + | TComp (c, _) -> + let rec convertFieldList = function + | [] -> Fnil + | {fname=str; ftype=t} :: rem -> + let idf = ident_of_string str in + let t' = convertCompositeType [c.ckey] t in + Fcons(idf, t', convertFieldList rem) in + let fList = convertFieldList c.cfields in + if c.cstruct then Tstruct fList else Tunion fList + | TEnum _ -> constInt32 (* enum constants are integers *) + | TBuiltin_va_list _ -> raise (Unsupported + (currentLoc() ^ "GCC built-in function")) + +(** Convert a [Cil.typ] within a composite structure into a [coq_type] *) +and convertCompositeType env = function + | TNamed (tinfo, _) -> convertCompositeType env tinfo.ttype + | TPtr _ -> Tpointer Tvoid + | TArray (ta, eOpt, _) -> + begin match eOpt with + | Some (Const (CInt64 (i64, _, _))) -> + let ta' = convertCompositeType env ta in + Tarray (ta', coqint_of_camlint (Int64.to_int32 i64)) + | Some _ -> raise (Unsupported + (currentLoc() ^ "size of array type not an integer constant")) + | None -> raise (Unsupported + (currentLoc() ^ "array type of unspecified size")) + end + | TFun (t, argListOpt, vArg, _) -> + if vArg then raise (Unsupported (currentLoc() ^ "variadic function")) + else + let argList = + match argListOpt with + | None -> + print_string ("Warning: " ^ + currentLoc() ^ "unknown function signature\n"); + [] + | Some l -> l + in + let convert = convertCompositeType env in + let t' = convert t in + begin match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | _ -> Tfunction (processParamsT convert argList, t') + end + | TComp (c, _) -> + if List.mem c.ckey env then + failwith (currentLoc() ^ + "convertCompositeType: illegal recursive structure"); + let rec convertFieldList = function + | [] -> Fnil + | {fname=str; ftype=t} :: rem -> + let idf = ident_of_string str in + let t' = convertCompositeType (c.ckey :: env) t in + Fcons(idf, t', convertFieldList rem) in + let fList = convertFieldList c.cfields in + if c.cstruct then Tstruct fList else Tunion fList + | t -> convertTyp t + + +(** 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 _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> 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 tfun eList = + match tfun with + | TFun (t, argListOpt, vArg, _) -> + let params = processParamsE eList in + let (Expr (efun, tfun)) as e' = convertExp e in + begin match argListOpt, vArg with + | Some argList, false -> + if List.length argList = List.length eList then (e', params) + else failwith + (currentLoc() ^ "convertExpFuncall: wrong number of arguments") + | _, _ -> + (* For variadic or unprototyped functions, we synthesize the + "real" type of the function from that of the actual + arguments, and insert a cast around e'. *) + begin match tfun with + | Tfunction (_, tret) -> + let rec typeOfExprList = function + | Enil -> Tnil + | Econs (Expr (_, ty), rem) -> + Tcons (ty, typeOfExprList rem) in + let tfun = Tfunction (typeOfExprList params, tret) in + (Expr (Ecast(tfun, e'), tfun), params) + | _ -> failwith + (currentLoc() ^ "convertExpFuncall: incorrect function type") + end + end + | _ -> failwith (currentLoc() ^ "convertExpFuncall: not a function") + + +(** 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 _ -> raise (Unsupported (currentLoc() ^ + "struct or union assignment")) + | t -> Sassign (convertLval lv, convertExp e) + end + | Call (lvOpt, e, eList, loc) -> + updateLoc(loc); + begin match Cil.unrollType (Cil.typeOf e) with + | TFun (t, _, _, _) as tfun -> + let t' = convertTyp t in + let (efun, params) = convertExpFuncall e tfun eList in + let e' = Expr (Ecall (efun, params), t') in + begin match lvOpt with + | None -> Sexpr e' + | Some lv -> + let (Expr (_, tlv)) as elv = convertLval lv in + begin match tlv with + | Tstruct _ | Tunion _ -> raise (Unsupported + (currentLoc() ^ "struct or union assignment")) + | _ -> + if tlv = t' then + Sassign (elv, e') + else + (* a cast must be inserted *) + if compatibleTypes tlv t' then + Sassign (elv, + Expr (Ecast (tlv, e'), tlv)) + else failwith + (currentLoc() ^ "processCast: illegal cast") + end + end + | _ -> failwith (currentLoc() ^ "convertInstr: illegal call") + end + | Asm (_, _, _, _, _, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "inline assembly")) + in + (* convert a list of instructions *) + match l with + | [] -> Sskip + | [s] -> convertInstr s + | s :: l -> Ssequence (convertInstr s, processInstrList l) + + +(** Convert a [Cil.stmt list] into a [CabsCoq.statement] *) +let rec processStmtList = function + | [] -> Sskip + | [s] -> convertStmt s + | s :: l -> Ssequence (convertStmt s, processStmtList l) + + +(** 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 + | _ -> failwith (currentLoc() ^ "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 + | [] -> failwith + (currentLoc() ^ "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 -> raise (Unsupported (currentLoc() ^ + "default case is not at the end of the switch structure")) + | 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); + raise (Unsupported (currentLoc() ^ "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); + raise (Unsupported (currentLoc() ^ "try...finally statement")) + | TryExcept (_, _, _, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "try...except statement")) + + +(** Convert a [Cil.GFun] into a pair [(ident * coq_fundecl)] *) +let convertGFun fdec = + let v = fdec.svar in + let ret = match v.vtype with + | TFun (t, _, vArg, _) -> + if vArg then raise (Unsupported (currentLoc() ^ "variadic function")) + else + begin match convertTyp t with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | t' -> t' + end + | _ -> failwith (currentLoc() ^ "convertGFun: incorrect function type") + in + let args = map_coqlist convertVarinfoParam fdec.sformals in (* parameters*) + let varList = map_coqlist convertVarinfo fdec.slocals in (* local vars *) + let s = processStmtList fdec.sbody.bstmts in (* function body *) + if v.vname = "main" then mainFound := true; + 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 + | CList.Coq_nil -> accu + | CList.Coq_cons(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 in + initDataLen (Int32.add sz accu) il + +(** Convert a [Cil.init] into a list of [AST.init_data] prepended to + the given list [k]. *) + +let rec convertInit init k = + match init with + | SingleInit e -> + begin match Cil.constFold true e with + | Const (CInt64(n, ikind, _)) -> + begin match convertIkind ikind with + | (I8, _) -> + CList.Coq_cons(Init_int8 (coqint_of_camlint (Int64.to_int32 n)), k) + | (I16, _) -> + CList.Coq_cons(Init_int16 (coqint_of_camlint (Int64.to_int32 n)), k) + | (I32, _) -> + CList.Coq_cons(Init_int32 (coqint_of_camlint (Int64.to_int32 n)), k) + end + | Const (CReal(n, fkind, _)) -> + begin match convertFkind fkind with + | F32 -> + CList.Coq_cons(Init_float32 n, k) + | F64 -> + CList.Coq_cons(Init_float64 n, k) + end + | _ -> + raise (Unsupported (currentLoc() ^ + "this kind of expression is not supported in global initializers")) + end + | CompoundInit(ty, data) -> + let init = (* in reverse order *) + Cil.foldLeftCompoundAll + ~doinit: (fun ofs init ty k -> convertInit init k) + ~ct: ty + ~initl: data + ~acc: CList.Coq_nil in + (* For struct or union, pad to size of type *) + begin match Cil.unrollType ty with + | TComp _ -> + let act_len = initDataLen 0l init in + let exp_len = camlint_of_z (Csyntax.sizeof (convertTyp ty)) in + assert (act_len <= exp_len); + let init' = + if act_len < exp_len + then let spc = z_of_camlint (Int32.sub exp_len act_len) in + CList.Coq_cons(Init_space spc, init) + else init in + revappend init' k + | _ -> + revappend init k + end + +(** Convert a [Cil.initinfo] into a list of [AST.init_data] *) + +let convertInitInfo ty info = + match info.init with + | None -> + CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil) + | Some init -> + convertInit init CList.Coq_nil + +(** 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, CList.Coq_nil), + 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 + | [] -> (CList.Coq_nil, CList.Coq_nil) + | g :: l -> + let (fList, vList) as rem = processGlobals l in + match g with + | GType _ -> rem (* typedefs are unrolled... *) + | GCompTag _ -> rem + | GCompTagDecl _ -> rem + | GEnumTag _ -> rem (* enum constants are folded... *) + | GEnumTagDecl _ -> rem + | GVarDecl (v, loc) -> + updateLoc(loc); + (* Functions become external declarations, + variables become uninitialized variables *) + if Cil.isFunctionType v.vtype + then (CList.Coq_cons (convertExtFun v, fList), vList) + else (fList, CList.Coq_cons (convertExtVar v, vList)) + | GVar (v, init, loc) -> + updateLoc(loc); + (fList, CList.Coq_cons (convertGVar v init, vList)) + | GFun (fdec, loc) -> + updateLoc(loc); + (CList.Coq_cons (convertGFun fdec, fList), vList) + | GAsm (_, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "asm statement")) + | GPragma (_, loc) -> + updateLoc(loc); + print_string ("Warning: " ^ + currentLoc() ^ "pragma directive ignored\n"); + rem + | GText _ -> rem (* 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 + | _ -> 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; + let (funList, defList) = processGlobals (cleanupGlobals f.globals) in + let funList' = match f.globinit with + | Some fdec -> CList.Coq_cons (convertGFun fdec, funList) + | None -> funList in + let defList' = globals_for_strings defList in +(*** + if not !mainFound then (* no main function *) + print_string ("Warning: program has no main function! (you should \ + probably have used ccomp's -nomain option)\n"); +***) + { AST.prog_funct = funList'; + AST.prog_vars = defList'; + AST.prog_main = intern_string "main" } + + +(*-----------------------------------------------------------------------*) +end + diff --git a/caml/Main2.ml b/caml/Main2.ml index 41815758..713af82b 100644 --- a/caml/Main2.ml +++ b/caml/Main2.ml @@ -1,5 +1,105 @@ open Printf -open Datatypes + +(* For the CIL -> Csyntax translator: + + * The meaning of some type specifiers may depend on compiler options: + the size of an int or the default signedness of char, for instance. + + * Those type conversions may be parameterized thanks to a functor. + + * Remark: [None] means that the type specifier is not supported + (that is, an Unsupported exception will be raised if that type + specifier is encountered in the program). +*) + +module TypeSpecifierTranslator = struct + + open Cil + open Csyntax + + (** Convert a Cil.ikind into an (intsize * signedness) option *) + let convertIkind = function + | IChar -> Some (I8, Unsigned) + | ISChar -> Some (I8, Signed) + | IUChar -> Some (I8, Unsigned) + | IInt -> Some (I32, Signed) + | IUInt -> Some (I32, Unsigned) + | IShort -> Some (I16, Signed) + | IUShort -> Some (I16, Unsigned) + | ILong -> Some (I32, Signed) + | IULong -> Some (I32, Unsigned) + | ILongLong -> (***Some (I32, Signed)***) None + | IULongLong -> (***Some (I32, Unsigned)***) None + + (** Convert a Cil.fkind into an floatsize option *) + let convertFkind = function + | FFloat -> Some F32 + | FDouble -> Some F64 + | FLongDouble -> (***Some F64***) None + +end + +module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator) + +let prepro_options = ref [] +let save_csyntax = ref false + +let preprocess file = + let temp = Filename.temp_file "compcert" ".i" in + let cmd = + sprintf "gcc %s -D__COMPCERT__ -E %s > %s" + (String.concat " " (List.rev !prepro_options)) + file + temp in + if Sys.command cmd = 0 + then temp + else (eprintf "Error during preprocessing.\n"; exit 2) + +let process_c_file sourcename = + let targetname = Filename.chop_suffix sourcename ".c" in + (* Preprocessing with cpp *) + let preproname = preprocess sourcename in + (* Parsing and production of a CIL.file *) + let cil = + try + Frontc.parse preproname () + with + Frontc.ParseError msg -> + eprintf "Error during parsing: %s\n" msg; + exit 2 in + Sys.remove preproname; + (* Restore source file name before preprocessing *) + cil.Cil.fileName <- sourcename; + (* Cleanup in the CIL.file *) + Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil; + (* Conversion to Csyntax *) + let csyntax = + try + Cil2CsyntaxTranslator.convertFile cil + with + | Cil2CsyntaxTranslator.Unsupported msg -> + eprintf "Unsupported C feature: %s\n" msg; + exit 2 + | Failure msg -> + eprintf "Error in translation CIL -> Csyntax:\n%s\n" msg; + exit 2 in + (* Save Csyntax if requested *) + if !save_csyntax then begin + let oc = open_out (targetname ^ ".csyntax") in + PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; + close_out oc + end; + (* Convert to PPC *) + let ppc = + match Main.transf_c_program csyntax with + | Datatypes.Some x -> x + | Datatypes.None -> + eprintf "Error in translation Csyntax -> PPC\n"; + exit 2 in + (* Save PPC asm *) + let oc = open_out (targetname ^ ".s") in + PrintPPC.print_program oc ppc; + close_out oc let process_cminor_file sourcename = let targetname = Filename.chop_suffix sourcename ".cm" ^ ".s" in @@ -9,10 +109,10 @@ let process_cminor_file sourcename = match Main.transf_cminor_program (CMtypecheck.type_program (CMparser.prog CMlexer.token lb)) with - | None -> + | Datatypes.None -> eprintf "Compiler failure\n"; exit 2 - | Some p -> + | Datatypes.Some p -> let oc = open_out targetname in PrintPPC.print_program oc p; close_out oc @@ -29,12 +129,36 @@ let process_cminor_file sourcename = sourcename msg; exit 2 -let process_file filename = - if Filename.check_suffix filename ".cm" then - process_cminor_file filename - else - raise (Arg.Bad ("unknown file type " ^ filename)) +(* Command-line parsing *) + +let starts_with s1 s2 = + String.length s1 >= String.length s2 && + String.sub s1 0 (String.length s2) = s2 + +let rec parse_cmdline i = + if i < Array.length Sys.argv then begin + let s = Sys.argv.(i) in + if s = "-dcsyntax" then begin + save_csyntax := true; + parse_cmdline (i + 1) + end else + if starts_with s "-I" || starts_with s "-D" || starts_with s "-U" + then begin + prepro_options := s :: !prepro_options; + parse_cmdline (i + 1) + end else + if Filename.check_suffix s ".cm" then begin + process_cminor_file s; + parse_cmdline (i + 1) + end else + if Filename.check_suffix s ".c" then begin + process_c_file s; + parse_cmdline (i + 1) + end else begin + eprintf "Unknown argument `%s'\n" s; + exit 2 + end + end let _ = - Arg.parse [] process_file - "Usage: ccomp \nOptions are:" + parse_cmdline 1 diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml new file mode 100644 index 00000000..ff2af16d --- /dev/null +++ b/caml/PrintCsyntax.ml @@ -0,0 +1,434 @@ +(** 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" + +(* Naming of structs and unions *) + +type su_kind = Struct | Union + +let struct_union_names = ref [] +let struct_union_name_counter = ref 0 + +let register_struct_union kind fld = + if not (List.mem_assoc (kind, fld) !struct_union_names) then begin + incr struct_union_name_counter; + let s = + match kind with + | Struct -> sprintf "s%d" !struct_union_name_counter + | Union -> sprintf "u%d" !struct_union_name_counter in + struct_union_names := ((kind, fld), s) :: !struct_union_names + end + +let struct_union_name kind fld = + try List.assoc (kind, fld) !struct_union_names with Not_found -> "" + +(* 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 '('; + 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; + Buffer.add_char b ')'; + name_cdecl (Buffer.contents b) res + | Tstruct fld -> + "struct " ^ struct_union_name Struct fld ^ name_optid id + | Tunion fld -> + "union " ^ struct_union_name Union fld ^ name_optid 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 + | Eindex(_, _) -> 20 + | Ecall(_, _) -> 20 + | 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 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 "@[%a@ %s %a@]" + print_expr_prec (level, e1) + (name_binop op) + print_expr_prec (level, e2) + | Ecast(ty, e1) -> + fprintf p "@[(%s)@,%a@]" + (name_type ty) + print_expr_prec (level, e1) + | Eindex(e1, e2) -> + fprintf p "@[%a@,[%a]@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Ecall(e1, el) -> + fprintf p "@[%a@,(@[%a@])@]" + print_expr_prec (level, e1) + print_expr_list (true, el) + | Eandbool(e1, e2) -> + fprintf p "@[%a@ && %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Eorbool(e1, e2) -> + fprintf p "@[%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 + +and print_expr_list p (first, el) = + match el with + | Enil -> () + | Econs(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*/;" + | Sexpr e -> + fprintf p "%a;" print_expr e + | Sassign(e1, e2) -> + fprintf p "@[%a =@ %a;@]" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a@ %a" print_stmt s1 print_stmt s2 + | Sifthenelse(e, s1, Sskip) -> + fprintf p "@[if (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Swhile(e, s) -> + fprintf p "@[while (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s + | Sdowhile(e, s) -> + fprintf p "@[do {@ %a@;<0 -2>} while(%a);@]" + print_stmt s + print_expr e + | Sfor(s_init, e, s_iter, s_body) -> + fprintf p "@[for (@[%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 "@[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 "@[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 "@[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*/" + | Sexpr e -> + fprintf p "%a" print_expr e + | 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 + | _ -> + fprintf p "" + +let name_function_parameters fun_name params = + let b = Buffer.create 20 in + Buffer.add_string b fun_name; + Buffer.add_char b '('; + let rec add_params first = function + | Coq_nil -> () + | Coq_cons(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; + 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 "@[{@ "; + coqlist_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 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) + +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = + match init with + | Coq_nil -> + fprintf p "extern %s;@ " + (name_cdecl (extern_atom id) ty) + | Coq_cons(Init_space _, Coq_nil) -> + fprintf p "%s;@ " + (name_cdecl (extern_atom id) ty) + | _ -> + fprintf p "@[%s = {@ " + (name_cdecl (extern_atom id) ty); + coqlist_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 fld -> register_struct_union Struct fld; collect_fields fld + | Tunion fld -> register_struct_union Union fld; collect_fields fld + +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 + | Eindex(e1, e2) -> collect_expr e1; collect_expr e2 + | Ecall(e1, el) -> collect_expr e1; collect_expr_list el + | 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 + +and collect_expr_list = function + | Enil -> () + | Econs(hd, tl) -> collect_expr hd; collect_expr_list tl + +let rec collect_stmt = function + | Sskip -> () + | Sexpr e -> collect_expr e + | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 + | 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; + coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; + coqlist_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 = + coqlist_iter collect_globvar p.prog_vars; + coqlist_iter collect_fundef p.prog_funct + +let print_struct_or_union p ((kind, fld), name) = + fprintf p "@[%s %s{@ " + (match kind with Struct -> "struct" | Union -> "union") + 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_union_names := []; + struct_union_name_counter := 0; + collect_program prog; + fprintf p "@["; + List.iter (print_struct_or_union p) !struct_union_names; + fprintf p "@ "; + coqlist_iter (print_globvar p) prog.prog_vars; + fprintf p "@ "; + coqlist_iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + + -- cgit