Cminor parsing and printing (from Andrew Tolmach)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 158 insertions, 19 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 4083c95..c400c5e 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -37,13 +37,18 @@ rule token = parse
   | "/*"         { comment lexbuf; token lexbuf }
   | "absf" { ABSF }
   | "&" { AMPERSAND }
+  | "&l" { AMPERSANDL }
   | "!"    { BANG }
   | "!="    { BANGEQUAL }
   | "!=f"    { BANGEQUALF }
+  | "!=l"    { BANGEQUALL }
+  | "!=lu"    { BANGEQUALLU }
   | "!=u"    { BANGEQUALU }
   | "|"     { BAR }
+  | "|l"     { BARL }
   | "builtin" { BUILTIN }
   | "^"     { CARET }
+  | "^l"     { CARETL }
   | "case"  { CASE }
   | ":"    { COLON }
   | ","    { COMMA }
@@ -52,23 +57,34 @@ rule token = parse
   | "="    { EQUAL }
   | "=="    { EQUALEQUAL }
   | "==f"    { EQUALEQUALF }
+  | "==l"    { EQUALEQUALL }
+  | "==lu"    { EQUALEQUALLU }
   | "==u"    { EQUALEQUALU }
   | "exit"    { EXIT }
   | "extern"    { EXTERN }
   | "float"    { FLOAT }
   | "float32"    { FLOAT32 }
   | "float64"    { FLOAT64 }
+  | "float64al32" { FLOAT64AL32 }
   | "floatofint"    { FLOATOFINT }
   | "floatofintu"    { FLOATOFINTU }
+  | "floatoflong"  { FLOATOFLONG }
+  | "floatoflongu" { FLOATOFLONGU }
   | "goto"  { GOTO } 
   | ">"    { GREATER }
   | ">f"    { GREATERF }
+  | ">l"    { GREATERL }
+  | ">lu"    { GREATERLU }
   | ">u"    { GREATERU }
   | ">="    { GREATEREQUAL }
   | ">=f"    { GREATEREQUALF }
+  | ">=l"    { GREATEREQUALL }
+  | ">=lu"    { GREATEREQUALLU }
   | ">=u"    { GREATEREQUALU }
   | ">>"    { GREATERGREATER }
   | ">>u"    { GREATERGREATERU }
+  | ">>l"    { GREATERGREATERL }
+  | ">>lu"    { GREATERGREATERLU }
   | "if"    { IF }
   | "in"    { IN }
   | "inline" { INLINE }
@@ -77,32 +93,48 @@ rule token = parse
   | "int16s"    { INT16S }
   | "int16u"    { INT16U }
   | "int32"    { INT32 }
+  | "int64"    { INT64 }
   | "int8"    { INT8 }
   | "int8s"    { INT8S }
   | "int8u"    { INT8U }
   | "intoffloat"    { INTOFFLOAT }
   | "intuoffloat"    { INTUOFFLOAT }
+  | "intoflong"   { INTOFLONG }
   | "{"    { LBRACE }
   | "{{"    { LBRACELBRACE }
   | "["    { LBRACKET }
   | "<"    { LESS }
   | "<u"    { LESSU }
+  | "<l"    { LESSL }
+  | "<lu"    { LESSLU }
   | "<f"    { LESSF }
   | "<="    { LESSEQUAL }
   | "<=u"    { LESSEQUALU }
   | "<=f"    { LESSEQUALF }
+  | "<=l"    { LESSEQUALL }
+  | "<=lu"    { LESSEQUALLU }
   | "<<"    { LESSLESS }
+  | "<<l"    { LESSLESSL }
   | "let"     { LET }
+  | "long"    { LONG }
+  | "longofint" { LONGOFINT }
+  | "longofintu" { LONGOFINTU }
+  | "longoffloat" { LONGOFFLOAT }
+  | "longuoffloat" { LONGUOFFLOAT }
   | "loop"    { LOOP }
   | "("    { LPAREN }
   | "match" { MATCH }
   | "-"    { MINUS }
   | "->"    { MINUSGREATER }
   | "-f"    { MINUSF }
+  | "-l"    { MINUSL }
   | "%"    { PERCENT }
+  | "%l"    { PERCENTL }
+  | "%lu"    { PERCENTLU }
   | "%u"    { PERCENTU }
   | "+"    { PLUS }
   | "+f"    { PLUSF }
