properties.py 6.28 KB
Newer Older
Maxime Perrotin's avatar
Maxime Perrotin committed
1
2
3
4
5
6
7
8
9
#!/usr/bin/python

''' Property parser for SDL systems

Parse expressions such as:
    "stop if state=toto and x = 3"

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.0.4"
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

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

40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
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
55

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

    # Parse the SDL model
Maxime Perrotin's avatar
Maxime Perrotin committed
61
62
63
64
65
66
67
    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')

68
    # Parse the stop conditions (property file)
Maxime Perrotin's avatar
Maxime Perrotin committed
69
70
71
72
73
74
75
76
77
78
79
80
    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')
81
82

    # Set the context in the Ada generator
Maxime Perrotin's avatar
Maxime Perrotin committed
83
84
85
86
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals
87
88
89
90
91

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
92
93
    # Flatten the process to have the proper state names
    opengeode.Helper.flatten(process, sep=u'\u00dc')
94
95
96
97
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
98
    process.mapping = {state:[] for state in process.mapping.keys()}
99
100
    orig_name = process.processName
    process.processName = '{}_stop_conditions'.format(orig_name)
101
    idx = 0
102
    # For each stop condition create a new Procedure with a boolean return type
103
104
105
106
107
108
109
110
111
112
113
    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
114
        proc.exported = True
115
116
117
118
119
120
        start = opengeode.ogAST.Start()
        start.transition = opengeode.ogAST.Transition()
        proc.content.start = start
        decision = opengeode.ogAST.Terminator()
        decision.kind = 'return'
        decision.return_expr = each
121
        proc.content.start.transition.terminator = decision
122
123
124
125
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1
126
127
128

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

131
    # gather asn.1 files and modules
132
    asn1_files = ' '.join(ast[0].asn1_filenames)
133
134
135
136
137
138
139
    asn1_modules = ' '.join(name.lower().replace('-', '_') + '.o'
                            for name in ast[0].asn1Modules)
    with open('Makefile.properties', 'w') as Makefile:
        Makefile.write(MAKEFILE_TEMPLATE.format(name=process.processName,
                                                asn1=asn1_files,
                                                modules=asn1_modules))

Maxime Perrotin's avatar
Maxime Perrotin committed
140
141
142
143
144
145
146
147
148
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')
149
150
    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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
    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
172
    try:
173
        parse_input_files(options.models, options.spec, not options.no_dll)
Maxime Perrotin's avatar
Maxime Perrotin committed
174
175
    except IOError as err:
        log.error(str(err))
Maxime Perrotin's avatar
Maxime Perrotin committed
176
177
178
179
180
181
182

    return 0

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