From 27ac540350a63ecbf2bb87665f022fdbf33ae5bb Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Mon, 20 Nov 2023 09:14:00 +0000 Subject: [PATCH] Remove ML connectives from the predicate type (#155) Turn `Predicate` into a newtype for `Terms` of sort `Bool`. This also removes all the predicate simplifications, since those rules introduce ML connectives. This should be a sound thing to do since the frontend turns all `requires REQ` clauses into `REQ #Equals true`. All we should do when internalising is to unwrap `REQ #Equals true` into `X`. If we add a restriction to requires/ensures that they can only be expressions of sort Bool (https://github.com/runtimeverification/k/issues/3284), this should be sound. Equally, we dont want to use any rules such as ``` rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) ``` from `domains.md`: https://github.com/runtimeverification/k/blob/71a183b85a48da94e34541ca138757fbeb37ce8a/k-distribution/include/kframework/builtin/domains.md?plain=1#L966-L974 since they would now introduce ML connectives which are unnecessary in this instance. We want this rule to be applied instead ``` rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2) ``` other rules, such as ``` rule {true #Equals @B1 andBool @B2} => {true #Equals @B1} #And {true #Equals @B2} ``` are kind of meta-rules which we implicitly apply already: https://github.com/runtimeverification/hs-backend-booster/blob/37717b4e33455e8e16e7ca51e946b9a7b4f3c1be/library/Booster/Pattern/Simplify.hs#L20-L25 There is still the question of ceil simplification rules but given that they are most likely unsound in their current state and the booster is very conservative around definedness, I don't think we need to worry about them right now... the question is whether/how we will have to deal with them in the future. --------- Co-authored-by: Jost Berthold Co-authored-by: github-actions Co-authored-by: Jost Berthold --- library/Booster/Definition/Base.hs | 14 +- library/Booster/Definition/Util.hs | 8 - library/Booster/JsonRpc.hs | 57 ++-- library/Booster/JsonRpc/Utils.hs | 25 +- library/Booster/Pattern/ApplyEquations.hs | 45 +--- library/Booster/Pattern/Base.hs | 197 ++++++++------ library/Booster/Pattern/Binary.hs | 47 +--- library/Booster/Pattern/Index.hs | 15 +- library/Booster/Pattern/Match.hs | 93 +------ library/Booster/Pattern/Rewrite.hs | 14 +- library/Booster/Pattern/Simplify.hs | 15 +- library/Booster/Pattern/Util.hs | 31 +-- library/Booster/Syntax/Json/Externalise.hs | 106 +++----- library/Booster/Syntax/Json/Internalise.hs | 120 +++++---- .../Booster/Syntax/ParsedKore/Internalise.hs | 245 +++++++++--------- package.yaml | 3 + test/internalisation/bool.kore.report | 10 - .../does-not-preserve-definedness.kore.report | 2 - test/internalisation/existentials.kore.report | 2 - test/internalisation/imp.kore.report | 33 --- ...ves-definedness-total-function.kore.report | 2 - .../preserves-definedness.kore.report | 2 - test/internalisation/subsorts.kore.report | 11 - .../test-totalSupply-definition.kore.report | 44 ---- test/llvm-integration/LLVM.hs | 2 - tools/booster/Proxy.hs | 4 +- unit-tests/Test/Booster/Fixture.hs | 1 - .../Test/Booster/Pattern/ApplyEquations.hs | 21 +- unit-tests/Test/Booster/Pattern/Binary.hs | 19 +- unit-tests/Test/Booster/Pattern/Rewrite.hs | 41 ++- 30 files changed, 467 insertions(+), 762 deletions(-) diff --git a/library/Booster/Definition/Base.hs b/library/Booster/Definition/Base.hs index 6ea1d1472..551362ed0 100644 --- a/library/Booster/Definition/Base.hs +++ b/library/Booster/Definition/Base.hs @@ -43,7 +43,6 @@ data KoreDefinition = KoreDefinition , rewriteTheory :: Theory (RewriteRule "Rewrite") , functionEquations :: Theory (RewriteRule "Function") , simplifications :: Theory (RewriteRule "Simplification") - , predicateSimplifications :: Theory PredicateEquation } deriving stock (Eq, Show, GHC.Generic) deriving anyclass (NFData) @@ -65,7 +64,6 @@ emptyKoreDefinition attributes = , rewriteTheory = Map.empty , functionEquations = Map.empty , simplifications = Map.empty - , predicateSimplifications = Map.empty } data RewriteRule (tag :: k) = RewriteRule @@ -84,17 +82,7 @@ data Alias = Alias { name :: AliasName , params :: [Sort] , args :: [Variable] - , rhs :: TermOrPredicate - } - deriving stock (Eq, Ord, Show, GHC.Generic) - deriving anyclass (NFData) - -data PredicateEquation = PredicateEquation - { target :: Predicate - , conditions :: [Predicate] - , rhs :: [Predicate] - , attributes :: AxiomAttributes - , computedAttributes :: ComputedAxiomAttributes + , rhs :: Pattern } deriving stock (Eq, Ord, Show, GHC.Generic) deriving anyclass (NFData) diff --git a/library/Booster/Definition/Util.hs b/library/Booster/Definition/Util.hs index 069dd4a91..7776b791f 100644 --- a/library/Booster/Definition/Util.hs +++ b/library/Booster/Definition/Util.hs @@ -47,7 +47,6 @@ data Summary = Summary , rewriteRules :: Map.Map TermIndex [SourceRef] , functionRules :: Map.Map TermIndex [SourceRef] , simplifications :: Map.Map TermIndex [SourceRef] - , predicateSimplifications :: Map.Map TermIndex [SourceRef] } deriving stock (Eq, Show, Generic) deriving anyclass (NFData) @@ -80,7 +79,6 @@ mkSummary file def = , rewriteRules = Map.map sourceRefs def.rewriteTheory , functionRules = Map.map sourceRefs def.functionEquations , simplifications = Map.map sourceRefs def.simplifications - , predicateSimplifications = Map.map sourceRefs def.predicateSimplifications } where sourceRefs :: HasSourceRef x => Map.Map k [x] -> [SourceRef] @@ -111,9 +109,6 @@ instance Pretty Summary where <> ( "Simplifications by term index:" : tableView prettyTermIndex pretty summary.simplifications ) - <> ( "Predicate simplifications by term index:" - : tableView prettyTermIndex pretty summary.predicateSimplifications - ) <> [mempty] where tableView :: (k -> Doc a) -> (elem -> Doc a) -> Map.Map k [elem] -> [Doc a] @@ -164,6 +159,3 @@ instance HasSourceRef AxiomAttributes where instance HasSourceRef (RewriteRule a) where sourceRef r = sourceRef r.attributes - -instance HasSourceRef PredicateEquation where - sourceRef r = sourceRef r.attributes diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index eb575402d..068601812 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -42,7 +42,14 @@ import Booster.Definition.Base (KoreDefinition (..)) import Booster.Definition.Base qualified as Definition (RewriteRule (..)) import Booster.LLVM.Internal qualified as LLVM import Booster.Pattern.ApplyEquations qualified as ApplyEquations -import Booster.Pattern.Base (Pattern (..), TermOrPredicate (..)) +import Booster.Pattern.Base ( + InternalisedPredicate (..), + Pattern (..), + Term, + TermOrPredicate (..), + Variable, + ) +import Booster.Pattern.Base qualified as Pattern import Booster.Pattern.Rewrite ( RewriteFailed (..), RewriteResult (..), @@ -88,7 +95,7 @@ respond stateVar = Left patternError -> do Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError) pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternError - Right pat -> do + Right (pat, substitution) -> do let cutPoints = fromMaybe [] req.cutPointRules terminals = fromMaybe [] req.terminalRules mbDepth = fmap RpcTypes.getNat req.maxDepth @@ -109,7 +116,7 @@ respond stateVar = Just $ fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 else Nothing - pure $ execResponse duration req result + pure $ execResponse duration req result substitution RpcTypes.AddModule req -> do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar @@ -172,11 +179,11 @@ respond stateVar = Log.logError $ "Error internalising cterm: " <> Text.pack (show patternErrors) pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors -- term and predicate (pattern) - Right (TermAndPredicate pat) -> do + Right (TermAndPredicateAndSubstitution pat substitution) -> do Log.logInfoNS "booster" "Simplifying a pattern" ApplyEquations.evaluatePattern doTracing def mLlvmLibrary mempty pat >>= \case (Right newPattern, patternTraces, _) -> do - let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern + let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution tSort = externaliseSort (sortOfPattern newPattern) result = case catMaybes [mbPredicate, mbSubstitution] of [] -> term @@ -190,7 +197,7 @@ respond stateVar = (Left other, _traces, _) -> pure . Left . RpcError.backendError RpcError.Aborted $ show other -- FIXME -- predicate only - Right (APredicate predicate) -> do + Right (BoolOrCeilOrSubstitutionPredicate (IsPredicate predicate)) -> do Log.logInfoNS "booster" "Simplifying a predicate" ApplyEquations.simplifyConstraint doTracing def mLlvmLibrary mempty predicate >>= \case (Right newPred, traces, _) -> do @@ -201,6 +208,9 @@ respond stateVar = pure $ Right (addHeader result, traces) (Left something, _traces, _) -> pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME + Right (BoolOrCeilOrSubstitutionPredicate _) -> + pure . Left . RpcError.backendError RpcError.Aborted $ + ("cannot simplify ceil/substitution at the moment" :: String) -- FIXME stop <- liftIO $ getTime Monotonic let duration = @@ -275,8 +285,9 @@ execResponse :: Maybe Double -> RpcTypes.ExecuteRequest -> (Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) -> + Map Variable Term -> Either ErrorObj (RpcTypes.API 'RpcTypes.Res) -execResponse mbDuration req (d, traces, rr) = case rr of +execResponse mbDuration req (d, traces, rr) originalSubstitution = case rr of RewriteBranch p nexts -> Right $ RpcTypes.Execute @@ -284,8 +295,8 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.Branching , depth , logs - , state = toExecState p - , nextStates = Just $ map (\(_, _, p') -> toExecState p') $ toList nexts + , state = toExecState p originalSubstitution + , nextStates = Just $ map (\(_, _, p') -> toExecState p' originalSubstitution) $ toList nexts , rule = Nothing } RewriteStuck p -> @@ -295,7 +306,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.Stuck , depth , logs - , state = toExecState p + , state = toExecState p originalSubstitution , nextStates = Nothing , rule = Nothing } @@ -306,7 +317,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.Vacuous , depth , logs - , state = toExecState p + , state = toExecState p originalSubstitution , nextStates = Nothing , rule = Nothing } @@ -317,8 +328,8 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.CutPointRule , depth , logs - , state = toExecState p - , nextStates = Just [toExecState next] + , state = toExecState p originalSubstitution + , nextStates = Just [toExecState next originalSubstitution] , rule = Just lbl } RewriteTerminal lbl _ p -> @@ -328,7 +339,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.TerminalRule , depth , logs - , state = toExecState p + , state = toExecState p originalSubstitution , nextStates = Nothing , rule = Just lbl } @@ -339,7 +350,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of { reason = RpcTypes.DepthBound , depth , logs - , state = toExecState p + , state = toExecState p originalSubstitution , nextStates = Nothing , rule = Nothing } @@ -356,7 +367,7 @@ execResponse mbDuration req (d, traces, rr) = case rr of (logSuccessfulSimplifications, logFailedSimplifications) (RewriteStepFailed failure) in logs <|> abortRewriteLog - , state = toExecState p + , state = toExecState p originalSubstitution , nextStates = Nothing , rule = Nothing } @@ -385,15 +396,15 @@ execResponse mbDuration req (d, traces, rr) = case rr of (Just t, Nothing) -> Just [t] (Just t, Just xs) -> Just (t : xs) -toExecState :: Pattern -> RpcTypes.ExecuteState -toExecState pat = +toExecState :: Pattern -> Map Variable Term -> RpcTypes.ExecuteState +toExecState pat sub = RpcTypes.ExecuteState { term = addHeader t , predicate = fmap addHeader p , substitution = fmap addHeader s } where - (t, p, s) = externalisePattern pat + (t, p, s) = externalisePattern pat sub mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry mkLogEquationTrace @@ -409,7 +420,7 @@ mkLogEquationTrace , origin , result = Success - { rewrittenTerm = Just $ execStateToKoreJson $ toExecState $ Pattern rewrittenTrm mempty + { rewrittenTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty , substitution = Nothing , ruleId = fromMaybe "UNKNOWN" _ruleId } @@ -474,7 +485,7 @@ mkLogEquationTrace } _ -> Nothing where - originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern subjectTerm mempty + originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ subjectTerm) mempty originalTermIndex = Nothing origin = Booster _ruleId = fmap getUniqueId uid @@ -495,7 +506,7 @@ mkLogRewriteTrace Rewrite { result = Success - { rewrittenTerm = Just $ execStateToKoreJson $ toExecState res + { rewrittenTerm = Just $ execStateToKoreJson $ toExecState res mempty , substitution = Nothing , ruleId = maybe "UNKNOWN" getUniqueId uid } @@ -547,7 +558,7 @@ mkLogRewriteTrace let final = singleton $ case failure of ApplyEquations.IndexIsNone trm -> Simplification - { originalTerm = Just $ execStateToKoreJson $ toExecState $ Pattern trm mempty + { originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ trm) mempty , originalTermIndex = Nothing , origin = Booster , result = Failure{reason = "No index found for term", _ruleId = Nothing} diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs index d311029b8..282093c99 100644 --- a/library/Booster/JsonRpc/Utils.hs +++ b/library/Booster/JsonRpc/Utils.hs @@ -21,9 +21,7 @@ import Data.Aeson as Json import Data.Aeson.Encode.Pretty (encodePretty') import Data.Aeson.Types (parseMaybe) import Data.ByteString.Lazy.Char8 qualified as BS -import Data.Functor.Foldable (Corecursive (embed), cata) import Data.Maybe (fromMaybe) -import Data.Set qualified as Set import Network.JSONRPC import Prettyprinter import System.Exit (ExitCode (..)) @@ -36,6 +34,7 @@ import Booster.Definition.Base qualified as Internal import Booster.Pattern.Base qualified as Internal import Booster.Prettyprinter import Booster.Syntax.Json.Internalise +import Data.Map qualified as Map import Kore.JsonRpc.Types import Kore.Syntax.Json.Types hiding (Left, Right) @@ -235,23 +234,15 @@ diffBy def pat1 pat2 = renderDiff (internalise pat1) (internalise pat2) where renderBS :: Internal.TermOrPredicate -> BS.ByteString - renderBS (Internal.APredicate p) = BS.pack . renderDefault $ pretty p - renderBS (Internal.TermAndPredicate p) = BS.pack . renderDefault $ pretty p + renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsPredicate p)) = BS.pack . renderDefault $ pretty p + renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsCeil c)) = BS.pack . renderDefault $ pretty c + renderBS (Internal.BoolOrCeilOrSubstitutionPredicate (Internal.IsSubstitution k v)) = BS.pack . renderDefault $ pretty k <+> "=" <+> pretty v + renderBS (Internal.TermAndPredicateAndSubstitution p m) = + BS.pack . renderDefault $ + pretty p <+> vsep (map (\(k, v) -> pretty k <+> "=" <+> pretty v) (Map.toList m)) internalise = either (("Pattern could not be internalised: " <>) . Json.encode) - (renderBS . orientEquals) + renderBS . runExcept . internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def - - orientEquals = \case - Internal.APredicate p -> - Internal.APredicate $ orient p - Internal.TermAndPredicate p -> - Internal.TermAndPredicate p{Internal.constraints = Set.map orient p.constraints} - where - orient :: Internal.Predicate -> Internal.Predicate - orient = cata $ \case - Internal.EqualsTermF t1 t2 - | t1 > t2 -> Internal.EqualsTerm t2 t1 - other -> embed other diff --git a/library/Booster/Pattern/ApplyEquations.hs b/library/Booster/Pattern/ApplyEquations.hs index 831c1c642..920fdca30 100644 --- a/library/Booster/Pattern/ApplyEquations.hs +++ b/library/Booster/Pattern/ApplyEquations.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE PatternSynonyms #-} - {- | Copyright : (c) Runtime Verification, 2022 License : BSD-3-Clause @@ -55,6 +53,7 @@ import Booster.Pattern.Match import Booster.Pattern.Simplify import Booster.Pattern.Util import Booster.Prettyprinter (renderDefault) +import Data.Coerce (coerce) newtype EquationT io a = EquationT (ReaderT EquationConfig (ExceptT EquationFailure (StateT EquationState io)) a) @@ -290,7 +289,7 @@ evaluatePattern' :: MonadLoggerIO io => Pattern -> EquationT io Pattern -evaluatePattern' Pattern{term, constraints} = do +evaluatePattern' Pattern{term, constraints, ceilConditions} = do pushConstraints constraints newTerm <- evaluateTerm' TopDown term -- after evaluating the term, evaluate all (existing and @@ -298,7 +297,7 @@ evaluatePattern' Pattern{term, constraints} = do traverse_ simplifyAssumedPredicate . predicates =<< getState -- this may yield additional new constraints, left unevaluated evaluatedConstraints <- predicates <$> getState - pure Pattern{constraints = evaluatedConstraints, term = newTerm} + pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions} where -- evaluate the given predicate assuming all others simplifyAssumedPredicate p = do @@ -578,7 +577,7 @@ applyEquation term rule = fmap (either id Success) $ runExceptT $ do -- check required conditions, using substitution let required = concatMap - (splitBoolPredicates . substituteInPredicate subst) + (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires unclearConditions' <- catMaybes <$> mapM (checkConstraint ConditionFalse) required @@ -605,8 +604,8 @@ applyEquation term rule = fmap (either id Success) $ runExceptT $ do ExceptT ApplyEquationResult (EquationT io) (Maybe Predicate) checkConstraint whenBottom p = lift (simplifyConstraint' False p) >>= \case - Bottom -> throwE $ whenBottom p - Top -> pure Nothing + Predicate FalseBool -> throwE $ whenBottom p + Predicate TrueBool -> pure Nothing _other -> pure $ Just p allMustBeConcrete (AllConstrained Concrete) = True @@ -655,14 +654,7 @@ applyEquation term rule = fmap (either id Success) $ runExceptT $ do -------------------------------------------------------------------- --- | Helper pattern for simplifyConstraint -pattern TrueBool :: Term -pattern TrueBool = DomainValue SortBool "true" - -pattern FalseBool :: Term -pattern FalseBool = DomainValue SortBool "false" - -{- | Simplification for boolean predicates +{- Simplification for boolean predicates This is used during rewriting to simplify side conditions of rules (to decide whether or not a rule can apply, not to retain the @@ -689,30 +681,19 @@ simplifyConstraint' :: MonadLoggerIO io => Bool -> Predicate -> EquationT io Pre -- evaluating them using simplifyBool if they are concrete. -- Non-concrete \equals predicates are simplified using evaluateTerm. simplifyConstraint' recurse = \case - p@(EqualsTerm TrueBool t@(Term attributes _)) - | isConcrete t && attributes.canBeEvaluated -> do + Predicate t@(Term TermAttributes{canBeEvaluated} _) + | isConcrete t && canBeEvaluated -> do mbApi <- (.llvmApi) <$> getConfig case mbApi of Just api -> if simplifyBool api t - then pure Top - else pure Bottom + then pure $ Predicate TrueBool + else pure $ Predicate FalseBool Nothing -> - if recurse then evalBool t >>= prune else pure p + Predicate <$> if recurse then evalBool t else pure t | otherwise -> - if recurse then evalBool t >>= prune else pure p - EqualsTerm t TrueBool -> - -- normalise to 'true' in first argument (like 'kore-rpc') - simplifyConstraint' recurse (EqualsTerm TrueBool t) - other -> - pure other -- should not occur, predicates should be 'true \equals _' + Predicate <$> if recurse then evalBool t else pure t where - prune = - pure . \case - TrueBool -> Top - FalseBool -> Bottom - other -> EqualsTerm TrueBool other - evalBool :: MonadLoggerIO io => Term -> EquationT io Term evalBool t = do prior <- getState -- save prior state so we can revert diff --git a/library/Booster/Pattern/Base.hs b/library/Booster/Pattern/Base.hs index e1573c09b..c9920e0f4 100644 --- a/library/Booster/Pattern/Base.hs +++ b/library/Booster/Pattern/Base.hs @@ -3,7 +3,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {- | Copyright : (c) Runtime Verification, 2022 @@ -37,10 +37,10 @@ import Data.ByteString.Char8 qualified as BS import Data.Data (Data) import Data.Either (fromRight) import Data.Functor.Foldable -import Data.Functor.Foldable.TH (makeBaseFunctor) import Data.Hashable (Hashable) import Data.Hashable qualified as Hashable import Data.List as List (foldl1', sort) +import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set, fromList, toList) import Data.Set qualified as Set @@ -66,8 +66,12 @@ data Sort deriving stock (Eq, Ord, Show, Generic, Data, Lift) deriving anyclass (NFData, Hashable) -pattern SortBool :: Sort +pattern SortBool, SortInt, SortK, SortKItem, SortBytes :: Sort pattern SortBool = SortApp "SortBool" [] +pattern SortInt = SortApp "SortInt" [] +pattern SortK = SortApp "SortK" [] +pattern SortKItem = SortApp "SortKItem" [] +pattern SortBytes = SortApp "SortBytes" [] -- | A variable for symbolic execution or for terms in a rule. data Variable = Variable @@ -699,26 +703,103 @@ pattern DotDotDot :: Term pattern DotDotDot = DomainValue (SortApp "internalDummySort" []) "..." {- | A predicate describes constraints on terms. It will always evaluate - to 'Top' or 'Bottom'. Notice that 'Predicate's don't have a sort. + to 'TrueBool' or 'FalseBool'. Notice that 'Predicate's don't have a sort. -} -data Predicate - = AndPredicate Predicate Predicate - | Bottom - | Ceil Term - | EqualsTerm Term Term - | EqualsPredicate Predicate Predicate - | Exists Variable Predicate - | Forall Variable Predicate - | Iff Predicate Predicate - | Implies Predicate Predicate - | In Term Term - | Not Predicate - | Or Predicate Predicate - | Top +newtype Predicate = Predicate Term deriving stock (Eq, Ord, Show, Generic, Data) deriving anyclass (NFData) -makeBaseFunctor ''Predicate +newtype Ceil = Ceil Term + deriving stock (Eq, Ord, Show, Generic, Data) + deriving anyclass (NFData) + +pattern NotBool :: Term -> Term +pattern NotBool t = + SymbolApplication + ( Symbol + "LblnotBool'Unds'" + [] + [SortBool] + SortBool + (SymbolAttributes TotalFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [t] + +pattern EqualsInt, NEqualsInt, EqualsK, NEqualsK :: Term -> Term -> Term +pattern EqualsInt a b = + SymbolApplication + ( Symbol + "Lbl'UndsEqlsEqls'Int'Unds'" + [] + [SortInt, SortInt] + SortBool + (SymbolAttributes TotalFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [a, b] +pattern NEqualsInt a b = + SymbolApplication + ( Symbol + "Lbl'UndsEqlsSlshEqls'Int'Unds'" + [] + [SortInt, SortInt] + SortBool + (SymbolAttributes TotalFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [a, b] +pattern EqualsK a b = + SymbolApplication + ( Symbol + "Lbl'UndsEqlsEqls'K'Unds'" + [] + [SortK, SortK] + SortBool + (SymbolAttributes TotalFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [a, b] +pattern NEqualsK a b = + SymbolApplication + ( Symbol + "Lbl'UndsEqlsSlshEqls'K'Unds'" + [] + [SortK, SortK] + SortBool + (SymbolAttributes TotalFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [a, b] + +-- kseq{}(inj{, SortKItem{}}(),dotk{}() +pattern KSeq :: Sort -> Term -> Term +pattern KSeq sort a = + SymbolApplication + ( Symbol + "kseq" + [] + [SortKItem, SortK] + SortK + (SymbolAttributes Constructor IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [ Injection sort SortKItem a + , SymbolApplication + ( Symbol + "dotk" + [] + [] + SortK + (SymbolAttributes Constructor IsNotIdem IsNotAssoc IsNotMacroOrAlias CanBeEvaluated Nothing) + ) + [] + [] + ] + +pattern TrueBool, FalseBool :: Term +pattern TrueBool = DomainValue SortBool "true" +pattern FalseBool = DomainValue SortBool "false" -------------------- @@ -726,13 +807,23 @@ makeBaseFunctor ''Predicate data Pattern = Pattern { term :: Term , constraints :: !(Set Predicate) + , ceilConditions :: ![Ceil] } deriving stock (Eq, Ord, Show, Generic, Data) deriving anyclass (NFData) +pattern Pattern_ :: Term -> Pattern +pattern Pattern_ t <- Pattern t _ _ + where + Pattern_ t = Pattern t mempty mempty + +data InternalisedPredicate = IsPredicate Predicate | IsCeil Ceil | IsSubstitution Variable Term + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (NFData) + data TermOrPredicate -- = Either Predicate Pattern - = APredicate Predicate - | TermAndPredicate Pattern + = BoolOrCeilOrSubstitutionPredicate InternalisedPredicate + | TermAndPredicateAndSubstitution Pattern (Map Variable Term) deriving stock (Eq, Ord, Show, Generic) deriving anyclass (NFData) @@ -859,60 +950,16 @@ instance Pretty Variable where <> pretty var.variableSort instance Pretty Predicate where - pretty = - \case - AndPredicate p1 p2 -> - "\\andPredicate" - <> KPretty.noParameters - <> KPretty.argumentsP [p1, p2] - Bottom -> - "\\bottom" - <> KPretty.noParameters - <> KPretty.noArguments - Ceil t -> - "\\ceil" - <> KPretty.noParameters - <> KPretty.argumentsP [t] - EqualsTerm t1 t2 -> - "\\equalsTerm" - <> KPretty.noParameters - <> KPretty.argumentsP [t1, t2] - EqualsPredicate p1 p2 -> - "\\equalsPredicate" - <> KPretty.noParameters - <> KPretty.argumentsP [p1, p2] - Exists v p -> - "\\exists" - <> KPretty.noParameters - <> KPretty.arguments' [pretty v, pretty p] - Forall v p -> - "\\forall" - <> KPretty.noParameters - <> KPretty.arguments' [pretty v, pretty p] - Iff p1 p2 -> - "\\iff" - <> KPretty.noParameters - <> KPretty.argumentsP [p1, p2] - Implies p1 p2 -> - "\\implies" - <> KPretty.noParameters - <> KPretty.argumentsP [p1, p2] - In t1 t2 -> - "\\in" - <> KPretty.noParameters - <> KPretty.argumentsP [t1, t2] - Not p -> - "\\not" - <> KPretty.noParameters - <> KPretty.argumentsP [p] - Or p1 p2 -> - "\\or" - <> KPretty.noParameters - <> KPretty.argumentsP [p1, p2] - Top -> - "\\top" - <> KPretty.noParameters - <> KPretty.noArguments + pretty (Predicate t) = + "\\equalsTerm" + <> KPretty.noParameters + <> KPretty.argumentsP [t, DomainValue SortBool "true"] + +instance Pretty Ceil where + pretty (Ceil t) = + "\\ceil" + <> KPretty.noParameters + <> KPretty.argumentsP [t] instance Pretty Pattern where pretty patt = diff --git a/library/Booster/Pattern/Binary.hs b/library/Booster/Pattern/Binary.hs index 270de4cd2..bd8417844 100644 --- a/library/Booster/Pattern/Binary.hs +++ b/library/Booster/Pattern/Binary.hs @@ -276,35 +276,24 @@ decodeBlock mbSize = do False -> m >> whileNotEnded m mkSymbolApplication :: ByteString -> [Sort] -> [Block] -> DecodeM Block - mkSymbolApplication "\\and" _ [BPredicate p1, BPredicate p2] = pure $ BPredicate $ AndPredicate p1 p2 mkSymbolApplication "\\and" _ [BTerm t1, BTerm t2] = pure $ BTerm $ AndTerm t1 t2 mkSymbolApplication "\\and" _ bs = - argError "AndTerm/AndPredicate" [BTerm undefined, BTerm undefined] bs - mkSymbolApplication "\\bottom" _ [] = pure $ BPredicate Bottom + argError "AndTerm" [BTerm undefined, BTerm undefined] bs mkSymbolApplication "\\bottom" _ bs = argError "Bottom" [] bs - mkSymbolApplication "\\ceil" _ [BTerm t] = pure $ BPredicate $ Ceil t mkSymbolApplication "\\ceil" _ bs = argError "Ceil" [BTerm undefined] bs mkSymbolApplication "\\dv" [sort] [BString txt] = pure $ BTerm $ DomainValue sort txt mkSymbolApplication "\\dv" _ bs = argError "DomainValue" [BString undefined] bs - mkSymbolApplication "\\equals" _ [BTerm t1, BTerm t2] = pure $ BPredicate $ EqualsTerm t1 t2 - mkSymbolApplication "\\equals" _ [BPredicate p1, BPredicate p2] = pure $ BPredicate $ EqualsPredicate p1 p2 + mkSymbolApplication "\\equals" _ [BTerm t, BTerm TrueBool] = pure $ BPredicate $ Predicate t + mkSymbolApplication "\\equals" _ [BTerm TrueBool, BTerm t] = pure $ BPredicate $ Predicate t mkSymbolApplication "\\equals" _ bs = argError "EqualBTerm/EqualBPredicate" [BTerm undefined, BTerm undefined] bs - mkSymbolApplication "\\exists" _ [BTerm (Var var), BPredicate p] = pure $ BPredicate $ Exists var p mkSymbolApplication "\\exists" _ bs = argError "Exists" [BTerm undefined, BPredicate undefined] bs - mkSymbolApplication "\\forall" _ [BTerm (Var var), BPredicate p] = pure $ BPredicate $ Forall var p mkSymbolApplication "\\forall" _ bs = argError "Forall" [BTerm undefined, BPredicate undefined] bs - mkSymbolApplication "\\iff" _ [BPredicate p1, BPredicate p2] = pure $ BPredicate $ Iff p1 p2 mkSymbolApplication "\\iff" _ bs = argError "Iff" [BPredicate undefined, BPredicate undefined] bs - mkSymbolApplication "\\implies" _ [BPredicate p1, BPredicate p2] = pure $ BPredicate $ Implies p1 p2 mkSymbolApplication "\\implies" _ bs = argError "Implies" [BPredicate undefined, BPredicate undefined] bs - mkSymbolApplication "\\in" _ [BTerm t1, BTerm t2] = pure $ BPredicate $ In t1 t2 mkSymbolApplication "\\in" _ bs = argError "In" [BTerm undefined, BTerm undefined] bs - mkSymbolApplication "\\not" _ [BPredicate p] = pure $ BPredicate $ Not p mkSymbolApplication "\\not" _ bs = argError "Not" [BPredicate undefined] bs - mkSymbolApplication "\\or" _ [BPredicate p1, BPredicate p2] = pure $ BPredicate $ Or p1 p2 mkSymbolApplication "\\or" _ bs = argError "Or" [BPredicate undefined, BPredicate undefined] bs - mkSymbolApplication "\\top" _ [] = pure $ BPredicate Top mkSymbolApplication "\\top" _ bs = argError "Top" [] bs mkSymbolApplication "inj" [source, target] [BTerm t] = pure $ BTerm $ Injection source target t mkSymbolApplication "inj" _ bs = argError "Injection" [BTerm undefined] bs @@ -397,7 +386,7 @@ decodePattern mDef = do preds <- forM preds' $ \case BPredicate p -> pure p _ -> fail "Expecting a predicate" - pure $ Pattern trm $ Set.fromList preds + pure $ Pattern trm (Set.fromList preds) mempty _ -> fail "Expecting a term on the top of the stack" decodeSingleBlock :: Get Block @@ -476,32 +465,8 @@ encodeSymbolApplication name sorts args = do encodeLength $ length args encodePredicate :: Predicate -> Put -encodePredicate = \case - AndPredicate p1 p2 -> encodeSymbolApplication "\\and" [] [Right p1, Right p2] - Bottom -> encodeSymbolApplication "\\bottom" [] [] - Ceil t -> encodeSymbolApplication "\\ceil" [] [Left t] - EqualsTerm t1 t2 -> encodeSymbolApplication "\\equals" [] [Left t1, Left t2] - EqualsPredicate p1 p2 -> encodeSymbolApplication "\\equals" [] [Right p1, Right p2] - Exists v p -> - encodeSymbolApplication - "\\exists" - [] - [ Left $ Var v - , Right p - ] - Forall v p -> - encodeSymbolApplication - "\\forall" - [] - [ Left $ Var v - , Right p - ] - Iff p1 p2 -> encodeSymbolApplication "\\iff" [] [Right p1, Right p2] - Implies p1 p2 -> encodeSymbolApplication "\\implies" [] [Right p1, Right p2] - In t1 t2 -> encodeSymbolApplication "\\in" [] [Left t1, Left t2] - Not p -> encodeSymbolApplication "\\not" [] [Right p] - Or p1 p2 -> encodeSymbolApplication "\\or" [] [Right p1, Right p2] - Top -> encodeSymbolApplication "\\top" [] [] +encodePredicate (Predicate t) = + encodeSymbolApplication "\\equals" [] [Left t, Left TrueBool] encodePattern :: Pattern -> Put encodePattern Pattern{term, constraints} = do diff --git a/library/Booster/Pattern/Index.hs b/library/Booster/Pattern/Index.hs index a4045ee34..aae6b856b 100644 --- a/library/Booster/Pattern/Index.hs +++ b/library/Booster/Pattern/Index.hs @@ -132,17 +132,4 @@ termTopIndex = \case -- indexes predicates by the name of their top-level connective predicateTopIndex :: Predicate -> TermIndex -predicateTopIndex = \case - AndPredicate{} -> TopSymbol "\\and" - Bottom -> TopSymbol "\\bottom" - Ceil{} -> TopSymbol "\\ceil" - EqualsTerm{} -> TopSymbol "\\equalsTerm" - EqualsPredicate{} -> TopSymbol "\\equalsPredicate" - Exists{} -> TopSymbol "\\exists" - Forall{} -> TopSymbol "\\forall" - Iff{} -> TopSymbol "\\iff" - Implies{} -> TopSymbol "\\implies" - In{} -> TopSymbol "\\in" - Not{} -> TopSymbol "\\not" - Or{} -> TopSymbol "\\or" - Top -> TopSymbol "\\top" +predicateTopIndex (Predicate t) = termTopIndex t diff --git a/library/Booster/Pattern/Match.hs b/library/Booster/Pattern/Match.hs index d52bffa7b..882eb840d 100644 --- a/library/Booster/Pattern/Match.hs +++ b/library/Booster/Pattern/Match.hs @@ -5,7 +5,6 @@ License : BSD-3-Clause module Booster.Pattern.Match ( MatchResult (..), MatchFailReason (..), - PredicatesDoNotMatch (..), matchTerm, matchPredicate, ) where @@ -14,8 +13,6 @@ import Control.Monad import Control.Monad.Trans.Class import Control.Monad.Trans.Except import Control.Monad.Trans.State -import Control.Monad.Trans.Writer -import Data.Bifunctor (second) import Data.Either.Extra import Data.Map (Map) import Data.Map qualified as Map @@ -34,7 +31,6 @@ import Booster.Pattern.Util ( isConcrete, isConstructorSymbol, isFunctionSymbol, - modifyVariablesInP, sortOfTerm, substituteInTerm, ) @@ -339,91 +335,16 @@ bindVariable var term = do ---------------------------------------- -{- | Match a predicate pattern (containing terms) to a predicate - subject. +{- | Match a predicate pattern (containing boolean terms) to a predicate + subject, by matching the contained terms. - Since the result is a variable substitution and variables are terms, - this will ultimately fall back to matching terms. The predicate is - traversed, collecting a queue of term matching problems to run once - the predicate shapes are matched completely. - - An additional error type is added for the case where the predicate - pattern does not match the subject syntactically. - - This is kept simple because we don't expect to use is much; only - few simplifications on ML constructs are allowed and used. + This will probably not be used in the booster, as we only accept + predicates which are boolean terms compared to true or false. -} matchPredicate :: KoreDefinition -> Predicate -> Predicate -> - Either PredicatesDoNotMatch MatchResult -matchPredicate def pat subj = - second runTermMatching $ matchPredicates (pat, subj) - where - runTermMatching :: Seq (Term, Term) -> MatchResult - runTermMatching = - fromEither - . runExcept - . fmap (MatchSuccess . mSubstitution) - . execStateT matching - . mkMatchState - - -- produce initial state with given work queue - mkMatchState mQueue = - State{mSubstitution = Map.empty, mQueue, mSubsorts = Map.map snd def.sorts} - - matchPredicates :: (Predicate, Predicate) -> Either PredicatesDoNotMatch (Seq (Term, Term)) - matchPredicates = runExcept . execWriterT . collect - - collect :: (Predicate, Predicate) -> WriterT (Seq (Term, Term)) (Except PredicatesDoNotMatch) () - collect (pPattern, pSubject) = case (pPattern, pSubject) of - (AndPredicate p1 p2, AndPredicate s1 s2) -> - collect (p1, s1) >> collect (p2, s2) - (Bottom, Bottom) -> - pure () - (Ceil p, Ceil s) -> - enqueue (p, s) - (EqualsTerm p1 p2, EqualsTerm s1 s2) -> - enqueue (p1, s1) >> enqueue (p2, s2) - (EqualsPredicate p1 p2, EqualsPredicate s1 s2) -> - collect (p1, s1) >> collect (p2, s2) - (Exists pv p, Exists sv s) -> do - -- forbid pv in the resulting substitution by injecting it here - enqueue (Var pv, Var sv) - let renamedS = modifyVariablesInP (renameVariable sv pv) s - collect (p, renamedS) - (Forall pv p, Forall sv s) -> do - -- forbid pv in the resulting substitution by injecting it here - enqueue (Var pv, Var sv) - let renamedS = modifyVariablesInP (renameVariable sv pv) s - collect (p, renamedS) - (Iff p1 p2, Iff s1 s2) -> - collect (p1, s1) >> collect (p2, s2) - (Implies p1 p2, Implies s1 s2) -> - collect (p1, s1) >> collect (p2, s2) - (In p1 p2, In s1 s2) -> - enqueue (p1, s1) >> enqueue (p2, s2) - (Not p, Not s) -> - collect (p, s) - (Or p1 p2, Or s1 s2) -> - collect (p1, s1) >> collect (p2, s2) - (Top, Top) -> - pure () - _other -> noMatch - where - enqueue = tell . Seq.singleton - noMatch = lift $ throwE PredicatesDoNotMatch{pPattern, pSubject} - - renameVariable :: Variable -> Variable -> Variable -> Variable - renameVariable before after target - | target == before = after - | target == after = error "variable name capture" - -- should never happen, equation variables will all be renamed - | otherwise = target - -data PredicatesDoNotMatch = PredicatesDoNotMatch - { pPattern :: Predicate - , pSubject :: Predicate - } - deriving (Eq, Show) + MatchResult +matchPredicate def (Predicate pat) (Predicate subj) = + matchTerm def pat subj diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index 5ab875f11..5cb6bfb53 100644 --- a/library/Booster/Pattern/Rewrite.hs +++ b/library/Booster/Pattern/Rewrite.hs @@ -50,6 +50,7 @@ import Booster.Pattern.Simplify import Booster.Pattern.Unify import Booster.Pattern.Util import Booster.Prettyprinter +import Data.Coerce (coerce) newtype RewriteT io err a = RewriteT {unRewriteT :: ReaderT RewriteConfig (StateT SimplifierCache (ExceptT err io)) a} @@ -237,7 +238,7 @@ applyRule :: Pattern -> RewriteRule k -> RewriteT io (RewriteFailed k) (RewriteRuleAppResult (RewriteRule k, Pattern)) -applyRule pat rule = runRewriteRuleAppT $ do +applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do def <- lift getDefinition -- unify terms let unified = unifyTerms def rule.lhs pat.term @@ -269,7 +270,7 @@ applyRule pat rule = runRewriteRuleAppT $ do -- apply substitution to rule requires constraints and simplify (one by one -- in isolation). Stop if false, abort rewrite if indeterminate. let ruleRequires = - concatMap (splitBoolPredicates . substituteInPredicate subst) rule.requires + concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires failIfUnclear = RuleConditionUnclear rule notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied unclearRequires <- @@ -281,7 +282,7 @@ applyRule pat rule = runRewriteRuleAppT $ do -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest let ruleEnsures = - concatMap (splitBoolPredicates . substituteInPredicate subst) $ + concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) $ Set.toList rule.ensures trivialIfBottom = RewriteRuleAppT $ pure Trivial newConstraints <- @@ -292,8 +293,9 @@ applyRule pat rule = runRewriteRuleAppT $ do (substituteInTerm (refreshExistentials subst) rule.rhs) -- adding new constraints that have not been trivially `Top` ( Set.fromList newConstraints - <> Set.map (substituteInPredicate subst) pat.constraints + <> Set.map (coerce . substituteInTerm subst . coerce) pat.constraints ) + ceilConditions return (rule, rewritten) where failRewrite = lift . throw @@ -313,8 +315,8 @@ applyRule pat rule = runRewriteRuleAppT $ do RewriteConfig{definition, llvmApi, doTracing} <- lift $ RewriteT ask (simplified, _traces, _cache) <- simplifyConstraint doTracing definition llvmApi mempty p case simplified of - Right Bottom -> onBottom - Right Top -> pure Nothing + Right (Predicate FalseBool) -> onBottom + Right (Predicate TrueBool) -> pure Nothing Right other -> pure $ Just $ onUnclear other Left _ -> pure $ Just $ onUnclear p diff --git a/library/Booster/Pattern/Simplify.hs b/library/Booster/Pattern/Simplify.hs index a994f92eb..6192eae6c 100644 --- a/library/Booster/Pattern/Simplify.hs +++ b/library/Booster/Pattern/Simplify.hs @@ -9,13 +9,12 @@ module Booster.Pattern.Simplify ( import Booster.Pattern.Base import Booster.Pattern.Util (isConcrete) -{- | We want to break apart predicates of type `X #Equals Y1 andBool ... Yn` into -`X #Equals Y1, ..., X #Equals Yn` in the case when some of the `Y`s are abstract -and thus the whole original expression could not be fed to the LLVM simplifyBool function +{- | We want to break apart predicates of type `Y1 andBool ... Yn` apart, in case some of the `Y`s are abstract +which prevents the original expression from being fed to the LLVM simplifyBool function -} splitBoolPredicates :: Predicate -> [Predicate] -splitBoolPredicates = \case - p@(EqualsTerm l r) | isConcrete l && isConcrete r -> [p] - EqualsTerm (AndBool ls) r -> concatMap (splitBoolPredicates . flip EqualsTerm r) ls - EqualsTerm l (AndBool rs) -> concatMap (splitBoolPredicates . EqualsTerm l) rs - other -> [other] +splitBoolPredicates p@(Predicate t) + | isConcrete t = [p] + | otherwise = case t of + AndBool ts -> concatMap (splitBoolPredicates . Predicate) ts + other -> [Predicate other] diff --git a/library/Booster/Pattern/Util.hs b/library/Booster/Pattern/Util.hs index f4aa2f73e..05cea11f6 100644 --- a/library/Booster/Pattern/Util.hs +++ b/library/Booster/Pattern/Util.hs @@ -12,7 +12,6 @@ module Booster.Pattern.Util ( substituteInPredicate, modifyVariables, modifyVariablesInT, - modifyVariablesInP, modifyVarName, modifyVarNameConcreteness, freeVariables, @@ -77,14 +76,14 @@ applySubst subst (SortApp n args) = SortApp n $ map (applySubst subst) args sortOfTermOrPredicate :: TermOrPredicate -> Maybe Sort -sortOfTermOrPredicate (TermAndPredicate Pattern{term}) = Just (sortOfTerm term) -sortOfTermOrPredicate (APredicate _) = Nothing +sortOfTermOrPredicate (TermAndPredicateAndSubstitution Pattern{term} _) = Just (sortOfTerm term) +sortOfTermOrPredicate (BoolOrCeilOrSubstitutionPredicate _) = Nothing sortOfPattern :: Pattern -> Sort sortOfPattern pat = sortOfTerm pat.term retractPattern :: TermOrPredicate -> Maybe Pattern -retractPattern (TermAndPredicate patt) = Just patt +retractPattern (TermAndPredicateAndSubstitution patt _) = Just patt retractPattern _ = Nothing substituteInTerm :: Map Variable Term -> Term -> Term @@ -107,16 +106,14 @@ substituteInTerm substitution = goSubst KSet def (map goSubst elements) (goSubst <$> rest) substituteInPredicate :: Map Variable Term -> Predicate -> Predicate -substituteInPredicate substitution = cata $ \case - EqualsTermF t1 t2 -> - EqualsTerm (substituteInTerm substitution t1) (substituteInTerm substitution t2) - other -> embed other +substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern modifyVariables f p = Pattern { term = modifyVariablesInT f p.term - , constraints = Set.map (modifyVariablesInP f) p.constraints + , constraints = Set.map (coerce $ modifyVariablesInT f) p.constraints + , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions } modifyVariablesInT :: (Variable -> Variable) -> Term -> Term @@ -124,20 +121,6 @@ modifyVariablesInT f = cata $ \case VarF v -> Var (f v) other -> embed other -modifyVariablesInP :: (Variable -> Variable) -> Predicate -> Predicate -modifyVariablesInP f = cata $ \case - EqualsTermF t1 t2 -> - EqualsTerm (modifyVariablesInT f t1) (modifyVariablesInT f t2) - InF t1 t2 -> - In (modifyVariablesInT f t1) (modifyVariablesInT f t2) - CeilF t -> - Ceil (modifyVariablesInT f t) - ExistsF v pr -> - Exists (f v) (modifyVariablesInP f pr) - ForallF v pr -> - Forall (f v) (modifyVariablesInP f pr) - other -> embed other - modifyVarName :: (VarName -> VarName) -> Variable -> Variable modifyVarName f v = v{variableName = f v.variableName} @@ -292,7 +275,7 @@ filterTermSymbols check = cata $ \case filter check [concatSym, elemSym] <> fromMaybe [] rest <> concat more isBottom :: Pattern -> Bool -isBottom = (Bottom `elem`) . constraints +isBottom = (Predicate FalseBool `elem`) . constraints -- | Calculate size of a term in bytes sizeOfTerm :: Term -> Int diff --git a/library/Booster/Syntax/Json/Externalise.hs b/library/Booster/Syntax/Json/Externalise.hs index dca33c539..709dc7476 100644 --- a/library/Booster/Syntax/Json/Externalise.hs +++ b/library/Booster/Syntax/Json/Externalise.hs @@ -10,13 +10,14 @@ module Booster.Syntax.Json.Externalise ( ) where import Data.Foldable () -import Data.List (partition) import Data.Set qualified as Set import Data.Text.Encoding qualified as Text import Booster.Pattern.Base (externaliseKmapUnsafe) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Util (sortOfTerm) +import Data.Map (Map) +import Data.Map qualified as Map import Kore.Syntax.Json.Types qualified as Syntax {- | Converts an internal pattern to a triple of term, predicate and substitution in @@ -25,20 +26,23 @@ import Kore.Syntax.Json.Types qualified as Syntax -} externalisePattern :: Internal.Pattern -> + Map Internal.Variable Internal.Term -> (Syntax.KorePattern, Maybe Syntax.KorePattern, Maybe Syntax.KorePattern) -externalisePattern Internal.Pattern{term = term, constraints} = +externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} substitutions = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - (substitutionItems, predicateItems) = - partition isSubstitutionItem $ Set.toList constraints substitution = - if null substitutionItems + if null substitutions then Nothing - else Just . multiAnd sort . map (externalisePredicate sort) $ substitutionItems + else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions predicate = - if null predicateItems + if null constraints && null ceilConditions then Nothing - else Just . multiAnd sort . map (externalisePredicate sort) $ predicateItems + else + Just $ + multiAnd sort $ + map (externalisePredicate sort) (Set.toList constraints) + ++ map (externaliseCeil sort) ceilConditions in (externaliseTerm term, predicate, substitution) where multiAnd :: Syntax.Sort -> [Syntax.KorePattern] -> Syntax.KorePattern @@ -46,15 +50,6 @@ externalisePattern Internal.Pattern{term = term, constraints} = multiAnd _ [p] = p multiAnd sort ps = Syntax.KJAnd sort ps - isSubstitutionItem :: Internal.Predicate -> Bool - isSubstitutionItem (Internal.EqualsTerm lhs _rhs) = isVariable lhs - isSubstitutionItem (Internal.AndPredicate lhs rhs) = isSubstitutionItem lhs && isSubstitutionItem rhs - isSubstitutionItem _ = False - - isVariable :: Internal.Term -> Bool - isVariable (Internal.Var _) = True - isVariable _ = False - -- TODO: should KorePattern be the only type with an actual Unparse instance? externaliseTerm :: Internal.Term -> Syntax.KorePattern externaliseTerm = \case @@ -85,59 +80,30 @@ externaliseTerm = \case externaliseTerm $ Internal.externaliseKSet def heads rest externalisePredicate :: Syntax.Sort -> Internal.Predicate -> Syntax.KorePattern -externalisePredicate sort = - let recursion = externalisePredicate sort - in \case - Internal.AndPredicate p1 p2 -> - Syntax.KJAnd{sort, patterns = [recursion p1, recursion p2]} - Internal.Bottom -> - Syntax.KJBottom{sort} - Internal.Ceil term -> - Syntax.KJCeil - { argSort = externaliseSort $ sortOfTerm term - , sort - , arg = externaliseTerm term - } - Internal.EqualsTerm t1 t2 -> - Syntax.KJEquals - { argSort = externaliseSort $ sortOfTerm t1 - , sort - , first = externaliseTerm t1 - , second = externaliseTerm t2 - } - Internal.EqualsPredicate p1 p2 -> - Syntax.KJEquals{argSort = sort, sort, first = recursion p1, second = recursion p2} - Internal.Exists var p1 -> - Syntax.KJExists - { sort - , var = varNameToId var.variableName - , varSort = externaliseSort var.variableSort - , arg = recursion p1 - } - Internal.Forall var p1 -> - Syntax.KJForall - { sort - , var = varNameToId var.variableName - , varSort = externaliseSort var.variableSort - , arg = recursion p1 - } - Internal.Iff p1 p2 -> - Syntax.KJIff{sort, first = recursion p1, second = recursion p2} - Internal.Implies p1 p2 -> - Syntax.KJImplies{sort, first = recursion p1, second = recursion p2} - Internal.In t1 t2 -> - Syntax.KJIn - { argSort = externaliseSort $ sortOfTerm t1 - , sort - , first = externaliseTerm t1 - , second = externaliseTerm t2 - } - Internal.Not p1 -> - Syntax.KJNot{sort, arg = recursion p1} - Internal.Or p1 p2 -> - Syntax.KJOr{sort, patterns = [recursion p1, recursion p2]} - Internal.Top -> - Syntax.KJTop{sort} +externalisePredicate sort (Internal.Predicate t) = + Syntax.KJEquals + { argSort = externaliseSort $ sortOfTerm t + , sort + , first = externaliseTerm Internal.TrueBool + , second = externaliseTerm t + } + +externaliseCeil :: Syntax.Sort -> Internal.Ceil -> Syntax.KorePattern +externaliseCeil sort (Internal.Ceil term) = + Syntax.KJCeil + { argSort = externaliseSort $ sortOfTerm term + , sort + , arg = externaliseTerm term + } + +externaliseSubstitution :: Syntax.Sort -> Internal.Variable -> Internal.Term -> Syntax.KorePattern +externaliseSubstitution sort Internal.Variable{variableSort = iSort, variableName = iName} t = + Syntax.KJEquals + { argSort = externaliseSort $ sortOfTerm t + , sort + , first = Syntax.KJEVar (varNameToId iName) (externaliseSort iSort) + , second = externaliseTerm t + } varNameToId :: Internal.VarName -> Syntax.Id varNameToId = Syntax.Id . Text.decodeLatin1 diff --git a/library/Booster/Syntax/Json/Internalise.hs b/library/Booster/Syntax/Json/Internalise.hs index 5ff324a45..ecb13187f 100644 --- a/library/Booster/Syntax/Json/Internalise.hs +++ b/library/Booster/Syntax/Json/Internalise.hs @@ -35,14 +35,13 @@ import Control.Monad.Extra import Control.Monad.Trans.Except import Data.Aeson (ToJSON (..), Value, object, (.=)) import Data.Bifunctor -import Data.ByteString.Char8 (ByteString) +import Data.ByteString.Char8 (ByteString, isPrefixOf) import Data.ByteString.Char8 qualified as BS import Data.Char (isLower) import Data.Coerce (coerce) import Data.Foldable () import Data.Generics (extQ) import Data.List (foldl1', nub) -import Data.List.NonEmpty as NE (toList) import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) @@ -56,6 +55,7 @@ import Prettyprinter (pretty) import Booster.Definition.Attributes.Base import Booster.Definition.Attributes.Base qualified as Internal import Booster.Definition.Base (KoreDefinition (..), emptyKoreDefinition) +import Booster.Pattern.Base (InternalisedPredicate (..)) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Util (sortOfTerm) import Booster.Prettyprinter (renderDefault) @@ -87,7 +87,7 @@ internalisePattern :: Maybe [Syntax.Id] -> KoreDefinition -> Syntax.KorePattern -> - Except PatternError Internal.Pattern + Except PatternError (Internal.Pattern, Map Internal.Variable Internal.Term) internalisePattern allowAlias checkSubsorts sortVars definition p = do (terms, predicates) <- partitionM isTermM $ explodeAnd p @@ -96,9 +96,23 @@ internalisePattern allowAlias checkSubsorts sortVars definition p = do -- construct an AndTerm from all terms (checking sort consistency) term <- andTerm p =<< mapM (internaliseTerm allowAlias checkSubsorts sortVars definition) terms -- internalise all predicates - constraints <- mapM (internalisePredicate allowAlias checkSubsorts sortVars definition) predicates - pure Internal.Pattern{term, constraints = Set.fromList constraints} + (constraints, ceilConditions, substitutions) <- + partitionInternalised + <$> mapM (internalisePredicate allowAlias checkSubsorts sortVars definition) predicates + pure (Internal.Pattern{term, constraints, ceilConditions}, substitutions) where + partitionInternalised :: + [InternalisedPredicate] -> + (Set Internal.Predicate, [Internal.Ceil], Map Internal.Variable Internal.Term) + partitionInternalised = + foldr + ( \r (preds, ceils, subs) -> case r of + IsPredicate pr -> (Set.insert pr preds, ceils, subs) + IsCeil c -> (preds, c : ceils, subs) + IsSubstitution k v -> (preds, ceils, Map.insert k v subs) + ) + mempty + andTerm :: Syntax.KorePattern -> [Internal.Term] -> Except PatternError Internal.Term andTerm _ [] = error "BUG: andTerm called with empty term list" andTerm pat ts = do @@ -120,9 +134,10 @@ internaliseTermOrPredicate :: Syntax.KorePattern -> Except [PatternError] Internal.TermOrPredicate internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPatt = - Internal.APredicate - <$> (withExcept (: []) $ internalisePredicate allowAlias checkSubsorts sortVars definition syntaxPatt) - <|> Internal.TermAndPredicate + Internal.BoolOrCeilOrSubstitutionPredicate + <$> ( withExcept (: []) $ internalisePredicate allowAlias checkSubsorts sortVars definition syntaxPatt + ) + <|> uncurry Internal.TermAndPredicateAndSubstitution <$> (withExcept (: []) $ internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt) lookupInternalSort :: @@ -269,46 +284,40 @@ internalisePredicate :: Maybe [Syntax.Id] -> KoreDefinition -> Syntax.KorePattern -> - Except PatternError Internal.Predicate + Except PatternError InternalisedPredicate internalisePredicate allowAlias checkSubsorts sortVars definition@KoreDefinition{sorts} pat = case pat of Syntax.KJEVar{} -> term Syntax.KJSVar{} -> term Syntax.KJApp{} -> term Syntax.KJString{} -> term - Syntax.KJTop{} -> do - pure Internal.Top - Syntax.KJBottom{} -> do - pure Internal.Bottom + Syntax.KJTop{} -> pure $ IsPredicate $ Internal.Predicate Internal.TrueBool + Syntax.KJBottom{} -> notSupported -- TODO should we throw here? Syntax.KJNot{arg} -> do - Internal.Not <$> recursion arg - Syntax.KJAnd{patterns} -> do - -- consistency should have been checked beforehand, - -- building an AndPredicate - args <- mapM recursion patterns - pure $ foldr1 Internal.AndPredicate args - Syntax.KJOr{patterns} -> do - args <- mapM recursion patterns - pure $ foldr1 Internal.Or args - Syntax.KJImplies{first = arg1, second = arg2} -> - Internal.Implies - <$> recursion arg1 - <*> recursion arg2 - Syntax.KJIff{first = arg1, second = arg2} -> - Internal.Iff - <$> recursion arg1 - <*> recursion arg2 - Syntax.KJForall{var, varSort, arg} -> do - variableSort <- lookupInternalSort' varSort - Internal.Forall Internal.Variable{variableSort, variableName = textToBS var.getId} - <$> recursion arg - Syntax.KJExists{var, varSort, arg} -> do - variableSort <- lookupInternalSort' varSort - Internal.Forall Internal.Variable{variableSort, variableName = textToBS var.getId} - <$> recursion arg + recursion arg >>= \case + IsPredicate (Internal.Predicate (Internal.EqualsInt a b)) -> pure $ IsPredicate $ Internal.Predicate $ Internal.NEqualsInt a b + IsPredicate (Internal.Predicate (Internal.EqualsK a b)) -> pure $ IsPredicate $ Internal.Predicate $ Internal.NEqualsK a b + IsPredicate (Internal.Predicate p) -> pure $ IsPredicate $ Internal.Predicate $ Internal.NotBool p + IsSubstitution k v -> + if "@" `isPrefixOf` k.variableName + then notSupported -- @ variables are set variables, the negation of which we do not support internalising + else case sortOfTerm v of + Internal.SortInt -> pure $ IsPredicate $ Internal.Predicate $ Internal.NEqualsInt (Internal.Var k) v + otherSort -> + pure $ + IsPredicate $ + Internal.Predicate $ + Internal.NEqualsK (Internal.KSeq otherSort $ Internal.Var k) (Internal.KSeq otherSort v) + _ -> notSupported + Syntax.KJAnd{} -> notSupported + Syntax.KJOr{} -> notSupported + Syntax.KJImplies{} -> notSupported + Syntax.KJIff{} -> notSupported + Syntax.KJForall{} -> notSupported + Syntax.KJExists{} -> notSupported Syntax.KJMu{} -> notSupported Syntax.KJNu{} -> notSupported Syntax.KJCeil{arg} -> - Internal.Ceil <$> internaliseTerm allowAlias checkSubsorts sortVars definition arg + IsCeil . Internal.Ceil <$> internaliseTerm allowAlias checkSubsorts sortVars definition arg Syntax.KJFloor{} -> notSupported Syntax.KJEquals{argSort, first = arg1, second = arg2} -> do -- distinguish term and predicate equality @@ -322,26 +331,27 @@ internalisePredicate allowAlias checkSubsorts sortVars definition@KoreDefinition -- check that argS and sorts of a and b "agree" ensureEqualSorts (sortOfTerm a) argS ensureEqualSorts (sortOfTerm b) argS - pure $ Internal.EqualsTerm a b - (False, False) -> - Internal.EqualsPredicate - <$> recursion arg1 - <*> recursion arg2 + case (argS, a, b) of + (Internal.SortBool, Internal.TrueBool, x) -> pure $ IsPredicate $ Internal.Predicate x + (Internal.SortBool, x, Internal.TrueBool) -> pure $ IsPredicate $ Internal.Predicate x + (Internal.SortBool, Internal.FalseBool, x) -> pure $ IsPredicate $ Internal.Predicate $ Internal.NotBool x + (Internal.SortBool, x, Internal.FalseBool) -> pure $ IsPredicate $ Internal.Predicate $ Internal.NotBool x + (_, Internal.Var x, t) -> pure $ IsSubstitution x t + (_, t, Internal.Var x) -> pure $ IsSubstitution x t + (Internal.SortInt, _, _) -> pure $ IsPredicate $ Internal.Predicate $ Internal.EqualsInt a b + (otherSort, _, _) -> + pure $ + IsPredicate $ + Internal.Predicate $ + Internal.EqualsK (Internal.KSeq otherSort a) (Internal.KSeq otherSort b) + (False, False) -> notSupported _other -> throwE $ InconsistentPattern pat - Syntax.KJIn{argSort, first = arg1, second = arg2} -> do - a <- internaliseTerm allowAlias checkSubsorts sortVars definition arg1 - b <- internaliseTerm allowAlias checkSubsorts sortVars definition arg2 - s <- lookupInternalSort' argSort - -- check that `sort` and sorts of a and b agree - ensureEqualSorts (sortOfTerm a) s - ensureEqualSorts (sortOfTerm b) s - pure $ Internal.In a b + Syntax.KJIn{} -> notSupported Syntax.KJNext{} -> notSupported Syntax.KJRewrites{} -> notSupported -- should only occur in claims! Syntax.KJDV{} -> term - Syntax.KJMultiOr{sort, argss} -> - recursion $ Syntax.KJOr sort $ NE.toList argss + Syntax.KJMultiOr{} -> notSupported Syntax.KJLeftAssoc{} -> term Syntax.KJRightAssoc{} -> term where @@ -467,6 +477,7 @@ data PatternError | PredicateExpected Syntax.KorePattern | UnknownSymbol Syntax.Id Syntax.KorePattern | MacroOrAliasSymbolNotAllowed Syntax.Id Syntax.KorePattern + | SubstitutionNotAllowed deriving stock (Eq, Show) {- | ToJson instance (user-facing): @@ -498,6 +509,7 @@ instance ToJSON PatternError where wrap ("Unknown symbol '" <> Syntax.getId sym <> "'") p MacroOrAliasSymbolNotAllowed sym p -> wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p + SubstitutionNotAllowed -> "Substitution predicates are not allowed here" where wrap :: Text -> Syntax.KorePattern -> Value wrap msg p = object ["error" .= msg, "context" .= toJSON [p]] diff --git a/library/Booster/Syntax/ParsedKore/Internalise.hs b/library/Booster/Syntax/ParsedKore/Internalise.hs index ead0b6f09..e2c1f2778 100644 --- a/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -24,7 +24,7 @@ import Control.Monad.Trans.State import Data.Aeson (ToJSON (..), Value (..), object, (.=)) import Data.Bifunctor (first, second) import Data.ByteString.Char8 (ByteString) -import Data.Coerce (coerce) +import Data.Coerce (Coercible, coerce) import Data.Function (on) import Data.Generics (extQ) import Data.List (foldl', groupBy, nub, partition, sortOn) @@ -172,7 +172,6 @@ mergeDefs k1 k2 <*> pure (mergeTheories rewriteTheory k1 k2) <*> pure (mergeTheories functionEquations k1 k2) <*> pure (mergeTheories simplifications k1 k2) - <*> pure (mergeTheories predicateSimplifications k1 k2) where mergeTheories :: forall r. @@ -226,7 +225,6 @@ addModule , rewriteTheory = currentRewriteTheory , functionEquations = currentFctEqs , simplifications = currentSimpls - , predicateSimplifications = currentPredicateSimplifications } ) ) = @@ -285,7 +283,6 @@ addModule , rewriteTheory = currentRewriteTheory -- no rules yet , functionEquations = Map.empty , simplifications = Map.empty - , predicateSimplifications = Map.empty } let internaliseAlias :: @@ -308,17 +305,22 @@ addModule withExcept DefinitionSortError $ internaliseSort (Set.fromList paramNames) sorts' sort let internalArgs = uncurry Def.Variable <$> zip internalArgSorts argNames - internalRhs <- - withExcept (DefinitionAliasError name.getId . InconsistentAliasPattern) $ - internaliseTermOrPredicate + + (internalRhs, substitution) <- + withExcept (DefinitionAliasError name.getId . InconsistentAliasPattern . (: [])) $ + internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) defWithNewSortsAndSymbols.partial rhs - let rhsSort = Util.sortOfTermOrPredicate internalRhs + unless (null substitution) $ + throwE $ + DefinitionAliasError name.getId $ + InconsistentAliasPattern [SubstitutionNotAllowed] + let rhsSort = Util.sortOfPattern internalRhs unless - (fromMaybe internalResSort rhsSort == internalResSort) + (rhsSort == internalResSort) (throwE (DefinitionSortError (GeneralError "IncompatibleSorts"))) return (internalName, Alias{name = internalName, params, args = internalArgs, rhs = internalRhs}) -- filter out "antiLeft" aliases, recognised by name and argument count @@ -336,7 +338,6 @@ addModule subsortPairs = mapMaybe retractSubsortRule newAxioms newFunctionEquations = mapMaybe retractFunctionRule newAxioms newSimplifications = mapMaybe retractSimplificationRule newAxioms - newPredicateSimplifications = mapMaybe retractPredicateSimplificationRule newAxioms let rewriteTheory = addToTheoryWith (Idx.kCellTermIndex . (.lhs)) newRewriteRules currentRewriteTheory functionEquations = @@ -344,19 +345,12 @@ addModule simplifications = addToTheoryWith (Idx.termTopIndex . (.lhs)) newSimplifications currentSimpls sorts = subsortClosure sorts' subsortPairs - predicateSimplifications = - addToTheoryWith - (predicateTopIndex . (.target)) - newPredicateSimplifications - currentPredicateSimplifications - pure $ defWithAliases.partial { sorts , rewriteTheory , functionEquations , simplifications - , predicateSimplifications } where -- Uses 'getKey' to construct a finite mapping from the list, @@ -488,9 +482,6 @@ data AxiomResult FunctionAxiom (RewriteRule "Function") | -- | Simplification SimplificationAxiom (RewriteRule "Simplification") - | -- | Predicate simplification - PredicateSimplificationAxiom PredicateEquation - deriving (Show) -- retract helpers retractRewriteRule :: AxiomResult -> Maybe (RewriteRule "Rewrite") @@ -509,10 +500,6 @@ retractSimplificationRule :: AxiomResult -> Maybe (RewriteRule "Simplification") retractSimplificationRule (SimplificationAxiom r) = Just r retractSimplificationRule _ = Nothing -retractPredicateSimplificationRule :: AxiomResult -> Maybe PredicateEquation -retractPredicateSimplificationRule (PredicateSimplificationAxiom r) = Just r -retractPredicateSimplificationRule _ = Nothing - -- helper type to carry relevant extracted data from a pattern (what -- is passed to the internalising function later) data AxiomData @@ -548,7 +535,7 @@ data AxiomData * matching logic simplification equation \implies(, \equals(lhs, \and(, ))) (with lhs something different from a symbol application). Used in - domains.md for SortBool simplification + domains.md for SortBool simplification and for ceil rules but ignored here. * functional/total rule \exists(V:_ , \equals(V, (..args..))) [functional()] * no confusion, same constructor (con) @@ -621,11 +608,9 @@ classifyAxiom parsedAx@ParsedAxiom{axiom, sortVars, attributes} = <$> withExcept DefinitionAttributeError (mkAttributes parsedAx) | otherwise -> throwE $ DefinitionAxiomError $ MalformedEquation parsedAx - -- implies with the LHS not a symbol application, tagged as simplification - Syntax.KJImplies _ req (Syntax.KJEquals _sort _ lhs rhs@Syntax.KJAnd{}) - | hasAttribute "simplification" -> - Just . SimplificationAxiom' req lhs rhs sortVars - <$> withExcept DefinitionAttributeError (mkAttributes parsedAx) + -- implies with the LHS not a symbol application, tagged as simplification. Ignoring + Syntax.KJImplies _ _ (Syntax.KJEquals _sort _ _ Syntax.KJAnd{}) + | hasAttribute "simplification" -> pure Nothing -- implies with equals but RHS not an and: malformed equation Syntax.KJImplies _ _req (Syntax.KJEquals _sort _ _lhs _rhs) -> throwE $ DefinitionAxiomError $ MalformedEquation parsedAx @@ -772,18 +757,12 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do -- prefix all variables in lhs and rhs with "Rule#" to avoid -- name clashes with patterns from the user -- filter out literal `Top` constraints - lhs <- - fmap (removeTops . Util.modifyVariables (Util.modifyVarName ("Rule#" <>))) $ - withExcept (DefinitionPatternError ref) $ - internalisePattern AllowAlias IgnoreSubsorts Nothing partialDefinition left + lhs <- internalisePattern' ref (Util.modifyVarName ("Rule#" <>)) left existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName ("Ex#" <>) v | otherwise = Util.modifyVarName ("Rule#" <>) v - rhs <- - fmap (removeTops . Util.modifyVariables renameVariable) $ - withExcept (DefinitionPatternError ref) $ - internalisePattern AllowAlias IgnoreSubsorts Nothing partialDefinition right + rhs <- internalisePattern' ref renameVariable right let notPreservesDefinednessReasons = -- users can override the definedness computation by an explicit attribute if coerce axAttributes.preserving @@ -808,6 +787,13 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do , existentials } where + internalisePattern' ref f t = do + (pat, substitution) <- + withExcept (DefinitionPatternError ref) $ + internalisePattern AllowAlias IgnoreSubsorts Nothing partialDefinition t + unless (null substitution) $ throwE $ DefinitionPatternError ref SubstitutionNotAllowed + pure $ removeTrueBools $ Util.modifyVariables f pat + mkVar (name, sort) = do variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort let variableName = textToBS name.getId @@ -839,17 +825,14 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu -- name clashes with patterns from the user -- filter out literal `Top` constraints lhs <- - fmap (removeTops . Util.modifyVariables (Util.modifyVarName ("Rule#" <>))) $ + fmap (removeTrueBools . Util.modifyVariables (Util.modifyVarName ("Rule#" <>))) $ Util.retractPattern result `orFailWith` DefinitionTermOrPredicateError ref (PatternExpected result) existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName ("Ex#" <>) v | otherwise = Util.modifyVarName ("Rule#" <>) v - rhs <- - fmap (removeTops . Util.modifyVariables renameVariable) $ - withExcept (DefinitionPatternError ref) $ - internalisePattern AllowAlias IgnoreSubsorts Nothing partialDefinition right + rhs <- internalisePattern' ref renameVariable right let notPreservesDefinednessReasons = -- users can override the definedness computation by an explicit attribute @@ -882,107 +865,104 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu let variableName = textToBS name.getId pure $ Variable{variableSort, variableName} + internalisePattern' ref f t = do + (pat, substitution) <- + withExcept (DefinitionPatternError ref) $ + internalisePattern AllowAlias IgnoreSubsorts Nothing partialDefinition t + unless (null substitution) $ throwE $ DefinitionPatternError ref SubstitutionNotAllowed + pure $ removeTrueBools $ Util.modifyVariables f pat + expandAlias :: Alias -> [Def.Term] -> Except DefinitionError Def.TermOrPredicate expandAlias alias currentArgs | length alias.args /= length currentArgs = throwE $ DefinitionAliasError (Text.decodeLatin1 alias.name) $ WrongAliasArgCount alias currentArgs - | otherwise = + | otherwise = do let substitution = Map.fromList (zip alias.args currentArgs) - in return $ substitute substitution alias.rhs + substitute substitution alias.rhs where - substitute substitution termOrPredicate = - case termOrPredicate of - Def.APredicate predicate -> - Def.APredicate $ Util.substituteInPredicate substitution predicate - Def.TermAndPredicate Def.Pattern{term, constraints} -> - Def.TermAndPredicate - Def.Pattern - { term = Util.substituteInTerm substitution term - , constraints = - Set.map (Util.substituteInPredicate substitution) constraints - } - -removeTops :: Def.Pattern -> Def.Pattern -removeTops p = p{Def.constraints = Set.delete Def.Top p.constraints} - -{- | Internalises simplification rules, for both term simplification - (represented as a 'RewriteRule') and predicate simplification - (represented as a 'PredicateEquation'). + substitute substitution Def.Pattern{term, constraints, ceilConditions} = do + pure $ + Def.TermAndPredicateAndSubstitution + Def.Pattern + { term = Util.substituteInTerm substitution term + , constraints = + Set.fromList $ sub substitution <$> Set.toList constraints + , ceilConditions = + sub substitution <$> ceilConditions + } + mempty + + sub :: (Coercible a Def.Term, Coercible Def.Term a) => Map Variable Def.Term -> a -> a + sub substitution = coerce . Util.substituteInTerm substitution . coerce + +removeTrueBools :: Def.Pattern -> Def.Pattern +removeTrueBools p = p{Def.constraints = Set.filter (/= Def.Predicate Def.TrueBool) p.constraints} + +{- | Internalises simplification rules, for term simplification + (represented as a 'RewriteRule'). Term simplifications may introduce undefined terms, or remove them erroneously, so the 'preservesDefinedness' check refers to both the LHS and the RHS term. - Predicates have no problem with definedness, as a rule with a - \bottom predicate will simply never apply -} internaliseSimpleEquation :: KoreDefinition -> -- context Syntax.KorePattern -> -- requires - Syntax.KorePattern -> -- LHS + Syntax.KorePattern -> -- LHS, assumed to be a _symbol application_ Syntax.KorePattern -> -- And(RHS, ensures) [Syntax.Id] -> -- sort variables AxiomAttributes -> Except DefinitionError AxiomResult internaliseSimpleEquation partialDef precond left right sortVars attrs - | coerce attrs.simplification = do - lhsIsTerm <- withExcept (DefinitionPatternError (sourceRef attrs)) $ isTermM left - if lhsIsTerm - then do - lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precond] - rhs <- internalisePattern' right - let - -- checking the lhs term, too, as a safe approximation - -- (rhs may _introduce_ undefined, lhs may _hide_ it) - undefinedSymbols = - nub . concatMap (Util.filterTermSymbols (not . Util.isDefinedSymbol)) $ - [lhs.term, rhs.term] - computedAttributes = - ComputedAxiomAttributes - { containsAcSymbols = - any (Util.checkTermSymbols Util.checkSymbolIsAc) [lhs.term, rhs.term] - , notPreservesDefinednessReasons = - if coerce attrs.preserving - then [] - else map (UndefinedSymbol . (.name)) undefinedSymbols - } - attributes = attrs{concreteness = Util.modifyVarNameConcreteness ("Eq#" <>) attrs.concreteness} - pure $ - SimplificationAxiom - RewriteRule - { lhs = lhs.term - , rhs = rhs.term - , requires = lhs.constraints - , ensures = rhs.constraints - , attributes - , computedAttributes - , existentials = Set.empty - } - else do - target <- internalisePredicate' left - conditions <- mapM internalisePredicate' $ explodeAnd precond - rhs <- mapM internalisePredicate' $ explodeAnd right - -- undefined predicates will invalidate the rule, no flags required - let computedAttributes = ComputedAxiomAttributes False [] - pure $ - PredicateSimplificationAxiom - PredicateEquation - { target - , conditions - , rhs - , attributes = attrs - , computedAttributes - } - | otherwise = error "internaliseSimpleEquation should only be called for simplifications" + | not (coerce attrs.simplification) = + error $ "internaliseSimpleEquation should only be called for simplifications" <> show attrs + | Syntax.KJApp{} <- left = do + -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) + lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precond] + rhs <- internalisePattern' right + let + -- checking the lhs term, too, as a safe approximation + -- (rhs may _introduce_ undefined, lhs may _hide_ it) + undefinedSymbols = + nub . concatMap (Util.filterTermSymbols (not . Util.isDefinedSymbol)) $ + [lhs.term, rhs.term] + computedAttributes = + ComputedAxiomAttributes + { containsAcSymbols = + any (Util.checkTermSymbols Util.checkSymbolIsAc) [lhs.term, rhs.term] + , notPreservesDefinednessReasons = + if coerce attrs.preserving + then [] + else map (UndefinedSymbol . (.name)) undefinedSymbols + } + attributes = + attrs{concreteness = Util.modifyVarNameConcreteness ("Eq#" <>) attrs.concreteness} + pure $ + SimplificationAxiom + RewriteRule + { lhs = lhs.term + , rhs = rhs.term + , requires = lhs.constraints + , ensures = rhs.constraints + , attributes + , computedAttributes + , existentials = Set.empty + } + | otherwise = + -- we hit a simplification with top level ML connective or an + -- unexpected top-level term, which we want to ignore + error $ "internaliseSimpleEquation should only be called with app nodes as LHS" <> show left where - internalisePattern' = - withExcept (DefinitionPatternError (sourceRef attrs)) - . fmap (removeTops . Util.modifyVariables (Util.modifyVarName ("Eq#" <>))) - . internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef - internalisePredicate' = - withExcept (DefinitionPatternError (sourceRef attrs)) - . internalisePredicate AllowAlias IgnoreSubsorts (Just sortVars) partialDef + internalisePattern' t = do + (pat, substitution) <- + withExcept (DefinitionPatternError (sourceRef attrs)) $ + internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef t + unless (null substitution) $ + throwE $ + DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed + pure $ removeTrueBools $ Util.modifyVariables (Util.modifyVarName ("Eq#" <>)) pat {- | Internalises a function rule from its components that were matched before. @@ -1008,16 +988,19 @@ internaliseFunctionEquation :: Except DefinitionError AxiomResult internaliseFunctionEquation partialDef requires args leftTerm right sortVars attrs = do -- internalise the LHS (LHS term and requires) - left <- -- expected to be a simple term, f(X_1, X_2,..) + (left, substitution) <- -- expected to be a simple term, f(X_1, X_2,..) withExcept (DefinitionPatternError (sourceRef attrs)) $ internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef $ Syntax.KJAnd leftTerm.sort [leftTerm, requires] + unless (null substitution) $ + throwE $ + DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed -- extract argument binders from predicates and inline in to LHS term argPairs <- mapM internaliseArg args let lhs = - removeTops . Util.modifyVariables (Util.modifyVarName ("Eq#" <>)) $ + removeTrueBools . Util.modifyVariables (Util.modifyVarName ("Eq#" <>)) $ left{Def.term = Util.substituteInTerm (Map.fromList argPairs) left.term} - rhs <- internaliseSide right + rhs <- internalisePattern' right let argsUndefined = concatMap (Util.filterTermSymbols (not . Util.isDefinedSymbol) . snd) argPairs rhsUndefined = @@ -1052,10 +1035,14 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att Def.SymbolApplication symbol _ _ -> symbol.attributes.symbolType == TotalFunction _ -> False - internaliseSide = - withExcept (DefinitionPatternError (sourceRef attrs)) - . fmap (removeTops . Util.modifyVariables (Util.modifyVarName ("Eq#" <>))) - . internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef + internalisePattern' t = do + (pat, substitution) <- + withExcept (DefinitionPatternError (sourceRef attrs)) $ + internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef t + unless (null substitution) $ + throwE $ + DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed + pure $ removeTrueBools $ Util.modifyVariables (Util.modifyVarName ("Eq#" <>)) pat internaliseTerm' = withExcept (DefinitionPatternError (sourceRef attrs)) diff --git a/package.yaml b/package.yaml index a60539183..41272b862 100644 --- a/package.yaml +++ b/package.yaml @@ -231,7 +231,9 @@ executables: main: Server.hs dependencies: - aeson + - aeson-pretty - base + - bytestring - casing - clock - conduit-extra @@ -246,6 +248,7 @@ executables: - monad-logger - optparse-applicative - prettyprinter + - recursion-schemes - stm - text - transformers diff --git a/test/internalisation/bool.kore.report b/test/internalisation/bool.kore.report index 9ca256e5c..82edf6a41 100644 --- a/test/internalisation/bool.kore.report +++ b/test/internalisation/bool.kore.report @@ -51,13 +51,3 @@ Function equations by term index: - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (929, 8) - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (928, 8) Simplifications by term index: -Predicate simplifications by term index: -- \equalsTerm: 8 - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (972, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (974, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (969, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (967, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (973, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (968, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (971, 8) - - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (966, 8) diff --git a/test/internalisation/does-not-preserve-definedness.kore.report b/test/internalisation/does-not-preserve-definedness.kore.report index 29d00fd42..2417cac8a 100644 --- a/test/internalisation/does-not-preserve-definedness.kore.report +++ b/test/internalisation/does-not-preserve-definedness.kore.report @@ -212,5 +212,3 @@ Function equations by term index: - UNKNOWN - UNKNOWN Simplifications by term index: -Predicate simplifications by term index: -- \ceil: UNKNOWN diff --git a/test/internalisation/existentials.kore.report b/test/internalisation/existentials.kore.report index ce4bb0601..00d0bc58e 100644 --- a/test/internalisation/existentials.kore.report +++ b/test/internalisation/existentials.kore.report @@ -223,5 +223,3 @@ Function equations by term index: - UNKNOWN - UNKNOWN Simplifications by term index: -Predicate simplifications by term index: -- \ceil: UNKNOWN diff --git a/test/internalisation/imp.kore.report b/test/internalisation/imp.kore.report index e5ee1de0a..c55e81ad4 100644 --- a/test/internalisation/imp.kore.report +++ b/test/internalisation/imp.kore.report @@ -537,36 +537,3 @@ Simplifications by term index: - Lbl_modInt_: 2 - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1242, 5) - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1162, 8) -Predicate simplifications by term index: -- \ceil: 6 - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1179, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1178, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1182, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1181, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1180, 8) - - UNKNOWN -- \equalsTerm: 24 - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1222, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1220, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2201, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2199, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1218, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1216, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2197, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2195, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (972, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (974, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (969, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (967, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1223, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2202, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1219, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2198, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (973, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (968, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1221, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2200, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1217, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2196, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (971, 8) - - /home/jost/work/RV/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (966, 8) diff --git a/test/internalisation/preserves-definedness-total-function.kore.report b/test/internalisation/preserves-definedness-total-function.kore.report index 8dba9d990..dc929c8ef 100644 --- a/test/internalisation/preserves-definedness-total-function.kore.report +++ b/test/internalisation/preserves-definedness-total-function.kore.report @@ -212,5 +212,3 @@ Function equations by term index: - UNKNOWN - UNKNOWN Simplifications by term index: -Predicate simplifications by term index: -- \ceil: UNKNOWN diff --git a/test/internalisation/preserves-definedness.kore.report b/test/internalisation/preserves-definedness.kore.report index 98b7f240c..7878b27e1 100644 --- a/test/internalisation/preserves-definedness.kore.report +++ b/test/internalisation/preserves-definedness.kore.report @@ -212,5 +212,3 @@ Function equations by term index: - UNKNOWN - UNKNOWN Simplifications by term index: -Predicate simplifications by term index: -- \ceil: UNKNOWN diff --git a/test/internalisation/subsorts.kore.report b/test/internalisation/subsorts.kore.report index c6154bf19..3473cd452 100644 --- a/test/internalisation/subsorts.kore.report +++ b/test/internalisation/subsorts.kore.report @@ -314,14 +314,3 @@ Function equations by term index: - UNKNOWN - UNKNOWN Simplifications by term index: -Predicate simplifications by term index: -- \ceil: UNKNOWN -- \equalsTerm: 8 - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (944, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (946, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (941, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (939, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (945, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (940, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (943, 8) - - /nix/store/9dqw7zw0v1fv1ghrv5hc8r071qpgz46z-k-5.6.88-4c09d86ed218ee08d521c5780b0368dc5f330383-maven/include/kframework/builtin/domains.md : (938, 8) diff --git a/test/internalisation/test-totalSupply-definition.kore.report b/test/internalisation/test-totalSupply-definition.kore.report index fce7ce6ef..4771101ad 100644 --- a/test/internalisation/test-totalSupply-definition.kore.report +++ b/test/internalisation/test-totalSupply-definition.kore.report @@ -5829,47 +5829,3 @@ Simplifications by term index: - evm-semantics/tests/specs/lemmas.k : (290, 10) - evm-semantics/tests/specs/lemmas.k : (291, 10) - evm-semantics/tests/specs/lemmas.k : (48, 10) -Predicate simplifications by term index: -- \ceil: 11 - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (411, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1085, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1084, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1088, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1087, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1086, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1996, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1995, 8) - - UNKNOWN - - UNKNOWN - - UNKNOWN -- \equalsTerm: 30 - - evm-semantics/tests/specs/lemmas.k : (408, 10) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1128, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1126, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2107, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2105, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1124, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1122, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2103, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2101, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (878, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (444, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (446, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (880, 8) - - evm-semantics/.build/usr/lib/kevm/include/kframework/infinite-gas.md : (62, 10) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (875, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (873, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1129, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2108, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1125, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2104, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (443, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (445, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (879, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (874, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1127, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2106, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (1123, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (2102, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (877, 8) - - /Users/anapantilie/RV/k/k-distribution/target/release/k/include/kframework/builtin/domains.md : (872, 8) diff --git a/test/llvm-integration/LLVM.hs b/test/llvm-integration/LLVM.hs index 7f0d2a547..6465f1452 100644 --- a/test/llvm-integration/LLVM.hs +++ b/test/llvm-integration/LLVM.hs @@ -204,7 +204,6 @@ testDef = Map.empty -- no rules Map.empty -- no function equations Map.empty -- no simplifications - Map.empty -- no predicate simplifications {- To refresh the definition below, run this using the repl and fix up the remainder of the file if differences are shown. @@ -221,7 +220,6 @@ displayTestDef = do , aliases = Map.empty , functionEquations = Map.empty , simplifications = Map.empty - , predicateSimplifications = Map.empty } -- compare to what we have if testDef == prunedDef diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index acfea7cfb..08b15c6e1 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -386,8 +386,8 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re def simplified.state.term case internalPattern of - Right p -> - pure $ Right (Booster.toExecState p, simplified.logs) + Right (p, sub) -> + pure $ Right (Booster.toExecState p sub, simplified.logs) Left err -> do Log.logWarnNS "proxy" $ "Error processing execute state simplification result: " diff --git a/unit-tests/Test/Booster/Fixture.hs b/unit-tests/Test/Booster/Fixture.hs index 6db51d5bc..722c614c5 100644 --- a/unit-tests/Test/Booster/Fixture.hs +++ b/unit-tests/Test/Booster/Fixture.hs @@ -56,7 +56,6 @@ testDefinition = , rewriteTheory = Map.empty , functionEquations = Map.empty , simplifications = Map.empty - , predicateSimplifications = Map.empty } where super `withSubsorts` subs = diff --git a/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index e235dfc35..e835e47a4 100644 --- a/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -126,25 +126,20 @@ test_simplifyPattern = "Performing simplifications" [ testCase "No simplification applies" $ do let subj = [trm| f1{}(f2{}(A:SomeSort{})) |] - simpl Pattern{term = subj, constraints = mempty} - @?= Right Pattern{term = subj, constraints = mempty} - simpl Pattern{term = subj, constraints = mempty} - @?= Right Pattern{term = subj, constraints = mempty} + simpl (Pattern_ subj) @?= Right (Pattern_ subj) + simpl (Pattern_ subj) @?= Right (Pattern_ subj) , -- con1(con2(f2(a))) => con2(f2(a)) testCase "Simplification of constructors" $ do let subj = app con1 [app con2 [app f2 [a]]] - simpl Pattern{term = subj, constraints = mempty} - @?= Right Pattern{term = app con2 [app f2 [a]], constraints = mempty} - simpl Pattern{term = subj, constraints = mempty} - @?= Right Pattern{term = app con2 [app f2 [a]], constraints = mempty} + simpl (Pattern_ subj) + @?= Right (Pattern_ $ app con2 [app f2 [a]]) + simpl (Pattern_ subj) + @?= Right (Pattern_ $ app con2 [app f2 [a]]) , -- con3(f2(a), f2(a)) => inj{sub,some}(con4(f2(a), f2(a))) testCase "Simplification with argument match" $ do - let subj = Pattern{term = [trm| con3{}(f2{}(A:SomeSort{}), f2{}(A:SomeSort{})) |], constraints = mempty} + let subj = Pattern_ [trm| con3{}(f2{}(A:SomeSort{}), f2{}(A:SomeSort{})) |] result = - Pattern - { term = [trm| inj{AnotherSort{}, SomeSort{}}(con4{}(f2{}(A:SomeSort{}), f2{}(A:SomeSort{}))) |] - , constraints = mempty - } + Pattern_ [trm| inj{AnotherSort{}, SomeSort{}}(con4{}(f2{}(A:SomeSort{}), f2{}(A:SomeSort{}))) |] simpl subj @?= Right result ] where diff --git a/unit-tests/Test/Booster/Pattern/Binary.hs b/unit-tests/Test/Booster/Pattern/Binary.hs index 610a787d1..4ca0b3636 100644 --- a/unit-tests/Test/Booster/Pattern/Binary.hs +++ b/unit-tests/Test/Booster/Pattern/Binary.hs @@ -54,24 +54,11 @@ genTerm = genPredicate :: Gen Predicate genPredicate = - Gen.recursive - Gen.choice - [pure Bottom, pure Top] - [ AndPredicate <$> genPredicate <*> genPredicate - , Ceil <$> genTerm - , EqualsTerm <$> genTerm <*> genTerm - , EqualsPredicate <$> genPredicate <*> genPredicate - , Exists <$> genVariable <*> genPredicate - , Forall <$> genVariable <*> genPredicate - , Iff <$> genPredicate <*> genPredicate - , Implies <$> genPredicate <*> genPredicate - , In <$> genTerm <*> genTerm - , Not <$> genPredicate - , Or <$> genPredicate <*> genPredicate - ] + Predicate + <$> Gen.choice [pure TrueBool, pure FalseBool, genTerm] genPattern :: Gen Pattern -genPattern = Pattern <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) +genPattern = (\t cs -> Pattern t cs mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) test_BinaryRoundTrips :: [TestTree] test_BinaryRoundTrips = diff --git a/unit-tests/Test/Booster/Pattern/Rewrite.hs b/unit-tests/Test/Booster/Pattern/Rewrite.hs index b81b3b616..d590d103b 100644 --- a/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -76,50 +76,50 @@ rule1, rule1', rule2, rule3, rule4 :: RewriteRule "Rewrite" rule1 = rule (Just "con1-f1") - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |] ) - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |] ) 42 rule1' = rule (Just "con1-f1'") - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( X:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) 50 rule2 = rule (Just "con1-f2") - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, X:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) 50 rule3 = rule (Just "con3-con1") - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), Y:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ), RuleVar:SortK{}) ) |] ) 42 rule4 = rule (Just "con4-f2-partial") - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, Y:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) - ( mkPattern + ( Pattern_ [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f2{}( Y:SomeSort{} ) ), RuleVar:SortK{}) ) |] ) 42 @@ -152,9 +152,6 @@ rule ruleLabel lhs rhs priority = , existentials = mempty } -mkPattern :: Term -> Pattern -mkPattern t = Pattern t mempty - withComputedAttributes :: RewriteRule r -> ComputedAxiomAttributes -> RewriteRule r r@RewriteRule{lhs} `withComputedAttributes` computedAttributes = r{lhs, computedAttributes} @@ -226,7 +223,7 @@ definednessUnclear = testCase "con4 rewrite to f2 might become undefined" $ do let pcon4 = [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( \dv{SomeSort{}}("thing"), \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |] - pcon4 `failsWith` DefinednessUnclear rule4 (mkPattern pcon4) [UndefinedSymbol "f2"] + pcon4 `failsWith` DefinednessUnclear rule4 (Pattern_ pcon4) [UndefinedSymbol "f2"] rewriteStuck = testCase "con3 app is stuck (no rules apply)" $ do let con3App = @@ -249,21 +246,21 @@ runWith :: Term -> Either (RewriteFailed "Rewrite") (RewriteResult Pattern) runWith t = second fst $ unsafePerformIO - (runNoLoggingT $ runRewriteT False def Nothing mempty (rewriteStep [] [] $ mkPattern t)) + (runNoLoggingT $ runRewriteT False def Nothing mempty (rewriteStep [] [] $ Pattern_ t)) rewritesTo :: Term -> (Text, Term) -> IO () t1 `rewritesTo` (lbl, t2) = - runWith t1 @?= Right (RewriteFinished (Just lbl) Nothing $ mkPattern t2) + runWith t1 @?= Right (RewriteFinished (Just lbl) Nothing $ Pattern_ t2) getsStuck :: Term -> IO () getsStuck t1 = - runWith t1 @?= Right (RewriteStuck $ mkPattern t1) + runWith t1 @?= Right (RewriteStuck $ Pattern_ t1) branchesTo :: Term -> [(Text, Term)] -> IO () t `branchesTo` ts = runWith t @?= Right - (RewriteBranch (mkPattern t) $ NE.fromList $ map (\(lbl, t') -> (lbl, Nothing, mkPattern t')) ts) + (RewriteBranch (Pattern_ t) $ NE.fromList $ map (\(lbl, t') -> (lbl, Nothing, Pattern_ t')) ts) failsWith :: Term -> RewriteFailed "Rewrite" -> IO () failsWith t err = @@ -274,7 +271,7 @@ failsWith t err = runRewrite :: Term -> IO (Natural, RewriteResult Term) runRewrite t = do - (counter, _, res) <- runNoLoggingT $ performRewrite False def Nothing Nothing [] [] $ mkPattern t + (counter, _, res) <- runNoLoggingT $ performRewrite False def Nothing Nothing [] [] $ Pattern_ t pure (counter, fmap (.term) res) aborts :: RewriteFailed "Rewrite" -> Term -> IO () @@ -417,7 +414,7 @@ supportsDepthControl = rewritesToDepth :: MaxDepth -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () rewritesToDepth (MaxDepth depth) (Steps n) t t' f = do (counter, _, res) <- - runNoLoggingT $ performRewrite False def Nothing (Just depth) [] [] $ mkPattern t + runNoLoggingT $ performRewrite False def Nothing (Just depth) [] [] $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t') supportsCutPoints :: TestTree @@ -469,7 +466,7 @@ supportsCutPoints = rewritesToCutPoint :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () rewritesToCutPoint lbl (Steps n) t t' f = do (counter, _, res) <- - runNoLoggingT $ performRewrite False def Nothing Nothing [lbl] [] $ mkPattern t + runNoLoggingT $ performRewrite False def Nothing Nothing [lbl] [] $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t') supportsTerminalRules :: TestTree @@ -499,5 +496,5 @@ supportsTerminalRules = rewritesToTerminal :: Text -> Steps -> Term -> t -> (t -> RewriteResult Term) -> IO () rewritesToTerminal lbl (Steps n) t t' f = do (counter, _, res) <- - runNoLoggingT $ performRewrite False def Nothing Nothing [] [lbl] $ mkPattern t + runNoLoggingT $ performRewrite False def Nothing Nothing [] [lbl] $ Pattern_ t (counter, fmap (.term) res) @?= (n, f t')