properties.py 6.44 KB
Newer Older
Maxime Perrotin's avatar
Maxime Perrotin committed
1
2
3
4
5
#!/usr/bin/python

''' Property parser for SDL systems

Parse expressions such as:
6
    "stop if state=toto and x=3"
Maxime Perrotin's avatar
Maxime Perrotin committed
7
8
9

and generate code to verify the property

10
11
This shall be used in combination with the OpenGEODE simulator

12
(c) European Space Agency, 2015-2016
Maxime Perrotin's avatar
Maxime Perrotin committed
13
14
15
16
17

Author: Maxime.Perrotin@esa.int
'''

__author__ = "Maxime Perrotin"
18
__license__ = "LGPL v3"
19
__version__ = "1.1.1"
Maxime Perrotin's avatar
Maxime Perrotin committed
20
21
22
23
24
25
26
27
28
29
30
31
32
33
__url__ = "http://taste.tuxfamily.org"

import os
import traceback
import signal
import sys
import platform
import re
import logging
import argparse

from ColorFormatter import ColorFormatter
import opengeode

Maxime Perrotin's avatar
Maxime Perrotin committed
34
35
import checker

36
# Set up the logging facilities
Maxime Perrotin's avatar
Maxime Perrotin committed
37
log = logging.getLogger(__name__)
38
39
40
console = logging.StreamHandler(sys.__stdout__)
console.setFormatter(ColorFormatter())
log.addHandler(console)
Maxime Perrotin's avatar
Maxime Perrotin committed
41

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
MAKEFILE_TEMPLATE = '''all: build

clean:
	@rm -rf *.o *.ad? *.ali bin examiner *.idx *_simu.sh *_interface.aadl *.wrn *.gpr gnat.cfg runSpark.sh lib{name}.so

build:
	asn1.exe -Ada {asn1} -typePrefix asn1Scc -equal
	gnatmake -gnat2012 -c {name}.adb
	gnatbind -n -Llib{name} {name}
	gnatmake -c -gnat2012 b~{name}.adb
	gcc -shared -fPIC -o lib{name}.so b~{name}.o {name}.o {modules} adaasn1rtl.o -lgnat


.PHONY: all clean build
'''
Maxime Perrotin's avatar
Maxime Perrotin committed
57

58
def parse_input_files(pr_files, ppty_file, simu=True):
Maxime Perrotin's avatar
Maxime Perrotin committed
59
60
    ''' Invoke opengeode to parse the SDL models and use the expression
    parser to analyse the properties (stop conditions) '''
61
62

    # Parse the SDL model
Maxime Perrotin's avatar
Maxime Perrotin committed
63
64
65
66
67
68
69
    try:
        ast = opengeode.parse(pr_files)
        process = ast[0].processes[0]
    except (IndexError, IOError) as err:
        raise IOError('SDL Parser failed - {}'.format(err))
    log.info('SDL parser OK')

70
    # Parse the stop conditions (property file)
Maxime Perrotin's avatar
Maxime Perrotin committed
71
72
73
74
75
76
77
78
79
80
81
82
    with open(ppty_file, 'r') as pt:
        stop_conditions, syntax, semantic, warnings, term = \
           opengeode.ogParser.parseSingleElement('stop_if', pt.read(), process)
        for each in syntax:
            log.error(each)
        for each in semantic:
            log.error(each[0])
        for each in warnings:
            log.warning(each[0])

    if syntax or semantic or warnings or not stop_conditions:
        raise IOError('Error parsing stop conditions - Aborting')
83

Maxime Perrotin's avatar
Maxime Perrotin committed
84
85
86
87
    if not simu:
        # Generate code for the model checker (not for interactive simulation)
        checker.generate(ast[0], stop_conditions)

88
    # Set the context in the Ada generator
Maxime Perrotin's avatar
Maxime Perrotin committed
89
90
91
92
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals
93
94
95
96
97

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
98
99
    # Flatten the process to have the proper state names
    opengeode.Helper.flatten(process, sep=u'\u00dc')
