Skip to content

Commit

Permalink
Factor out sub-functions in kore-json for readability (#601)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@ehildenb @rv-jenkins
ehildenb authored and rv-jenkins committed Dec 5, 2019
1 parent 6f79bef commit f9036d5
Show file tree
Hide file tree
Showing 3 changed files with 57 additions and 24 deletions.
12 changes: 9 additions & 3 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -397,17 +397,23 @@ tests/ethereum-tests/VMTests/%: KEVM_MODE=VMTESTS
tests/ethereum-tests/VMTests/%: KEVM_SCHEDULE=DEFAULT

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

tests/%.run-interactive: tests/%
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) $(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) \
$(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) \
$< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out

tests/%.run-expected: tests/% tests/%.expected
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) $(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
MODE=$(KEVM_MODE) SCHEDULE=$(KEVM_SCHEDULE) \
$(TEST) run $(TEST_OPTIONS) --backend $(TEST_CONCRETE_BACKEND) \
$< > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/$*.expected
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out

Expand Down
14 changes: 10 additions & 4 deletions kevm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,10 @@ run_krun() {
ocaml) args=(--interpret) ;;
*) args=() ;;
esac
krun --directory "$backend_dir" -cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' -cMODE="$cMODE" -pMODE='printf %s' "$run_file" "${args[@]-}" "$@"
krun --directory "$backend_dir" \
-cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' \
-cMODE="$cMODE" -pMODE='printf %s' \
"$run_file" "${args[@]-}" "$@"
}

run_kast() {
Expand Down Expand Up @@ -175,9 +178,12 @@ run_interpret() {
ocaml) run_kast kast > "$kast"
output_format='kast'
if $debug; then debugger=ocamldebug; fi
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" -c PGM "$kast" textfile \
-c SCHEDULE "$cSCHEDULE" text -c MODE "$cMODE" text --initializer 'initKevmCell' \
--output-file "$output" "$@" \
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" \
-c PGM "$kast" textfile \
-c SCHEDULE "$cSCHEDULE" text \
-c MODE "$cMODE" text \
--initializer 'initKevmCell' \
--output-file "$output" "$@" \
|| exit_status="$?"
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
k-bin-to-text "$output" "$output_text"
Expand Down
55 changes: 38 additions & 17 deletions kore-json.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,25 @@
def escape(data):
return data.encode('unicode_escape')

def print_kast(data, sort="SortJSON"):
def print_int(data):
sys.stdout.write("\dv{SortInt{}}(\"")
sys.stdout.write(data)
sys.stdout.write("\")")

def print_string(data):
sys.stdout.write("\dv{SortString{}}(")
sys.stdout.write(json.dumps(data))
sys.stdout.write(")")

def print_k_config_var(data):
sys.stdout.write("\dv{SortKConfigVar{}}(\"$" + data + "\")")

def print_sort_injection(s1, s2, data, printer):
sys.stdout.write("inj{Sort" + s1 + "{}, " + "Sort" + s2 + "{}}(")
printer(data)
sys.stdout.write(")")

def print_kast(data, sort="JSON"):
if isinstance(data, list):
sys.stdout.write("LblJSONList{}(")
for elem in data:
Expand All @@ -27,7 +45,7 @@ def print_kast(data, sort="SortJSON"):
sys.stdout.write("LblJSONObject{}(")
for key, value in data.items():
sys.stdout.write("LblJSONs{}(LblJSONEntry{}(")
print_kast(key, "SortJSONKey")
print_kast(key, sort = "JSONKey")
sys.stdout.write(',')
print_kast(value)
sys.stdout.write('),')
Expand All @@ -36,26 +54,29 @@ def print_kast(data, sort="SortJSON"):
sys.stdout.write(')')
sys.stdout.write(')')
elif isinstance(data, str) or isinstance(data, unicode):
sys.stdout.write("inj{SortString{}, " + sort + "{}}(\dv{SortString{}}("),
sys.stdout.write(json.dumps(data))
sys.stdout.write('))')
print_sort_injection("String", sort, data, print_string)
elif isinstance(data, long) or isinstance(data, int):
sys.stdout.write("inj{SortInt{}, " + sort + '{}}(\dv{SortInt{}}("'),
sys.stdout.write(str(data))
sys.stdout.write('"))')
print_sort_injection("Int", sort, data, print_int)
else:
sys.stdout.write(type(data))
raise AssertionError

def print_klabel(s):
sys.stdout.write("Lbl" + s.replace("_", "'Unds'").replace("`", "").replace("(.KList)", "{}") + " ")

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{}}( ")
print_kast(data)
sys.stdout.write("))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(\"$SCHEDULE\")),inj{SortSchedule{}, SortKItem{}}( ")
print_klabel(sys.argv[2])
sys.stdout.write("()))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(\"$MODE\")),inj{SortMode{}, SortKItem{}}( ")
print_klabel(sys.argv[3])
sys.stdout.write("()))))\n")
sys.stdout.write("Lbl" + s.replace("_", "'Unds'").replace("`", "").replace("(.KList)", "{}") + "()")

def print_config_map_entry(k, v, vsort, vprint):
sys.stdout.write("Lbl'UndsPipe'-'-GT-Unds'{}(")
print_sort_injection("KConfigVar", "KItem", k, print_k_config_var)
sys.stdout.write(",")
print_sort_injection(vsort, "KItem", v, vprint)
sys.stdout.write(")")

sys.stdout.write("LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),")
print_config_map_entry("PGM", data, "JSON", print_kast)
sys.stdout.write("),")
print_config_map_entry("SCHEDULE", sys.argv[2], "Schedule", print_klabel)
sys.stdout.write("),")
print_config_map_entry("MODE", sys.argv[3], "Mode", print_klabel)
sys.stdout.write("))\n")
sys.stdout.write("\n")
sys.stdout.flush()

0 comments on commit f9036d5

Please sign in to comment.