Return vacuous in kore-rpc when state goes to #bottom (#3637)

goodlyrottenapple · web-flow · commit be6592d784c1 · 2023-08-09T14:48:08.000+01:00
Another attempt at addressing runtimeverification/evm-semantics#1944. Addresses #3630 (needs a follow-up in booster) This change mimicks what kore-exe in prover mode returns(as introduced by #2451), namely the configuration goes to bottom
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
@@ -115,6 +115,7 @@ data ExecuteState = ExecuteState
 data HaltReason
     = Branching
     | Stuck
+    | Vacuous
     | DepthBound
     | CutPointRule
     | TerminalRule
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
@@ -79,6 +79,7 @@ import Kore.Equation qualified as Equation (
     argument,
     requires,
  )
+import Kore.Exec.GraphTraversal (extractStuckTraversalResult)
 import Kore.Exec.GraphTraversal qualified as GraphTraversal
 import Kore.IndexedModule.IndexedModule (
     IndexedModule (..),
@@ -323,7 +324,7 @@ exec
                         GraphTraversal.Ended results ->
                             pure results
                         GraphTraversal.GotStuck _ results ->
-                            pure results
+                            pure $ map extractStuckTraversalResult results
                         GraphTraversal.Stopped results nexts -> do
                             when (null nexts) $
                                 forM_ depthLimit warnDepthLimitExceeded
@@ -535,7 +536,8 @@ rpcExec
         toTransitionResult prior@RpcExecState{rpcProgState = priorPState} [] =
             case priorPState of
                 Remaining _ -> GraphTraversal.Stuck prior
-                Kore.Rewrite.Bottom -> GraphTraversal.Stuck prior
+                -- this should not be reachable unless we received bottom as initial configuration?
+                Kore.Rewrite.Bottom -> GraphTraversal.Vacuous prior
                 -- returns `Final` to signal that no instructions were left.
                 Start _ -> GraphTraversal.Final prior
                 Rewritten _ -> GraphTraversal.Final prior
@@ -548,13 +550,13 @@ rpcExec
                 GraphTraversal.Stop
                     (setTraces rules priorRules next)
                     []
-        toTransitionResult RpcExecState{rpcRules = priorRules} [(next@RpcExecState{rpcProgState = nextPState}, rules)] =
+        toTransitionResult prior@RpcExecState{rpcRules = priorRules} [(next@RpcExecState{rpcProgState = nextPState}, rules)] =
             let next' = setTraces rules priorRules next
              in case nextPState of
                     Start _ -> GraphTraversal.Continuing next'
                     Rewritten _ -> GraphTraversal.Continuing next'
                     Remaining _ -> GraphTraversal.Stuck next'
-                    Kore.Rewrite.Bottom -> GraphTraversal.Stuck next'
+                    Kore.Rewrite.Bottom -> GraphTraversal.Vacuous prior
         toTransitionResult prior (s : ss) =
             GraphTraversal.Branch prior $ fmap fst (s :| ss)
 
diff --git a/kore/src/Kore/Exec/GraphTraversal.hs b/kore/src/Kore/Exec/GraphTraversal.hs
@@ -13,6 +13,8 @@ module Kore.Exec.GraphTraversal (
     TraversalResult (..),
     transitionWithRule,
     GraphTraversalTimeoutMode (..),
+    StuckTraversalResult (..),
+    extractStuckTraversalResult,
 ) where
 
 import Control.Concurrent (
@@ -78,6 +80,8 @@ data TransitionResult a
     | -- | no next state but not final (e.g., not goal state, or side
       -- conditions do not hold)
       Stuck a
+    | -- | the current configuration was simplified to bottom
+      Vacuous a
     | -- | final state (e.g., goal state reached, side conditions hold)
       Final a
     | -- | not stuck, but also not final (maximum depth reached before
@@ -90,6 +94,7 @@ instance Functor TransitionResult where
         Continuing a -> Continuing $ f a
         Branch a as -> Branch (f a) $ NE.map f as
         Stuck a -> Stuck $ f a
+        Vacuous a -> Vacuous $ f a
         Final a -> Final $ f a
         Stop a as -> Stop (f a) (map f as)
 
@@ -98,6 +103,7 @@ instance Pretty a => Pretty (TransitionResult a) where
         Continuing a -> single "Continuing" a
         Branch a as -> multi "Branch" "node" a "successors" (NE.toList as)
         Stuck a -> single "Stuck" a
+        Vacuous a -> single "Vacuous" a
         Final a -> single "Final" a
         Stop a as -> multi "Stop" "node" a "successors" as
       where
@@ -115,9 +121,10 @@ instance Pretty a => Pretty (TransitionResult a) where
                 ]
                     <> map (Pretty.indent 4 . Pretty.pretty) as
 
-isStuck, isFinal, isStop, isBranch :: TransitionResult a -> Bool
-isStuck (Stuck _) = True
-isStuck _ = False
+isStuckOrVacuous, isFinal, isStop, isBranch :: TransitionResult a -> Bool
+isStuckOrVacuous (Stuck _) = True
+isStuckOrVacuous (Vacuous _) = True
+isStuckOrVacuous _ = False
 isFinal (Final _) = True
 isFinal _ = False
 isStop (Stop _ _) = True
@@ -130,6 +137,7 @@ extractNext = \case
     Continuing a -> [a]
     Branch _ as -> NE.toList as
     Stuck _ -> []
+    Vacuous _ -> []
     Final _ -> []
     Stop _ as -> as
 
@@ -138,9 +146,16 @@ extractState = \case
     Continuing _ -> Nothing
     Branch a _ -> Just a
     Stuck a -> Just a
+    Vacuous a -> Just a
     Final a -> Just a
     Stop a _ -> Just a
 
+extractStuckOrVacuous :: TransitionResult a -> Maybe (StuckTraversalResult a)
+extractStuckOrVacuous = \case
+    Stuck a -> Just $ IsStuck a
+    Vacuous a -> Just $ IsVacuous a
+    _ -> Nothing
+
 {- | The traversal state, including subsequent steps to take in the
    traversal.
 -}
@@ -239,7 +254,7 @@ graphTraversal
         ma <- liftIO newEmptyMVar
         enqueue [TState steps start] Seq.empty
             >>= either
-                (pure . const (GotStuck 0 [start]))
+                (pure . const (GotStuck 0 [IsStuck start]))
                 (\q -> evalStateT (worker ma q >>= checkLeftUnproven) [])
       where
         enqueue' = unfoldSearchOrder direction
@@ -287,14 +302,14 @@ graphTraversal
                 Continue nextQ -> worker ma nextQ
                 Output oneResult nextQ -> do
                     modify (oneResult :)
-                    if not (isStuck oneResult)
+                    if not (isStuckOrVacuous oneResult)
                         then worker ma nextQ
                         else do
-                            stuck <- gets (filter isStuck)
+                            stuck <- gets (filter isStuckOrVacuous)
                             if maxCounterExamples <= Limit (fromIntegral (length stuck))
                                 then
                                     pure $
-                                        GotStuck (Seq.length nextQ) (mapMaybe extractState stuck)
+                                        GotStuck (Seq.length nextQ) (mapMaybe extractStuckOrVacuous stuck)
                                 else worker ma nextQ
                 Abort _lastState queue -> do
                     pure $ Aborted $ toList queue
@@ -337,7 +352,7 @@ graphTraversal
             Simplifier (StepResult (TState instr config))
         step a q = do
             next <- branchStop <$> transit a
-            if (isStuck next || isFinal next || isStop next)
+            if (isStuckOrVacuous next || isFinal next || isStop next)
                 then pure (Output next q)
                 else
                     let abort (LimitExceeded queue) = Abort next queue
@@ -353,7 +368,7 @@ graphTraversal
             result@(Ended{}) -> do
                 collected <- gets reverse
                 -- we collect a maximum of 'maxCounterExamples' Stuck states
-                let stuck = map (fmap currentState) $ filter isStuck collected
+                let stuck = map (fmap currentState) $ filter isStuckOrVacuous collected
                 -- Other states may be unfinished but not stuck (Stop)
                 -- Only provide the requested amount of states (maxCounterExamples)
                 let unproven =
@@ -362,7 +377,7 @@ graphTraversal
                 pure $
                     if
                             | (not $ null stuck) ->
-                                GotStuck 0 (mapMaybe extractState stuck)
+                                GotStuck 0 (mapMaybe extractStuckOrVacuous stuck)
                             | not $ null unproven ->
                                 Stopped
                                     (mapMaybe extractState unproven)
@@ -394,10 +409,28 @@ data StepResult a
       Timeout a (Seq a)
     deriving stock (Eq, Show)
 
+data StuckTraversalResult a = IsStuck a | IsVacuous a
+    deriving stock (Eq, Show)
+    deriving stock (GHC.Generics.Generic, Functor)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+
+instance Debug a => Debug (StuckTraversalResult a)
+instance (Debug a, Diff a) => Diff (StuckTraversalResult a)
+
+instance Pretty a => Pretty (StuckTraversalResult a) where
+    pretty = \case
+        IsStuck a -> pretty a
+        IsVacuous a -> "(vacuous)" <+> pretty a
+
+extractStuckTraversalResult :: StuckTraversalResult a -> a
+extractStuckTraversalResult = \case
+    IsStuck a -> a
+    IsVacuous a -> a
+
 data TraversalResult a
     = -- | remaining queue length and stuck results (always at most
       -- maxCounterExamples many).
-      GotStuck Int [a]
+      GotStuck Int [StuckTraversalResult a]
     | -- | queue (length exceeding the limit), including result(s) of
       -- the last step that led to stopping.
       Aborted [a]
@@ -438,7 +471,7 @@ instance Pretty a => Pretty (TraversalResult a) where
                     : ("Queue" : map Pretty.pretty qu)
 instance Functor TraversalResult where
     fmap f = \case
-        GotStuck n rs -> GotStuck n (map f rs)
+        GotStuck n rs -> GotStuck n (map (fmap f) rs)
         Aborted rs -> Aborted (map f rs)
         Ended rs -> Ended (map f rs)
         Stopped rs qu -> Stopped (map f rs) (map f qu)
diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -211,7 +211,9 @@ respond serverState moduleName runSMT =
                                         }
                     GraphTraversal.GotStuck
                         _n
-                        [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState = result, rpcRules = rules}] ->
+                        [ GraphTraversal.IsStuck
+                                Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState = result, rpcRules = rules}
+                            ] ->
                             Right $
                                 Execute $
                                     ExecuteResult
