source: rtems-central/formal/promela/src/src/modules/promela_yacc/promela/lex.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: 5.6 KB
Line 
1"""Lexer for Promela, using Python Lex-Yacc (PLY)."""
2import logging
3import ply.lex
4import re
5
6logger = logging.getLogger(__name__)
7
8
9class Lexer(object):
10    """Lexer for the Promela modeling language."""
11
12    states = tuple([('ltl', 'inclusive')])
13    reserved = {
14        '_np': 'NONPROGRESS',
15        'true': 'TRUE',
16        'false': 'FALSE',
17        'active': 'ACTIVE',
18        'assert': 'ASSERT',
19        'atomic': 'ATOMIC',
20        'bit': 'BIT',
21        'bool': 'BOOL',
22        'break': 'BREAK',
23        'byte': 'BYTE',
24        'chan': 'CHAN',
25        'd_step': 'D_STEP',
26        'd_proctype': 'D_PROCTYPE',
27        'do': 'DO',
28        'else': 'ELSE',
29        'empty': 'EMPTY',
30        'enabled': 'ENABLED',
31        'eval': 'EVAL',
32        'fi': 'FI',
33        'for': 'FOR',
34        'full': 'FULL',
35        'get_priority': 'GET_P',
36        'goto': 'GOTO',
37        'hidden': 'HIDDEN',
38        'if': 'IF',
39        'init': 'INIT',
40        'inline': 'INLINE',
41        'int': 'INT',
42        'len': 'LEN',
43        'local': 'ISLOCAL',
44        'ltl': 'LTL',
45        'mtype': 'MTYPE',
46        'nempty': 'NEMPTY',
47        'never': 'CLAIM',
48        'nfull': 'NFULL',
49        'od': 'OD',
50        'of': 'OF',
51        'pc_value': 'PC_VAL',
52        'pid': 'PID',
53        'printf': 'PRINT',
54        'priority': 'PRIORITY',
55        'proctype': 'PROCTYPE',
56        'provided': 'PROVIDED',
57        'R': 'RELEASE',
58        'return': 'RETURN',
59        'run': 'RUN',
60        'short': 'SHORT',
61        'skip': 'SKIP',
62        'show': 'SHOW',
63        'timeout': 'TIMEOUT',
64        'typedef': 'TYPEDEF',
65        'U': 'UNTIL',
66        'unless': 'UNLESS',
67        'unsigned': 'UNSIGNED',
68        'X': 'NEXT',
69        'xr': 'XR',
70        'xs': 'XS',
71        'W': 'WEAK_UNTIL'}
72    values = {'': ''}
73    delimiters = ['LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET',
74                  'LBRACE', 'RBRACE', 'COMMA', 'PERIODS', 'PERIOD',
75                  'SEMI', 'COLONS', 'COLON', 'ELLIPSIS']
76    # remember to check precedence
77    operators = ['PLUS', 'INCR', 'MINUS', 'DECR', 'TIMES', 'DIVIDE',
78                 'MOD', 'OR', 'AND', 'NOT', 'XOR', 'IMPLIES', 'EQUIV',
79                 'LOR', 'LAND', 'LNOT', 'LT', 'GT',
80                 'LE', 'GE', 'EQ', 'NE',
81                 'RCV', 'R_RCV', 'TX2', 'LSHIFT', 'RSHIFT', 'AT',
82                 'ALWAYS', 'EVENTUALLY']
83    misc = ['EQUALS', 'ARROW', 'STRING', 'NAME', 'INTEGER',
84            'PREPROC', 'NEWLINE', 'COMMENT']
85
86    def __init__(self, debug=False):
87        self.tokens = (
88            self.delimiters + self.operators +
89            self.misc + list(set(self.reserved.values())))
90        self.build(debug=debug)
91
92    def build(self, debug=False, debuglog=None, **kwargs):
93        """Create a lexer.
94
95        @param kwargs: Same arguments as C{ply.lex.lex}:
96
97          - except for C{module} (fixed to C{self})
98          - C{debuglog} defaults to the module's logger.
99        """
100        if debug and debuglog is None:
101            debuglog = logger
102        self.lexer = ply.lex.lex(
103            module=self,
104            debug=debug,
105            debuglog=debuglog,
106            **kwargs)
107
108    # check for reserved words
109    def t_NAME(self, t):
110        r'[a-zA-Z_][a-zA-Z_0-9]*'
111        t.value = self.values.get(t.value, t.value)
112        t.type = self.reserved.get(t.value, 'NAME')
113        # switch to LTL context
114        if t.value == 'ltl':
115            self.lexer.level = 0
116            self.lexer.begin('ltl')
117        return t
118
119    def t_STRING(self, t):
120        r'"[^"]*"'
121        return t
122
123    # operators
124    t_PLUS = r'\+'
125    t_INCR = r'\+\+'
126    t_MINUS = r'-'
127    t_DECR = r'--'
128    t_TIMES = r'\*'
129    t_DIVIDE = r'/'
130    t_MOD = r'%'
131    t_OR = r'\|'
132    t_AND = r'&'
133    t_NOT = r'~'
134    t_XOR = r'\^'
135    t_LOR = r'\|\|'
136    t_LAND = r'&&'
137    t_LNOT = r'!'
138    t_TX2 = r'!!'
139    t_LT = r'<'
140    t_LSHIFT = r'<<'
141    t_GT = r'>'
142    t_RSHIFT = r'>>'
143    t_LE = r'<='
144    t_GE = r'>='
145    t_EQ = r'=='
146    t_NE = r'!='
147    t_RCV = r'\?'
148    t_R_RCV = r'\?\?'
149    t_AT = r'@'
150    t_EQUIV = r'<->'
151    # assignment
152    t_EQUALS = r'='
153    # temporal operators
154    t_ALWAYS = r'\[\]'
155    t_EVENTUALLY = r'\<\>'
156    # delimeters
157    t_LPAREN = r'\('
158    t_RPAREN = r'\)'
159    t_LBRACKET = r'\['
160    t_RBRACKET = r'\]'
161    t_LBRACE = r'\{'
162    t_RBRACE = r'\}'
163    t_COMMA = r','
164    t_PERIODS = r'\.\.'
165    t_PERIOD = r'\.'
166    t_SEMI = r';'
167    t_COLONS = r'::'
168    t_COLON = r':'
169    t_ELLIPSIS = r'\.\.\.'
170
171    def t_ltl_LBRACE(self, t):
172        r'\{'
173        self.lexer.level += 1
174        return t
175
176    def t_ltl_RBRACE(self, t):
177        r'\}'
178        self.lexer.level -= 1
179        if self.lexer.level == 0:
180            self.lexer.begin('INITIAL')
181        return t
182
183    def t_ltl_ARROW(self, t):
184        r'->'
185        t.type = 'IMPLIES'
186        return t
187
188    t_INITIAL_ARROW = r'->'
189
190    def t_PREPROC_stdin(self, t):
191        r'\# .+ "<stdin>"[0-9 ]*' # WARNING: using '\d+' instead of '.+' does not necessarily result in the same matching
192        t.lexer.lineno = int (re.search (r'\# (\d+) "<stdin>"', t.value).group (1)) - 1
193        pass
194
195    def t_PREPROC(self, t):
196        r'\#.*'
197        pass
198
199    def t_INTEGER(self, t):
200        r'\d+([uU]|[lL]|[uU][lL]|[lL][uU])?'
201        return t
202
203    # t_ignore is reserved by lex to provide
204    # much more efficient internal handling by lex
205    #
206    # A string containing ignored characters (spaces and tabs)
207    t_ignore = ' \t'
208
209    def t_NEWLINE(self, t):
210        r'\n+'
211        t.lexer.lineno += t.value.count('\n')
212
213    def t_COMMENT(self, t):
214        r' /\*(.|\n)*?\*/'
215        t.lexer.lineno += t.value.count('\n')
216
217    def t_error(self, t):
218        logger.error('Illegal character "{s}"'.format(s=t.value[0]))
219        t.lexer.skip(1)
Note: See TracBrowser for help on using the repository browser.