+  | "+l"    { PLUSL }
   | "}"    { RBRACE }
   | "}}"    { RBRACERBRACE }
   | "]"    { RBRACKET }
@@ -112,18 +144,25 @@ rule token = parse
   | ";"    { SEMICOLON }
   | "/"    { SLASH }
   | "/f"    { SLASHF }
+  | "/l"    { SLASHL }
+  | "/lu"    { SLASHLU }
   | "/u"    { SLASHU }
+  | "single" { SINGLE }
   | "stack"    { STACK }
   | "*" { STAR }
   | "*f"    { STARF }
+  | "*l"    { STARL }
   | "switch"    { SWITCH }
   | "tailcall"  { TAILCALL }
   | "~"    { TILDE }
+  | "~l"    { TILDEL }
   | "var"    { VAR }
   | "void"    { VOID }
   | "volatile" { VOLATILE }
   | "while" { WHILE }
 
+  | intlit"LL"  { let s = Lexing.lexeme lexbuf in
+                LONGLIT(Int64.of_string(String.sub s 0 (String.length s - 2))) }
   | intlit    { INTLIT(Int32.of_string(Lexing.lexeme lexbuf)) }
   | floatlit     { FLOATLIT(float_of_string(Lexing.lexeme lexbuf)) }
   | stringlit { let s = Lexing.lexeme lexbuf in
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 273d572..b28578e 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -183,6 +183,9 @@ let mkwhile expr body =
 let intconst n =
   Rconst(Ointconst(coqint_of_camlint n))
 
+let longconst n =
+  Rconst(Olongconst(coqint_of_camlint64 n))
+
 let exitnum n = Nat.of_int32 n
 
 let mkswitch expr (cases, dfl) =
@@ -245,13 +248,18 @@ let mkmatch expr cases =
 
 %token ABSF
 %token AMPERSAND
+%token AMPERSANDL
 %token BANG
 %token BANGEQUAL
 %token BANGEQUALF
 %token BANGEQUALU
+%token BANGEQUALL
+%token BANGEQUALLU
 %token BAR
+%token BARL
 %token BUILTIN
 %token CARET
+%token CARETL
 %token CASE
 %token COLON
 %token COMMA
@@ -261,24 +269,35 @@ let mkmatch expr cases =
 %token EQUALEQUAL
 %token EQUALEQUALF
 %token EQUALEQUALU
+%token EQUALEQUALL
+%token EQUALEQUALLU
 %token EOF
 %token EXIT
 %token EXTERN
 %token FLOAT
 %token FLOAT32
 %token FLOAT64
+%token FLOAT64AL32
 %token <float> FLOATLIT
 %token FLOATOFINT
 %token FLOATOFINTU
+%token FLOATOFLONG
+%token FLOATOFLONGU
 %token GOTO
 %token GREATER
 %token GREATERF
 %token GREATERU
+%token GREATERL
+%token GREATERLU
 %token GREATEREQUAL
 %token GREATEREQUALF
 %token GREATEREQUALU
+%token GREATEREQUALL
+%token GREATEREQUALLU
 %token GREATERGREATER
 %token GREATERGREATERU
+%token GREATERGREATERL
+%token GREATERGREATERLU
 %token <string> IDENT
 %token IF
 %token IN
@@ -288,33 +307,50 @@ let mkmatch expr cases =
 %token INT16S
 %token INT16U
 %token INT32
+%token INT64
 %token INT8
 %token INT8S
 %token INT8U
 %token <int32> INTLIT
 %token INTOFFLOAT
 %token INTUOFFLOAT
+%token INTOFLONG
 %token LBRACE
 %token LBRACELBRACE
 %token LBRACKET
 %token LESS
 %token LESSU
 %token LESSF
+%token LESSL
+%token LESSLU
 %token LESSEQUAL
 %token LESSEQUALU
 %token LESSEQUALF
+%token LESSEQUALL
+%token LESSEQUALLU
 %token LESSLESS
+%token LESSLESSL
 %token LET
+%token LONG
+%token <int64> LONGLIT
+%token LONGOFINT 
+%token LONGOFINTU
+%token LONGOFFLOAT 
+%token LONGUOFFLOAT
 %token LOOP
 %token LPAREN
 %token MATCH
 %token MINUS
 %token MINUSF
+%token MINUSL
 %token MINUSGREATER
 %token PERCENT
 %token PERCENTU
+%token PERCENTL
+%token PERCENTLU
 %token PLUS
 %token PLUSF
+%token PLUSL
 %token RBRACE
 %token RBRACERBRACE
 %token RBRACKET
@@ -322,15 +358,20 @@ let mkmatch expr cases =
 %token RETURN
 %token RPAREN
 %token SEMICOLON
+%token SINGLE
 %token SLASH
 %token SLASHF
 %token SLASHU
+%token SLASHL
+%token SLASHLU
 %token STACK
 %token STAR
 %token STARF
+%token STARL
 %token <string> STRINGLIT
 %token SWITCH
 %token TILDE
+%token TILDEL
 %token TAILCALL
 %token VAR
 %token VOID
@@ -342,14 +383,14 @@ let mkmatch expr cases =
 %left COMMA
 %left p_let
 %right EQUAL
-%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 BAR BARL
+%left CARET CARETL
+%left AMPERSAND AMPERSANDL
+%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF EQUALEQUALL BANGEQUALL LESSL LESSEQUALL GREATERL GREATEREQUALL EQUALEQUALLU BANGEQUALLU LESSLU LESSEQUALLU GREATERLU GREATEREQUALLU
+%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU 
+%left PLUS PLUSF PLUSL MINUS MINUSF MINUSL
+%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU
+%nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
 %left LPAREN
 
 /* Entry point */
@@ -362,7 +403,11 @@ let mkmatch expr cases =
 /* Programs */
 
 prog:
-    global_declarations EOF
+   EQUAL STRINGLIT global_declarations EOF
+      { { prog_defs = List.rev $3;
+          prog_main = intern_string $2; } }
+
+|  global_declarations EOF
       { { prog_defs = List.rev $1;
           prog_main = intern_string "main" } }
 ;
@@ -409,6 +454,8 @@ init_data:
    | INT32 INTLIT                                { Init_int32 (coqint_of_camlint $2) }
    | INT INTLIT                                  { Init_int32 (coqint_of_camlint $2) }
    | INTLIT                                      { Init_int32 (coqint_of_camlint $1) }
+   | LONGLIT                                     { Init_int64 (coqint_of_camlint64 $1) }
+   | INT64 LONGLIT                               { Init_int64 (coqint_of_camlint64 $2) }
    | FLOAT32 FLOATLIT                            { Init_float32 (coqfloat_of_camlfloat $2) }
    | FLOAT64 FLOATLIT                            { Init_float64 (coqfloat_of_camlfloat $2) }
    | FLOAT FLOATLIT                              { Init_float64 (coqfloat_of_camlfloat $2) }
@@ -528,6 +575,7 @@ expr:
     LPAREN expr RPAREN                          { $2 }
   | IDENT                                       { Rvar(intern_string $1) }
   | INTLIT                                      { intconst $1 }
+  | LONGLIT                                     { longconst $1 }
   | FLOATLIT                                    { Rconst(Ofloatconst (coqfloat_of_camlfloat $1)) }
   | STRINGLIT                                   { Rconst(Oaddrsymbol(intern_string $1, Int.zero)) }
   | AMPERSAND INTLIT                            { Rconst(Oaddrstack(coqint_of_camlint $2)) }
@@ -545,6 +593,15 @@ expr:
   | INT16S expr                                 { Runop(Ocast16signed, $2) }
   | INT16U expr                                 { Runop(Ocast16unsigned, $2) }
   | FLOAT32 expr                                { Runop(Osingleoffloat, $2) }
+  | MINUSL expr %prec p_uminus                  { Runop(Onegl, $2) }
+  | TILDEL expr                                 { Runop(Onotl, $2) }
+  | INTOFLONG expr                              { Runop(Ointoflong, $2) }
+  | LONGOFINT expr                              { Runop(Olongofint, $2) }
+  | LONGOFINTU expr                             { Runop(Olongofintu, $2) }
+  | LONGOFFLOAT expr                            { Runop(Olongoffloat, $2) }
+  | LONGUOFFLOAT expr                           { Runop(Olonguoffloat, $2) }
+  | FLOATOFLONG expr                            { Runop(Ofloatoflong, $2) }
+  | FLOATOFLONGU expr                           { Runop(Ofloatoflongu, $2) }
   | expr PLUS expr                              { Rbinop(Oadd, $1, $3) }
   | expr MINUS expr                             { Rbinop(Osub, $1, $3) }
   | expr STAR expr                              { Rbinop(Omul, $1, $3) }
@@ -558,6 +615,19 @@ expr:
   | expr LESSLESS expr                          { Rbinop(Oshl, $1, $3) }
   | expr GREATERGREATER expr                    { Rbinop(Oshr, $1, $3) }
   | expr GREATERGREATERU expr                   { Rbinop(Oshru, $1, $3) }
+  | expr PLUSL expr                             { Rbinop(Oaddl, $1, $3) }
+  | expr MINUSL expr                            { Rbinop(Osubl, $1, $3) }
+  | expr STARL expr                             { Rbinop(Omull, $1, $3) }
+  | expr SLASHL expr                            { Rbinop(Odivl, $1, $3) }
+  | expr PERCENTL expr                          { Rbinop(Omodl, $1, $3) }
+  | expr SLASHLU expr                           { Rbinop(Odivlu, $1, $3) }
+  | expr PERCENTLU expr                         { Rbinop(Omodlu, $1, $3) }
+  | expr AMPERSANDL expr                        { Rbinop(Oandl, $1, $3) }
+  | expr BARL expr                              { Rbinop(Oorl, $1, $3) }
+  | expr CARETL expr                            { Rbinop(Oxorl, $1, $3) }
+  | expr LESSLESSL expr                         { Rbinop(Oshll, $1, $3) }
+  | expr GREATERGREATERL expr                   { Rbinop(Oshrl, $1, $3) }
+  | expr GREATERGREATERLU expr                  { Rbinop(Oshrlu, $1, $3) }
   | expr PLUSF expr                             { Rbinop(Oaddf, $1, $3) }
   | expr MINUSF expr                            { Rbinop(Osubf, $1, $3) }
   | expr STARF expr                             { Rbinop(Omulf, $1, $3) }
@@ -574,6 +644,18 @@ expr:
   | 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 EQUALEQUALL expr                       { Rbinop(Ocmpl Ceq, $1, $3) }
+  | expr BANGEQUALL expr                        { Rbinop(Ocmpl Cne, $1, $3) }
+  | expr LESSL expr                             { Rbinop(Ocmpl Clt, $1, $3) }
+  | expr LESSEQUALL expr                        { Rbinop(Ocmpl Cle, $1, $3) }
+  | expr GREATERL expr                          { Rbinop(Ocmpl Cgt, $1, $3) }
+  | expr GREATEREQUALL expr                     { Rbinop(Ocmpl Cge, $1, $3) }
+  | expr EQUALEQUALLU expr                      { Rbinop(Ocmplu Ceq, $1, $3) }
+  | expr BANGEQUALLU expr                       { Rbinop(Ocmplu Cne, $1, $3) }
+  | expr LESSLU expr                            { Rbinop(Ocmplu Clt, $1, $3) }
+  | expr LESSEQUALLU expr                       { Rbinop(Ocmplu Cle, $1, $3) }
+  | expr GREATERLU expr                         { Rbinop(Ocmplu Cgt, $1, $3) }
+  | expr GREATEREQUALLU expr                    { Rbinop(Ocmplu 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) }
@@ -601,9 +683,11 @@ memory_chunk:
   | INT16S                                      { Mint16signed }
   | INT16U                                      { Mint16unsigned }
   | INT32                                       { Mint32 }
+  | INT64                                       { Mint64 }
   | INT                                         { Mint32 }
   | FLOAT32                                     { Mfloat32 }
   | FLOAT64                                     { Mfloat64 }
+  | FLOAT64AL32                                 { Mfloat64al32 }
   | FLOAT                                       { Mfloat64 }
 ;
 
@@ -612,6 +696,8 @@ memory_chunk:
 type_:
     INT                                         { Tint }
   | FLOAT                                       { Tfloat }
+  | LONG                                        { Tlong }
+  | SINGLE                                      { Tsingle }
 ;
 
 /* External functions */
@@ -623,6 +709,7 @@ eftok:
   | VOLATILE                                    { EFT_tok "volatile" }
   | EXTERN                                      { EFT_tok "extern" }
   | BUILTIN                                     { EFT_tok "builtin" }
+  | memory_chunk                                { EFT_chunk $1 }
 ;
 
 eftoks:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index f78f470..d0bccca 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -39,7 +39,7 @@ let ty_of_typ = function
   | Tint -> tint
   | Tfloat -> tfloat
   | Tlong -> tlong
-  | Tsingle -> tsingle
+  | Tsingle -> tfloat (* should be tsingle when supported *)
 
 let ty_of_sig_args tyl = List.map ty_of_typ tyl
 
@@ -56,7 +56,7 @@ let unify t1 t2 =
                               (name_of_type b1) (name_of_type b2)))
   | Base b, Var r -> r := Some (Base b)
   | Var r, Base b -> r := Some (Base b)
