source: Deliverables/D2.2/8051/src/cminor/cminorParser.mly @ 740

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 18.9 KB
Line 
1/* Adapted from Leroy's CompCert */
2/* TODO: check coherence with CminorPrinter */
3
4/* tokens ALLOC, DOLLAR, IN, LET, p_let were unused and have been removed */
5/* precedence levels unused were also removed */
6
7/* *********************************************************************/
8/*                                                                     */
9/*              The Compcert verified compiler                         */
10/*                                                                     */
11/*          Xavier Leroy, INRIA Paris-Rocquencourt                     */
12/*                                                                     */
13/*  Copyright Institut National de Recherche en Informatique et en     */
14/*  Automatique.  All rights reserved.  This file is distributed       */
15/*  under the terms of the GNU General Public License as published by  */
16/*  the Free Software Foundation, either version 2 of the License, or  */
17/*  (at your option) any later version.  This file is also distributed */
18/*  under the terms of the INRIA Non-Commercial License Agreement.     */
19/*                                                                     */
20/* *********************************************************************/
21
22%{
23
24  open AST
25  open Cminor
26  open Memory
27
28  (* Function calls are not allowed in the AST of expressions, but function
29     calls in the AST of statements have a special argument which can be used to
30     store the result of the function call in a side-effect manner.
31     Example: the statement
32       x = y + f(z,g(t));
33     will be transformed into the (simplified syntax) AST statements
34       g(_t1,t)
35       f(_t2,y,_t1);
36       x = y + _t2
37     where _t1 and _t2 are fresh temporary variables. *)
38
39
40  (* Thus, to deal with function calls in expressions, we need to create fresh
41     temporary variables *)
42
43  let temp_counter = ref 0
44  let temporaries = ref []
45
46  let mktemp () =
47    incr temp_counter;
48    let id = Printf.sprintf "_t%d" !temp_counter in
49      temporaries := id :: !temporaries;
50      id
51
52
53  (* Expressions with function calls *)
54
55  type rexpr =
56    | RId of ident
57    | RCst of cst
58    | ROp1 of op1 * rexpr
59    | ROp2 of op2 * rexpr * rexpr
60    | RMem of Memory.quantity * rexpr
61    | RCond of rexpr * rexpr * rexpr
62    | RCall of rexpr * rexpr list * signature
63
64  (* [convert_accu] stores the function calls of expressions with function
65     calls being converted to expressions without function calls *)
66  let convert_accu = ref []
67
68  (* [convert_rexpr rexpr] converts the expression with function calls [rexpr]
69     into an expression without function calls. The function calls in [rexpr]
70     are stored in [convert_accu] *)
71  let rec convert_rexpr = function
72    | RId id -> Id id
73    | RCst c -> Cst c
74    | ROp1 (op, e1) -> Op1 (op, convert_rexpr e1)
75    | ROp2 (op, e1, e2) -> Op2 (op, convert_rexpr e1, convert_rexpr e2)
76    | RMem (chunk, e1) -> Mem (chunk, convert_rexpr e1)
77    | RCond (e1, e2, e3) ->
78        Cond (convert_rexpr e1, convert_rexpr e2, convert_rexpr e3)
79    | RCall(e1, el, sg) ->
80        let c1 = convert_rexpr e1 in
81        let cl = convert_rexpr_list el in
82        let t = mktemp() in
83          convert_accu := St_call (Some t, c1, cl, sg) :: !convert_accu;
84          Id t
85
86  and convert_rexpr_list el = List.map convert_rexpr el
87
88  (* [prepend_seq stmts last] reverses and sequences the list of statements
89     [stmts] and puts [last] at the end *)
90  let rec prepend_seq stmts last =
91    match stmts with
92      | [] -> last
93      | s1 :: sl -> prepend_seq sl (St_seq (s1, last))
94
95  (* [mkeval e] creates the AST statement associated to the Cminor instruction
96       e;
97     where [e] is an expression with possible function calls *)
98  let mkeval e =
99    convert_accu := [];
100    match e with
101      | RCall (e1, el, sg) ->
102          let c1 = convert_rexpr e1 in
103          let cl = convert_rexpr_list el in
104            prepend_seq !convert_accu (St_call (None, c1, cl, sg))
105      | _ ->
106          ignore (convert_rexpr e);
107          prepend_seq !convert_accu St_skip
108
109  (* [mkeval id e] creates the AST statement associated to the Cminor
110     instruction
111       id = e;
112     where [e] is an expression with possible function calls *)
113  let mkassign id e =
114    convert_accu := [];
115    match e with
116      | RCall (e1, el, sg) ->
117          let c1 = convert_rexpr e1 in
118          let cl = convert_rexpr_list el in
119            prepend_seq !convert_accu (St_call (Some id, c1, cl, sg))
120      | _ ->
121          let c = convert_rexpr e in
122            prepend_seq !convert_accu (St_assign (id, c))
123
124  (* [mkstore size e1 e2] creates the AST statement associated to the Cminor
125     instruction
126       size[e1] = e2;
127     where [e1] and [e2] are expressions with possible function calls *)
128  let mkstore size e1 e2 =
129    convert_accu := [];
130    let c1 = convert_rexpr e1 in
131    let c2 = convert_rexpr e2 in
132      prepend_seq !convert_accu (St_store (size, c1, c2))
133
134  (* [mkifthenelse e s1 s2] creates the AST statement associated to the Cminor
135     instruction
136       if (e) { s1 } else { s2 }
137     where [e] is an expression with possible function calls *)
138  let mkifthenelse e s1 s2 =
139    convert_accu := [];
140    let c = convert_rexpr e in
141      prepend_seq !convert_accu (St_ifthenelse (c, s1, s2))
142
143  (* [mkreturn_some e] creates the AST statement associated to the Cminor
144     instruction
145       return e;
146     where [e] is an expression with possible function calls *)
147  let mkreturn_some e =
148    convert_accu := [];
149    let c = convert_rexpr e in
150      prepend_seq !convert_accu (St_return (Some c))
151
152  (* [mkswitch e (cases, dfl)] creates the AST statement associated to the
153     Cminor instruction
154       switch (e) {
155         case i: exit j_i;
156         ...
157         default: exit j_default; }
158     where [e] is an expression with possible function calls *)
159  let mkswitch e (cases, dfl) =
160    convert_accu := [];
161    let c = convert_rexpr e in
162      prepend_seq !convert_accu (St_switch (c, cases, dfl))
163
164  (* The Cminor instruction
165      match (e) {
166        case 0: s0;
167        case 1: s1;
168        case 2: s2; }
169     is syntaxic sugar for the Cminor instruction
170       block {
171         block {
172           block {
173             block {
174               switch (e) {
175                 case 0: exit 0;
176                 case 1: exit 1;
177                 default: exit 2; }
178             } s0; exit 2;
179           } s1; exit 1;
180         } s2;
181       }
182     Note that matches are assumed to be exhaustive *)
183
184  let mkmatch_aux e cases =
185    let ncases = List.length cases in
186    let rec mktable n = function
187      | [] -> assert false
188      | [key, action] -> []
189      | (key, action) :: rem -> (key, n) :: mktable (n+1) rem in
190    let sw =
191      St_switch (e, mktable 0 cases, pred ncases) in
192    let rec mkblocks body n = function
193      | [] -> assert false
194      | [key, action] -> St_block (St_seq (body, action))
195      | (key, action) :: rem ->
196          mkblocks
197            (St_block (St_seq (body, St_seq (action, St_exit n))))
198            (pred n) rem in
199      mkblocks (St_block sw) (pred ncases) cases
200
201  (* [mkmatch e cases] creates the AST statement associated to the Cminor
202     instruction
203       match (e) {
204         case i: s_i;
205         ... }
206     where [e] is an expression with possible function calls *)
207  let mkmatch e cases =
208    convert_accu := [];
209    let c = convert_rexpr e in
210    let s =
211      match cases with
212        | [] -> St_skip (* ??? *)
213        | [key, action] -> action
214        | _ -> mkmatch_aux c cases in
215      prepend_seq !convert_accu s
216
217  (* [mktailcall f [e1;e2;...] sig] creates the AST statement associated to the
218     Cminor instruction
219     tailcall f(e1,e2,...): sig
220     where [e], [e1], [e2], ... are expressions with possible function calls *)
221  let mktailcall e1 el sg =
222    convert_accu := [];
223    let c1 = convert_rexpr e1 in
224    let cl = convert_rexpr_list el in
225      prepend_seq !convert_accu (St_tailcall (c1, cl, sg))
226
227  (* Parse error handler *)
228  let raise_error (_, pos) s = Error.error "parse error" pos (s ^ "\n")
229
230%}
231
232%token ABSF
233%token AMPERSAND
234%token AMPERSANDAMPERSAND
235%token BANG
236%token BANGEQUAL
237%token BANGEQUALF
238%token BANGEQUALU
239%token BAR
240%token BARBAR
241%token CARET
242%token CASE
243%token COLON
244%token COMMA
245%token DEFAULT
246%token ELSE
247%token EQUAL
248%token EQUALEQUAL
249%token EQUALEQUALF
250%token EQUALEQUALU
251%token EOF
252%token EXIT
253%token EXTERN
254%token FLOAT
255%token FLOAT32
256%token FLOAT64
257%token <float> FLOATLIT
258%token FLOATOFINT
259%token FLOATOFINTU
260%token GREATER
261%token GREATERF
262%token GREATERU
263%token GREATEREQUAL
264%token GREATEREQUALF
265%token GREATEREQUALU
266%token GREATERGREATER
267%token GREATERGREATERU
268%token <string> IDENT
269%token IF
270%token INT
271%token INT16
272%token INT16S
273%token INT16U
274%token INT32
275%token INT8
276%token INT8S
277%token INT8U
278%token <int> INTLIT
279%token INTOFFLOAT
280%token INTUOFFLOAT
281%token LBRACE
282/* %token LBRACELBRACE */
283%token LBRACKET
284%token LESS
285%token LESSU
286%token LESSF
287%token LESSEQUAL
288%token LESSEQUALU
289%token LESSEQUALF
290%token LESSLESS
291%token LOOP
292%token LPAREN
293%token MATCH
294%token MINUS
295%token MINUSF
296%token MINUSGREATER
297%token PERCENT
298%token PERCENTU
299%token PLUS
300%token PLUSF
301%token QUESTION
302%token RBRACE
303/* %token RBRACERBRACE */
304%token RBRACKET
305%token RETURN
306%token RPAREN
307%token SEMICOLON
308%token SLASH
309%token SLASHF
310%token SLASHU
311%token STACK
312%token STAR
313%token STARF
314%token <string> STRINGLIT
315%token SWITCH
316%token TILDE
317%token TAILCALL
318%token VAR
319%token VOID
320%token GOTO BLOCK
321%token PTR
322
323/* Unused */
324/* %token ALLOC DOLLAR IN LET p_let */
325
326/* Precedences from low to high */
327
328/* %left COMMA */
329/* %left p_let */
330/* %right EQUAL */
331%right QUESTION COLON
332%left BARBAR
333%left AMPERSANDAMPERSAND
334%left BAR
335%left CARET
336%left AMPERSAND
337%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF
338%left LESSLESS GREATERGREATER GREATERGREATERU
339%left PLUS PLUSF MINUS MINUSF
340%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
341%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 /* ALLOC */
342%left LPAREN
343
344/* Entry point */
345
346%start program
347%type <Cminor.program> program
348
349%%
350
351%inline position(X): x = X { (x, Position.lex_join $startpos $endpos) }
352
353/* Programs */
354
355program:
356    global_declarations proc_list EOF { { vars   = List.rev $1 ;
357                                          functs = List.rev $2 ;
358                                          main   = Some "main" } }
359;
360
361global_declarations:
362    /* empty */                            { [] }
363  | global_declarations global_declaration { $2 :: $1 }
364;
365
366global_declaration:
367    VAR STRINGLIT init_datas { ($2, List.rev $3) }
368  | pos = position(error)    { raise_error pos
369                                 "Global declaration syntax error" }
370;
371
372init_datas:
373    /* empty */                  { [] }
374  | init_data                    { [$1] }
375  | LBRACE init_data_list RBRACE { $2 }
376;
377
378init_data:
379    INTLIT                         { AST.Data_int32 $1 }
380  | FLOATLIT                       { AST.Data_float32 $1 }
381  | LPAREN INT8 RPAREN INTLIT      { AST.Data_int8 $4 }
382  | LPAREN INT16 RPAREN INTLIT     { AST.Data_int16 $4 }
383  | LPAREN INT32 RPAREN INTLIT     { AST.Data_int32 $4 }
384  | LPAREN FLOAT32 RPAREN FLOATLIT { AST.Data_float32 $4 }
385  | LPAREN FLOAT64 RPAREN FLOATLIT { AST.Data_float64 $4 }
386  | LBRACKET INTLIT RBRACKET       { AST.Data_reserve $2 }
387;
388
389quantity:
390    INTLIT { Memory.QInt $1 }
391  | PTR    { Memory.QPtr }
392
393init_data_list:
394    init_data                      { [$1] }
395  | init_data COMMA init_data_list { $1 :: $3 }
396;
397
398proc_list:
399    /* empty */    { [] }
400  | proc_list proc { $2 :: $1 }
401;
402
403/* Procedures */
404
405proc:
406    STRINGLIT LPAREN parameters RPAREN COLON signature
407    LBRACE
408      stack_declaration
409      var_declarations
410      stmt_list
411    RBRACE
412  { let tmp = !temporaries in
413      temporaries := [];
414      temp_counter := 0;
415      ($1, F_int { f_sig = $6 ;
416                   f_params = List.rev $3 ;
417                   f_vars = List.rev (tmp @ $9) ;
418                   f_ptrs = [] (* TODO *) ;
419                   f_stacksize = $8 ;
420                   f_body = $10 }) }
421  | EXTERN STRINGLIT COLON signature { ($2, F_ext { ef_tag = $2 ;
422                                                    ef_sig = $4 }) }
423  | pos = position(error) { raise_error pos
424                            "Procedure or function declaration syntax error" }
425;
426
427parameters:
428    /* empty */    { [] }
429  | parameter_list { $1 }
430;
431
432parameter_list:
433    IDENT                      { $1 :: [] }
434  | parameter_list COMMA IDENT { $3 :: $1 }
435  | pos = position(error) { raise_error pos
436                            "Parameter declaration syntax error" }
437;
438
439signature:
440    type_  { { args = [] ; res = Type_ret $1 } }
441  | VOID
442      { { args = [] ; res = Type_void } }
443  | type_ MINUSGREATER signature
444          { let s = $3 in {s with args = $1 :: s.args } }
445  | pos = position(error) { raise_error pos "Signature syntax error" }
446;
447
448stack_declaration:
449    /* empty */            { 0 }
450  | STACK INTLIT SEMICOLON { $2 }
451  | pos = position(error)  { raise_error pos "Stack declaration syntax error" }
452;
453
454var_declarations:
455    /* empty */                      { [] }
456  | var_declarations var_declaration { $2 @ $1 }
457  | pos = position(error)            { raise_error pos
458                                         "Variable declaration syntax error" }
459;
460
461var_declaration:
462    VAR parameter_list SEMICOLON { $2 }
463;
464
465/* Statements */
466
467stmt:
468    expr SEMICOLON                         { mkeval $1 }
469  | IDENT EQUAL expr SEMICOLON             { mkassign $1 $3 }
470  | quantity LBRACKET expr RBRACKET EQUAL expr SEMICOLON
471      { mkstore $1 $3 $6 }
472  | IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 }
473  | IF LPAREN expr RPAREN stmts            { mkifthenelse $3 $5 St_skip }
474  | LOOP stmts                             { St_loop $2 }
475  | BLOCK LBRACE stmt_list RBRACE          { St_block $3 }
476  | EXIT SEMICOLON                         { St_exit 0 }
477  | EXIT INTLIT SEMICOLON                  { St_exit $2 }
478  | RETURN SEMICOLON                       { St_return None }
479  | RETURN expr SEMICOLON                  { mkreturn_some $2 }
480  | GOTO IDENT SEMICOLON                   { St_goto $2 }
481  | IDENT COLON stmt                       { St_label ($1, $3) }
482  | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
483        { mkswitch $3 $6 }
484  | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
485          { mkmatch $3 $6 }
486  | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON
487              { mktailcall $2 $4 $7 }
488;
489
490stmt_list:
491    /* empty */    { St_skip }
492  | stmt stmt_list { St_seq ($1, $2) }
493  | pos = position(error) { raise_error pos "Statement syntax error" }
494;
495
496stmts:
497    LBRACE stmt_list RBRACE { $2 }
498  | stmt                    { $1 }
499;
500
501switch_cases:
502    DEFAULT COLON EXIT INTLIT SEMICOLON
503    { ([], $4) }
504  | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases
505        { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
506  | pos = position(error) { raise_error pos "Syntax error in switch construct" }
507;
508
509match_cases:
510    /* empty */                             { [] }
511  | CASE INTLIT COLON stmt_list match_cases { ($2, $4) :: $5 }
512  | pos = position(error) { raise_error pos "Syntax error in match construct" }
513;
514
515/* Expressions */
516
517expr:
518    LPAREN expr RPAREN                      { $2 }
519  | IDENT                               { RId $1 }
520  | INTLIT                              { RCst (Cst_int $1) }
521  | FLOATLIT                            { RCst (Cst_float $1) }
522  | STRINGLIT                           { RCst (Cst_addrsymbol $1) }
523  | AMPERSAND INTLIT                    { RCst (Cst_stackoffset $2) }
524  | MINUS expr    %prec p_uminus        { ROp1 (Op_negint, $2) }
525  | MINUSF expr   %prec p_uminus        { ROp1 (Op_negf, $2) }
526  | ABSF expr                           { ROp1 (Op_absf, $2) }
527  | INTOFFLOAT expr                     { ROp1 (Op_intoffloat, $2) }
528  | INTUOFFLOAT expr                    { ROp1 (Op_intuoffloat, $2) }
529  | FLOATOFINT expr                     { ROp1 (Op_floatofint, $2) }
530  | FLOATOFINTU expr                    { ROp1 (Op_floatofintu, $2) }
531  | TILDE expr                          { ROp1 (Op_notint, $2) }
532  | BANG expr                           { ROp1 (Op_notbool, $2) }
533  | INT8S expr                          { ROp1 (Op_cast8signed, $2) }
534  | INT8U expr                          { ROp1 (Op_cast8unsigned, $2) }
535  | INT16S expr                         { ROp1 (Op_cast16signed, $2) }
536  | INT16U expr                         { ROp1 (Op_cast16unsigned, $2) }
537  | FLOAT32 expr                        { ROp1 (Op_singleoffloat, $2) }
538  | expr PLUS expr                      { ROp2 (Op_add, $1, $3) }
539  | expr MINUS expr                     { ROp2 (Op_sub, $1, $3) }
540  | expr STAR expr                      { ROp2 (Op_mul, $1, $3) }
541  | expr SLASH expr                     { ROp2 (Op_div, $1, $3) }
542  | expr PERCENT expr                   { ROp2 (Op_mod, $1, $3) }
543  | expr SLASHU expr                    { ROp2 (Op_divu, $1, $3) }
544  | expr PERCENTU expr                  { ROp2 (Op_modu, $1, $3) }
545  | expr AMPERSAND expr                 { ROp2 (Op_and, $1, $3) }
546  | expr BAR expr                       { ROp2 (Op_or, $1, $3) }
547  | expr CARET expr                     { ROp2 (Op_xor, $1, $3) }
548  | expr LESSLESS expr                  { ROp2 (Op_shl, $1, $3) }
549  | expr GREATERGREATER expr            { ROp2 (Op_shr, $1, $3) }
550  | expr GREATERGREATERU expr           { ROp2 (Op_shru, $1, $3) }
551  | expr PLUSF expr                     { ROp2 (Op_addf, $1, $3) }
552  | expr MINUSF expr                    { ROp2 (Op_subf, $1, $3) }
553  | expr STARF expr                     { ROp2 (Op_mulf, $1, $3) }
554  | expr SLASHF expr                    { ROp2 (Op_divf, $1, $3) }
555  | expr EQUALEQUAL expr                { ROp2 (Op_cmp Cmp_eq, $1, $3) }
556  | expr BANGEQUAL expr                 { ROp2 (Op_cmp Cmp_ne, $1, $3) }
557  | expr LESS expr                      { ROp2 (Op_cmp Cmp_lt, $1, $3) }
558  | expr LESSEQUAL expr                 { ROp2 (Op_cmp Cmp_le, $1, $3) }
559  | expr GREATER expr                   { ROp2 (Op_cmp Cmp_gt, $1, $3) }
560  | expr GREATEREQUAL expr              { ROp2 (Op_cmp Cmp_ge, $1, $3) }
561  | expr EQUALEQUALU expr               { ROp2 (Op_cmpu Cmp_eq, $1, $3) }
562  | expr BANGEQUALU expr                { ROp2 (Op_cmpu Cmp_ne, $1, $3) }
563  | expr LESSU expr                     { ROp2 (Op_cmpu Cmp_lt, $1, $3) }
564  | expr LESSEQUALU expr                { ROp2 (Op_cmpu Cmp_le, $1, $3) }
565  | expr GREATERU expr                  { ROp2 (Op_cmpu Cmp_gt, $1, $3) }
566  | expr GREATEREQUALU expr             { ROp2 (Op_cmpu Cmp_ge, $1, $3) }
567  | expr EQUALEQUALF expr               { ROp2 (Op_cmpf Cmp_eq, $1, $3) }
568  | expr BANGEQUALF expr                { ROp2 (Op_cmpf Cmp_ne, $1, $3) }
569  | expr LESSF expr                     { ROp2 (Op_cmpf Cmp_lt, $1, $3) }
570  | expr LESSEQUALF expr                { ROp2 (Op_cmpf Cmp_le, $1, $3) }
571  | expr GREATERF expr                  { ROp2 (Op_cmpf Cmp_gt, $1, $3) }
572  | expr GREATEREQUALF expr             { ROp2 (Op_cmpf Cmp_ge, $1, $3) }
573  | quantity LBRACKET expr RBRACKET       { RMem ($1, $3) }
574  | expr AMPERSANDAMPERSAND expr        { RCond ($1, $3, RCst (Cst_int 0)) }
575  | expr BARBAR expr                    { RCond ($1, RCst (Cst_int 1), $3) }
576  | expr QUESTION expr COLON expr       { RCond ($1, $3, $5) }
577  | expr LPAREN expr_list RPAREN COLON signature
578      { RCall ($1, $3, $6) }
579  | pos = position(error) { raise_error pos "Expression syntax error" }
580;
581
582expr_list:
583    /* empty */ { [] }
584  | expr_list_1 { $1 }
585;
586
587expr_list_1:
588    expr /* %prec COMMA */ { $1 :: [] }
589  | expr COMMA expr_list_1 { $1 :: $3 }
590;
591
592type_:
593    INT   { Sig_int }
594  | FLOAT { Sig_float }
595;
596
Note: See TracBrowser for help on using the repository browser.