Skip to content

Commit

Permalink
Upstreaming pyk functionality (#2756)
Browse files Browse the repository at this point in the history 
* pyk/tests: move simplifyBool tests from integration to unit tests

* pyk/Makefile: explicit options

* pyk/kast: add KDefinition.{production_for_klabel,production_for_cell_sort,empty_config} from downstream

* pyk/kast: add KDefinition.module_names

* pyk/kprint: SymbolTable is a Dict, not a Mapping

* pyk/: factor out build_claim from build_rule, with stronger typing

* pyk/: factor out class Bool in prelude

* pyk/: rename simplifyBool => simplify_bool

* Update pyk/src/pyk/tests/test_kastManip.py

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
  • Loading branch information
@ehildenb @rv-jenkins
ehildenb and rv-jenkins authored Jul 29, 2022
1 parent 0ec7270 commit e72bb80
Show file tree
Hide file tree
Showing 12 changed files with 252 additions and 124 deletions.
4 changes: 2 additions & 2 deletions pyk/Makefile
View file
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
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
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
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

0 comments on commit e72bb80

Please sign in to comment.