-  | Var r1, Var r2 -> r1 := Some (Var r2)
+  | Var r1, Var r2 -> if r1 != r2 then r1 := Some (Var r2)
 
 let unify_list l1 l2 =
   let ll1 = List.length l1 and ll2 = List.length l2 in
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index ad02ed8..5b91d41 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -62,7 +62,7 @@ let name_of_unop = function
   | Ofloatofintu -> "floatofintu"
   | Onegl -> "-l"
   | Onotl -> "~l"
-  | Ointoflong -> "intofflong"
+  | Ointoflong -> "intoflong"
   | Olongofint -> "longofint"
   | Olongofintu -> "longofintu"
   | Olongoffloat -> "longoffloat"
@@ -179,6 +179,13 @@ let rec print_sig p = function
       fprintf p "%s ->@ " (name_of_type t1);
       print_sig p {sig_args = tl; sig_res = tres}
 
+let rec just_skips s =
+  match s with
+  | Sskip -> true
+  | Sseq(s1,s2) -> just_skips s1 && just_skips s2
+  | _ -> false
+
+
 (* Statements *)
 
 let rec print_stmt p s =
@@ -207,17 +214,21 @@ let rec print_stmt p s =
                 print_expr_list (true, el)
                 print_sig sg
   | Sbuiltin(None, ef, el) ->
