source: rtems-central/formal/promela/src/src/modules/promela_yacc/promela/lex.py @ 5d08ea3

Last change on this file since 5d08ea3 was 5d08ea3, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/13/23 at 15:37:36

forked from https://github.com/johnyf/promela,
commit 32d14184a50e920a92201058e4f601329be8c9c7

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