From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cil2Csyntax.ml | 992 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 992 insertions(+) create mode 100644 cfrontend/Cil2Csyntax.ml (limited to 'cfrontend/Cil2Csyntax.ml') 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 + -- cgit