Merge of Andrew Tolmach's HASP-related changes

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

4 files changed, 120 insertions, 20 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 3506e50..780d812 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -24,7 +24,8 @@ let floatlit =
   ['0'-'9'] ['0'-'9' '_']* 
   ('.' ['0'-'9' '_']* )?
   (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)?
-let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '0'-'9']*
+let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']*
+let temp = "$" ['0'-'9'] ['0'-'9']*
 let intlit = "-"? ( ['0'-'9']+ | "0x" ['0'-'9' 'a'-'f' 'A'-'F']+
                                | "0o" ['0'-'7']+ | "0b" ['0'-'1']+ )
 let stringlit = "\"" [ ^ '"' ] * '"'
@@ -46,7 +47,6 @@ rule token = parse
   | ":"    { COLON }
   | ","    { COMMA }
   | "default" { DEFAULT }
-  | "$"    { DOLLAR }
   | "else"    { ELSE }
   | "="    { EQUAL }
   | "=="    { EQUALEQUAL }
@@ -59,6 +59,7 @@ rule token = parse
   | "float64"    { FLOAT64 }
   | "floatofint"    { FLOATOFINT }
   | "floatofintu"    { FLOATOFINTU }
+  | "goto"  { GOTO } 
   | ">"    { GREATER }
   | ">f"    { GREATERF }
   | ">u"    { GREATERU }
@@ -69,10 +70,13 @@ rule token = parse
   | ">>u"    { GREATERGREATERU }
   | "if"    { IF }
   | "in"    { IN }
+  | "inline" { INLINE }
   | "int"    { INT }
+  | "int16"    { INT16 }
   | "int16s"    { INT16S }
   | "int16u"    { INT16U }
   | "int32"    { INT32 }
+  | "int8"    { INT8 }
   | "int8s"    { INT8S }
   | "int8u"    { INT8U }
   | "intoffloat"    { INTOFFLOAT }
@@ -102,6 +106,7 @@ rule token = parse
   | "}"    { RBRACE }
   | "}}"    { RBRACERBRACE }
   | "]"    { RBRACKET }
+  | "readonly" { READONLY }
   | "return"    { RETURN }
   | ")"    { RPAREN }
   | ";"    { SEMICOLON }
@@ -116,12 +121,17 @@ rule token = parse
   | "~"    { TILDE }
   | "var"    { VAR }
   | "void"    { VOID }
+  | "volatile" { VOLATILE }
+  | "while" { WHILE }
 
   | intlit    { INTLIT(Int32.of_string(Lexing.lexeme lexbuf)) }
   | floatlit     { FLOATLIT(float_of_string(Lexing.lexeme lexbuf)) }
   | stringlit { let s = Lexing.lexeme lexbuf in
                 STRINGLIT(intern_string(String.sub s 1 (String.length s - 2))) }
-  | ident    { IDENT(intern_string(Lexing.lexeme lexbuf)) }
+  | ident    { IDENT(BinPos.Coq_xO (intern_string(Lexing.lexeme lexbuf))) }
+  | temp     { let s = Lexing.lexeme lexbuf in
+               let n = Int32.of_string(String.sub s 1 (String.length s -1)) in
+	       IDENT(if n = 0l then BinPos.Coq_xH else BinPos.Coq_xI (positive_of_camlint n)) }
   | eof      { EOF }
   | _        { raise(Error("illegal character `" ^ Char.escaped (Lexing.lexeme_char lexbuf 0) ^ "'")) }
 
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 3df3f54..c52261d 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -13,6 +13,10 @@
 /*                                                                     */
 /* *********************************************************************/
 
