-
Notifications
You must be signed in to change notification settings - Fork 0
/
buildtools.py
164 lines (143 loc) · 7.12 KB
/
buildtools.py
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
48
49
50
51
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
from kninja import *
from kninja.runner import KRunner
import copy
import functools
import subprocess
import re
import sys
# Customize KDefinition For Hybrid Program Semantics
# ==============================================
class KHPDefinition(KDefinition):
def synthesis(self, expected = None, inputs = [], implicit_inputs = [], glob = None, alias = None, default = True, flags = ''):
if glob is not None:
inputs += glob_module.glob(glob)
ret = []
for input in inputs:
e = expected
if e is None:
e = append_extension(input, 'cond.expected')
input = self.proj.to_target(input)
test = input.then(self.runner_script(mode = 'synthesis', flags = flags).implicit(implicit_inputs)) \
.then(self.proj.check(expected = e))
if default: test.default()
ret += [test]
if alias is not None:
ret = self.proj.alias(alias, ret)
return ret
class KHPProject(KProject):
def definition( self
, alias
, backend
, main
, runner_script
, other = []
, directory = None
, tangle_selector = '.k'
, flags = ''
):
if directory is None:
directory = self.builddir('defn', alias)
# If a source file has extension '.md', tangle it:
def target_from_source(source):
source = self.to_target(source)
assert(type(source) == Target)
source = self.tangle_if_markdown( source
, selector = tangle_selector
, directory = directory
)
return source
main = target_from_source(main)
other = map(target_from_source, other)
kompiled_dir = os.path.join(directory, basename_no_ext(main.path) + '-kompiled')
output = None
env = ''
implicit_inputs = [self.build_k(backend)]
if backend == 'ocaml':
output = os.path.join(kompiled_dir, 'interpreter')
implicit_inputs += [self.configure_opam()]
env = 'opam config exec --'
elif backend == 'llvm':
output = os.path.join(kompiled_dir, 'interpreter')
elif backend == 'java':
output = os.path.join(kompiled_dir, 'timestamp')
elif backend == 'haskell':
output = os.path.join(kompiled_dir, 'definition.kore')
else:
assert false, 'Unknown backend "' + backend + "'"
target = main.then(self.rule_kompile() \
.output(output) \
.implicit(other) \
.implicit(implicit_inputs) \
.variable('backend', backend) \
.variable('directory', directory) \
.variable('env', env) \
.variable('flags', '-I ' + directory + ' ' + flags) \
).alias(alias)
return KHPDefinition( self, alias, directory, kompiled_dir, target
, runner_script = runner_script
, krun_extension = alias + '-krun', krun_env = env
, kprove_extension = alias + '-kprove'
, backend = backend
)
# Customize KRunner For Hybrid Program Semantics
# ==============================================
class KHPRunner(KRunner):
def __init__(self, proj, default_definition = None):
self.parser = argparse.ArgumentParser()
self.proj = proj
parser = self.parser
self.default_definition = default_definition
parser.add_argument('--opamswitch', default = '4.06.1+k')
subparsers = parser.add_subparsers()
kast_parser = subparsers.add_parser('kast', help = 'Run a program against a definition')
self.add_definition_argument(kast_parser)
kast_parser.add_argument('program', help = 'Path to program')
kast_parser.add_argument('args', nargs = argparse.REMAINDER, help = 'Arguments to pass to K')
kast_parser.set_defaults(func = functools.partial(self.execute_kast, self))
run_parser = subparsers.add_parser('run', help = 'Run a program against a definition')
self.add_definition_argument(run_parser)
run_parser.add_argument('program', help = 'Path to program')
run_parser.add_argument('args', nargs = argparse.REMAINDER, help = 'Arguments to pass to K')
run_parser.set_defaults(func = functools.partial(self.execute_krun, self))
prove_parser = subparsers.add_parser('prove', help = 'Use KProve to check a specification')
self.add_definition_argument(prove_parser)
prove_parser.add_argument('specification', help = 'Path to spec')
prove_parser.add_argument('args', nargs = argparse.REMAINDER, help = 'Arguments to pass to K')
prove_parser.set_defaults(func = functools.partial(self.execute_kprove, self))
synthesis_parser = subparsers.add_parser('synthesis', help = 'Use Symbolic Execution to Synthesize Constraints')
self.add_definition_argument(synthesis_parser)
synthesis_parser.add_argument('program', help = 'Path to program')
synthesis_parser.add_argument('args', nargs = argparse.REMAINDER, help = 'Arguments to pass to K')
synthesis_parser.set_defaults(func = functools.partial(self.execute_synthesis, self))
def execute_synthesis(self, args):
definition = self.proj._k_definitions[args.definition]
binary = self.proj.kbindir('krun')
process_args = []
opam_config_exec = []
if definition.backend == 'ocaml':
opam_config_exec = ['opam', 'config', 'exec', '--']
binary = 'opam'
process_args = opam_config_exec \
+ [ self.proj.kbindir('krun') \
, '--directory', definition.directory()
, args.program
, '-cMODE=\"#constraintSynthesis\"'] \
+ self.proj._k_definitions[args.definition]._krun_flags.split() \
+ args.args
result = subprocess.run( process_args
, stdout = subprocess.PIPE
, stderr = subprocess.PIPE
, check = True)
if(result.returncode == 0):
pattern = re.compile(r'#constraints\s*\(\s*\"(.*).*\"\s*\)', re.DOTALL)
matches = re.search(pattern, str(result.stdout))
if matches == None:
print(result.stdout, file = sys.stderr)
sys.exit(1)
else:
output = matches.group(1)
output = re.sub(r'\\\\n$', '', output) #weird newline at end
print(output)
else:
print(result.stderr, file = sys.stderr)
sys.exit(result.returncode)