Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Remove support for antiLeft rules and aliases #4039

Merged
merged 3 commits into from
Aug 19, 2024
Merged

Remove support for antiLeft rules and aliases #4039

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4afb68a
Remove support for antiLeft rules and aliases
goodlyrottenapple Aug 19, 2024
1200121
fix tests
goodlyrottenapple Aug 19, 2024
14ecb2c
Merge branch 'master' into sam/remove-antileft-aliases
rv-jenkins Aug 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 0 additions & 13 deletions booster/library/Booster/Definition/Base.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ data KoreDefinition = KoreDefinition
, modules :: Map ByteString ModuleAttributes
, sorts :: Map SortName (SortAttributes, Set SortName)
, symbols :: Map SymbolName Symbol -- constructors and functions
, aliases :: Map AliasName Alias
, rewriteTheory :: Theory (RewriteRule "Rewrite")
, functionEquations :: Theory (RewriteRule "Function")
, simplifications :: Theory (RewriteRule "Simplification")
Expand All @@ -63,7 +62,6 @@ emptyKoreDefinition attributes =
, modules = Map.empty
, sorts = Map.empty
, symbols = Map.empty
, aliases = Map.empty
, rewriteTheory = Map.empty
, functionEquations = Map.empty
, simplifications = Map.empty
Expand All @@ -80,17 +78,6 @@ data RewriteRule (tag :: k) = RewriteRule
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)

type AliasName = ByteString

data Alias = Alias
{ name :: AliasName
, params :: [Sort]
, args :: [Variable]
, rhs :: Term
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)

