From baa73d39a782df2bb5520fbf9459df559c2d9ca5 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Fri, 28 Jun 2024 09:26:38 +0100 Subject: [PATCH] Add options to the kore term pretty printer (#3963) Add the following options when pretty printing terms: * `decode` - decode symbol labels and strip the `Lbl` prefix * `truncate` - truncate long domain values * `infix` - try to re-assemble infix notation from the holes in label syntax (may not always be correct). For example: ``` ... Uncertain about match with rule. Remainder: #range( Eq#VarB1:SortBytes{} , Eq#VarS2:SortInt{} , Eq#VarW2:SortInt{} ) == buf("32", lookup(VarCONTRACT-FAKEETH_STORAGE:SortMap{}, keccak( buf("32", VarCALLER_ID:SortInt{}) +Bytes "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL" ))), #range( Eq#VarB1:SortBytes{} , Eq#VarS1:SortInt{} , Eq#VarW1:SortInt{} ) == buf("32", lookup(VarCONTRACT-FAKEETH_STORAGE:SortMap{}, keccak( buf("32", VarCONTRACT_ID:SortInt{}) +Bytes buf("32", keccak( buf("32", VarCALLER_ID:SortInt{}) +Bytes "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH" )) ))) ``` These can now be passed to the server via the `--pretty-print` flag. E.g. `--pretty-print truncated,decode` will preserve current behaviour (and is set as default when no explicit option is provided) --------- Co-authored-by: github-actions Co-authored-by: rv-jenkins --- booster/library/Booster/Builtin/Base.hs | 3 +- booster/library/Booster/Builtin/KEQUAL.hs | 5 +- booster/library/Booster/CLOptions.hs | 17 + booster/library/Booster/Definition/Ceil.hs | 19 +- booster/library/Booster/Definition/Util.hs | 7 +- booster/library/Booster/JsonRpc.hs | 758 +++++++++--------- booster/library/Booster/JsonRpc/Utils.hs | 31 +- booster/library/Booster/Log.hs | 37 +- .../library/Booster/Pattern/ApplyEquations.hs | 272 ++++--- booster/library/Booster/Pattern/Base.hs | 83 -- booster/library/Booster/Pattern/Binary.hs | 5 +- booster/library/Booster/Pattern/Match.hs | 39 +- booster/library/Booster/Pattern/Pretty.hs | 189 +++++ booster/library/Booster/Pattern/Rewrite.hs | 435 +++++----- booster/library/Booster/SMT/Interface.hs | 23 +- booster/library/Booster/SMT/Translate.hs | 17 +- .../Booster/Syntax/Json/Internalise.hs | 23 +- .../Booster/Syntax/ParsedKore/Internalise.hs | 14 +- .../simplify-log.txt.golden | 10 +- booster/tools/booster/Server.hs | 80 +- dev-tools/booster-dev/Server.hs | 8 +- dev-tools/kore-rpc-dev/Server.hs | 6 +- dev-tools/parsetest/Parsetest.hs | 4 +- dev-tools/pretty/Pretty.hs | 11 +- 24 files changed, 1195 insertions(+), 901 deletions(-) create mode 100644 booster/library/Booster/Pattern/Pretty.hs diff --git a/booster/library/Booster/Builtin/Base.hs b/booster/library/Booster/Builtin/Base.hs index d50a1ff2f2..515f0b16ef 100644 --- a/booster/library/Booster/Builtin/Base.hs +++ b/booster/library/Booster/Builtin/Base.hs @@ -21,6 +21,7 @@ import Data.Text.Encoding qualified as Text import Prettyprinter (pretty) import Booster.Pattern.Base +import Booster.Pattern.Pretty import Booster.Pattern.Util import Booster.Prettyprinter @@ -68,5 +69,5 @@ t `shouldHaveSort` s throwE $ Text.unlines [ "Argument term has unexpected sort (expected " <> Text.decodeLatin1 s <> "):" - , renderText (pretty t) + , renderText (pretty (PrettyWithModifiers @['Decoded, 'Truncated] t)) ] diff --git a/booster/library/Booster/Builtin/KEQUAL.hs b/booster/library/Booster/Builtin/KEQUAL.hs index 6a27b30276..94911b671b 100644 --- a/booster/library/Booster/Builtin/KEQUAL.hs +++ b/booster/library/Booster/Builtin/KEQUAL.hs @@ -22,6 +22,7 @@ import Prettyprinter import Booster.Builtin.Base import Booster.Pattern.Base import Booster.Pattern.Bool +import Booster.Pattern.Pretty import Booster.Pattern.Util (isConstructorSymbol, sortOfTerm) import Booster.Prettyprinter (renderText) @@ -40,8 +41,8 @@ iteHook args unless (sortOfTerm thenVal == sortOfTerm elseVal) $ throwE . Text.unlines $ [ "Different sorts in alternatives:" - , renderText $ pretty thenVal - , renderText $ pretty elseVal + , renderText $ pretty (PrettyWithModifiers @['Decoded, 'Truncated] thenVal) + , renderText $ pretty (PrettyWithModifiers @['Decoded, 'Truncated] elseVal) ] case cond of TrueBool -> pure $ Just thenVal diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index 8862f906ed..42c9fa516f 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -28,6 +28,7 @@ import Text.Read (readMaybe) import Booster.GlobalState (EquationOptions (..)) import Booster.Log.Context (ContextFilter, ctxt, readContextFilter) +import Booster.Pattern.Pretty import Booster.SMT.Interface (SMTOptions (..), defaultSMTOptions) import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr) import Booster.Trace (CustomUserEventType) @@ -48,6 +49,7 @@ data CLOptions = CLOptions , smtOptions :: Maybe SMTOptions , equationOptions :: EquationOptions , indexCells :: [Text] + , prettyPrintOptions :: [ModifierT] , -- developer options below eventlogEnabledUserEvents :: [CustomUserEventType] } @@ -162,6 +164,14 @@ clOptionsParser = <> help "Names of configuration cells to index rewrite rules with (default: 'k')" <> value [] ) + <*> option + (eitherReader $ mapM (readModifierT . trim) . splitOn ",") + ( metavar "PRETTY_PRINT" + <> value [Decoded, Truncated] + <> long "pretty-print" + <> help "Prety print options for kore terms: decode, infix, truncated" + <> showDefault + ) -- developer options below <*> many ( option @@ -201,6 +211,13 @@ clOptionsParser = "json" -> Right Json other -> Left $ other <> ": Unsupported log format" + readModifierT :: String -> Either String ModifierT + readModifierT = \case + "truncated" -> Right Truncated + "infix" -> Right Infix + "decoded" -> Right Decoded + other -> Left $ other <> ": Unsupported prettry printer option" + readTimeStampFormat :: String -> Either String TimestampFormat readTimeStampFormat = \case "pretty" -> Right Pretty diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs index d3e1b90c8f..f2b9922816 100644 --- a/booster/library/Booster/Definition/Ceil.hs +++ b/booster/library/Booster/Definition/Ceil.hs @@ -16,6 +16,7 @@ import Booster.Pattern.Base import Booster.LLVM as LLVM (API, simplifyBool) import Booster.Log import Booster.Pattern.Bool +import Booster.Pattern.Pretty import Booster.Pattern.Util (isConcrete, sortOfTerm) import Booster.Util (Flag (..)) import Control.DeepSeq (NFData) @@ -43,20 +44,20 @@ data ComputeCeilSummary = ComputeCeilSummary deriving stock (Eq, Ord, Show, GHC.Generic) deriving anyclass (NFData) -instance Pretty ComputeCeilSummary where - pretty ComputeCeilSummary{rule, ceils} = +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSummary) where + pretty (PrettyWithModifiers ComputeCeilSummary{rule, ceils}) = Pretty.vsep $ [ "\n\n----------------------------\n" , pretty $ sourceRef rule - , pretty rule.lhs + , pretty' @mods rule.lhs , "=>" - , pretty rule.rhs + , pretty' @mods rule.rhs ] <> ( if null rule.requires then [] else [ "requires" - , Pretty.indent 2 . Pretty.vsep $ map pretty $ Set.toList rule.requires + , Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) $ Set.toList rule.requires ] ) <> [ Pretty.line @@ -69,7 +70,9 @@ instance Pretty ComputeCeilSummary where [ Pretty.line , "computed ceils:" , Pretty.indent 2 . Pretty.vsep $ - map (either pretty (\t -> "#Ceil(" Pretty.<+> pretty t Pretty.<+> ")")) (Set.toList ceils) + map + (either (pretty' @mods) (\t -> "#Ceil(" Pretty.<+> pretty' @mods t Pretty.<+> ")")) + (Set.toList ceils) ] computeCeilsDefinition :: @@ -209,7 +212,7 @@ mkInKeys inKeysSymbols k m = Nothing -> error $ "in_keys for key sort '" - <> show (pretty $ sortOfTerm k) + <> show (pretty $ PrettyWithModifiers @'[Decoded, Truncated] $ sortOfTerm k) <> "' and map sort '" - <> show (pretty $ sortOfTerm m) + <> show (pretty $ PrettyWithModifiers @'[Decoded, Truncated] $ sortOfTerm m) <> "' does not exist." diff --git a/booster/library/Booster/Definition/Util.hs b/booster/library/Booster/Definition/Util.hs index 643ca77f65..5cec9ded08 100644 --- a/booster/library/Booster/Definition/Util.hs +++ b/booster/library/Booster/Definition/Util.hs @@ -31,6 +31,7 @@ import Booster.Definition.Base import Booster.Definition.Ceil (ComputeCeilSummary (..)) import Booster.Pattern.Base import Booster.Pattern.Index (CellIndex (..), TermIndex (..)) +import Booster.Pattern.Pretty import Booster.Prettyprinter import Booster.Util @@ -92,7 +93,8 @@ prettySummary :: Bool -> Summary -> String prettySummary veryVerbose summary@Summary{computeCeilsSummary} = Pretty.renderString . layoutPrettyUnbounded $ Pretty.vcat $ - pretty summary : if veryVerbose then map pretty computeCeilsSummary else [] + pretty summary + : if veryVerbose then map (pretty' @['Decoded, 'Truncated] $) computeCeilsSummary else [] instance Pretty Summary where pretty summary = @@ -146,7 +148,8 @@ instance Pretty Summary where prettyCellIndex None = "None" prettyCeilRule :: RewriteRule r -> Doc a - prettyCeilRule RewriteRule{lhs, rhs} = "#Ceil(" <+> pretty lhs <+> ") =>" <+> pretty rhs + prettyCeilRule RewriteRule{lhs, rhs} = + "#Ceil(" <+> pretty' @['Decoded, 'Truncated] lhs <+> ") =>" <+> pretty' @['Decoded, 'Truncated] rhs sourceRefText :: HasSourceRef a => a -> Text sourceRefText = renderOneLineText . pretty . sourceRef diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 11ecf9fbdc..13f038eef3 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} {- | Module : Booster.JsonRpc @@ -26,9 +27,11 @@ import Crypto.Hash (SHA256 (..), hashWith) import Data.Bifunctor (second) import Data.Foldable import Data.List (singleton) +import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe) +import Data.Proxy qualified import Data.Sequence (Seq) import Data.Set qualified as Set import Data.Text (Text, pack) @@ -36,7 +39,7 @@ import Data.Text qualified as Text import Data.Text.Encoding qualified as Text import GHC.Records import Numeric.Natural -import Prettyprinter (pretty) +import Prettyprinter (comma, hsep, punctuate, (<+>)) import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs) import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId) @@ -49,6 +52,7 @@ import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable) import Booster.Pattern.Base qualified as Pattern import Booster.Pattern.Bool (pattern TrueBool) import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms) +import Booster.Pattern.Pretty import Booster.Pattern.Rewrite ( RewriteFailed (..), RewriteResult (..), @@ -97,222 +101,136 @@ respond :: LoggerMIO m => MVar ServerState -> Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res) -respond stateVar = - \case - RpcTypes.Execute req - | isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String) - | isJust req.movingAverageStepTimeout -> - pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String) - RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ do - start <- liftIO $ getTime Monotonic - -- internalise given constrained term - let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term - - case internalised of - Left patternError -> do - void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError - pure $ - Left $ - RpcError.backendError $ - RpcError.CouldNotVerifyPattern - [ patternErrorToRpcError patternError - ] - Right (pat, substitution, unsupported) -> do - unless (null unsupported) $ do - withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ - logMessage ("ignoring unsupported predicate parts" :: Text) - let cutPoints = fromMaybe [] req.cutPointRules - terminals = fromMaybe [] req.terminalRules - mbDepth = fmap RpcTypes.getNat req.maxDepth - doTracing = - Flag $ - any - (fromMaybe False) - [ req.logSuccessfulRewrites - , req.logFailedRewrites - , req.logFallbacks - ] - -- apply the given substitution before doing anything else - let substPat = - Pattern - { term = substituteInTerm substitution pat.term - , constraints = Set.map (substituteInPredicate substitution) pat.constraints - , ceilConditions = pat.ceilConditions - } - - solver <- traverse (SMT.initSolver def) mSMTOptions - result <- - performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat - whenJust solver SMT.finaliseSolver - stop <- liftIO $ getTime Monotonic - let duration = - if fromMaybe False req.logTiming - then - Just $ - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - else Nothing - pure $ execResponse duration req result substitution unsupported - RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do - -- block other request executions while modifying the server state - state <- liftIO $ takeMVar stateVar - let nameAsId = fromMaybe False nameAsId' - moduleHash = Text.pack $ ('m' :) . show . hashWith SHA256 $ Text.encodeUtf8 _module - restoreStateAndRethrow err = do - liftIO (putMVar stateVar state) - throwE $ RpcError.backendError err - listNames :: (HasField "name" a b, HasField "getId" b Text) => [a] -> Text - listNames = Text.intercalate ", " . map (.name.getId) - - flip catchE restoreStateAndRethrow $ do - newModule <- - withExceptT (RpcError.InvalidModule . RpcError.ErrorOnly . pack) $ - except $ - parseKoreModule "rpc-request" _module - - unless (null newModule.sorts) $ - throwE $ - RpcError.InvalidModule . RpcError.ErrorOnly $ - "Module introduces new sorts: " <> listNames newModule.sorts - - unless (null newModule.symbols) $ - throwE $ - RpcError.InvalidModule . RpcError.ErrorOnly $ - "Module introduces new symbols: " <> listNames newModule.symbols - - -- check if we already received a module with this name - when nameAsId $ - case Map.lookup (getId newModule.name) state.addedModules of - -- if a different module was already added, throw error - Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName $ getId newModule.name - _ -> pure () +respond stateVar request = + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Data.Proxy.Proxy mods) -> case request of + RpcTypes.Execute req + | isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String) + | isJust req.movingAverageStepTimeout -> + pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String) + RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ do + start <- liftIO $ getTime Monotonic + -- internalise given constrained term + let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term - -- Check for a corner case when we send module M1 with the name "m"" and name-as-id: true - -- followed by adding M2. Should not happen in practice... - case Map.lookup moduleHash state.addedModules of - Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName moduleHash - _ -> pure () - - newDefinitions <- - withExceptT (RpcError.InvalidModule . definitionErrorToRpcError) $ - except $ - runExcept $ - addToDefinitions newModule{ParsedModule.name = Id moduleHash} state.definitions - - liftIO $ - putMVar - stateVar - state - { definitions = - if nameAsId - then Map.insert (getId newModule.name) (newDefinitions Map.! moduleHash) newDefinitions - else newDefinitions - , addedModules = - (if nameAsId then Map.insert (getId newModule.name) _module else id) $ - Map.insert moduleHash _module state.addedModules - } - Booster.Log.logMessage $ - "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions) - pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash - RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do - start <- liftIO $ getTime Monotonic - let internalised = - runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term - let mkTraces duration - | Just True <- req.logTiming = - Just [ProcessingTime (Just Booster) duration] - | otherwise = - Nothing - - solver <- traverse (SMT.initSolver def) mSMTOptions - - result <- case internalised of - Left patternErrors -> do - forM_ patternErrors $ \patternError -> + case internalised of + Left patternError -> do void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError - pure $ - Left $ - RpcError.backendError $ - RpcError.CouldNotVerifyPattern $ - map patternErrorToRpcError patternErrors - -- term and predicate (pattern) - Right (TermAndPredicates pat substitution unsupported) -> do - unless (null unsupported) $ do - withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do - logMessage ("ignoring unsupported predicate parts" :: Text) - -- apply the given substitution before doing anything else - let substPat = - Pattern - { term = substituteInTerm substitution pat.term - , constraints = Set.map (substituteInPredicate substitution) pat.constraints - , ceilConditions = pat.ceilConditions - } - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case - (Right newPattern, _) -> do - let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution - tSort = externaliseSort (sortOfPattern newPattern) - result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of - [] -> term - ps -> KoreJson.KJAnd tSort $ term : ps - pure $ Right (addHeader result) - (Left ApplyEquations.SideConditionFalse{}, _) -> do - let tSort = externaliseSort $ sortOfPattern pat - pure $ Right (addHeader $ KoreJson.KJBottom tSort) - (Left (ApplyEquations.EquationLoop _terms), _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" - (Left other, _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) - -- predicate only - Right (Predicates ps) - | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported -> pure $ - Right - (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term)) - | otherwise -> do - unless (null ps.unsupported) $ do - withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern + [ patternErrorToRpcError patternError + ] + Right (pat, substitution, unsupported) -> do + unless (null unsupported) $ do + withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ logMessage ("ignoring unsupported predicate parts" :: Text) + let cutPoints = fromMaybe [] req.cutPointRules + terminals = fromMaybe [] req.terminalRules + mbDepth = fmap RpcTypes.getNat req.maxDepth + doTracing = + Flag $ + any + (fromMaybe False) + [ req.logSuccessfulRewrites + , req.logFailedRewrites + , req.logFallbacks + ] -- apply the given substitution before doing anything else - let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates - withContext CtxConstraint $ - ApplyEquations.simplifyConstraints - def - mLlvmLibrary - solver - mempty - predicates - >>= \case - (Right newPreds, _) -> do - let predicateSort = - fromMaybe (error "not a predicate") $ - sortOfJson req.state.term - result = - map (externalisePredicate predicateSort) newPreds - <> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates) - <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution) - <> ps.unsupported - - pure $ Right (addHeader $ Syntax.KJAnd predicateSort result) - (Left something, _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something - whenJust solver SMT.finaliseSolver - stop <- liftIO $ getTime Monotonic - - let duration = - fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 - mkSimplifyResponse state = - RpcTypes.Simplify - RpcTypes.SimplifyResult{state, logs = mkTraces duration} - pure $ second mkSimplifyResponse result - RpcTypes.GetModel req -> withModule req._module $ \case - (_, _, Nothing) -> do - withContext CtxGetModel $ - logMessage' ("get-model request, not supported without SMT solver" :: Text) - pure $ Left RpcError.notImplemented - (def, _, Just smtOptions) -> do + let substPat = + Pattern + { term = substituteInTerm substitution pat.term + , constraints = Set.map (substituteInPredicate substitution) pat.constraints + , ceilConditions = pat.ceilConditions + } + + solver <- traverse (SMT.initSolver def) mSMTOptions + result <- + performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat + whenJust solver SMT.finaliseSolver + stop <- liftIO $ getTime Monotonic + let duration = + if fromMaybe False req.logTiming + then + Just $ + fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 + else Nothing + pure $ execResponse duration req result substitution unsupported + RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do + -- block other request executions while modifying the server state + state <- liftIO $ takeMVar stateVar + let nameAsId = fromMaybe False nameAsId' + moduleHash = Text.pack $ ('m' :) . show . hashWith SHA256 $ Text.encodeUtf8 _module + restoreStateAndRethrow err = do + liftIO (putMVar stateVar state) + throwE $ RpcError.backendError err + listNames :: (HasField "name" a b, HasField "getId" b Text) => [a] -> Text + listNames = Text.intercalate ", " . map (.name.getId) + + flip catchE restoreStateAndRethrow $ do + newModule <- + withExceptT (RpcError.InvalidModule . RpcError.ErrorOnly . pack) $ + except $ + parseKoreModule "rpc-request" _module + + unless (null newModule.sorts) $ + throwE $ + RpcError.InvalidModule . RpcError.ErrorOnly $ + "Module introduces new sorts: " <> listNames newModule.sorts + + unless (null newModule.symbols) $ + throwE $ + RpcError.InvalidModule . RpcError.ErrorOnly $ + "Module introduces new symbols: " <> listNames newModule.symbols + + -- check if we already received a module with this name + when nameAsId $ + case Map.lookup (getId newModule.name) state.addedModules of + -- if a different module was already added, throw error + Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName $ getId newModule.name + _ -> pure () + + -- Check for a corner case when we send module M1 with the name "m"" and name-as-id: true + -- followed by adding M2. Should not happen in practice... + case Map.lookup moduleHash state.addedModules of + Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName moduleHash + _ -> pure () + + newDefinitions <- + withExceptT (RpcError.InvalidModule . definitionErrorToRpcError) $ + except $ + runExcept $ + addToDefinitions newModule{ParsedModule.name = Id moduleHash} state.definitions + + liftIO $ + putMVar + stateVar + state + { definitions = + if nameAsId + then Map.insert (getId newModule.name) (newDefinitions Map.! moduleHash) newDefinitions + else newDefinitions + , addedModules = + (if nameAsId then Map.insert (getId newModule.name) _module else id) $ + Map.insert moduleHash _module state.addedModules + } + Booster.Log.logMessage $ + "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions) + pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash + RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do + start <- liftIO $ getTime Monotonic let internalised = - runExcept $ - internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term - case internalised of + runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term + let mkTraces duration + | Just True <- req.logTiming = + Just [ProcessingTime (Just Booster) duration] + | otherwise = + Nothing + + solver <- traverse (SMT.initSolver def) mSMTOptions + + result <- case internalised of Left patternErrors -> do forM_ patternErrors $ \patternError -> void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError @@ -321,175 +239,267 @@ respond stateVar = RpcError.backendError $ RpcError.CouldNotVerifyPattern $ map patternErrorToRpcError patternErrors - -- various predicates obtained - Right things -> do - -- term and predicates were sent. Only work on predicates - (boolPs, suppliedSubst) <- - case things of - TermAndPredicates pat substitution unsupported -> do - withContext CtxGetModel $ - logMessage' ("ignoring supplied terms and only checking predicates" :: Text) - - unless (null unsupported) $ do - withContext CtxGetModel $ do - logMessage' ("ignoring unsupported predicates" :: Text) - withContext CtxDetail $ - logMessage (Text.unwords $ map prettyPattern unsupported) - pure (Set.toList pat.constraints, substitution) - Predicates ps -> do - unless (null ps.ceilPredicates && null ps.unsupported) $ do - withContext CtxGetModel $ do - logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text) - withContext CtxDetail $ - logMessage - ( Text.unlines $ - map - (renderText . ("#Ceil:" <>) . pretty) - (Set.toList ps.ceilPredicates) - <> map prettyPattern ps.unsupported - ) - pure (Set.toList ps.boolPredicates, ps.substitution) - - smtResult <- - if null boolPs && Map.null suppliedSubst - then do - -- as per spec, no predicate, no answer - withContext CtxGetModel $ - withContext CtxSMT $ - logMessage ("No predicates or substitutions given, returning Unknown" :: Text) - pure $ Left SMT.Unknown - else do - solver <- SMT.initSolver def smtOptions - result <- SMT.getModelFor solver boolPs suppliedSubst - SMT.finaliseSolver solver - case result of - Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors - Right response -> pure response - withContext CtxGetModel $ - withContext CtxSMT $ - logMessage $ - "SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult) - pure . Right . RpcTypes.GetModel $ case smtResult of - Left SMT.Unsat -> - RpcTypes.GetModelResult - { satisfiable = RpcTypes.Unsat - , substitution = Nothing - } - Left SMT.ReasonUnknown{} -> - RpcTypes.GetModelResult - { satisfiable = RpcTypes.Unknown - , substitution = Nothing - } - Left SMT.Unknown -> - RpcTypes.GetModelResult - { satisfiable = RpcTypes.Unknown - , substitution = Nothing + -- term and predicate (pattern) + Right (TermAndPredicates pat substitution unsupported) -> do + unless (null unsupported) $ do + withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do + logMessage ("ignoring unsupported predicate parts" :: Text) + -- apply the given substitution before doing anything else + let substPat = + Pattern + { term = substituteInTerm substitution pat.term + , constraints = Set.map (substituteInPredicate substitution) pat.constraints + , ceilConditions = pat.ceilConditions } - Left other -> - error $ "Unexpected result " <> show other <> " from getModelFor" - Right subst -> - let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term - substitution - | Map.null subst = Nothing - | [(var, term)] <- Map.assocs subst = - Just . addHeader $ - KoreJson.KJEquals - (externaliseSort var.variableSort) - sort - (externaliseTerm $ Pattern.Var var) - (externaliseTerm term) - | otherwise = - Just . addHeader $ - KoreJson.KJAnd - sort - [ KoreJson.KJEquals + ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case + (Right newPattern, _) -> do + let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution + tSort = externaliseSort (sortOfPattern newPattern) + result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of + [] -> term + ps -> KoreJson.KJAnd tSort $ term : ps + pure $ Right (addHeader result) + (Left ApplyEquations.SideConditionFalse{}, _) -> do + let tSort = externaliseSort $ sortOfPattern pat + pure $ Right (addHeader $ KoreJson.KJBottom tSort) + (Left (ApplyEquations.EquationLoop _terms), _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" + (Left other, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + -- predicate only + Right (Predicates ps) + | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported -> + pure $ + Right + (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term)) + | otherwise -> do + unless (null ps.unsupported) $ do + withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do + logMessage ("ignoring unsupported predicate parts" :: Text) + -- apply the given substitution before doing anything else + let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates + withContext CtxConstraint $ + ApplyEquations.simplifyConstraints + def + mLlvmLibrary + solver + mempty + predicates + >>= \case + (Right newPreds, _) -> do + let predicateSort = + fromMaybe (error "not a predicate") $ + sortOfJson req.state.term + result = + map (externalisePredicate predicateSort) newPreds + <> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates) + <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution) + <> ps.unsupported + + pure $ Right (addHeader $ Syntax.KJAnd predicateSort result) + (Left something, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something + whenJust solver SMT.finaliseSolver + stop <- liftIO $ getTime Monotonic + + let duration = + fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 + mkSimplifyResponse state = + RpcTypes.Simplify + RpcTypes.SimplifyResult{state, logs = mkTraces duration} + pure $ second mkSimplifyResponse result + RpcTypes.GetModel req -> withModule req._module $ \case + (_, _, Nothing) -> do + withContext CtxGetModel $ + logMessage' ("get-model request, not supported without SMT solver" :: Text) + pure $ Left RpcError.notImplemented + (def, _, Just smtOptions) -> do + let internalised = + runExcept $ + internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term + case internalised of + Left patternErrors -> do + forM_ patternErrors $ \patternError -> + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern $ + map patternErrorToRpcError patternErrors + -- various predicates obtained + Right things -> do + -- term and predicates were sent. Only work on predicates + (boolPs, suppliedSubst) <- + case things of + TermAndPredicates pat substitution unsupported -> do + withContext CtxGetModel $ + logMessage' ("ignoring supplied terms and only checking predicates" :: Text) + + unless (null unsupported) $ do + withContext CtxGetModel $ do + logMessage' ("ignoring unsupported predicates" :: Text) + withContext CtxDetail $ + logMessage (Text.unwords $ map prettyPattern unsupported) + pure (Set.toList pat.constraints, substitution) + Predicates ps -> do + unless (null ps.ceilPredicates && null ps.unsupported) $ do + withContext CtxGetModel $ do + logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text) + withContext CtxDetail $ + logMessage + ( Text.unlines $ + map + (renderText . ("#Ceil:" <>) . pretty' @mods) + (Set.toList ps.ceilPredicates) + <> map prettyPattern ps.unsupported + ) + pure (Set.toList ps.boolPredicates, ps.substitution) + + smtResult <- + if null boolPs && Map.null suppliedSubst + then do + -- as per spec, no predicate, no answer + withContext CtxGetModel $ + withContext CtxSMT $ + logMessage ("No predicates or substitutions given, returning Unknown" :: Text) + pure $ Left SMT.Unknown + else do + solver <- SMT.initSolver def smtOptions + result <- SMT.getModelFor solver boolPs suppliedSubst + SMT.finaliseSolver solver + case result of + Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors + Right response -> pure response + withContext CtxGetModel $ + withContext CtxSMT $ + logMessage $ + "SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult) + pure . Right . RpcTypes.GetModel $ case smtResult of + Left SMT.Unsat -> + RpcTypes.GetModelResult + { satisfiable = RpcTypes.Unsat + , substitution = Nothing + } + Left SMT.ReasonUnknown{} -> + RpcTypes.GetModelResult + { satisfiable = RpcTypes.Unknown + , substitution = Nothing + } + Left SMT.Unknown -> + RpcTypes.GetModelResult + { satisfiable = RpcTypes.Unknown + , substitution = Nothing + } + Left other -> + error $ "Unexpected result " <> show other <> " from getModelFor" + Right subst -> + let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term + substitution + | Map.null subst = Nothing + | [(var, term)] <- Map.assocs subst = + Just . addHeader $ + KoreJson.KJEquals (externaliseSort var.variableSort) sort (externaliseTerm $ Pattern.Var var) (externaliseTerm term) - | (var, term) <- Map.assocs subst - ] - in RpcTypes.GetModelResult - { satisfiable = RpcTypes.Sat - , substitution - } - RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do - -- internalise given constrained term - let internalised = - runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials - - case (internalised req.antecedent.term, internalised req.consequent.term) of - (Left patternError, _) -> do - void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError - pure $ - Left $ - RpcError.backendError $ - RpcError.CouldNotVerifyPattern - [ patternErrorToRpcError patternError - ] - (_, Left patternError) -> do - void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError - pure $ - Left $ - RpcError.backendError $ - RpcError.CouldNotVerifyPattern - [ patternErrorToRpcError patternError - ] - (Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do - unless (null unsupportedL && null unsupportedR) $ do - logMessage' - ("aborting due to unsupported predicate parts" :: Text) - unless (null unsupportedL) $ - withContext CtxDetail $ - logMessage - (Text.unwords $ map prettyPattern unsupportedL) - unless (null unsupportedR) $ - withContext CtxDetail $ - logMessage - (Text.unwords $ map prettyPattern unsupportedR) - let - -- apply the given substitution before doing anything else - substPatL = - Pattern - { term = substituteInTerm substitutionL patL.term - , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints - , ceilConditions = patL.ceilConditions - } - substPatR = - Pattern - { term = substituteInTerm substitutionR patR.term - , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints - , ceilConditions = patR.ceilConditions - } + | otherwise = + Just . addHeader $ + KoreJson.KJAnd + sort + [ KoreJson.KJEquals + (externaliseSort var.variableSort) + sort + (externaliseTerm $ Pattern.Var var) + (externaliseTerm term) + | (var, term) <- Map.assocs subst + ] + in RpcTypes.GetModelResult + { satisfiable = RpcTypes.Sat + , substitution + } + RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do + -- internalise given constrained term + let internalised = + runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials + + case (internalised req.antecedent.term, internalised req.consequent.term) of + (Left patternError, _) -> do + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern + [ patternErrorToRpcError patternError + ] + (_, Left patternError) -> do + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError + pure $ + Left $ + RpcError.backendError $ + RpcError.CouldNotVerifyPattern + [ patternErrorToRpcError patternError + ] + (Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do + unless (null unsupportedL && null unsupportedR) $ do + logMessage' + ("aborting due to unsupported predicate parts" :: Text) + unless (null unsupportedL) $ + withContext CtxDetail $ + logMessage + (Text.unwords $ map prettyPattern unsupportedL) + unless (null unsupportedR) $ + withContext CtxDetail $ + logMessage + (Text.unwords $ map prettyPattern unsupportedR) + let + -- apply the given substitution before doing anything else + substPatL = + Pattern + { term = substituteInTerm substitutionL patL.term + , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints + , ceilConditions = patL.ceilConditions + } + substPatR = + Pattern + { term = substituteInTerm substitutionR patR.term + , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints + , ceilConditions = patR.ceilConditions + } - case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of - MatchFailed (SubsortingError sortError) -> - pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ - show sortError - MatchFailed{} -> - doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term - MatchIndeterminate remainder -> - pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ - "match remainder: " - <> renderDefault (pretty remainder) - MatchSuccess subst -> do - let filteredConsequentPreds = - Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints - solver <- traverse (SMT.initSolver def) mSMTOptions - - if null filteredConsequentPreds - then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst - else - ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case - (Right newPreds, _) -> - if all (== Pattern.Predicate TrueBool) newPreds - then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst - else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains" - (Left other, _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) - - -- this case is only reachable if the cancel appeared as part of a batch request - RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode + case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of + MatchFailed (SubsortingError sortError) -> + pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ + show sortError + MatchFailed{} -> + doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term + MatchIndeterminate remainder -> + pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ + "match remainder: " + <> renderDefault + ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NonEmpty.toList remainder + ) + MatchSuccess subst -> do + let filteredConsequentPreds = + Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints + solver <- traverse (SMT.initSolver def) mSMTOptions + + if null filteredConsequentPreds + then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst + else + ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case + (Right newPreds, _) -> + if all (== Pattern.Predicate TrueBool) newPreds + then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst + else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains" + (Left other, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + + -- this case is only reachable if the cancel appeared as part of a batch request + RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode where withModule :: Maybe Text -> diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs index 1be9b76f7f..16dc8bb660 100644 --- a/booster/library/Booster/JsonRpc/Utils.hs +++ b/booster/library/Booster/JsonRpc/Utils.hs @@ -33,6 +33,7 @@ import System.IO.Unsafe (unsafePerformIO) import System.Process (readProcessWithExitCode) import Booster.Definition.Base qualified as Internal +import Booster.Pattern.Pretty import Booster.Prettyprinter import Booster.Syntax.Json.Internalise import Data.Binary.Builder (fromLazyByteString, toLazyByteString) @@ -246,11 +247,24 @@ diffBy def pat1 pat2 = ( BS.pack . renderDefault . Pretty.vsep $ concat [ "Conditions:" - : fmap (Pretty.indent 4 . pretty) (Set.toList ps.boolPredicates) + : fmap + (Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated]) + (Set.toList ps.boolPredicates) , "Ceil conditions:" - : map (Pretty.indent 4 . pretty) (Set.toList ps.ceilPredicates) + : map + (Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated]) + (Set.toList ps.ceilPredicates) , "Substitutions:" - : fmap (Pretty.indent 4) (map (\(k, v) -> pretty k <+> "=" <+> pretty v) (Map.toList ps.substitution)) + : fmap + (Pretty.indent 4) + ( map + ( \(k, v) -> + pretty (PrettyWithModifiers @['Decoded, 'Truncated] k) + <+> "=" + <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v) + ) + (Map.toList ps.substitution) + ) ] ) <> if null ps.unsupported @@ -258,7 +272,16 @@ diffBy def pat1 pat2 = else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported) renderBS (TermAndPredicates p m u) = ( BS.pack . renderDefault $ - pretty p <+> vsep (map (\(k, v) -> pretty k <+> "=" <+> pretty v) (Map.toList m)) + pretty (PrettyWithModifiers @['Decoded, 'Truncated] p) + <+> vsep + ( map + ( \(k, v) -> + pretty (PrettyWithModifiers @['Decoded, 'Truncated] k) + <+> "=" + <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v) + ) + (Map.toList m) + ) ) <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u) internalise = diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index 45443af0e4..5e862f8345 100644 --- a/booster/library/Booster/Log.hs +++ b/booster/library/Booster/Log.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} @@ -15,6 +16,7 @@ module Booster.Log ( logMessage, logMessage', logPretty, + logPretty', filterLogger, jsonLogger, textLogger, @@ -29,6 +31,7 @@ module Booster.Log ( SimpleContext (..), ) where +import Control.Arrow (first) import Control.Monad (when) import Control.Monad.IO.Class import Control.Monad.Logger qualified @@ -42,6 +45,7 @@ import Data.Aeson (ToJSON (..), Value (..), (.=)) import Data.Aeson.Encode.Pretty (Config (confIndent), Indent (Spaces), encodePretty') import Data.Aeson.Types (object) import Data.Coerce (coerce) +import Data.Data (Proxy (..)) import Data.Hashable qualified import Data.List (foldl', intercalate, intersperse) import Data.List.Extra (splitOn, takeEnd) @@ -64,6 +68,7 @@ import Booster.Pattern.Base ( TermAttributes (hash), pattern AndTerm, ) +import Booster.Pattern.Pretty import Booster.Prettyprinter (renderOneLineText) import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern) import Booster.Syntax.Json.Externalise (externaliseTerm) @@ -90,9 +95,9 @@ instance ToLogFormat String where toTextualLog = pack toJSONLog = String . pack -instance ToLogFormat Term where +instance ToLogFormat (PrettyWithModifiers mods Term) where toTextualLog t = renderOneLineText $ pretty t - toJSONLog t = toJSON $ addHeader $ externaliseTerm t + toJSONLog (PrettyWithModifiers t) = toJSON $ addHeader $ externaliseTerm t instance ToLogFormat (RewriteRule tag) where toTextualLog = shortRuleLocation @@ -114,6 +119,10 @@ class MonadIO m => LoggerMIO m where default getLogger :: (Trans.MonadTrans t, LoggerMIO n, m ~ t n) => m (Logger LogMessage) getLogger = Trans.lift getLogger + getPrettyModifiers :: m ModifiersRep + default getPrettyModifiers :: (Trans.MonadTrans t, LoggerMIO n, m ~ t n) => m ModifiersRep + getPrettyModifiers = Trans.lift getPrettyModifiers + withLogger :: (Logger LogMessage -> Logger LogMessage) -> m a -> m a instance LoggerMIO m => LoggerMIO (MaybeT m) where @@ -129,6 +138,7 @@ instance LoggerMIO m => LoggerMIO (Strict.StateT s m) where instance MonadIO m => LoggerMIO (Control.Monad.Logger.NoLoggingT m) where getLogger = pure $ Logger $ \_ -> pure () + getPrettyModifiers = pure $ ModifiersRep @'[Decoded, Truncated] Proxy withLogger _ = id logMessage :: (LoggerMIO m, ToLogFormat a) => a -> m () @@ -145,12 +155,19 @@ logMessage' a = logPretty :: (LoggerMIO m, Pretty a) => a -> m () logPretty = logMessage . renderOneLineText . pretty +logPretty' :: + forall mods m a. + (LoggerMIO m, Pretty (PrettyWithModifiers mods a), FromModifiersT mods) => + a -> + m () +logPretty' = logMessage . renderOneLineText . pretty' @mods + withContext :: LoggerMIO m => SimpleContext -> m a -> m a withContext c = withContext_ (CLNullary c) withContexts :: LoggerMIO m => [SimpleContext] -> m a -> m a withContexts [] m = m -withContexts cs m = foldr withContext m cs +withContexts cs m = foldr (withContext) m cs withContext_ :: LoggerMIO m => CLContext -> m a -> m a withContext_ c = @@ -161,7 +178,10 @@ withContext_ c = withTermContext :: LoggerMIO m => Term -> m a -> m a withTermContext t@(Term attrs _) m = withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash) $ do - withContext CtxKoreTerm $ logMessage t + withContext CtxKoreTerm $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage (PrettyWithModifiers @mods t) m withPatternContext :: LoggerMIO m => Pattern -> m a -> m a @@ -224,7 +244,7 @@ instance ContextFor Symbol where withContextFor s = withContext_ (CLWithId . CtxHook $ maybe "not-hooked" decodeUtf8 s.attributes.hook) -instance ContextFor (JSONRPC.Id) where +instance ContextFor JSONRPC.Id where withContextFor r = withContext_ (CLWithId . CtxRequest $ pack $ JSONRPC.fromId r) @@ -238,7 +258,7 @@ instance ToLogFormat WithJsonMessage where toTextualLog (WithJsonMessage _ a) = toTextualLog a toJSONLog (WithJsonMessage v _) = v -newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a} +newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage, ModifiersRep) m a} deriving newtype ( Applicative , Functor @@ -250,8 +270,9 @@ newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a} ) instance MonadIO m => LoggerMIO (LoggerT m) where - getLogger = LoggerT ask - withLogger modL (LoggerT m) = LoggerT $ withReaderT modL m + getLogger = LoggerT (fst <$> ask) + getPrettyModifiers = LoggerT (snd <$> ask) + withLogger modL (LoggerT m) = LoggerT $ withReaderT (first modL) m textLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage textLogger l = Logger $ \(LogMessage _ ctxts msg) -> diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 9a001d2196..f153111b63 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} {- | Copyright : (c) Runtime Verification, 2022 @@ -36,9 +37,10 @@ import Data.Aeson (object, (.=)) import Data.Bifunctor (bimap) import Data.ByteString.Char8 qualified as BS import Data.Coerce (coerce) -import Data.Data (Data) +import Data.Data (Data, Proxy) import Data.Foldable (toList, traverse_) import Data.List (intersperse, partition) +import Data.List.NonEmpty qualified as NonEmpty import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (catMaybes, fromMaybe) @@ -62,6 +64,7 @@ import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index qualified as Idx import Booster.Pattern.Match +import Booster.Pattern.Pretty import Booster.Pattern.Util import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT @@ -77,6 +80,7 @@ newtype EquationT io a instance MonadIO io => LoggerMIO (EquationT io) where getLogger = EquationT $ asks logger + getPrettyModifiers = EquationT $ asks prettyModifiers withLogger modL (EquationT m) = EquationT $ withReaderT (\cfg@EquationConfig{logger} -> cfg{logger = modL logger}) m throw :: Monad io => EquationFailure -> EquationT io a @@ -105,31 +109,31 @@ data EquationFailure | UndefinedTerm Term LLVM.LlvmError deriving stock (Eq, Show, Data) -instance Pretty EquationFailure where - pretty = \case +instance Pretty (PrettyWithModifiers mods EquationFailure) where + pretty (PrettyWithModifiers f) = case f of IndexIsNone t -> - "Index 'None' for term " <> pretty t + "Index 'None' for term " <> pretty' @mods t TooManyIterations count start end -> vsep [ "Unable to finish evaluation in " <> pretty count <> " iterations" - , "Started with: " <> pretty start - , "Stopped at: " <> pretty end + , "Started with: " <> pretty' @mods start + , "Stopped at: " <> pretty' @mods end ] EquationLoop ts -> - vsep $ "Evaluation produced a loop:" : map pretty ts + vsep $ "Evaluation produced a loop:" : map (pretty' @mods) ts TooManyRecursions ts -> vsep $ "Recursion limit exceeded. The following terms were evaluated:" - : map pretty ts + : map (pretty' @mods) ts SideConditionFalse p -> vsep [ "A side condition was found to be false during evaluation (pruning)" - , pretty p + , pretty' @mods p ] UndefinedTerm t (LLVM.LlvmError err) -> vsep [ "Term" - , pretty t + , pretty' @mods t , "is undefined: " , pretty (BS.unpack err) ] @@ -143,6 +147,7 @@ data EquationConfig = EquationConfig , maxRecursion :: Bound "Recursion" , maxIterations :: Bound "Iterations" , logger :: Logger LogMessage + , prettyModifiers :: ModifiersRep } data EquationState = EquationState @@ -282,6 +287,7 @@ runEquationT :: runEquationT definition llvmApi smtSolver sCache (EquationT m) = do globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions logger <- getLogger + prettyModifiers <- getPrettyModifiers (res, endState) <- flip runStateT (startState sCache) $ runExceptT $ @@ -294,6 +300,7 @@ runEquationT definition llvmApi smtSolver sCache (EquationT m) = do , maxIterations = globalEquationOptions.maxIterations , maxRecursion = globalEquationOptions.maxRecursion , logger + , prettyModifiers } pure (res, endState.cache) @@ -326,8 +333,11 @@ iterateEquations direction preference startTerm = do logWarn $ renderOneLineText $ "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations." - withContext CtxDetail . logMessage . renderOneLineText $ - "Final term:" <+> pretty currentTerm + withContext CtxDetail $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage . renderOneLineText $ + "Final term:" <+> pretty' @mods currentTerm throw $ TooManyIterations currentCount startTerm currentTerm pushTerm currentTerm @@ -709,125 +719,141 @@ applyEquation :: EquationT io (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term) -applyEquation term rule = runExceptT $ do - -- ensured by internalisation: no existentials in equations - unless (null rule.existentials) $ do - withContext CtxAbort $ - logMessage ("Equation with existentials" :: Text) - lift . throw . InternalError $ - "Equation with existentials: " <> Text.pack (show rule) - -- immediately cancel if not preserving definedness - unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do - throwE - ( \ctxt -> - ctxt $ - logMessage $ - renderOneLineText $ - "Uncertain about definedness of rule due to:" - <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) - , RuleNotPreservingDefinedness - ) - -- immediately cancel if rule has concrete() flag and term has variables - when (allMustBeConcrete rule.attributes.concreteness && not (Set.null (freeVariables term))) $ do - throwE - ( \ctxt -> ctxt $ logMessage ("Concreteness constraint violated: term has variables" :: Text) - , MatchConstraintViolated Concrete "* (term has variables)" - ) - -- match lhs - koreDef <- (.definition) <$> lift getConfig - case matchTerms Eval koreDef rule.lhs term of - MatchFailed failReason -> - throwE - ( \ctxt -> - withContext CtxMatch $ - ctxt $ - logPretty failReason - , FailedMatch failReason - ) - MatchIndeterminate remainder -> - throwE - ( \ctxt -> - withContext CtxMatch $ - ctxt $ - logMessage $ - WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ +applyEquation term rule = + runExceptT $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do + -- ensured by internalisation: no existentials in equations + unless (null rule.existentials) $ do + withContext CtxAbort $ + logMessage ("Equation with existentials" :: Text) + lift . throw . InternalError $ + "Equation with existentials: " <> Text.pack (show rule) + -- immediately cancel if not preserving definedness + unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do + throwE + ( \ctxt -> + ctxt $ + logMessage $ renderOneLineText $ - "Uncertain about match with rule. Remainder:" <+> pretty remainder - , IndeterminateMatch - ) - MatchSuccess subst -> do - -- cancel if condition - -- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\ - -- symbolic(v) -> not $ t isConstructorLike(t) - -- is violated - withContext CtxMatch $ checkConcreteness rule.attributes.concreteness subst - - withContext CtxMatch $ withContext CtxSuccess $ do - logMessage rule - withContext CtxSubstitution - $ logMessage - $ WithJsonMessage - (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList subst)]) - $ renderOneLineText - $ "Substitution:" - <+> (hsep $ intersperse "," $ map (\(k, v) -> pretty k <+> "->" <+> pretty v) $ Map.toList subst) - - -- instantiate the requires clause with the obtained substitution - let required = - concatMap - (splitBoolPredicates . coerce . substituteInTerm subst . coerce) - rule.requires - -- If the required condition is _syntactically_ present in - -- the prior (known constraints), we don't check it. - knownPredicates <- (.predicates) <$> lift getState - toCheck <- lift $ filterOutKnownConstraints knownPredicates required - - -- check the filtered requires clause conditions - unclearConditions <- - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) + "Uncertain about definedness of rule due to:" + <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) + , RuleNotPreservingDefinedness ) - toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions - - -- abort if any of the conditions is still unclear at that point - unless (null stillUnclear) $ - throwE - ( \ctxt -> - ctxt $ - logMessage $ - renderOneLineText $ - "Uncertain about a condition(s) in rule:" <+> hsep (intersperse "," $ map pretty unclearConditions) - , IndeterminateCondition unclearConditions - ) - - -- check ensured conditions, filter any - -- true ones, prune if any is false - let ensured = - concatMap - (splitBoolPredicates . substituteInPredicate subst) - (Set.toList rule.ensures) - ensuredConditions <- - -- throws if an ensured condition found to be false - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) + -- immediately cancel if rule has concrete() flag and term has variables + when (allMustBeConcrete rule.attributes.concreteness && not (Set.null (freeVariables term))) $ do + throwE + ( \ctxt -> ctxt $ logMessage ("Concreteness constraint violated: term has variables" :: Text) + , MatchConstraintViolated Concrete "* (term has variables)" ) - ensured - lift $ pushConstraints $ Set.fromList ensuredConditions - pure $ substituteInTerm subst rule.rhs + -- match lhs + koreDef <- (.definition) <$> lift getConfig + case matchTerms Eval koreDef rule.lhs term of + MatchFailed failReason -> + throwE + ( \ctxt -> + withContext CtxMatch $ + ctxt $ + logPretty' @mods failReason + , FailedMatch failReason + ) + MatchIndeterminate remainder -> + throwE + ( \ctxt -> + withContext CtxMatch $ + ctxt $ + logMessage $ + WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ + renderOneLineText $ + "Uncertain about match with rule. Remainder:" + <+> ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NonEmpty.toList remainder + ) + , IndeterminateMatch + ) + MatchSuccess subst -> do + -- cancel if condition + -- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\ + -- symbolic(v) -> not $ t isConstructorLike(t) + -- is violated + withContext CtxMatch $ checkConcreteness rule.attributes.concreteness subst + + withContext CtxMatch $ withContext CtxSuccess $ do + logMessage rule + withContext CtxSubstitution + $ logMessage + $ WithJsonMessage + (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList subst)]) + $ renderOneLineText + $ "Substitution:" + <+> ( hsep $ + intersperse "," $ + map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ + Map.toList subst + ) + + -- instantiate the requires clause with the obtained substitution + let required = + concatMap + (splitBoolPredicates . coerce . substituteInTerm subst . coerce) + rule.requires + -- If the required condition is _syntactically_ present in + -- the prior (known constraints), we don't check it. + knownPredicates <- (.predicates) <$> lift getState + toCheck <- lift $ filterOutKnownConstraints knownPredicates required + + -- check the filtered requires clause conditions + unclearConditions <- + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) + ) + toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions + + -- abort if any of the conditions is still unclear at that point + unless (null stillUnclear) $ + throwE + ( \ctxt -> + ctxt $ + logMessage $ + renderOneLineText $ + "Uncertain about a condition(s) in rule:" + <+> hsep (intersperse "," $ map (pretty' @mods) unclearConditions) + , IndeterminateCondition unclearConditions + ) + + -- check ensured conditions, filter any + -- true ones, prune if any is false + let ensured = + concatMap + (splitBoolPredicates . substituteInPredicate subst) + (Set.toList rule.ensures) + ensuredConditions <- + -- throws if an ensured condition found to be false + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) + ) + ensured + lift $ pushConstraints $ Set.fromList ensuredConditions + pure $ substituteInTerm subst rule.rhs where filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate] filterOutKnownConstraints priorKnowledge constraitns = do let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns unless (null knownTrue) $ - logMessage $ - renderOneLineText $ - "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue) + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage $ + renderOneLineText $ + "Known true side conditions (won't check):" + <+> hsep (intersperse "," $ map (pretty' @mods) knownTrue) pure toCheck -- Simplify given predicate in a nested EquationT execution. diff --git a/booster/library/Booster/Pattern/Base.hs b/booster/library/Booster/Pattern/Base.hs index 2873fbc5fe..a2b4661614 100644 --- a/booster/library/Booster/Pattern/Base.hs +++ b/booster/library/Booster/Pattern/Base.hs @@ -27,13 +27,10 @@ import Booster.Definition.Attributes.Base ( pattern IsNotIdem, pattern IsNotMacroOrAlias, ) -import Booster.Prettyprinter qualified as KPretty -import Booster.Util (decodeLabel') import Control.DeepSeq (NFData (..)) import Data.Bifunctor (second) import Data.ByteString.Char8 (ByteString) -import Data.ByteString.Char8 qualified as BS import Data.Data (Data) import Data.Functor.Foldable import Data.Hashable (Hashable) @@ -41,12 +38,8 @@ import Data.Hashable qualified as Hashable import Data.List as List (foldl', foldl1', sort) import Data.Set (Set) import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Text.Encoding qualified as Text import GHC.Generics (Generic) import Language.Haskell.TH.Syntax (Lift (..)) -import Prettyprinter (Pretty (..), (<+>)) -import Prettyprinter qualified as Pretty type VarName = ByteString type SymbolName = ByteString @@ -782,82 +775,6 @@ pattern Pattern_ t <- Pattern t _ _ where Pattern_ t = Pattern t mempty mempty --- used for printing the string as it appears (with codepoints) -prettyBS :: ByteString -> Pretty.Doc a -prettyBS = Pretty.pretty . Text.decodeUtf8 - -instance Pretty Term where - pretty = \case - AndTerm t1 t2 -> - pretty t1 <+> "/\\" <+> pretty t2 - SymbolApplication symbol _sortParams args -> - pretty (Text.replace "Lbl" "" $ Text.decodeUtf8 $ decodeLabel' symbol.name) - <> KPretty.argumentsP args - DotDotDot -> "..." - DomainValue _sort bs -> pretty . show . Text.decodeLatin1 . shortenBS $ bs - Var var -> pretty var - Injection _source _target t' -> pretty t' - KMap _attrs keyVals rest -> - Pretty.braces . Pretty.hsep . Pretty.punctuate Pretty.comma $ - [pretty k <+> "->" <+> pretty v | (k, v) <- keyVals] - ++ maybe [] ((: []) . pretty) rest - KList _meta heads (Just (mid, tails)) -> - Pretty.hsep $ - Pretty.punctuate - " +" - [renderList heads, pretty mid, renderList tails] - KList _meta [] Nothing -> - "[]" - KList _meta heads Nothing -> - renderList heads - KSet _meta [] Nothing -> "{}" - KSet _meta [] (Just rest) -> pretty rest - KSet _meta es rest -> - (Pretty.braces . Pretty.hsep . Pretty.punctuate Pretty.comma $ map pretty es) - Pretty.<+> maybe mempty ((" ++ " <>) . pretty) rest - where - renderList l - | null l = mempty - | otherwise = - Pretty.brackets . Pretty.hsep . Pretty.punctuate Pretty.comma $ - map pretty l - - -- shorten domain value ByteString to a readable length - shortenBS dv = - let cutoff = 16 - in if BS.length dv < cutoff then dv else BS.take cutoff dv <> "...truncated" - -instance Pretty Sort where - pretty (SortApp name params) = - prettyBS name <> KPretty.parametersP params - pretty (SortVar name) = - prettyBS name - -instance Pretty Variable where - pretty var = - prettyBS (decodeLabel' var.variableName) - <> Pretty.colon - <> pretty var.variableSort - -instance Pretty Predicate where - pretty (Predicate t) = pretty t - -instance Pretty Ceil where - pretty (Ceil t) = - "\\ceil" - <> KPretty.noParameters - <> KPretty.argumentsP [t] - -instance Pretty Pattern where - pretty patt = - Pretty.vsep $ - [ "Term:" - , Pretty.indent 4 $ pretty patt.term - , "Conditions:" - ] - <> fmap (Pretty.indent 4 . pretty) (Set.toList patt.constraints) - <> fmap (Pretty.indent 4 . pretty) patt.ceilConditions - pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term pattern ConsApplication sym sorts args <- Term diff --git a/booster/library/Booster/Pattern/Binary.hs b/booster/library/Booster/Pattern/Binary.hs index f865b2835b..c398e33878 100644 --- a/booster/library/Booster/Pattern/Binary.hs +++ b/booster/library/Booster/Pattern/Binary.hs @@ -39,6 +39,7 @@ import Booster.Definition.Attributes.Base import Booster.Definition.Base import Booster.Pattern.Base import Booster.Pattern.Bool (pattern TrueBool) +import Booster.Pattern.Pretty import Booster.Pattern.Util (sortOfTerm) import Booster.Prettyprinter (renderDefault) @@ -441,9 +442,9 @@ decodeBlock mbSize = do unless (sortOfTerm trm == srt) $ fail $ "Argument has incorrect sort. Expecting " - <> renderDefault (pretty srt) + <> renderDefault (pretty (PrettyWithModifiers @['Decoded, 'Truncated] srt)) <> " but got " - <> renderDefault (pretty $ sortOfTerm trm) + <> renderDefault (pretty (PrettyWithModifiers @['Decoded, 'Truncated] $ sortOfTerm trm)) pure argIdx _ -> fail "Expecting term" returnRegistered BTerm $ diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 243d7fadc9..2e7d3e43ee 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -35,6 +35,7 @@ import Prettyprinter import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition) import Booster.Definition.Base import Booster.Pattern.Base +import Booster.Pattern.Pretty import Booster.Pattern.Util ( checkSymbolIsAc, freeVariables, @@ -82,40 +83,40 @@ data FailReason SubjectVariableMatch Term Variable deriving stock (Eq, Show) -instance Pretty FailReason where - pretty = \case +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) where + pretty (PrettyWithModifiers f) = case f of DifferentValues t1 t2 -> - "Values differ:" <> align (sep [pretty t1, pretty t2]) + "Values differ:" <> align (sep [pretty' @mods t1, pretty' @mods t2]) DifferentSymbols t1 t2 -> - hsep ["Symbols differ:", pretty t1, pretty t2] -- shorten? + hsep ["Symbols differ:", pretty' @mods t1, "=/=", pretty' @mods t2] -- shorten? DifferentSorts t1 t2 -> - hsep ["Sorts differ:", pretty t1, pretty t2] -- shorten? + hsep ["Sorts differ:", pretty' @mods t1, "=/=", pretty' @mods t2] -- shorten? VariableRecursion v t -> - "Variable recursion found: " <> pretty v <> " in " <> pretty t + "Variable recursion found: " <> pretty' @mods v <> " in " <> pretty' @mods t VariableConflict v t1 t2 -> hsep - [ "Variable conflict for " <> pretty v - , pretty t1 - , pretty t2 + [ "Variable conflict for " <> pretty' @mods v + , pretty' @mods t1 + , pretty' @mods t2 ] KeyNotFound k m -> hsep - [ "Key " <> pretty k <> " not found in map" - , pretty m + [ "Key " <> pretty' @mods k <> " not found in map" + , pretty' @mods m ] DuplicateKeys k m -> hsep - [ "Key " <> pretty k <> " appears more than once in map" - , pretty m + [ "Key " <> pretty' @mods k <> " appears more than once in map" + , pretty' @mods m ] SharedVariables vs -> - "Shared variables:" <+> hsep (map pretty $ Set.toList vs) + "Shared variables:" <+> hsep (map (pretty' @mods) $ Set.toList vs) SubsortingError err -> pretty $ show err ArgLengthsDiffer t1 t2 -> - hsep ["Argument length differ", pretty t1, pretty t2] + hsep ["Argument length differ", pretty' @mods t1, pretty' @mods t2] SubjectVariableMatch t v -> - hsep ["Cannot match variable in subject:", pretty v, pretty t] + hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t] type Substitution = Map Variable Term @@ -805,7 +806,7 @@ data SortError | FoundUnknownSort Sort deriving (Eq, Show) -instance Pretty SortError where - pretty = \case +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods SortError) where + pretty (PrettyWithModifiers e) = case e of FoundSortVariable v -> "Found sort variable" <+> pretty (show v) - FoundUnknownSort s -> "FOund unknown sort" <+> pretty s + FoundUnknownSort s -> "Found unknown sort" <+> pretty' @mods s diff --git a/booster/library/Booster/Pattern/Pretty.hs b/booster/library/Booster/Pattern/Pretty.hs new file mode 100644 index 0000000000..625f63052b --- /dev/null +++ b/booster/library/Booster/Pattern/Pretty.hs @@ -0,0 +1,189 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +module Booster.Pattern.Pretty ( + -- export everything, modules above can re-export only type names + module Booster.Pattern.Pretty, +) where + +import Data.ByteString (ByteString) +import Data.Text.Encoding qualified as Text +import Prettyprinter (Pretty (..), (<+>)) +import Prettyprinter qualified as Pretty + +import Booster.Definition.Attributes.Base (NotPreservesDefinednessReason (UndefinedSymbol)) +import Booster.Pattern.Base +import Booster.Prettyprinter qualified as KPretty +import Booster.Util (decodeLabel') +import Data.ByteString.Char8 qualified as BS +import Data.Data (Proxy (..)) +import Data.Set qualified as Set +import Data.Text qualified as Text + +data ModifierT = Truncated | Infix | Decoded deriving (Show) + +data Modifiers = Modifiers + { isTruncated, isInfix, isDecoded :: Bool + } + +defaultModifiers :: Modifiers +defaultModifiers = Modifiers False False False + +class FromModifierT (m :: ModifierT) where + modifiers' :: Modifiers -> Modifiers + +instance FromModifierT 'Truncated where + modifiers' m = m{isTruncated = True} + +instance FromModifierT 'Infix where + modifiers' m = m{isInfix = True} + +instance FromModifierT 'Decoded where + modifiers' m = m{isDecoded = True} + +class FromModifiersT (m :: [ModifierT]) where + modifiers :: Modifiers -> Modifiers + +instance FromModifiersT '[] where + modifiers = id + +instance (FromModifierT m, FromModifiersT ms) => FromModifiersT (m ': ms) where + modifiers = modifiers @ms . modifiers' @m + +data ModifiersRep = forall mods. FromModifiersT mods => ModifiersRep (Proxy mods) + +toModifiersRep :: [ModifierT] -> ModifiersRep +toModifiersRep = go (ModifiersRep @'[] Proxy) + where + go rep@(ModifiersRep (Proxy :: Proxy mods)) = \case + [] -> rep + (Truncated : xs) -> go (ModifiersRep @('Truncated ': mods) Proxy) xs + (Infix : xs) -> go (ModifiersRep @('Infix ': mods) Proxy) xs + (Decoded : xs) -> go (ModifiersRep @('Decoded ': mods) Proxy) xs + +data PrettyWithModifiers (ms :: [ModifierT]) a = FromModifiersT ms => PrettyWithModifiers a + +-- used for printing the string as it appears (with codepoints) +prettyBS :: ByteString -> Pretty.Doc a +prettyBS = Pretty.pretty . Text.decodeUtf8 + +pretty' :: + forall ms a ann. (Pretty (PrettyWithModifiers ms a), FromModifiersT ms) => a -> Pretty.Doc ann +pretty' = pretty @(PrettyWithModifiers ms a) . PrettyWithModifiers + +instance Pretty (PrettyWithModifiers mods Term) where + pretty (PrettyWithModifiers t) = case t of + AndTerm t1 t2 -> + pretty' @mods t1 <+> "/\\" <+> pretty' @mods t2 + SymbolApplication symbol _sortParams args | not isInfix -> symbolApp symbol args + SymbolApplication symbol _sortParams args + | otherwise -> + if BS.count '_' (decodeLabel' symbol.name) >= length args + then + let split = Text.splitOn "_" $ Text.replace "Lbl" "" $ Text.decodeUtf8 $ decodeLabel' symbol.name + in Pretty.hsep $ interleaveArgs split $ map (pretty' @mods) args + else symbolApp symbol args + DotDotDot -> "..." + DomainValue _sort bs -> pretty . show . Text.decodeLatin1 . shortenBS $ bs + Var var -> pretty' @mods var + Injection _source _target t' -> pretty' @mods t' + KMap _attrs keyVals rest -> + Pretty.braces . Pretty.hsep . Pretty.punctuate Pretty.comma $ + [pretty' @mods k <+> "->" <+> pretty' @mods v | (k, v) <- keyVals] + ++ maybe [] ((: []) . pretty' @mods) rest + KList _meta heads (Just (mid, tails)) -> + Pretty.hsep $ + Pretty.punctuate + " +" + [renderList heads, pretty' @mods mid, renderList tails] + KList _meta [] Nothing -> + "[]" + KList _meta heads Nothing -> + renderList heads + KSet _meta [] Nothing -> "{}" + KSet _meta [] (Just rest) -> pretty' @mods rest + KSet _meta es rest -> + (Pretty.braces . Pretty.hsep . Pretty.punctuate Pretty.comma $ map (pretty' @mods) es) + Pretty.<+> maybe mempty ((" ++ " <>) . pretty' @mods) rest + where + Modifiers + { isTruncated + , isInfix + , isDecoded + } = modifiers @mods defaultModifiers + + symbolApp symbol args = + pretty + ( if isDecoded + then Text.replace "Lbl" "" $ Text.decodeUtf8 $ decodeLabel' symbol.name + else Text.decodeUtf8 symbol.name + ) + <> KPretty.arguments' (map (pretty' @mods) args) + renderList l + | null l = mempty + | otherwise = + Pretty.brackets . Pretty.hsep . Pretty.punctuate Pretty.comma $ + map (pretty' @mods) l + + interleaveArgs [] _ = [] + interleaveArgs (s : _) [] = [pretty s | not (Text.null s)] + interleaveArgs (s : ss) (a : as) | Text.null s = a : interleaveArgs ss as + interleaveArgs (s : ss) (a : as) = pretty s : a : interleaveArgs ss as + + -- shorten domain value ByteString to a readable length + shortenBS dv = + let cutoff = 16 + in if isTruncated + then if BS.length dv < cutoff then dv else BS.take cutoff dv <> "...truncated" + else dv + +instance Pretty (PrettyWithModifiers mods Sort) where + pretty (PrettyWithModifiers (SortApp name params)) = + prettyBS name <> KPretty.parameters' (map (pretty' @mods) params) + pretty (PrettyWithModifiers (SortVar name)) = + prettyBS name + +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods Variable) where + pretty :: PrettyWithModifiers mods Variable -> Pretty.Doc ann + pretty (PrettyWithModifiers var) = + prettyBS (if isDecoded then decodeLabel' var.variableName else var.variableName) + <> Pretty.colon + <> pretty' @mods var.variableSort + where + Modifiers + { isDecoded + } = modifiers @mods defaultModifiers + +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods Predicate) where + pretty (PrettyWithModifiers (Predicate t)) = pretty' @mods t + +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods Ceil) where + pretty (PrettyWithModifiers (Ceil t)) = + "\\ceil" + <> KPretty.noParameters + <> KPretty.arguments' [pretty' @mods t] + +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods Pattern) where + pretty (PrettyWithModifiers patt) = + Pretty.vsep $ + [ "Term:" + , Pretty.indent 4 $ pretty' @mods patt.term + , "Conditions:" + ] + <> fmap (Pretty.indent 4) (map (pretty' @mods) $ Set.toList patt.constraints) + <> fmap (Pretty.indent 4) (map (pretty' @mods) patt.ceilConditions) + +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods NotPreservesDefinednessReason) where + pretty = \case + PrettyWithModifiers (UndefinedSymbol name) -> + pretty $ + if isDecoded + then Text.replace "Lbl" "" $ Text.decodeUtf8 $ decodeLabel' name + else Text.decodeUtf8 name + where + Modifiers + { isDecoded + } = modifiers @mods defaultModifiers diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index ba37452c53..d5e3f86cd0 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} {- | Copyright : (c) Runtime Verification, 2022 @@ -29,6 +30,7 @@ import Control.Monad.Trans.State.Strict (StateT (runStateT), get, modify) import Data.Aeson (object, (.=)) import Data.Bifunctor (bimap) import Data.Coerce (coerce) +import Data.Data (Proxy) import Data.Hashable qualified as Hashable import Data.List (intersperse, partition) import Data.List.NonEmpty (NonEmpty (..), toList) @@ -61,6 +63,7 @@ import Booster.Pattern.Match ( SortError, matchTerms, ) +import Booster.Pattern.Pretty import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT @@ -79,10 +82,13 @@ data RewriteConfig = RewriteConfig , smtSolver :: Maybe SMT.SMTContext , doTracing :: Flag "CollectRewriteTraces" , logger :: Logger LogMessage + , prettyModifiers :: ModifiersRep } instance MonadIO io => LoggerMIO (RewriteT io) where getLogger = RewriteT $ asks logger + getPrettyModifiers = RewriteT $ asks prettyModifiers + withLogger modL (RewriteT m) = RewriteT $ withReaderT (\cfg@RewriteConfig{logger} -> cfg{logger = modL logger}) m pattern CollectRewriteTraces :: Flag "CollectRewriteTraces" @@ -102,9 +108,10 @@ runRewriteT :: io (Either (RewriteFailed "Rewrite") (a, SimplifierCache)) runRewriteT doTracing definition llvmApi smtSolver cache m = do logger <- getLogger + prettyModifiers <- getPrettyModifiers runExceptT . flip runStateT cache - . flip runReaderT RewriteConfig{definition, llvmApi, smtSolver, doTracing, logger} + . flip runReaderT RewriteConfig{definition, llvmApi, smtSolver, doTracing, logger, prettyModifiers} . unRewriteT $ m @@ -269,155 +276,176 @@ applyRule :: Pattern -> RewriteRule "Rewrite" -> RewriteT io (RewriteRuleAppResult (RewriteRule "Rewrite", Pattern)) -applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRuleAppT $ do - def <- lift getDefinition - -- unify terms - subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of - MatchFailed (SubsortingError sortError) -> do - withContext CtxError $ logPretty sortError - failRewrite $ RewriteSortError rule pat.term sortError - MatchFailed err@ArgLengthsDiffer{} -> do - withContext CtxError $ logPretty err - failRewrite $ InternalMatchError $ renderText $ pretty err - MatchFailed reason -> do - withContext CtxFailure $ logPretty reason - fail "Rule matching failed" - MatchIndeterminate remainder -> do - withContext CtxIndeterminate $ - logMessage $ - WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ - renderOneLineText $ - "Uncertain about match with rule. Remainder:" <+> pretty remainder - failRewrite $ RuleApplicationUnclear rule pat.term remainder - MatchSuccess substitution -> do - withContext CtxSuccess $ do - logMessage rule - withContext CtxSubstitution - $ logMessage - $ WithJsonMessage - ( object - ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)] - ) - $ renderOneLineText - $ "Substitution:" - <+> (hsep $ intersperse "," $ map (\(k, v) -> pretty k <+> "->" <+> pretty v) $ Map.toList substitution) - pure substitution - - -- Also fail the whole rewrite if a rule applies but may introduce - -- an undefined term. - unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do - withContext CtxDefinedness . withContext CtxAbort $ - logMessage $ - renderOneLineText $ - "Uncertain about definedness of rule due to:" - <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) - failRewrite $ - DefinednessUnclear - rule - pat - rule.computedAttributes.notPreservesDefinednessReasons - - -- apply substitution to rule requires constraints and simplify (one by one - -- in isolation). Stop if false, abort rewrite if indeterminate. - let ruleRequires = - concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires - notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied - -- filter out any predicates known to be _syntactically_ present in the known prior - let prior = pat.constraints - (knownTrue, toCheck) = partition (`Set.member` prior) ruleRequires - unless (null knownTrue) $ - logMessage $ - renderOneLineText $ - "Known true side conditions (won't check):" <+> pretty knownTrue - - unclearRequires <- - catMaybes <$> mapM (checkConstraint id notAppliedIfBottom) toCheck - - -- check unclear requires-clauses in the context of known constraints (prior) - mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask - - let smtUnclear = do - withContext CtxConstraint . withContext CtxAbort . logMessage . renderOneLineText $ - "Uncertain about condition(s) in a rule:" <+> pretty unclearRequires - failRewrite $ - RuleConditionUnclear rule . coerce . foldl1 AndTerm $ - map coerce unclearRequires - case mbSolver of - Just solver -> do - checkAllRequires <- - SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires) - - case checkAllRequires of - Left SMT.SMTSolverUnknown{} -> - smtUnclear -- abort rewrite if a solver result was Unknown - Left other -> - liftIO $ Exception.throw other -- fail hard on other SMT errors - Right (Just False) -> do - -- requires is actually false given the prior - withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure NotApplied - Right (Just True) -> - pure () -- can proceed - Right Nothing -> - smtUnclear -- no implication could be determined - Nothing -> - unless (null unclearRequires) $ do - withContext CtxConstraint . withContext CtxAbort $ - logMessage $ - renderOneLineText $ - "Uncertain about a condition(s) in rule, no SMT solver:" <+> pretty unclearRequires - failRewrite $ - RuleConditionUnclear rule (head unclearRequires) - - -- 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 . coerce . substituteInTerm subst . coerce) $ - Set.toList rule.ensures - trivialIfBottom = RewriteRuleAppT $ pure Trivial - newConstraints <- - catMaybes <$> mapM (checkConstraint id trivialIfBottom) ruleEnsures - - -- check all new constraints together with the known side constraints - whenJust mbSolver $ \solver -> - (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case - Right (Just False) -> do - withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure Trivial - Right _other -> - pure () - Left SMT.SMTSolverUnknown{} -> - pure () - Left other -> - liftIO $ Exception.throw other - - -- existential variables may be present in rule.rhs and rule.ensures, - -- need to strip prefixes and freshen their names with respect to variables already - -- present in the input pattern and in the unification substitution - let varsFromInput = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) - varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst - forbiddenVars = varsFromInput <> varsFromSubst - existentialSubst = - Map.fromSet - (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) - rule.existentials - - -- modify the substitution to include the existentials - let substWithExistentials = subst `Map.union` existentialSubst - - let rewritten = - Pattern - (substituteInTerm substWithExistentials rule.rhs) - -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables - ( pat.constraints - <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) - ) - ceilConditions - withContext CtxSuccess $ - withPatternContext rewritten $ - return (rule, rewritten) +applyRule pat@Pattern{ceilConditions} rule = + withRuleContext rule $ + runRewriteRuleAppT $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do + def <- lift getDefinition + -- unify terms + subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of + MatchFailed (SubsortingError sortError) -> do + withContext CtxError $ logPretty' @mods sortError + failRewrite $ RewriteSortError rule pat.term sortError + MatchFailed err@ArgLengthsDiffer{} -> do + withContext CtxError $ + logPretty' @mods err + failRewrite $ InternalMatchError $ renderText $ pretty' @mods err + MatchFailed reason -> do + withContext CtxFailure $ logPretty' @mods reason + fail "Rule matching failed" + MatchIndeterminate remainder -> do + withContext CtxIndeterminate $ + logMessage $ + WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ + renderOneLineText $ + "Uncertain about match with rule. Remainder:" + <+> ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NE.toList remainder + ) + failRewrite $ RuleApplicationUnclear rule pat.term remainder + MatchSuccess substitution -> do + withContext CtxSuccess $ do + logMessage rule + withContext CtxSubstitution + $ logMessage + $ WithJsonMessage + ( object + ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)] + ) + $ renderOneLineText + $ "Substitution:" + <+> ( hsep $ + intersperse "," $ + map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ + Map.toList substitution + ) + pure substitution + + -- Also fail the whole rewrite if a rule applies but may introduce + -- an undefined term. + unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do + withContext CtxDefinedness . withContext CtxAbort $ + logMessage $ + renderOneLineText $ + "Uncertain about definedness of rule due to:" + <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) + failRewrite $ + DefinednessUnclear + rule + pat + rule.computedAttributes.notPreservesDefinednessReasons + + -- apply substitution to rule requires constraints and simplify (one by one + -- in isolation). Stop if false, abort rewrite if indeterminate. + let ruleRequires = + concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires + notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied + -- filter out any predicates known to be _syntactically_ present in the known prior + let prior = pat.constraints + (knownTrue, toCheck) = partition (`Set.member` prior) ruleRequires + unless (null knownTrue) $ + logMessage $ + renderOneLineText $ + "Known true side conditions (won't check):" + <+> (hsep . punctuate comma . map (pretty' @mods) $ knownTrue) + + unclearRequires <- + catMaybes <$> mapM (checkConstraint id notAppliedIfBottom) toCheck + + -- check unclear requires-clauses in the context of known constraints (prior) + mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask + + let smtUnclear = do + withContext CtxConstraint . withContext CtxAbort . logMessage $ + WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> unclearRequires)]) $ + renderOneLineText $ + "Uncertain about condition(s) in a rule:" + <+> (hsep . punctuate comma . map (pretty' @mods) $ unclearRequires) + failRewrite $ + RuleConditionUnclear rule . coerce . foldl1 AndTerm $ + map coerce unclearRequires + case mbSolver of + Just solver -> do + checkAllRequires <- + SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires) + + case checkAllRequires of + Left SMT.SMTSolverUnknown{} -> + smtUnclear -- abort rewrite if a solver result was Unknown + Left other -> + liftIO $ Exception.throw other -- fail hard on other SMT errors + Right (Just False) -> do + -- requires is actually false given the prior + withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) + RewriteRuleAppT $ pure NotApplied + Right (Just True) -> + pure () -- can proceed + Right Nothing -> + smtUnclear -- no implication could be determined + Nothing -> + unless (null unclearRequires) $ do + withContext CtxConstraint . withContext CtxAbort $ + logMessage $ + WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> unclearRequires)]) $ + renderOneLineText $ + "Uncertain about a condition(s) in rule, no SMT solver:" + <+> (hsep . punctuate comma . map (pretty' @mods) $ unclearRequires) + failRewrite $ + RuleConditionUnclear rule (head unclearRequires) + + -- 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 . coerce . substituteInTerm subst . coerce) $ + Set.toList rule.ensures + trivialIfBottom = RewriteRuleAppT $ pure Trivial + newConstraints <- + catMaybes <$> mapM (checkConstraint id trivialIfBottom) ruleEnsures + + -- check all new constraints together with the known side constraints + whenJust mbSolver $ \solver -> + (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case + Right (Just False) -> do + withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) + RewriteRuleAppT $ pure Trivial + Right _other -> + pure () + Left SMT.SMTSolverUnknown{} -> + pure () + Left other -> + liftIO $ Exception.throw other + + -- existential variables may be present in rule.rhs and rule.ensures, + -- need to strip prefixes and freshen their names with respect to variables already + -- present in the input pattern and in the unification substitution + let varsFromInput = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) + varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst + forbiddenVars = varsFromInput <> varsFromSubst + existentialSubst = + Map.fromSet + (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) + rule.existentials + + -- modify the substitution to include the existentials + let substWithExistentials = subst `Map.union` existentialSubst + + let rewritten = + Pattern + (substituteInTerm substWithExistentials rule.rhs) + -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables + ( pat.constraints + <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) + ) + ceilConditions + withContext CtxSuccess $ + withPatternContext rewritten $ + return (rule, rewritten) where - failRewrite = lift . throw + failRewrite :: RewriteFailed "Rewrite" -> RewriteRuleAppT (RewriteT io) a + failRewrite = lift . (throw) checkConstraint :: (Predicate -> a) -> @@ -460,44 +488,49 @@ data RewriteFailed k TermIndexIsNone Term deriving stock (Eq, Show) -instance Pretty (RewriteFailed k) where - pretty (NoApplicableRules pat) = - "No rules applicable for the pattern " <> pretty pat - pretty (RuleApplicationUnclear rule term remainder) = - hsep - [ "Uncertain about unification of rule" - , ruleLabelOrLoc rule - , " with term " - , pretty term - , "Remainder:" - , pretty remainder - ] - pretty (RuleConditionUnclear rule predicate) = - hsep - [ "Uncertain about a condition in rule" - , ruleLabelOrLoc rule - , ": " - , pretty predicate - ] - pretty (DefinednessUnclear rule _pat reasons) = - hsep $ - [ "Uncertain about definedness of rule " - , ruleLabelOrLoc rule - , "because of:" - ] - ++ map pretty reasons - pretty (RewriteSortError rule term sortError) = - hsep - [ "Sort error while unifying" - , pretty term - , "with rule" - , ruleLabelOrLoc rule - , ":" - , pretty $ show sortError - ] - pretty (TermIndexIsNone term) = - "Term index is None for term " <> pretty term - pretty (InternalMatchError err) = "An internal error occured" <> pretty err +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods (RewriteFailed k)) where + pretty (PrettyWithModifiers f) = case f of + NoApplicableRules pat -> + "No rules applicable for the pattern " <> pretty' @mods pat + RuleApplicationUnclear rule term remainder -> + hsep + [ "Uncertain about unification of rule" + , ruleLabelOrLoc rule + , " with term " + , pretty' @mods term + , "Remainder:" + , ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NE.toList remainder + ) + ] + RuleConditionUnclear rule predicate -> + hsep + [ "Uncertain about a condition in rule" + , ruleLabelOrLoc rule + , ": " + , pretty' @mods predicate + ] + DefinednessUnclear rule _pat reasons -> + hsep $ + [ "Uncertain about definedness of rule " + , ruleLabelOrLoc rule + , "because of:" + ] + ++ map pretty reasons + RewriteSortError rule term sortError -> + hsep + [ "Sort error while unifying" + , pretty' @mods term + , "with rule" + , ruleLabelOrLoc rule + , ":" + , pretty $ show sortError + ] + TermIndexIsNone term -> + "Term index is None for term " <> pretty' @mods term + InternalMatchError err -> "An internal error occured" <> pretty err ruleLabelOrLoc :: RewriteRule k -> Doc a ruleLabelOrLoc rule = @@ -546,29 +579,29 @@ eraseStates = \case RewriteStepFailed failureInfo -> RewriteStepFailed failureInfo RewriteSimplified mbEquationFailure -> RewriteSimplified mbEquationFailure -instance Pretty (RewriteTrace Pattern) where - pretty = \case +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods (RewriteTrace Pattern)) where + pretty (PrettyWithModifiers t) = case t of RewriteSingleStep lbl _uniqueId pat rewritten -> let (l, r) = diff pat rewritten in hang 4 . vsep $ [ "Rewriting configuration" - , pretty l.term + , pretty' @mods l.term , "to" - , pretty r.term + , pretty' @mods r.term , "Using rule:" , pretty lbl ] RewriteBranchingStep pat branches -> hang 4 . vsep $ [ "Configuration" - , pretty (term pat) + , pretty' @mods (term pat) , "branches on rules:" , hang 2 $ vsep [pretty lbl | (lbl, _) <- toList branches] ] RewriteSimplified{} -> "Applied simplification" - RewriteStepFailed failure -> pretty failure + RewriteStepFailed failure -> pretty' @mods failure diff :: Pattern -> Pattern -> (Pattern, Pattern) diff p1 p2 = @@ -843,10 +876,18 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL withSimplified pat' "Retrying with simplified pattern" (doSteps True) | otherwise -> do -- was already simplified, emit an abort log entry - withRuleContext rule . withContext CtxMatch . withContext CtxAbort . logMessage $ - WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ - renderOneLineText $ - "Uncertain about match with rule. Remainder:" <+> pretty remainder + withRuleContext rule . withContext CtxMatch . withContext CtxAbort $ + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + logMessage $ + WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ + renderOneLineText $ + "Uncertain about match with rule. Remainder:" + <+> ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NE.toList remainder + ) emitRewriteTrace $ RewriteStepFailed failure logMessage $ "Aborted after " <> showCounter counter pure (RewriteAborted failure pat') diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index fe0dedcf2e..b6efb0eae8 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} + {- | Copyright : (c) Runtime Verification, 2023 License : BSD-3-Clause @@ -22,6 +25,7 @@ import Control.Monad.Trans.Except import Control.Monad.Trans.State import Data.ByteString.Char8 qualified as BS import Data.Coerce +import Data.Data (Proxy) import Data.Either (isLeft) import Data.Either.Extra (fromLeft', fromRight') import Data.Map (Map) @@ -29,12 +33,13 @@ import Data.Map qualified as Map import Data.Set (Set) import Data.Set qualified as Set import Data.Text as Text (Text, pack, unlines, unwords) -import Prettyprinter (Pretty, hsep, pretty) +import Prettyprinter (Pretty, hsep) import SMTLIB.Backends.Process qualified as Backend import Booster.Definition.Base import Booster.Log qualified as Log import Booster.Pattern.Base +import Booster.Pattern.Pretty import Booster.Pattern.Util (sortOfTerm) import Booster.Prettyprinter qualified as Pretty import Booster.SMT.Base as SMT @@ -266,8 +271,10 @@ getModelFor ctxt ps subst (const . ((`Set.member` sortsToTranslate) . (.variableSort))) freeVarsMap unless (Map.null untranslatableVars) $ - let vars = Pretty.renderText . hsep . map pretty $ Map.keys untranslatableVars - in Log.logMessage ("Untranslatable variables in model: " <> vars) + Log.getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + let vars = Pretty.renderText . hsep . map (pretty' @mods) $ Map.keys untranslatableVars + in Log.logMessage ("Untranslatable variables in model: " <> vars) response <- if Map.null freeVarsMap @@ -293,8 +300,8 @@ getModelFor ctxt ps subst other -> throwSMT' $ "Unexpected SMT response to GetValue: " <> show other -mkComment :: Pretty a => a -> BS.ByteString -mkComment = BS.pack . Pretty.renderDefault . pretty +mkComment :: Pretty (PrettyWithModifiers '[Decoded] a) => a -> BS.ByteString +mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded] {- | Check a predicates, given a set of predicates as known truth. @@ -354,8 +361,10 @@ checkPredicates ctxt givenPs givenSubst psToCheck , "assertions and a substitution of size" , pack (show $ Map.size givenSubst) ] - Log.logMessage . Pretty.renderOneLineText $ - hsep ("Predicates to check:" : map pretty (Set.toList psToCheck)) + Log.getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> + Log.logMessage . Pretty.renderOneLineText $ + hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck)) result <- interactWithSolver smtGiven sexprsToCheck Log.logMessage $ "Check of Given ∧ P and Given ∧ !P produced " diff --git a/booster/library/Booster/SMT/Translate.hs b/booster/library/Booster/SMT/Translate.hs index 42cd44e50e..37b72b7331 100644 --- a/booster/library/Booster/SMT/Translate.hs +++ b/booster/library/Booster/SMT/Translate.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE FlexibleContexts #-} + {- | Copyright : (c) Runtime Verification, 2023 License : BSD-3-Clause @@ -36,6 +38,7 @@ import Booster.Definition.Attributes.Base import Booster.Definition.Base import Booster.Pattern.Base import Booster.Pattern.Bool +import Booster.Pattern.Pretty import Booster.Pattern.Util (sortOfTerm) import Booster.Prettyprinter qualified as Pretty import Booster.SMT.Base as SMT @@ -84,7 +87,7 @@ translateTerm t = | otherwise -> throw $ "General \and not supported for SMT. Failed to translate " - <> Pretty.renderText (pretty t) + <> Pretty.renderText (pretty (PrettyWithModifiers @['Decoded, 'Truncated] t)) SymbolApplication sym _sorts args -> case sym.attributes.smt of Nothing -> asSMTVar t @@ -198,7 +201,7 @@ equationToSMTLemma equation -- for detailed error messages: let prettyMappings m = Pretty.vsep - [ Pretty.pretty (show v) <> " <== " <> Pretty.pretty t + [ Pretty.pretty (show v) <> " <== " <> Pretty.pretty (PrettyWithModifiers @['Decoded, 'Truncated] t) | (t, v) <- Map.toList m ] lemmaId = @@ -241,10 +244,16 @@ equationToSMTLemma equation ] prettyLemma = Pretty.vsep - ( pretty equation.lhs <> " == " <> pretty equation.rhs + ( pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.lhs) + <> " == " + <> pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.rhs) : if Set.null equation.requires then [] - else " requires" : map (Pretty.indent 4 . pretty) (Set.toList equation.requires) + else + " requires" + : map + ((Pretty.indent 4 . pretty) . (PrettyWithModifiers @['Decoded, 'Truncated])) + (Set.toList equation.requires) ) lemmaComment = BS.pack (Pretty.renderDefault prettyLemma) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 8582453e0b..0ab79b7378 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -67,6 +67,7 @@ import Booster.Definition.Base (KoreDefinition (..), emptyKoreDefinition) import Booster.Log (LoggerMIO, logMessage, withKorePatternContext) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal +import Booster.Pattern.Pretty import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort) import Booster.Prettyprinter (renderDefault) import Booster.Syntax.Json (addHeader) @@ -110,12 +111,16 @@ data InternalisedPredicates = InternalisedPredicates } deriving stock (Eq, Show) -instance Pretty InternalisedPredicates where - pretty ps = +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods InternalisedPredicates) where + pretty (PrettyWithModifiers ps) = Pretty.vsep $ - ("Bool predicates: " : map pretty (Set.toList ps.boolPredicates)) - <> ("Ceil predicates: " : map pretty (Set.toList ps.ceilPredicates)) - <> ("Substitution: " : map pretty (Map.assocs ps.substitution)) + ("Bool predicates: " : map (pretty' @mods) (Set.toList ps.boolPredicates)) + <> ("Ceil predicates: " : map (pretty' @mods) (Set.toList ps.ceilPredicates)) + <> ( "Substitution: " + : map + (\(v, t) -> pretty' @mods v Pretty.<+> "->" Pretty.<+> pretty' @mods t) + (Map.assocs ps.substitution) + ) <> ("Unsupported predicates: " : map (pretty . show) ps.unsupported) data TermOrPredicates -- = Either Predicate Pattern @@ -652,7 +657,7 @@ patternErrorToRpcError = \case NoTermFound p -> wrap "Pattern must contain at least one term" p PatternSortError p sortErr -> - wrap (renderSortError sortErr) p + wrap (renderSortError (PrettyWithModifiers @['Decoded, 'Truncated] sortErr)) p InconsistentPattern p -> wrap "Inconsistent pattern" p TermExpected p -> @@ -708,8 +713,8 @@ data SortError | IncorrectSort Internal.Sort Internal.Sort deriving stock (Eq, Show) -renderSortError :: SortError -> Text -renderSortError = \case +renderSortError :: forall mods. FromModifiersT mods => PrettyWithModifiers mods SortError -> Text +renderSortError (PrettyWithModifiers e) = case e of UnknownSort sort -> "Unknown " <> render sort WrongSortArgCount sort expected -> @@ -729,7 +734,7 @@ renderSortError = \case <> " but got " <> prettyText got where - prettyText = pack . renderDefault . pretty + prettyText = pack . renderDefault . pretty' @mods render = \case Syntax.SortVar (Syntax.Id n) -> diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 2171578a16..7f3bda4c3d 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -56,6 +56,7 @@ import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..)) import Booster.Pattern.Bool (foldAndBool) import Booster.Pattern.Bool qualified as Def import Booster.Pattern.Index as Idx +import Booster.Pattern.Pretty import Booster.Pattern.Util qualified as Util import Booster.Prettyprinter hiding (attributes) import Booster.Syntax.Json.Internalise @@ -1333,8 +1334,8 @@ data DefinitionError | ElemSymbolNotFound Def.SymbolName deriving stock (Eq, Show) -instance Pretty DefinitionError where - pretty = \case +instance FromModifiersT mods => Pretty (PrettyWithModifiers mods DefinitionError) where + pretty (PrettyWithModifiers e) = case e of ParseError msg -> "Parse error: " <> pretty msg NoSuchModule name -> @@ -1352,7 +1353,7 @@ instance Pretty DefinitionError where DefinitionAttributeError msg -> pretty $ "Attribute error: " <> msg DefinitionSortError sortErr -> - pretty $ "Sort error: " <> renderSortError sortErr + pretty $ "Sort error: " <> renderSortError @mods (PrettyWithModifiers sortErr) DefinitionPatternError ref patErr -> "Pattern error in " <> pretty ref <> ": " <> pretty (show patErr) -- TODO define a pretty instance? @@ -1382,7 +1383,8 @@ definitionErrorToRpcError = \case let err@RpcError.ErrorWithTermAndContext{context} = patternErrorToRpcError patErr in err { RpcError.context = - Just $ "Pattern error at " <> render ref <> " in definition" : fromMaybe [] context + Just $ + "Pattern error at " <> renderOneLineText (pretty ref) <> " in definition" : fromMaybe [] context } DefinitionAxiomError (MalformedRewriteRule rule) -> "Malformed rewrite rule" `withContext` [renderOneLineText $ location rule] @@ -1396,8 +1398,8 @@ definitionErrorToRpcError = \case withContext :: Text -> [Text] -> RpcError.ErrorWithTermAndContext withContext = RpcError.ErrorWithContext - render :: Pretty a => a -> Text - render = renderOneLineText . pretty + render :: forall a. Pretty (PrettyWithModifiers ['Decoded, 'Truncated] a) => a -> Text + render = renderOneLineText . pretty @(PrettyWithModifiers ['Decoded, 'Truncated] a) . PrettyWithModifiers location rule = either (const "unknown location") pretty $ diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index 00257900ef..5ce3270771 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -2,20 +2,20 @@ {"context":["proxy"],"message":"Starting RPC server"} {"context":["proxy"],"message":"Processing request 4"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"} +{"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\")"} +{"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\")"} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"2fbed22"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"80d934c"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} \"$n\""} +{"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= \"$n\""} {"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} @@ -31,7 +31,7 @@ {"context":[{"request":"4"},"booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"5b84449"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"} +{"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} @@ -39,7 +39,7 @@ {"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"} {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 42441b832a..8f1cdadbe7 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {- | @@ -47,7 +48,6 @@ import System.IO (hPutStrLn, stderr) import Booster.CLOptions import Booster.Definition.Attributes.Base ( ComputedAxiomAttributes (notPreservesDefinednessReasons), - NotPreservesDefinednessReason (UndefinedSymbol), ) import Booster.Definition.Base ( KoreDefinition (..), @@ -60,6 +60,7 @@ import Booster.LLVM.Internal (mkAPI, withDLib) import Booster.Log hiding (withLogger) import Booster.Log.Context qualified as Ctxt import Booster.Pattern.Base (Predicate (..)) +import Booster.Pattern.Pretty import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..)) import Booster.SMT.Interface (SMTOptions (..)) @@ -67,6 +68,7 @@ import Booster.Syntax.Json.Externalise (externaliseTerm) import Booster.Syntax.ParsedKore (loadDefinition) import Booster.Trace import Booster.Util qualified as Booster +import Data.Data (Proxy) import GlobalMain qualified import Kore.Attribute.Symbol (StepperAttributes) import Kore.BugReport (BugReportOption (..), withBugReport) @@ -133,6 +135,7 @@ main = do , smtOptions , equationOptions , indexCells + , prettyPrintOptions , eventlogEnabledUserEvents } , proxyOptions = @@ -196,7 +199,9 @@ main = do in any (flip Ctxt.mustMatch ctxt) logContextsWithcustomLevelContexts runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a - runBoosterLogger = flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT + runBoosterLogger = + flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions) + . Booster.Log.unLoggerT koreLogActions :: forall m. MonadIO m => [Log.LogAction m Log.SomeEntry] koreLogActions = [koreLogAction] @@ -245,47 +250,48 @@ main = do liftIO $ runBoosterLogger $ - Booster.Log.withContext CtxInfo $ -- FIXME "ceil" $ - forM_ (Map.elems definitionsWithCeilSummaries) $ \(KoreDefinition{simplifications}, summaries) -> do - forM_ summaries $ \ComputeCeilSummary{rule, ceils} -> - Booster.Log.withRuleContext rule $ do - Booster.Log.withContext CtxInfo -- FIXME "partial-symbols" + getPrettyModifiers >>= \case + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> Booster.Log.withContext CtxInfo $ -- FIXME "ceil" $ + forM_ (Map.elems definitionsWithCeilSummaries) $ \(KoreDefinition{simplifications}, summaries) -> do + forM_ summaries $ \ComputeCeilSummary{rule, ceils} -> + Booster.Log.withRuleContext rule $ do + Booster.Log.withContext CtxInfo -- FIXME "partial-symbols" + $ Booster.Log.logMessage + $ Booster.Log.WithJsonMessage + (JSON.toJSON rule.computedAttributes.notPreservesDefinednessReasons) + $ renderOneLineText + $ Pretty.hsep + $ Pretty.punctuate Pretty.comma + $ map + (pretty' @mods) + rule.computedAttributes.notPreservesDefinednessReasons + unless (null ceils) + $ Booster.Log.withContext CtxInfo -- FIXME"computed-ceils" + $ Booster.Log.logMessage + $ Booster.Log.WithJsonMessage + ( JSON.object + ["ceils" JSON..= (bimap (externaliseTerm . coerce) externaliseTerm <$> Set.toList ceils)] + ) + $ renderOneLineText + $ Pretty.hsep + $ Pretty.punctuate Pretty.comma + $ map + (either (pretty' @mods) (\t -> "#Ceil(" Pretty.<+> pretty' @mods t Pretty.<+> ")")) + (Set.toList ceils) + + forM_ (concat $ concatMap Map.elems simplifications) $ \s -> + unless (null s.computedAttributes.notPreservesDefinednessReasons) + $ Booster.Log.withRuleContext s + $ Booster.Log.withContext CtxInfo -- FIXME"partial-symbols" $ Booster.Log.logMessage $ Booster.Log.WithJsonMessage - (JSON.toJSON rule.computedAttributes.notPreservesDefinednessReasons) + (JSON.toJSON s.computedAttributes.notPreservesDefinednessReasons) $ renderOneLineText $ Pretty.hsep $ Pretty.punctuate Pretty.comma $ map - (\(UndefinedSymbol sym) -> Pretty.pretty $ Text.decodeUtf8 $ Booster.decodeLabel' sym) - rule.computedAttributes.notPreservesDefinednessReasons - unless (null ceils) - $ Booster.Log.withContext CtxInfo -- FIXME"computed-ceils" - $ Booster.Log.logMessage - $ Booster.Log.WithJsonMessage - ( JSON.object - ["ceils" JSON..= (bimap (externaliseTerm . coerce) externaliseTerm <$> Set.toList ceils)] - ) - $ renderOneLineText - $ Pretty.hsep - $ Pretty.punctuate Pretty.comma - $ map - (either Pretty.pretty (\t -> "#Ceil(" Pretty.<+> Pretty.pretty t Pretty.<+> ")")) - (Set.toList ceils) - - forM_ (concat $ concatMap Map.elems simplifications) $ \s -> - unless (null s.computedAttributes.notPreservesDefinednessReasons) - $ Booster.Log.withRuleContext s - $ Booster.Log.withContext CtxInfo -- FIXME"partial-symbols" - $ Booster.Log.logMessage - $ Booster.Log.WithJsonMessage - (JSON.toJSON s.computedAttributes.notPreservesDefinednessReasons) - $ renderOneLineText - $ Pretty.hsep - $ Pretty.punctuate Pretty.comma - $ map - (\(UndefinedSymbol sym) -> Pretty.pretty $ Text.decodeUtf8 $ Booster.decodeLabel' sym) - s.computedAttributes.notPreservesDefinednessReasons + (pretty' @mods) + s.computedAttributes.notPreservesDefinednessReasons mvarLogAction <- newMVar actualLogAction let logAction = swappableLogger mvarLogAction diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs index abb3855b7c..316ce0c864 100644 --- a/dev-tools/booster-dev/Server.hs +++ b/dev-tools/booster-dev/Server.hs @@ -31,6 +31,7 @@ import Booster.LLVM as LLVM (API) import Booster.LLVM.Internal (mkAPI, withDLib) import Booster.Log qualified import Booster.Log.Context qualified as Booster.Log +import Booster.Pattern.Pretty import Booster.SMT.Interface qualified as SMT import Booster.Syntax.ParsedKore (loadDefinition) import Booster.Trace @@ -60,6 +61,7 @@ main = do , smtOptions , equationOptions , indexCells + , prettyPrintOptions , eventlogEnabledUserEvents , logFile } = options @@ -98,6 +100,7 @@ main = do logTimeStamps timeStampsFormat logFormat + prettyPrintOptions where withLlvmLib libFile m = case libFile of Nothing -> m Nothing @@ -128,8 +131,9 @@ runServer :: Bool -> TimestampFormat -> LogFormat -> + [ModifierT] -> IO () -runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat = +runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat prettyPrintOptions = do let timestampFlag = case timeStampsFormat of Pretty -> PrettyTimestamps @@ -159,7 +163,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev jsonRpcServer (serverSettings port "*") ( const $ - flip runReaderT filteredBoosterContextLogger + flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions) . Booster.Log.unLoggerT . Booster.Log.withContext Booster.Log.CtxBooster . respond stateVar diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs index 1a0e4dfefe..768d3d2788 100644 --- a/dev-tools/kore-rpc-dev/Server.hs +++ b/dev-tools/kore-rpc-dev/Server.hs @@ -41,6 +41,7 @@ import System.Log.FastLogger (newTimeCache) import Booster.CLOptions import Booster.Log import Booster.Log.Context qualified +import Booster.Pattern.Pretty import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..)) import Booster.SMT.Interface (SMTOptions (..)) import Booster.Trace @@ -147,6 +148,7 @@ main = do , eventlogEnabledUserEvents , logFile , logTimeStamps + , prettyPrintOptions } } = options (logLevel, customLevels) = adjustLogLevels logLevels @@ -221,7 +223,9 @@ main = do in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a - runBoosterLogger = flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT + runBoosterLogger = + flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions) + . Booster.Log.unLoggerT liftIO $ void $ withBugReport (ExeName "kore-rpc-dev") BugReportOnError $ \_reportDirectory -> Kore.Log.BoosterAdaptor.withLogger koreLogOptions $ \actualLogAction -> do diff --git a/dev-tools/parsetest/Parsetest.hs b/dev-tools/parsetest/Parsetest.hs index 442c55cb38..40354db90c 100644 --- a/dev-tools/parsetest/Parsetest.hs +++ b/dev-tools/parsetest/Parsetest.hs @@ -15,13 +15,13 @@ import Control.Monad.Trans.Except import Data.Bifunctor (first) import Data.List (isPrefixOf, partition) import Data.Text.IO qualified as Text -import Prettyprinter import System.Directory import System.Environment import System.FilePath import Booster.Definition.Ceil (computeCeilsDefinition) import Booster.Definition.Util +import Booster.Pattern.Pretty import Booster.Prettyprinter as Pretty import Booster.Syntax.ParsedKore as ParsedKore @@ -57,7 +57,7 @@ testParse verbose veryVerbose file = do report = runExceptT $ do parsedDef <- liftIO (Text.readFile file) >>= except . parseKoreDefinition file - internalDef' <- except (first (renderDefault . pretty) $ internalise Nothing parsedDef) + internalDef' <- except (first (renderDefault . pretty' @'[Decoded]) $ internalise Nothing parsedDef) (internalDef, ceilSummary) <- runNoLoggingT $ computeCeilsDefinition Nothing internalDef' pure $ mkSummary file internalDef ceilSummary diff --git a/dev-tools/pretty/Pretty.hs b/dev-tools/pretty/Pretty.hs index 8d4ef4c428..e7a2400bc9 100644 --- a/dev-tools/pretty/Pretty.hs +++ b/dev-tools/pretty/Pretty.hs @@ -9,6 +9,7 @@ module Main ( main, ) where +import Booster.Pattern.Pretty import Booster.Prettyprinter (renderDefault) import Booster.Syntax.Json (KoreJson (..)) import Booster.Syntax.Json.Internalise ( @@ -32,7 +33,7 @@ main = do [def, json] <- getArgs parsedDef <- either (error . renderDefault . pretty) id . parseKoreDefinition def <$> Text.readFile def - let internalDef = either (error . renderDefault . pretty) id $ internalise Nothing parsedDef + let internalDef = either (error . renderDefault . pretty' @'[Decoded]) id $ internalise Nothing parsedDef fileContent <- BS.readFile json case eitherDecode fileContent of @@ -41,18 +42,18 @@ main = do case runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term of Right (trm, _subst, _unsupported) -> do putStrLn "Pretty-printing pattern: " - putStrLn $ renderDefault $ pretty trm + putStrLn $ renderDefault $ pretty' @'[Decoded] trm Left (NoTermFound _) -> case runExcept $ internalisePredicates DisallowAlias CheckSubsorts Nothing internalDef [term] of Left es -> error (show es) Right ts -> do putStrLn "Pretty-printing predicates: " putStrLn "Bool predicates: " - mapM_ (putStrLn . renderDefault . pretty) ts.boolPredicates + mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.boolPredicates putStrLn "Ceil predicates: " - mapM_ (putStrLn . renderDefault . pretty) ts.ceilPredicates + mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.ceilPredicates putStrLn "Substitution: " - mapM_ (putStrLn . renderDefault . pretty) ts.substitution + mapM_ (putStrLn . renderDefault . pretty' @'[Decoded]) ts.substitution putStrLn "Unsupported predicates: " mapM_ print ts.unsupported Left err -> error (show err)