Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upstreaming pyk functionality #2756

Merged
merged 10 commits into from
Jul 29, 2022
Merged

Upstreaming pyk functionality #2756

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
6be42a6
pyk/tests: move simplifyBool tests from integration to unit tests
ehildenb Jul 28, 2022
ccae8a5
pyk/Makefile: explicit options
ehildenb Jul 28, 2022
bb2e7e8
pyk/kast: add KDefinition.{production_for_klabel,production_for_cell_…
ehildenb Jul 28, 2022
9162734
pyk/kast: add KDefinition.module_names
ehildenb Jul 28, 2022
81924eb
pyk/kprint: SymbolTable is a Dict, not a Mapping
ehildenb Jul 28, 2022
99ebae0
pyk/: factor out build_claim from build_rule, with stronger typing
ehildenb Jul 28, 2022
b988e1f
pyk/: factor out class Bool in prelude
ehildenb Jul 28, 2022
d3d2e02
pyk/: rename simplifyBool => simplify_bool
ehildenb Jul 28, 2022
9903b8d
Update pyk/src/pyk/tests/test_kastManip.py
ehildenb Jul 28, 2022
72d9767
Merge branch 'master' into pyk-upstream
rv-jenkins Jul 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions pyk/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,10 +55,10 @@ install:
test: test-unit test-integration test-pyk

test-unit: $(VENV_DEV)
$(ACTIVATE_DEV) && python3 -m unittest discover -vt src pyk.tests
$(ACTIVATE_DEV) && python3 -m unittest discover --verbose --top src pyk.tests

test-integration: $(VENV_DEV)
$(ACTIVATE_DEV) && python3 -m unittest discover -vt src pyk.integration_tests
$(ACTIVATE_DEV) && python3 -m unittest discover --verbose --top src pyk.integration_tests

test-pyk: $(VENV_PROD)
$(ACTIVATE_PROD) && $(MAKE) -C pyk-tests
Expand Down
42 changes: 32 additions & 10 deletions pyk/src/pyk/integration_tests/test_defn.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,15 @@
KApply,
KClaim,
KRewrite,
KSort,
KToken,
KVariable,
assocWithUnit,
constLabel,
)
from ..kastManip import push_down_rewrites, simplifyBool
from ..kastManip import push_down_rewrites
from ..ktool import KompileBackend
from ..prelude import boolToken, intToken
from ..prelude import Sorts
from .kprove_test import KProveTest


Expand Down Expand Up @@ -75,15 +76,36 @@ def test_print_prove_rewrite(self):
self.assertEqual(minimized_claim_rewrite_expected, minimized_claim_rewrite_actual)
self.assertTop(result)

def test_bool_simplify(self):
def test_empty_config(self):
# Given
bool_test_1 = KApply('_andBool_', [boolToken(False), boolToken(True)])
bool_test_2 = KApply('_andBool_', [KApply('_==Int_', [intToken(3), intToken(4)]), boolToken(True)])
empty_config_generated_top = self.kprove.definition.empty_config(Sorts.GENERATED_TOP_CELL)
empty_config_t = self.kprove.definition.empty_config(KSort('TCell'))

# When
bool_test_1_simplified = simplifyBool(bool_test_1)
bool_test_2_simplified = simplifyBool(bool_test_2)
empty_config_generated_top_printed = '\n'.join([ '<generatedTop>' # noqa
, ' <T>' # noqa
, ' <k>' # noqa
, ' K_CELL' # noqa
, ' </k>' # noqa
, ' <state>' # noqa
, ' STATE_CELL' # noqa
, ' </state>' # noqa
, ' </T>' # noqa
, ' <generatedCounter>' # noqa
, ' GENERATEDCOUNTER_CELL' # noqa
, ' </generatedCounter>' # noqa
, '</generatedTop>' # noqa
]) # noqa

empty_config_t_printed = '\n'.join([ '<T>' # noqa
, ' <k>' # noqa
, ' K_CELL' # noqa
, ' </k>' # noqa
, ' <state>' # noqa
, ' STATE_CELL' # noqa
, ' </state>' # noqa
, '</T>' # noqa
]) # noqa

