From f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 12:07:11 +0000 Subject: Elimination of "alloc" instruction in Caml files and test files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 2 -- backend/CMlexer.mll | 1 - backend/CMparser.mly | 11 ----------- backend/CMtypecheck.ml | 9 --------- backend/Linearizeaux.ml | 1 - backend/RTLtypingaux.ml | 2 -- powerpc/PrintAsm.ml | 2 -- test/cminor/lists.cm | 6 ++++-- 8 files changed, 4 insertions(+), 30 deletions(-) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index e5b21f9c..16f22d60 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -336,8 +336,6 @@ let print_instruction oc labels = function | Psufd(r1, r2, r3) -> fprintf oc " sufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 (* Pseudo-instructions *) - | Pallocblock -> - fprintf oc " bl compcert_alloc\n"; 1 | Pallocframe(lo, hi, ofs) -> let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 9854117c..3506e502 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -33,7 +33,6 @@ rule token = parse | blank + { token lexbuf } | "/*" { comment lexbuf; token lexbuf } | "absf" { ABSF } - | "alloc" { ALLOC } | "&" { AMPERSAND } | "&&" { AMPERSANDAMPERSAND } | "!" { BANG } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b995132c..f369f9ea 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -33,7 +33,6 @@ type 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 @@ -68,11 +67,6 @@ let rec convert_rexpr = function 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 | [] -> [] @@ -104,9 +98,6 @@ let mkassign id e = 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)) @@ -206,7 +197,6 @@ let mkmatch expr cases = %token ABSF %token AMPERSAND %token AMPERSANDAMPERSAND -%token ALLOC %token BANG %token BANGEQUAL %token BANGEQUALF @@ -508,7 +498,6 @@ expr: | expr BARBAR expr { orbool $1 $3 } | 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: diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index d761f759..c4f45b22 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -294,15 +294,6 @@ let rec type_stmt env blk ret s = 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/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 2f2333fb..d2d2f24a 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -70,7 +70,6 @@ let enumerate_aux f reach = | Lstore (chunk, addr, args, src, s) -> emit_block pending s | Lcall (sig0, ros, args, res, s) -> emit_block pending s | Ltailcall (sig0, ros, args) -> emit_restart pending - | Lalloc (arg, res, s) -> emit_block pending s | Lcond (cond, args, ifso, ifnot) -> emit_restart (IntSet.add (int_of_pos ifso) (IntSet.add (int_of_pos ifnot) pending)) diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index ff704ebe..632f2aa5 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -86,8 +86,6 @@ let type_instr retty (Coq_pair(pc, i)) = raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" name msg)) end - | Ialloc(arg, res, _) -> - set_type arg Tint; set_type res Tint | Icond(cond, args, _, _) -> set_types args (type_of_condition cond) | Ireturn(optres) -> diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index a52a90f0..352da05a 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -180,8 +180,6 @@ let print_instruction oc labels = function fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddze(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocblock -> - fprintf oc " bl %a\n" raw_symbol "compcert_alloc" | Pallocframe(lo, hi, ofs) -> let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi diff --git a/test/cminor/lists.cm b/test/cminor/lists.cm index c4456236..6007f3ce 100644 --- a/test/cminor/lists.cm +++ b/test/cminor/lists.cm @@ -1,11 +1,13 @@ /* List manipulations */ +extern "malloc" : int -> int + "buildlist"(n): int -> int { var b; if (n < 0) return 0; - b = alloc 8; + b = "malloc"(8) : int -> int; int32[b] = n; int32[b+4] = "buildlist"(n - 1) : int -> int; return b; @@ -17,7 +19,7 @@ r = 0; loop { if (l == 0) return r; - r2 = alloc 8; + r2 = "malloc"(8) : int -> int; int32[r2] = int32[l]; int32[r2+4] = r; r = r2; -- cgit