properties.py 6.47 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
#!/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

This shall be used in combination with the OpenGEODE simulator

(c) European Space Agency, 2015-2016

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

__author__ = "Maxime Perrotin"
__license__ = "LGPL v3"
__version__ = "1.1.4"
__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

import checker

# Set up the logging facilities
log = logging.getLogger(__name__)
console = logging.StreamHandler(sys.__stdout__)
console.setFormatter(ColorFormatter())
log.addHandler(console)

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:
48
	mono $(shell which asn1.exe) -Ada -typePrefix asn1Scc -equal {asn1}
49
	gnatmake -gnat2012 -c -fPIC {name}.adb
50
	gnatbind -n -Llib{name} {name}
51
	gnatmake -c -gnat2012 -fPIC b~{name}.adb
52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
	gcc -shared -fPIC -o lib{name}.so b~{name}.o {name}.o {modules} adaasn1rtl.o -lgnat


.PHONY: all clean build
'''

def parse_input_files(pr_files, ppty_file, simu=True):
    ''' Invoke opengeode to parse the SDL models and use the expression
    parser to analyse the properties (stop conditions) '''

    # Parse the SDL model
    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')

    # Parse the stop conditions (property file)
    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')

    if not simu:
        # Generate code for the model checker (not for interactive simulation)
        checker.generate(ast[0], stop_conditions)

    # Set the context in the Ada generator
    opengeode.AdaGenerator.TYPES = process.dataview
    opengeode.AdaGenerator.VARIABLES = process.variables
    opengeode.AdaGenerator.PROCEDURES = process.procedures
    opengeode.AdaGenerator.OUT_SIGNALS = process.output_signals

    # Generate Ada code for each stop condition
    for each in stop_conditions:
        stmts, string, local_decl = opengeode.AdaGenerator.expression(each)
        log.info(string)
    # Flatten the process to have the proper state names
    opengeode.Helper.flatten(process, sep=u'\u00dc')
    process.content.inner_procedures = []
    process.procedures = []
    process.transitions = []
    process.composite_states = []
    process.mapping = {state:[] for state in process.mapping.keys()}
    orig_name = process.processName
    process.processName = '{}_stop_conditions'.format(orig_name)
    idx = 0
    # For each stop condition create a new Procedure with a boolean return type
    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
        proc.exported = True
        start = opengeode.ogAST.Start()
        start.transition = opengeode.ogAST.Transition()
        proc.content.start = start
        decision = opengeode.ogAST.Terminator()
        decision.kind = 'return'
        decision.return_expr = each
        proc.content.start.transition.terminator = decision
        proc.content.start.terminators = [decision]
        proc.content.start.transition.terminators = [decision]
        process.content.inner_procedures.append(proc)
        idx += 1

    opengeode.AdaGenerator.generate(process,
                                    simu=simu,
                                    ppty_check=orig_name if not simu else "")

    # gather asn.1 files and modules
    asn1_files = ' '.join(ast[0].asn1_filenames)
    asn1_modules_o = ' '.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_o))

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')
    parser.add_argument('-d', '--no_dll', action='store_true', default=False,
                      help='Generate standalone Ada code (not for DLL use)')
    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))

    try:
        parse_input_files(options.models, options.spec, not options.no_dll)
    except IOError as err:
        log.error(str(err))

    return 0

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