Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / modules / zustre @ b406445c

History | View | Annotate | Download (4.61 KB)

1
#!/usr/bin/env python
2

    
3
import sys
4
import os
5
import os.path
6
import threading
7
from multiprocessing import Process, Pool
8
import multiprocessing
9

    
10

    
11
def parseArgs (argv):
12
    import argparse as a
13
    p = a.ArgumentParser (description='\t Zustre: A fully automated verification and contract generation engine for Lustre Programs')
14

    
15
    p.add_argument ('file', metavar='BENCHMARK', help='Benchmark file')
16
    p.add_argument ('--pp',
17
                    help='Enable default pre-processing',
18
                    action='store_true', default=False)
19
    p.add_argument ('--trace', help='Trace levels to enable',
20
                   default='')
21
    p.add_argument ('--stat', help='Print Spacer statistics', dest="stat",
22
                    default=False, action='store_true')
23
    p.add_argument ('--verbose', help='Verbose', action='store_true',
24
                    default=False, dest="verbose")
25
    p.add_argument ('--spacer_verbose', help='Spacer Verbose', action='store_true', default= False, dest='spacer_verbose')
26
    p.add_argument ('--no-simp', help='Z3 simplification', action='store_false',
27
                    default=True, dest="simp")
28
    p.add_argument ('--invs', help='Additional invariants', default=None)
29
    p.add_argument ('--node', help='Specify top node (default:top)'
30
                    , dest='node', default="top")
31
    p.add_argument ('--cg', dest='cg', default=False, action='store_true',
32
                    help='Generate CoCoSpec Contract')
33
    p.add_argument ('--ri', dest='ri', default=False, action='store_true',
34
                    help='Get Raw Invariants')
35
    p.add_argument ('--smt2', dest='smt2', default=False, action='store_true',
36
                    help='Directly encoded file in SMT2 Format')
37
    p.add_argument ('--to-smt', dest='tosmt', default=False, action='store_true',
38
                       help='Print Horn Clause in SMT Format')
39
    p.add_argument ('--no-solving', dest='no_solving', default=False, action='store_true',
40
                    help='Generate only Horn clauses, i.e. do not solve')
41
    p.add_argument ('--validate', help='Validate generated contract with Kind2', action='store_true',
42
                    default=False, dest="kind2")
43
    p.add_argument ('--xml', help='Output result in XML format', action='store_true',
44
                    default=False, dest="xml")
45
    p.add_argument ('--save', help='Save intermediate files', action='store_true',
46
                    default=False, dest="save")
47
    p.add_argument ('--no-dl', help='Disable Difference Logic (UTVPI) in SPACER', action='store_true',
48
                    default=False, dest="utvpi")
49
    p.add_argument ('--reg-test', help='Run regression tests', action='store_true',
50
                      default=False, dest="regTest")
51
    p.add_argument ('--timeout', help='Timeout',
52
                    type=float, default=20.0, dest="timeout")
53
    p.add_argument ('--s-func', help='S-Function', default=None, dest="sfunction")
54
    p.add_argument ('--eldarica', help='Use Eldarica', default =False, action='store_true', dest="eldarica")
55
    p.add_argument ('--stateflow', help='Cex for Stateflow', default =False, action='store_true', dest="stateflow")
56
    pars = p.parse_args (argv)
57
    return pars
58

    
59

    
60
def stat (key, val): stats.put (key, val)
61

    
62

    
63
def main (args):
64
    from zustre import Zustre
65
    import z3
66
    stat ('Result', 'UNKNOWN')
67
    ctx = z3.Context ()
68
    fp = z3.Fixedpoint (ctx=ctx)
69
    zus = Zustre(args,ctx,fp)
70
    if args.no_solving:
71
        zus.encode()
72
    elif args.sfunction:
73
        zus.sFunction()
74
    elif args.eldarica:
75
        zus.eldarica()
76
    else:
77
        zus.encodeAndSolve()
78

    
79

    
80
if __name__ == '__main__':
81
     # unbuffered output
82
    sys.stdout = os.fdopen (sys.stdout.fileno (), 'w', 0)
83
    path = os.path.abspath (sys.argv[0])
84
    path = os.path.dirname(path)
85

    
86
    ## update system PATH to location of the package
87
    if os.path.isdir (path):
88
        os.environ['PATH'] = path + os.pathsep + os.environ['PATH']
89

    
90
    path = os.path.abspath (os.path.join(path, '..', 'lib', 'zustrepy', 'src'))
91
    if os.path.isdir (path): sys.path.insert(0, path)
92
    z3_path = os.path.abspath (os.path.join(path, '..', '..', '..', 'lib', 'z3py'))
93
    if os.path.isdir (z3_path):   sys.path.insert(0, z3_path)
94
    import stats
95
    args = parseArgs(sys.argv[1:])
96
    try:
97
        p = multiprocessing.Process(target=main, args=(args,))
98
        p.start()
99
        p.join(args.timeout)
100
        if p.is_alive():
101
            stat('Result','TIMEOUT')
102
            if args.xml:
103
                stats.xml_print(args.node, None, None, True)
104
            else:
105
                stats.brunch_print()
106
            p.terminate()
107
            p.join()
108
        #main (args)
109
    except Exception as e:
110
        print str(e)