Symbolic execution and search should apply rules correctly (#2234)

Author: ana-pantilie

kore/app/exec/Main.hs

@@ -56,6 +56,7 @@ import Options.Applicative
     , value
     )
 import qualified Options.Applicative as Options
+import qualified Options.Applicative.Help.Pretty as OptPretty
 import System.Clock
     ( Clock (Monotonic)
     , TimeSpec
@@ -82,7 +83,6 @@ import System.IO
     , withFile
     )
 
-import qualified Data.Limit as Limit
 import Kore.Attribute.Symbol as Attribute
 import Kore.BugReport
 import Kore.Exec
@@ -148,9 +148,6 @@ import Kore.Reachability
 import qualified Kore.Reachability.Claim as Claim
 import Kore.Rewriting.RewritingVariable
 import Kore.Step
-import Kore.Step.RulePattern
-    ( RewriteRule
-    )
 import Kore.Step.Search
     ( SearchType (..)
     )
@@ -268,9 +265,6 @@ applyKoreSearchOptions Nothing koreExecOpts = koreExecOpts
 applyKoreSearchOptions koreSearchOptions@(Just koreSearchOpts) koreExecOpts =
     koreExecOpts
         { koreSearchOptions
-        , strategy =
-            -- Search relies on exploring the entire space of states.
-            ("all", priorityAllStrategy)
         , depthLimit = min depthLimit searchTypeDepthLimit
         }
   where
@@ -293,7 +287,7 @@ data KoreExecOptions = KoreExecOptions
     -- ^ The name of the main module in the definition
     , breadthLimit        :: !(Limit Natural)
     , depthLimit          :: !(Limit Natural)
-    , strategy            :: !(String, [RewriteRule RewritingVariableName] -> Strategy (Prim (RewriteRule RewritingVariableName)))
+    , strategy            :: !ExecutionMode
     , koreSolverOptions   :: !KoreSolverOptions
     , koreLogOptions      :: !KoreLogOptions
     , koreSearchOptions   :: !(Maybe KoreSearchOptions)
@@ -346,17 +340,12 @@ parseKoreExecOptions startTime =
     parseBreadthLimit = Limit <$> breadth <|> pure Unlimited
     parseDepthLimit = Limit <$> depth <|> pure Unlimited
     parseStrategy =
-        option (readSum "strategy" strategies)
+        option parseExecutionMode
             (  metavar "STRATEGY"
             <> long "strategy"
-            <> value ("all", priorityAllStrategy)
+            <> value All
             <> help "Select rewrites using STRATEGY."
             )
-      where
-        strategies =
-            [ ("any", priorityAnyStrategy)
-            , ("all", priorityAllStrategy)
-            ]
 
     breadth =
         option auto
@@ -384,6 +373,20 @@ parseKoreExecOptions startTime =
             , long "rts-statistics"
             , help "Write runtime statistics to FILENAME in JSON format."
             ]
+    parseExecutionMode = do
+        val <- str
+        case val :: String of
+            "all" -> return All
+            "any" -> return Any
+            _ ->
+                readerError
+                $ show
+                $ OptPretty.hsep
+                    [ "Unknown option"
+                    , OptPretty.squotes (OptPretty.text val)
+                        <> OptPretty.dot
+                    , "Known options are 'all' and 'any'."
+                    ]
 
 -- | modifiers for the Command line parser description
 parserInfoModifiers :: InfoMod options
@@ -462,7 +465,7 @@ koreExecSh
                 <$> maybeLimit Nothing Just breadthLimit
             , (\limit -> unwords ["--depth", show limit])
                 <$> maybeLimit Nothing Just depthLimit
-            , pure $ unwords ["--strategy", fst strategy]
+            , pure $ unwords ["--strategy", unparseExecutionMode strategy]
             , rtsStatistics $>
                 unwords ["--rts-statistics", defaultRtsStatisticsFilePath]
             ]
