From af0b7e52dfbcd06417ea83c11cfd74f5e806509d Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 23 Jun 2021 16:48:48 +0300 Subject: [PATCH 01/14] WIP: kore-match-disjunction tool --- kore/app/match-disjunction/Main.hs | 66 ++++++++++++++++++++++++++++++ kore/kore.cabal | 7 ++++ 2 files changed, 73 insertions(+) create mode 100644 kore/app/match-disjunction/Main.hs diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs new file mode 100644 index 0000000000..9f24784892 --- /dev/null +++ b/kore/app/match-disjunction/Main.hs @@ -0,0 +1,66 @@ +module Main (main) where + +import Prelude.Kore +import GlobalMain (mainGlobal, ExeName (..)) + +exeName :: ExeName +exeName = ExeName "kore-match-disjunction" + +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 + } + +parseKoreMatchDisjunctionOptions :: Parser KoreMatchDisjunctionOptions +parseKoreMatchDisjunctionOptions = + KoreMatchDisjunctionOptions + <$> argument + str + ( metavar "DEFINITION_FILE" + <> help "Kore definition file to verify and use for execution" + ) + <*> strOption + ( metavar "DISJUNCTION_FILE" + <> long "disjunction" + <> help "TODO" + ) + <*> strOption + ( metavar "MATCH_FILE" + <> long "match" + <> help "TODO" + ) + <*> optional + ( strOption + ( metavar "PATTERN_OUTPUT_FILE" + <> long "output" + <> help "Output file to contain final Kore pattern." + ) + ) + <*> parseMainModuleName + where + parseMainModuleName = + GlobalMain.parseModuleName + "MODULE" + "module" + "The name of the main module in the Kore definition." + + +main :: IO () +main = do + options <- + mainGlobal + exeName + Nothing + undefined -- parseKoreMatchDisjunctionOptions + undefined -- parserInfoModifiers + undefined + diff --git a/kore/kore.cabal b/kore/kore.cabal index a00365abd7..bb9f8655e0 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -584,6 +584,13 @@ 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 + test-suite kore-test import: haskell import: library From 4d93128290793004178001fc120afcfdfe319edc Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 24 Jun 2021 09:38:45 +0300 Subject: [PATCH 02/14] General structure of new tool --- kore/app/match-disjunction/Main.hs | 82 +++++++++++++++++++++++++++--- kore/app/share/GlobalMain.hs | 52 ++++++++++++++++++- 2 files changed, 127 insertions(+), 7 deletions(-) diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs index 9f24784892..841bddd0ba 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/kore/app/match-disjunction/Main.hs @@ -1,11 +1,29 @@ module Main (main) where import Prelude.Kore -import GlobalMain (mainGlobal, ExeName (..)) +import System.Clock (TimeSpec, getTime, Clock (..)) +import Kore.Log (runKoreLog, KoreLogOptions, parseKoreLogOptions) +import Kore.BugReport +import GlobalMain +import Kore.Internal.TermLike (pattern Or_, VariableName) +import Kore.Internal.Pattern (Pattern) +import Kore.Attribute.Symbol ( + StepperAttributes, + ) +import Kore.IndexedModule.IndexedModule ( + VerifiedModule, + ) +import Kore.Syntax.Module (ModuleName (..)) +import Options.Applicative (Parser, argument, str, metavar, help, strOption, long, InfoMod, fullDesc, progDesc, header) +import qualified GlobalMain +import System.Exit (ExitCode, exitWith) 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 @@ -18,10 +36,12 @@ data KoreMatchDisjunctionOptions = outputFileName :: !(Maybe FilePath) , -- | The name of the main module in the definition mainModuleName :: !ModuleName + , bugReportOption :: !BugReportOption + , koreLogOptions :: !KoreLogOptions } -parseKoreMatchDisjunctionOptions :: Parser KoreMatchDisjunctionOptions -parseKoreMatchDisjunctionOptions = +parseKoreMatchDisjunctionOptions :: TimeSpec -> Parser KoreMatchDisjunctionOptions +parseKoreMatchDisjunctionOptions startTime = KoreMatchDisjunctionOptions <$> argument str @@ -46,21 +66,71 @@ parseKoreMatchDisjunctionOptions = ) ) <*> parseMainModuleName + <*> parseBugReportOption + <*> parseKoreLogOptions exeName startTime where + -- TODO: factor this out in GlobalMain? 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 - TODO" main :: IO () main = do + startTime <- getTime Monotonic options <- mainGlobal exeName - Nothing - undefined -- parseKoreMatchDisjunctionOptions - undefined -- parserInfoModifiers + (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 + -- TODO: do we wanna do some simplification of the disjunction + -- pattern, since the simplifier will return a list of patterns, + -- and then we can match on this? + disjunctionPattern <- + mainParseDisjunctionPattern mainModule disjunctionFileName undefined + where + mainParseMatchPattern = mainParseSearchPattern + KoreMatchDisjunctionOptions + { definitionFileName + , disjunctionFileName + , matchFileName + , outputFileName + , mainModuleName + } = options +mainParseDisjunctionPattern :: + VerifiedModule StepperAttributes -> + String -> + Main [Pattern VariableName] +mainParseDisjunctionPattern indexedModule patternFileName = do + purePattern <- mainPatternParseAndVerify indexedModule patternFileName + return $ parseDisjunction purePattern + where + parseDisjunction = undefined diff --git a/kore/app/share/GlobalMain.hs b/kore/app/share/GlobalMain.hs index a70b9660f1..91dbdb251f 100644 --- a/kore/app/share/GlobalMain.hs +++ b/kore/app/share/GlobalMain.hs @@ -22,20 +22,34 @@ module GlobalMain ( LoadedModule, loadDefinitions, loadModule, + mainParseSearchPattern, + mainPatternParseAndVerify ) where import Control.Exception ( evaluate, ) +import Kore.Internal.Predicate (makePredicate) +import Kore.Parser ( + ParsedPattern, + parseKorePattern, + ) +import Kore.Attribute.Symbol ( + StepperAttributes, + ) import Control.Lens ( (%~), ) import qualified Control.Lens as Lens import qualified Control.Monad as Monad +import qualified Pretty as KorePretty import Data.List ( intercalate, nub, ) +import Kore.Internal.TermLike (pattern And_, TermLike) +import Kore.Internal.Conditional (Conditional (..)) +import Kore.Internal.Pattern (Pattern) import Data.Map.Strict ( Map, ) @@ -88,7 +102,7 @@ import Kore.Parser.ParserUtils ( import Kore.Step.Strategy ( GraphSearchOrder (..), ) -import Kore.Syntax +import Kore.Syntax hiding (Pattern) import Kore.Syntax.Definition ( ModuleName (..), ParsedDefinition, @@ -513,3 +527,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 From b645ddaee70fcc200f10a2c13417f15edea13517 Mon Sep 17 00:00:00 2001 From: github-actions Date: Thu, 24 Jun 2021 06:40:52 +0000 Subject: [PATCH 03/14] Format with fourmolu --- kore/app/match-disjunction/Main.hs | 51 +++++++++++++++--------------- kore/app/share/GlobalMain.hs | 23 ++++++-------- 2 files changed, 35 insertions(+), 39 deletions(-) diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs index 841bddd0ba..d6073f7de0 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/kore/app/match-disjunction/Main.hs @@ -1,21 +1,21 @@ module Main (main) where -import Prelude.Kore -import System.Clock (TimeSpec, getTime, Clock (..)) -import Kore.Log (runKoreLog, KoreLogOptions, parseKoreLogOptions) -import Kore.BugReport import GlobalMain -import Kore.Internal.TermLike (pattern Or_, VariableName) -import Kore.Internal.Pattern (Pattern) +import qualified GlobalMain import Kore.Attribute.Symbol ( StepperAttributes, ) +import Kore.BugReport import Kore.IndexedModule.IndexedModule ( VerifiedModule, ) +import Kore.Internal.Pattern (Pattern) +import Kore.Internal.TermLike (VariableName, pattern Or_) +import Kore.Log (KoreLogOptions, parseKoreLogOptions, runKoreLog) import Kore.Syntax.Module (ModuleName (..)) -import Options.Applicative (Parser, argument, str, metavar, help, strOption, long, InfoMod, fullDesc, progDesc, header) -import qualified GlobalMain +import Options.Applicative (InfoMod, Parser, argument, fullDesc, header, help, long, metavar, progDesc, str, strOption) +import Prelude.Kore +import System.Clock (Clock (..), TimeSpec, getTime) import System.Exit (ExitCode, exitWith) exeName :: ExeName @@ -24,21 +24,20 @@ 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 - } +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 = @@ -98,11 +97,11 @@ mainWithOptions options = do exitCode <- withBugReport exeName bugReportOption $ \tmpDir -> koreMatchDisjunction options - & runKoreLog tmpDir koreLogOptions + & runKoreLog tmpDir koreLogOptions exitWith exitCode where - KoreMatchDisjunctionOptions { bugReportOption } = options - KoreMatchDisjunctionOptions { koreLogOptions } = options + KoreMatchDisjunctionOptions{bugReportOption} = options + KoreMatchDisjunctionOptions{koreLogOptions} = options koreMatchDisjunction :: KoreMatchDisjunctionOptions -> Main ExitCode koreMatchDisjunction options = do diff --git a/kore/app/share/GlobalMain.hs b/kore/app/share/GlobalMain.hs index 91dbdb251f..4b9ec5668e 100644 --- a/kore/app/share/GlobalMain.hs +++ b/kore/app/share/GlobalMain.hs @@ -23,33 +23,21 @@ module GlobalMain ( loadDefinitions, loadModule, mainParseSearchPattern, - mainPatternParseAndVerify + mainPatternParseAndVerify, ) where import Control.Exception ( evaluate, ) -import Kore.Internal.Predicate (makePredicate) -import Kore.Parser ( - ParsedPattern, - parseKorePattern, - ) -import Kore.Attribute.Symbol ( - StepperAttributes, - ) import Control.Lens ( (%~), ) import qualified Control.Lens as Lens import qualified Control.Monad as Monad -import qualified Pretty as KorePretty import Data.List ( intercalate, nub, ) -import Kore.Internal.TermLike (pattern And_, TermLike) -import Kore.Internal.Conditional (Conditional (..)) -import Kore.Internal.Pattern (Pattern) import Data.Map.Strict ( Map, ) @@ -77,6 +65,9 @@ import Kore.Attribute.Definition ( import Kore.Attribute.SourceLocation ( notDefault, ) +import Kore.Attribute.Symbol ( + StepperAttributes, + ) import qualified Kore.Attribute.Symbol as Attribute ( Symbol, ) @@ -84,6 +75,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, @@ -94,6 +89,7 @@ import Kore.Log.ErrorVerify ( import Kore.Parser ( ParsedPattern, parseKoreDefinition, + parseKorePattern, ) import qualified Kore.Parser.Lexer as Lexer import Kore.Parser.ParserUtils ( @@ -144,6 +140,7 @@ import qualified Paths_kore as MetaData ( version, ) import Prelude.Kore +import qualified Pretty as KorePretty import System.Clock ( Clock (Monotonic), diffTimeSpec, From 5b5a44ecdd0d730cc82b2e5e579562eab2b90d0c Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 29 Jun 2021 15:48:16 +0300 Subject: [PATCH 04/14] Implement kore-match-disjunction --- kore/app/match-disjunction/Main.hs | 109 +++++++++++++++++++++++++---- 1 file changed, 94 insertions(+), 15 deletions(-) diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs index d6073f7de0..016818494d 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/kore/app/match-disjunction/Main.hs @@ -1,7 +1,9 @@ module Main (main) where +import Control.Monad.Trans.Maybe ( + runMaybeT, + ) import GlobalMain -import qualified GlobalMain import Kore.Attribute.Symbol ( StepperAttributes, ) @@ -9,14 +11,62 @@ import Kore.BugReport import Kore.IndexedModule.IndexedModule ( VerifiedModule, ) +import qualified Kore.Internal.Condition as Condition import Kore.Internal.Pattern (Pattern) -import Kore.Internal.TermLike (VariableName, pattern Or_) -import Kore.Log (KoreLogOptions, parseKoreLogOptions, runKoreLog) -import Kore.Syntax.Module (ModuleName (..)) -import Options.Applicative (InfoMod, Parser, argument, fullDesc, header, help, long, metavar, progDesc, str, strOption) +import qualified Kore.Internal.Pattern as Pattern +import qualified Kore.Internal.Predicate as Predicate +import qualified Kore.Internal.SideCondition as SideCondition +import Kore.Internal.TermLike ( + pattern Or_, + ) +import Kore.Log ( + KoreLogOptions, + parseKoreLogOptions, + runKoreLog, + ) +import Kore.Rewriting.RewritingVariable ( + RewritingVariableName, + getRewritingTerm, + mkRewritingPattern, + ) +import qualified Kore.Step.Search as Search +import Kore.Step.Simplification.Data ( + evalSimplifier, + ) +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 System.Clock (Clock (..), TimeSpec, getTime) -import System.Exit (ExitCode, exitWith) +import Pretty +import qualified SMT +import System.Clock ( + Clock (..), + TimeSpec, + getTime, + ) +import System.Exit ( + exitWith, + ) +import System.IO ( + IOMode (WriteMode), + withFile, + ) exeName :: ExeName exeName = ExeName "kore-match-disjunction" @@ -108,28 +158,57 @@ koreMatchDisjunction options = do definition <- loadDefinitions [definitionFileName] mainModule <- loadModule mainModuleName definition matchPattern <- mainParseMatchPattern mainModule matchFileName - -- TODO: do we wanna do some simplification of the disjunction - -- pattern, since the simplifier will return a list of patterns, - -- and then we can match on this? disjunctionPattern <- mainParseDisjunctionPattern mainModule disjunctionFileName - undefined + let sort = Pattern.patternSort matchPattern + final <- + clockSomethingIO "Executing" $ + SMT.runNoSMT $ + evalSimplifier mainModule $ do + results <- + traverse (runMaybeT . match matchPattern) disjunctionPattern + <&> catMaybes + <&> concatMap toList + results + <&> Condition.toPredicate + & Predicate.makeMultipleOrPredicate + & Predicate.fromPredicate sort + & getRewritingTerm + & return + lift $ renderResult options (unparse final) + return ExitSuccess where - mainParseMatchPattern = mainParseSearchPattern + mainParseMatchPattern mainModule fileName = + mainParseSearchPattern mainModule fileName + <&> mkRewritingPattern + match = Search.matchWith SideCondition.top KoreMatchDisjunctionOptions { definitionFileName , disjunctionFileName , matchFileName - , outputFileName , mainModuleName } = options mainParseDisjunctionPattern :: VerifiedModule StepperAttributes -> String -> - Main [Pattern VariableName] + Main [Pattern RewritingVariableName] mainParseDisjunctionPattern indexedModule patternFileName = do purePattern <- mainPatternParseAndVerify indexedModule patternFileName return $ parseDisjunction purePattern where - parseDisjunction = undefined + 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) From 43ea6652c302a05ea9a2b214767af38e76f9e290 Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 29 Jun 2021 12:51:13 +0000 Subject: [PATCH 05/14] Materialize Nix expressions --- nix/kore.nix.d/kore.nix | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index 8bdf7381df..c35ccb8601 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -566,6 +566,27 @@ "" ]; }; + "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")) + ]; + 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" = { From ad4b9c84da931106d7628b182aff0db843c6a23f Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 29 Jun 2021 16:41:36 +0300 Subject: [PATCH 06/14] Clean-up kore-exec main --- kore/app/exec/Main.hs | 49 ------------------------------------------- 1 file changed, 49 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 0623cb2fd1..e6cd796616 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.Reachability ( ProveClaimsResult (..), SomeClaim, @@ -158,7 +146,6 @@ import Options.SMT ( import Prelude.Kore import Pretty ( Doc, - Pretty (..), hPutDoc, putDoc, vsep, @@ -902,48 +889,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 From f7d0aca1e046ec556da927aa158c1cd253f91eaa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Mon, 26 Jul 2021 13:01:26 +0300 Subject: [PATCH 07/14] Fix building and HLS processing --- hie-cabal.yaml | 1 + hie-stack.yaml | 1 + kore/kore.cabal | 1 + 3 files changed, 3 insertions(+) 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/kore.cabal b/kore/kore.cabal index bb9f8655e0..5e14a91194 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -590,6 +590,7 @@ executable kore-match-disjunction import: global-main main-is: Main.hs hs-source-dirs: app/match-disjunction + build-depends: transformers >= 0.5 test-suite kore-test import: haskell From 5dac97a1178dab5c0f83d5e2cced14e6377acc50 Mon Sep 17 00:00:00 2001 From: github-actions Date: Mon, 26 Jul 2021 11:37:33 +0000 Subject: [PATCH 08/14] Materialize Nix expressions --- nix/kore.nix.d/kore.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index c35ccb8601..1a5c5c28c2 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -577,6 +577,7 @@ (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" ]; From e0559ff294b6692d6ac738585e92c5fd918378d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Mon, 26 Jul 2021 15:26:39 +0300 Subject: [PATCH 09/14] Allow "make ghcid-match" --- kore/Makefile | 2 ++ 1 file changed, 2 insertions(+) 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: From 9815891ac20bd4b7773e4c4ca574d36768b9956f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Mon, 26 Jul 2021 15:53:59 +0300 Subject: [PATCH 10/14] Apply pedantic --- kore/app/exec/Main.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 0af1b80579..6244d4d3aa 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -83,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, ) From 32ca719ce9c83caed36ac48f5ec9ab2d8caf2227 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Mon, 26 Jul 2021 17:45:16 +0300 Subject: [PATCH 11/14] Add two trivial unit tests --- kore/app/match-disjunction/Main.hs | 33 +++++--------------------- kore/src/Kore/Exec.hs | 29 +++++++++++++++++++++++ kore/test/Test/Kore/Exec.hs | 37 ++++++++++++++++++++++++++++-- 3 files changed, 70 insertions(+), 29 deletions(-) diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs index f7d8331dc2..c49b3e4405 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/kore/app/match-disjunction/Main.hs @@ -1,21 +1,16 @@ module Main (main) where -import Control.Monad.Trans.Maybe ( - runMaybeT, - ) import GlobalMain import Kore.Attribute.Symbol ( StepperAttributes, ) import Kore.BugReport +import Kore.Exec (matchDisjunction) import Kore.IndexedModule.IndexedModule ( VerifiedModule, ) -import qualified Kore.Internal.Condition as Condition import Kore.Internal.Pattern (Pattern) import qualified Kore.Internal.Pattern as Pattern -import qualified Kore.Internal.Predicate as Predicate -import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike ( pattern Or_, ) @@ -26,13 +21,8 @@ import Kore.Log ( ) import Kore.Rewrite.RewritingVariable ( RewritingVariableName, - getRewritingTerm, mkRewritingPattern, ) -import qualified Kore.Rewrite.Search as Search -import Kore.Simplify.Data ( - evalSimplifier, - ) import Kore.Syntax.Module ( ModuleName (..), ) @@ -54,7 +44,6 @@ import Options.Applicative ( ) import Prelude.Kore import Pretty -import qualified SMT import System.Clock ( Clock (..), TimeSpec, @@ -160,28 +149,18 @@ koreMatchDisjunction options = do matchPattern <- mainParseMatchPattern mainModule matchFileName disjunctionPattern <- mainParseDisjunctionPattern mainModule disjunctionFileName - let sort = Pattern.patternSort matchPattern final <- clockSomethingIO "Executing" $ - SMT.runNoSMT $ - evalSimplifier mainModule $ do - results <- - traverse (runMaybeT . match matchPattern) disjunctionPattern - <&> catMaybes - <&> concatMap toList - results - <&> Condition.toPredicate - & Predicate.makeMultipleOrPredicate - & Predicate.fromPredicate sort - & getRewritingTerm - & return - lift $ renderResult options (unparse final) + matchDisjunction mainModule matchPattern disjunctionPattern + lift $ + renderResult + options + (unparse final) return ExitSuccess where mainParseMatchPattern mainModule fileName = mainParseSearchPattern mainModule fileName <&> mkRewritingPattern - match = Search.matchWith SideCondition.top KoreMatchDisjunctionOptions { definitionFileName , disjunctionFileName diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 41077790b9..a8f181cc78 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 a5afb61585..ae518a7b6d 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -5,6 +5,7 @@ module Test.Kore.Exec ( test_searchExceedingBreadthLimit, test_execGetExitCode, test_execDepthLimitExceeded, + test_matchDisjunction, ) where import Control.Exception as Exception @@ -74,6 +75,7 @@ import Kore.Validate.DefinitionVerifier ( import qualified Kore.Verified as Verified import Log ( Entry (..), + runLoggerT, ) import Prelude.Kore import System.Exit ( @@ -160,6 +162,36 @@ test_execDepthLimitExceeded = testCase "exec exceeds depth limit" $ } inputPattern = applyToNoArgs mySort "a" +test_matchDisjunction :: [TestTree] +test_matchDisjunction = + [ testCase "match disjunction" $ + do + let actual = matchDisjunction verifiedModule a [a] + result <- runLoggerT actual mempty + assertEqual "" (mkTop mySort) result + , testCase "match disjunction" $ + do + let actual = matchDisjunction verifiedModule a [b] + result <- runLoggerT actual mempty + assertEqual "" (mkBottom mySort) result + ] + where + verifiedModule = + verifiedMyModule + Module + { moduleName = ModuleName "MY-MODULE" + , moduleSentences = + [ asSentence mySortDecl + , asSentence $ constructorDecl "a" + , asSentence $ constructorDecl "b" + , functionalAxiom "a" + , functionalAxiom "b" + ] + , moduleAttributes = Attributes [] + } + a = fromTermLike $ applyToNoArgs mySort "a" + b = fromTermLike $ applyToNoArgs mySort "b" + test_exec :: TestTree test_exec = testCase "exec" $ actual >>= assertEqual "" expected where @@ -518,7 +550,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 @@ -530,7 +563,7 @@ applyAliasToNoArgs sort name = } [] -applyToNoArgs :: Sort -> Text -> TermLike VariableName +applyToNoArgs :: InternalVariable variable => Sort -> Text -> TermLike variable applyToNoArgs sort name = mkApplySymbol Symbol From 8c56ab724496ed3341af78fcc2e449b28b865e32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Tue, 3 Aug 2021 16:05:58 +0300 Subject: [PATCH 12/14] Add unit tests inspired by "search" integration test --- kore/test/Test/Kore/Exec.hs | 87 ++++++++++++++++++++++++++++++++----- 1 file changed, 77 insertions(+), 10 deletions(-) diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs index ae518a7b6d..463209e32b 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -166,31 +166,98 @@ test_matchDisjunction :: [TestTree] test_matchDisjunction = [ testCase "match disjunction" $ do - let actual = matchDisjunction verifiedModule a [a] + let actual = + matchDisjunction verifiedModule initial [final1, final2] result <- runLoggerT actual mempty - assertEqual "" (mkTop mySort) result - , testCase "match disjunction" $ + 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 a [b] + 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 "a" - , asSentence $ constructorDecl "b" - , functionalAxiom "a" - , functionalAxiom "b" + , 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" + -- , simpleRewriteAxiom "initial" "next1" + -- , simpleRewriteAxiom "initial" "next2" + -- , simpleRewriteAxiom "next1" "final1" + -- , simpleRewriteAxiom "next2" "final2" ] , moduleAttributes = Attributes [] } - a = fromTermLike $ applyToNoArgs mySort "a" - b = fromTermLike $ applyToNoArgs mySort "b" + 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 From 771d3848ea927474dd8f997a8d6e5324b2f16ea0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Wed, 4 Aug 2021 16:38:25 +0300 Subject: [PATCH 13/14] Remove comments --- kore/test/Test/Kore/Exec.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs index 463209e32b..881c20bc08 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -245,10 +245,6 @@ test_matchDisjunction = , functionalAxiom "final1" , functionalAxiom "final2" , functionalAxiom "unreachable" - -- , simpleRewriteAxiom "initial" "next1" - -- , simpleRewriteAxiom "initial" "next2" - -- , simpleRewriteAxiom "next1" "final1" - -- , simpleRewriteAxiom "next2" "final2" ] , moduleAttributes = Attributes [] } From 72d334600030649286c3a1f9fe0581b28e1a57e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Thu, 5 Aug 2021 14:44:29 +0300 Subject: [PATCH 14/14] Address or remove TODOs --- kore/app/match-disjunction/Main.hs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kore/app/match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs index c49b3e4405..61790aa531 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/kore/app/match-disjunction/Main.hs @@ -84,17 +84,17 @@ parseKoreMatchDisjunctionOptions startTime = <$> argument str ( metavar "DEFINITION_FILE" - <> help "Kore definition file to verify and use for execution" + <> help "Kore definition file to verify and use for execution." ) <*> strOption ( metavar "DISJUNCTION_FILE" <> long "disjunction" - <> help "TODO" + <> help "File containing a disjunction of concrete terms." ) <*> strOption ( metavar "MATCH_FILE" <> long "match" - <> help "TODO" + <> help "Kore source file representing pattern to search for." ) <*> optional ( strOption @@ -107,7 +107,6 @@ parseKoreMatchDisjunctionOptions startTime = <*> parseBugReportOption <*> parseKoreLogOptions exeName startTime where - -- TODO: factor this out in GlobalMain? parseMainModuleName = GlobalMain.parseModuleName "MODULE" @@ -118,7 +117,7 @@ parserInfoModifiers :: InfoMod options parserInfoModifiers = fullDesc <> progDesc "Matches Kore pattern in MATCH_FILE with Kore pattern in DISJUNCTION_FILE" - <> header "kore-match-disjunction - TODO" + <> header "kore-match-disjunction - a tool for applying search patterns to disjunctions of configurations" main :: IO () main = do