diff --git a/hie-cabal.yaml b/hie-cabal.yaml index b8b275812c..df908d86bf 100644 --- a/hie-cabal.yaml +++ b/hie-cabal.yaml @@ -9,3 +9,4 @@ cradle: - { path: "./kore/app/parser", component: "kore:kore-parser" } - { path: "./kore/app/prof", component: "kore:kore-prof" } - { path: "./kore/app/repl", component: "kore:kore-repl" } + - { path: "./kore/app/match-disjunction", component: "kore:kore-match-disjunction" } diff --git a/hie-stack.yaml b/hie-stack.yaml index 354f821c56..5df287a357 100644 --- a/hie-stack.yaml +++ b/hie-stack.yaml @@ -9,3 +9,4 @@ cradle: - { path: "./kore/app/parser", component: "kore:kore-parser" } - { path: "./kore/app/prof", component: "kore:kore-prof" } - { path: "./kore/app/repl", component: "kore:kore-repl" } + - { path: "./kore/app/match-disjunction", component: "kore:kore-match-disjunction" } diff --git a/kore/Makefile b/kore/Makefile index 53229776a5..4e92234e36 100644 --- a/kore/Makefile +++ b/kore/Makefile @@ -46,6 +46,8 @@ ghcid: ghcid-repl: $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-repl --work-dir .stack-work-ghci" +ghcid-match: + $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-match-disjunction --work-dir .stack-work-ghci" # TODO(Vladimir): remove 'hyperlink-source' when we upgrade from lts-12.10 (8.4.3) hoogle-gen: diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index ff3b793d1d..6244d4d3aa 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -55,19 +55,11 @@ import Kore.Internal.MultiAnd ( ) import qualified Kore.Internal.MultiAnd as MultiAnd import qualified Kore.Internal.OrPattern as OrPattern -import Kore.Internal.Pattern ( - Conditional (..), - Pattern, - ) -import Kore.Internal.Predicate ( - makePredicate, - ) import Kore.Internal.TermLike ( TermLike, VariableName, mkSortVariable, mkTop, - pattern And_, ) import Kore.Log ( KoreLogOptions (..), @@ -91,10 +83,6 @@ import Kore.Log.WarnIfLowProductivity ( import qualified Kore.ModelChecker.Bounded as Bounded ( CheckResult (..), ) -import Kore.Parser ( - ParsedPattern, - parseKorePattern, - ) import Kore.Parser.ParserUtils ( readPositiveIntegral, ) @@ -161,7 +149,6 @@ import Options.SMT ( import Prelude.Kore import Pretty ( Doc, - Pretty (..), hPutDoc, putDoc, vsep, @@ -919,48 +906,12 @@ loadPattern mainModule (Just fileName) = mainPatternParseAndVerify mainModule fileName loadPattern _ Nothing = error "Missing: --pattern PATTERN_FILE" -{- | IO action that parses a kore pattern from a filename and prints timing - information. --} -mainPatternParse :: String -> Main ParsedPattern -mainPatternParse = mainParse parseKorePattern - renderResult :: KoreExecOptions -> Doc ann -> IO () renderResult KoreExecOptions{outputFileName} doc = case outputFileName of Nothing -> putDoc doc Just outputFile -> withFile outputFile WriteMode (`hPutDoc` doc) -{- | IO action that parses a kore pattern from a filename, verifies it, - converts it to a pure pattern, and prints timing information. --} -mainPatternParseAndVerify :: - VerifiedModule StepperAttributes -> - String -> - Main (TermLike VariableName) -mainPatternParseAndVerify indexedModule patternFileName = - mainPatternParse patternFileName >>= mainPatternVerify indexedModule - -mainParseSearchPattern :: - VerifiedModule StepperAttributes -> - String -> - Main (Pattern VariableName) -mainParseSearchPattern indexedModule patternFileName = do - purePattern <- mainPatternParseAndVerify indexedModule patternFileName - case purePattern of - And_ _ term predicateTerm -> - return - Conditional - { term - , predicate = - either - (error . show . pretty) - id - (makePredicate predicateTerm) - , substitution = mempty - } - _ -> error "Unexpected non-conjunctive pattern" - savedProofsModuleName :: ModuleName savedProofsModuleName = ModuleName diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs new file mode 100644 index 0000000000..61790aa531 --- /dev/null +++ b/kore/app/match-disjunction/Main.hs @@ -0,0 +1,192 @@ +module Main (main) where + +import GlobalMain +import Kore.Attribute.Symbol ( + StepperAttributes, + ) +import Kore.BugReport +import Kore.Exec (matchDisjunction) +import Kore.IndexedModule.IndexedModule ( + VerifiedModule, + ) +import Kore.Internal.Pattern (Pattern) +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.TermLike ( + pattern Or_, + ) +import Kore.Log ( + KoreLogOptions, + parseKoreLogOptions, + runKoreLog, + ) +import Kore.Rewrite.RewritingVariable ( + RewritingVariableName, + mkRewritingPattern, + ) +import Kore.Syntax.Module ( + ModuleName (..), + ) +import Kore.Unparser ( + unparse, + ) +import Options.Applicative ( + InfoMod, + Parser, + argument, + fullDesc, + header, + help, + long, + metavar, + progDesc, + str, + strOption, + ) +import Prelude.Kore +import Pretty +import System.Clock ( + Clock (..), + TimeSpec, + getTime, + ) +import System.Exit ( + exitWith, + ) +import System.IO ( + IOMode (WriteMode), + withFile, + ) + +exeName :: ExeName +exeName = ExeName "kore-match-disjunction" + +envName :: String +envName = "KORE_MATCH_DISJUNCTION_OPTS" + +data KoreMatchDisjunctionOptions = KoreMatchDisjunctionOptions + { -- | Name of file containing a definition to verify and use for execution + definitionFileName :: !FilePath + , -- | Name of file containing a disjunction to verify and use for matching + disjunctionFileName :: !FilePath + , -- | Name of file used to match with disjunction + matchFileName :: !FilePath + , -- | Name for file to contain the output pattern + outputFileName :: !(Maybe FilePath) + , -- | The name of the main module in the definition + mainModuleName :: !ModuleName + , bugReportOption :: !BugReportOption + , koreLogOptions :: !KoreLogOptions + } + +parseKoreMatchDisjunctionOptions :: TimeSpec -> Parser KoreMatchDisjunctionOptions +parseKoreMatchDisjunctionOptions startTime = + KoreMatchDisjunctionOptions + <$> argument + str + ( metavar "DEFINITION_FILE" + <> help "Kore definition file to verify and use for execution." + ) + <*> strOption + ( metavar "DISJUNCTION_FILE" + <> long "disjunction" + <> help "File containing a disjunction of concrete terms." + ) + <*> strOption + ( metavar "MATCH_FILE" + <> long "match" + <> help "Kore source file representing pattern to search for." + ) + <*> optional + ( strOption + ( metavar "PATTERN_OUTPUT_FILE" + <> long "output" + <> help "Output file to contain final Kore pattern." + ) + ) + <*> parseMainModuleName + <*> parseBugReportOption + <*> parseKoreLogOptions exeName startTime + where + parseMainModuleName = + GlobalMain.parseModuleName + "MODULE" + "module" + "The name of the main module in the Kore definition." + +parserInfoModifiers :: InfoMod options +parserInfoModifiers = + fullDesc + <> progDesc "Matches Kore pattern in MATCH_FILE with Kore pattern in DISJUNCTION_FILE" + <> header "kore-match-disjunction - a tool for applying search patterns to disjunctions of configurations" + +main :: IO () +main = do + startTime <- getTime Monotonic + options <- + mainGlobal + exeName + (Just envName) + (parseKoreMatchDisjunctionOptions startTime) + parserInfoModifiers + for_ (localOptions options) mainWithOptions + +mainWithOptions :: KoreMatchDisjunctionOptions -> IO () +mainWithOptions options = do + exitCode <- + withBugReport exeName bugReportOption $ \tmpDir -> + koreMatchDisjunction options + & runKoreLog tmpDir koreLogOptions + exitWith exitCode + where + KoreMatchDisjunctionOptions{bugReportOption} = options + KoreMatchDisjunctionOptions{koreLogOptions} = options + +koreMatchDisjunction :: KoreMatchDisjunctionOptions -> Main ExitCode +koreMatchDisjunction options = do + definition <- loadDefinitions [definitionFileName] + mainModule <- loadModule mainModuleName definition + matchPattern <- mainParseMatchPattern mainModule matchFileName + disjunctionPattern <- + mainParseDisjunctionPattern mainModule disjunctionFileName + final <- + clockSomethingIO "Executing" $ + matchDisjunction mainModule matchPattern disjunctionPattern + lift $ + renderResult + options + (unparse final) + return ExitSuccess + where + mainParseMatchPattern mainModule fileName = + mainParseSearchPattern mainModule fileName + <&> mkRewritingPattern + KoreMatchDisjunctionOptions + { definitionFileName + , disjunctionFileName + , matchFileName + , mainModuleName + } = options + +mainParseDisjunctionPattern :: + VerifiedModule StepperAttributes -> + String -> + Main [Pattern RewritingVariableName] +mainParseDisjunctionPattern indexedModule patternFileName = do + purePattern <- mainPatternParseAndVerify indexedModule patternFileName + return $ parseDisjunction purePattern + where + parseDisjunction (Or_ _ term1 term2) = + parseDisjunction term1 <> parseDisjunction term2 + parseDisjunction term = + let patt = + mkRewritingPattern + . Pattern.fromTermLike + $ term + in [patt] + +renderResult :: KoreMatchDisjunctionOptions -> Doc ann -> IO () +renderResult KoreMatchDisjunctionOptions{outputFileName} doc = + case outputFileName of + Nothing -> putDoc doc + Just outputFile -> + withFile outputFile WriteMode (`hPutDoc` doc) diff --git a/kore/app/share/GlobalMain.hs b/kore/app/share/GlobalMain.hs index 8b13e9d11c..41cc1a5659 100644 --- a/kore/app/share/GlobalMain.hs +++ b/kore/app/share/GlobalMain.hs @@ -22,6 +22,8 @@ module GlobalMain ( LoadedModule, loadDefinitions, loadModule, + mainParseSearchPattern, + mainPatternParseAndVerify, ) where import Control.Exception ( @@ -58,6 +60,9 @@ import Kore.Attribute.Definition ( import Kore.Attribute.SourceLocation ( notDefault, ) +import Kore.Attribute.Symbol ( + StepperAttributes, + ) import qualified Kore.Attribute.Symbol as Attribute ( Symbol, ) @@ -65,6 +70,10 @@ import qualified Kore.Builtin as Builtin import Kore.IndexedModule.IndexedModule ( VerifiedModule, ) +import Kore.Internal.Conditional (Conditional (..)) +import Kore.Internal.Pattern (Pattern) +import Kore.Internal.Predicate (makePredicate) +import Kore.Internal.TermLike (TermLike, pattern And_) import Kore.Log as Log import Kore.Log.ErrorParse ( errorParse, @@ -75,6 +84,7 @@ import Kore.Log.ErrorVerify ( import Kore.Parser ( ParsedPattern, parseKoreDefinition, + parseKorePattern, ) import qualified Kore.Parser.Lexer as Lexer import Kore.Parser.ParserUtils ( @@ -83,7 +93,7 @@ import Kore.Parser.ParserUtils ( import Kore.Rewrite.Strategy ( GraphSearchOrder (..), ) -import Kore.Syntax +import Kore.Syntax hiding (Pattern) import Kore.Syntax.Definition ( ModuleName (..), ParsedDefinition, @@ -130,6 +140,7 @@ import qualified Paths_kore as MetaData ( version, ) import Prelude.Kore +import qualified Pretty as KorePretty import System.Clock ( Clock (Monotonic), diffTimeSpec, @@ -513,3 +524,39 @@ loadDefinitions filePaths = loadModule :: ModuleName -> LoadedDefinition -> Main LoadedModule loadModule moduleName = lookupMainModule moduleName . indexedModules + +mainParseSearchPattern :: + VerifiedModule StepperAttributes -> + String -> + Main (Pattern VariableName) +mainParseSearchPattern indexedModule patternFileName = do + purePattern <- mainPatternParseAndVerify indexedModule patternFileName + case purePattern of + And_ _ term predicateTerm -> + return + Conditional + { term + , predicate = + either + (error . show . KorePretty.pretty) + id + (makePredicate predicateTerm) + , substitution = mempty + } + _ -> error "Unexpected non-conjunctive pattern" + +{- | IO action that parses a kore pattern from a filename, verifies it, + converts it to a pure pattern, and prints timing information. +-} +mainPatternParseAndVerify :: + VerifiedModule StepperAttributes -> + String -> + Main (TermLike VariableName) +mainPatternParseAndVerify indexedModule patternFileName = + mainPatternParse patternFileName >>= mainPatternVerify indexedModule + +{- | IO action that parses a kore pattern from a filename and prints timing + information. +-} +mainPatternParse :: String -> Main ParsedPattern +mainPatternParse = mainParse parseKorePattern diff --git a/kore/kore.cabal b/kore/kore.cabal index 013f2b0296..7b61204416 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -589,6 +589,14 @@ executable kore-repl build-depends: exceptions >=0.10 build-depends: reflection >=2.1 +executable kore-match-disjunction + import: haskell + import: exe + import: global-main + main-is: Main.hs + hs-source-dirs: app/match-disjunction + build-depends: transformers >= 0.5 + test-suite kore-test import: haskell import: library diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index b5f19225cb..ef60a42029 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -16,6 +16,7 @@ module Kore.Exec ( prove, proveWithRepl, boundedModelCheck, + matchDisjunction, Rewrite, Equality, ) where @@ -39,6 +40,7 @@ import Control.Monad.Trans.Except ( runExceptT, throwE, ) +import Control.Monad.Trans.Maybe (runMaybeT) import Data.Coerce ( coerce, ) @@ -60,6 +62,7 @@ import Kore.Attribute.Definition import Kore.Attribute.Symbol ( StepperAttributes, ) +import qualified Kore.Attribute.Symbol as Attribute import qualified Kore.Builtin as Builtin import Kore.Equation ( Equation, @@ -89,6 +92,7 @@ import Kore.Internal.Predicate ( fromPredicate_, makeMultipleOrPredicate, ) +import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike import Kore.Log.ErrorRewriteLoop ( @@ -174,6 +178,7 @@ import Kore.Unparser ( unparseToText2, ) import Log ( + LoggerT, MonadLog, ) import qualified Log @@ -187,6 +192,7 @@ import Prof import SMT ( MonadSMT, SMT, + runNoSMT, ) import System.Exit ( ExitCode (..), @@ -574,6 +580,29 @@ boundedModelCheck breadthLimit depthLimit definitionModule specModule searchOrde searchOrder (head claims, depthLimit) +matchDisjunction :: + VerifiedModule Attribute.Symbol -> + Pattern RewritingVariableName -> + [Pattern RewritingVariableName] -> + LoggerT IO (TermLike VariableName) +matchDisjunction mainModule matchPattern disjunctionPattern = + do + SMT.runNoSMT $ + evalSimplifier mainModule $ do + results <- + traverse (runMaybeT . match matchPattern) disjunctionPattern + <&> catMaybes + <&> concatMap toList + results + <&> Condition.toPredicate + & Predicate.makeMultipleOrPredicate + & Predicate.fromPredicate sort + & getRewritingTerm + & return + where + sort = Pattern.patternSort matchPattern + match = Search.matchWith SideCondition.top + -- | Rule merging mergeAllRules :: ( MonadLog smt diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs index 51fd7ddf05..2e9aaa1218 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -6,6 +6,7 @@ module Test.Kore.Exec ( test_searchExceedingBreadthLimit, test_execGetExitCode, test_execDepthLimitExceeded, + test_matchDisjunction, ) where import Control.Exception as Exception @@ -75,6 +76,7 @@ import Kore.Validate.DefinitionVerifier ( import qualified Kore.Verified as Verified import Log ( Entry (..), + runLoggerT, ) import Prelude.Kore import System.Exit ( @@ -161,6 +163,99 @@ test_execDepthLimitExceeded = testCase "exec exceeds depth limit" $ } inputPattern = applyToNoArgs mySort "a" +test_matchDisjunction :: [TestTree] +test_matchDisjunction = + [ testCase "match disjunction" $ + do + let actual = + matchDisjunction verifiedModule initial [final1, final2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 1" $ + do + let actual = + matchDisjunction + verifiedModule + unreachable + [final1, final2, next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 2" $ + do + let actual = + matchDisjunction + verifiedModule + initial + [final1, final2, next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 3" $ + do + let actual = + matchDisjunction verifiedModule unreachable [final1, final2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 4" $ + do + let actual = + matchDisjunction verifiedModule initial [next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 5" $ + do + let actual = + matchDisjunction verifiedModule unreachable [next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - bottom 6" $ + do + let actual = + matchDisjunction + verifiedModule + unreachable + [final1, final2, initial, next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + , testCase "match disjunction - top" $ + do + let actual = + matchDisjunction + verifiedModule + initial + [final1, final2, initial, next1, next2] + result <- runLoggerT actual mempty + assertEqual "" (mkTop mySort) result + ] + where + -- these tests are inspired by the "search" integration test + verifiedModule = + verifiedMyModule + Module + { moduleName = ModuleName "MY-MODULE" + , moduleSentences = + [ asSentence mySortDecl + , asSentence $ constructorDecl "initial" + , asSentence $ constructorDecl "next1" + , asSentence $ constructorDecl "next2" + , asSentence $ constructorDecl "final1" + , asSentence $ constructorDecl "final2" + , asSentence $ constructorDecl "unreachable" + , functionalAxiom "initial" + , functionalAxiom "next1" + , functionalAxiom "next2" + , functionalAxiom "final1" + , functionalAxiom "final2" + , functionalAxiom "unreachable" + ] + , moduleAttributes = Attributes [] + } + initial = fromTermLike $ applyToNoArgs mySort "initial" + next1 = fromTermLike $ applyToNoArgs mySort "next1" + next2 = fromTermLike $ applyToNoArgs mySort "next2" + final1 = fromTermLike $ applyToNoArgs mySort "final1" + final2 = fromTermLike $ applyToNoArgs mySort "final2" + unreachable = fromTermLike $ applyToNoArgs mySort "unreachable" + test_exec :: TestTree test_exec = testCase "exec" $ actual >>= assertEqual "" expected where @@ -543,7 +638,8 @@ axiomWithAttribute attribute axiom = where currentAttributes = sentenceAxiomAttributes axiom -applyAliasToNoArgs :: Sort -> Text -> TermLike VariableName +applyAliasToNoArgs :: + InternalVariable variable => Sort -> Text -> TermLike variable applyAliasToNoArgs sort name = mkApplyAlias Alias @@ -555,7 +651,7 @@ applyAliasToNoArgs sort name = } [] -applyToNoArgs :: Sort -> Text -> TermLike VariableName +applyToNoArgs :: InternalVariable variable => Sort -> Text -> TermLike variable applyToNoArgs sort name = mkApplySymbol Symbol diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index 4734b37feb..90e3b4661b 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -571,6 +571,28 @@ "" ]; }; + "kore-match-disjunction" = { + depends = [ + (hsPkgs."base" or (errorHandler.buildDepError "base")) + (hsPkgs."kore" or (errorHandler.buildDepError "kore")) + (hsPkgs."clock" or (errorHandler.buildDepError "clock")) + (hsPkgs."containers" or (errorHandler.buildDepError "containers")) + (hsPkgs."filepath" or (errorHandler.buildDepError "filepath")) + (hsPkgs."lens" or (errorHandler.buildDepError "lens")) + (hsPkgs."megaparsec" or (errorHandler.buildDepError "megaparsec")) + (hsPkgs."optparse-applicative" or (errorHandler.buildDepError "optparse-applicative")) + (hsPkgs."text" or (errorHandler.buildDepError "text")) + (hsPkgs."transformers" or (errorHandler.buildDepError "transformers")) + ]; + buildable = true; + modules = [ "GlobalMain" "Paths_kore" ]; + hsSourceDirs = [ "app/share" "app/match-disjunction" ]; + mainPath = (([ + "Main.hs" + ] ++ (pkgs.lib).optional (compiler.isGhc && (compiler.version).ge "8.4") "") ++ (pkgs.lib).optional (compiler.isGhc && (compiler.version).ge "8.8") "") ++ [ + "" + ]; + }; }; tests = { "kore-test" = {