+/* HASP: Modified to parse global data declarations, other small changes */
+/* Note that this compiles a superset of the language defined by the AST, 
+   including function calls in expressions, matches, while statements, etc. */
+
 %{
 open Datatypes
 open Camlcoq
@@ -22,6 +26,7 @@ open Integers
 open AST
 open Cminor
 
+
 (** Naming function calls in expressions *)
 
 type rexpr =
@@ -40,7 +45,7 @@ let temporaries = ref []
 let mktemp () =
   incr temp_counter;
   let n = Printf.sprintf "__t%d" !temp_counter in
-  let id = intern_string n in
+  let id = Coq_xO (intern_string n) in
   temporaries := id :: !temporaries;
   id
 
@@ -123,6 +128,9 @@ let mktailcall sg e1 el =
   let cl = convert_rexpr_list el in
   prepend_seq !convert_accu (Stailcall(sg, c1, cl))
 
+let mkwhile expr body =
+  Sblock (Sloop (mkifthenelse expr body (Sexit O)))
+
 (** Other constructors *)
 
 let intconst n =
@@ -133,7 +141,7 @@ let andbool e1 e2 =
 let orbool e1 e2 =
   Rcondition(e1, intconst 1l, e2)
 
-let exitnum n = nat_of_camlint(Int32.pred n)
+let exitnum n = nat_of_camlint n
 
 let mkswitch expr (cases, dfl) =
   convert_accu := [];
@@ -207,7 +215,6 @@ let mkmatch expr cases =
 %token COLON
 %token COMMA
 %token DEFAULT
-%token DOLLAR
 %token ELSE
 %token EQUAL
 %token EQUALEQUAL
@@ -222,6 +229,7 @@ let mkmatch expr cases =
 %token <float> FLOATLIT
 %token FLOATOFINT
 %token FLOATOFINTU
+%token GOTO
 %token GREATER
 %token GREATERF
 %token GREATERU
@@ -233,10 +241,13 @@ let mkmatch expr cases =
 %token <AST.ident> IDENT
 %token IF
 %token IN
+%token INLINE
 %token INT
+%token INT16
 %token INT16S
 %token INT16U
 %token INT32
+%token INT8
 %token INT8S
 %token INT8U
 %token <int32> INTLIT
@@ -267,6 +278,7 @@ let mkmatch expr cases =
 %token RBRACE
 %token RBRACERBRACE
 %token RBRACKET
+%token READONLY
 %token RETURN
 %token RPAREN
 %token SEMICOLON
@@ -282,6 +294,8 @@ let mkmatch expr cases =
 %token TAILCALL
 %token VAR
 %token VOID
+%token VOLATILE
+%token WHILE
 
 /* Precedences from low to high */
 
@@ -323,11 +337,47 @@ global_declarations:
 ;
 
 global_declaration:
-    VAR STRINGLIT LBRACKET INTLIT RBRACKET
+    VAR STRINGLIT LBRACKET INTLIT RBRACKET  /* old style */
       { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
               gvar_readonly = false; gvar_volatile = false}) }
+  | VAR STRINGLIT is_readonly is_volatile LBRACE init_data_list RBRACE
+       { ($2, {gvar_info = (); gvar_init = List.rev $6;
+               gvar_readonly = $3; gvar_volatile = $4; } ) }
 ;
 
+is_readonly:
+  /* empty */          { false }
+  | READONLY           { true }
+
+is_volatile:
+  /* empty */          { false }
+  |  VOLATILE          { true }
+
+init_data_list:
+    /* empty */                                 { [] }
+   | init_data_list_1                           { $1 }
+ ;
+ 
+init_data_list_1:
+     init_data                                   { [$1] }
+   | init_data_list_1 COMMA init_data            { $3 :: $1 }
+ ;
+ 
+init_data:
+     INT8 INTLIT                                 { Init_int8 (coqint_of_camlint $2) }
+   | INT16 INTLIT                                { Init_int16 (coqint_of_camlint $2) }
+   | INT32 INTLIT                                { Init_int32 (coqint_of_camlint $2) }
+   | INT INTLIT                                  { Init_int32 (coqint_of_camlint $2) }
+   | INTLIT                                      { Init_int32 (coqint_of_camlint $1) }
+   | FLOAT32 FLOATLIT                            { Init_float32 ($2) }
+   | FLOAT64 FLOATLIT                            { Init_float64 ($2) }
+   | FLOAT FLOATLIT                              { Init_float64 ($2) }
+   | FLOATLIT                                    { Init_float64 ($1) }
+   | LBRACKET INTLIT RBRACKET                    { Init_space (z_of_camlint $2) }
+   | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof ($3, coqint_of_camlint $1) }
+ ;
+ 
+
 proc_list:
     /* empty */                                 { [] }
   | proc_list proc                              { $2 :: $1 }