@@ -222,6 +224,21 @@ respond serverState moduleName runSMT =
                                         , nextStates = Nothing
                                         , logs = mkLogs rules
                                         }
+                    GraphTraversal.GotStuck
+                        _n
+                        [ GraphTraversal.IsVacuous
+                                Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState = result, rpcRules = rules}
+                            ] ->
+                            Right $
+                                Execute $
+                                    ExecuteResult
+                                        { state = patternToExecState sort result
+                                        , depth = Depth depth
+                                        , reason = Vacuous
+                                        , rule = Nothing
+                                        , nextStates = Nothing
+                                        , logs = mkLogs rules
+                                        }
                     GraphTraversal.Stopped
                         [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules}]
                         nexts
diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs
@@ -55,6 +55,7 @@ import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
 import Kore.Attribute.Axiom qualified as Attribute.Axiom
 import Kore.Debug
+import Kore.Exec.GraphTraversal (extractStuckTraversalResult)
 import Kore.Exec.GraphTraversal qualified as GraphTraversal
 import Kore.Internal.Conditional (
     Conditional (..),
@@ -399,7 +400,7 @@ proveClaim
 
         case traversalResult of
             GraphTraversal.GotStuck n rs ->
-                returnUnprovenClaims n rs
+                returnUnprovenClaims n $ map extractStuckTraversalResult rs
             GraphTraversal.Stopped rs nexts ->
                 returnUnprovenClaims (length nexts) rs
             GraphTraversal.Aborted rs ->
diff --git a/kore/src/Kore/Rewrite.hs b/kore/src/Kore/Rewrite.hs
@@ -176,26 +176,23 @@ transitionRule ::
         (ProgramState (Pattern RewritingVariableName))
 transitionRule rewriteGroups = transitionRuleWorker
   where
+    transitionRuleWorker _ Simplify Bottom = pure Bottom
+    transitionRuleWorker _ _ Bottom = empty
     transitionRuleWorker _ Begin (Rewritten a) = pure $ Start a
     transitionRuleWorker _ Begin (Remaining _) = empty
     transitionRuleWorker _ Begin state@(Start _) = pure state
-    transitionRuleWorker _ Begin Bottom = empty
     transitionRuleWorker _ Simplify (Rewritten patt) =
         transitionSimplify Rewritten patt
     transitionRuleWorker _ Simplify (Remaining patt) =
         transitionSimplify Remaining patt
     transitionRuleWorker _ Simplify (Start patt) =
         transitionSimplify Start patt
-    transitionRuleWorker _ Simplify Bottom =
-        empty
     transitionRuleWorker mode Rewrite (Remaining patt) =
         transitionRewrite mode patt
     transitionRuleWorker mode Rewrite (Start patt) =
         transitionRewrite mode patt
     transitionRuleWorker _ Rewrite state@(Rewritten _) =
         pure state
-    transitionRuleWorker _ Rewrite Bottom =
-        empty
 
     transitionSimplify prim config = do
         configs <- lift $ Pattern.simplifyTopConfiguration config
@@ -230,7 +227,7 @@ deriveResults ::
     Result.Results (w (RulePattern variable)) a ->
     TransitionT (RewriteRule variable, Seq SimplifierTrace) Simplifier (ProgramState a)
 deriveResults Result.Results{results, remainders} =
-    if null results && null remainders
+    if (null results || all (\Result.Result{result} -> null result) results) && null remainders
         then pure Bottom
         else addResults results <|> addRemainders remainders
   where
diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs
@@ -47,7 +47,7 @@ import Kore.Equation.Equation (
  )
 import Kore.Error qualified
 import Kore.Exec
-import Kore.Exec.GraphTraversal (TraversalResult (..))
+import Kore.Exec.GraphTraversal (StuckTraversalResult (..), TraversalResult (..))
 import Kore.IndexedModule.IndexedModule
 import Kore.Internal.ApplicationSorts
 import Kore.Internal.Pattern (
@@ -201,15 +201,15 @@ test_rpcExecDepth =
     [ testCase "without depth limit" $ do
         result <-
             runDepth $ rpcExecTest [] [] Unlimited verifiedModule (state "c")
-        assertEqual "depth" (stuckAt 2) result
+        assertEqual "depth" (stuckAt $ IsStuck 2) result
     , testCase "with depth limit limiting execution" $ do
         result <-
             runDepth $ rpcExecTest [] [] (Limit 1) verifiedModule (state "c")
         assertEqual "depth" (endsAt 1) result
     , testCase "with depth limit above execution limit" $ do
         result <-
             runDepth $ rpcExecTest [] [] (Limit 3) verifiedModule (state "c")
-        assertEqual "depth" (stuckAt 2) result
+        assertEqual "depth" (stuckAt $ IsStuck 2) result
     , testCase "when branching" $ do
         result <-
             runDepth $ rpcExecTest [] [] Unlimited verifiedModule (state "a")
diff --git a/test/kevm-optimism-invariant/Makefile b/test/kevm-optimism-invariant/Makefile
@@ -2,4 +2,4 @@ DEF_KORE =
 include $(CURDIR)/../include.mk
 
 test-%.sh.out: $(TEST_DIR)/test-%-*
-KORE_EXEC_OPTS += --smt-timeout 100
+KORE_EXEC_OPTS += --smt-timeout 125
diff --git a/test/kevm-optimism-invariant/test-optimism-invariant.sh b/test/kevm-optimism-invariant/test-optimism-invariant.sh
@@ -5,7 +5,7 @@ exec kore-exec \
     --module FOUNDRY-MAIN \
     --strategy all \
     --max-counterexamples 1 \
-    --smt-retry-limit 1 \
+    --smt-retry-limit 4 \
     --smt-reset-interval 100 \
     --smt z3 \
     --log-level \
diff --git a/test/regression-wasm/test-wrc20.sh b/test/regression-wasm/test-wrc20.sh
@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-wrc20-vdefinition.kore --module WRC20-LEMMAS --prove test-wrc20-spec.kore --spec-module WRC20-SPEC "$@"
+${KORE_EXEC:?} test-wrc20-vdefinition.kore --module WRC20-LEMMAS --prove test-wrc20-spec.kore --spec-module WRC20-SPEC --smt-timeout 40 --smt-retry-limit 1 --smt-reset-interval 100 "$@"
diff --git a/test/rpc-server/execute/vacuous/definition.kore b/test/rpc-server/execute/vacuous/definition.kore
diff --git a/test/rpc-server/execute/vacuous/params.json b/test/rpc-server/execute/vacuous/params.json
diff --git a/test/rpc-server/execute/vacuous/response.golden b/test/rpc-server/execute/vacuous/response.golden
diff --git a/test/rpc-server/execute/vacuous/state.json b/test/rpc-server/execute/vacuous/state.json

Original file line number	Diff line number	Diff line change
`@@ -1,2 +1,2 @@`
`1`	`1`	`#!/bin/sh`
`2`		`-${KORE_EXEC:?} test-wrc20-vdefinition.kore --module WRC20-LEMMAS --prove test-wrc20-spec.kore --spec-module WRC20-SPEC "$@"`
	`2`	`+${KORE_EXEC:?} test-wrc20-vdefinition.kore --module WRC20-LEMMAS --prove test-wrc20-spec.kore --spec-module WRC20-SPEC --smt-timeout 40 --smt-retry-limit 1 --smt-reset-interval 100 "$@"`