-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathkmich
executable file
·200 lines (164 loc) · 6.95 KB
/
kmich
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
#!/usr/bin/env bash
set -euo pipefail
shopt -s extglob
notif() { echo "== $@" >&2 ; }
fatal() { echo "[FATAL] $@" ; exit 1 ; }
scriptpath="$( cd "$(dirname "$0")" >/dev/null 2>&1 ; pwd -P )"
kmich_dir="${KMICH_DIR:-$scriptpath}"
build_dir="$kmich_dir/.build"
defn_dir="${KMICH_DEFN_DIR:-$build_dir/defn}"
lib_dir="$build_dir/local/lib"
k_release_dir="${K_RELEASE:-$kmich_dir/ext/k/k-distribution/target/release/k}"
if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then
if which kompile &> /dev/null; then
k_release_dir="$(dirname $(which kompile))/.."
else
fatal "Cannot find K Installation!"
fi
fi
PATH="$scriptpath/lib:$k_release_dir/bin:$PATH"
export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}"
export PYTHONPATH="$k_release_dir/lib/kframework:${PYTHONPATH:-}"
# Runners
# -------
# User Commands
run_krun() {
export K_OPTS=-Xss500m
krun --directory "$backend_dir" "$run_file" "${extra_args[@]}" "$@"
}
run_kast() {
local output_mode
[[ $# -lt 1 ]] && fatal "kast: no output mode provided"
output_mode="$1" ; shift
! $debug || set -x
kast --directory "$backend_dir" "$run_file" --output "$output_mode" "${extra_args[@]}" "$@"
}
run_prove() {
local def_module
[[ $# -lt 1 ]] && fatal "prove: no definition module provided"
def_module="$1" ; shift
additional_proof_args=()
! $debug || additional_proof_args+=(--debug)
! $repl || additional_proof_args+=(--debugger --debug-script ./lib/kast-$backend.kscript)
export K_OPTS=-Xmx8G
! $debug || set -x
kprove-legacy --directory "$backend_dir" "$run_file" --def-module "$def_module" "${additional_proof_args[@]}" "${extra_args[@]}" "$@"
}
run_interpret() {
krun --directory "$backend_dir" "$run_file" "${extra_args[@]}" "$@"
}
run_symbtest() {
output="--output none"
! $debug || { set -x; output=""; }
export K_OPTS=-Xss500m
krun --directory "$backend_dir" \
-cInputFilename="\"$run_file\"" \
-cDefnDir="\"$defn_dir\"" \
$output \
"${extra_args[@]}" \
"$@"
}
run_cfg() {
if $(which python3 &> /dev/null); then
python_bin=python3
else
python_bin=python
fi
"$python_bin" "$kmich_dir/ext/tezos-utils/tezos-utils" convert -i michelson -o dot "$@" -- "$run_file" -
}
# Main
# ----
[[ $# -gt 0 ]] && { run_command="$1" ; shift ; }
if [[ "$run_command" == 'version' ]] || [[ "$run_command" == '--version' ]]; then
notif "KMich Version"
git rev-parse --short HEAD
notif "K Version"
kompile --version
notif "Kore Version"
kore-exec --version
notif "Z3 Version"
z3 --version
exit 0
fi
if [[ $# -le 0 ]] || [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
echo "
usage: $0 run [--backend (llvm|symbolic|contract-expander|extractor|input-creator|output-compare)] <pgm> <K arg>*
$0 kast [--backend (llvm|symbolic|contract-expander|extractor|input-creator|output-compare)] <pgm> <output format> <K arg>*
$0 symbtest <pgm> <K arg>*
$0 prove [--backend (symbolic|prove|dexter|lqt|lb)] <spec> <def_module> <K arg>*
$0 interpret [--backend (llvm|symbolic|contract-expander|extractor|input-creator|output-compare)] <pgm> <LLVM KRun arg>*
$0 cfg <pgm>
$0 [help|--help|version|--version]
$0 run : Run a single Michelson program.
$0 kast : Parse a Michelson program and output it in a supported format.
$0 symbtest : Run a Michelson symbolic test.
$0 prove : Run a Michelson K proof.
$0 interpret : Run a single Michelson program using the fast bison parser.
$0 cfg : Build a control flow graph corresponding to a Michelson program
$0 help : Display this help message.
$0 version : Display the versions of KMichelson, K, Kore, and Z3 in use.
Note: <pgm> is a path to a file containing an EVM program/test.
<spec> is a K specification to be proved.
<K arg> is an argument you want to pass to K.
<LLVM KRun arg> are arguments to pass to llvm-krun.
<output format> is the format for Kast to output the term in.
<def_module> is the module to take as axioms when doing verification.
"
exit 0
fi
backend="llvm"
debug=false
repl=false
virtual_backend=false
[[ ! "$run_command" == 'prove' ]] || backend='prove'
[[ ! "$run_command" == 'symbtest' ]] || backend='driver'
[[ ! "$run_command" == 'cfg' ]] || backend='virtual'
args=()
while [[ $# -gt 0 ]]; do
arg="$1"
case $arg in
--backend) backend="$2" ; shift 2 ;;
--backend-dir) backend_dir="$2" ; shift 2 ;;
--repl) repl=true ; shift ;;
--debug) debug=true ; shift ;;
--) break ; shift ;;
*) args+=("$1") ; shift ;;
esac
done
set -- "${args[@]}" "$@"
if [ "$backend" != "virtual" ]; then
backend_dir="${backend_dir:-$defn_dir/$backend}"
kompiled_dir=$(find $backend_dir -name '*-kompiled')
[[ -d "$kompiled_dir" ]] || fatal "Could not find single *-kompiled directory in $backend_dir"
fi
! $repl || \
[[ "$backend" == dexter ]] || \
[[ "$backend" == lb ]] || \
[[ "$backend" == lqt ]] || \
[[ "$backend" == prove ]] || \
fatal 'Option --repl only usable with `--backend` values `prove`, `dexter`, `lb`, or `lqt` !'
# get the run file
run_file="$1" ; shift
if [[ "$run_file" == '-' ]]; then
tmp_input="$(mktemp)"
trap "rm -rf $tmp_input" INT TERM EXIT
cat - > "$tmp_input"
run_file="$tmp_input"
fi
[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
extra_args=()
! $debug \
|| extra_args+=(--debug)
[[ ! "$backend" == "llvm" ]] \
|| extra_args+=(-cPATH="\"$(dirname $run_file)\"")
[ "$backend" == "virtual" ] || export PATH="$kompiled_dir:$PATH"
case "$run_command-$backend" in
# Running
run-@(llvm|prove|symbolic|contract-expander|extractor|input-creator|output-compare) ) run_krun "$@" ;;
kast-@(llvm|prove|symbolic|contract-expander|extractor|input-creator|output-compare) ) run_kast "$@" ;;
symbtest-driver ) run_symbtest "$@" ;;
prove-@(prove|symbolic|dexter|lb|lqt) ) run_prove "$@" ;;
interpret-@(llvm|prove|symbolic|contract-expander|extractor|input-creator|output-compare) ) run_interpret "$@" ;;
cfg-virtual ) run_cfg "$@" ;;
*) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;;
esac