source: rtems-central/formal/promela/src/src/modules/promela_yacc/promela/ast.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: 31.4 KB
Line 
1"""Abstract syntax tree for Promela."""
2from __future__ import absolute_import
3from __future__ import division
4import logging
5import copy
6import ctypes
7import pprint
8import networkx as nx
9from networkx.utils import misc
10
11
12logger = logging.getLogger(__name__)
13DATATYPES = {
14    'bit': ctypes.c_bool,
15    'bool': ctypes.c_bool,
16    'byte': ctypes.c_ubyte,
17    'pid': ctypes.c_ubyte,
18    'short': ctypes.c_short,
19    'int': ctypes.c_int,
20    'unsigned': None,
21    'chan': None,
22    'mtype': None}
23N = 0
24
25
26def generate_unique_node():
27    """Return a fresh integer to be used as node."""
28    global N
29    N += 1
30    return N
31
32
33def _indent(s, depth=1, skip=0):
34    w = []
35    for i, line in enumerate(s.splitlines()):
36        indent = '' if i < skip else depth * '\t'
37        w.append(indent + line)
38    return '\n'.join(w)
39
40
41def to_str(x):
42    try:
43        return x.to_str()
44    except AttributeError:
45        return str(x)
46
47
48class Proctype(object):
49    def __init__(self, name, body, args=None,
50                 active=None, d_proc=False,
51                 priority=None, provided=None,
52                 disable_negation=False):
53        self.name = name
54        self.body = body
55        self.args = args
56        if active is None:
57            active = 0
58        self.d_proc = d_proc
59        if priority is not None:
60            priority = int(priority.value)
61        self.active = active
62        self.priority = priority
63        self.provided = provided
64        self.disable_negation = disable_negation
65
66    def __str__(self):
67        return "Proctype('{name}')".format(name=self.name)
68
69    def to_str(self):
70        return (
71            '{active} proctype {name}({args}){{\n'
72            '{body}\n'
73            '}}\n\n').format(
74                active=self._active_str(),
75                name=self.name,
76                args=self._args_str(),
77                body=_indent(to_str(self.body)))
78
79    def _active_str(self):
80        if self.active is None:
81            active = ''
82        else:
83            active = 'active [' + to_str(self.active) + '] '
84        return active
85
86    def _args_str(self):
87        if self.args is None:
88            args = ''
89        else:
90            args = '; '.join(to_str(xx) for x in self.args for xx in x)
91        return args
92
93    def to_pg(self, syntactic_else=False):
94        """Return program graph of proctype.
95
96        @param syntactic_else: if `True`, then "else"
97            statements in directly nested "if" or "do"
98            take precedence based on syntactic context.
99            The Promela language reference defines
100            "else" semantically, with respect to
101            the program graph.
102        """
103        global N
104        N = 1
105        g = nx.MultiDiGraph(name=self.name)
106        g.locals = set()
107        ine, out = self.body.to_pg(g, syntactic_else=syntactic_else)
108        # root: explicit is better than implicit
109        u = generate_unique_node()
110        g.add_node(u, color='red', context=None)
111        g.root = u
112        for v, d in ine:
113            g.add_edge(u, v, **d)
114        # rm unreachable nodes
115        S = nx.descendants(g, g.root)
116        S.add(g.root)
117        nodes_to_rm = {x for x in g.nodes() if x not in S}
118        [g.remove_node(x) for x in nodes_to_rm]
119        if logger.getEffectiveLevel() == 1:
120            dump_graph(
121                g, 'dbg.pdf', node_label='context',
122                edge_label='stmt', relabel=True)
123        # contract goto edges
124        assert_gotos_are_admissible(g)
125        for u in sorted(g.nodes(), key=str):
126            contract_goto_edges(g, u)
127        h = map_uuid_to_int(g)
128        # other out-edges of each node with an `else`
129        if not syntactic_else:
130            semantic_else(h)
131        return h
132
133
134def contract_goto_edges(g, u):
135    """Identify nodes connected with `goto` edge."""
136    assert u in g
137    assert g.root in g
138    n = g.out_degree(u)
139    if n == 0 or 1 < n:
140        return
141    assert n == 1, n
142    # single outgoing edge: safe to contract
143    _, q, d = next(iter(g.edges(u, data=True)))
144    if d['stmt'] != 'goto':
145        return
146    # goto
147    assert u != q, 'loop of `goto`s detected'
148    # the source node context (atomic or d_step) is overwritten
149    for p, _, d in g.in_edges(u, data=True):
150        g.add_edge(p, q, **d)
151    # but the source node label is preserved
152    u_label = g.node[u].get('labels')
153    if u_label is not None:
154        g.node[q].setdefault('labels', set()).update(u_label)
155    g.remove_node(u)
156    if u == g.root:
157        g.root = q
158
159
160def assert_gotos_are_admissible(g):
161    """Assert no branch node has outgoing `goto`."""
162    # branch node cannot have goto
163    # `goto` and `break` must have transformed to `true`
164    # labels must have raised `Exception`
165    for u in g:
166        if g.out_degree(u) <= 1:
167            continue
168        for _, v, d in g.edges(u, data=True):
169            assert 'stmt' in d
170            stmt = d['stmt']
171            assert stmt != 'goto', stmt
172    for u, d in g.nodes(data=True):
173        assert 'context' in d
174    for u, v, d in g.edges(data=True):
175        assert 'stmt' in d
176
177
178def map_uuid_to_int(g):
179    """Reinplace uuid nodes with integers."""
180    umap = {u: i for i, u in enumerate(sorted(g, key=str))}
181    h = nx.MultiDiGraph(name=g.name)
182    for u, d in g.nodes(data=True):
183        p = umap[u]
184        h.add_node(p, **d)
185    for u, v, key, d in g.edges(keys=True, data=True):
186        p = umap[u]
187        q = umap[v]
188        h.add_edge(p, q, key=key, **d)
189    h.root = umap[g.root]
190    h.locals = g.locals
191    return h
192
193
194def semantic_else(g):
195    """Set `Else.other_guards` to other edges with same source."""
196    for u, v, d in g.edges(data=True):
197        stmt = d['stmt']
198        if not isinstance(stmt, Else):
199            continue
200        # is `Else`
201        stmt.other_guards = [
202            q['stmt'] for _, _, q in g.out_edges(u, data=True)
203            if q['stmt'] != stmt]
204
205
206class NeverClaim(Proctype):
207    """Subclass exists only for semantic purposes."""
208    def to_str(self):
209        name = '' if self.name is None else self.name
210        s = (
211            'never ' + name + '{\n' +
212            _indent(to_str(self.body)) + '\n'
213            '}\n\n')
214        return s
215
216
217class Init(Proctype):
218    def to_str(self):
219        return (
220            'init ' + '{\n' +
221            _indent(to_str(self.body)) + '\n'
222            '}\n\n')
223
224
225class Program(list):
226    def __str__(self):
227        return '\n'.join(to_str(x) for x, _ in self)
228
229    def __repr__(self):
230        c = super(Program, self).__repr__()
231        return 'Program({c})'.format(c=c)
232
233    def to_table(self):
234        """Return global definitions, proctypes, and LTL blocks.
235
236        @rtype: 3-`tuple` of `set`
237        """
238        units = misc.flatten(self)
239        ltl = {x for x in units if isinstance(x, LTL)}
240        proctypes = {x for x in units if isinstance(x, Proctype)}
241        global_defs = {x for x in units
242                       if x not in proctypes and x not in ltl}
243        return global_defs, proctypes, ltl
244
245
246class LTL(object):
247    """Used to mark strings as LTL blocks."""
248
249    def __init__(self, formula, name = None):
250        self.formula = formula
251        self.name = name
252
253    def __repr__(self):
254        return 'LTL({f})'.format(f=repr(self.formula))
255
256    def __str__(self):
257        return 'ltl ' + (self.name + ' ' if self.name else '') + '{' + str(self.formula) + '}'
258
259
260class Sequence(list):
261    def __init__(self, iterable, context=None, context_for_var=None, context_for_begin=None, context_for_end=None, is_option=False):
262        super(Sequence, self).__init__(iterable)
263        # "for" or "atomic" or "dstep"
264        self.context = context
265        self.context_for_var = context_for_var
266        self.context_for_begin = context_for_begin
267        self.context_for_end = context_for_end
268        self.is_option = is_option
269
270    def to_str(self):
271        if self.context is None:
272            return '\n'.join(to_str(x) for x in self)
273        else:
274            return (
275                self.context +
276                (' (' + self.context_for_var + ' : ' + to_str (self.context_for_begin) + ' .. ' + to_str (self.context_for_end) + ') ' if self.context == 'for' else '') +
277                '{\n' +
278                '\n'.join(_indent(to_str(x)) for x in self) + '\n}\n')
279
280    def __repr__(self):
281        l = super(Sequence, self).__repr__()
282        return 'Sequence({l}, context={c}, context_for_var={cfv}, context_for_begin={cfb}, context_for_end={cfe}, is_option={isopt})'.format(
283            l=l, c=self.context, cfv=self.context_for_var, cfb=self.context_for_begin, cfe=self.context_for_end, isopt=self.is_option)
284
285    def to_pg(self, g, context=None, option_guard=None, **kw):
286        # set context
287        if context is None:
288            context = self.context
289        c = context
290        assert c in {'atomic', 'd_step', None} # TODO: 'for'
291        # atomic cannot appear inside d_step
292        if context == 'd_step' and c == 'atomic':
293            raise Exception('atomic inside d_step')
294        context = c
295        # find first non-decl
296        # option guard first
297        option_guard = self.is_option or option_guard
298        assert len(self) > 0
299        stmts = iter(self)
300        t = None
301        for stmt in stmts:
302            t = stmt.to_pg(g, context=context,
303                           option_guard=option_guard, **kw)
304            if t is not None:
305                break
306        # no statements ?
307        if t is None:
308            return None
309        e, tail = t
310        # guard can't be a goto or label
311        # (should have been caught below)
312        if option_guard:
313            for u, d in e:
314                assert d.get('stmt') != 'goto', self
315        # other option statements
316        for stmt in stmts:
317            t = stmt.to_pg(g, context=context, option_guard=None, **kw)
318            # decl ?
319            if t is None:
320                continue
321            ine, out = t
322            # connect tail to ine
323            assert ine
324            for v, d in ine:
325                g.add_edge(tail, v, **d)
326            # update tail
327            assert out in g
328            tail = out
329        return e, tail
330
331
332class Node(object):
333    def to_pg(self, g, context=None, **kw):
334        u = generate_unique_node()
335        g.add_node(u, context=context)
336        e = (u, dict(stmt=self))
337        return [e], u
338
339
340class Options(Node):
341    def __init__(self, opt_type, options):
342        self.type = opt_type
343        self.options = options
344
345    def to_str(self):
346        a, b = self.entry_exit
347        c = list()
348        c.append(a)
349        c.append('\n')
350        for option in self.options:
351            option_guard = _indent(to_str(option[0]), skip=1)
352            w = [_indent(to_str(x)) for x in option[1:]]
353            c.append(
354                ':: {option_guard}{tail}\n'.format(
355                    option_guard=option_guard,
356                    tail=(' ->\n' + '\n'.join(w)) if w else ''))
357        c.append(b)
358        c.append(';\n')
359        return ''.join(c)
360
361    @property
362    def entry_exit(self):
363        if self.type == 'if':
364            return ('if', 'fi')
365        elif self.type == 'do':
366            return ('do', 'od')
367
368    def to_pg(self, g, od_exit=None,
369              context=None, option_guard=None,
370              syntactic_else=False, **kw):
371        logger.info('-- start flattening {t}'.format(t=self.type))
372        assert self.options
373        assert self.type in {'if', 'do'}
374        # create target
375        target = generate_unique_node()
376        g.add_node(target, context=context)
377        # target != exit node ?
378        if self.type == 'do':
379            od_exit = generate_unique_node()
380            g.add_node(od_exit, context=context)
381        self_else = None
382        self_has_else = False
383        option_has_else = False
384        edges = list()
385        else_ine = None
386        for option in self.options:
387            logger.debug('option: {opt}'.format(opt=option))
388            t = option.to_pg(g, od_exit=od_exit, context=context, **kw)
389            assert t is not None  # decls filtered by `Sequence`
390            ine, out = t
391            assert out in g
392            # detect `else`
393            has_else = False
394            for u, d in ine:
395                stmt = d.get('stmt')
396                if isinstance(stmt, Else):
397                    has_else = True
398                    self_else = stmt
399                # option cannot start with goto (= contraction)
400                assert stmt != 'goto'
401            # who owns this else ?
402            if has_else:
403                if len(ine) == 1:
404                    assert not self_has_else, option
405                    self_has_else = True
406                    if not syntactic_else:
407                        assert not option_has_else, option
408                elif len(ine) > 1:
409                    option_has_else = True
410                    if not syntactic_else:
411                        assert not self_has_else, option
412                else:
413                    raise Exception('option with no in edges')
414            # collect in edges, except for own `else`
415            if not (has_else and self_has_else):
416                edges.extend(ine)
417            else:
418                else_ine = ine  # keep for later
419            # forward edges
420            # goto from last option node to target node
421            g.add_edge(out, target, stmt='goto')
422            # backward edges
423            if self.type == 'if':
424                continue
425            for u, d in ine:
426                g.add_edge(target, u, **d)
427        # handle else
428        if self_has_else and not option_has_else:
429            self_else.other_guards = [d['stmt'] for v, d in edges]
430            # add back the `else` edge
431            edges.extend(else_ine)
432        # what is the exit node ?
433        if self.type == 'if':
434            out = target
435        elif self.type == 'do':
436            out = od_exit
437        else:
438            raise Exception('Unknown type: {t}'.format(t=out))
439        # is not itself an option guard ?
440        if option_guard:
441            logger.debug('is option guard')
442        if self.type == 'do' and option_guard is None:
443            edge = (target, dict(stmt='goto'))
444            in_edges = [edge]
445        else:
446            in_edges = edges
447        logger.debug('in edges: {ie}, out: {out}\n'.format(
448            ie=in_edges, out=out))
449        logger.info('-- end flattening {t}'.format(t=self.type))
450        assert out in g
451        return in_edges, out
452
453
454class Else(Node):
455    def __init__(self):
456        self.other_guards = None
457
458    def __str__(self):
459        return 'else'
460
461
462class Break(Node):
463    def __str__(self):
464        return 'break'
465
466    def to_pg(self, g, od_exit=None, **kw):
467        if od_exit is None:
468            raise Exception('Break outside repetition construct.')
469        # like goto, but with: v = od_exit
470        # context of od_tail is determined by do loop
471        assert od_exit in g
472        v = od_exit
473        return goto_to_pg(g, v, **kw)
474
475
476class Goto(Node):
477    def __init__(self, label):
478        self.label = label
479
480    def __str__(self):
481        return 'goto {l}'.format(l=self.label)
482
483    def to_pg(self, g, context=None, **kw):
484        v = _format_label(self.label)
485        # ok, because source node context
486        # is overwritten during contraction
487        g.add_node(v, context=context)
488        return goto_to_pg(g, v, context=context, **kw)
489
490
491def goto_to_pg(g, v, option_guard=None, context=None, **kw):
492    assert v in g
493    if option_guard is None:
494        stmt = 'goto'
495    else:
496        stmt = Bool('true')
497    e = (v, dict(stmt=stmt))
498    u = generate_unique_node()
499    g.add_node(u, context=context)
500    return [e], u
501
502
503class Label(Node):
504    def __init__(self, label, body):
505        self.label = label
506        self.body = body
507
508    def to_str(self):
509        return '{l}: {b}'.format(l=self.label, b=to_str(self.body))
510
511    def to_pg(self, g, option_guard=None, context=None, **kw):
512        if option_guard is not None:
513            raise Exception('option guard cannot be labeled')
514        # add label node, with context
515        u = _format_label(self.label)
516        g.add_node(u, context=context, labels={self.label})
517        # flatten body
518        t = self.body.to_pg(g, context=context, **kw)
519        if t is None:
520            raise Exception('Label of variable declaration.')
521        ine, out = t
522        assert out in g
523        # make ine out edges of label node
524        for v, d in ine:
525            g.add_edge(u, v, **d)
526        # appear like a goto (almost)
527        e = (u, dict(stmt='goto'))
528        return [e], out
529
530
531def _format_label(label):
532    return 'label_{l}'.format(l=label)
533
534
535# TODO: check that referenced types exist, before adding typedef
536# to symbol table
537
538class VarDef(Node):
539    def __init__(self, name, vartype, length=None,
540                 visible=None, bitwidth=None,
541                 msg_types=None, initval=None):
542        self.name = name
543        self.type = vartype
544        if length is None:
545            l = None
546        else:
547            l = eval(str(length))
548            assert isinstance(l, int), l
549        self.length = l
550        self.visible = visible
551        self.bitwidth = int(bitwidth.value) if bitwidth else None
552        if vartype == 'bool':
553            default_initval = Bool('false')
554        else:
555            default_initval = Integer('0')
556        self.msg_types = msg_types
557        self.initial_value0 = initval
558        if initval is None:
559            initval = Expression(default_initval)
560        self.initial_value = initval
561        # TODO message types
562
563    def __repr__(self):
564        return 'VarDef({t}, {v})'.format(t=self.type, v=self.name)
565
566    def to_str(self):
567        s = '{type} {varname}{bitwidth}{len}{initval}{msg_types}'.format(
568            type=self._type_str(),
569            varname=self.name,
570            bitwidth=' : {n}'.format(n =self.bitwidth) if self.bitwidth else '',
571            len=' [{n}]'.format(n=self.length) if self.length and not self.msg_types else '',
572            initval=' = {i}'.format(i=self.initial_value0) if self.initial_value0 else '',
573            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 '')
574        return s
575
576    def _type_str(self):
577        return self.type
578
579    def to_pg(self, g, **kw):
580        # var declarations are collected before the process runs
581        # man page: datatypes, p.405
582        g.locals.add(self)
583        return None
584
585    def insert(self, symbol_table, pid):
586        """Insert variable into table of symbols.
587
588        @type symbol_table: L{SymbolTable}
589
590        @type pid: int or None
591        """
592        t = self.type
593        if t == 'chan':
594            v = MessageChannel(self.len)
595            # channels are always available globally
596            # note how this differs from having global scope:
597            # no name conflicts
598            symbol_table.channels.add(v)
599        elif t == 'mtype':
600            raise NotImplementedError
601        elif t in {'bit', 'bool', 'byte', 'pid', 'short', 'int'}:
602            if self.len is None:
603                v = DATATYPES[t]()
604            else:
605                v = [DATATYPES[t]() for i in range(self.len)]
606        elif t == 'unsigned':
607            n = self.bitwidth
608
609            class Unsigned(ctypes.Structure):
610                _fields_ = [('value', ctypes.c_uint, n)]
611
612            if self.len is None:
613                v = Unsigned()
614            else:
615                v = [Unsigned() for i in range(self.len)]
616        else:
617            raise TypeError('unknown type "{t}"'.format(t=t))
618        # global scope ?
619        if pid is None:
620            d = symbol_table.globals
621        else:
622            d = symbol_table.locals[pid]
623        name = self.name
624        if name in d:
625            raise Exception('variable "{name}" is already defined'.format(
626                            name=name))
627        else:
628            d[name] = v
629
630
631class SymbolTable(object):
632    """Variable, user data and message type definitions.
633
634    Attributes:
635
636      - `globals`: `dict` of global vars
637      - `locals`: `dict` of `dicts`, keys of outer `dict` are pids
638      - `channels`: `dict` of global lists for channels
639      - `pids`: map from:
640
641          pid integers
642
643          to:
644
645            - name of proctype (name)
646            - current value of program counter (pc)
647
648      - `types`: `dict` of data types
649
650    pids are non-negative integers.
651    The type name "mtype" corresponds to a message type.
652    """
653
654    def __init__(self):
655        # see Def. 7.6, p.157
656        self.exclusive = None
657        self.handshake = None
658        self.timeout = False
659        self.else_ = False
660        self.stutter = False
661        # tables of variables
662        self.globals = dict()
663        self.channels = set()
664        self.locals = dict()
665        self.pids = dict()
666        self.types = DATATYPES
667
668    def __hash__(self):
669        return hash(repr(self))
670
671    def __eq__(self, other):
672        assert(isinstance(other, SymbolTable))
673        if self.globals != other.globals:
674            return False
675        if self.channels != other.channels:
676            return False
677        if set(self.locals) != set(other.locals):
678            return False
679        for pid, d in self.locals.items():
680            if d != other.locals[pid]:
681                return False
682        if set(self.pids) != set(other.pids):
683            return False
684        for pid, d in self.pids.items():
685            q = other.pids[pid]
686            if d['name'] != q['name']:
687                return False
688            if d['pc'] != q['pc']:
689                return False
690        return True
691
692    def __str__(self):
693        return (
694            'globals: {g}\n'
695            'channels: {c}\n'
696            'pids: {p}\n\n'
697            'types: {t}\n'
698            'locals: {l}\n'
699            'exclusive: {e}\n').format(
700                g=self.globals,
701                l=self.locals,
702                p=pprint.pformat(self.pids, width=15),
703                t=self.types,
704                e=self.exclusive,
705                c=self.channels)
706
707    def copy(self):
708        new = SymbolTable()
709        # auxiliary
710        new.exclusive = self.exclusive
711        new.handshake = self.handshake
712        new.timeout = self.timeout
713        new.else_ = self.else_
714        new.stutter = self.stutter
715        # copy symbols
716        new.globals = copy.deepcopy(self.globals)
717        new.channels = copy.deepcopy(self.channels)
718        new.locals = copy.deepcopy(self.locals)
719        new.pids = {k: {'name': d['name'],
720                        'pc': d['pc']}
721                    for k, d in self.pids.items()}
722        new.types = self.types
723        return new
724
725
726class MessageChannel(object):
727    def __init__(self, nslots):
728        self.nslots = nslots
729        self.contents = list()
730
731    def send(self, x):
732        if len(self.contents) < self.nslots:
733            self.contents.append(x)
734        else:
735            raise Exception('channel {name} is full'.format(
736                            name=self.name))
737
738    def receive(self, x=None, random=False, rm=True):
739        c = self.contents
740        i = 0
741        if x and random:
742            i = c.index(x)
743        m = c[i]
744        if rm:
745            c.pop(i)
746        return m
747
748
749class TypeDef(Node):
750    def __init__(self, name, decls):
751        self.name = name
752        self.decls = decls
753
754    def __str__(self):
755        return 'typedef {name} {{ {decls} }}'.format(
756            name=self.name, decls='; '.join(to_str(x) for x in self.decls))
757
758    def exe(self, t):
759        t.types[self.name] = self
760
761
762class MessageType(Node):
763    def __init__(self, values, visible=None):
764        self.values = values
765
766    def to_str(self):
767        return 'mtype = {{ {values} }}'.format(values=' , '.join(to_str(x) for x in self.values))
768
769    def exe(self, t):
770        t.types[self.name] = self
771
772
773class Return(Node):
774    def __init__(self, expr):
775        self.expr = expr
776
777    def __str__(self):
778        return to_str(self.expr)
779
780
781class Run(Node):
782    def __init__(self, func, args=None, priority=None):
783        self.func = func
784        self.args = args
785        self.priority = priority
786
787    def __str__(self):
788        return 'run {f} ({args})'.format(f=self.func, args='' if self.args is None else ' , '.join(to_str(x) for x in self.args))
789
790
791class InlineDef(Node):
792    def __init__(self, name, decl, body, disable_negation=False):
793        self.name = name
794        self.decl = decl
795        self.body = body
796        self.disable_negation = disable_negation
797
798    def __str__(self):
799        return ('inline {name} ({decl}) {{\n'
800                '{body}\n'
801                '}}\n\n').format(
802                    name = self.name,
803                    decl = ', '.join(to_str(x) for x in self.decl) if self.decl else '',
804                    body = _indent(to_str(self.body)))
805
806class Call(Node):
807    def __init__(self, name, args):
808        self.name = name
809        self.args = args
810
811    def __str__(self):
812        return '{name} ({args})'.format(name = self.name, args = ', '.join(to_str(x) for x in self.args) if self.args else '')
813
814
815class Assert(Node):
816    def __init__(self, expr, pos = None):
817        self.expr = expr
818        self.pos = pos
819
820    def __str__(self):
821        return 'assert({expr})'.format(expr=to_str(self.expr))
822
823
824class Expression(Node):
825    def __init__(self, expr):
826        self.expr = expr
827
828    def __repr__(self):
829        return 'Expression({expr})'.format(expr=repr(self.expr))
830
831    def __str__(self):
832        return to_str(self.expr)
833
834    def eval(self, g, l):
835        s = str(self)
836        g = dict(g)
837        for k, v in g.items():
838            if 'ctypes' in str(type(v)):
839                g[k] = int(v.value)
840            elif isinstance(v, list):
841                for x in v:
842                    if 'ctypes' in str(type(x)):
843                        v[v.index(x)] = int(x.value)
844        l = dict(l)
845        for k, v in l.items():
846            if 'ctypes' in str(type(v)):
847                l[k] = int(v.value)
848            elif isinstance(v, list):
849                for x in v:
850                    if 'ctypes' in str(type(x)):
851                        v[v.index(x)] = int(x.value)
852
853        v = eval(s, g, l)
854        return v
855
856
857class Assignment(Node):
858    def __init__(self, var, value):
859        self.var = var
860        self.value = value
861
862    def __repr__(self):
863        return 'Assignment({var}, {val})'.format(
864            var=repr(self.var), val=repr(self.value))
865
866    def __str__(self):
867        return '{var} = {val}'.format(var=self.var, val=self.value)
868
869    def exe(self, g, l):
870        logger.debug('Assign: {var} = {val}'.format(
871                     var=self.var, val=self.value))
872        s = self.to_str()
873        og = g
874        ol = l
875        g = dict(g)
876        for k, v in g.items():
877            if 'ctypes' in str(type(v)):
878                g[k] = int(v.value)
879            elif isinstance(v, list):
880                for x in v:
881                    if 'ctypes' in str(type(x)):
882                        v[v.index(x)] = int(x.value)
883        l = dict(l)
884        for k, v in l.items():
885            if 'ctypes' in str(type(v)):
886                l[k] = int(v.value)
887            elif isinstance(v, list):
888                for x in v:
889                    if 'ctypes' in str(type(x)):
890                        v[v.index(x)] = int(x.value)
891        exec(s, g, l)
892        for k in og:
893            og[k] = g[k]
894        for k in ol:
895            ol[k] = l[k]
896
897
898class Receive(Node):
899    def __init__(self, varref, args):
900        self.var = varref
901        self.args = args
902
903    def __str__(self):
904        v = to_str(self.var)
905        return '{v} ? {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
906
907
908class Send(Node):
909    def __init__(self, varref, args):
910        self.var = varref
911        self.args = args
912
913    def __str__(self):
914        v = to_str(self.var)
915        return '{v} ! {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
916
917
918class Printf(Node):
919    def __init__(self, s, args=None):
920        self.s = s
921        self.args = args
922
923    def __str__(self):
924        return 'printf({s}{args})'.format(s=self.s, args='' if self.args is None else ' , ' + ' , '.join(to_str(x) for x in self.args))
925
926
927class Operator(object):
928    def __init__(self, operator, *operands):
929        self.operator = operator
930        self.operands = operands
931
932    def __repr__(self):
933        return 'Operator({op}, {xy})'.format(
934            op=repr(self.operator),
935            xy=', '.join(repr(x) for x in self.operands))
936
937    def __str__(self):
938        return '({op} {xy})'.format(
939            op=self.operator,
940            xy=' '.join(to_str(x) for x in self.operands))
941
942
943class Binary(Operator):
944    def __str__(self):
945        return '({x} {op} {y})'.format(
946            x=to_str(self.operands[0]),
947            op=self.operator,
948            y=to_str(self.operands[1]))
949
950
951class Unary(Operator):
952    pass
953
954class ReceiveExpr(Node):
955    def __init__(self, varref, args):
956        self.var = varref
957        self.args = args
958
959    def __str__(self):
960        v = to_str(self.var)
961        return '({v} ? [{args}])'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
962
963class Terminal(object):
964    def __init__(self, value):
965        self.value = value
966
967    def __repr__(self):
968        return '{classname}({val})'.format(
969            classname=type(self).__name__,
970            val=repr(self.value))
971
972    def __str__(self):
973        return str(self.value)
974
975
976class VarRef(Terminal):
977    def __init__(self, name, index=None, extension=None):
978        self.name = name
979        if index is None:
980            i = None
981        else:
982            i = index
983        self.index = i
984        self.extension = extension
985        # used by some external methods
986        self.value = name
987
988    def __repr__(self):
989        return 'VarRef({name}, {index}, {ext})'.format(
990            name=repr(self.name),
991            index=repr(self.index),
992            ext=repr(self.extension))
993
994    def __str__(self):
995        if self.index is None:
996            i = ''
997        else:
998            i = '[{i}]'.format(i=to_str(self.index))
999        return '{name}{index}{ext}'.format(
1000            name=self.name,
1001            index=i,
1002            ext=('.' + to_str(self.extension)) if self.extension else '' )
1003
1004
1005class Integer(Terminal):
1006    def __bool__(self):
1007        return bool(int(self.value))
1008
1009
1010class Bool(Terminal):
1011    def __init__(self, val):
1012        self.value = val.upper() == 'TRUE'
1013
1014    def __bool__(self):
1015        return self.value
1016
1017    def __repr__(self):
1018        return 'Bool({value})'.format(value=repr(self.value))
1019
1020    def __str__(self):
1021        return str('true' if self.value else 'false')
1022
1023
1024class RemoteRef(Terminal):
1025    def __init__(self, proctype, label, pid=None):
1026        self.proctype = proctype
1027        self.label = label
1028        self.pid = pid
1029
1030    def __repr__(self):
1031        return 'RemoteRef({proc}, {label}, {pid})'.format(
1032            proc=self.proctype, label=self.label, pid=self.pid)
1033
1034    def __str__(self):
1035        if self.pid is None:
1036            inst = ''
1037        else:
1038            inst = '[{pid}]'.format(pid=self.pid)
1039        return '{proc} {inst} @ {label}'.format(
1040            proc=self.proctype, inst=inst, label=self.label)
1041
1042
1043class Timeout(Node):
1044    def __init__(self):
1045        return
1046
1047    def __str__(self):
1048        return 'timeout'
1049
1050
1051def dump_graph(g, fname='a.pdf', node_label='label',
1052               edge_label='label', relabel=False):
1053    """Write the program graph, annotated with formulae, to PDF file."""
1054    # map nodes to integers
1055    if relabel:
1056        mapping = {u: i for i, u in enumerate(g)}
1057        g = nx.relabel_nodes(g, mapping)
1058        inv_mapping = {v: k for k, v in mapping.items()}
1059        s = list()
1060        s.append('mapping of nodes:')
1061        for k in sorted(inv_mapping):
1062            v = inv_mapping[k]
1063            s.append('{k}: {v}'.format(k=k, v=v))
1064        print('\n'.join(s))
1065    h = nx.MultiDiGraph()
1066    for u, d in g.nodes(data=True):
1067        label = d.get(node_label, u)
1068        label = '"{label}"'.format(label=label)
1069        h.add_node(u, label=label)
1070    for u, v, d in g.edges(data=True):
1071        label = d.get(edge_label, ' ')
1072        label = '"{label}"'.format(label=label)
1073        h.add_edge(u, v, label=label)
1074    pd = nx.drawing.nx_pydot.to_pydot(h)
1075    pd.write_pdf(fname)
Note: See TracBrowser for help on using the repository browser.