@@ -472,6 +475,8 @@ koreExecSh
         , maybe mempty unparseKoreProveOptions koreProveOptions
         , maybe mempty unparseKoreMergeOptions koreMergeOptions
         ]
+    unparseExecutionMode All = "all"
+    unparseExecutionMode Any = "any"
 
 defaultDefinitionFilePath :: KoreExecOptions -> FilePath
 defaultDefinitionFilePath KoreExecOptions { koreProveOptions }
@@ -615,14 +620,13 @@ koreSearch execOptions searchOptions = do
     initial <- loadPattern mainModule patternFileName
     final <-
         execute execOptions mainModule
-        $ search breadthLimit mainModule strategy' initial target config
+        $ search depthLimit breadthLimit mainModule initial target config
     lift $ renderResult execOptions (unparse final)
     return ExitSuccess
   where
     KoreSearchOptions { bound, searchType } = searchOptions
     config = Search.Config { bound, searchType }
-    KoreExecOptions { breadthLimit, depthLimit, strategy } = execOptions
-    strategy' = Limit.replicate depthLimit . snd strategy
+    KoreExecOptions { breadthLimit, depthLimit } = execOptions
 
 koreRun :: KoreExecOptions -> Main ExitCode
 koreRun execOptions = do
@@ -634,12 +638,11 @@ koreRun execOptions = do
     initial <- loadPattern mainModule patternFileName
     (exitCode, final) <-
         execute execOptions mainModule
-        $ exec breadthLimit mainModule strategy' initial
+        $ exec depthLimit breadthLimit mainModule strategy initial
     lift $ renderResult execOptions (unparse final)
     return exitCode
   where
     KoreExecOptions { breadthLimit, depthLimit, strategy } = execOptions
-    strategy' = Limit.replicate depthLimit . snd strategy
 
 koreProve :: KoreExecOptions -> KoreProveOptions -> Main ExitCode
 koreProve execOptions proveOptions = do

kore/src/Kore/Exec.hs

@@ -81,9 +81,6 @@ import Kore.IndexedModule.Resolvers
     ( resolveInternalSymbol
     )
 import qualified Kore.Internal.Condition as Condition
-import Kore.Internal.MultiOr
-    ( make
-    )
 import qualified Kore.Internal.MultiOr as MultiOr
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
@@ -160,7 +157,6 @@ import Kore.Step.Search
 import qualified Kore.Step.Search as Search
 import Kore.Step.Simplification.Data
     ( MonadProf
-    , SimplifierT
     , evalSimplifier
     )
 import qualified Kore.Step.Simplification.Data as Simplifier
@@ -213,14 +209,14 @@ exec
         , MonadProf smt
         )
     => Limit Natural
+    -> Limit Natural
     -> VerifiedModule StepperAttributes
     -- ^ The main module
-    -> ([Rewrite] -> [Strategy (Prim Rewrite)])
-    -- ^ The strategy to use for execution; see examples in "Kore.Step.Step"
+    -> ExecutionMode
     -> TermLike VariableName
     -- ^ The input pattern
     -> smt (ExitCode, TermLike VariableName)
-exec breadthLimit verifiedModule strategy initialTerm =
+exec depthLimit breadthLimit verifiedModule strategy initialTerm =
     evalSimplifier verifiedModule' $ do
         initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
@@ -237,9 +233,10 @@ exec breadthLimit verifiedModule strategy initialTerm =
                             . Strategy.applyBreadthLimit
                                 breadthLimit
                                 dropStrategy
+                    rewriteGroups = groupRewritesByPriority rewriteRules
                     transit instr config =
                         Strategy.transitionRule
-                            (transitionRule & trackExecDepth)
+                            (transitionRule rewriteGroups strategy & trackExecDepth)
                             instr
                             config
                         & runTransitionT
@@ -248,24 +245,21 @@ exec breadthLimit verifiedModule strategy initialTerm =
                 Strategy.leavesM
                     updateQueue
                     (Strategy.unfoldTransition transit)
