From 4afb68a61e8b461275a43d9e8ecfb03736ebe64b Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Mon, 19 Aug 2024 10:18:08 +0200 Subject: [PATCH 1/2] Remove support for antiLeft rules and aliases --- booster/library/Booster/Definition/Base.hs | 13 -- .../Booster/Syntax/ParsedKore/Internalise.hs | 174 +----------------- 2 files changed, 9 insertions(+), 178 deletions(-) diff --git a/booster/library/Booster/Definition/Base.hs b/booster/library/Booster/Definition/Base.hs index 8c51122201..fc9766d795 100644 --- a/booster/library/Booster/Definition/Base.hs +++ b/booster/library/Booster/Definition/Base.hs @@ -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") @@ -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 @@ -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 diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 342141d899..6a1acbd6f5 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -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) @@ -223,7 +222,6 @@ addModule { name = Syntax.Id n , sorts = parsedSorts , symbols = parsedSymbols - , aliases = parsedAliases , axioms = parsedAxioms } ( Imported @@ -232,7 +230,6 @@ addModule , modules = currentModules , sorts = currentSorts , symbols = currentSymbols - , aliases = currentAliases , rewriteTheory = currentRewriteTheory , functionEquations = currentFctEqs , simplifications = currentSimpls @@ -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 @@ -378,7 +319,7 @@ addModule subsortClosure sorts' subsortPairs pure $ - defWithAliases.partial + def.partial { sorts , rewriteTheory , functionEquations @@ -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 @@ -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 -> @@ -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'). @@ -1320,7 +1175,6 @@ data DefinitionError | DefinitionAttributeError Text | DefinitionSortError SortError | DefinitionPatternError SourceRef PatternError - | DefinitionAliasError Text AliasError | DefinitionAxiomError AxiomError | DefinitionTermOrPredicateError SourceRef TermOrPredicateError | ElemSymbolMalformed Def.Symbol @@ -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) -> @@ -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 From 1200121e24fc137cd4d816db5c91dcfcd86e27ce Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Mon, 19 Aug 2024 10:34:31 +0200 Subject: [PATCH 2/2] fix tests --- booster/test/llvm-integration/LLVM.hs | 2 -- booster/unit-tests/Test/Booster/Fixture.hs | 1 - 2 files changed, 3 deletions(-) diff --git a/booster/test/llvm-integration/LLVM.hs b/booster/test/llvm-integration/LLVM.hs index 11bc937e51..fbe71af89d 100644 --- a/booster/test/llvm-integration/LLVM.hs +++ b/booster/test/llvm-integration/LLVM.hs @@ -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 @@ -334,7 +333,6 @@ displayTestDef = do prunedDef = def { modules = Map.empty - , aliases = Map.empty , functionEquations = Map.empty , simplifications = Map.empty } diff --git a/booster/unit-tests/Test/Booster/Fixture.hs b/booster/unit-tests/Test/Booster/Fixture.hs index d0f527473a..2a5a16601c 100644 --- a/booster/unit-tests/Test/Booster/Fixture.hs +++ b/booster/unit-tests/Test/Booster/Fixture.hs @@ -63,7 +63,6 @@ testDefinition = ] <> listSymbols <> setSymbols - , aliases = Map.empty , rewriteTheory = Map.empty , functionEquations = Map.empty , simplifications = Map.empty