100
101
102
103
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
104
    process.mapping = {state:[] for state in process.mapping.keys()}
105
106
    orig_name = process.processName
    process.processName = '{}_stop_conditions'.format(orig_name)
107
    idx = 0
108
    # For each stop condition create a new Procedure with a boolean return type
109
110
111
112
113
114
115
116
117
118
119
    for each in stop_conditions:
        proc = opengeode.ogAST.Procedure()
        proc.return_type = opengeode.ogParser.BOOLEAN
        proc.inputString = 'property_{}'.format(idx)
        proc.global_variables = process.variables
        proc.global_timers = process.timers
        proc.input_signals = process.input_signals
        proc.output_signals = process.output_signals
        proc.procedures = process.procedures
        proc.operators = process.operators
        proc.content.parent = process
120
        proc.exported = True
121
122
123
124
125
126
        start = opengeode.ogAST.Start()
        start.transition = opengeode.ogAST.Transition()
        proc.content.start = start
        decision = opengeode.ogAST.Terminator()
        decision.kind = 'return'
        decision.return_expr = each
127
        proc.content.start.transition.terminator = decision
128
129
130
131
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1
132
133
134

    opengeode.AdaGenerator.generate(process,
                                    simu=simu,
Maxime Perrotin's avatar
Maxime Perrotin committed
135
                                    ppty_check=orig_name if not simu else "")
Maxime Perrotin's avatar
Maxime Perrotin committed
136

137
    # gather asn.1 files and modules
138
    asn1_files = ' '.join(ast[0].asn1_filenames)
Maxime Perrotin's avatar
Maxime Perrotin committed
139
140
    asn1_modules_o = ' '.join(name.lower().replace('-', '_') + '.o'
                              for name in ast[0].asn1Modules)
141
142
143
    with open('Makefile.properties', 'w') as Makefile:
        Makefile.write(MAKEFILE_TEMPLATE.format(name=process.processName,
                                                asn1=asn1_files,
Maxime Perrotin's avatar
Maxime Perrotin committed
144
                                                modules=asn1_modules_o))
145

Maxime Perrotin's avatar
Maxime Perrotin committed
146
147
148
149
150
151
152
153
154
def cli():
    ''' Application entry point, when used from the command line '''

    version = 'Taste Properties version {}'.format(__version__)

    # Parse the command line
    parser = argparse.ArgumentParser(version=version)
    parser.add_argument('-g', '--verbose', action='store_true', default=False,
                      help='Display debug information')
155
156
    parser.add_argument('-d', '--no_dll', action='store_true', default=False,
                      help='Generate standalone Ada code (not for DLL use)')
Maxime Perrotin's avatar
Maxime Perrotin committed
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
    parser.add_argument('-s', '--spec', dest='spec', default='./spec',
                  help='Path and filename of the property list (one per line)')
    parser.add_argument('models', metavar='file.pr', type=str, nargs='*',
                         help='SDL model(s)')
    options = parser.parse_args()
    if options.verbose:
        log.setLevel(logging.DEBUG)
    else:
        log.setLevel(logging.INFO)
    log.info(version)

    log.debug('{version} using Python {pyVersion}'.format(
                        version=version, pyVersion=platform.python_version()))

    if not options.models or not options.spec:
        log.error('You must specify SDL and property files')
        return 1

    log.debug('SDL files: {}'.format(', '.join(options.models)))
    log.debug('Property file: {}'.format(options.spec))

Maxime Perrotin's avatar
Maxime Perrotin committed
178
    try:
179
        parse_input_files(options.models, options.spec, not options.no_dll)
Maxime Perrotin's avatar
Maxime Perrotin committed
180
181
    except IOError as err:
        log.error(str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
182
183
184
185
186
187
188

    return 0

if __name__ == '__main__':
    # Exit app on Ctrl-C
    signal.signal(signal.SIGINT, signal.SIG_DFL)
    sys.exit(cli())