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

1 files changed, 541 insertions, 0 deletions

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
new file mode 100644
index 0000000..25fb032
--- /dev/null
+++ b/backend/CMparser.mly
@@ -0,0 +1,541 @@
+/* *********************************************************************/
+/*                                                                     */
+/*              The Compcert verified compiler                         */
+/*                                                                     */
+/*          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.     */
+/*                                                                     */
+/* *********************************************************************/
+
+%{
+open Datatypes
+open CList
+open Camlcoq
+open BinPos
+open BinInt
+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 []
+
+let mktemp () =
+  incr temp_counter;
+  let n = Printf.sprintf "__t%d" !temp_counter in
+  let id = intern_string n in
+  temporaries := 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
+  | [] -> []
+  | e1 :: el ->
+      let c1 = convert_rexpr e1 in
+      let cl = convert_rexpr_list el in
+      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 =
+  Rconst(Ointconst(coqint_of_camlint n))
+
+let andbool e1 e2 =
+  Rcondition(e1, e2, intconst 0l)
+let orbool e1 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
+  | [] -> []
+  | (key, exit) :: rem ->
+      Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
+  prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
+
+(***
+   match (a) { case 0: s0; case 1: s1; case 2: s2; }  --->
+
+   block {
+   block {
+   block {
+   block {
+     switch(a) { case 0: exit 0; case 1: exit 1; default: exit 2; }
+   }; s0; exit 2;
+   }; s1; exit 1;
+   }; s2;
+   }
+
+   Note that matches are assumed to be exhaustive
+***)
+
+let mkmatch_aux expr cases =
+  let ncases = Int32.of_int (List.length cases) in
+  let rec mktable n = function
+    | [] -> assert false
+    | [key, action] -> []
+    | (key, action) :: rem ->
+        Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+        :: mktable (Int32.succ n) rem in
+  let sw =
+    Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
+  let rec mkblocks body n = function
+    | [] -> assert false
+    | [key, action] ->
+        Sblock(Sseq(body, action))
+    | (key, action) :: rem ->
+        mkblocks
+          (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n)))))
+          (Int32.pred n)
+          rem in
+  mkblocks (Sblock sw) (Int32.pred ncases) cases
+
+let mkmatch 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
+
+%}
+
+%token ABSF
+%token AMPERSAND
+%token AMPERSANDAMPERSAND
+%token ALLOC
+%token BANG
+%token BANGEQUAL
+%token BANGEQUALF
+%token BANGEQUALU
+%token BAR
+%token BARBAR
+%token CARET
+%token CASE
+%token COLON
+%token COMMA
+%token DEFAULT
+%token DOLLAR
+%token ELSE
+%token EQUAL
+%token EQUALEQUAL
+%token EQUALEQUALF
+%token EQUALEQUALU
+%token EOF
+%token EXIT
+%token EXTERN
+%token FLOAT
+%token FLOAT32
+%token FLOAT64
+%token <float> FLOATLIT
+%token FLOATOFINT
+%token FLOATOFINTU
+%token GREATER
+%token GREATERF
+%token GREATERU
+%token GREATEREQUAL
+%token GREATEREQUALF
+%token GREATEREQUALU
+%token GREATERGREATER
+%token GREATERGREATERU
+%token <AST.ident> IDENT
+%token IF
+%token IN
+%token INT
+%token INT16S
+%token INT16U
+%token INT32
+%token INT8S
+%token INT8U
+%token <int32> INTLIT
+%token INTOFFLOAT
+%token INTUOFFLOAT
+%token LBRACE
+%token LBRACELBRACE
+%token LBRACKET
+%token LESS
+%token LESSU
+%token LESSF
+%token LESSEQUAL
+%token LESSEQUALU
+%token LESSEQUALF
+%token LESSLESS
+%token LET
+%token LOOP
+%token LPAREN
+%token MATCH
+%token MINUS
+%token MINUSF
+%token MINUSGREATER
+%token PERCENT
+%token PERCENTU
+%token PLUS
+%token PLUSF
+%token QUESTION
+%token RBRACE
+%token RBRACERBRACE
+%token RBRACKET
+%token RETURN
+%token RPAREN
+%token SEMICOLON
+%token SLASH
+%token SLASHF
+%token SLASHU
+%token STACK
+%token STAR
+%token STARF
+%token <AST.ident> STRINGLIT
+%token SWITCH
+%token TILDE
+%token TAILCALL
+%token VAR
+%token VOID
+
+/* Precedences from low to high */
+
+%left COMMA
+%left p_let
+%right EQUAL
+%right QUESTION COLON
+%left BARBAR
+%left AMPERSANDAMPERSAND
+%left BAR
+%left CARET
+%left AMPERSAND
+%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF 
+%left LESSLESS GREATERGREATER GREATERGREATERU
+%left PLUS PLUSF MINUS MINUSF
+%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
+%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC
+%left LPAREN
+
+/* Entry point */
+
+%start prog
+%type <Cminor.program> prog
+
+%%
+
+/* Programs */
+
+prog:
+    global_declarations proc_list EOF
+      { { prog_funct = CList.rev $2;
+          prog_main = intern_string "main";
+          prog_vars = CList.rev $1; } }
+;
+
+global_declarations:
+    /* empty */                                 { [] }
+  | global_declarations global_declaration      { $2 :: $1 }
+;
+
+global_declaration:
+    VAR STRINGLIT LBRACKET INTLIT RBRACKET
+      { Coq_pair(Coq_pair($2, [ Init_space (z_of_camlint $4) ]), ()) }
+;
+
+proc_list:
+    /* empty */                                 { [] }
+  | proc_list proc                              { $2 :: $1 }
+;
+
+/* Procedures */
+
+proc:
+    STRINGLIT LPAREN parameters RPAREN COLON signature
+    LBRACE
+      stack_declaration
+      var_declarations
+      stmt_list
+    RBRACE
+      { let tmp = !temporaries in
+        temporaries := [];
+        temp_counter := 0;
+        Coq_pair($1,
+        Internal { fn_sig = $6;
+                   fn_params = CList.rev $3;
+                   fn_vars = CList.rev (CList.app tmp $9);
+                   fn_stackspace = $8;
+                   fn_body = $10 }) }
+  | EXTERN STRINGLIT COLON signature 
+      { Coq_pair($2,
+        External { ef_id = $2;
+                   ef_sig = $4 }) }
+;
+
+signature:
+    type_ 
+               { {sig_args = []; sig_res = Some $1} }
+  | VOID
+               { {sig_args = []; sig_res = None} }
+  | type_ MINUSGREATER signature
+               { let s = $3 in {s with sig_args = $1 :: s.sig_args} }
+;
+
+parameters:
+    /* empty */                                 { [] }
+  | parameter_list                              { $1 }
+;
+
+parameter_list:
+    IDENT                                       { $1 :: [] }
+  | parameter_list COMMA IDENT                  { $3 :: $1 }
+;
+
+stack_declaration:
+    /* empty */                                 { Z0 }
+  | STACK INTLIT SEMICOLON                      { z_of_camlint $2 }
+;
+
+var_declarations:
+    /* empty */                                 { [] }
+  | var_declarations var_declaration            { CList.app $2 $1 }
+;
+
+var_declaration:
+    VAR parameter_list SEMICOLON                { $2 }
+;
+
+/* Statements */
+
+stmt:
+    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                       { 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:
+    LBRACE stmt_list RBRACE                     { $2 }
+  | stmt                                        { $1 }
+;
+
+stmt_list:
+    /* empty */                                 { Sskip }
+  | stmt stmt_list                              { Sseq($1, $2) }
+;
+
+switch_cases:
+    DEFAULT COLON EXIT INTLIT SEMICOLON
+           { ([], $4) }
+  | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases
+           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
+;
+
+match_cases:
+    /* empty */                                 { [] }
+  | CASE INTLIT COLON stmt_list match_cases     { ($2, $4) :: $5 }
+;
+
+/* Expressions */
+
+expr:
+    LPAREN expr RPAREN                          { $2 }
+  | IDENT                                       { Rvar $1 }
+  | INTLIT                                      { intconst $1 }
+  | 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) }
+  | INTUOFFLOAT expr                            { Runop(Ointuoffloat, $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               { Rcondition($1, $3, $5) }
+  | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) }
+  | ALLOC expr                                  { Ralloc $2 }
+;
+
+expr_list:
+    /* empty */                                 { [] }
+  | expr_list_1                                 { $1 }
+;
+
+expr_list_1:
+    expr                     %prec COMMA        { $1 :: [] }
+  | expr COMMA expr_list_1                      { $1 :: $3 }
+;
+
+memory_chunk:
+    INT8S                                       { Mint8signed }
+  | INT8U                                       { Mint8unsigned }
+  | INT16S                                      { Mint16signed }
+  | INT16U                                      { Mint16unsigned }
+  | INT32                                       { Mint32 }
+  | INT                                         { Mint32 }
+  | FLOAT32                                     { Mfloat32 }
+  | FLOAT64                                     { Mfloat64 }
+  | FLOAT                                       { Mfloat64 }
+;
+
+/* Types */
+
+type_:
+    INT                                         { Tint }
+  | FLOAT                                       { Tfloat }
+;