Skip to content

Commit b2fb1ea

Browse files
ehildenbehildenb
authored
Automatically generate symbol table from JSON definition (runtimeverification#807)
* k-distribution/pyk/kastManip: dont need to prefix with pyk * k-distribution/pyk/kast: generic unparser based on reading in json definition * k-distribution/tests/pyk: update to use new generic unparsing * Makefile: make sure --emit-json is passed
1 parent 7dcbd76 commit b2fb1ea

4 files changed

Lines changed: 41 additions & 62 deletions

File tree

‎k-distribution/src/main/scripts/lib/pyk/kast.py‎

Lines changed: 29 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -216,53 +216,35 @@ def _underbarUnparsing(*args):
216216
def indent(input):
217217
return "\n".join([" " + l for l in input.split("\n")])
218218

219-
K_builtin_labels = { klabelCells : (lambda *args: "\n".join(args))
220-
, klabelEmptyK : (lambda : ".")
221-
}
222-
223-
BOOL_expressions = { "_andBool_" : binOpStr("\nandBool")
224-
, "_orBool_" : paren(binOpStr("orBool"))
225-
, "notBool_" : (lambda a: "notBool " + a)
226-
, "_==K_" : binOpStr("==K")
227-
}
228-
229-
INT_predicates = { "_<Int_" : binOpStr("<Int")
230-
, "_>Int_" : binOpStr(">Int")
231-
, "_<=Int_" : binOpStr("<=Int")
232-
, "_>=Int_" : binOpStr(">=Int")
233-
, "_==Int_" : binOpStr("==Int")
234-
, "_=/=Int_" : binOpStr("=/=Int")
235-
}
236-
237-
INT_expressions = { "_+Int_" : paren(binOpStr("+Int"))
238-
, "_-Int_" : paren(binOpStr("-Int"))
239-
, "_*Int_" : paren(binOpStr("*Int"))
240-
, "_/Int_" : paren(binOpStr("-Int"))
241-
, "_modInt_" : paren(binOpStr("modInt"))
242-
, "_&Int_" : paren(binOpStr("&Int"))
243-
, "_|Int_" : paren(binOpStr("|Int"))
244-
, "_xorInt_" : paren(binOpStr("xorInt"))
245-
, "_>>Int_" : paren(binOpStr(">>Int"))
246-
}
247-
248-
MAP_expressions = { "Map:update" : paren(underbarUnparsing("_[_<-_]"))
249-
, "Map:lookup" : paren(underbarUnparsing("_[_]"))
250-
, "_Map_" : lambda m1, m2: m1 + "\n" + m2 if m2 != ".Map" else m1
251-
, "_|->_" : underbarUnparsing("_|->_")
252-
, "_[_<-undef]" : paren(underbarUnparsing("_[_ <- undef ]"))
253-
, ".Map" : constLabel(".Map")
254-
}
255-
256-
LIST_expressions = { "_List_" : (lambda a1, a2: a1 + " " + a2)
257-
, "ListItem" : appliedLabelStr("ListItem")
258-
}
259-
260-
SET_expressions = { "Set:in" : binOpStr("in")
261-
, "_Set_" : (lambda a1, a2: a1 + " " + a2)
262-
, "SetItem" : appliedLabelStr("SetItem")
263-
}
264-
265-
K_symbols = combineDicts(K_builtin_labels, BOOL_expressions, INT_predicates, INT_expressions, MAP_expressions, LIST_expressions, SET_expressions)
219+
def buildSymbolTable(definition):
220+
"""Build the unparsing symbol table given a JSON encoded definition.
221+
222+
- Input: JSON encoded K definition.
223+
- Return: Python dictionary mapping klabels to automatically generated unparsers.
224+
"""
225+
if not isKDefinition(definition):
226+
_fatal('Must supply a KDefinition!')
227+
228+
def _unparserFromProductionItems(prodItems):
229+
unparseString = ""
230+
for prodItem in prodItems:
231+
if isKTerminal(prodItem):
232+
unparseString += prodItem['value']
233+
elif isKNonTerminal(prodItem):
234+
unparseString += '_'
235+
return underbarUnparsing(unparseString)
236+
237+
symbolTable = { }
238+
for module in definition['modules']:
239+
for sent in module['localSentences']:
240+
if isKProduction(sent) and 'klabel' in sent:
241+
label = sent['klabel']
242+
if 'symbol' in sent['att']['att'] and 'klabel' in sent['att']['att']:
243+
label = sent['att']['att']['klabel']
244+
unparser = _unparserFromProductionItems(sent['productionItems'])
245+
symbolTable[label] = unparser
246+
247+
return symbolTable
266248

267249
def prettyPrintKast(kast, symbolTable):
268250
if kast is None or kast == {}:

‎k-distribution/src/main/scripts/lib/pyk/kastManip.py‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -132,13 +132,13 @@ def splitConfigFrom(configuration):
132132
initial_substitution = {}
133133
_mkCellVar = lambda label: label.replace('-', '_').replace('<', '').replace('>', '').upper() + '_CELL'
134134
def _replaceWithVar(k):
135-
if pyk.isKApply(k) and pyk.isCellKLabel(k['label']):
136-
if len(k['args']) == 1 and not (pyk.isKApply(k['args'][0]) and pyk.isCellKLabel(k['args'][0]['label'])):
135+
if isKApply(k) and isCellKLabel(k['label']):
136+
if len(k['args']) == 1 and not (isKApply(k['args'][0]) and isCellKLabel(k['args'][0]['label'])):
137137
config_var = _mkCellVar(k['label'])
138138
initial_substitution[config_var] = k['args'][0]
139139
return KApply(k['label'], [KVariable(config_var)])
140140
return k
141-
symbolic_config = pyk.traverseBottomUp(configuration, _replaceWithVar)
141+
symbolic_config = traverseBottomUp(configuration, _replaceWithVar)
142142
return (symbolic_config, initial_substitution)
143143

144144
def collapseDots(kast):

‎k-distribution/tests/pyk/Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,9 @@ clean:
2121
imp_kompiled:=imp-kompiled/compiled.txt
2222

2323
$(imp_kompiled): imp.k $(KOMPILE)
24-
$(KOMPILE) --backend $(KOMPILE_BACKEND) -I . $<
24+
$(KOMPILE) --backend $(KOMPILE_BACKEND) -I . $< --emit-json
2525

26-
kast-tests/%.gen: build-config.py kast-tests/%.json
26+
kast-tests/%.gen: build-config.py kast-tests/%.json $(imp_kompiled)
2727
python3 $^ > $@
2828

2929
proof-tests/%-spec.k: build-config.py proof-tests/%-spec.json

‎k-distribution/tests/pyk/build-config.py‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,14 @@
55
from functools import reduce
66

77
# From K's pyk-library
8-
from pyk.kast import *
9-
from pyk.kastManip import *
8+
from pyk import *
109

11-
IMP_symbols = { 'int_;_' : (lambda ds, ss : 'int ' + ds + ';\n' + ss)
12-
, '_,_' : assocWithUnit(' , ', '.Ids')
13-
, '.List{"_,_"}' : constLabel('.Ids')
14-
, '{}' : constLabel('{ }')
15-
, '_+_' : binOpStr('+')
16-
}
10+
IMP_definition = readKastTerm('imp-kompiled/compiled.json')
1711

18-
ALL_symbols = combineDicts(K_symbols, IMP_symbols)
12+
IMP_symbols = buildSymbolTable(IMP_definition)
13+
14+
IMP_symbols['_,_'] = assocWithUnit(' , ', '')
15+
IMP_symbols['.List{"_,_"}'] = constLabel('')
1916

2017
kast_term = readKastTerm(sys.argv[1])
2118

@@ -27,4 +24,4 @@
2724
elif isKApply(kast_term):
2825
kast_term = simplifyBool(kast_term)
2926

30-
print(prettyPrintKast(kast_term, ALL_symbols))
27+
print(prettyPrintKast(kast_term, IMP_symbols))

0 commit comments

Comments
 (0)