--- .../src/src/modules/promela_yacc/.gitignore | 20 - .../src/src/modules/promela_yacc/.travis.yml | 21 - .../src/src/modules/promela_yacc/LICENSE | 1 + .../src/src/modules/promela_yacc/MANIFEST.in | 4 - .../src/src/modules/promela_yacc/doc.md | 100 --- .../src/modules/promela_yacc/promela/ast.py | 120 ++- .../src/modules/promela_yacc/promela/lex.py | 18 +- .../src/modules/promela_yacc/promela/yacc.py | 207 +++-- .../modules/promela_yacc/tests/yacc_test.py | 759 ------------------ 9 files changed, 228 insertions(+), 1022 deletions(-) delete mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore delete mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml delete mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in delete mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md delete mode 100644 formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore b/formal/promela/src/src/modules/promela_yacc/.gitignore deleted file mode 100644 index f4cd3f85..00000000 --- a/formal/promela/src/src/modules/promela_yacc/.gitignore +++ /dev/null @@ -1,20 +0,0 @@ -build/* -dist/* -promela/_version.py -*parsetab.py -.coverage -.DS_Store -Icon? - -*.*~ -__pycache__ -*.pyc -*.swp -*.pdf -*.PDF -*.txt -*.log -*.egg-info -*.html -*.css - diff --git a/formal/promela/src/src/modules/promela_yacc/.travis.yml b/formal/promela/src/src/modules/promela_yacc/.travis.yml deleted file mode 100644 index 2fee40c9..00000000 --- a/formal/promela/src/src/modules/promela_yacc/.travis.yml +++ /dev/null @@ -1,21 +0,0 @@ -language: python - -python: - - 2.7 - - 3.4 - - 3.5 - - 3.6 - -install: - - sudo apt-get update -qq - - sudo apt-get install -y graphviz - - pip install --upgrade pip setuptools - - pip install -r requirements.txt - - pip install . - -script: - - cd tests/ - - nosetests --with-coverage --cover-package=promela - -after_success: - - coveralls diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE b/formal/promela/src/src/modules/promela_yacc/LICENSE index bebe3694..40f0a792 100644 --- a/formal/promela/src/src/modules/promela_yacc/LICENSE +++ b/formal/promela/src/src/modules/promela_yacc/LICENSE @@ -1,3 +1,4 @@ +Copyright (c) 2019-2021 by Trinity College Dublin, Ireland Copyright (c) 2014-2018 by California Institute of Technology Copyright (c) 2014-2018 by Ioannis Filippidis All rights reserved. diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in deleted file mode 100644 index bbacf5bf..00000000 --- a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in +++ /dev/null @@ -1,4 +0,0 @@ -include tests/*.py -include README.md -include LICENSE -include doc.md diff --git a/formal/promela/src/src/modules/promela_yacc/doc.md b/formal/promela/src/src/modules/promela_yacc/doc.md deleted file mode 100644 index 02d73431..00000000 --- a/formal/promela/src/src/modules/promela_yacc/doc.md +++ /dev/null @@ -1,100 +0,0 @@ -This package provides a lexer, parser, and abstract syntax tree (AST) for the [Promela](http://en.wikipedia.org/wiki/Promela) modeling language. -The lexer and parser are generated using [PLY](https://pypi.python.org/pypi/ply/3.4) (Python `lex`-`yacc`). -The [grammar](http://spinroot.com/spin/Man/grammar.html) is based on that used in the [SPIN](http://spinroot.com/spin/whatispin.html) model checker (in the files `spin.y` and `spinlex.c` of SPIN's source distribution), with modifications where needed. - -To instantiate a Promela parser: - -```python -from promela.yacc import Parser -parser = Parser() -``` - -Then Promela code, as a string, can be parsed by: - -```python -s = ''' -active proctype foo(){ - int x; - do - :: x = x + 1; - od -} -''' -program = parser.parse(s) -``` - -then - -```python ->>> print(program) -active [1] proctype foo(){ - int x - do - :: x = (x + 1) - od; -} -``` - -The parser returns the result as an abstract syntax tree using classes from the `promela.ast` module. -The top production rule returns a `Program` instance, which itself is a `list`. -The contents of this list - -There are two categories of AST classes: those that represent control flow constructs: - -- `Proctype`, (`Init`, `NeverClaim`), `Node`, (`Expression`, `Assignment`, `Assert`, `Options` (if, do), `Else`, `Break`, `Goto`, `Label`, `Call`, `Return`, `Run`), `Sequence` - -and those that represent only syntax inside an expression: - -- `Terminal`, (`VarRef`, `Integer`, `Bool`), `Operator`, (`Binary`, `Unary`) - -The classes in parentheses are subclasses of the last class preceding the parentheses. -Each control flow class has a method `to_pg` that recursively converts the abstract syntax tree to a program graph. - -A program graph is a directed graph whose edges are labeled with statements from the program. -Nodes represent states of the program. -Note the difference with a control flow graph, whose nodes are program statements and edges are program states. -AST node classes correspond to nodes of the control flow graph and edges of the program graph (possibly with branching). - -For some node classes like `Expression` and `Assignment`, the `to_pg` method returns themselves, a. -Almost all statements are represented as either an `Expression` or an `Assignment`. -These label edges in the program graph, using the edge attribute `"stmt"`. - -The program graph is represented as a [multi-digraph](http://en.wikipedia.org/wiki/Multigraph) using [`networkx.MultiDiGraph`](https://networkx.github.io/documentation/latest/reference/classes.multidigraph.html). -A multi-digraph is necessary, because two nodes in the program graph may be connected by two edges, each edge labeled with a different statement. -For example, this is the case in the code fragment: - -```promela -bit x; -do -:: x == 0 -:: x == 1 -od -``` - -The above defines a program graph with a single node and two self-loops, one labeled with the statement `x == 0` and another with the statement `x == 1`. -These two statements here are guards, so they only determine whether the edge can be traversed, without affecting the program's data state (variable values). - -Program graph nodes are labeled with a `"context"` attribute that can take the values: -- `"atomic"` -- `"d_step"` -- `None` -The values `"atomic"` and `"d_step"` signify that the state is inside an atomic or deterministic step block. - -Continuing our earlier example: - -```python ->>> g = program[0].to_pg() ->>> g.nodes(data=True) -[(0, {'context': None}), (1, {'context': None})] ->>> g.edges(data=True) -[(0, 1, {'stmt': Assignment( - VarRef('x', None, None), - Expression( - Operator('+', - VarRef('x', None, None), - Integer('1'))))}), - (1, 0, {'stmt': Expression( - Operator('==', - VarRef('x', None, None), - Integer('2')))})] -``` diff --git a/formal/promela/src/src/modules/promela_yacc/promela/ast.py b/formal/promela/src/src/modules/promela_yacc/promela/ast.py index 16baaa05..77db1fe9 100644 --- a/formal/promela/src/src/modules/promela_yacc/promela/ast.py +++ b/formal/promela/src/src/modules/promela_yacc/promela/ast.py @@ -48,19 +48,20 @@ def to_str(x): class Proctype(object): def __init__(self, name, body, args=None, active=None, d_proc=False, - priority=None, provided=None): + priority=None, provided=None, + disable_negation=False): self.name = name self.body = body self.args = args if active is None: active = 0 - else: - active = int(active.value) + self.d_proc = d_proc if priority is not None: priority = int(priority.value) self.active = active self.priority = priority self.provided = provided + self.disable_negation = disable_negation def __str__(self): return "Proctype('{name}')".format(name=self.name) @@ -86,7 +87,7 @@ class Proctype(object): if self.args is None: args = '' else: - args = to_str(self.args) + args = '; '.join(to_str(xx) for x in self.args for xx in x) return args def to_pg(self, syntactic_else=False): @@ -223,7 +224,7 @@ class Init(Proctype): class Program(list): def __str__(self): - return '\n'.join(to_str(x) for x in self) + return '\n'.join(to_str(x) for x, _ in self) def __repr__(self): c = super(Program, self).__repr__() @@ -245,21 +246,25 @@ class Program(list): class LTL(object): """Used to mark strings as LTL blocks.""" - def __init__(self, formula): + def __init__(self, formula, name = None): self.formula = formula + self.name = name def __repr__(self): return 'LTL({f})'.format(f=repr(self.formula)) def __str__(self): - return 'ltl {' + str(self.formula) + '}' + return 'ltl ' + (self.name + ' ' if self.name else '') + '{' + str(self.formula) + '}' class Sequence(list): - def __init__(self, iterable, context=None, is_option=False): + def __init__(self, iterable, context=None, context_for_var=None, context_for_begin=None, context_for_end=None, is_option=False): super(Sequence, self).__init__(iterable) - # "atomic" or "dstep" + # "for" or "atomic" or "dstep" self.context = context + self.context_for_var = context_for_var + self.context_for_begin = context_for_begin + self.context_for_end = context_for_end self.is_option = is_option def to_str(self): @@ -267,20 +272,22 @@ class Sequence(list): return '\n'.join(to_str(x) for x in self) else: return ( - self.context + '{\n' + - _indent(to_str(self)) + '\n}\n') + self.context + + (' (' + self.context_for_var + ' : ' + to_str (self.context_for_begin) + ' .. ' + to_str (self.context_for_end) + ') ' if self.context == 'for' else '') + + '{\n' + + '\n'.join(_indent(to_str(x)) for x in self) + '\n}\n') def __repr__(self): l = super(Sequence, self).__repr__() - return 'Sequence({l}, context={c}, is_option={isopt})'.format( - l=l, c=self.context, isopt=self.is_option) + return 'Sequence({l}, context={c}, context_for_var={cfv}, context_for_begin={cfb}, context_for_end={cfe}, is_option={isopt})'.format( + l=l, c=self.context, cfv=self.context_for_var, cfb=self.context_for_begin, cfe=self.context_for_end, isopt=self.is_option) def to_pg(self, g, context=None, option_guard=None, **kw): # set context if context is None: context = self.context c = context - assert c in {'atomic', 'd_step', None} + assert c in {'atomic', 'd_step', None} # TODO: 'for' # atomic cannot appear inside d_step if context == 'd_step' and c == 'atomic': raise Exception('atomic inside d_step') @@ -541,12 +548,13 @@ class VarDef(Node): assert isinstance(l, int), l self.length = l self.visible = visible - if bitwidth is not None: - self.bitwidth = int(bitwidth.value) + self.bitwidth = int(bitwidth.value) if bitwidth else None if vartype == 'bool': default_initval = Bool('false') else: default_initval = Integer('0') + self.msg_types = msg_types + self.initial_value0 = initval if initval is None: initval = Expression(default_initval) self.initial_value = initval @@ -556,10 +564,13 @@ class VarDef(Node): return 'VarDef({t}, {v})'.format(t=self.type, v=self.name) def to_str(self): - s = '{type} {varname}{len}'.format( + s = '{type} {varname}{bitwidth}{len}{initval}{msg_types}'.format( type=self._type_str(), varname=self.name, - len='[{n}]'.format(n=self.len) if self.len else '') + bitwidth=' : {n}'.format(n =self.bitwidth) if self.bitwidth else '', + len=' [{n}]'.format(n=self.length) if self.length and not self.msg_types else '', + initval=' = {i}'.format(i=self.initial_value0) if self.initial_value0 else '', + msg_types=' = [{l}] of {{ {m} }}'.format(l=self.length, m=' , '.join(to_str(x) for x in self.msg_types)) if self.msg_types else '') return s def _type_str(self): @@ -741,8 +752,8 @@ class TypeDef(Node): self.decls = decls def __str__(self): - return 'typedef {name} {\ndecls\n}'.format( - name=self.name, decls=to_str(self.decls)) + return 'typedef {name} {{ {decls} }}'.format( + name=self.name, decls='; '.join(to_str(x) for x in self.decls)) def exe(self, t): t.types[self.name] = self @@ -752,8 +763,8 @@ class MessageType(Node): def __init__(self, values, visible=None): self.values = values - def __str__(self): - return 'mtype {{ {values} }}'.format(values=self.values) + def to_str(self): + return 'mtype = {{ {values} }}'.format(values=' , '.join(to_str(x) for x in self.values)) def exe(self, t): t.types[self.name] = self @@ -774,27 +785,40 @@ class Run(Node): self.priority = priority def __str__(self): - return 'run({f})'.format(f=self.func) + return 'run {f} ({args})'.format(f=self.func, args='' if self.args is None else ' , '.join(to_str(x) for x in self.args)) -class Inline(Node): - def __init__(self, name, args): +class InlineDef(Node): + def __init__(self, name, decl, body, disable_negation=False): self.name = name - self.args = args + self.decl = decl + self.body = body + self.disable_negation = disable_negation + def __str__(self): + return ('inline {name} ({decl}) {{\n' + '{body}\n' + '}}\n\n').format( + name = self.name, + decl = ', '.join(to_str(x) for x in self.decl) if self.decl else '', + body = _indent(to_str(self.body))) class Call(Node): - def __init__(self, func, args): - self.func = func + def __init__(self, name, args): + self.name = name self.args = args + def __str__(self): + return '{name} ({args})'.format(name = self.name, args = ', '.join(to_str(x) for x in self.args) if self.args else '') + class Assert(Node): - def __init__(self, expr): + def __init__(self, expr, pos = None): self.expr = expr + self.pos = pos - def __repr__(self): - return 'assert({expr})'.format(expr=repr(self.expr)) + def __str__(self): + return 'assert({expr})'.format(expr=to_str(self.expr)) class Expression(Node): @@ -872,32 +896,32 @@ class Assignment(Node): class Receive(Node): - def __init__(self, varref, args=None): + def __init__(self, varref, args): self.var = varref self.args = args def __str__(self): v = to_str(self.var) - return 'Rx({v})'.format(v=v) + return '{v} ? {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args)) class Send(Node): - def __init__(self, varref, args=None): - self.varref = varref + def __init__(self, varref, args): + self.var = varref self.args = args def __str__(self): v = to_str(self.var) - return 'Tx({v})'.format(v=v) + return '{v} ! {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args)) class Printf(Node): - def __init__(self, s, args): + def __init__(self, s, args=None): self.s = s self.args = args def __str__(self): - return 'printf()'.format(s=self.s, args=self.args) + return 'printf({s}{args})'.format(s=self.s, args='' if self.args is None else ' , ' + ' , '.join(to_str(x) for x in self.args)) class Operator(object): @@ -927,6 +951,14 @@ class Binary(Operator): class Unary(Operator): pass +class ReceiveExpr(Node): + def __init__(self, varref, args): + self.var = varref + self.args = args + + def __str__(self): + v = to_str(self.var) + return '({v} ? [{args}])'.format(v=v, args = ' , '.join(to_str(x) for x in self.args)) class Terminal(object): def __init__(self, value): @@ -967,7 +999,7 @@ class VarRef(Terminal): return '{name}{index}{ext}'.format( name=self.name, index=i, - ext='' if self.extension is None else self.extension) + ext=('.' + to_str(self.extension)) if self.extension else '' ) class Integer(Terminal): @@ -986,7 +1018,7 @@ class Bool(Terminal): return 'Bool({value})'.format(value=repr(self.value)) def __str__(self): - return str(self.value) + return str('true' if self.value else 'false') class RemoteRef(Terminal): @@ -1008,6 +1040,14 @@ class RemoteRef(Terminal): proc=self.proctype, inst=inst, label=self.label) +class Timeout(Node): + def __init__(self): + return + + def __str__(self): + return 'timeout' + + def dump_graph(g, fname='a.pdf', node_label='label', edge_label='label', relabel=False): """Write the program graph, annotated with formulae, to PDF file.""" diff --git a/formal/promela/src/src/modules/promela_yacc/promela/lex.py b/formal/promela/src/src/modules/promela_yacc/promela/lex.py index cd3eafe0..e31a51c0 100644 --- a/formal/promela/src/src/modules/promela_yacc/promela/lex.py +++ b/formal/promela/src/src/modules/promela_yacc/promela/lex.py @@ -1,7 +1,7 @@ """Lexer for Promela, using Python Lex-Yacc (PLY).""" import logging import ply.lex - +import re logger = logging.getLogger(__name__) @@ -30,12 +30,14 @@ class Lexer(object): 'enabled': 'ENABLED', 'eval': 'EVAL', 'fi': 'FI', + 'for': 'FOR', 'full': 'FULL', 'get_priority': 'GET_P', 'goto': 'GOTO', 'hidden': 'HIDDEN', 'if': 'IF', 'init': 'INIT', + 'inline': 'INLINE', 'int': 'INT', 'len': 'LEN', 'local': 'ISLOCAL', @@ -56,7 +58,7 @@ class Lexer(object): 'return': 'RETURN', 'run': 'RUN', 'short': 'SHORT', - 'skip': 'TRUE', + 'skip': 'SKIP', 'show': 'SHOW', 'timeout': 'TIMEOUT', 'typedef': 'TYPEDEF', @@ -67,9 +69,9 @@ class Lexer(object): 'xr': 'XR', 'xs': 'XS', 'W': 'WEAK_UNTIL'} - values = {'skip': 'true'} + values = {'': ''} delimiters = ['LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET', - 'LBRACE', 'RBRACE', 'COMMA', 'PERIOD', + 'LBRACE', 'RBRACE', 'COMMA', 'PERIODS', 'PERIOD', 'SEMI', 'COLONS', 'COLON', 'ELLIPSIS'] # remember to check precedence operators = ['PLUS', 'INCR', 'MINUS', 'DECR', 'TIMES', 'DIVIDE', @@ -159,6 +161,7 @@ class Lexer(object): t_LBRACE = r'\{' t_RBRACE = r'\}' t_COMMA = r',' + t_PERIODS = r'\.\.' t_PERIOD = r'\.' t_SEMI = r';' t_COLONS = r'::' @@ -184,6 +187,11 @@ class Lexer(object): t_INITIAL_ARROW = r'->' + def t_PREPROC_stdin(self, t): + r'\# .+ "<stdin>"[0-9 ]*' # WARNING: using '\d+' instead of '.+' does not necessarily result in the same matching + t.lexer.lineno = int (re.search (r'\# (\d+) "<stdin>"', t.value).group (1)) - 1 + pass + def t_PREPROC(self, t): r'\#.*' pass @@ -204,7 +212,7 @@ class Lexer(object): def t_COMMENT(self, t): r' /\*(.|\n)*?\*/' - t.lineno += t.value.count('\n') + t.lexer.lineno += t.value.count('\n') def t_error(self, t): logger.error('Illegal character "{s}"'.format(s=t.value[0])) diff --git a/formal/promela/src/src/modules/promela_yacc/promela/yacc.py b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py index d650c063..af96dc99 100644 --- a/formal/promela/src/src/modules/promela_yacc/promela/yacc.py +++ b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py @@ -15,6 +15,7 @@ import os import subprocess import warnings import ply.yacc +from sys import platform as _platform # inline # # import promela.ast as promela_ast @@ -90,11 +91,11 @@ class Parser(object): debuglog=debuglog, errorlog=errorlog) - def parse(self, promela): + def parse(self, promela, fic): """Parse string of Promela code.""" - s = cpp(promela) + s = cpp(promela, fic) program = self.parser.parse( - s, lexer=self.lexer.lexer, debug=self.logger) + s, lexer=self.lexer.lexer, debug=self.logger, tracking=True) return program def _iter(self, p): @@ -115,6 +116,10 @@ class Parser(object): """program : units""" p[0] = self.ast.Program(p[1]) + def p_program_empty(self, p): + """program : empty""" + p[0] = self.ast.Program([]) + def p_units_iter(self, p): """units : units unit""" p[0] = self._iter(p) @@ -126,17 +131,18 @@ class Parser(object): # TODO: events, c_fcts, ns, error def p_unit_proc(self, p): """unit : proc + | inline | init | claim | ltl """ - p[0] = p[1] + p[0] = (p[1], p.lineno(1)) def p_unit_decl(self, p): """unit : one_decl | utype """ - p[0] = p[1] + p[0] = (p[1], p.lineno(1)) def p_unit_semi(self, p): """unit : semi""" @@ -158,6 +164,13 @@ class Parser(object): name, body, args=args, priority=priority, provided=enabler, **inst) + def p_inline(self, p): + ("""inline : INLINE NAME""" + """ LPAREN var_list0 RPAREN""" + """ body + """) + p[0] = self.ast.InlineDef(name = p[2], decl = p[4], body = p[6]) + # instantiator def p_inst(self, p): """prefix_proctype : ACTIVE opt_index proctype""" @@ -166,7 +179,7 @@ class Parser(object): n_active = self.ast.Integer('1') else: n_active = p[2] - d['active'] = n_active + d['active'] = int(n_active.value) p[0] = d def p_inactive_proctype(self, p): @@ -197,7 +210,11 @@ class Parser(object): seq = self.ast.Sequence(p[4]) p[0] = self.ast.TypeDef(p[2], seq) - def p_ltl(self, p): + def p_ltl1(self, p): + """ltl : LTL NAME LBRACE expr RBRACE""" + p[0] = self.ast.LTL(p[4], name = p[2]) + + def p_ltl2(self, p): """ltl : LTL LBRACE expr RBRACE""" p[0] = self.ast.LTL(p[3]) @@ -219,6 +236,21 @@ class Parser(object): """decl_lst : one_decl""" p[0] = [p[1]] + def p_decl0(self, p): + """decl0 : decl_lst0""" + p[0] = self.ast.Sequence(p[1]) + + def p_decl_empty0(self, p): + """decl0 : empty""" + + def p_decl_lst_iter0(self, p): + """decl_lst0 : expr COMMA decl_lst0""" + p[0] = [p[1]] + p[3] + + def p_decl_lst_end0(self, p): + """decl_lst0 : expr""" + p[0] = [p[1]] + def p_one_decl_visible(self, p): """one_decl : vis typename var_list | vis NAME var_list @@ -251,7 +283,7 @@ class Parser(object): def p_one_decl_mtype(self, p): """one_decl : MTYPE asgn LBRACE name_list RBRACE""" - p[0] = self.ast.MessageType(p[3]) + p[0] = self.ast.MessageType(p[4]) def p_name_list_iter(self, p): """name_list : name_list COMMA NAME""" @@ -270,8 +302,28 @@ class Parser(object): """var_list : ivar""" p[0] = [p[1]] + def p_var_list00_iter(self, p): + """var_list00 : ivar0 COMMA var_list00""" + p[0] = [p[1]] + p[3] + + def p_var_list00_end(self, p): + """var_list00 : ivar0""" + p[0] = [p[1]] + + def p_var_list0(self, p): + """var_list0 : var_list00""" + p[0] = p[1] + + def p_var_list0_empty(self, p): + """var_list0 : empty""" + p[0] = [] + # TODO: vardcl asgn LBRACE c_list RBRACE + def p_ivar0(self, p): + """ivar0 : NAME""" + p[0] = p[1] + # ivar = initialized variable def p_ivar(self, p): """ivar : vardcl""" @@ -342,7 +394,7 @@ class Parser(object): def p_cmpnd_iter(self, p): """cmpnd : cmpnd PERIOD cmpnd %prec DOT""" - p[0] = self.ast.VarRef(extension=p[3], **p[1]) + p[0] = self.ast.VarRef(extension=p[3], name = p[1].name, index = p[1].index) def p_cmpnd_end(self, p): """cmpnd : pfld""" @@ -467,7 +519,7 @@ class Parser(object): def p_statement_assert(self, p): """statement : ASSERT full_expr""" - p[0] = self.ast.Assert(p[2]) + p[0] = self.ast.Assert(p[2], pos = p.lineno(1)) def p_statement_fifo_receive(self, p): """statement : varref RCV rargs""" @@ -486,7 +538,7 @@ class Parser(object): p[0] = self.ast.Receive(p[1], p[4]) def p_statement_tx2(self, p): - """statement : varref TX2 margs""" + """statement : varref TX2 rargs""" p[0] = self.ast.Send(p[1], p[3]) def p_statement_full_expr(self, p): @@ -497,6 +549,19 @@ class Parser(object): """statement : ELSE""" p[0] = self.ast.Else() + def p_statement_for(self, p): + """statement : for""" + p[0] = p[1] + + def p_for(self, p): + """for : FOR LPAREN NAME COLON full_expr PERIODS full_expr RPAREN LBRACE sequence os RBRACE""" + s = p[10] + s.context = 'for' + s.context_for_var = p[3] + s.context_for_begin = p[5] + s.context_for_end = p[7] + p[0] = s + def p_statement_atomic(self, p): """statement : atomic""" p[0] = p[1] @@ -523,23 +588,27 @@ class Parser(object): # the stmt of line 696 in spin.y collects the inline ? def p_statement_call(self, p): - """statement : NAME LPAREN args RPAREN""" + """statement : NAME LPAREN decl0 RPAREN""" # NAME = INAME = inline - c = self.ast.Inline(p[1], p[3]) + c = self.ast.Call(p[1], p[3]) p[0] = self.ast.Sequence([c]) def p_statement_assgn_call(self, p): - """statement : varref asgn NAME LPAREN args RPAREN statement""" - inline = self.ast.Inline(p[3], p[5]) + """statement : varref asgn NAME LPAREN decl0 RPAREN statement""" + inline = self.ast.Call(p[3], p[5]) p[0] = self.ast.Assignment(p[1], inline) def p_statement_return(self, p): """statement : RETURN full_expr""" p[0] = self.ast.Return(p[2]) - def p_printf(self, p): - """statement : PRINT LPAREN STRING prargs RPAREN""" - p[0] = self.ast.Printf(p[3], p[4]) + def p_printf1(self, p): + """statement : PRINT LPAREN STRING RPAREN""" + p[0] = self.ast.Printf(p[3]) + + def p_printf2(self, p): + """statement : PRINT LPAREN STRING COMMA decl0 RPAREN""" + p[0] = self.ast.Printf(p[3], p[5]) # yet unimplemented for statement: # SET_P l_par two_args r_par @@ -555,8 +624,8 @@ class Parser(object): p[0] = self.ast.Receive(p[1]) def p_varref_lnot(self, p): - """special : varref LNOT margs""" - raise NotImplementedError + """special : varref LNOT rargs""" + p[0] = self.ast.Send(p[1], p[3]) def p_break(self, p): """special : BREAK""" @@ -609,17 +678,23 @@ class Parser(object): p[0] = self.ast.Expression(p[1]) # probe expr = no negation allowed (positive) - def p_pexpr(self, p): - """pexpr : probe - | LPAREN pexpr RPAREN - | pexpr LAND pexpr + def p_pexpr_probe(self, p): + """pexpr : probe""" + p[0] = p[1] + + def p_pexpr_paren(self, p): + """pexpr : LPAREN pexpr RPAREN""" + p[0] = p[2] + + def p_pexpr_logical(self, p): + """pexpr : pexpr LAND pexpr | pexpr LAND expr | expr LAND pexpr | pexpr LOR pexpr | pexpr LOR expr | expr LOR pexpr """ - p[0] = 'pexpr' + p[0] = self.ast.Binary(p[2], p[1], p[3]) def p_probe(self, p): """probe : FULL LPAREN varref RPAREN @@ -627,7 +702,7 @@ class Parser(object): | EMPTY LPAREN varref RPAREN | NEMPTY LPAREN varref RPAREN """ - p[0] = 'probe' + p[0] = self.ast.Call(p[1], self.ast.Sequence([p[3]])) def p_expr_paren(self, p): """expr : LPAREN expr RPAREN""" @@ -676,8 +751,7 @@ class Parser(object): """expr : varref RCV LBRACKET rargs RBRACKET | varref R_RCV LBRACKET rargs RBRACKET """ - p[0] = p[1] - warnings.warn('not implemented') + p[0] = self.ast.ReceiveExpr(p[1], p[4]) def p_expr_other(self, p): """expr : LPAREN expr ARROW expr COLON expr RPAREN @@ -689,12 +763,15 @@ class Parser(object): warnings.warn('"{s}" not implemented'.format(s=p[1])) def p_expr_run(self, p): - """expr : RUN aname LPAREN args RPAREN opt_priority""" + """expr : RUN aname LPAREN decl0 RPAREN opt_priority""" p[0] = self.ast.Run(p[2], p[4], p[6]) + def p_expr_other_1(self, p): + """expr : TIMEOUT""" + p[0] = self.ast.Timeout() + def p_expr_other_2(self, p): - """expr : TIMEOUT - | NONPROGRESS + """expr : NONPROGRESS | PC_VAL LPAREN expr RPAREN """ raise NotImplementedError() @@ -764,10 +841,10 @@ class Parser(object): p[0] = p[2] def p_const(self, p): - """const : boolean + """const : SKIP + | boolean | number """ - # lex maps `skip` to `TRUE` p[0] = p[1] def p_bool(self, p): @@ -783,47 +860,24 @@ class Parser(object): # Auxiliary # ========= - def p_two_args(self, p): - """two_args : expr COMMA expr""" - - def p_args(self, p): - """args : arg""" - p[0] = p[1] - - def p_prargs(self, p): - """prargs : COMMA arg""" - p[0] = p[2] - - def p_prargs_empty(self, p): - """prargs : empty""" - - def p_args_empty(self, p): - """args : empty""" - - def p_margs(self, p): - """margs : arg - | expr LPAREN arg RPAREN - """ - - def p_arg(self, p): - """arg : expr - | expr COMMA arg - """ - p[0] = 'arg' - # TODO: CONST, MINUS CONST %prec UMIN def p_rarg(self, p): - """rarg : varref + """rarg : const + | varref | EVAL LPAREN expr RPAREN """ - p[0] = 'rarg' + # todo: support all cases + # | rarg LPAREN rargs RPAREN + # | LPAREN rargs RPAREN + p[0] = p[1] - def p_rargs(self, p): - """rargs : rarg - | rarg COMMA rargs - | rarg LPAREN rargs RPAREN - | LPAREN rargs RPAREN - """ + def p_rargs_iter(self, p): + """rargs : rarg COMMA rargs""" + p[0] = [p[1]] + p[3] + + def p_rargs_end(self, p): + """rargs : rarg""" + p[0] = [p[1]] def p_proctype(self, p): """proctype : PROCTYPE @@ -887,10 +941,14 @@ class Parser(object): raise Exception('syntax error at: {p}'.format(p=p)) -def cpp(s): +def cpp(code, fic): """Call the C{C} preprocessor with input C{s}.""" try: - p = subprocess.Popen(['cpp', '-E', '-x', 'c'], + if _platform == "darwin": + cppprog = 'clang' + else: + cppprog = 'cpp' + 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 stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE, @@ -900,10 +958,13 @@ def cpp(s): raise Exception('C preprocessor (cpp) not found in path.') else: raise - logger.debug('cpp input:\n' + s) - stdout, stderr = p.communicate(s) + if code: + logger.debug('cpp input:\n' + code) + stdout, stderr = p.communicate(code) logger.debug('cpp returned: {c}'.format(c=p.returncode)) logger.debug('cpp stdout:\n {out}'.format(out=stdout)) + if p.returncode != 0: + raise Exception('C preprocessor return code: {returncode}'.format(returncode=p.returncode)) return stdout diff --git a/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py b/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py deleted file mode 100644 index b26d22aa..00000000 --- a/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py +++ /dev/null @@ -1,759 +0,0 @@ -import logging -import networkx as nx -import networkx.algorithms.isomorphism as iso -from nose.tools import assert_raises -from promela import ast, yacc - - -logger = logging.getLogger(__name__) -logger.setLevel('WARNING') -log = logging.getLogger('promela.yacc') -log.setLevel(logging.ERROR) -h = logging.StreamHandler() -log = logging.getLogger('promela.ast') -log.setLevel('WARNING') -log.addHandler(h) - - -parser = yacc.Parser() - - -def parse_proctype_test(): - s = ''' - active [3] proctype main(){ - int x; - } - ''' - tree = parser.parse(s) - assert isinstance(tree, ast.Program) - assert len(tree) == 1 - p = tree[0] - assert isinstance(p, ast.Proctype) - assert p.name == 'main' - assert isinstance(p.body, ast.Sequence) - assert p.active == 3, type(p.active) - assert p.args is None - assert p.priority is None - assert p.provided is None - - -def parse_if_test(): - s = ''' - proctype p (){ - if - :: skip - fi - } - ''' - tree = parser.parse(s) - assert isinstance(tree, ast.Program) - assert len(tree) == 1 - proc = tree[0] - assert isinstance(proc, ast.Proctype) - assert isinstance(proc.body, ast.Sequence) - assert len(proc.body) == 1 - if_block = proc.body[0] - assert isinstance(if_block, ast.Options) - assert if_block.type == 'if' - options = if_block.options - assert isinstance(options, list) - assert len(options) == 1 - opt0 = options[0] - assert isinstance(opt0, ast.Sequence) - assert len(opt0) == 1 - assert isinstance(opt0[0], ast.Expression) - e = opt0[0].expr - assert isinstance(e, ast.Bool) - assert e.value, e - - -def parse_do_multiple_options_test(): - s = ''' - proctype p (){ - do - :: x -> x = x + 1; - :: (y == 0) -> y = x; y == 1; - od - } - ''' - tree = parser.parse(s) - assert isinstance(tree, ast.Program) - assert len(tree) == 1 - proc = tree[0] - assert isinstance(proc, ast.Proctype) - assert isinstance(proc.body, ast.Sequence) - assert len(proc.body) == 1 - do_block = proc.body[0] - assert isinstance(do_block, ast.Options) - assert do_block.type == 'do' - options = do_block.options - assert isinstance(options, list) - assert len(options) == 2 - opt = options[0] - assert isinstance(opt, ast.Sequence) - assert len(opt) == 2 - assert isinstance(opt[0], ast.Expression) - assert isinstance(opt[1], ast.Assignment) - - opt = options[1] - assert isinstance(opt, ast.Sequence) - assert len(opt) == 3 - assert isinstance(opt[0], ast.Expression) - assert isinstance(opt[1], ast.Assignment) - assert isinstance(opt[2], ast.Expression) - - -def if_one_option_pg_test(): - s = ''' - proctype p (){ - if - :: skip - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1)]) - assert nx.is_isomorphic(g, h) - - -def if_two_options_pg_test(): - s = ''' - proctype p(){ - if - :: true - :: false - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 1)]) - assert nx.is_isomorphic(g, h) - - -def do_one_option_pg_test(): - s = ''' - proctype p(){ - do - :: skip - od - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 0)]) - assert nx.is_isomorphic(g, h) - - -def do_two_options_pg_test(): - s = ''' - proctype p(){ - do - :: true - :: false - od - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 0), (0, 0)]) - assert nx.is_isomorphic(g, h) - - -def nested_if_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: if - :: true - :: false - fi - :: x - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 1), (0, 1)]) - assert nx.is_isomorphic(g, h) - - -def nested_if_not_guard_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: true; - if - :: true - :: false - fi - :: x - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 2), (2, 1), (2, 1)]) - assert nx.is_isomorphic(g, h) - - -def doubly_nested_if_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: if - :: true - :: if - :: true - :: skip - fi - :: false - fi - :: if - :: if - :: true - :: false - fi - fi - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - for i in range(6): - h.add_edge(0, 1) - assert nx.is_isomorphic(g, h) - - -def nested_do_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: do - :: true - :: false - od - :: x - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 2), (0, 2), (2, 2), (2, 2)]) - assert nx.is_isomorphic(g, h) - - -def nested_do_not_guard_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: true; - do - :: true - :: false - od - :: x - fi - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 2), (2, 2), (2, 2)]) - assert nx.is_isomorphic(g, h) - - -def combined_if_do_program_graph_test(): - s = ''' - active proctype p(){ - int x, y, z; - if /* 0 */ - :: do - :: x = 1; /* 2 */ - y == 5 /* 1 */ - - :: z = 3; /* 3 */ - skip /* 1 */ - - :: if - :: z = (3 - x) * y; /* 4 */ - true; /* 5 */ - y = 3 /* 1 */ - - :: true /* 1 */ - fi - od - /* 1 */ - - :: true; /* 6 */ - if - :: true /* 7 */ - - :: true -> /* 8 */ - x = y /* 7 */ - - fi - fi - /* 7 */ - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([ - (0, 2), (0, 3), (0, 4), (0, 1), - (2, 1), (3, 1), (5, 1), - (1, 2), (1, 3), (1, 4), (1, 1), - (4, 5), - # false; if ... - (0, 6), - (6, 7), (6, 8), (8, 7)]) - dump(g, node_label=None) - assert iso.is_isomorphic(g, h) - - -def invalid_label_pg_test(): - s = ''' - proctype p(){ - do - :: S0: x = 1; - od - } - ''' - tree = parser.parse(s) - with assert_raises(Exception): - tree[0].to_pg() - - -def goto_pg_test(): - s = ''' - proctype p(){ - bit x; - x = 1; - goto S0; - x = 2; - S0: x = 3; - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (1, 2)]) - assert nx.is_isomorphic(g, h) - - -def double_goto_pg_test(): - s = ''' - proctype p(){ - bit x; - x = 1; - goto S0; - x = 2; - S0: goto S1; - x = 3; - S1: skip - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (1, 2)]) - assert nx.is_isomorphic(g, h) - - -def goto_inside_if_pg_test(): - s = ''' - proctype p(){ - bit x; - if - :: true; goto S0; x = 1; - :: x = 3; false - fi; - S0: skip - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 2), (2, 1), (1, 3)]) - assert nx.is_isomorphic(g, h) - - -def goto_loop_pg_test(): - s = ''' - proctype p(){ - bit x; - S0: if - :: true; goto S0; x = 1; - :: x = 3; - fi; - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (0, 0)]) - assert nx.is_isomorphic(g, h) - - -def goto_self_loop_pg_test(): - s = ''' - proctype p(){ - S0: goto S1; - S1: goto S0 - } - ''' - tree = parser.parse(s) - with assert_raises(AssertionError): - tree[0].to_pg() - - -def break_pg_test(): - s = ''' - proctype p(){ - bit x; - do - :: true; x = 1; - :: break; x = 3; - od - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 1), (1, 0), (0, 2)]) - assert nx.is_isomorphic(g, h) - - -def nested_break_pg_test(): - s = ''' - proctype p(){ - bit x; - /* 0 */ - do - :: true; /* 2 */ - x == 1; /* 0 */ - - :: do - :: x == 2; - break /* 0 */ - - :: false; /* 4 */ - x == 3 /* 5 */ - - od - /* 5 */ - - :: break; /* 1 */ - x == 4; - - od - /* 1 */ - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([ - (0, 1), - (0, 2), (2, 0), - (0, 0), - (0, 4), (4, 5), - (5, 4), (5, 0)]) - assert nx.is_isomorphic(g, h) - - -def atomic_pg_test(): - s = ''' - proctype p(){ - bit x; - x = 1; - atomic { x = 2; } - x = 3; - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_node(0, context=None) - h.add_node(1, context=None) - h.add_node(2, context='atomic') - h.add_node(3, context=None) - h.add_edges_from([(0, 1), (1, 2), (2, 3)]) - nm = lambda x, y: x['context'] == y['context'] - gm = iso.GraphMatcher(g, h, node_match=nm) - assert gm.is_isomorphic() - - -def do_atomic_dissapears_pg_test(): - s = ''' - proctype p(){ - bit x, y; - /* 0 */ - do - :: true; /* 3 */ - atomic { x = 2; goto S0; /* 1 */ y = 1} - :: x == 1; /* 4 */ y == 2; /* 0 */ - od; - x = 3; - /* 1 */ - S0: skip - /* 2 */ - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([ - (0, 3), (3, 1), (1, 2), - (0, 4), (4, 0)]) - for u in h: - h.add_node(u, context=None) - nm = lambda x, y: x['context'] == y['context'] - gm = iso.GraphMatcher(g, h, node_match=nm) - assert gm.is_isomorphic() - - -def do_atomic_pg_test(): - s = ''' - proctype p(){ - bit x, y; - /* 0 */ - do - :: true; /* 1 */ - atomic { x = 2; /* 2 */ - y = 1; goto S0; } /* 3 */ - :: x == 1; /* 4 */ y == 2; /* 0 */ - od; - x = 3; - /* 3 */ - S0: skip - /* 5 */ - } - ''' - tree = parser.parse(s) - g = tree[0].to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([ - (0, 1), (1, 2), (2, 3), - (3, 5), (0, 4), (4, 0)]) - for u in h: - h.add_node(u, context=None) - h.add_node(2, context='atomic') - nm = lambda x, y: x['context'] == y['context'] - gm = iso.GraphMatcher(g, h, node_match=nm) - assert gm.is_isomorphic() - - -def ltl_block_test(): - s = ''' - bit x, y, c; - - proctype p(){ - if - :: x; - fi - } - - ltl { (x == 1) && []<>(y != 2) && <>[](c == 1) && (x U y) } - ''' - tree = parser.parse(s) - assert len(tree) == 3, repr(tree) - decl, p, ltl = tree - assert isinstance(p, ast.Proctype) - assert isinstance(ltl, ast.LTL) - s = str(ltl.formula) - assert s == ( - '((((x == 1) && ([] (<> (y != 2)))) && ' - '(<> ([] (c == 1)))) && (x U y))'), s - - -def test_else(): - s = ''' - proctype p(){ - byte x; - do - :: x == 0 - :: x == 1 - :: else - od - } - ''' - (proc,) = parser.parse(s) - g = proc.to_pg() - dump(g) - for u, v, d in g.edges(data=True): - c = d['stmt'] - if isinstance(c, ast.Else): - print(c.other_guards) - - -def test_nested_else(): - s = ''' - proctype p(){ - byte x; - do - :: - if - :: false - :: else - fi - od - } - ''' - (proc,) = parser.parse(s) - g = proc.to_pg() - dump(g) - h = nx.MultiDiGraph() - h.add_edges_from([(0, 0), (0, 0)]) - for u in h: - h.add_node(u, context=None) - nm = lambda x, y: x['context'] == y['context'] - gm = iso.GraphMatcher(g, h, node_match=nm) - assert gm.is_isomorphic() - - -def test_double_else(): - s = ''' - proctype foo(){ - bit x; - do - :: - if - :: x - :: else - fi - :: else - od - } - ''' - # syntactic else = Promela language definition - (proc,) = parser.parse(s) - with assert_raises(AssertionError): - proc.to_pg() - # different from Promela language definition - g = proc.to_pg(syntactic_else=True) - active_else = 0 - off_else = 0 - for u, v, d in g.edges(data=True): - stmt = d['stmt'] - if isinstance(stmt, ast.Else): - other = stmt.other_guards - if other is None: - off_else += 1 - else: - active_else += 1 - assert len(other) == 1, other - (other_stmt,) = other - s = str(other_stmt) - assert s == 'x', s - assert active_else == 1, active_else - assert off_else == 1, off_else - - -def test_pg_node_order(): - s = ''' - proctype foo(){ - bit x; - if - :: - do - :: x > 2; x = 1 - :: else; break - od; - x = 1 - :: x = 2 - fi - } - ''' - (proc,) = parser.parse(s) - g = proc.to_pg() - dump(g) - # Final indexing depends on the - # aux goto nodes created and the contraction order. - # The latter depend on the intermediate indexing, - # which is fixed syntactically - # (see `generate_unique_node`). - edges = {(0, 1), (0, 3), (0, 4), (2, 3), - (2, 4), (3, 1), (4, 2)} - assert set(g) == set(range(5)), g.nodes() - assert set(g.edges()) == edges, g.edges() - - -def test_labels(): - s = ''' - active proctype foo(){ - progress: - do - :: true - od - } - ''' - (proc,) = parser.parse(s) - g = proc.to_pg() - for u, d in g.nodes(data=True): - print(d.get('label')) - - -def test_remote_ref(): - s = ''' - proctype foo(){ - bar @ critical - } - ''' - (proc,) = parser.parse(s) - g = proc.to_pg() - (e,) = g.edges(data=True) - u, v, d = e - s = d['stmt'] - assert isinstance(s, ast.Expression), s - ref = s.expr - assert isinstance(ref, ast.RemoteRef), ref - assert ref.proctype == 'bar', ref.proctype - assert ref.label == 'critical', ref.label - assert ref.pid is None, ref.pid - - -def dump(g, fname='g.pdf', node_label='context'): - if logger.getEffectiveLevel() >= logging.DEBUG: - return - # map nodes to integers - ast.dump_graph( - g, fname, node_label=node_label, edge_label='stmt') - - -if __name__ == '__main__': - test_labels() -- 2.37.1 (Apple Git-137.1) _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH 13/18] modifies 3rd party code - promela parser
andrew.butterfi...@scss.tcd.ie Thu, 22 Dec 2022 03:47:14 -0800
