source: rtems-central/formal/promela/src/src/modules/promela_yacc/promela/yacc.py @ ebe9144

Last change on this file since ebe9144 was ebe9144, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/13/23 at 15:42:20

modifications made to promela_yacc

  • Property mode set to 100644
File size: 26.3 KB
Line 
1"""Parser for Promela, using Python Lex-Yacc (PLY).
2
3
4References
5==========
6
7Holzmann G.J., The SPIN Model Checker,
8    Addison-Wesley, 2004, pp. 365--368
9    http://spinroot.com/spin/Man/Quick.html
10"""
11from __future__ import absolute_import
12from __future__ import division
13import logging
14import os
15import subprocess
16import warnings
17import ply.yacc
18from sys import platform as _platform
19# inline
20#
21# import promela.ast as promela_ast
22# from promela import lex
23
24
25TABMODULE = 'promela.promela_parsetab'
26logger = logging.getLogger(__name__)
27
28
29class Parser(object):
30    """Production rules for Promela parser."""
31
32    logger = logger
33    tabmodule = TABMODULE
34    start = 'program'
35    # http://spinroot.com/spin/Man/operators.html
36    # spin.y
37    # lowest to highest
38    precedence = (
39        ('right', 'EQUALS'),
40        ('left', 'TX2', 'RCV', 'R_RCV'),
41        ('left', 'IMPLIES', 'EQUIV'),
42        ('left', 'LOR'),
43        ('left', 'LAND'),
44        ('left', 'ALWAYS', 'EVENTUALLY'),
45        ('left', 'UNTIL', 'WEAK_UNTIL', 'RELEASE'),
46        ('right', 'NEXT'),
47        ('left', 'OR'),
48        ('left', 'XOR'),
49        ('left', 'AND'),
50        ('left', 'EQ', 'NE'),
51        ('left', 'LT', 'LE', 'GT', 'GE'),
52        ('left', 'LSHIFT', 'RSHIFT'),
53        ('left', 'PLUS', 'MINUS'),
54        ('left', 'TIMES', 'DIVIDE', 'MOD'),
55        ('left', 'INCR', 'DECR'),
56        ('right', 'LNOT', 'NOT', 'UMINUS', 'NEG'),  # LNOT is also SND
57        ('left', 'DOT'),
58        ('left', 'LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET'))
59
60    def __init__(self, ast=None, lexer=None):
61        if ast is None:
62            import promela.ast as ast
63        if lexer is None:
64            from promela import lex
65            lexer = lex.Lexer()
66        self.lexer = lexer
67        self.ast = ast
68        self.tokens = self.lexer.tokens
69        self.build()
70
71    def build(self, tabmodule=None, outputdir='', write_tables=False,
72              debug=False, debuglog=None, errorlog=None):
73        """Build parser using `ply.yacc`.
74
75        Default table module is `self.tabmodule`.
76        Module logger used as default debug logger.
77        Default error logger is that created by PLY.
78        """
79        if tabmodule is None:
80            tabmodule = self.tabmodule
81        if debug and debuglog is None:
82            debuglog = self.logger
83        self.parser = ply.yacc.yacc(
84            method='LALR',
85            module=self,
86            start=self.start,
87            tabmodule=tabmodule,
88            outputdir=outputdir,
89            write_tables=write_tables,
90            debug=debug,
91            debuglog=debuglog,
92            errorlog=errorlog)
93
94    def parse(self, promela, fic):
95        """Parse string of Promela code."""
96        s = cpp(promela, fic)
97        program = self.parser.parse(
98            s, lexer=self.lexer.lexer, debug=self.logger, tracking=True)
99        return program
100
101    def _iter(self, p):
102        if p[2] is not None:
103            p[1].append(p[2])
104        return p[1]
105
106    def _end(self, p):
107        if p[1] is None:
108            return list()
109        else:
110            return [p[1]]
111
112    # Top-level constructs
113    # ====================
114
115    def p_program(self, p):
116        """program : units"""
117        p[0] = self.ast.Program(p[1])
118
119    def p_program_empty(self, p):
120        """program : empty"""
121        p[0] = self.ast.Program([])
122
123    def p_units_iter(self, p):
124        """units : units unit"""
125        p[0] = self._iter(p)
126
127    def p_units_end(self, p):
128        """units : unit"""
129        p[0] = self._end(p)
130
131    # TODO: events, c_fcts, ns, error
132    def p_unit_proc(self, p):
133        """unit : proc
134                | inline
135                | init
136                | claim
137                | ltl
138        """
139        p[0] = (p[1], p.lineno(1))
140
141    def p_unit_decl(self, p):
142        """unit : one_decl
143                | utype
144        """
145        p[0] = (p[1], p.lineno(1))
146
147    def p_unit_semi(self, p):
148        """unit : semi"""
149
150    def p_proc(self, p):
151        ("""proc : prefix_proctype NAME"""
152         """       LPAREN decl RPAREN"""
153         """       opt_priority opt_enabler"""
154         """       body
155         """)
156        inst = p[1]
157        name = p[2]
158        args = p[4]
159        priority = p[6]
160        enabler = p[7]
161        body = p[8]
162
163        p[0] = self.ast.Proctype(
164            name, body, args=args, priority=priority,
165            provided=enabler, **inst)
166
167    def p_inline(self, p):
168        ("""inline : INLINE NAME"""
169         """         LPAREN var_list0 RPAREN"""
170         """         body
171         """)
172        p[0] = self.ast.InlineDef(name = p[2], decl = p[4], body = p[6])
173
174    # instantiator
175    def p_inst(self, p):
176        """prefix_proctype : ACTIVE opt_index proctype"""
177        d = p[3]
178        if p[2] is None:
179            n_active = self.ast.Integer('1')
180        else:
181            n_active = p[2]
182        d['active'] = int(n_active.value)
183        p[0] = d
184
185    def p_inactive_proctype(self, p):
186        """prefix_proctype : proctype"""
187        p[0] = p[1]
188
189    def p_opt_index(self, p):
190        """opt_index : LBRACKET expr RBRACKET
191                     | LBRACKET NAME RBRACKET
192        """
193        p[0] = p[2]
194
195    def p_opt_index_empty(self, p):
196        """opt_index : empty"""
197
198    def p_init(self, p):
199        """init : INIT opt_priority body"""
200        p[0] = self.ast.Init(name='init', body=p[3], priority=p[2])
201
202    def p_claim(self, p):
203        """claim : CLAIM optname body"""
204        name = p[2] if p[2] else 'never'
205        p[0] = self.ast.NeverClaim(name=name, body=p[3])
206
207    # user-defined type
208    def p_utype(self, p):
209        """utype : TYPEDEF NAME LBRACE decl_lst RBRACE"""
210        seq = self.ast.Sequence(p[4])
211        p[0] = self.ast.TypeDef(p[2], seq)
212
213    def p_ltl1(self, p):
214        """ltl : LTL NAME LBRACE expr RBRACE"""
215        p[0] = self.ast.LTL(p[4], name = p[2])
216
217    def p_ltl2(self, p):
218        """ltl : LTL LBRACE expr RBRACE"""
219        p[0] = self.ast.LTL(p[3])
220
221    # Declarations
222    # ============
223
224    def p_decl(self, p):
225        """decl : decl_lst"""
226        p[0] = self.ast.Sequence(p[1])
227
228    def p_decl_empty(self, p):
229        """decl : empty"""
230
231    def p_decl_lst_iter(self, p):
232        """decl_lst : one_decl SEMI decl_lst"""
233        p[0] = [p[1]] + p[3]
234
235    def p_decl_lst_end(self, p):
236        """decl_lst : one_decl"""
237        p[0] = [p[1]]
238
239    def p_decl0(self, p):
240        """decl0 : decl_lst0"""
241        p[0] = self.ast.Sequence(p[1])
242
243    def p_decl_empty0(self, p):
244        """decl0 : empty"""
245
246    def p_decl_lst_iter0(self, p):
247        """decl_lst0 : expr COMMA decl_lst0"""
248        p[0] = [p[1]] + p[3]
249
250    def p_decl_lst_end0(self, p):
251        """decl_lst0 : expr"""
252        p[0] = [p[1]]
253
254    def p_one_decl_visible(self, p):
255        """one_decl : vis typename var_list
256                    | vis NAME var_list
257        """
258        visible = p[1]
259        typ = p[2]
260        var_list = p[3]
261
262        p[0] = self.one_decl(typ, var_list, visible)
263
264    def p_one_decl(self, p):
265        """one_decl : typename var_list
266                    | NAME var_list
267        """
268        typ = p[1]
269        var_list = p[2]
270        p[0] = self.one_decl(typ, var_list)
271
272    def one_decl(self, typ, var_list, visible=None):
273        c = list()
274        for d in var_list:
275            v = self.ast.VarDef(vartype=typ, visible=visible, **d)
276            c.append(v)
277        return self.ast.Sequence(c)
278
279    # message type declaration
280    def p_one_decl_mtype_vis(self, p):
281        """one_decl : vis MTYPE asgn LBRACE name_list RBRACE"""
282        p[0] = self.ast.MessageType(p[5], visible=p[1])
283
284    def p_one_decl_mtype(self, p):
285        """one_decl : MTYPE asgn LBRACE name_list RBRACE"""
286        p[0] = self.ast.MessageType(p[4])
287
288    def p_name_list_iter(self, p):
289        """name_list : name_list COMMA NAME"""
290        p[1].append(p[3])
291        p[0] = p[1]
292
293    def p_name_list_end(self, p):
294        """name_list : NAME"""
295        p[0] = [p[1]]
296
297    def p_var_list_iter(self, p):
298        """var_list : ivar COMMA var_list"""
299        p[0] = [p[1]] + p[3]
300
301    def p_var_list_end(self, p):
302        """var_list : ivar"""
303        p[0] = [p[1]]
304
305    def p_var_list00_iter(self, p):
306        """var_list00 : ivar0 COMMA var_list00"""
307        p[0] = [p[1]] + p[3]
308
309    def p_var_list00_end(self, p):
310        """var_list00 : ivar0"""
311        p[0] = [p[1]]
312
313    def p_var_list0(self, p):
314        """var_list0 : var_list00"""
315        p[0] = p[1]
316
317    def p_var_list0_empty(self, p):
318        """var_list0 : empty"""
319        p[0] = []
320
321    # TODO: vardcl asgn LBRACE c_list RBRACE
322
323    def p_ivar0(self, p):
324        """ivar0 : NAME"""
325        p[0] = p[1]
326
327    # ivar = initialized variable
328    def p_ivar(self, p):
329        """ivar : vardcl"""
330        p[0] = p[1]
331
332    def p_ivar_asgn(self, p):
333        """ivar : vardcl asgn expr"""
334        expr = self.ast.Expression(p[3])
335        p[1]['initval'] = expr
336        p[0] = p[1]
337
338    def p_vardcl(self, p):
339        """vardcl : NAME"""
340        p[0] = {'name': p[1]}
341
342    # p.403, SPIN manual
343    def p_vardcl_unsigned(self, p):
344        """vardcl : NAME COLON const"""
345        p[0] = {'name': p[1], 'bitwidth': p[3]}
346
347    def p_vardcl_array(self, p):
348        """vardcl : NAME LBRACKET const_expr RBRACKET"""
349        p[0] = {'name': p[1], 'length': p[3]}
350
351    def p_vardcl_chan(self, p):
352        """vardcl : vardcl EQUALS ch_init"""
353        p[1].update(p[3])
354        p[0] = p[1]
355
356    def p_typename(self, p):
357        """typename : BIT
358                    | BOOL
359                    | BYTE
360                    | CHAN
361                    | INT
362                    | PID
363                    | SHORT
364                    | UNSIGNED
365                    | MTYPE
366        """
367        p[0] = p[1]
368
369    def p_ch_init(self, p):
370        ("""ch_init : LBRACKET const_expr RBRACKET """
371         """ OF LBRACE typ_list RBRACE""")
372        p[0] = {'length': p[2], 'msg_types': p[6]}
373
374    def p_typ_list_iter(self, p):
375        """typ_list : typ_list COMMA basetype"""
376        p[1].append(p[3])
377        p[0] = p[1]
378
379    def p_typ_list_end(self, p):
380        """typ_list : basetype"""
381        p[0] = [p[1]]
382
383    # TODO: | UNAME | error
384    def p_basetype(self, p):
385        """basetype : typename"""
386        p[0] = p[1]
387
388    # References
389    # ==========
390
391    def p_varref(self, p):
392        """varref : cmpnd"""
393        p[0] = p[1]
394
395    def p_cmpnd_iter(self, p):
396        """cmpnd : cmpnd PERIOD cmpnd %prec DOT"""
397        p[0] = self.ast.VarRef(extension=p[3], name = p[1].name, index = p[1].index)
398
399    def p_cmpnd_end(self, p):
400        """cmpnd : pfld"""
401        p[0] = self.ast.VarRef(**p[1])
402
403    # pfld = prefix field
404    def p_pfld_indexed(self, p):
405        """pfld : NAME LBRACKET expr RBRACKET"""
406        p[0] = {'name': p[1], 'index': p[3]}
407
408    def p_pfld(self, p):
409        """pfld : NAME"""
410        p[0] = {'name': p[1]}
411
412    # Attributes
413    # ==========
414
415    def p_opt_priority(self, p):
416        """opt_priority : PRIORITY number"""
417        p[0] = p[2]
418
419    def p_opt_priority_empty(self, p):
420        """opt_priority : empty"""
421
422    def p_opt_enabler(self, p):
423        """opt_enabler : PROVIDED LPAREN expr RPAREN"""
424        p[0] = p[3]
425
426    def p_opt_enabler_empty(self, p):
427        """opt_enabler : empty"""
428
429    def p_body(self, p):
430        """body : LBRACE sequence os RBRACE"""
431        p[0] = p[2]
432
433    # Sequence
434    # ========
435
436    def p_sequence(self, p):
437        """sequence : sequence msemi step"""
438        p[1].append(p[3])
439        p[0] = p[1]
440
441    def p_sequence_ending_with_atomic(self, p):
442        """sequence : seq_block step"""
443        p[1].append(p[2])
444        p[0] = p[1]
445
446    def p_sequence_single(self, p):
447        """sequence : step"""
448        p[0] = self.ast.Sequence([p[1]])
449
450    def p_seq_block(self, p):
451        """seq_block : sequence msemi atomic
452                     | sequence msemi dstep
453        """
454        p[1].append(p[3])
455        p[0] = p[1]
456
457    def p_seq_block_iter(self, p):
458        """seq_block : seq_block atomic
459                     | seq_block dstep
460        """
461        p[1].append(p[2])
462        p[0] = p[1]
463
464    def p_seq_block_single(self, p):
465        """seq_block : atomic
466                     | dstep
467        """
468        p[0] = [p[1]]
469
470    # TODO: XU vref_lst
471    def p_step_1(self, p):
472        """step : one_decl
473                | stmnt
474        """
475        p[0] = p[1]
476
477    def p_step_labeled(self, p):
478        """step : NAME COLON one_decl"""
479        raise Exception(
480            'label preceding declaration: {s}'.format(s=p[3]))
481
482    def p_step_3(self, p):
483        """step : NAME COLON XR
484                | NAME COLON XS
485        """
486        raise Exception(
487            'label preceding xr/xs claim')
488
489    def p_step_4(self, p):
490        """step : stmnt UNLESS stmnt"""
491        p[0] = (p[1], 'unless', p[3])
492        self.logger.warning('UNLESS not interpreted yet')
493
494    # Statement
495    # =========
496
497    def p_stmnt(self, p):
498        """stmnt : special
499                 | statement
500        """
501        p[0] = p[1]
502
503    # Stmnt in spin.y
504    def p_statement_asgn(self, p):
505        """statement : varref asgn full_expr"""
506        p[0] = self.ast.Assignment(var=p[1], value=p[3])
507
508    def p_statement_incr(self, p):
509        """statement : varref INCR"""
510        one = self.ast.Integer('1')
511        expr = self.ast.Expression(self.ast.Binary('+', p[1], one))
512        p[0] = self.ast.Assignment(p[1], expr)
513
514    def p_statement_decr(self, p):
515        """statement : varref DECR"""
516        one = self.ast.Integer('1')
517        expr = self.ast.Expression(self.ast.Binary('-', p[1], one))
518        p[0] = self.ast.Assignment(p[1], expr)
519
520    def p_statement_assert(self, p):
521        """statement : ASSERT full_expr"""
522        p[0] = self.ast.Assert(p[2], pos = p.lineno(1))
523
524    def p_statement_fifo_receive(self, p):
525        """statement : varref RCV rargs"""
526        p[0] = self.ast.Receive(p[1], p[3])
527
528    def p_statement_copy_fifo_receive(self, p):
529        """statement : varref RCV LT rargs GT"""
530        p[0] = self.ast.Receive(p[1], p[4])
531
532    def p_statement_random_receive(self, p):
533        """statement : varref R_RCV rargs"""
534        p[0] = self.ast.Receive(p[1], p[3])
535
536    def p_statement_copy_random_receive(self, p):
537        """statement : varref R_RCV LT rargs GT"""
538        p[0] = self.ast.Receive(p[1], p[4])
539
540    def p_statement_tx2(self, p):
541        """statement : varref TX2 rargs"""
542        p[0] = self.ast.Send(p[1], p[3])
543
544    def p_statement_full_expr(self, p):
545        """statement : full_expr"""
546        p[0] = p[1]
547
548    def p_statement_else(self, p):
549        """statement : ELSE"""
550        p[0] = self.ast.Else()
551
552    def p_statement_for(self, p):
553        """statement : for"""
554        p[0] = p[1]
555
556    def p_for(self, p):
557        """for : FOR LPAREN NAME COLON full_expr PERIODS full_expr RPAREN LBRACE sequence os RBRACE"""
558        s = p[10]
559        s.context = 'for'
560        s.context_for_var = p[3]
561        s.context_for_begin = p[5]
562        s.context_for_end = p[7]
563        p[0] = s
564
565    def p_statement_atomic(self, p):
566        """statement : atomic"""
567        p[0] = p[1]
568
569    def p_atomic(self, p):
570        """atomic : ATOMIC LBRACE sequence os RBRACE"""
571        s = p[3]
572        s.context = 'atomic'
573        p[0] = s
574
575    def p_statement_dstep(self, p):
576        """statement : dstep"""
577        p[0] = p[1]
578
579    def p_dstep(self, p):
580        """dstep : D_STEP LBRACE sequence os RBRACE"""
581        s = p[3]
582        s.context = 'd_step'
583        p[0] = s
584
585    def p_statement_braces(self, p):
586        """statement : LBRACE sequence os RBRACE"""
587        p[0] = p[2]
588
589    # the stmt of line 696 in spin.y collects the inline ?
590    def p_statement_call(self, p):
591        """statement : NAME LPAREN decl0 RPAREN"""
592        # NAME = INAME = inline
593        c = self.ast.Call(p[1], p[3])
594        p[0] = self.ast.Sequence([c])
595
596    def p_statement_assgn_call(self, p):
597        """statement : varref asgn NAME LPAREN decl0 RPAREN statement"""
598        inline = self.ast.Call(p[3], p[5])
599        p[0] = self.ast.Assignment(p[1], inline)
600
601    def p_statement_return(self, p):
602        """statement : RETURN full_expr"""
603        p[0] = self.ast.Return(p[2])
604
605    def p_printf1(self, p):
606        """statement : PRINT LPAREN STRING RPAREN"""
607        p[0] = self.ast.Printf(p[3])
608
609    def p_printf2(self, p):
610        """statement : PRINT LPAREN STRING COMMA decl0 RPAREN"""
611        p[0] = self.ast.Printf(p[3], p[5])
612
613    # yet unimplemented for statement:
614        # SET_P l_par two_args r_par
615        # PRINTM l_par varref r_par
616        # PRINTM l_par CONST r_par
617        # ccode
618
619    # Special
620    # =======
621
622    def p_special(self, p):
623        """special : varref RCV"""
624        p[0] = self.ast.Receive(p[1])
625
626    def p_varref_lnot(self, p):
627        """special : varref LNOT rargs"""
628        p[0] = self.ast.Send(p[1], p[3])
629
630    def p_break(self, p):
631        """special : BREAK"""
632        p[0] = self.ast.Break()
633
634    def p_goto(self, p):
635        """special : GOTO NAME"""
636        p[0] = self.ast.Goto(p[2])
637
638    def p_labeled_stmt(self, p):
639        """special : NAME COLON stmnt"""
640        p[0] = self.ast.Label(p[1], p[3])
641
642    def p_labeled(self, p):
643        """special : NAME COLON"""
644        p[0] = self.ast.Label(
645            p[1],
646            self.ast.Expression(self.ast.Bool('true')))
647
648    def p_special_if(self, p):
649        """special : IF options FI"""
650        p[0] = self.ast.Options('if', p[2])
651
652    def p_special_do(self, p):
653        """special : DO options OD"""
654        p[0] = self.ast.Options('do', p[2])
655
656    def p_options_end(self, p):
657        """options : option"""
658        p[0] = [p[1]]
659
660    def p_options_iter(self, p):
661        """options : options option"""
662        p[1].append(p[2])
663        p[0] = p[1]
664
665    def p_option(self, p):
666        """option : COLONS sequence os"""
667        s = p[2]
668        s.is_option = True
669        p[0] = s
670
671    # Expressions
672    # ===========
673
674    def p_full_expr(self, p):
675        """full_expr : expr
676                     | pexpr
677        """
678        p[0] = self.ast.Expression(p[1])
679
680    # probe expr = no negation allowed (positive)
681    def p_pexpr_probe(self, p):
682        """pexpr : probe"""
683        p[0] = p[1]
684
685    def p_pexpr_paren(self, p):
686        """pexpr : LPAREN pexpr RPAREN"""
687        p[0] = p[2]
688
689    def p_pexpr_logical(self, p):
690        """pexpr : pexpr LAND pexpr
691                 | pexpr LAND expr
692                 | expr LAND pexpr
693                 | pexpr LOR pexpr
694                 | pexpr LOR expr
695                 | expr LOR pexpr
696        """
697        p[0] = self.ast.Binary(p[2], p[1], p[3])
698
699    def p_probe(self, p):
700        """probe : FULL LPAREN varref RPAREN
701                 | NFULL LPAREN varref RPAREN
702                 | EMPTY LPAREN varref RPAREN
703                 | NEMPTY LPAREN varref RPAREN
704        """
705        p[0] = self.ast.Call(p[1], self.ast.Sequence([p[3]]))
706
707    def p_expr_paren(self, p):
708        """expr : LPAREN expr RPAREN"""
709        p[0] = p[2]
710
711    def p_expr_arithmetic(self, p):
712        """expr : expr PLUS expr
713                | expr MINUS expr
714                | expr TIMES expr
715                | expr DIVIDE expr
716                | expr MOD expr
717        """
718        p[0] = self.ast.Binary(p[2], p[1], p[3])
719
720    def p_expr_not(self, p):
721        """expr : NOT expr
722                | MINUS expr %prec UMINUS
723                | LNOT expr %prec NEG
724        """
725        p[0] = self.ast.Unary(p[1], p[2])
726
727    def p_expr_logical(self, p):
728        """expr : expr AND expr
729                | expr OR expr
730                | expr XOR expr
731                | expr LAND expr
732                | expr LOR expr
733        """
734        p[0] = self.ast.Binary(p[2], p[1], p[3])
735
736    # TODO: cexpr
737
738    def p_expr_shift(self, p):
739        """expr : expr LSHIFT expr
740                | expr RSHIFT expr
741        """
742        p[0] = p[1]
743
744    def p_expr_const_varref(self, p):
745        """expr : const
746                | varref
747        """
748        p[0] = p[1]
749
750    def p_expr_varref(self, p):
751        """expr : varref RCV LBRACKET rargs RBRACKET
752                | varref R_RCV LBRACKET rargs RBRACKET
753        """
754        p[0] = self.ast.ReceiveExpr(p[1], p[4])
755
756    def p_expr_other(self, p):
757        """expr : LPAREN expr ARROW expr COLON expr RPAREN
758                | LEN LPAREN varref RPAREN
759                | ENABLED LPAREN expr RPAREN
760                | GET_P LPAREN expr RPAREN
761        """
762        p[0] = p[1]
763        warnings.warn('"{s}" not implemented'.format(s=p[1]))
764
765    def p_expr_run(self, p):
766        """expr : RUN aname LPAREN decl0 RPAREN opt_priority"""
767        p[0] = self.ast.Run(p[2], p[4], p[6])
768
769    def p_expr_other_1(self, p):
770        """expr : TIMEOUT"""
771        p[0] = self.ast.Timeout()
772
773    def p_expr_other_2(self, p):
774        """expr : NONPROGRESS
775                | PC_VAL LPAREN expr RPAREN
776        """
777        raise NotImplementedError()
778
779    def p_expr_remote_ref_proctype_pc(self, p):
780        """expr : NAME AT NAME
781        """
782        p[0] = self.ast.RemoteRef(p[1], p[3])
783
784    def p_expr_remote_ref_pid_pc(self, p):
785        """expr : NAME LBRACKET expr RBRACKET AT NAME"""
786        p[0] = self.ast.RemoteRef(p[1], p[6], pid=p[3])
787
788    def p_expr_remote_ref_var(self, p):
789        """expr : NAME LBRACKET expr RBRACKET COLON pfld"""
790        # | NAME COLON pfld %prec DOT2
791        raise NotImplementedError()
792
793    def p_expr_comparator(self, p):
794        """expr : expr EQ expr
795                | expr NE expr
796                | expr LT expr
797                | expr LE expr
798                | expr GT expr
799                | expr GE expr
800        """
801        p[0] = self.ast.Binary(p[2], p[1], p[3])
802
803    def p_binary_ltl_expr(self, p):
804        """expr : expr UNTIL expr
805                | expr WEAK_UNTIL expr
806                | expr RELEASE expr
807                | expr IMPLIES expr
808                | expr EQUIV expr
809        """
810        p[0] = self.ast.Binary(p[2], p[1], p[3])
811
812    def p_unary_ltl_expr(self, p):
813        """expr : NEXT expr
814                | ALWAYS expr
815                | EVENTUALLY expr
816        """
817        p[0] = self.ast.Unary(p[1], p[2])
818
819    # Constants
820    # =========
821
822    def p_const_expr_const(self, p):
823        """const_expr : const"""
824        p[0] = p[1]
825
826    def p_const_expr_unary(self, p):
827        """const_expr : MINUS const_expr %prec UMINUS"""
828        p[0] = self.ast.Unary(p[1], p[2])
829
830    def p_const_expr_binary(self, p):
831        """const_expr : const_expr PLUS const_expr
832                      | const_expr MINUS const_expr
833                      | const_expr TIMES const_expr
834                      | const_expr DIVIDE const_expr
835                      | const_expr MOD const_expr
836        """
837        p[0] = self.ast.Binary(p[2], p[1], p[3])
838
839    def p_const_expr_paren(self, p):
840        """const_expr : LPAREN const_expr RPAREN"""
841        p[0] = p[2]
842
843    def p_const(self, p):
844        """const : SKIP
845                 | boolean
846                 | number
847        """
848        p[0] = p[1]
849
850    def p_bool(self, p):
851        """boolean : TRUE
852                   | FALSE
853        """
854        p[0] = self.ast.Bool(p[1])
855
856    def p_number(self, p):
857        """number : INTEGER"""
858        p[0] = self.ast.Integer(p[1])
859
860    # Auxiliary
861    # =========
862
863    # TODO: CONST, MINUS CONST %prec UMIN
864    def p_rarg(self, p):
865        """rarg : const
866                | varref
867                | EVAL LPAREN expr RPAREN
868        """
869        # todo: support all cases
870        #       | rarg LPAREN rargs RPAREN
871        #       | LPAREN rargs RPAREN
872        p[0] = p[1]
873
874    def p_rargs_iter(self, p):
875        """rargs : rarg COMMA rargs"""
876        p[0] = [p[1]] + p[3]
877
878    def p_rargs_end(self, p):
879        """rargs : rarg"""
880        p[0] = [p[1]]
881
882    def p_proctype(self, p):
883        """proctype : PROCTYPE
884                    | D_PROCTYPE
885        """
886        if p[1] == 'proctype':
887            p[0] = dict(d_proc=False)
888        else:
889            p[0] = dict(d_proc=True)
890
891    # PNAME
892    def p_aname(self, p):
893        """aname : NAME"""
894        p[0] = p[1]
895
896    # optional name
897    def p_optname(self, p):
898        """optname : NAME"""
899        p[0] = p[1]
900
901    def p_optname_empty(self, p):
902        """optname : empty"""
903
904    # optional semi
905    def p_os(self, p):
906        """os : empty
907              | semi
908        """
909        p[0] = ';'
910
911    # multi-semi
912    def p_msemi(self, p):
913        """msemi : semi
914                 | msemi semi
915        """
916        p[0] = ';'
917
918    def p_semi(self, p):
919        """semi : SEMI
920                | ARROW
921        """
922        p[0] = ';'
923
924    def p_asgn(self, p):
925        """asgn : EQUALS
926                | empty
927        """
928        p[0] = None
929
930    def p_visible(self, p):
931        """vis : HIDDEN
932               | SHOW
933               | ISLOCAL
934        """
935        p[0] = {'visible': p[1]}
936
937    def p_empty(self, p):
938        """empty : """
939
940    def p_error(self, p):
941        raise Exception('syntax error at: {p}'.format(p=p))
942
943
944def cpp(code, fic):
945    """Call the C{C} preprocessor with input C{s}."""
946    try:
947        if _platform == "darwin":
948            cppprog = 'clang'
949        else:
950            cppprog = 'cpp'
951        p = subprocess.Popen([cppprog, '-E', '-x', 'c', '-' if code is not None else fic], # NOTE: if code is empty, then '-' must be returned as well
952                             stdin=subprocess.PIPE,
953                             stdout=subprocess.PIPE,
954                             stderr=subprocess.PIPE,
955                             universal_newlines=True)
956    except OSError as e:
957        if e.errno == os.errno.ENOENT:
958            raise Exception('C preprocessor (cpp) not found in path.')
959        else:
960            raise
961    if code:
962        logger.debug('cpp input:\n' + code)
963    stdout, stderr = p.communicate(code)
964    logger.debug('cpp returned: {c}'.format(c=p.returncode))
965    logger.debug('cpp stdout:\n {out}'.format(out=stdout))
966    if p.returncode != 0:
967        raise Exception('C preprocessor return code: {returncode}'.format(returncode=p.returncode))
968    return stdout
969
970
971def rebuild_table(parser, tabmodule):
972    # log details to file
973    h = logging.FileHandler('log.txt', mode='w')
974    debuglog = logging.getLogger()
975    debuglog.addHandler(h)
976    debuglog.setLevel('DEBUG')
977    import os
978    outputdir = './'
979    # rm table files to force rebuild to get debug output
980    tablepy = tabmodule + '.py'
981    tablepyc = tabmodule + '.pyc'
982    try:
983        os.remove(tablepy)
984    except:
985        print('no "{t}" found'.format(t=tablepy))
986    try:
987        os.remove(tablepyc)
988    except:
989        print('no "{t}" found'.format(t=tablepyc))
990    parser.build(tabmodule, outputdir=outputdir,
991                 write_tables=True, debug=True,
992                 debuglog=debuglog)
993
994
995if __name__ == '__main__':
996    rebuild_table(Parser(), TABMODULE.split('.')[-1])
997
998
999# TODO
1000#
1001# expr << expr
1002# expr >> expr
1003# (expr -> expr : expr)
1004# run func(args) priority
1005# len(varref)
1006# enabled(expr)
1007# get_p(expr)
1008# var ? [rargs]
1009# var ?? [rargs]
1010# timeout
1011# nonprogress
1012# pc_val(expr)
1013# name[expr] @ name
1014# name[expr] : pfld
1015# name @ name
1016# name : pfld
Note: See TracBrowser for help on using the repository browser.