-                    ( strategy rewriteRules
-                    , (ExecDepth 0, mkRewritingPattern initialConfig)
+                    ( limitedExecutionStrategy depthLimit
+                    , (ExecDepth 0, Start (mkRewritingPattern initialConfig))
                     )
         let (depths, finalConfigs) = unzip finals
         infoExecDepth (maximum depths)
-        let finalConfigs' = make $ getRewritingPattern <$> finalConfigs
+        let finalConfigs' =
+                MultiOr.make
+                $ getRewritingPattern
+                . extractProgramState
+                <$> finalConfigs
         exitCode <- getExitCode verifiedModule finalConfigs'
         let finalTerm = forceSort initialSort $ OrPattern.toTermLike finalConfigs'
         return (exitCode, finalTerm)
   where
     dropStrategy = snd
-    getFinalConfigsOf
-        :: LogicT
-            (SimplifierT smt)
-            ( [Strategy (Prim (RewriteRule RewritingVariableName))]
-            , (ExecDepth, Pattern RewritingVariableName)
-            )
-        -> SimplifierT smt [(ExecDepth, Pattern RewritingVariableName)]
     getFinalConfigsOf act = observeAllT $ fmap snd act
     verifiedModule' =
         IndexedModule.mapPatterns
@@ -290,8 +284,8 @@ trackExecDepth transit prim (execDepth, execState) = do
   where
     didRewrite _ = isRewrite prim
 
-    isRewrite Simplify = False
-    isRewrite (Rewrite _) = True
+    isRewrite Rewrite = True
+    isRewrite _ = False
 
 -- | Project the value of the exit cell, if it is present.
 getExitCode
@@ -341,18 +335,17 @@ search
         , MonadProf smt
         )
     => Limit Natural
+    -> Limit Natural
     -> VerifiedModule StepperAttributes
     -- ^ The main module
-    -> ([Rewrite] -> [Strategy (Prim Rewrite)])
-    -- ^ The strategy to use for execution; see examples in "Kore.Step.Step"
     -> TermLike VariableName
     -- ^ The input pattern
     -> Pattern VariableName
     -- ^ The pattern to match during execution
     -> Search.Config
     -- ^ The bound on the number of search matches and the search type
     -> smt (TermLike VariableName)
-search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
+search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfig
   =
     evalSimplifier verifiedModule $ do
         initialized <- initializeAndSimplify verifiedModule
@@ -365,15 +358,30 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
                 case toList simplifiedPatterns of
                     [] -> Pattern.bottomOf (termLikeSort termLike)
                     (config : _) -> config
+            rewriteGroups =
+                groupRewritesByPriority rewriteRules
             runStrategy' =
-                runStrategy breadthLimit transitionRule (strategy rewriteRules)
-        executionGraph <- runStrategy' (mkRewritingPattern initialPattern)
+                runStrategy
+                    breadthLimit
+                    -- search relies on exploring
+                    -- the entire space of states.
+                    (transitionRule rewriteGroups All)
+                    (limitedExecutionStrategy depthLimit)
+        executionGraph <-
+            runStrategy' (Start $ mkRewritingPattern initialPattern)
         let
-            match target config = Search.matchWith target config
+            match target config1 config2 =
+                Search.matchWith
+                    target
+                    config1
+                    (extractProgramState config2)
         solutionsLists <-
             searchGraph
                 searchConfig
-                (match SideCondition.topTODO (mkRewritingPattern searchPattern))
+                (match
+                    SideCondition.topTODO
+                    (mkRewritingPattern searchPattern)
+                )
                 executionGraph
         let
             solutions = concatMap toList solutionsLists
@@ -387,7 +395,6 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
   where
     patternSort = termLikeSort termLike
 
-
 -- | Proving a spec given as a module containing rules to be proven
 prove
     ::  forall smt