-      fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@])@;@]"
+      fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@])@ : @[<hov 0>%a@];@]"
                 (name_of_external ef)
                 print_expr_list (true, el)
+	        print_sig (ef_sig ef)
   | Sbuiltin(Some id, ef, el) ->
-      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]@]"
+      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]) : @[<hov 0>%a@];@]" 
                 (ident_name id)
                 (name_of_external ef)
                 print_expr_list (true, el)
-  | Sseq(Sskip, s2) ->
+	        print_sig (ef_sig ef)
+  | Sseq(s1,s2) when just_skips s1 && just_skips s2 ->
+      ()
+  | Sseq(s1, s2) when just_skips s1 -> 
       print_stmt p s2
-  | Sseq(s1, Sskip) ->
+  | Sseq(s1, s2) when just_skips s2 ->
       print_stmt p s1
   | Sseq(s1, s2) ->
       fprintf p "%a@ %a" print_stmt s1 print_stmt s2
@@ -225,10 +236,10 @@ let rec print_stmt p s =
       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
               print_expr e
               print_stmt s1
-  | Sifthenelse(e, Sskip, s2) ->
+(*  | Sifthenelse(e, Sskip, s2) ->
       fprintf p "@[<v 2>if (! %a) {@ %a@;<0 -2>}@]"
               expr (15, e)
-              print_stmt s2
+              print_stmt s2 *)
   | Sifthenelse(e, s1, s2) ->
       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
               print_expr e
@@ -292,7 +303,7 @@ let print_init_data p = function
   | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i)
   | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i)
   | Init_int32 i -> fprintf p "%ld" (camlint_of_coqint i)
-  | Init_int64 i -> fprintf p "%Ld" (camlint64_of_coqint i)
+  | Init_int64 i -> fprintf p "%LdLL" (camlint64_of_coqint i)
   | Init_float32 f -> fprintf p "float32 %F" (camlfloat_of_coqfloat f)
   | Init_float64 f -> fprintf p "%F" (camlfloat_of_coqfloat f)
   | Init_space i -> fprintf p "[%ld]" (camlint_of_coqint i)
@@ -326,6 +337,8 @@ let print_globdef p (id, gd) =
 
 let print_program p prog =
   fprintf p "@[<v 0>";
+  if extern_atom prog.prog_main <> "main" then
+    fprintf p "= \"%s\"\n" (extern_atom prog.prog_main);
   List.iter (print_globdef p) prog.prog_defs;
   fprintf p "@]@."