From b3e5393fb44d35f0a294988104cb3d87083f90ed Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 14:43:40 +0100 Subject: [PATCH 01/16] Add Summarizer utility functions to kastManip Co-authored-by: Everett Hildenbrandt --- .../src/main/scripts/lib/pyk/kastManip.py | 368 ++++++++++++++++++ 1 file changed, 368 insertions(+) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 42f652780b4..44381a51d66 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -514,3 +514,371 @@ def _removeSourceMap(att): newAtts[attKey] = atts[attKey] return KAtt(atts = newAtts) return onAttributes(k, _removeSourceMap) + + +def boolToken(b): + return KToken(str(b).lower(), 'Bool') + + +def intToken(i): + return KToken(str(i), 'Int') + + +def stringToken(s): + return KToken('"' + s + '"', 'String') + + +def ltInt(i1, i2): + return KApply('_ and from a configuration. + + - Input: Constrained term which contains and . + - Output: Constrained term with those cells removed. + """ + rule = KApply('', [KVariable('CONFIG'), KApply('', [KVariable('_')])]), KVariable('CONFIG') + return rewriteAnywhereWith(rule, constrainedTerm) + + +def isAnonVariable(kast): + return isKVariable(kast) and kast['name'].startswith('_') + + +def omitLargeTokens(kast, maxLen=78): + def _largeTokensToDots(_k): + if isKToken(_k) and len(_k['token']) > maxLen: + return KToken('...', _k['sort']) + return _k + return traverseBottomUp(kast, _largeTokensToDots) + + +def getCell(constrainedTerm, cellVariable): + (state, _) = splitConfigAndConstraints(constrainedTerm) + (_, subst) = splitConfigFrom(state) + return subst[cellVariable] + + +def setCell(constrainedTerm, cellVariable, cellValue): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + (config, subst) = splitConfigFrom(state) + subst[cellVariable] = cellValue + return KApply('#And', [substitute(config, subst), constraint]) + + +def structurallyFrameKCell(constrainedTerm): + kCell = getCell(constrainedTerm, 'K_CELL') + if isKSequence(kCell) and len(kCell['items']) > 0 and isAnonVariable(kCell['items'][-1]): + kCell = KSequence(kCell['items'][0:-1] + [ktokenDots]) + return setCell(constrainedTerm, 'K_CELL', kCell) + + +def applyCellSubst(constrainedTerm, cellSubst): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + (config, subst) = splitConfigFrom(state) + for k in cellSubst: + subst[k] = cellSubst[k] + return KApply('#And', [substitute(config, subst), constraint]) + + +def removeUselessConstraints(constrainedTerm, keepVars=None): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + constraints = flattenLabel('#And', constraint) + usedVars = collectFreeVars(state) + usedVars = usedVars if keepVars is None else (usedVars + keepVars) + prevLenUsedVars = 0 + newConstraints = [] + while len(usedVars) > prevLenUsedVars: + prevLenUsedVars = len(usedVars) + for c in constraints: + if c not in newConstraints: + newVars = collectFreeVars(c) + if any([v in usedVars for v in newVars]): + newConstraints.append(c) + usedVars.extend(newVars) + usedVars = list(set(usedVars)) + return mlAnd([state] + newConstraints) + + +def removeConstraintClausesFor(varNames, constraint): + constraints = flattenLabel('#And', constraint) + newConstraints = [] + for c in constraints: + if not any([v in varNames for v in collectFreeVars(c)]): + newConstraints.append(c) + return mlAnd(newConstraints) + + +def removeConstraintsFor(varNames, constrainedTerm): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + constraint = removeConstraintClausesFor(varNames, constraint) + return mlAnd([state, constraint]) + + +def hasExistentials(pattern): + return any([v.startswith('?') for v in collectFreeVars(pattern)]) + + +def buildRule(ruleId, initConstrainedTerm, finalConstrainedTerm, claim=False, priority=None, keepVars=None): + (initConfig, initConstraint) = splitConfigAndConstraints(initConstrainedTerm) + (finalConfig, finalConstraint) = splitConfigAndConstraints(finalConstrainedTerm) + initConstraints = flattenLabel('#And', initConstraint) + finalConstraints = [c for c in flattenLabel('#And', finalConstraint) if c not in initConstraints] + initConstrainedTerm = mlAnd([initConfig] + initConstraints) + finalConstrainedTerm = mlAnd([finalConfig] + finalConstraints) + + lhsVars = collectFreeVars(initConstrainedTerm) + rhsVars = collectFreeVars(finalConstrainedTerm) + varOccurances = countVarOccurances(mlAnd([initConstrainedTerm, finalConstrainedTerm])) + vSubst = {} + vremapSubst = {} + for v in varOccurances: + newV = v + if varOccurances[v] == 1: + newV = '_' + newV + if v in rhsVars and v not in lhsVars: + newV = '?' + newV + vSubst[v] = KVariable(newV) + vremapSubst[newV] = KVariable(v) + + initConstrainedTerm = substitute(initConstrainedTerm, vSubst) + finalConstrainedTerm = applyExistentialSubstitutions(substitute(finalConstrainedTerm, vSubst)) + (initConfig, initConstraint) = splitConfigAndConstraints(initConstrainedTerm) + (finalConfig, finalConstraint) = splitConfigAndConstraints(finalConstrainedTerm) + + ruleBody = pushDownRewrites(KRewrite(initConfig, finalConfig)) + ruleRequires = simplifyBool(unsafeMlPredToBool(initConstraint)) + ruleEnsures = simplifyBool(unsafeMlPredToBool(finalConstraint)) + ruleAtt = None if claim or priority is None else KAtt(atts={'priority': str(priority)}) + if not claim: + rule = KRule(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtt) + else: + rule = KClaim(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtt) + rule = addAttributes(rule, {'label': ruleId}) + newKeepVars = None + if keepVars is not None: + newKeepVars = [vSubst[v]['name'] for v in keepVars] + return (minimizeRule(rule, keepVars=newKeepVars), vremapSubst) + + +def onCells(cellHandler, constrainedTerm): + """Given an effect and a constrained term, return the effect applied to the cells in the term. + + - Input: Effect that takes as input a cell name and the contents of the cell, and a constrained term. + - Output: Constrained term with the effect applied to each cell. + """ + (config, constraint) = splitConfigAndConstraints(constrainedTerm) + constraints = flattenLabel('#And', constraint) + (emptyConfig, subst) = splitConfigFrom(config) + for k in subst: + newCell = cellHandler(k, subst[k]) + if newCell is not None: + (term, constraint) = newCell + subst[k] = term + if constraint not in constraints: + constraints.append(constraint) + return mlAnd([substitute(emptyConfig, subst)] + constraints) + + +def abstractTermSafely(kast, baseName='V'): + vname = strHash(kast)[0:8] + return KVariable(baseName + '_' + vname) + + +def antiUnify(state1, state2): + subst1 = {} + subst2 = {} + + def _rewritesToAbstractions(_kast): + if isKRewrite(_kast): + return abstractTermSafely(_kast) + return _kast + + minimizedRewrite = pushDownRewrites(KRewrite(state1, state2)) + abstractedState = traverseBottomUp(minimizedRewrite, _rewritesToAbstractions) + subst1 = match(abstractedState, state1) + subst2 = match(abstractedState, state2) + if subst1 is None or subst2 is None: + fatal('Anti-unification failed to produce a more general state!') + return (abstractedState, subst1, subst2) + + +def antiUnifyWithConstraints(constrainedTerm1, constrainedTerm2, implications=False, disjunct=False): + (state1, constraint1) = splitConfigAndConstraints(constrainedTerm1) + (state2, constraint2) = splitConfigAndConstraints(constrainedTerm2) + constraints1 = flattenLabel('#And', constraint1) + constraints2 = flattenLabel('#And', constraint2) + (state, subst1, subst2) = antiUnify(state1, state2) + + constraints = [c for c in constraints1 if c in constraints2] + constraint1 = mlAnd([c for c in constraints1 if c not in constraints]) + constraint2 = mlAnd([c for c in constraints2 if c not in constraints]) + implication1 = mlImplies(constraint1, substToMlPred(subst1)) + implication2 = mlImplies(constraint2, substToMlPred(subst2)) + + if implications: + constraints.append(implication1) + constraints.append(implication2) + + if disjunct: + constraints.append(mlOr([constraint1, constraint2])) + + return mlAnd([state] + constraints) + + +def removeDisjuncts(constrainedTerm): + clauses = flattenLabel('#And', constrainedTerm) + clauses = [c for c in clauses if not (isKApply(c) and c['label'] == '#Or')] + constrainedTerm = mlAnd(clauses) + return constrainedTerm + + +def abstractCell(constrainedTerm, cellName): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + constraints = flattenLabel('#And', constraint) + cell = getCell(state, cellName) + cellVar = KVariable(cellName) + if not isKVariable(cell): + state = setCell(state, cellName, cellVar) + constraints.append(KApply('#Equals', [cellVar, cell])) + return mlAnd([state] + constraints) + + +def applyExistentialSubstitutions(constrainedTerm): + (state, constraint) = splitConfigAndConstraints(constrainedTerm) + constraints = flattenLabel('#And', constraint) + substPattern = mlEqualsTrue(KApply('_==K_', [KVariable('#VAR'), KVariable('#VAL')])) + subst = {} + newConstraints = [] + for c in constraints: + substMatch = match(substPattern, c) + if substMatch is not None and isKVariable(substMatch['#VAR']) and substMatch['#VAR']['name'].startswith('?'): + subst[substMatch['#VAR']['name']] = substMatch['#VAL'] + else: + newConstraints.append(c) + return substitute(mlAnd([state] + newConstraints), subst) + + +def constraintSubsume(constraint1, constraint2): + if constraint1 == mlTop() or constraint1 == constraint2: + return True + elif isKApply(constraint1) and constraint1['label'] == '#And': + constraints1 = flattenLabel('#And', constraint1) + if all([constraintSubsume(c, constraint2) for c in constraints1]): + return True + elif isKApply(constraint1) and constraint1['label'] == '#Or': + constraints1 = flattenLabel('#Or', constraint1) + if any([constraintSubsume(c, constraint2) for c in constraints1]): + return True + elif isKApply(constraint2) and constraint2['label'] == '#And': + constraints2 = flattenLabel('#And', constraint2) + if any([constraintSubsume(constraint1, c) for c in constraints2]): + return True + elif isKApply(constraint2) and constraint2['label'] == '#Or': + constraints2 = flattenLabel('#Or', constraint2) + if all([constraintSubsume(constraint1, c) for c in constraints2]): + return True + else: + return False + + +def matchWithConstraint(constrainedTerm1, constrainedTerm2): + (state1, constraint1) = splitConfigAndConstraints(constrainedTerm1) + (state2, constraint2) = splitConfigAndConstraints(constrainedTerm2) + subst = match(state1, state2) + if subst is not None and constraintSubsume(substitute(constraint1, subst), constraint2): + return subst + return None + + +def minimizeSubst(subst): + return {k: subst[k] for k in subst if not (isKVariable(subst[k]) and k == subst[k]['name'])} + + +def substToMlPred(subst): + mlTerms = [] + for k in subst: + if KVariable(k) != subst[k]: + mlTerms.append(mlEquals(KVariable(k), subst[k])) + return mlAnd(mlTerms) + + +def substToMap(subst): + mapItems = [KApply('_|->_', [KVariable(k), subst[k]]) for k in subst] + return buildAssoc(KConstant('.Map'), '_Map_', mapItems) + + +def setAttribute(k, key, value): + if 'att' in k and k['att'] is not None and isKAtt(k['att']): + k['att']['att'][key] = value + return k + + +def getLHS(kast): + def _getLHS(_k): + if isKRewrite(_k): + return _k['lhs'] + return _k + return traverseBottomUp(kast, _getLHS) + + +def getRHS(kast): + def _getRHS(_k): + if isKRewrite(_k): + return _k['rhs'] + return _k + return traverseBottomUp(kast, _getRHS) + + +def markExistentialVars(constrainedTerm): + (config, constraint) = splitConfigAndConstraints(constrainedTerm) + configLhs = getLHS(config) + configRhs = getRHS(config) + lhsOccurances = countVarOccurances(configLhs) + rhsOccurances = countVarOccurances(configRhs) + subst = {} + for v in rhsOccurances: + if v not in lhsOccurances: + subst[v] = KVariable('?' + v) + return substitute(mlAnd([config, constraint]), subst) + + +def undoAliases(definition, kast): + alias_undo_rewrites = [(sent['body']['rhs'], sent['body']['lhs']) for module in definition['modules'] for sent in module['localSentences'] if isKRule(sent) and getAttribute(sent, 'alias') is not None] + newKast = kast + for r in alias_undo_rewrites: + newKast = rewriteAnywhereWith(r, newKast) + return newKast From a2fa87b0f35802c6d7a4870d33f91631963977be Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 15:34:02 +0100 Subject: [PATCH 02/16] Organize imports in kastManip --- .../src/main/scripts/lib/pyk/kastManip.py | 58 ++++++++++++++++--- 1 file changed, 50 insertions(+), 8 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 44381a51d66..fee122eadbb 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -1,11 +1,53 @@ -#!/usr/bin/env python3 - -import sys -import subprocess - from .cli_utils import fatal -from .utils import combine_dicts, dedupe, find_common_items -from .kast import * +from .kast import ( + KApply, + KAs, + KAtt, + KBubble, + KClaim, + KConstant, + KContext, + KDefinition, + KFlatModule, + KProduction, + KRewrite, + KRule, + KSequence, + KSortSynonym, + KSyntaxAssociativity, + KSyntaxLexical, + KSyntaxPriority, + KSyntaxSort, + KToken, + KVariable, + addAttributes, + flattenLabel, + getAttribute, + isCellKLabel, + isKApply, + isKAs, + isKAtt, + isKBubble, + isKClaim, + isKContext, + isKDefinition, + isKFlatModule, + isKProduction, + isKRewrite, + isKRule, + isKSequence, + isKSortSynonym, + isKSyntaxAssociativity, + isKSyntaxLexical, + isKSyntaxPriority, + isKSyntaxSort, + isKToken, + isKVariable, + klabelEmptyK, + ktokenDots, +) +from .utils import combine_dicts, dedupe, find_common_items, hash_str + def buildAssoc(unit, join, ls): """Build an associative binary operator term given the join and unit ops. @@ -714,7 +756,7 @@ def onCells(cellHandler, constrainedTerm): def abstractTermSafely(kast, baseName='V'): - vname = strHash(kast)[0:8] + vname = hash_str(kast)[0:8] return KVariable(baseName + '_' + vname) From dc65009e9f42aa69a8481de47c34109630acfe24 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 15:56:01 +0100 Subject: [PATCH 03/16] Fix linting issues in kastManip --- .../src/main/scripts/lib/pyk/kastManip.py | 180 +++++++++++------- 1 file changed, 110 insertions(+), 70 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index fee122eadbb..73a0f32c45f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -64,6 +64,7 @@ def buildAssoc(unit, join, ls): return buildAssoc(unit, join, ls[1:]) return KApply(join, [ls[0], buildAssoc(unit, join, ls[1:])]) + def buildCons(unit, cons, ls): """Build a cons operator term given the cons and unit ops. @@ -74,6 +75,7 @@ def buildCons(unit, cons, ls): return unit return KApply(cons, [ls[0], buildCons(unit, cons, ls[1:])]) + def match(pattern, kast): """Perform syntactic pattern matching and return the substitution. @@ -82,11 +84,11 @@ def match(pattern, kast): """ subst = {} if isKVariable(pattern): - return { pattern["name"] : kast } + return {pattern["name"]: kast} if isKToken(pattern) and isKToken(kast): return {} if pattern["token"] == kast["token"] else None - if isKApply(pattern) and isKApply(kast) \ - and pattern["label"] == kast["label"] and len(pattern["args"]) == len(kast["args"]): + if isKApply(pattern) and isKApply(kast) \ + and pattern["label"] == kast["label"] and len(pattern["args"]) == len(kast["args"]): for (patternArg, kastArg) in zip(pattern["args"], kast["args"]): argSubst = match(patternArg, kastArg) subst = combine_dicts(subst, argSubst) @@ -106,24 +108,29 @@ def match(pattern, kast): return subst return None + def onChildren(kast, effect): if isKApply(kast): - return KApply(kast['label'], [ effect(arg) for arg in kast['args'] ]) + return KApply(kast['label'], [effect(arg) for arg in kast['args']]) elif isKRewrite(kast): return KRewrite(effect(kast['lhs']), effect(kast['rhs'])) elif isKSequence(kast): - return KSequence([ effect(item) for item in kast['items'] ]) + return KSequence([effect(item) for item in kast['items']]) return kast + def traverseBottomUp(kast, effect): return effect(onChildren(kast, lambda _kast: traverseBottomUp(_kast, effect))) + def traverseTopDown(kast, effect): return onChildren(effect(kast), lambda _kast: traverseTopDown(_kast, effect)) + def collectBottomUp(kast, callback): callback(onChildren(kast, lambda _kast: collectBottomUp(_kast, callback))) + def substitute(pattern, substitution): """Apply a substitution to a pattern. @@ -136,6 +143,7 @@ def replace(k): return k return traverseBottomUp(pattern, replace) + def whereMatchingBottomUp(effect, matchPattern, pattern): def _effect(k): matchingSubst = match(matchPattern, k) @@ -145,6 +153,7 @@ def _effect(k): return newK return traverseBottomUp(_effect, pattern) + def replaceKLabels(pattern, klabelMap): def replace(k): if isKApply(k) and k["label"] in klabelMap: @@ -152,6 +161,7 @@ def replace(k): return k return traverseBottomUp(pattern, replace) + def rewriteWith(rule, pattern): """Rewrite a given pattern at the top with the supplied rule. @@ -164,6 +174,7 @@ def rewriteWith(rule, pattern): return substitute(ruleRHS, matchingSubst) return pattern + def rewriteAnywhereWith(rule, pattern): """Attempt rewriting once at every position in an AST bottom-up. @@ -172,15 +183,18 @@ def rewriteAnywhereWith(rule, pattern): """ return traverseBottomUp(pattern, lambda p: rewriteWith(rule, p)) + def replaceWith(rule, pattern): (ruleLHS, ruleRHS) = rule if ruleLHS == pattern: return ruleRHS return pattern + def replaceAnywhereWith(rule, pattern): return traverseBottomUp(pattern, lambda p: replaceWith(rule, p)) + def unsafeMlPredToBool(k): """Attempt to convert an ML Predicate back into a boolean expression. @@ -189,61 +203,67 @@ def unsafeMlPredToBool(k): """ if k is None: return None - mlPredToBoolRules = [ (KApply('#Top' , []) , KToken('true' , 'Bool')) - , (KApply('#Bottom' , []) , KToken('false' , 'Bool')) - , (KApply('#And' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_andBool_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('#Or' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_orBool_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('#Not' , [KVariable('#V1')]) , KApply('notBool_' , [KVariable('#V1')])) - , (KApply('#Equals' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('#Implies' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_impliesBool_' , [KVariable('#V1'), KVariable('#V2')])) - ] + mlPredToBoolRules = [ (KApply('#Top' , []) , KToken('true' , 'Bool')) # noqa + , (KApply('#Bottom' , []) , KToken('false' , 'Bool')) # noqa + , (KApply('#And' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_andBool_' , [KVariable('#V1'), KVariable('#V2')])) # noqa + , (KApply('#Or' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_orBool_' , [KVariable('#V1'), KVariable('#V2')])) # noqa + , (KApply('#Not' , [KVariable('#V1')]) , KApply('notBool_' , [KVariable('#V1')])) # noqa + , (KApply('#Equals' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa + , (KApply('#Implies' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_impliesBool_' , [KVariable('#V1'), KVariable('#V2')])) # noqa + ] # noqa newK = k for rule in mlPredToBoolRules: newK = rewriteAnywhereWith(rule, newK) return newK + def simplifyBool(k): if k is None: return None - simplifyRules = [ (KApply('_==K_', [KVariable('#LHS'), KToken('true', 'Bool')]), KVariable('#LHS')) - , (KApply('_==K_', [KToken('true', 'Bool'), KVariable('#RHS')]), KVariable('#RHS')) - , (KApply('_==K_', [KVariable('#LHS'), KToken('false', 'Bool')]), KApply('notBool_', [KVariable('#LHS')])) - , (KApply('_==K_', [KToken('false', 'Bool'), KVariable('#RHS')]), KApply('notBool_', [KVariable('#RHS')])) - , (KApply('notBool_', [KToken('false' , 'Bool')]), KToken('true' , 'Bool')) - , (KApply('notBool_', [KToken('true' , 'Bool')]), KToken('false' , 'Bool')) - , (KApply('notBool_', [KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('notBool_', [KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('notBool_', [KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('notBool_', [KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])) - , (KApply('_andBool_', [KToken('true', 'Bool'), KVariable('#REST')]), KVariable('#REST')) - , (KApply('_andBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KVariable('#REST')) - , (KApply('_andBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KToken('false', 'Bool')) - , (KApply('_andBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KToken('false', 'Bool')) - , (KApply('_orBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KVariable('#REST')) - , (KApply('_orBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KVariable('#REST')) - , (KApply('_orBool_', [KToken('true', 'Bool'), KVariable('#REST')]), KToken('true', 'Bool')) - , (KApply('_orBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KToken('true', 'Bool')) - ] + simplifyRules = [ (KApply('_==K_', [KVariable('#LHS'), KToken('true', 'Bool')]), KVariable('#LHS')) # noqa + , (KApply('_==K_', [KToken('true', 'Bool'), KVariable('#RHS')]), KVariable('#RHS')) # noqa + , (KApply('_==K_', [KVariable('#LHS'), KToken('false', 'Bool')]), KApply('notBool_', [KVariable('#LHS')])) # noqa + , (KApply('_==K_', [KToken('false', 'Bool'), KVariable('#RHS')]), KApply('notBool_', [KVariable('#RHS')])) # noqa + , (KApply('notBool_', [KToken('false' , 'Bool')]), KToken('true' , 'Bool')) # noqa + , (KApply('notBool_', [KToken('true' , 'Bool')]), KToken('false' , 'Bool')) # 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_', [KToken('true', 'Bool'), KVariable('#REST')]), KVariable('#REST')) # noqa + , (KApply('_andBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KVariable('#REST')) # noqa + , (KApply('_andBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KToken('false', 'Bool')) # noqa + , (KApply('_andBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KToken('false', 'Bool')) # noqa + , (KApply('_orBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KVariable('#REST')) # noqa + , (KApply('_orBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KVariable('#REST')) # noqa + , (KApply('_orBool_', [KToken('true', 'Bool'), KVariable('#REST')]), KToken('true', 'Bool')) # noqa + , (KApply('_orBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KToken('true', 'Bool')) # noqa + ] # noqa newK = k for rule in simplifyRules: newK = rewriteAnywhereWith(rule, newK) return newK + def getOccurances(kast, pattern): occurances = [] + def addOccurance(k): if match(pattern, k): occurances.append(k) + collectBottomUp(kast, addOccurance) return occurances -def countVarOccurances(kast, numOccurances = None): + +def countVarOccurances(kast, numOccurances=None): """Count the number of occurances of each variable in a proof. - Input: Kast term. - Output: Map of variable names to their number of occurances. """ numOccurances = {} if numOccurances is None else numOccurances + def _getNumOccurances(_kast): if isKVariable(_kast): vName = _kast['name'] @@ -251,12 +271,15 @@ def _getNumOccurances(_kast): numOccurances[vName] += 1 else: numOccurances[vName] = 1 + collectBottomUp(kast, _getNumOccurances) return numOccurances + def collectFreeVars(kast): return list(countVarOccurances(kast).keys()) + def splitConfigAndConstraints(kast): """Split the configuration/term from the constraints. @@ -274,6 +297,7 @@ def splitConfigAndConstraints(kast): constraint = buildAssoc(KConstant('#Top'), '#And', constraints) return (term, constraint) + def propagateUpConstraints(k): """Try to propagate common constraints up disjuncts. @@ -283,8 +307,8 @@ def propagateUpConstraints(k): def _propagateUpConstraints(_k): if not (isKApply(_k) and _k['label'] == '#Or'): return _k - conjuncts1 = flattenLabel('#And', _k['args'][0]) - conjuncts2 = flattenLabel('#And', _k['args'][1]) + conjuncts1 = flattenLabel('#And', _k['args'][0]) + conjuncts2 = flattenLabel('#And', _k['args'][1]) (common1, l1, r1) = find_common_items(conjuncts1, conjuncts2) (common2, r2, l2) = find_common_items(r1, l1) common = common1 + common2 @@ -292,10 +316,11 @@ def _propagateUpConstraints(_k): return _k conjunct1 = buildAssoc(KConstant('#Top'), '#And', l2) conjunct2 = buildAssoc(KConstant('#Top'), '#And', r2) - disjunct = KApply('#Or', [conjunct1, conjunct2]) + disjunct = KApply('#Or', [conjunct1, conjunct2]) return buildAssoc(KConstant('#Top'), '#And', [disjunct] + common) return traverseBottomUp(k, _propagateUpConstraints) + def splitConfigFrom(configuration): """Split the substitution from a given configuration. @@ -306,7 +331,10 @@ def splitConfigFrom(configuration): 3. `subst` is the substitution for the generated KVariables back to the original configuration contents. """ initial_substitution = {} - _mkCellVar = lambda label: label.replace('-', '_').replace('<', '').replace('>', '').upper() + '_CELL' + + def _mkCellVar(label): + return label.replace('-', '_').replace('<', '').replace('>', '').upper() + '_CELL' + def _replaceWithVar(k): if isKApply(k) and isCellKLabel(k['label']): if len(k['args']) == 1 and not (isKApply(k['args'][0]) and isCellKLabel(k['args'][0]['label'])): @@ -314,9 +342,11 @@ def _replaceWithVar(k): initial_substitution[config_var] = k['args'][0] return KApply(k['label'], [KVariable(config_var)]) return k + symbolic_config = traverseTopDown(configuration, _replaceWithVar) return (symbolic_config, initial_substitution) + def collapseDots(kast): """Given a configuration with structural frames `...`, minimize the structural frames needed. @@ -326,10 +356,10 @@ def collapseDots(kast): def _collapseDots(_kast): if isKApply(_kast): label = _kast['label'] - args = _kast['args'] + args = _kast['args'] if isCellKLabel(label) and len(args) == 1 and args[0] == ktokenDots: return ktokenDots - newArgs = [ arg for arg in args if arg != ktokenDots ] + newArgs = [arg for arg in args if arg != ktokenDots] if isCellKLabel(label) and len(newArgs) == 0: return ktokenDots if len(newArgs) < len(args): @@ -341,6 +371,7 @@ def _collapseDots(_kast): return _kast return traverseBottomUp(kast, _collapseDots) + def pushDownRewrites(kast): """Traverse a term and push rewrites down as far as possible. @@ -355,8 +386,8 @@ def _pushDownRewrites(_kast): return lhs if isKVariable(lhs) and isKVariable(rhs) and lhs['name'] == rhs['name']: return lhs - if isKApply(lhs) and isKApply(rhs) and lhs['label'] == rhs['label'] and len(lhs['args']) == len(rhs['args']): - newArgs = [ KRewrite(lArg, rArg) for (lArg, rArg) in zip(lhs['args'], rhs['args']) ] + if isKApply(lhs) and isKApply(rhs) and lhs['label'] == rhs['label'] and len(lhs['args']) == len(rhs['args']): + newArgs = [KRewrite(lArg, rArg) for (lArg, rArg) in zip(lhs['args'], rhs['args'])] return KApply(lhs['label'], newArgs) if isKSequence(lhs) and isKSequence(rhs) and len(lhs['items']) > 0 and len(rhs['items']) > 0: if lhs['items'][0] == rhs['items'][0]: @@ -370,6 +401,7 @@ def _pushDownRewrites(_kast): return _kast return traverseTopDown(kast, _pushDownRewrites) + def inlineCellMaps(kast): """Ensure that cell map collections are printed nicely, not as Maps." @@ -384,6 +416,7 @@ def _inlineCellMaps(_kast): return _kast return traverseBottomUp(kast, _inlineCellMaps) + def removeSemanticCasts(kast): """Remove injected `#SemanticCast*` nodes in AST. @@ -396,6 +429,7 @@ def _removeSemanticCasts(_kast): return _kast return traverseBottomUp(kast, _removeSemanticCasts) + def markUselessVars(kast): """Given a kast term as input with variables, return one where the useless vars are appropriately marked. @@ -411,7 +445,8 @@ def markUselessVars(kast): subst[v] = KVariable('_' + v) return substitute(kast, subst) -def uselessVarsToDots(kast, keepVars = None): + +def uselessVarsToDots(kast, keepVars=None): """Structurally abstract away useless variables. - Input: kast term, and a requires clause and ensures clause. @@ -424,7 +459,7 @@ def uselessVarsToDots(kast, keepVars = None): initList[v] = 1 else: initList[v] += 1 - numOccurances = countVarOccurances(kast, numOccurances = initList) + numOccurances = countVarOccurances(kast, numOccurances=initList) def _collapseUselessVars(_kast): if isKApply(_kast) and isCellKLabel(_kast['label']): @@ -439,6 +474,7 @@ def _collapseUselessVars(_kast): return traverseBottomUp(kast, _collapseUselessVars) + def labelsToDots(kast, labels): """Abstract specific labels for printing. @@ -451,39 +487,41 @@ def _labelstoDots(k): return k return traverseBottomUp(kast, _labelstoDots) + def onAttributes(kast, effect): if isKAs(kast): - return KAs(kast['pattern'], kast['alias'], att = effect(kast['att'])) + return KAs(kast['pattern'], kast['alias'], att=effect(kast['att'])) elif isKRule(kast): - return KRule(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = effect(kast['att'])) + return KRule(kast['body'], requires=kast['requires'], ensures=kast['ensures'], att=effect(kast['att'])) elif isKClaim(kast): - return KClaim(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = effect(kast['att'])) + return KClaim(kast['body'], requires=kast['requires'], ensures=kast['ensures'], att=effect(kast['att'])) elif isKContext(kast): - return KContext(kast['body'], requires = kast['requires'], att = effect(kast['att'])) + return KContext(kast['body'], requires=kast['requires'], att=effect(kast['att'])) elif isKBubble(kast): - return KBubble(kast['sentenceType'], kast['contents'], att = effect(kast['att'])) + return KBubble(kast['sentenceType'], kast['contents'], att=effect(kast['att'])) elif isKProduction(kast): - return KProduction(kast['productionItems'], kast['sort'], att = effect(kast['att'])) + return KProduction(kast['productionItems'], kast['sort'], att=effect(kast['att'])) elif isKSyntaxAssociativity(kast): - return KSyntaxAssociativity(kast['assoc'], tags = kast['tags'], att = effect(kast['att'])) + return KSyntaxAssociativity(kast['assoc'], tags=kast['tags'], att=effect(kast['att'])) elif isKSyntaxPriority(kast): - return KSyntaxPriority(priorities = kast['priorities'], att = effect(kast['att'])) + return KSyntaxPriority(priorities=kast['priorities'], att=effect(kast['att'])) elif isKSyntaxSort(kast): - return KSyntaxSort(kast['sort'], att = effect(kast['att'])) + return KSyntaxSort(kast['sort'], att=effect(kast['att'])) elif isKSortSynonym(kast): - return KSortSynonym(kast['newSort'], kast['oldSort'], att = effect(kast['att'])) + return KSortSynonym(kast['newSort'], kast['oldSort'], att=effect(kast['att'])) elif isKSyntaxLexical(kast): - return KSyntaxLexical(kast['name'], kast['regex'], att = effect(kast['att'])) + return KSyntaxLexical(kast['name'], kast['regex'], att=effect(kast['att'])) elif isKFlatModule(kast): - localSentences = [ onAttributes(sent, effect) for sent in kast['localSentences'] ] - return KFlatModule(kast['name'], kast['imports'], localSentences, att = effect(kast['att'])) + localSentences = [onAttributes(sent, effect) for sent in kast['localSentences']] + return KFlatModule(kast['name'], kast['imports'], localSentences, att=effect(kast['att'])) elif isKDefinition(kast): - modules = [ onAttributes(mod, effect) for mod in kast['modules'] ] + modules = [onAttributes(mod, effect) for mod in kast['modules']] requires = None if 'requires' not in kast else kast['requires'] - return KDefinition(kast['mainModule'], modules, requires = requires, att = effect(kast['att'])) + return KDefinition(kast['mainModule'], modules, requires=requires, att=effect(kast['att'])) fatal('No attributes for: ' + kast['node'] + '.') -def minimizeTerm(term, keepVars = None, abstractLabels = []): + +def minimizeTerm(term, keepVars=None, abstractLabels=[]): """Minimize a K term for pretty-printing. - Input: kast term, and optionally requires and ensures clauses with constraints. @@ -494,12 +532,13 @@ def minimizeTerm(term, keepVars = None, abstractLabels = []): """ term = inlineCellMaps(term) term = removeSemanticCasts(term) - term = uselessVarsToDots(term, keepVars = keepVars) + term = uselessVarsToDots(term, keepVars=keepVars) term = labelsToDots(term, abstractLabels) term = collapseDots(term) return term -def minimizeRule(rule, keepVars = []): + +def minimizeRule(rule, keepVars=[]): """Minimize a K rule or claim for pretty-printing. - Input: kast representing a K rule or claim. @@ -511,10 +550,10 @@ def minimizeRule(rule, keepVars = []): if not (isKRule(rule) or isKClaim(rule)): return rule - ruleBody = rule['body'] + ruleBody = rule['body'] ruleRequires = rule['requires'] - ruleEnsures = rule['ensures'] - ruleAtts = rule['att'] + ruleEnsures = rule['ensures'] + ruleAtts = rule['att'] if ruleRequires is not None: ruleRequires = buildAssoc(KToken('true', 'Bool'), '_andBool_', dedupe(flattenLabel('_andBool_', ruleRequires))) @@ -525,21 +564,22 @@ def minimizeRule(rule, keepVars = []): ruleEnsures = simplifyBool(ruleEnsures) ruleRequires = None if ruleRequires == KToken('true', 'Bool') else ruleRequires - ruleEnsures = None if ruleEnsures == KToken('true', 'Bool') else ruleEnsures + ruleEnsures = None if ruleEnsures == KToken('true', 'Bool') else ruleEnsures constrainedVars = [] if keepVars is None else keepVars if ruleRequires is not None: constrainedVars = constrainedVars + collectFreeVars(ruleRequires) if ruleEnsures is not None: constrainedVars = constrainedVars + collectFreeVars(ruleEnsures) - ruleBody = minimizeTerm(ruleBody, keepVars = constrainedVars) + ruleBody = minimizeTerm(ruleBody, keepVars=constrainedVars) if ruleRequires == KToken('true', 'Bool'): ruleRequires = None if isKRule(rule): - return KRule(ruleBody, requires = ruleRequires, ensures = ruleEnsures, att = ruleAtts) + return KRule(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtts) else: - return KClaim(ruleBody, requires = ruleRequires, ensures = ruleEnsures, att = ruleAtts) + return KClaim(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtts) + def removeSourceMap(k): """Remove source map information from a given definition. @@ -550,11 +590,11 @@ def removeSourceMap(k): def _removeSourceMap(att): if isKAtt(att): atts = att['att'] - newAtts = { } + newAtts = {} for attKey in atts.keys(): if attKey != 'org.kframework.attributes.Source' and attKey != 'org.kframework.attributes.Location': newAtts[attKey] = atts[attKey] - return KAtt(atts = newAtts) + return KAtt(atts=newAtts) return onAttributes(k, _removeSourceMap) From 4b55c3452b3bdd2bc6988b0ac5a2fc4bbbf62cbd Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 16:49:41 +0100 Subject: [PATCH 04/16] Organize imports in coverage --- .../src/main/scripts/lib/pyk/coverage.py | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/coverage.py b/k-distribution/src/main/scripts/lib/pyk/coverage.py index a1bdfc369ab..0a49192d259 100755 --- a/k-distribution/src/main/scripts/lib/pyk/coverage.py +++ b/k-distribution/src/main/scripts/lib/pyk/coverage.py @@ -1,11 +1,14 @@ -#!/usr/bin/env python3 - -import json -import sys - from .cli_utils import fatal -from .kast import * -from .kastManip import * +from .kast import ( + KRewrite, + KRule, + isKApply, + isKRewrite, + isKRule, + isKSequence, + readKastTerm, +) + def getRuleById(definition, rule_id): """Get a rule from the definition by coverage rule id. From 700b56c6bfb3f07a7f65101a9414615668e02494 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 16:54:39 +0100 Subject: [PATCH 05/16] Fix linting issues in coverage --- .../src/main/scripts/lib/pyk/coverage.py | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/coverage.py b/k-distribution/src/main/scripts/lib/pyk/coverage.py index 0a49192d259..68cb90c78d4 100755 --- a/k-distribution/src/main/scripts/lib/pyk/coverage.py +++ b/k-distribution/src/main/scripts/lib/pyk/coverage.py @@ -29,11 +29,12 @@ def getRuleById(definition, rule_id): return sentence fatal('Could not find rule with ID: ' + rule_id) + def stripCoverageLogger(rule): - ruleBody = rule['body'] + ruleBody = rule['body'] ruleRequires = rule['requires'] - ruleEnsures = rule['ensures'] - ruleAtts = rule['att'] + ruleEnsures = rule['ensures'] + ruleAtts = rule['att'] if isKRewrite(ruleBody): ruleLHS = ruleBody['lhs'] @@ -42,7 +43,8 @@ def stripCoverageLogger(rule): ruleRHSseq = ruleRHS['args'][0] if isKSequence(ruleRHSseq) and len(ruleRHSseq['items']) == 2: ruleBody = KRewrite(ruleLHS, ruleRHSseq['items'][1]) - return KRule(ruleBody, requires = ruleRequires, ensures = ruleEnsures, att = ruleAtts) + return KRule(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtts) + def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_list): """Translate the coverage data from one kompiled definition to another. @@ -60,18 +62,18 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li # Load the src_rule_id -> src_source_location rule map from the src kompiled directory src_rule_map = {} for line in src_all_rules: - [ src_rule_hash, src_rule_loc ] = line.split(' ') + src_rule_hash, src_rule_loc = line.split(' ') src_rule_loc = src_rule_loc.split('/')[-1] src_rule_map[src_rule_hash.strip()] = src_rule_loc.strip() # Load the dst_rule_id -> dst_source_location rule map (and inverts it) from the dst kompiled directory dst_rule_map = {} for line in dst_all_rules: - [ dst_rule_hash, dst_rule_loc ] = line.split(' ') + dst_rule_hash, dst_rule_loc = line.split(' ') dst_rule_loc = dst_rule_loc.split('/')[-1] dst_rule_map[dst_rule_loc.strip()] = dst_rule_hash.strip() - src_rule_list = [ rule_hash.strip() for rule_hash in src_rules_list ] + src_rule_list = [rule_hash.strip() for rule_hash in src_rules_list] # Filter out non-functional rules from rule map (determining if they are functional via the top symbol in the rule being ``) dst_non_function_rules = [] @@ -79,9 +81,9 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li for sentence in module['localSentences']: if isKRule(sentence): ruleBody = sentence['body'] - ruleAtt = sentence['att']['att'] - if (isKApply(ruleBody) and ruleBody['label'] == '') \ - or (isKRewrite(ruleBody) and isKApply(ruleBody['lhs']) and ruleBody['lhs']['label'] == ''): + ruleAtt = sentence['att']['att'] + if (isKApply(ruleBody) and ruleBody['label'] == '') \ + or (isKRewrite(ruleBody) and isKApply(ruleBody['lhs']) and ruleBody['lhs']['label'] == ''): if 'UNIQUE_ID' in ruleAtt: dst_non_function_rules.append(ruleAtt['UNIQUE_ID']) @@ -101,6 +103,7 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li return dst_rule_list + def translateCoverageFromPaths(src_kompiled_dir, dst_kompiled_dir, src_rules_file): """Translate coverage information given paths to needed files. @@ -114,16 +117,16 @@ def translateCoverageFromPaths(src_kompiled_dir, dst_kompiled_dir, src_rules_fil """ src_all_rules = [] with open(src_kompiled_dir + '/allRules.txt', 'r') as src_all_rules_file: - src_all_rules = [ line.strip() for line in src_all_rules_file ] + src_all_rules = [line.strip() for line in src_all_rules_file] dst_all_rules = [] with open(dst_kompiled_dir + '/allRules.txt', 'r') as dst_all_rules_file: - dst_all_rules = [ line.strip() for line in dst_all_rules_file ] + dst_all_rules = [line.strip() for line in dst_all_rules_file] dst_definition = readKastTerm(dst_kompiled_dir + '/compiled.json') src_rules_list = [] with open(src_rules_file, 'r') as src_rules: - src_rules_list = [ line.strip() for line in src_rules ] + src_rules_list = [line.strip() for line in src_rules] return translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_list) From d2197542058add4f075cf6b7a810c6a112ab8f33 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 17:04:49 +0100 Subject: [PATCH 06/16] Organize imports in ktool --- .../src/main/scripts/lib/pyk/ktool.py | 21 ++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 757a06634be..acefad099e4 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -1,13 +1,24 @@ -#!/usr/bin/env python3 - +import json import os -from pathlib import Path import subprocess +import sys +from pathlib import Path from typing import List -from .cli_utils import gen_file_timestamp, notif +from .cli_utils import fatal, gen_file_timestamp, notif +from .kast import ( + KConstant, + KDefinition, + KFlatModule, + KImport, + KRequire, + buildSymbolTable, + flattenLabel, + prettyPrintKast, + readKastTerm, +) from .utils import hash_str -from .kastManip import * + class KPrint: """Given a kompiled directory, build an unparser for it. From 16c9ebf3afaebd682f639af18218cdf1d68b9fdb Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 17:16:13 +0100 Subject: [PATCH 07/16] FIx linting issues in ktool --- .../src/main/scripts/lib/pyk/ktool.py | 71 ++++++++++--------- 1 file changed, 36 insertions(+), 35 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index acefad099e4..81e66db74b7 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -26,36 +26,37 @@ class KPrint: def __init__(self, kompiledDirectory): self.kompiledDirectory = Path(kompiledDirectory) - self.definition = readKastTerm(self.kompiledDirectory / 'compiled.json') - self.symbolTable = buildSymbolTable(self.definition, opinionated = True) - self.definitionHash = hash_str(self.definition) + self.definition = readKastTerm(self.kompiledDirectory / 'compiled.json') + self.symbolTable = buildSymbolTable(self.definition, opinionated=True) + self.definitionHash = hash_str(self.definition) - def prettyPrint(self, kast, debug = False): + def prettyPrint(self, kast, debug=False): """Given a KAST term, pretty-print it using the current definition. - Input: KAST term in JSON. - Output: Best-effort pretty-printed representation of the KAST term. """ - return prettyPrintKast(kast, self.symbolTable, debug = debug) + return prettyPrintKast(kast, self.symbolTable, debug=debug) + class KProve(KPrint): """Given a kompiled directory and a main file name, build a prover for it. """ - def __init__(self, kompiledDirectory, mainFileName, useDirectory = None): + def __init__(self, kompiledDirectory, mainFileName, useDirectory=None): super(KProve, self).__init__(kompiledDirectory) - self.directory = Path(self.kompiledDirectory).parent - self.useDirectory = (self.directory / 'kprove') if useDirectory is None else Path(useDirectory) - self.useDirectory.mkdir(parents = True, exist_ok = True) - self.mainFileName = mainFileName - self.prover = [ 'kprovex' ] - self.proverArgs = [ ] + self.directory = Path(self.kompiledDirectory).parent + self.useDirectory = (self.directory / 'kprove') if useDirectory is None else Path(useDirectory) + self.useDirectory.mkdir(parents=True, exist_ok=True) + self.mainFileName = mainFileName + self.prover = ['kprovex'] + self.proverArgs = [] with open(self.kompiledDirectory / 'backend.txt', 'r') as ba: - self.backend = ba.read() + self.backend = ba.read() with open(self.kompiledDirectory / 'mainModule.txt', 'r') as mm: self.mainModule = mm.read() - def prove(self, specFile, specModuleName, args = [], haskellArgs = [], logAxiomsFile = None, allowZeroStep = False): + def prove(self, specFile, specModuleName, args=[], haskellArgs=[], logAxiomsFile=None, allowZeroStep=False): """Given the specification to prove and arguments for the prover, attempt to prove it. - Input: Specification file name, specification module name, optionall arguments, haskell backend arguments, and file to log axioms to. @@ -64,45 +65,45 @@ def prove(self, specFile, specModuleName, args = [], haskellArgs = [], logAxioms logFile = specFile.with_suffix('.debug-log') if logAxiomsFile is None else logAxiomsFile if logFile.exists(): logFile.unlink() - haskellLogArgs = [ '--log' , str(logFile) , '--log-format' , 'oneline' , '--log-entries' , 'DebugTransition' ] - command = [ c for c in self.prover ] - command += [ str(specFile) ] - command += [ '--backend' , self.backend , '--directory' , str(self.directory) , '-I' , str(self.directory) , '--spec-module' , specModuleName , '--output' , 'json' ] - command += [ c for c in self.proverArgs ] + haskellLogArgs = ['--log', str(logFile), '--log-format', 'oneline', '--log-entries', 'DebugTransition'] + command = [c for c in self.prover] + command += [str(specFile)] + command += ['--backend', self.backend, '--directory', str(self.directory), '-I', str(self.directory), '--spec-module', specModuleName, '--output', 'json'] + command += [c for c in self.proverArgs] command += args - commandEnv = os.environ.copy() + commandEnv = os.environ.copy() commandEnv['KORE_EXEC_OPTS'] = ' '.join(haskellArgs + haskellLogArgs) notif(' '.join(command)) - process = subprocess.Popen(command, stdout = subprocess.PIPE, stderr = subprocess.PIPE, universal_newlines = True, env = commandEnv) - (stdout, stderr) = process.communicate(input = None) + process = subprocess.Popen(command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, universal_newlines=True, env=commandEnv) + stdout, stderr = process.communicate(input=None) try: finalState = json.loads(stdout)['term'] - except: + except Exception: sys.stderr.write(stdout + '\n') sys.stderr.write(stderr + '\n') - fatal('Exiting...', exitCode = process.returncode) + fatal(f'Exiting: process returned {process.returncode}') if finalState == KConstant('#Top') and len(_getAppliedAxiomList(logFile)) == 0 and not allowZeroStep: fatal('Proof took zero steps, likely the LHS is invalid: ' + str(specFile)) return finalState - def proveClaim(self, claim, claimId, lemmas = [], args = [], haskellArgs = [], logAxiomsFile = None, allowZeroStep = False): + def proveClaim(self, claim, claimId, lemmas=[], args=[], haskellArgs=[], logAxiomsFile=None, allowZeroStep=False): """Given a K claim, write the definition needed for the prover, and attempt to prove it. - Input: KAST representation of a claim to prove, and an identifer for said claim. - Output: KAST representation of final state the prover supplies for it. """ - self._writeClaimDefinition(claim, claimId, lemmas = lemmas) - return self.prove(self.useDirectory / (claimId.lower() + '-spec.k'), claimId.upper() + '-SPEC', args = args, haskellArgs = haskellArgs, logAxiomsFile = logAxiomsFile, allowZeroStep = allowZeroStep) + self._writeClaimDefinition(claim, claimId, lemmas=lemmas) + return self.prove(self.useDirectory / (claimId.lower() + '-spec.k'), claimId.upper() + '-SPEC', args=args, haskellArgs=haskellArgs, logAxiomsFile=logAxiomsFile, allowZeroStep=allowZeroStep) - def proveClaimNoBranching(self, claim, claimId, args = [], haskellArgs = [], logAxiomsFile = None, maxDepth = 1000, allowZeroStep = False): + def proveClaimNoBranching(self, claim, claimId, args=[], haskellArgs=[], logAxiomsFile=None, maxDepth=1000, allowZeroStep=False): """Given a K claim, attempt to prove it, but do not allow the prover to branch. - Input: KAST representation of a claim to prove, and identifier for said claim. - Output: KAST representation of final state of prover. """ logFileName = logAxiomsFile if logAxiomsFile is not None else (self.useDirectory / claimId.lower()).with_suffix('.debug.log') - nextState = self.proveClaim(claim, claimId, args = (args + ['--branching-allowed', '1', '--depth', str(maxDepth)]), haskellArgs = haskellArgs, logAxiomsFile = logFileName, allowZeroStep = allowZeroStep) - depth = 0 + nextState = self.proveClaim(claim, claimId, args=(args + ['--branching-allowed', '1', '--depth', str(maxDepth)]), haskellArgs=haskellArgs, logAxiomsFile=logFileName, allowZeroStep=allowZeroStep) + depth = 0 for axioms in _getAppliedAxiomList(str(logFileName)): depth += 1 if len(axioms) > 1: @@ -110,18 +111,18 @@ def proveClaimNoBranching(self, claim, claimId, args = [], haskellArgs = [], log nextStates = flattenLabel('#Or', nextState) return (depth, nextStates) - def _writeClaimDefinition(self, claim, claimId, lemmas = [], rule = False): + def _writeClaimDefinition(self, claim, claimId, lemmas=[], rule=False): """Given a K claim, write the definition file needed for the prover to it. - Input: KAST representation of a claim to prove, and an identifier for said claim. - Output: Write to filesystem the specification with the claim. """ - tmpClaim = self.useDirectory / (claimId.lower() if rule else (claimId.lower() + '-spec')) + tmpClaim = self.useDirectory / (claimId.lower() if rule else (claimId.lower() + '-spec')) tmpModuleName = claimId.upper() if rule else (claimId.upper() + '-SPEC') - tmpClaim = tmpClaim.with_suffix('.k') + tmpClaim = tmpClaim.with_suffix('.k') with open(tmpClaim, 'w') as tc: - claimModule = KFlatModule(tmpModuleName, [KImport(self.mainModule, True)], lemmas + [claim]) - claimDefinition = KDefinition(tmpModuleName, [claimModule], requires = [KRequire(self.mainFileName)]) + claimModule = KFlatModule(tmpModuleName, [KImport(self.mainModule, True)], lemmas + [claim]) + claimDefinition = KDefinition(tmpModuleName, [claimModule], requires=[KRequire(self.mainFileName)]) tc.write(gen_file_timestamp() + '\n') tc.write(self.prettyPrint(claimDefinition) + '\n\n') tc.flush() From ba6adae55e52b0dd3a6d0d818d813129c2ed781a Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 17:41:12 +0100 Subject: [PATCH 08/16] Fix linting issues in kast --- .../src/main/scripts/lib/pyk/kast.py | 297 +++++++++++------- 1 file changed, 182 insertions(+), 115 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index fccca75a03f..231bba94944 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/k-distribution/src/main/scripts/lib/pyk/kast.py @@ -1,170 +1,222 @@ -#!/usr/bin/env python3 - -import sys import json +import sys from .cli_utils import fatal, notif, warning from .utils import combine_dicts + def KApply(label, args): - return { 'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args } + return {'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args} + def isKApply(k): return k['node'] == 'KApply' -def KAs(pattern, alias, att = None): - return { 'node': 'KAs', 'pattern': pattern, 'alias': alias, 'att': att } + +def KAs(pattern, alias, att=None): + return {'node': 'KAs', 'pattern': pattern, 'alias': alias, 'att': att} + def isKAs(k): return k['node'] == 'KAs' + def KConstant(label): return KApply(label, []) + def isKConstant(k): return isKApply(k) and len(k['args']) == 0 + def KSequence(items): - return { 'node': 'KSequence', 'arity': len(items), 'items': items } + return {'node': 'KSequence', 'arity': len(items), 'items': items} + def isKSequence(k): return k['node'] == 'KSequence' + def KVariable(name): - return { 'node' : 'KVariable', 'name': name, 'originalName': name } + return {'node': 'KVariable', 'name': name, 'originalName': name} + def isKVariable(k): return k['node'] == 'KVariable' + def KToken(token, sort): - return { 'node' : 'KToken', 'sort': sort, 'token': token} + return {'node': 'KToken', 'sort': sort, 'token': token} + def isKToken(k): return k['node'] == 'KToken' + def KRewrite(lhs, rhs): - return { 'node': 'KRewrite', 'lhs': lhs, 'rhs': rhs } + return {'node': 'KRewrite', 'lhs': lhs, 'rhs': rhs} + def isKRewrite(k): return k['node'] == 'KRewrite' -def KAtt(atts = {}): + +def KAtt(atts={}): return {'node': 'KAtt', 'att': atts} + def isKAtt(k): return k['node'] == 'KAtt' -def KRule(body, requires = None, ensures = None, att = None): - return { 'node': 'KRule', 'body': body, 'requires': requires, 'ensures': ensures, 'att': att } + +def KRule(body, requires=None, ensures=None, att=None): + return {'node': 'KRule', 'body': body, 'requires': requires, 'ensures': ensures, 'att': att} + def isKRule(k): return k['node'] == 'KRule' -def KClaim(body, requires = None, ensures = None, att = None): - return { 'node': 'KClaim', 'body': body, 'requires': requires, 'ensures': ensures, 'att': att } + +def KClaim(body, requires=None, ensures=None, att=None): + return {'node': 'KClaim', 'body': body, 'requires': requires, 'ensures': ensures, 'att': att} + def isKClaim(k): return k['node'] == 'KClaim' -def KContext(body, requires = None, ensures = None, att = None): - return { 'node': 'KContext', 'body': body, 'requires': requires, 'att': att } + +def KContext(body, requires=None, ensures=None, att=None): + return {'node': 'KContext', 'body': body, 'requires': requires, 'att': att} + def isKContext(k): return k['node'] == 'KContext' -def KBubble(sentenceType, contents, att = None): - return { 'node': 'KBubble', 'sentenceType': sentenceType, 'contents': contents, 'att': att } + +def KBubble(sentenceType, contents, att=None): + return {'node': 'KBubble', 'sentenceType': sentenceType, 'contents': contents, 'att': att} + def isKBubble(k): return k['node'] == 'KBubble' -def KProduction(productionItems, sort, att = None): - return { 'node': 'KProduction', 'productionItems': productionItems, 'sort': sort, 'att': att } + +def KProduction(productionItems, sort, att=None): + return {'node': 'KProduction', 'productionItems': productionItems, 'sort': sort, 'att': att} + def isKProduction(k): return k['node'] == 'KProduction' + def KNonTerminal(sort): - return { 'node': 'KNonTerminal', 'sort': sort } + return {'node': 'KNonTerminal', 'sort': sort} + def isKNonTerminal(k): return k['node'] == 'KNonTerminal' + def KTerminal(value): - return { 'node': 'KTerminal', 'value': value} + return {'node': 'KTerminal', 'value': value} + def isKTerminal(k): return k['node'] == 'KTerminal' -def KRegexTerminal(regex, precedeRegex = None, followRegex = None): - return { 'node': 'KRegexTerminal', 'regex': regex, 'precedeRegex': precedeRegex, 'followRegex': followRegex } + +def KRegexTerminal(regex, precedeRegex=None, followRegex=None): + return {'node': 'KRegexTerminal', 'regex': regex, 'precedeRegex': precedeRegex, 'followRegex': followRegex} + def isKRegexTerminal(k): return k['node'] == 'KRegexTerminal' + def KSort(name): - return { 'node': 'KSort', 'name': name } + return {'node': 'KSort', 'name': name} + def isKSort(k): return k['node'] == 'KSort' -def KSyntaxAssociativity(assoc, tags = [], att = None): - return { 'node': 'KSyntaxAssociativity', 'assoc': assoc, 'tags': tags, 'att': att } + +def KSyntaxAssociativity(assoc, tags=[], att=None): + return {'node': 'KSyntaxAssociativity', 'assoc': assoc, 'tags': tags, 'att': att} + def isKSyntaxAssociativity(k): return k['node'] == 'KSyntaxAssociativity' -def KSyntaxPriority(priorities = [], att = None): - return { 'node': 'KSyntaxPriority', 'priorities': priorities, 'att': att } + +def KSyntaxPriority(priorities=[], att=None): + return {'node': 'KSyntaxPriority', 'priorities': priorities, 'att': att} + def isKSyntaxPriority(k): return k['node'] == 'KSyntaxPriority' -def KSyntaxSort(sort, att = None): - return { 'node': 'KSyntaxSort', 'sort': sort, 'att': att } + +def KSyntaxSort(sort, att=None): + return {'node': 'KSyntaxSort', 'sort': sort, 'att': att} + def isKSyntaxSort(k): return k['node'] == 'KSyntaxSort' -def KSortSynonym(newSort, oldSort, att = None): - return { 'node': 'KSortSynonym', 'newSort': newSort, 'oldSort': oldSort, 'att': att } + +def KSortSynonym(newSort, oldSort, att=None): + return {'node': 'KSortSynonym', 'newSort': newSort, 'oldSort': oldSort, 'att': att} + def isKSortSynonym(k): return k['node'] == 'KSortSynonym' -def KSyntaxLexical(newSort, oldSort, att = None): - return { 'node': 'KSyntaxLexical', 'newSort': newSort, 'oldSort': oldSort, 'att': att } + +def KSyntaxLexical(newSort, oldSort, att=None): + return {'node': 'KSyntaxLexical', 'newSort': newSort, 'oldSort': oldSort, 'att': att} + def isKSyntaxLexical(k): return k['node'] == 'KSyntaxLexical' -def KImport(name, public = True): - return { 'node': 'KImport', 'name': name, 'isPublic': public } + +def KImport(name, public=True): + return {'node': 'KImport', 'name': name, 'isPublic': public} + def isKImport(k): return k['node'] == 'KImport' -def KFlatModule(name, imports, localSentences, att = None): - return { 'node': 'KFlatModule', 'name': name, 'imports': imports, 'localSentences': localSentences, 'att': att } + +def KFlatModule(name, imports, localSentences, att=None): + return {'node': 'KFlatModule', 'name': name, 'imports': imports, 'localSentences': localSentences, 'att': att} + def isKFlatModule(k): return k['node'] == 'KFlatModule' + def KRequire(krequire): - return { 'node': 'KRequire', 'require': krequire } + return {'node': 'KRequire', 'require': krequire} + def isKRequire(k): return k['node'] == 'KRequire' -def KDefinition(mainModule, modules, requires = None, att = None): - return { 'node': 'KDefinition', 'mainModule': mainModule, 'modules': modules, 'requires': requires, 'att': att } + +def KDefinition(mainModule, modules, requires=None, att=None): + return {'node': 'KDefinition', 'mainModule': mainModule, 'modules': modules, 'requires': requires, 'att': att} + def isKDefinition(k): return k['node'] == 'KDefinition' + def isCellKLabel(label): return len(label) > 1 and label[0] == '<' and label[-1] == '>' + def getAttribute(k, key): """Returns the value of the attribute if present, None otherwise. @@ -177,6 +229,7 @@ def getAttribute(k, key): return katts[key] return None + def addAttributes(kast, att): """Returns the input Kast with the given attributes added. @@ -187,17 +240,18 @@ def addAttributes(kast, att): return KAtt(combine_dicts(att, kast['att'])) newAtt = KAtt(att) if not ('att' in kast and kast['att'] is not None and isKAtt(kast['att'])) else addAttributes(kast['att'], att) if isKRule(kast): - return KRule(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = newAtt) + return KRule(kast['body'], requires=kast['requires'], ensures=kast['ensures'], att=newAtt) if isKClaim(kast): - return KClaim(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = newAtt) + return KClaim(kast['body'], requires=kast['requires'], ensures=kast['ensures'], att=newAtt) if isKProduction(kast): - return KProduction(kast['productionItems'], kast['sort'], att = newAtt) + return KProduction(kast['productionItems'], kast['sort'], att=newAtt) else: notif('Do not know how to add attributes to KAST!') sys.stderr.write(str(kast)) sys.stderr.flush() sys.exit(1) + def flattenLabel(label, kast): """Given a cons list, return a flat Python list of the elements. @@ -205,36 +259,42 @@ def flattenLabel(label, kast): - Output: Items of cons list. """ if isKApply(kast) and kast['label'] == label: - items = [ flattenLabel(label, arg) for arg in kast['args'] ] - return [ c for cs in items for c in cs ] + items = [flattenLabel(label, arg) for arg in kast['args']] + return [c for cs in items for c in cs] return [kast] -klabelCells = '#KCells' -klabelEmptyK = '#EmptyK' +klabelCells = '#KCells' +klabelEmptyK = '#EmptyK' ktokenDots = KToken('...', 'K') + def paren(printer): return (lambda *args: '( ' + printer(*args) + ' )') + def binOpStr(symbol): return (lambda a1, a2: a1 + ' ' + symbol + ' ' + a2) + def appliedLabelStr(symbol): return (lambda *args: symbol + ' ( ' + ' , '.join(args) + ' )') + def constLabel(symbol): return (lambda: symbol) + def assocWithUnit(assocJoin, unit): def _assocWithUnit(*args): - newArgs = [ arg for arg in args if arg != unit ] + newArgs = [arg for arg in args if arg != unit] return assocJoin.join(newArgs) return _assocWithUnit + def underbarUnparsing(symbol): splitSymbol = symbol.split('_') - numArgs = len([symb for symb in splitSymbol if symb == '']) + def _underbarUnparsing(*args): result = [] i = 0 @@ -245,15 +305,19 @@ def _underbarUnparsing(*args): result.append(args[i]) i += 1 return ' '.join(result) + return _underbarUnparsing -def indent(input, size = 2): - return '\n'.join([(' ' * size) + l for l in input.split('\n')]) + +def indent(input, size=2): + return '\n'.join([(' ' * size) + line for line in input.split('\n')]) + def newLines(input): return '\n'.join(input) -def buildSymbolTable(definition, opinionated = False): + +def buildSymbolTable(definition, opinionated=False): """Build the unparsing symbol table given a JSON encoded definition. - Input: JSON encoded K definition. @@ -271,7 +335,7 @@ def _unparserFromProductionItems(prodItems): unparseString += '_' return underbarUnparsing(unparseString) - symbolTable = { } + symbolTable = {} for module in definition['modules']: for sent in module['localSentences']: if isKProduction(sent) and 'klabel' in sent: @@ -282,16 +346,18 @@ def _unparserFromProductionItems(prodItems): symbolTable[label] = unparser if opinionated: - symbolTable [ '#And' ] = lambda c1, c2: c1 + '\n#And ' + c2 - symbolTable [ '#Or' ] = lambda c1, c2: c1 + '\n#Or\n' + indent(c2, size = 4) + symbolTable['#And'] = lambda c1, c2: c1 + '\n#And ' + c2 + symbolTable['#Or'] = lambda c1, c2: c1 + '\n#Or\n' + indent(c2, size=4) return symbolTable + def readKastTerm(termPath): with open(termPath, 'r') as termFile: return json.loads(termFile.read())['term'] -def prettyPrintKastBool(kast, symbolTable, debug = False): + +def prettyPrintKastBool(kast, symbolTable, debug=False): """Print out KAST requires/ensures clause. - Input: KAST Bool for requires/ensures clause. @@ -302,19 +368,23 @@ def prettyPrintKastBool(kast, symbolTable, debug = False): sys.stderr.write('\n') sys.stderr.flush() if isKApply(kast) and kast['label'] in ['_andBool_', '_orBool_']: - clauses = [ prettyPrintKastBool(c, symbolTable, debug = debug) for c in flattenLabel(kast['label'], kast) ] - head = kast['label'].replace('_', ' ') + clauses = [prettyPrintKastBool(c, symbolTable, debug=debug) for c in flattenLabel(kast['label'], kast)] + head = kast['label'].replace('_', ' ') if head == ' orBool ': head = ' orBool ' - separator = ' ' * (len(head) - 7) - spacer = ' ' * len(head) - joinSep = lambda s: ('\n' + separator).join(s.split('\n')) - clauses = ['( ' + joinSep(clauses[0])] + [ head + '( ' + joinSep(c) for c in clauses[1:] ] + [spacer + (')' * len(clauses))] + separator = ' ' * (len(head) - 7) + spacer = ' ' * len(head) + + def joinSep(s): + return ('\n' + separator).join(s.split('\n')) + + clauses = ['( ' + joinSep(clauses[0])] + [head + '( ' + joinSep(c) for c in clauses[1:]] + [spacer + (')' * len(clauses))] return '\n'.join(clauses) else: - return prettyPrintKast(kast, symbolTable, debug = debug) + return prettyPrintKast(kast, symbolTable, debug=debug) -def prettyPrintKast(kast, symbolTable, debug = False): + +def prettyPrintKast(kast, symbolTable, debug=False): """Print out KAST terms/outer syntax. - Input: KAST term. @@ -332,32 +402,32 @@ def prettyPrintKast(kast, symbolTable, debug = False): return kast['token'] if isKApply(kast): label = kast['label'] - args = kast['args'] - unparsedArgs = [ prettyPrintKast(arg, symbolTable, debug = debug) for arg in args ] + args = kast['args'] + unparsedArgs = [prettyPrintKast(arg, symbolTable, debug=debug) for arg in args] if isCellKLabel(label): cellContents = '\n'.join(unparsedArgs).rstrip() - cellStr = label + '\n' + indent(cellContents) + '\n ' + rhsStr + ' )' if isKSequence(kast): if len(kast['items']) == 0: - return prettyPrintKast(KConstant(klabelEmptyK), symbolTable, debug = debug) + return prettyPrintKast(KConstant(klabelEmptyK), symbolTable, debug=debug) if len(kast['items']) == 1: - return prettyPrintKast(kast['items'][0], symbolTable, debug = debug) - unparsedKSequence = '\n~> '.join([ prettyPrintKast(item, symbolTable, debug = debug) for item in kast['items'][0:-1] ]) + return prettyPrintKast(kast['items'][0], symbolTable, debug=debug) + unparsedKSequence = '\n~> '.join([prettyPrintKast(item, symbolTable, debug=debug) for item in kast['items'][0:-1]]) if kast['items'][-1] == ktokenDots: - unparsedKSequence = unparsedKSequence + '\n' + prettyPrintKast(ktokenDots, symbolTable, debug = debug) + unparsedKSequence = unparsedKSequence + '\n' + prettyPrintKast(ktokenDots, symbolTable, debug=debug) else: - unparsedKSequence = unparsedKSequence + '\n~> ' + prettyPrintKast(kast['items'][-1], symbolTable, debug = debug) + unparsedKSequence = unparsedKSequence + '\n~> ' + prettyPrintKast(kast['items'][-1], symbolTable, debug=debug) return unparsedKSequence if isKSort(kast): return kast['name'] @@ -366,89 +436,86 @@ def prettyPrintKast(kast, symbolTable, debug = False): if isKRegexTerminal(kast): return 'r"' + kast['regex'] + '"' if isKNonTerminal(kast): - return prettyPrintKast(kast['sort'], symbolTable, debug = debug) + return prettyPrintKast(kast['sort'], symbolTable, debug=debug) if isKProduction(kast): if getAttribute(kast, 'klabel') is None and 'klabel' in kast: - kast = addAttributes(kast, {'klabel' : kast['klabel']}) - sortStr = prettyPrintKast(kast['sort'], symbolTable, debug = debug) - productionStr = ' '.join([ prettyPrintKast(pi, symbolTable, debug = debug) for pi in kast['productionItems'] ]) - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + kast = addAttributes(kast, {'klabel': kast['klabel']}) + sortStr = prettyPrintKast(kast['sort'], symbolTable, debug=debug) + productionStr = ' '.join([prettyPrintKast(pi, symbolTable, debug=debug) for pi in kast['productionItems']]) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return 'syntax ' + sortStr + ' ::= ' + productionStr + ' ' + attStr if isKSyntaxSort(kast): - sortStr = prettyPrintKast(kast['sort'], symbolTable, debug = debug) - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + sortStr = prettyPrintKast(kast['sort'], symbolTable, debug=debug) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return 'syntax ' + sortStr + ' ' + attStr if isKSortSynonym(kast): - newSortStr = prettyPrintKast(kast['newSort'], symbolTable, debug = debug) - oldSortStr = prettyPrintKast(kast['oldSort'], symbolTable, debug = debug) - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + newSortStr = prettyPrintKast(kast['newSort'], symbolTable, debug=debug) + oldSortStr = prettyPrintKast(kast['oldSort'], symbolTable, debug=debug) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return 'syntax ' + newSortStr + ' = ' + oldSortStr + ' ' + attStr if isKSyntaxLexical(kast): nameStr = kast['name'] regexStr = kast['regex'] - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) # todo: proper escaping - return 'syntax lexical ' + name + ' = r"' + regex + '" ' + attStr + return 'syntax lexical ' + nameStr + ' = r"' + regexStr + '" ' + attStr if isKSyntaxAssociativity(kast): assocStr = kast['assoc'].lower() - tagsStr = ' '.join(kast['tags']) - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + tagsStr = ' '.join(kast['tags']) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return 'syntax associativity ' + assocStr + ' ' + tagsStr + ' ' + attStr if isKSyntaxPriority(kast): - prioritiesStr = ' > '.join([ ' '.join(group) for group in kast['priorities'] ]) - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + prioritiesStr = ' > '.join([' '.join(group) for group in kast['priorities']]) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return 'syntax priority ' + prioritiesStr + ' ' + attStr if isKBubble(kast): body = '// KBubble(' + kast['sentenceType'] + ', ' + kast['contents'] + ')' - attStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + attStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) return body + ' ' + attStr if isKRule(kast) or isKClaim(kast): - body = '\n '.join(prettyPrintKast(kast['body'], symbolTable, debug = debug).split('\n')) - ruleStr = 'rule ' if isKRule(kast) else 'claim ' + body = '\n '.join(prettyPrintKast(kast['body'], symbolTable, debug=debug).split('\n')) + ruleStr = 'rule ' if isKRule(kast) else 'claim ' if getAttribute(kast, 'label') is not None: ruleStr = ruleStr + '[' + getAttribute(kast, 'label') + ']:' - ruleStr = ruleStr + ' ' + body - attsStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + ruleStr = ruleStr + ' ' + body + attsStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) if kast['requires'] is not None: - requiresStr = 'requires ' + '\n '.join(prettyPrintKastBool(kast['requires'], symbolTable, debug = debug).split('\n')) + requiresStr = 'requires ' + '\n '.join(prettyPrintKastBool(kast['requires'], symbolTable, debug=debug).split('\n')) ruleStr = ruleStr + '\n ' + requiresStr if kast['ensures'] is not None: - ensuresStr = 'ensures ' + '\n '.join(prettyPrintKastBool(kast['ensures'], symbolTable, debug = debug).split('\n')) + ensuresStr = 'ensures ' + '\n '.join(prettyPrintKastBool(kast['ensures'], symbolTable, debug=debug).split('\n')) ruleStr = ruleStr + '\n ' + ensuresStr return ruleStr + '\n ' + attsStr if isKContext(kast): - body = indent(prettyPrintKast(kast['body'], symbolTable, debug = debug)) - contextStr = 'context alias ' + body + body = indent(prettyPrintKast(kast['body'], symbolTable, debug=debug)) + contextStr = 'context alias ' + body requiresStr = '' - attsStr = prettyPrintKast(kast['att'], symbolTable, debug = debug) + attsStr = prettyPrintKast(kast['att'], symbolTable, debug=debug) if kast['requires'] is not None: - requiresStr = prettyPrintKast(kast['requires'], symbolTable, debug = debug) + requiresStr = prettyPrintKast(kast['requires'], symbolTable, debug=debug) requiresStr = 'requires ' + indent(requiresStr) return contextStr + '\n ' + requiresStr + '\n ' + attsStr if isKAtt(kast): if len(kast['att']) == 0: return '' - attStrs = [ att + '(' + kast['att'][att] + ')' for att in kast['att'].keys() ] + attStrs = [att + '(' + kast['att'][att] + ')' for att in kast['att'].keys()] return '[' + ', '.join(attStrs) + ']' if isKImport(kast): return ' '.join(['imports', ('public' if kast['isPublic'] else 'private'), kast['name']]) if isKFlatModule(kast): name = kast['name'] - imports = '\n'.join([prettyPrintKast(kimport, symbolTable, debug = debug) for kimport in kast['imports']]) - localSentences = '\n\n'.join([prettyPrintKast(sent, symbolTable, debug = debug) for sent in kast['localSentences']]) + imports = '\n'.join([prettyPrintKast(kimport, symbolTable, debug=debug) for kimport in kast['imports']]) + localSentences = '\n\n'.join([prettyPrintKast(sent, symbolTable, debug=debug) for sent in kast['localSentences']]) contents = imports + '\n\n' + localSentences - return 'module ' + name + '\n ' \ - + '\n '.join(contents.split('\n')) + '\n' \ - + 'endmodule' + return 'module ' + name + '\n ' + '\n '.join(contents.split('\n')) + '\nendmodule' if isKRequire(kast): return 'requires "' + kast['require'] + '"' if isKDefinition(kast): - requires = '' if kast['requires'] is None else '\n'.join([prettyPrintKast(require, symbolTable, debug = debug) for require in kast['requires']]) - modules = '\n\n'.join([prettyPrintKast(module, symbolTable, debug = debug) for module in kast['modules']]) + requires = '' if kast['requires'] is None else '\n'.join([prettyPrintKast(require, symbolTable, debug=debug) for require in kast['requires']]) + modules = '\n\n'.join([prettyPrintKast(module, symbolTable, debug=debug) for module in kast['modules']]) return requires + '\n\n' + modules print() warning('Error unparsing kast!') print(kast) fatal('Error unparsing!') - From fd5632542d4a30723e5673ec3d75dab9017cea73 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 18:08:21 +0100 Subject: [PATCH 09/16] Organize imports in __main__ --- .../src/main/scripts/lib/pyk/__main__.py | 32 ++++++++++++++----- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__main__.py b/k-distribution/src/main/scripts/lib/pyk/__main__.py index 48a9d01e769..61f5f08db79 100644 --- a/k-distribution/src/main/scripts/lib/pyk/__main__.py +++ b/k-distribution/src/main/scripts/lib/pyk/__main__.py @@ -1,13 +1,29 @@ -#!/usr/bin/env python3 - import argparse -from graphviz import Digraph -import tempfile +import json import os.path as path import sys - -from . import * -from .cli_utils import notif, warning +from pathlib import Path + +from graphviz import Digraph + +from .cli_utils import fatal, notif, warning +from .coverage import getRuleById, stripCoverageLogger +from .kast import ( + KApply, + KConstant, + buildSymbolTable, + flattenLabel, + prettyPrintKast, + readKastTerm, +) +from .kastManip import ( + buildAssoc, + minimizeRule, + minimizeTerm, + propagateUpConstraints, + removeSourceMap, + splitConfigAndConstraints, +) from .ktool import KPrint, KProve pykArgs = argparse.ArgumentParser() @@ -98,7 +114,7 @@ def main(commandLineArgs, extraMain = None): extraMain(args, kompiled_dir) if returncode != 0: - _fatal('Non-zero exit code (' + str(returncode) + '): ' + str(kCommand), code = returncode) + fatal('Non-zero exit code (' + str(returncode) + '): ' + str(args['command'])) if __name__ == '__main__': # KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...). From 21716118721a51782e8ebaea4c93f3846a88ca44 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 18:12:57 +0100 Subject: [PATCH 10/16] Fix linting issues in __main__ --- .../src/main/scripts/lib/pyk/__main__.py | 60 ++++++++++--------- 1 file changed, 32 insertions(+), 28 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__main__.py b/k-distribution/src/main/scripts/lib/pyk/__main__.py index 61f5f08db79..c3f0e6adf3b 100644 --- a/k-distribution/src/main/scripts/lib/pyk/__main__.py +++ b/k-distribution/src/main/scripts/lib/pyk/__main__.py @@ -26,53 +26,56 @@ ) from .ktool import KPrint, KProve + pykArgs = argparse.ArgumentParser() -pykArgs.add_argument('kompiled-dir', type = str, help = 'Kompiled directory for definition.') +pykArgs.add_argument('kompiled-dir', type=str, help='Kompiled directory for definition.') + +pykCommandParsers = pykArgs.add_subparsers(dest='command') -pykCommandParsers = pykArgs.add_subparsers(dest = 'command') +kprintArgs = pykCommandParsers.add_parser('print', help='Pretty print a term.') +kprintArgs.add_argument('term', type=argparse.FileType('r'), help='Input term (in JSON).') +kprintArgs.add_argument('--minimize', default=True, action='store_true', help='Minimize the JSON configuration before printing.') +kprintArgs.add_argument('--no-minimize', dest='minimize', action='store_false', help='Do not minimize the JSON configuration before printing.') +kprintArgs.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.') +kprintArgs.add_argument('--output-file', type=argparse.FileType('w'), default='-') -kprintArgs = pykCommandParsers.add_parser('print', help = 'Pretty print a term.') -kprintArgs.add_argument('term', type = argparse.FileType('r'), help = 'Input term (in JSON).') -kprintArgs.add_argument('--minimize', default = True, action = 'store_true', help = 'Minimize the JSON configuration before printing.') -kprintArgs.add_argument('--no-minimize', dest = 'minimize', action = 'store_false', help = 'Do not minimize the JSON configuration before printing.') -kprintArgs.add_argument('--omit-labels', default = '', nargs = '?', help = 'List of labels to omit from output.') -kprintArgs.add_argument('--output-file', type = argparse.FileType('w'), default = '-') +kproveArgs = pykCommandParsers.add_parser('prove', help='Prove an input specification (using kprovex).') +kproveArgs.add_argument('main-file', type=str, help='Main file used for kompilation.') +kproveArgs.add_argument('spec-file', type=str, help='File with the specification module.') +kproveArgs.add_argument('spec-module', type=str, help='Module with claims to be proven.') +kproveArgs.add_argument('--output-file', type=argparse.FileType('w'), default='-') +kproveArgs.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.') -kproveArgs = pykCommandParsers.add_parser('prove', help = 'Prove an input specification (using kprovex).') -kproveArgs.add_argument('main-file', type = str, help = 'Main file used for kompilation.') -kproveArgs.add_argument('spec-file', type = str, help = 'File with the specification module.') -kproveArgs.add_argument('spec-module', type = str, help = 'Module with claims to be proven.') -kproveArgs.add_argument('--output-file', type = argparse.FileType('w'), default = '-') -kproveArgs.add_argument('kArgs', nargs='*', help = 'Arguments to pass through to K invocation.') +graphImportsArgs = pykCommandParsers.add_parser('graph-imports', help='Graph the imports of a given definition.') -graphImportsArgs = pykCommandParsers.add_parser('graph-imports', help = 'Graph the imports of a given definition.') +coverageArgs = pykCommandParsers.add_parser('coverage', help='Convert coverage file to human readable log.') +coverageArgs.add_argument('coverage-file', type=argparse.FileType('r'), help='Coverage file to build log for.') +coverageArgs.add_argument('-o', '--output', type=argparse.FileType('w'), default='-') -coverageArgs = pykCommandParsers.add_parser('coverage', help = 'Convert coverage file to human readable log.') -coverageArgs.add_argument('coverage-file', type = argparse.FileType('r'), help = 'Coverage file to build log for.') -coverageArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-') def definitionDir(kompiledDir): return path.dirname(path.abspath(kompiledDir)) -def main(commandLineArgs, extraMain = None): + +def main(commandLineArgs, extraMain=None): returncode = 0 args = vars(commandLineArgs.parse_args()) kompiled_dir = Path(args['kompiled-dir']) if args['command'] == 'print': printer = KPrint(kompiled_dir) - term = json.loads(args['term'].read()) + term = json.loads(args['term'].read()) if 'term' in term: term = term['term'] if term == KConstant('#Top'): args['output_file'].write(printer.prettyPrint(term)) else: if args['minimize']: - abstractLabels = [] if args['omit_labels'] is None else args['omit_labels'].split(',') + abstractLabels = [] if args['omit_labels'] is None else args['omit_labels'].split(',') minimizedDisjuncts = [] for d in flattenLabel('#Or', term): - dMinimized = minimizeTerm(d, abstractLabels = abstractLabels) - (dConfig, dConstraint) = splitConfigAndConstraints(dMinimized) + dMinimized = minimizeTerm(d, abstractLabels=abstractLabels) + dConfig, dConstraint = splitConfigAndConstraints(dMinimized) if dConstraint != KConstant('#Top'): minimizedDisjuncts.append(KApply('#And', [dConfig, dConstraint])) else: @@ -81,17 +84,17 @@ def main(commandLineArgs, extraMain = None): args['output_file'].write(printer.prettyPrint(term)) elif args['command'] == 'prove': - kprover = KProve(kompiled_dir, args['main-file']) - finalState = kprover.prove(Path(args['spec-file']), args['spec-module'], args = args['kArgs']) + kprover = KProve(kompiled_dir, args['main-file']) + finalState = kprover.prove(Path(args['spec-file']), args['spec-module'], args=args['kArgs']) args['output_file'].write(json.dumps(finalState)) if finalState != KConstant('#Top'): warning('Proof failed!') elif args['command'] == 'graph-imports': - kprinter = KPrint(kompiled_dir) - kDefn = kprinter.definition + kprinter = KPrint(kompiled_dir) + kDefn = kprinter.definition importGraph = Digraph() - graphFile = kompiled_dir / 'import-graph' + graphFile = kompiled_dir / 'import-graph' for module in kDefn['modules']: modName = module['name'] importGraph.node(modName) @@ -116,6 +119,7 @@ def main(commandLineArgs, extraMain = None): if returncode != 0: fatal('Non-zero exit code (' + str(returncode) + '): ' + str(args['command'])) + if __name__ == '__main__': # KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...). # Most pyk operations are defined recursively, meaning you get a callstack the same depth as the term. From 52ada89f21bda5aaf2fd49305c0576429e81a790 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 18:13:42 +0100 Subject: [PATCH 11/16] Remove re-exports from __init__ --- k-distribution/src/main/scripts/lib/pyk/__init__.py | 11 ----------- k-distribution/tests/pyk/unit_test.py | 8 +++----- 2 files changed, 3 insertions(+), 16 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__init__.py b/k-distribution/src/main/scripts/lib/pyk/__init__.py index 6160b0daec9..e69de29bb2d 100755 --- a/k-distribution/src/main/scripts/lib/pyk/__init__.py +++ b/k-distribution/src/main/scripts/lib/pyk/__init__.py @@ -1,11 +0,0 @@ -#!/usr/bin/env python3 - -import os -import subprocess -import sys -import tempfile - -from .kast import * -from .kastManip import * -from .coverage import * -from .ktool import * diff --git a/k-distribution/tests/pyk/unit_test.py b/k-distribution/tests/pyk/unit_test.py index d1ddd398811..82bdc3f1110 100644 --- a/k-distribution/tests/pyk/unit_test.py +++ b/k-distribution/tests/pyk/unit_test.py @@ -1,12 +1,10 @@ -#!/usr/bin/env python3 - import sys import unittest - from functools import reduce -# From K's pyk-library -from pyk import * +from pyk.kast import KApply, KConstant, KSequence, KVariable, newLines +from pyk.kastManip import splitConfigFrom + class TestPyk(unittest.TestCase): From d2e5cb403aa6da191bd251be9d05699bc5593205 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 18:15:29 +0100 Subject: [PATCH 12/16] Fix file permissions --- k-distribution/src/main/scripts/lib/pyk/__init__.py | 0 k-distribution/src/main/scripts/lib/pyk/coverage.py | 0 2 files changed, 0 insertions(+), 0 deletions(-) mode change 100755 => 100644 k-distribution/src/main/scripts/lib/pyk/__init__.py mode change 100755 => 100644 k-distribution/src/main/scripts/lib/pyk/coverage.py diff --git a/k-distribution/src/main/scripts/lib/pyk/__init__.py b/k-distribution/src/main/scripts/lib/pyk/__init__.py old mode 100755 new mode 100644 diff --git a/k-distribution/src/main/scripts/lib/pyk/coverage.py b/k-distribution/src/main/scripts/lib/pyk/coverage.py old mode 100755 new mode 100644 From 6f0613a46a8f789b9519eab6230f3f221d1d4a22 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Fri, 18 Feb 2022 09:55:44 +0100 Subject: [PATCH 13/16] Add Summarizer hash utility functions to utils Co-authored-by: Everett Hildenbrandt --- .../src/main/scripts/lib/pyk/utils.py | 55 +++++++++++++++++-- 1 file changed, 49 insertions(+), 6 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index ae9ee0da338..0ea83099684 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -1,4 +1,5 @@ import hashlib +import string from typing import Any, Dict, Iterable, List, Mapping, Optional, Tuple, TypeVar T = TypeVar('T') @@ -59,12 +60,6 @@ def dedupe(xs: Iterable[T]) -> List[T]: return res -def hash_str(x: Any) -> str: - hash = hashlib.sha256() - hash.update(str(x).encode('utf-8')) - return str(hash.hexdigest()) - - def nonempty_str(x: Any) -> str: if x is None: raise ValueError('Expected nonempty string, found: null.') @@ -73,3 +68,51 @@ def nonempty_str(x: Any) -> str: if x == '': raise ValueError("Expected nonempty string, found: ''") return x + + +# Hashes + +def hash_str(x: Any) -> str: + hash = hashlib.sha256() + hash.update(str(x).encode('utf-8')) + return str(hash.hexdigest()) + + +def is_hash(x: Any) -> bool: + # NB! currently only sha256 in hexdec form is detected + # 2b9e b7c5 441e 9f7e 97f9 a4e5 fc04 a0f7 9f62 c8e9 605a ad1e 02db e8de 3c21 0422 + # 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 + return type(x) is str and len(x) == 64 and all(c in string.hexdigits for c in x) + + +def shorten_hash(h: str, leftChars=6, rightChars=6) -> str: + left = h[0:leftChars] if leftChars > 0 else '' + right = h[-rightChars:] if rightChars > 0 else '' + return left + ".." + right + + +def shorten_hashes(value: Any, leftChars=6, rightChars=6) -> Any: + result: Any = None + if is_hash(value): + result = shorten_hash(value, leftChars, rightChars) + elif type(value) is tuple: + result = tuple([shorten_hashes(item) for item in value]) + elif type(value) is list: + result = [shorten_hashes(v) for v in value] + elif type(value) is dict: + result = {} + for (k, v) in value.items(): + result[shorten_hashes(k)] = shorten_hashes(v) + elif type(value) is set: + result = set() + for item in value: + result.add(shorten_hashes(item)) + else: + result = value + return result + + +def compare_short_hashes(lhs: str, rhs: str): + left, right = lhs.split('.'), rhs.split('.') + (l0, l1, r0, r1) = (left[0].upper(), left[-1].upper(), right[0].upper(), right[-1].upper()) + return (l0.startswith(r0) or r0.startswith(l0)) and (l1.endswith(r1) or r1.endswith(l1)) From 1fba293d9f1720b79b742f86b4df290d60cff931 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Fri, 18 Feb 2022 10:23:51 +0100 Subject: [PATCH 14/16] Add module prelude --- .../src/main/scripts/lib/pyk/__main__.py | 3 +- .../src/main/scripts/lib/pyk/kastManip.py | 84 ++----------------- .../src/main/scripts/lib/pyk/prelude.py | 76 +++++++++++++++++ 3 files changed, 86 insertions(+), 77 deletions(-) create mode 100644 k-distribution/src/main/scripts/lib/pyk/prelude.py diff --git a/k-distribution/src/main/scripts/lib/pyk/__main__.py b/k-distribution/src/main/scripts/lib/pyk/__main__.py index c3f0e6adf3b..648049b922c 100644 --- a/k-distribution/src/main/scripts/lib/pyk/__main__.py +++ b/k-distribution/src/main/scripts/lib/pyk/__main__.py @@ -17,7 +17,6 @@ readKastTerm, ) from .kastManip import ( - buildAssoc, minimizeRule, minimizeTerm, propagateUpConstraints, @@ -25,7 +24,7 @@ splitConfigAndConstraints, ) from .ktool import KPrint, KProve - +from .prelude import buildAssoc pykArgs = argparse.ArgumentParser() pykArgs.add_argument('kompiled-dir', type=str, help='Kompiled directory for definition.') diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 73a0f32c45f..6bd111429a8 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -46,36 +46,18 @@ klabelEmptyK, ktokenDots, ) +from .prelude import ( + buildAssoc, + mlAnd, + mlEquals, + mlEqualsTrue, + mlImplies, + mlOr, + mlTop, +) from .utils import combine_dicts, dedupe, find_common_items, hash_str -def buildAssoc(unit, join, ls): - """Build an associative binary operator term given the join and unit ops. - - - Input: unit, join, and list of elements to join. - - Output: cons-list style construction of the joined term. - """ - ls = list(filter(lambda l: l != unit, ls)) - if len(ls) == 0: - return unit - if len(ls) == 1: - return ls[0] - if ls[0] == unit: - return buildAssoc(unit, join, ls[1:]) - return KApply(join, [ls[0], buildAssoc(unit, join, ls[1:])]) - - -def buildCons(unit, cons, ls): - """Build a cons operator term given the cons and unit ops. - - - Input: unit, cons, and list of elements to join. - - Output: cons-list style construction of the joined term. - """ - if len(ls) == 0: - return unit - return KApply(cons, [ls[0], buildCons(unit, cons, ls[1:])]) - - def match(pattern, kast): """Perform syntactic pattern matching and return the substitution. @@ -598,54 +580,6 @@ def _removeSourceMap(att): return onAttributes(k, _removeSourceMap) -def boolToken(b): - return KToken(str(b).lower(), 'Bool') - - -def intToken(i): - return KToken(str(i), 'Int') - - -def stringToken(s): - return KToken('"' + s + '"', 'String') - - -def ltInt(i1, i2): - return KApply('_ and from a configuration. diff --git a/k-distribution/src/main/scripts/lib/pyk/prelude.py b/k-distribution/src/main/scripts/lib/pyk/prelude.py new file mode 100644 index 00000000000..d82a9113329 --- /dev/null +++ b/k-distribution/src/main/scripts/lib/pyk/prelude.py @@ -0,0 +1,76 @@ +from .kast import KApply, KConstant, KToken + + +def buildAssoc(unit, join, ls): + """Build an associative binary operator term given the join and unit ops. + + - Input: unit, join, and list of elements to join. + - Output: cons-list style construction of the joined term. + """ + ls = list(filter(lambda l: l != unit, ls)) + if len(ls) == 0: + return unit + if len(ls) == 1: + return ls[0] + if ls[0] == unit: + return buildAssoc(unit, join, ls[1:]) + return KApply(join, [ls[0], buildAssoc(unit, join, ls[1:])]) + + +def buildCons(unit, cons, ls): + """Build a cons operator term given the cons and unit ops. + + - Input: unit, cons, and list of elements to join. + - Output: cons-list style construction of the joined term. + """ + if len(ls) == 0: + return unit + return KApply(cons, [ls[0], buildCons(unit, cons, ls[1:])]) + + +def boolToken(b): + return KToken(str(b).lower(), 'Bool') + + +def intToken(i): + return KToken(str(i), 'Int') + + +def stringToken(s): + return KToken('"' + s + '"', 'String') + + +def ltInt(i1, i2): + return KApply('_ Date: Fri, 18 Feb 2022 10:29:38 +0100 Subject: [PATCH 15/16] Remove unused functions from kastManip --- .../src/main/scripts/lib/pyk/kastManip.py | 35 ------------------- 1 file changed, 35 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 6bd111429a8..5c0e4d7b75d 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -857,41 +857,6 @@ def substToMap(subst): return buildAssoc(KConstant('.Map'), '_Map_', mapItems) -def setAttribute(k, key, value): - if 'att' in k and k['att'] is not None and isKAtt(k['att']): - k['att']['att'][key] = value - return k - - -def getLHS(kast): - def _getLHS(_k): - if isKRewrite(_k): - return _k['lhs'] - return _k - return traverseBottomUp(kast, _getLHS) - - -def getRHS(kast): - def _getRHS(_k): - if isKRewrite(_k): - return _k['rhs'] - return _k - return traverseBottomUp(kast, _getRHS) - - -def markExistentialVars(constrainedTerm): - (config, constraint) = splitConfigAndConstraints(constrainedTerm) - configLhs = getLHS(config) - configRhs = getRHS(config) - lhsOccurances = countVarOccurances(configLhs) - rhsOccurances = countVarOccurances(configRhs) - subst = {} - for v in rhsOccurances: - if v not in lhsOccurances: - subst[v] = KVariable('?' + v) - return substitute(mlAnd([config, constraint]), subst) - - def undoAliases(definition, kast): alias_undo_rewrites = [(sent['body']['rhs'], sent['body']['lhs']) for module in definition['modules'] for sent in module['localSentences'] if isKRule(sent) and getAttribute(sent, 'alias') is not None] newKast = kast From 6ca20b24d9c3113170323279bc7409769170ad97 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Fri, 18 Feb 2022 10:55:18 +0100 Subject: [PATCH 16/16] Add Makefile with linter checks --- k-distribution/src/main/scripts/lib/.isort.cfg | 4 ++++ k-distribution/src/main/scripts/lib/Makefile | 16 ++++++++++++++++ 2 files changed, 20 insertions(+) create mode 100644 k-distribution/src/main/scripts/lib/.isort.cfg create mode 100644 k-distribution/src/main/scripts/lib/Makefile diff --git a/k-distribution/src/main/scripts/lib/.isort.cfg b/k-distribution/src/main/scripts/lib/.isort.cfg new file mode 100644 index 00000000000..07fd65c992a --- /dev/null +++ b/k-distribution/src/main/scripts/lib/.isort.cfg @@ -0,0 +1,4 @@ +[settings] +multi_line_output=3 +include_trailing_comma=true +ensure_newline_before_comments=true diff --git a/k-distribution/src/main/scripts/lib/Makefile b/k-distribution/src/main/scripts/lib/Makefile new file mode 100644 index 00000000000..a83c8fbc787 --- /dev/null +++ b/k-distribution/src/main/scripts/lib/Makefile @@ -0,0 +1,16 @@ +.PHONY: all test test-code-style test-flake8 test-isort isort + +all: test + +test: test-code-style + +test-code-style: test-flake8 test-isort + +test-flake8: + flake8 . --ignore=E501 + +test-isort: + isort . --check + +isort: + isort .