@@ -345,13 +395,14 @@ proc:
       { let tmp = !temporaries in
         temporaries := [];
         temp_counter := 0;
-        ($1, Internal { fn_sig = $6;
-                        fn_params = List.rev $3;
-                        fn_vars = List.rev (tmp @ $9);
-                        fn_stackspace = $8;
-                        fn_body = $10 }) }
+        ($1,
+        Internal { fn_sig = $6;
+                   fn_params = List.rev $3;
+                   fn_vars = List.rev (tmp @ $9);
+                   fn_stackspace = $8;
+                   fn_body = $10 }) }
   | EXTERN STRINGLIT COLON signature 
-      { ($2, External(EF_external($2, $4))) }
+      { ($2, External(EF_external($2,$4))) }
 ;
 
 signature:
@@ -408,6 +459,9 @@ stmt:
                                                 { mkmatch $3 $6 }
   | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON
                                                 { mktailcall $7 $2 $4 }
+  | WHILE LPAREN expr RPAREN stmts              { mkwhile $3 $5 }
+  | IDENT COLON stmts                           { Slabel ($1,$3) }
+  | GOTO IDENT SEMICOLON                        { Sgoto $2 }
 ;
 
 stmts:
@@ -525,3 +579,4 @@ type_:
     INT                                         { Tint }
   | FLOAT                                       { Tfloat }
 ;
+
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 110e735..330c6c2 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -42,7 +42,7 @@ let rec precedence = function
   | Eload _ -> (15, RtoL)
   | Econdition _ -> (3, RtoL)
 
-(* Naming idents.  We assume we run after Cminorgen, which encoded idents. *)
+(* Naming idents.  We assume idents are encoded as in Cminorgen. *)
 
 let ident_name id =
   match id with
@@ -185,7 +185,7 @@ let rec print_stmt p s =
                 print_expr_list (true, el)
                 print_sig sg
   | Scall(Some id, sg, e1, el) ->
-      fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@]);@] : @[<hov 0>%a@]"
+      fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@])@] : @[<hov 0>%a;@]"
                 (ident_name id)
                 print_expr e1
                 print_expr_list (true, el)
@@ -245,9 +245,9 @@ let rec print_stmt p s =
   | Sreturn (Some e) ->
       fprintf p "return %a;" print_expr e
   | Slabel(lbl, s1) ->
-      fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1
+      fprintf p "%s:@ %a" (ident_name lbl) print_stmt s1  (* wrong for Cminorgen output *)
   | Sgoto lbl ->
-      fprintf p "goto %s;" (extern_atom lbl)
+      fprintf p "goto %s;" (ident_name lbl)               (* wrong for Cminorgen output *)
 
 (* Functions *)
 
@@ -273,15 +273,50 @@ let print_function p id f =
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ "
 
+let print_extfun p id ef =
+  fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ "
+    (extern_atom id) print_sig (ef_sig ef)
+
 let print_fundef p (id, fd) =
   match fd with
   | External ef ->
-      () (* Todo? *)
+      print_extfun p id ef
   | Internal f ->
       print_function p id f
 
+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_float32 f -> fprintf p "float32 %F" f
+  | Init_float64 f -> fprintf p "%F" f
+  | Init_space i -> fprintf p "[%ld]" (camlint_of_coqint i)
+  | Init_addrof(id,off) -> fprintf p "%ld(\"%s\")" (camlint_of_coqint off) (extern_atom id)
+
+let rec print_init_data_list p = function
+  | [] -> ()
+  | [item] -> print_init_data p item
+  | item::rest -> 
+      (print_init_data p item;
+       fprintf p ",";
+       print_init_data_list p rest)
+
+let print_globvar p gv = 
+  if (gv.gvar_readonly) then
+    fprintf p "readonly ";
+  if (gv.gvar_volatile) then
+    fprintf p "volatile ";
+  fprintf p "{";
+  print_init_data_list p gv.gvar_init;
+  fprintf p "}"
+
+let print_var p (id, gv) =
+  fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv
+
 let print_program p prog =
-  fprintf p "@[<v 0>";
+  fprintf p "@[<v>";
+  List.iter (print_var p) prog.prog_vars;
+  fprintf p "@]@[<v 0>";
   List.iter (print_fundef p) prog.prog_funct;
   fprintf p "@]@."
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index a9c8f97..28d2b06 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -319,7 +319,7 @@ Fixpoint add_vars (map: mapping) (names: list ident)
 
 Definition find_var (map: mapping) (name: ident) : mon reg :=
   match PTree.get name map.(map_vars) with
-  | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil)
+  | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTXL name :: nil)
   | Some r => ret r
   end.