From 389d13028b3d55b47a54d1988ae9b45d451ce459 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Fri, 28 Jul 2023 12:47:35 +0100 Subject: [PATCH 1/4] Fail when checking definition with Z3 returns Unknown (#3628) Fixes #3619 The definition provided in the above issue now throws the following error after re-trying once with quadruple the smt timeout: ``` kore-rpc: [4462799] Error (ErrorException): The definitions sent to the solver may not be consistent (Z3 timed out). CallStack (from HasCallStack): error, called at src/Kore/Rewrite/SMT/Lemma.hs:180:9 in kore-0.60.0.0-inplace:Kore.Rewrite.SMT.Lemma ``` --- kore/src/Kore/Rewrite/SMT/Lemma.hs | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/kore/src/Kore/Rewrite/SMT/Lemma.hs b/kore/src/Kore/Rewrite/SMT/Lemma.hs index bcb3d4e274d..3ba461d6782 100644 --- a/kore/src/Kore/Rewrite/SMT/Lemma.hs +++ b/kore/src/Kore/Rewrite/SMT/Lemma.hs @@ -24,6 +24,7 @@ import Control.Monad.Except import Control.Monad.State qualified as State import Data.Functor.Foldable qualified as Recursive import Data.Generics.Product.Fields +import Data.Limit (Limit (..)) import Data.Map.Strict qualified as Map import Data.Text qualified as Text import Kore.Attribute.Axiom qualified as Attribute @@ -52,8 +53,10 @@ import SMT ( MonadSMT (..), Result (..), SExpr (..), + TimeOut (..), assert, check, + localTimeOut, ) getSMTLemmas :: @@ -84,9 +87,22 @@ declareSMTLemmas :: declareSMTLemmas tools lemmas = do declareSortsSymbols $ smtData tools mapM_ declareRule lemmas - isUnsatisfiable <- fmap (Unsat ==) <$> SMT.check - when (fromMaybe False isUnsatisfiable) errorInconsistentDefinitions + SMT.check >>= \case + Nothing -> pure () + Just Sat -> pure () + Just Unsat -> errorInconsistentDefinitions + Just Unknown -> do + SMT.localTimeOut quadrupleTimeOut $ + SMT.check >>= \case + Nothing -> pure () + Just Sat -> pure () + Just Unsat -> errorInconsistentDefinitions + Just Unknown -> errorPossiblyInconsistentDefinitions where + quadrupleTimeOut :: SMT.TimeOut -> SMT.TimeOut + quadrupleTimeOut (SMT.TimeOut Unlimited) = SMT.TimeOut Unlimited + quadrupleTimeOut (SMT.TimeOut (Limit r)) = SMT.TimeOut (Limit (4 * r)) + declareRule :: SentenceAxiom (TermLike VariableName) -> m (Maybe ()) @@ -173,6 +189,8 @@ declareSMTLemmas tools lemmas = do ~errorInconsistentDefinitions = error "The definitions sent to the solver are inconsistent." + ~errorPossiblyInconsistentDefinitions = + error "The definitions sent to the solver may not be consistent (Z3 timed out)." translateUninterpreted :: ( Ord variable From 74b14c4de7aa7b7f1edc2f1b53b8432157ba8334 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 1 Aug 2023 06:03:11 -0600 Subject: [PATCH 2/4] Update dependency: deps/k_release (#3627) Co-authored-by: devops Co-authored-by: Samuel Balco --- deps/k_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/k_release b/deps/k_release index 11f6712c862..290c47f4a5d 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.24 +6.0.36 From 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Tue, 1 Aug 2023 15:57:31 +0100 Subject: [PATCH 3/4] RPC server should return stuck (#3634) The server currently returns `depth-bound` as a reason, when no applicable rules were found. The reason should instead be `stuck` if max-depth wasn't reached. --- kore/src/Kore/JsonRpc.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 628c90c420a..ae14f227536 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -204,7 +204,7 @@ respond serverState moduleName runSMT = ExecuteResult { state = patternToExecState sort result , depth = Depth depth - , reason = DepthBound + , reason = if Just (Depth depth) == maxDepth then DepthBound else Stuck , rule = Nothing , nextStates = Nothing , logs = mkLogs rules From a47444ba3a8080cc510e16b48a7d70e13c764f7b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 7 Aug 2023 16:50:23 +1000 Subject: [PATCH 4/4] Update haskell-nix dependency to enable upgrading K release downstream (#3635) Downstream nix setup for `hs-backend-booster` fails with "unknown index state" when trying to upgrade to 6.0.x versions. --- flake.lock | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/flake.lock b/flake.lock index 30e15bb32df..49139dd134b 100644 --- a/flake.lock +++ b/flake.lock @@ -152,11 +152,11 @@ "hackage": { "flake": false, "locked": { - "lastModified": 1687998569, - "narHash": "sha256-VfTZVu2JV5z8KgPV++JAwn51gug02PDnTSnVrmt2YL8=", + "lastModified": 1690935861, + "narHash": "sha256-CxYnaxQudPKOoSPOtpQ9ZVogjDWz3B+ZgL4YumEBY9g=", "owner": "input-output-hk", "repo": "hackage.nix", - "rev": "2ef1dc1b2cac3fec82df01d8ee3fb3dd0a33815a", + "rev": "4e6c3592ff197354762f3272515245ca862608ca", "type": "github" }, "original": { @@ -196,11 +196,11 @@ "stackage": "stackage" }, "locked": { - "lastModified": 1687999883, - "narHash": "sha256-4PxsyJekURUD/cZ7q0OAxfA6ZOoiton+6G1vgo9u+98=", + "lastModified": 1690937149, + "narHash": "sha256-XInxxsmuJmw1HraaETdalh0qAzlQSdjaWw5NdIp++0k=", "owner": "input-output-hk", "repo": "haskell.nix", - "rev": "b113a4a63c54f34d49d9f5d48ba6bbd65300bfa3", + "rev": "61d2d278aa765ffc70cf259f3290620a63dde0ca", "type": "github" }, "original": { @@ -229,16 +229,16 @@ "hls-2.0": { "flake": false, "locked": { - "lastModified": 1684398654, - "narHash": "sha256-RW44up2BIyBBYN6tZur5f9kDDR3kr0Rd+TgPbLTfwB4=", + "lastModified": 1687698105, + "narHash": "sha256-OHXlgRzs/kuJH8q7Sxh507H+0Rb8b7VOiPAjcY9sM1k=", "owner": "haskell", "repo": "haskell-language-server", - "rev": "20c6d1e731cd9c0beef7338e2fc7a8126ba9b6fb", + "rev": "783905f211ac63edf982dd1889c671653327e441", "type": "github" }, "original": { "owner": "haskell", - "ref": "2.0.0.0", + "ref": "2.0.0.1", "repo": "haskell-language-server", "type": "github" } @@ -285,11 +285,11 @@ "iserv-proxy": { "flake": false, "locked": { - "lastModified": 1670983692, - "narHash": "sha256-avLo34JnI9HNyOuauK5R69usJm+GfW3MlyGlYxZhTgY=", + "lastModified": 1688517130, + "narHash": "sha256-hUqfxSlo+ffqVdkSZ1EDoB7/ILCL25eYkcCXW9/P3Wc=", "ref": "hkm/remote-iserv", - "rev": "50d0abb3317ac439a4e7495b185a64af9b7b9300", - "revCount": 10, + "rev": "9151db2a9a61d7f5fe52ff8836f18bbd0fd8933c", + "revCount": 13, "type": "git", "url": "https://gitlab.haskell.org/hamishmack/iserv-proxy.git" }, @@ -511,11 +511,11 @@ "stackage": { "flake": false, "locked": { - "lastModified": 1687911052, - "narHash": "sha256-iWrKX6JfcN1+uUQimaFXzvLwj3tLMvWTwf0zqflCf1s=", + "lastModified": 1690934965, + "narHash": "sha256-0uPK61CXFgsr074NALEtHScOhCM6kxsRFlixeZ8lonI=", "owner": "input-output-hk", "repo": "stackage.nix", - "rev": "8e758d849bd7cf8c423d9f9308a9c1b5f56c286c", + "rev": "182ad27462c196cfd8fd93998ba67d1ae8d5df4e", "type": "github" }, "original": {