diff options
Diffstat (limited to 'caml')
| -rw-r--r-- | caml/CMlexer.mll | 1 | ||||
| -rw-r--r-- | caml/CMparser.mly | 279 | ||||
| -rw-r--r-- | caml/CMtypecheck.ml | 76 | ||||
| -rw-r--r-- | caml/Cil2Csyntax.ml | 88 | ||||
| -rw-r--r-- | caml/PrintCsyntax.ml | 43 |
5 files changed, 322 insertions, 165 deletions
diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll index ae71e0c1..7951982f 100644 --- a/caml/CMlexer.mll +++ b/caml/CMlexer.mll @@ -99,6 +99,7 @@ rule token = parse | "*" { STAR } | "*f" { STARF } | "switch" { SWITCH } + | "tailcall" { TAILCALL } | "~" { TILDE } | "var" { VAR } | "void" { VOID } diff --git a/caml/CMparser.mly b/caml/CMparser.mly index 0db0af2b..fb095275 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -10,22 +10,136 @@ open Integers open AST open Cminor +(** Naming function calls in expressions *) + +type rexpr = + | Rvar of ident + | Rconst of constant + | Runop of unary_operation * rexpr + | Rbinop of binary_operation * rexpr * rexpr + | Rload of memory_chunk * rexpr + | Rcondition of rexpr * rexpr * rexpr + | Rcall of signature * rexpr * rexpr list + | Ralloc of rexpr + +let temp_counter = ref 0 + +let temporaries = ref Coq_nil + +let mktemp () = + incr temp_counter; + let n = Printf.sprintf "__t%d" !temp_counter in + let id = intern_string n in + temporaries := Coq_cons(id, !temporaries); + id + +let convert_accu = ref [] + +let rec convert_rexpr = function + | Rvar id -> Evar id + | Rconst c -> Econst c + | Runop(op, e1) -> Eunop(op, convert_rexpr e1) + | Rbinop(op, e1, e2) -> + let c1 = convert_rexpr e1 in + let c2 = convert_rexpr e2 in + Ebinop(op, c1, c2) + | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1) + | Rcondition(e1, e2, e3) -> + let c1 = convert_rexpr e1 in + let c2 = convert_rexpr e2 in + let c3 = convert_rexpr e3 in + Econdition(c1, c2, c3) + | Rcall(sg, e1, el) -> + let c1 = convert_rexpr e1 in + let cl = convert_rexpr_list el in + let t = mktemp() in + convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu; + Evar t + | Ralloc e1 -> + let c1 = convert_rexpr e1 in + let t = mktemp() in + convert_accu := Salloc(t, c1) :: !convert_accu; + Evar t + +and convert_rexpr_list = function + | Coq_nil -> Coq_nil + | Coq_cons(e1, el) -> + let c1 = convert_rexpr e1 in + let cl = convert_rexpr_list el in + Coq_cons(c1, cl) + +let rec prepend_seq stmts last = + match stmts with + | [] -> last + | s1 :: sl -> prepend_seq sl (Sseq(s1, last)) + +let mkeval e = + convert_accu := []; + match e with + | Rcall(sg, e1, el) -> + let c1 = convert_rexpr e1 in + let cl = convert_rexpr_list el in + prepend_seq !convert_accu (Scall(None, sg, c1, cl)) + | _ -> + ignore (convert_rexpr e); + prepend_seq !convert_accu Sskip + +let mkassign id e = + convert_accu := []; + match e with + | Rcall(sg, e1, el) -> + let c1 = convert_rexpr e1 in + let cl = convert_rexpr_list el in + prepend_seq !convert_accu (Scall(Some id, sg, c1, cl)) + | Ralloc(e1) -> + let c1 = convert_rexpr e1 in + prepend_seq !convert_accu (Salloc(id, c1)) + | _ -> + let c = convert_rexpr e in + prepend_seq !convert_accu (Sassign(id, c)) + +let mkstore chunk e1 e2 = + convert_accu := []; + let c1 = convert_rexpr e1 in + let c2 = convert_rexpr e2 in + prepend_seq !convert_accu (Sstore(chunk, c1, c2)) + +let mkifthenelse e s1 s2 = + convert_accu := []; + let c = convert_rexpr e in + prepend_seq !convert_accu (Sifthenelse(c, s1, s2)) + +let mkreturn_some e = + convert_accu := []; + let c = convert_rexpr e in + prepend_seq !convert_accu (Sreturn (Some c)) + +let mktailcall sg e1 el = + convert_accu := []; + let c1 = convert_rexpr e1 in + let cl = convert_rexpr_list el in + prepend_seq !convert_accu (Stailcall(sg, c1, cl)) + +(** Other constructors *) + let intconst n = - Econst(Ointconst(coqint_of_camlint n)) + Rconst(Ointconst(coqint_of_camlint n)) let andbool e1 e2 = - Econdition(e1, e2, intconst 0l) + Rcondition(e1, e2, intconst 0l) let orbool e1 e2 = - Econdition(e1, intconst 1l, e2) + Rcondition(e1, intconst 1l, e2) let exitnum n = nat_of_camlint(Int32.pred n) let mkswitch expr (cases, dfl) = + convert_accu := []; + let c = convert_rexpr expr in let rec mktable = function | [] -> Coq_nil | (key, exit) :: rem -> Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in - Sswitch(expr, mktable cases, exitnum dfl) + prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl)) (*** match (a) { case 0: s0; case 1: s1; case 2: s2; } ---> @@ -65,10 +179,14 @@ let mkmatch_aux expr cases = mkblocks (Sblock sw) (Int32.pred ncases) cases let mkmatch expr cases = - match cases with - | [] -> Sskip (* ??? *) - | [key, action] -> action - | _ -> mkmatch_aux expr cases + convert_accu := []; + let c = convert_rexpr expr in + let s = + match cases with + | [] -> Sskip (* ??? *) + | [key, action] -> action + | _ -> mkmatch_aux c cases in + prepend_seq !convert_accu s %} @@ -158,6 +276,7 @@ let mkmatch expr cases = %token <AST.ident> STRINGLIT %token SWITCH %token TILDE +%token TAILCALL %token VAR %token VOID @@ -221,10 +340,13 @@ proc: var_declarations stmt_list RBRACE - { Coq_pair($1, + { let tmp = !temporaries in + temporaries := Coq_nil; + temp_counter := 0; + Coq_pair($1, Internal { fn_sig = $6; fn_params = CList.rev $3; - fn_vars = CList.rev $9; + fn_vars = CList.rev (CList.app tmp $9); fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature @@ -269,20 +391,24 @@ var_declaration: /* Statements */ stmt: - expr SEMICOLON { Sexpr $1 } - | IDENT EQUAL expr SEMICOLON { Sassign($1, $3) } - | IF LPAREN expr RPAREN stmts ELSE stmts { Sifthenelse($3, $5, $7) } - | IF LPAREN expr RPAREN stmts { Sifthenelse($3, $5, Sskip) } + expr SEMICOLON { mkeval $1 } + | IDENT EQUAL expr SEMICOLON { mkassign $1 $3 } + | memory_chunk LBRACKET expr RBRACKET EQUAL expr SEMICOLON + { mkstore $1 $3 $6 } + | IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 } + | IF LPAREN expr RPAREN stmts { mkifthenelse $3 $5 Sskip } | LOOP stmts { Sloop($2) } | LBRACELBRACE stmt_list RBRACERBRACE { Sblock($2) } | EXIT SEMICOLON { Sexit O } | EXIT INTLIT SEMICOLON { Sexit (exitnum $2) } | RETURN SEMICOLON { Sreturn None } - | RETURN expr SEMICOLON { Sreturn (Some $2) } + | RETURN expr SEMICOLON { mkreturn_some $2 } | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE { mkswitch $3 $6 } | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE { mkmatch $3 $6 } + | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON + { mktailcall $7 $2 $4 } ; stmts: @@ -311,80 +437,75 @@ match_cases: expr: LPAREN expr RPAREN { $2 } - | IDENT { Evar $1 } + | IDENT { Rvar $1 } | INTLIT { intconst $1 } - | FLOATLIT { Econst(Ofloatconst $1) } - | STRINGLIT { Econst(Oaddrsymbol($1, Int.zero)) } - | AMPERSAND INTLIT { Econst(Oaddrstack(coqint_of_camlint $2)) } - | MINUS expr %prec p_uminus { Eunop(Onegint, $2) } - | MINUSF expr %prec p_uminus { Eunop(Onegf, $2) } - | ABSF expr { Eunop(Oabsf, $2) } - | INTOFFLOAT expr { Eunop(Ointoffloat, $2) } - | FLOATOFINT expr { Eunop(Ofloatofint, $2) } - | FLOATOFINTU expr { Eunop(Ofloatofintu, $2) } - | TILDE expr { Eunop(Onotint, $2) } - | BANG expr { Eunop(Onotbool, $2) } - | INT8S expr { Eunop(Ocast8signed, $2) } - | INT8U expr { Eunop(Ocast8unsigned, $2) } - | INT16S expr { Eunop(Ocast16signed, $2) } - | INT16U expr { Eunop(Ocast16unsigned, $2) } - | FLOAT32 expr { Eunop(Osingleoffloat, $2) } - | ALLOC expr { Ealloc $2 } - | expr PLUS expr { Ebinop(Oadd, $1, $3) } - | expr MINUS expr { Ebinop(Osub, $1, $3) } - | expr STAR expr { Ebinop(Omul, $1, $3) } - | expr SLASH expr { Ebinop(Odiv, $1, $3) } - | expr PERCENT expr { Ebinop(Omod, $1, $3) } - | expr SLASHU expr { Ebinop(Odivu, $1, $3) } - | expr PERCENTU expr { Ebinop(Omodu, $1, $3) } - | expr AMPERSAND expr { Ebinop(Oand, $1, $3) } - | expr BAR expr { Ebinop(Oor, $1, $3) } - | expr CARET expr { Ebinop(Oxor, $1, $3) } - | expr LESSLESS expr { Ebinop(Oshl, $1, $3) } - | expr GREATERGREATER expr { Ebinop(Oshr, $1, $3) } - | expr GREATERGREATERU expr { Ebinop(Oshru, $1, $3) } - | expr PLUSF expr { Ebinop(Oaddf, $1, $3) } - | expr MINUSF expr { Ebinop(Osubf, $1, $3) } - | expr STARF expr { Ebinop(Omulf, $1, $3) } - | expr SLASHF expr { Ebinop(Odivf, $1, $3) } - | expr EQUALEQUAL expr { Ebinop(Ocmp Ceq, $1, $3) } - | expr BANGEQUAL expr { Ebinop(Ocmp Cne, $1, $3) } - | expr LESS expr { Ebinop(Ocmp Clt, $1, $3) } - | expr LESSEQUAL expr { Ebinop(Ocmp Cle, $1, $3) } - | expr GREATER expr { Ebinop(Ocmp Cgt, $1, $3) } - | expr GREATEREQUAL expr { Ebinop(Ocmp Cge, $1, $3) } - | expr EQUALEQUALU expr { Ebinop(Ocmpu Ceq, $1, $3) } - | expr BANGEQUALU expr { Ebinop(Ocmpu Cne, $1, $3) } - | expr LESSU expr { Ebinop(Ocmpu Clt, $1, $3) } - | expr LESSEQUALU expr { Ebinop(Ocmpu Cle, $1, $3) } - | expr GREATERU expr { Ebinop(Ocmpu Cgt, $1, $3) } - | expr GREATEREQUALU expr { Ebinop(Ocmpu Cge, $1, $3) } - | expr EQUALEQUALF expr { Ebinop(Ocmpf Ceq, $1, $3) } - | expr BANGEQUALF expr { Ebinop(Ocmpf Cne, $1, $3) } - | expr LESSF expr { Ebinop(Ocmpf Clt, $1, $3) } - | expr LESSEQUALF expr { Ebinop(Ocmpf Cle, $1, $3) } - | expr GREATERF expr { Ebinop(Ocmpf Cgt, $1, $3) } - | expr GREATEREQUALF expr { Ebinop(Ocmpf Cge, $1, $3) } - | memory_chunk LBRACKET expr RBRACKET { Eload($1, $3) } - | memory_chunk LBRACKET expr RBRACKET EQUAL expr - { Estore($1, $3, $6) } - | expr LPAREN expr_list RPAREN COLON signature - { Ecall($6, $1, $3) } + | FLOATLIT { Rconst(Ofloatconst $1) } + | STRINGLIT { Rconst(Oaddrsymbol($1, Int.zero)) } + | AMPERSAND INTLIT { Rconst(Oaddrstack(coqint_of_camlint $2)) } + | MINUS expr %prec p_uminus { Rbinop(Osub, intconst 0l, $2) } /***FIXME***/ + | MINUSF expr %prec p_uminus { Runop(Onegf, $2) } + | ABSF expr { Runop(Oabsf, $2) } + | INTOFFLOAT expr { Runop(Ointoffloat, $2) } + | FLOATOFINT expr { Runop(Ofloatofint, $2) } + | FLOATOFINTU expr { Runop(Ofloatofintu, $2) } + | TILDE expr { Runop(Onotint, $2) } + | BANG expr { Runop(Onotbool, $2) } + | INT8S expr { Runop(Ocast8signed, $2) } + | INT8U expr { Runop(Ocast8unsigned, $2) } + | INT16S expr { Runop(Ocast16signed, $2) } + | INT16U expr { Runop(Ocast16unsigned, $2) } + | FLOAT32 expr { Runop(Osingleoffloat, $2) } + | expr PLUS expr { Rbinop(Oadd, $1, $3) } + | expr MINUS expr { Rbinop(Osub, $1, $3) } + | expr STAR expr { Rbinop(Omul, $1, $3) } + | expr SLASH expr { Rbinop(Odiv, $1, $3) } + | expr PERCENT expr { Rbinop(Omod, $1, $3) } + | expr SLASHU expr { Rbinop(Odivu, $1, $3) } + | expr PERCENTU expr { Rbinop(Omodu, $1, $3) } + | expr AMPERSAND expr { Rbinop(Oand, $1, $3) } + | expr BAR expr { Rbinop(Oor, $1, $3) } + | expr CARET expr { Rbinop(Oxor, $1, $3) } + | expr LESSLESS expr { Rbinop(Oshl, $1, $3) } + | expr GREATERGREATER expr { Rbinop(Oshr, $1, $3) } + | expr GREATERGREATERU expr { Rbinop(Oshru, $1, $3) } + | expr PLUSF expr { Rbinop(Oaddf, $1, $3) } + | expr MINUSF expr { Rbinop(Osubf, $1, $3) } + | expr STARF expr { Rbinop(Omulf, $1, $3) } + | expr SLASHF expr { Rbinop(Odivf, $1, $3) } + | expr EQUALEQUAL expr { Rbinop(Ocmp Ceq, $1, $3) } + | expr BANGEQUAL expr { Rbinop(Ocmp Cne, $1, $3) } + | expr LESS expr { Rbinop(Ocmp Clt, $1, $3) } + | expr LESSEQUAL expr { Rbinop(Ocmp Cle, $1, $3) } + | expr GREATER expr { Rbinop(Ocmp Cgt, $1, $3) } + | expr GREATEREQUAL expr { Rbinop(Ocmp Cge, $1, $3) } + | expr EQUALEQUALU expr { Rbinop(Ocmpu Ceq, $1, $3) } + | expr BANGEQUALU expr { Rbinop(Ocmpu Cne, $1, $3) } + | expr LESSU expr { Rbinop(Ocmpu Clt, $1, $3) } + | expr LESSEQUALU expr { Rbinop(Ocmpu Cle, $1, $3) } + | expr GREATERU expr { Rbinop(Ocmpu Cgt, $1, $3) } + | expr GREATEREQUALU expr { Rbinop(Ocmpu Cge, $1, $3) } + | expr EQUALEQUALF expr { Rbinop(Ocmpf Ceq, $1, $3) } + | expr BANGEQUALF expr { Rbinop(Ocmpf Cne, $1, $3) } + | expr LESSF expr { Rbinop(Ocmpf Clt, $1, $3) } + | expr LESSEQUALF expr { Rbinop(Ocmpf Cle, $1, $3) } + | expr GREATERF expr { Rbinop(Ocmpf Cgt, $1, $3) } + | expr GREATEREQUALF expr { Rbinop(Ocmpf Cge, $1, $3) } + | memory_chunk LBRACKET expr RBRACKET { Rload($1, $3) } | expr AMPERSANDAMPERSAND expr { andbool $1 $3 } | expr BARBAR expr { orbool $1 $3 } - | expr QUESTION expr COLON expr { Econdition($1, $3, $5) } - | LET expr IN expr %prec p_let { Elet($2, $4) } - | DOLLAR INTLIT { Eletvar (nat_of_camlint $2) } + | expr QUESTION expr COLON expr { Rcondition($1, $3, $5) } + | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) } + | ALLOC expr { Ralloc $2 } ; expr_list: - /* empty */ { Enil } + /* empty */ { Coq_nil } | expr_list_1 { $1 } ; expr_list_1: - expr %prec COMMA { Econs($1, Enil) } - | expr COMMA expr_list_1 { Econs($1, $3) } + expr %prec COMMA { Coq_cons($1, Coq_nil) } + | expr COMMA expr_list_1 { Coq_cons($1, $3) } ; memory_chunk: diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 495ded0c..9277829c 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -206,30 +206,6 @@ let rec type_expr env lenv e = (name_of_chunk chunk) s)) end; type_chunk chunk - | Estore(chunk, e1, e2) -> - let te1 = type_expr env lenv e1 in - let te2 = type_expr env lenv e2 in - begin try - unify tint te1; - unify (type_chunk chunk) te2 - with Error s -> - raise (Error (sprintf "In store %s:\n%s" - (name_of_chunk chunk) s)) - end; - te1 - | Ecall(sg, e1, el) -> - let te1 = type_expr env lenv e1 in - let tel = type_exprlist env lenv el in - begin try - unify tint te1; - unify_list (ty_of_sig_args sg.sig_args) tel - with Error s -> - raise (Error (sprintf "In call:\n%s" s)) - end; - begin match sg.sig_res with - | None -> tint (*???*) - | Some t -> ty_of_typ t - end | Econdition(e1, e2, e3) -> type_condexpr env lenv e1; let te2 = type_expr env lenv e2 in @@ -240,25 +216,19 @@ let rec type_expr env lenv e = raise (Error (sprintf "In conditional expression:\n%s" s)) end; te2 +(* | Elet(e1, e2) -> let te1 = type_expr env lenv e1 in let te2 = type_expr env (te1 :: lenv) e2 in te2 | Eletvar n -> type_letvar lenv n - | Ealloc e -> - let te = type_expr env lenv e in - begin try - unify tint te - with Error s -> - raise (Error (sprintf "In alloc:\n%s" s)) - end; - tint +*) and type_exprlist env lenv el = match el with - | Enil -> [] - | Econs (e1, et) -> + | Coq_nil -> [] + | Coq_cons (e1, et) -> let te1 = type_expr env lenv e1 in let tet = type_exprlist env lenv et in (te1 :: tet) @@ -274,8 +244,6 @@ and type_condexpr env lenv e = let rec type_stmt env blk ret s = match s with | Sskip -> () - | Sexpr e -> - ignore (type_expr env [] e) | Sassign(id, e1) -> let tid = type_var env id in let te1 = type_expr env [] e1 in @@ -284,6 +252,42 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s)) end + | Sstore(chunk, e1, e2) -> + let te1 = type_expr env [] e1 in + let te2 = type_expr env [] e2 in + begin try + unify tint te1; + unify (type_chunk chunk) te2 + with Error s -> + raise (Error (sprintf "In store %s:\n%s" + (name_of_chunk chunk) s)) + end + | Scall(optid, sg, e1, el) -> + let te1 = type_expr env [] e1 in + let tel = type_exprlist env [] el in + begin try + unify tint te1; + unify_list (ty_of_sig_args sg.sig_args) tel; + let ty_res = + match sg.sig_res with + | None -> tint (*???*) + | Some t -> ty_of_typ t in + begin match optid with + | None -> () + | Some id -> unify (type_var env id) ty_res + end + with Error s -> + raise (Error (sprintf "In call:\n%s" s)) + end + | Salloc(id, e) -> + let tid = type_var env id in + let te = type_expr env [] e in + begin try + unify tint te; + unify tint tid + with Error s -> + raise (Error (sprintf "In alloc:\n%s" s)) + end | Sseq(s1, s2) -> type_stmt env blk ret s1; type_stmt env blk ret s2 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 }) diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml index f9abd9a2..59c42d3b 100644 --- a/caml/PrintCsyntax.ml +++ b/caml/PrintCsyntax.ml @@ -129,7 +129,6 @@ let parenthesis_level (Expr (e, ty)) = end | Ecast _ -> 30 | Eindex(_, _) -> 20 - | Ecall(_, _) -> 20 | Eandbool(_, _) -> 80 | Eorbool(_, _) -> 80 | Esizeof _ -> 20 @@ -163,10 +162,6 @@ let rec print_expr p (Expr (eb, ty) as e) = fprintf p "@[<hov 2>%a@,[%a]@]" print_expr_prec (level, e1) print_expr_prec (level, e2) - | Ecall(e1, el) -> - fprintf p "@[<hov 2>%a@,(@[<hov 0>%a@])@]" - print_expr_prec (level, e1) - print_expr_list (true, el) | Eandbool(e1, e2) -> fprintf p "@[<hov 0>%a@ && %a@]" print_expr_prec (level, e1) @@ -186,10 +181,10 @@ and print_expr_prec p (context_prec, e) = then fprintf p "(%a)" print_expr e else print_expr p e -and print_expr_list p (first, el) = +let rec print_expr_list p (first, el) = match el with - | Enil -> () - | Econs(e1, et) -> + | Coq_nil -> () + | Coq_cons(e1, et) -> if not first then fprintf p ",@ "; print_expr p e1; print_expr_list p (false, et) @@ -198,10 +193,17 @@ 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 "@[<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) -> @@ -260,12 +262,19 @@ 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 + | 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 "<impossible>" @@ -395,20 +404,20 @@ let rec collect_expr (Expr(ed, ty)) = | 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_expr_list = function + | Coq_nil -> () + | Coq_cons(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 + | 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 |