diff options
Diffstat (limited to 'caml/Cil2Csyntax.ml')
-rw-r--r-- | caml/Cil2Csyntax.ml | 88 |
1 files changed, 55 insertions, 33 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 553229c6..0e168414 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -3,6 +3,7 @@ CIL -> CabsCoq translator **************************************************************************) open Cil +open CList open Camlcoq open AST open Csyntax @@ -192,6 +193,17 @@ let declare_stub_functions k = Hashtbl.fold (fun n i k -> CList.Coq_cons(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 + (** ** Translation functions *) (** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) @@ -310,13 +322,13 @@ and processCast t e = (** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *) and processParamsE = function - | [] -> Enil + | [] -> Coq_nil | e :: l -> let (Expr (_, t)) as e' = convertExp e in match t with | Tstruct _ | Tunion _ -> unsupported "function parameter of struct or union type" - | _ -> Econs (e', processParamsE l) + | _ -> Coq_cons (e', processParamsE l) (** Convert a [Cil.exp] into a [CabsCoq.expr] *) @@ -489,8 +501,8 @@ let convertVarinfoParam v = (** 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 +let convertExpFuncall e eList = + match typeOf e with | TFun (res, argListOpt, vArg, _) -> begin match argListOpt, vArg with | Some argList, false -> @@ -512,8 +524,8 @@ let convertExpFuncall e tfun eList = | _ -> unsupported "call to variadic or non-prototyped function" in let rec typeOfExprList = function - | Enil -> Tnil - | Econs (Expr (_, ty), rem) -> Tcons (ty, typeOfExprList rem) in + | Coq_nil -> Tnil + | Coq_cons (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) = @@ -523,6 +535,33 @@ let convertExpFuncall e tfun eList = 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 *) @@ -533,33 +572,14 @@ let rec processInstrList l = | Tstruct _ | Tunion _ -> unsupported "struct or union assignment" | t -> Sassign (convertLval lv, convertExp e) end - | Call (lvOpt, e, eList, loc) -> + | Call (None, 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 _ -> - unsupported "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 internal_error "processCast: illegal cast" - end - end - | _ -> internal_error "convertInstr: illegal call" - end + 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" @@ -687,6 +707,7 @@ and convertStmt s = (** 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, _) -> @@ -698,15 +719,16 @@ let convertGFun fdec = 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 = 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 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 }) |