# Then
self.assertEqual(boolToken(False), bool_test_1_simplified)
self.assertEqual(KApply('_==Int_', [intToken(3), intToken(4)]), bool_test_2_simplified)
self.assertEqual(empty_config_generated_top_printed, self.kprove.pretty_print(empty_config_generated_top))
self.assertEqual(empty_config_t_printed, self.kprove.pretty_print(empty_config_t))
49 changes: 49 additions & 0 deletions pyk/src/pyk/kast.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1477,6 +1477,10 @@ def let(
def let_att(self, att: KAtt) -> 'KDefinition':
return self.let(att=att)

@property
def module_names(self) -> List[str]:
return [_m.name for _m in self.modules]

@property
def productions(self) -> List[KProduction]:
return [prod for module in self.modules for prod in module.productions]
Expand All @@ -1493,6 +1497,51 @@ def functions(self) -> List[KProduction]:
def constructors(self) -> List[KProduction]:
return [prod for module in self.modules for prod in module.constructors]

def production_for_klabel(self, klabel: KLabel) -> KProduction:
productions = [prod for prod in self.productions if prod.klabel and prod.klabel == klabel]
if len(productions) != 1:
raise ValueError(f'Expected 1 production for label {klabel}, not {productions}.')
return productions[0]

def production_for_cell_sort(self, sort: KSort) -> KProduction:
# Typical cell production has 3 productions:
# syntax KCell ::= "project:KCell" "(" K ")" [function, projection]
# syntax KCell ::= "initKCell" "(" Map ")" [function, initializer, noThread]
# syntax KCell ::= "<k>" K "</k>" [cell, cellName(k), format(%1%i%n%2%d%n%3), maincell, org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
# And it may have a 4th:
# syntax GeneratedCounterCell ::= "getGeneratedCounterCell" "(" GeneratedTopCell ")" [function]
# We want the actual label one (3rd one in the list).
if not sort.name.endswith('Cell'):
raise ValueError(f'Method production_for_cell_sort only intended to be called on sorts ending in "Cell", not: {sort}')
productions = [prod for prod in self.productions if prod.sort == sort and 'cell' in prod.att]
if len(productions) != 1:
raise ValueError(f'Expected 1 cell production for sort {sort}, not: {productions}')
return productions[0]

def empty_config(self, sort: KSort) -> KInner:

def _kdefinition_empty_config(_sort):
cell_prod = self.production_for_cell_sort(_sort)
cell_klabel = cell_prod.klabel
assert cell_klabel is not None
production = self.production_for_klabel(cell_klabel)
args = []
num_nonterminals = 0
num_freshvars = 0
for p_item in production.items:
if type(p_item) is KNonTerminal:
num_nonterminals += 1
if p_item.sort.name.endswith('Cell'):
args.append(_kdefinition_empty_config(p_item.sort))
else:
num_freshvars += 1
args.append(KVariable(_sort.name[0:-4].upper() + '_CELL'))
if num_nonterminals > 1 and num_freshvars > 0:
raise ValueError(f'Found mixed cell and non-cell arguments to cell constructor for: {sort}')
return KApply(cell_klabel, args)

return _kdefinition_empty_config(sort)


# TODO make method of KInner
def bottom_up(f: Callable[[KInner], KInner], kinner: KInner) -> KInner:
Expand Down
116 changes: 58 additions & 58 deletions pyk/src/pyk/kastManip.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,18 +15,14 @@

from .cterm import CTerm, split_config_and_constraints
from .kast import (
FALSE,
TRUE,
KApply,
KAtt,
KClaim,
KDefinition,
KFlatModule,
KInner,
KLabel,
KRewrite,
KRule,
KRuleLike,
KSequence,
KToken,
KVariable,
Expand All @@ -39,10 +35,9 @@
top_down,
)
from .prelude import (
Bool,
Labels,
Sorts,
boolToken,
build_assoc,
mlAnd,
mlBottom,
mlEquals,
Expand All @@ -51,7 +46,7 @@
mlOr,
mlTop,
)
from .utils import find_common_items, hash_str, unique
from .utils import find_common_items, hash_str

_LOGGER: Final = logging.getLogger(__name__)

Expand Down Expand Up @@ -83,22 +78,22 @@ def ml_pred_to_bool(kast: KInner, unsafe: bool = False) -> KInner:
def _ml_constraint_to_bool(_kast: KInner) -> KInner:
if type(_kast) is KApply:
if _kast.label.name == '#Top':
return TRUE
return Bool.true
if _kast.label.name == '#Bottom':
return FALSE
if _kast.label.name == '#Not':
return KApply('notBool_', map(_ml_constraint_to_bool, _kast.args))
return Bool.false
if _kast.label.name == '#Not' and len(_kast.args) == 1:
return Bool.notBool(_ml_constraint_to_bool(_kast.args[0]))
if _kast.label.name == '#And':
return KApply('_andBool_', map(_ml_constraint_to_bool, _kast.args))
return Bool.andBool(map(_ml_constraint_to_bool, _kast.args))
if _kast.label.name == '#Or':
return KApply('_orBool_', map(_ml_constraint_to_bool, _kast.args))
if _kast.label.name == '#Implies':
return KApply('_impliesBool_', map(_ml_constraint_to_bool, _kast.args))
return Bool.orBool(map(_ml_constraint_to_bool, _kast.args))
if _kast.label.name == '#Implies' and len(_kast.args) == 2:
return Bool.impliesBool(_ml_constraint_to_bool(_kast.args[0]), _ml_constraint_to_bool(_kast.args[1]))
if _kast.label.name == '#Equals':
if _kast.args[0] == TRUE:
if _kast.args[0] == Bool.true:
return _kast.args[1]
if _kast.args[0] == FALSE:
return KApply(KLabel('notBool_'), [_kast.args[1]])
if _kast.args[0] == Bool.false:
return Bool.notBool(_kast.args[1])
if type(_kast.args[0]) in [KVariable, KToken]:
return KApply('_==K_', _kast.args)
if unsafe:
Expand All @@ -117,33 +112,33 @@ def _ml_constraint_to_bool(_kast: KInner) -> KInner:
return _ml_constraint_to_bool(kast)


def simplifyBool(k):
def simplify_bool(k):
if k is None:
return None
simplifyRules = [ (KApply('_==K_', [KVariable('#LHS'), TRUE]), KVariable('#LHS')) # noqa
, (KApply('_==K_', [TRUE, KVariable('#RHS')]), KVariable('#RHS')) # noqa
, (KApply('_==K_', [KVariable('#LHS'), FALSE]), KApply('notBool_', [KVariable('#LHS')])) # noqa
, (KApply('_==K_', [FALSE, KVariable('#RHS')]), KApply('notBool_', [KVariable('#RHS')])) # noqa
, (KApply('notBool_', [FALSE]), TRUE) # noqa
, (KApply('notBool_', [TRUE]), FALSE) # noqa
, (KApply('notBool_', [KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('_andBool_', [TRUE, KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [KVariable('#REST'), TRUE]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [FALSE, KVariable('#REST')]), FALSE) # noqa
, (KApply('_andBool_', [KVariable('#REST'), FALSE]), FALSE) # noqa
, (KApply('_orBool_', [FALSE, KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [KVariable('#REST'), FALSE]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [TRUE, KVariable('#REST')]), TRUE) # noqa
, (KApply('_orBool_', [KVariable('#REST'), TRUE]), TRUE) # noqa
] # noqa
newK = k
for rule in simplifyRules:
simplify_rules = [ (KApply('_==K_', [KVariable('#LHS'), Bool.true]), KVariable('#LHS')) # noqa
, (KApply('_==K_', [Bool.true, KVariable('#RHS')]), KVariable('#RHS')) # noqa
, (KApply('_==K_', [KVariable('#LHS'), Bool.false]), Bool.notBool([KVariable('#LHS')])) # noqa
, (KApply('_==K_', [Bool.false, KVariable('#RHS')]), Bool.notBool([KVariable('#RHS')])) # noqa
, (Bool.notBool([Bool.false]), Bool.true) # noqa
, (Bool.notBool([Bool.true]), Bool.false) # noqa
, (Bool.notBool([KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (Bool.notBool([KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (Bool.notBool([KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (Bool.notBool([KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (Bool.andBool([Bool.true, KVariable('#REST')]), KVariable('#REST')) # noqa
, (Bool.andBool([KVariable('#REST'), Bool.true]), KVariable('#REST')) # noqa
, (Bool.andBool([Bool.false, KVariable('#REST')]), Bool.false) # noqa
, (Bool.andBool([KVariable('#REST'), Bool.false]), Bool.false) # noqa
, (Bool.orBool([Bool.false, KVariable('#REST')]), KVariable('#REST')) # noqa
, (Bool.orBool([KVariable('#REST'), Bool.false]), KVariable('#REST')) # noqa
, (Bool.orBool([Bool.true, KVariable('#REST')]), Bool.true) # noqa
, (Bool.orBool([KVariable('#REST'), Bool.true]), Bool.true) # noqa
] # noqa
new_k = k
for rule in simplify_rules:
rewrite = KRewrite(*rule)
newK = rewrite(newK)
return newK
new_k = rewrite(new_k)
return new_k


def extract_lhs(term: KInner) -> KInner:
Expand Down Expand Up @@ -171,7 +166,7 @@ def _extract_subst(conjunct: KInner) -> Optional[Subst]:
if subst is not None:
return subst

if conjunct.args[0] == boolToken(True) and type(conjunct.args[1]) is KApply and conjunct.args[1].label.name in {'_==K_', '_==Int_'}:
if conjunct.args[0] == Bool.true and type(conjunct.args[1]) is KApply and conjunct.args[1].label.name in {'_==K_', '_==Int_'}:
subst = _subst_for_terms(conjunct.args[1].args[0], conjunct.args[1].args[1])

if subst is not None:
Expand Down Expand Up @@ -449,11 +444,11 @@ def minimizeRule(rule, keepVars=[]):
ruleRequires = rule.requires
ruleEnsures = rule.ensures

ruleRequires = build_assoc(TRUE, '_andBool_', unique(flattenLabel('_andBool_', ruleRequires)))
ruleRequires = simplifyBool(ruleRequires)
ruleRequires = Bool.andBool(flattenLabel('_andBool_', ruleRequires))
ruleRequires = simplify_bool(ruleRequires)

ruleEnsures = build_assoc(TRUE, '_andBool_', unique(flattenLabel('_andBool_', ruleEnsures)))
ruleEnsures = simplifyBool(ruleEnsures)
ruleEnsures = Bool.andBool(flattenLabel('_andBool_', ruleEnsures))
ruleEnsures = simplify_bool(ruleEnsures)

constrainedVars = [] if keepVars is None else keepVars
constrainedVars = constrainedVars + collectFreeVars(ruleRequires)
Expand Down Expand Up @@ -553,10 +548,9 @@ def build_rule(
rule_id: str,
init_cterm: CTerm,
final_cterm: CTerm,
claim: bool = False,
priority: Optional[int] = None,
keep_vars: Optional[List[str]] = None
) -> Tuple[KRuleLike, Dict[str, KVariable]]:
) -> Tuple[KRule, Dict[str, KVariable]]:

init_config, *init_constraints = init_cterm
final_config, *final_constraints = final_cterm
Expand Down Expand Up @@ -584,24 +578,30 @@ def build_rule(
(final_config, final_constraint) = split_config_and_constraints(final_term)

rule_body = push_down_rewrites(KRewrite(init_config, final_config))
rule_requires = simplifyBool(ml_pred_to_bool(init_constraint))
rule_ensures = simplifyBool(ml_pred_to_bool(final_constraint))
att_dict = {} if claim or priority is None else {'priority': str(priority)}
rule_requires = simplify_bool(ml_pred_to_bool(init_constraint))
rule_ensures = simplify_bool(ml_pred_to_bool(final_constraint))
att_dict = {} if priority is None else {'priority': str(priority)}
rule_att = KAtt(atts=att_dict)

rule: KRuleLike
if not claim:
rule = KRule(rule_body, requires=rule_requires, ensures=rule_ensures, att=rule_att)
else:
rule = KClaim(rule_body, requires=rule_requires, ensures=rule_ensures, att=rule_att)

rule = KRule(rule_body, requires=rule_requires, ensures=rule_ensures, att=rule_att)
rule = rule.update_atts({'label': rule_id})
new_keep_vars = None
if keep_vars is not None:
new_keep_vars = [v_subst[v].name for v in keep_vars]
return (minimizeRule(rule, keepVars=new_keep_vars), vremap_subst)


def build_claim(
claim_id: str,
init_cterm: CTerm,
final_cterm: CTerm,
keep_vars: Optional[List[str]] = None
) -> Tuple[KClaim, Dict[str, KVariable]]:
rule, var_map = build_rule(claim_id, init_cterm, final_cterm, keep_vars=keep_vars)
claim = KClaim(rule.body, requires=rule.requires, ensures=rule.ensures, att=rule.att)
return claim, var_map


def abstract_term_safely(kast: KInner, base_name: str = 'V') -> KVariable:
vname = hash_str(kast)[0:8]
return KVariable(base_name + '_' + vname)
Expand Down
Loading