data SourceRef
= Labeled Text
| Located Location
Expand Down
174 changes: 9 additions & 165 deletions booster/library/Booster/Syntax/ParsedKore/Internalise.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,6 @@ mergeDefs k1 k2
<$> mergeDisjoint Def.modules k1 k2
<*> mergeDisjoint Def.sorts k1 k2
<*> mergeDisjoint Def.symbols k1 k2
<*> mergeDisjoint Def.aliases k1 k2
<*> pure (mergeTheories rewriteTheory k1 k2)
<*> pure (mergeTheories functionEquations k1 k2)
<*> pure (mergeTheories simplifications k1 k2)
Expand Down Expand Up @@ -223,7 +222,6 @@ addModule
{ name = Syntax.Id n
, sorts = parsedSorts
, symbols = parsedSymbols
, aliases = parsedAliases
, axioms = parsedAxioms
}
( Imported
Expand All @@ -232,7 +230,6 @@ addModule
, modules = currentModules
, sorts = currentSorts
, symbols = currentSymbols
, aliases = currentAliases
, rewriteTheory = currentRewriteTheory
, functionEquations = currentFctEqs
, simplifications = currentSimpls
Expand Down Expand Up @@ -286,76 +283,20 @@ addModule
let symbols =
renameSmtLibDuplicates symbols'

let defWithNewSortsAndSymbols =
let def =
Partial
KoreDefinition
{ attributes = defAttributes
, modules
, sorts = sorts' -- no subsort information yet
, symbols
, aliases = currentAliases -- no aliases yet
, rewriteTheory = currentRewriteTheory -- no rules yet
, functionEquations = Map.empty
, simplifications = Map.empty
, ceils = Map.empty
}

let internaliseAlias ::
ParsedAlias ->
Except DefinitionError (Def.AliasName, Alias)
-- TODO(Ana): do we need to handle attributes?
internaliseAlias palias@ParsedAlias{name, sortVars, argSorts, sort, args, rhs} = do
unless
(length argSorts == length args)
(throwE (DefinitionAliasError name.getId . WrongAliasSortCount $ palias))
let paramNames = (.getId) <$> sortVars
params = Def.SortVar . textToBS <$> paramNames
argNames = textToBS . (.getId) <$> args
internalName = textToBS name.getId
internalArgSorts <-
traverse
(withExcept DefinitionSortError . internaliseSort (Set.fromList paramNames) sorts')
argSorts
internalResSort <-
withExcept DefinitionSortError $
internaliseSort (Set.fromList paramNames) sorts' sort
let internalArgs = uncurry Def.Variable <$> zip internalArgSorts argNames

(rhsTerm, predicates, ceilConditions, substitution, _unsupported) <- -- FIXME
withExcept (DefinitionAliasError name.getId . InconsistentAliasPattern . (: [])) $
internalisePattern
AllowAlias
IgnoreSubsorts
(Just sortVars)
defWithNewSortsAndSymbols.partial
rhs
unless (null substitution) $
throwE $
DefinitionAliasError name.getId $
InconsistentAliasPattern [SubstitutionNotAllowed]
unless (null predicates) $
throwE $
DefinitionAliasError name.getId $
InconsistentAliasPattern [PredicateNotAllowed]
unless (null ceilConditions) $
throwE $
DefinitionAliasError name.getId $
InconsistentAliasPattern [CeilNotAllowed]
let rhsSort = Util.sortOfTerm rhsTerm
unless
(rhsSort == internalResSort)
(throwE (DefinitionSortError (GeneralError "IncompatibleSorts")))
return (internalName, Alias{name = internalName, params, args = internalArgs, rhs = rhsTerm})
-- filter out "antiLeft" aliases, recognised by name and argument count
notPriority :: ParsedAlias -> Bool
notPriority alias =
not $ null alias.args && "priority" `Text.isPrefixOf` alias.name.getId
newAliases <- traverse internaliseAlias $ filter notPriority parsedAliases
let aliases = Map.fromList newAliases <> currentAliases

let defWithAliases :: PartialDefinition
defWithAliases = Partial defWithNewSortsAndSymbols.partial{aliases}
newAxioms <- mapMaybeM (internaliseAxiom defWithAliases) parsedAxioms
newAxioms <- mapMaybeM (internaliseAxiom def) parsedAxioms

let newRewriteRules = mapMaybe retractRewriteRule newAxioms
subsortPairs = mapMaybe retractSubsortRule newAxioms
Expand All @@ -378,7 +319,7 @@ addModule
subsortClosure sorts' subsortPairs

pure $
defWithAliases.partial
def.partial
{ sorts
, rewriteTheory
, functionEquations
Expand Down Expand Up @@ -790,16 +731,12 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom =
lhs
rhs
attribs
RewriteRuleAxiom' alias args rhs' attribs ->
let (rhs, existentials) = extractExistentials rhs'
in Just . RewriteRuleAxiom
<$> internaliseRewriteRule
partialDefinition
existentials
(textToBS alias)
args
rhs
attribs
RewriteRuleAxiom'{} ->
throwE $
DefinitionSortError $
GeneralError
( "Rules with antiLeft aliases are no longer supported. Please rekompile your definition with a newer version of K."
)
SimplificationAxiom' requires lhs rhs sortVars attribs ->
Just
<$> internaliseSimpleEquation
Expand Down Expand Up @@ -828,9 +765,6 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom =
sortVars
attribs

orFailWith :: Maybe a -> e -> Except e a
mbX `orFailWith` err = maybe (throwE err) pure mbX

internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported ::
KoreDefinition ->
SourceRef ->
Expand Down Expand Up @@ -913,85 +847,6 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
let variableName = textToBS name.getId
pure $ Variable{variableSort, variableName}

internaliseRewriteRule ::
KoreDefinition ->
[(Id, Sort)] ->
AliasName ->
[Syntax.KorePattern] ->
Syntax.KorePattern ->
AxiomAttributes ->
Except DefinitionError (RewriteRule k)
internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttributes = do
let ref = sourceRef axAttributes
alias <-
withExcept (DefinitionAliasError $ Text.decodeLatin1 aliasName) $
Map.lookup aliasName partialDefinition.aliases
`orFailWith` UnknownAlias aliasName
args <-
traverse
( withExcept (DefinitionPatternError ref)
. internaliseTerm AllowAlias IgnoreSubsorts Nothing partialDefinition
)
aliasArgs
-- prefix all variables in lhs and rhs with "Rule#" and "Ex#" to avoid
-- name clashes with patterns from the user
lhs <- Util.modifyVariablesInT (Util.modifyVarName Util.markAsRuleVar) <$> expandAlias alias args

existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs
let renameVariable v
| v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
| otherwise = Util.modifyVarName Util.markAsRuleVar v
(rhs, ensures) <-
internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
partialDefinition
ref
Nothing
renameVariable
right

let notPreservesDefinednessReasons =
-- users can override the definedness computation by an explicit attribute
if coerce axAttributes.preserving
then []
else
[ UndefinedSymbol s.name
| s <- Util.filterTermSymbols (not . Util.isDefinedSymbol) rhs
]
containsAcSymbols =
Util.checkTermSymbols Util.checkSymbolIsAc lhs
computedAttributes =
ComputedAxiomAttributes{notPreservesDefinednessReasons, containsAcSymbols}
existentials = Set.map (Util.modifyVarName Util.markAsExVar) existentials'
attributes =
axAttributes
{ concreteness = Util.modifyVarNameConcreteness Util.markAsRuleVar axAttributes.concreteness
}
return
RewriteRule
{ lhs
, rhs
, requires = mempty
, ensures
, attributes
, computedAttributes
, existentials
}
where
mkVar (name, sort) = do
variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort
let variableName = textToBS name.getId
pure $ Variable{variableSort, variableName}

expandAlias :: Alias -> [Def.Term] -> Except DefinitionError Def.Term
expandAlias alias currentArgs
| length alias.args /= length currentArgs =
throwE $
DefinitionAliasError (Text.decodeLatin1 alias.name) $
WrongAliasArgCount alias currentArgs
| otherwise = do
let substitution = Map.fromList (zip alias.args currentArgs)
pure $ Util.substituteInTerm substitution alias.rhs

{- | Internalises simplification rules, for term simplification
(represented as a 'RewriteRule').

Expand Down Expand Up @@ -1320,7 +1175,6 @@ data DefinitionError
| DefinitionAttributeError Text
| DefinitionSortError SortError
| DefinitionPatternError SourceRef PatternError
| DefinitionAliasError Text AliasError
| DefinitionAxiomError AxiomError
| DefinitionTermOrPredicateError SourceRef TermOrPredicateError
| ElemSymbolMalformed Def.Symbol
Expand Down Expand Up @@ -1349,9 +1203,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods DefinitionError
pretty $ "Sort error: " <> renderSortError @mods (PrettyWithModifiers sortErr)
DefinitionPatternError ref patErr ->
"Pattern error in " <> pretty ref <> ": " <> pretty (show patErr)
-- TODO define a pretty instance?
DefinitionAliasError name err ->
pretty $ "Alias error in " <> Text.unpack name <> ": " <> show err
DefinitionAxiomError err ->
"Bad rewrite rule " <> pretty err
DefinitionTermOrPredicateError ref (PatternExpected p) ->
Expand Down Expand Up @@ -1398,13 +1249,6 @@ definitionErrorToRpcError = \case
either (const "unknown location") pretty $
runExcept (Attributes.readLocation rule.attributes)

data AliasError
= UnknownAlias AliasName
| WrongAliasSortCount ParsedAlias
| WrongAliasArgCount Alias [Def.Term]
| InconsistentAliasPattern [PatternError]
deriving stock (Eq, Show)

data AxiomError
= MalformedRewriteRule ParsedAxiom
| MalformedEquation ParsedAxiom
Expand Down
2 changes: 0 additions & 2 deletions booster/test/llvm-integration/LLVM.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -316,7 +316,6 @@ testDef =
Map.empty -- no modules (HACK)
defSorts
defSymbols
Map.empty -- no aliases
Map.empty -- no rules
Map.empty -- no function equations
Map.empty -- no simplifications
Expand All @@ -334,7 +333,6 @@ displayTestDef = do
prunedDef =
def
{ modules = Map.empty
, aliases = Map.empty
, functionEquations = Map.empty
, simplifications = Map.empty
}
Expand Down
1 change: 0 additions & 1 deletion booster/unit-tests/Test/Booster/Fixture.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,6 @@ testDefinition =
]
<> listSymbols
<> setSymbols
, aliases = Map.empty
, rewriteTheory = Map.empty
, functionEquations = Map.empty
, simplifications = Map.empty
Expand Down
Loading