From f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 11 Jan 2009 12:07:11 +0000
Subject: [PATCH] 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 e5b21f9c2..16f22d60d 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 9854117c3..3506e5021 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 b995132c8..f369f9eac 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 d761f759a..c4f45b221 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 2f2333fb1..d2d2f24ad 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 ff704ebe7..632f2aa51 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 a52a90f06..352da05ab 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 c44562368..6007f3ce4 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;
--
GitLab