Skip to content

Commit f9036d5

Browse files
ehildenbrv-jenkins
ehildenb
authored and
rv-jenkins
committed
Factor out sub-functions in kore-json for readability (#601)
* kore-json: factor out `print_int` * kore-json: factor out print_string * kore-json: factor out print_sort_injection * kore-json: factor out print_k_config_var * kore-json: print_klabel handles the closing parens * kore-json: break up writing injections into constituent parts * kore-json: replace manual prints of sort injections with print_sort_injection * kore-json: factor out print_config_map_entry * kevm: formatting * Makefile: formatting
1 parent 6f79bef commit f9036d5

File tree

3 files changed

+57
-24
lines changed

3 files changed

+57
-24
lines changed

‎Makefile

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -397,17 +397,23 @@ tests/ethereum-tests/VMTests/%: KEVM_MODE=VMTESTS
397397
tests/ethereum-tests/VMTests/%: KEVM_SCHEDULE=DEFAULT
398398

399399
tests/%.run: tests/%
400-
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) $(TEST) interpret $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
400+
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) \
401+
$(TEST) interpret $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) \
402+
$< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
401403
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
402404
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
403405

404406
tests/%.run-interactive: tests/%
405-
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) $(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
407+
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) \
408+
$(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) \
409+
$< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
406410
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
407411
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
408412

409413
tests/%.run-expected: tests/% tests/%.expected
410-
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) $(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
414+
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) \
415+
$(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) \
416+
$< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
411417
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/$*.expected
412418
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
413419

‎kevm

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,10 @@ run_krun() {
4141
ocaml) args=(--interpret) ;;
4242
*) args=() ;;
4343
esac
44-
krun --directory "$backend_dir" -cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' -cMODE="$cMODE" -pMODE='printf %s' "$run_file" "${args[@]-}" "$@"
44+
krun --directory "$backend_dir" \
45+
-cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' \
46+
-cMODE="$cMODE" -pMODE='printf %s' \
47+
"$run_file" "${args[@]-}" "$@"
4548
}
4649

4750
run_kast() {
@@ -175,9 +178,12 @@ run_interpret() {
175178
ocaml) run_kast kast > "$kast"
176179
output_format='kast'
177180
if $debug; then debugger=ocamldebug; fi
178-
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" -c PGM "$kast" textfile \
179-
-c SCHEDULE "$cSCHEDULE" text -c MODE "$cMODE" text --initializer 'initKevmCell' \
180-
--output-file "$output" "$@" \
181+
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" \
182+
-c PGM "$kast" textfile \
183+
-c SCHEDULE "$cSCHEDULE" text \
184+
-c MODE "$cMODE" text \
185+
--initializer 'initKevmCell' \
186+
--output-file "$output" "$@" \
181187
|| exit_status="$?"
182188
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
183189
k-bin-to-text "$output" "$output_text"

‎kore-json.py

Lines changed: 38 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,25 @@
1212
def escape(data):
1313
return data.encode('unicode_escape')
1414

15-
def print_kast(data, sort="SortJSON"):
15+
def print_int(data):
16+
sys.stdout.write("\dv{SortInt{}}(\"")
17+
sys.stdout.write(data)
18+
sys.stdout.write("\")")
19+
20+
def print_string(data):
21+
sys.stdout.write("\dv{SortString{}}(")
22+
sys.stdout.write(json.dumps(data))
23+
sys.stdout.write(")")
24+
25+
def print_k_config_var(data):
26+
sys.stdout.write("\dv{SortKConfigVar{}}(\"$" + data + "\")")
27+
28+
def print_sort_injection(s1, s2, data, printer):
29+
sys.stdout.write("inj{Sort" + s1 + "{}, " + "Sort" + s2 + "{}}(")
30+
printer(data)
31+
sys.stdout.write(")")
32+
33+
def print_kast(data, sort="JSON"):
1634
if isinstance(data, list):
1735
sys.stdout.write("LblJSONList{}(")
1836
for elem in data:
@@ -27,7 +45,7 @@ def print_kast(data, sort="SortJSON"):
2745
sys.stdout.write("LblJSONObject{}(")
2846
for key, value in data.items():
2947
sys.stdout.write("LblJSONs{}(LblJSONEntry{}(")
30-
print_kast(key, "SortJSONKey")
48+
print_kast(key, sort = "JSONKey")
3149
sys.stdout.write(',')
3250
print_kast(value)
3351
sys.stdout.write('),')
@@ -36,26 +54,29 @@ def print_kast(data, sort="SortJSON"):
3654
sys.stdout.write(')')
3755
sys.stdout.write(')')
3856
elif isinstance(data, str) or isinstance(data, unicode):
39-
sys.stdout.write("inj{SortString{}, " + sort + "{}}(\dv{SortString{}}("),
40-
sys.stdout.write(json.dumps(data))
41-
sys.stdout.write('))')
57+
print_sort_injection("String", sort, data, print_string)
4258
elif isinstance(data, long) or isinstance(data, int):
43-
sys.stdout.write("inj{SortInt{}, " + sort + '{}}(\dv{SortInt{}}("'),
44-
sys.stdout.write(str(data))
45-
sys.stdout.write('"))')
59+
print_sort_injection("Int", sort, data, print_int)
4660
else:
4761
sys.stdout.write(type(data))
4862
raise AssertionError
4963

5064
def print_klabel(s):
51-
sys.stdout.write("Lbl" + s.replace("_", "'Unds'").replace("`", "").replace("(.KList)", "{}") + " ")
52-
53-
sys.stdout.write("LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(\"$PGM\")),inj{SortJSON{}, SortKItem{}}( ")
54-
print_kast(data)
55-
sys.stdout.write("))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(\"$SCHEDULE\")),inj{SortSchedule{}, SortKItem{}}( ")
56-
print_klabel(sys.argv[2])
57-
sys.stdout.write("()))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(\"$MODE\")),inj{SortMode{}, SortKItem{}}( ")
58-
print_klabel(sys.argv[3])
59-
sys.stdout.write("()))))\n")
65+
sys.stdout.write("Lbl" + s.replace("_", "'Unds'").replace("`", "").replace("(.KList)", "{}") + "()")
66+
67+
def print_config_map_entry(k, v, vsort, vprint):
68+
sys.stdout.write("Lbl'UndsPipe'-'-GT-Unds'{}(")
69+
print_sort_injection("KConfigVar", "KItem", k, print_k_config_var)
70+
sys.stdout.write(",")
71+
print_sort_injection(vsort, "KItem", v, vprint)
72+
sys.stdout.write(")")
73+
74+
sys.stdout.write("LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),")
75+
print_config_map_entry("PGM", data, "JSON", print_kast)
76+
sys.stdout.write("),")
77+
print_config_map_entry("SCHEDULE", sys.argv[2], "Schedule", print_klabel)
78+
sys.stdout.write("),")
79+
print_config_map_entry("MODE", sys.argv[3], "Mode", print_klabel)
80+
sys.stdout.write("))\n")
6081
sys.stdout.write("\n")
6182
sys.stdout.flush()

0 commit comments

Comments
 (0)