From 2c30316ae3843062aad957aae791ebfe47b4b213 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 15 Nov 2023 19:24:19 +0100 Subject: [PATCH 1/7] Return JSON of term on Kore's DecidePredicateUnknown --- cabal.project | 2 +- flake.lock | 6 +++--- stack.yaml | 2 +- stack.yaml.lock | 10 +++++----- tools/booster/Server.hs | 2 +- tools/kore-rpc-dev/Server.hs | 2 +- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/cabal.project b/cabal.project index f08d01924..c745efc58 100644 --- a/cabal.project +++ b/cabal.project @@ -17,7 +17,7 @@ source-repository-package source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + tag: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 --sha256: subdir: kore kore-rpc-types diff --git a/flake.lock b/flake.lock index dd9c97643..2e01ac145 100644 --- a/flake.lock +++ b/flake.lock @@ -7,11 +7,11 @@ "z3": "z3" }, "locked": { - "lastModified": 1698918605, - "narHash": "sha256-p3n0+My1U+rfHjaFPClK92HxAjAWIxSmCYyORCWJfxo=", + "lastModified": 1700072510, + "narHash": "sha256-6HTLeB7o1KSOqigGgD5Dwl0gOg6lGH9DY/GNIVWjV2E=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "eebe4e9fd9dd6c606b37a384dbbfecca85943a38", + "rev": "1690d266738955c6fbf8fad6a36b14c2e6c2bbf4", "type": "github" }, "original": { diff --git a/stack.yaml b/stack.yaml index 53670b45d..da150d9a5 100644 --- a/stack.yaml +++ b/stack.yaml @@ -11,7 +11,7 @@ extra-deps: - typerep-map-0.5.0.0 - monad-validate-1.2.0.1 - git: https://github.com/runtimeverification/haskell-backend.git - commit: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index 3967b7d62..39e1a4766 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,20 +40,20 @@ packages: original: hackage: monad-validate-1.2.0.1 - completed: - commit: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: - sha256: 4e10ba0429ca8270171f2b1d1fcdc646631707fc7c468c14d2a2962b203c7f5c + sha256: bae5826dab9e9b0a9c73fef4de3160b15c461ddcd423a66dcfc4a76fc08f2176 size: 44685 subdir: kore version: 0.60.0.0 original: - commit: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: @@ -62,7 +62,7 @@ packages: subdir: kore-rpc-types version: 0.60.0.0 original: - commit: eebe4e9fd9dd6c606b37a384dbbfecca85943a38 + commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types snapshots: diff --git a/tools/booster/Server.hs b/tools/booster/Server.hs index f8188340a..fd891969d 100644 --- a/tools/booster/Server.hs +++ b/tools/booster/Server.hs @@ -159,7 +159,7 @@ main = do jsonRpcServer srvSettings (const $ Proxy.respondEither proxyConfig boosterRespond koreRespond) - [handleErrorCall, handleSomeException] + [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException] interruptHandler _ = do when (logLevel >= LevelInfo) $ hPutStrLn stderr "[Info#proxy] Server shutting down" diff --git a/tools/kore-rpc-dev/Server.hs b/tools/kore-rpc-dev/Server.hs index 4ee44b84d..d4fb42d9b 100644 --- a/tools/kore-rpc-dev/Server.hs +++ b/tools/kore-rpc-dev/Server.hs @@ -170,7 +170,7 @@ main = do jsonRpcServer srvSettings (const $ respond koreRespond) - [handleErrorCall, handleSomeException] + [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException] interruptHandler _ = do when (logLevel >= LevelInfo) $ hPutStrLn stderr "[Info#proxy] Server shutting down" From c5bbb5266563e0d4ca25e3350c2006eeb4149cc7 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 20 Nov 2023 16:04:04 +0100 Subject: [PATCH 2/7] Catch ErrorDecidePredicateUknown in postExecSimplify --- tools/booster/Proxy.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index 08b15c6e1..82b924a73 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -14,6 +14,7 @@ module Proxy ( import Control.Concurrent.MVar qualified as MVar import Control.Monad (when) +import Control.Monad.Catch (MonadCatch (..), catch) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Logger qualified as Log import Control.Monad.Trans.Except (runExcept) @@ -43,6 +44,7 @@ import Kore.JsonRpc.Types qualified as ExecuteRequest (ExecuteRequest (..)) import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..)) import Kore.JsonRpc.Types.Log qualified as RPCLog import Kore.Log qualified +import Kore.Log.DecidePredicateUnknown (DecidePredicateUnknown) import Kore.Syntax.Definition (SentenceAxiom) import Kore.Syntax.Json.Types qualified as KoreJson import SMT qualified @@ -72,7 +74,7 @@ serverError detail = ErrorObj ("Server error: " <> detail) (-32032) respondEither :: forall m. Log.MonadLogger m => - MonadIO m => + (MonadIO m, MonadCatch m) => ProxyConfig -> Respond (API 'Req) m (API 'Res) -> Respond (API 'Req) m (API 'Res) -> @@ -411,7 +413,7 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re postExecSimplify :: LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res) postExecSimplify logSettings start mbModule def = \case - Execute res -> Execute <$> simplifyResult res + Execute res -> Execute <$> simplifyResult res `catch` (\(_err :: DecidePredicateUnknown) -> pure res) other -> pure other where -- timeLog :: TimeDiff -> Maybe [LogEntry] From a0ebefbb0501db8345ace9be7d5bfe7cd6c3942f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 23 Nov 2023 09:56:44 +0100 Subject: [PATCH 3/7] Update HB --- cabal.project | 2 +- flake.lock | 6 +++--- stack.yaml | 2 +- stack.yaml.lock | 10 +++++----- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/cabal.project b/cabal.project index c745efc58..757d045bc 100644 --- a/cabal.project +++ b/cabal.project @@ -17,7 +17,7 @@ source-repository-package source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + tag: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 --sha256: subdir: kore kore-rpc-types diff --git a/flake.lock b/flake.lock index 2e01ac145..5173df612 100644 --- a/flake.lock +++ b/flake.lock @@ -7,11 +7,11 @@ "z3": "z3" }, "locked": { - "lastModified": 1700072510, - "narHash": "sha256-6HTLeB7o1KSOqigGgD5Dwl0gOg6lGH9DY/GNIVWjV2E=", + "lastModified": 1700651020, + "narHash": "sha256-7BpAXfdiixge0SsSJCjwqgNy085azJ7PpH/eQW9jQ7o=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "1690d266738955c6fbf8fad6a36b14c2e6c2bbf4", + "rev": "2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1", "type": "github" }, "original": { diff --git a/stack.yaml b/stack.yaml index da150d9a5..657b654c5 100644 --- a/stack.yaml +++ b/stack.yaml @@ -11,7 +11,7 @@ extra-deps: - typerep-map-0.5.0.0 - monad-validate-1.2.0.1 - git: https://github.com/runtimeverification/haskell-backend.git - commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + commit: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index 39e1a4766..00a7ca65b 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,20 +40,20 @@ packages: original: hackage: monad-validate-1.2.0.1 - completed: - commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + commit: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: - sha256: bae5826dab9e9b0a9c73fef4de3160b15c461ddcd423a66dcfc4a76fc08f2176 + sha256: 8291a1c0becedd72896f86ce074216fd7bfb8c76c48f9aa74dd078442e72b938 size: 44685 subdir: kore version: 0.60.0.0 original: - commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + commit: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + commit: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: @@ -62,7 +62,7 @@ packages: subdir: kore-rpc-types version: 0.60.0.0 original: - commit: 1690d266738955c6fbf8fad6a36b14c2e6c2bbf4 + commit: 2f90bbf6a7a970fe0b8fc4c8a5c1ec3fd8aee4f1 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types snapshots: From ceac2391756017c31873c6987846d770036485fd Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 28 Nov 2023 17:51:47 +0100 Subject: [PATCH 4/7] Return `Aborted` after catching `DecidePredicateUnknown` --- cabal.project | 2 +- flake.lock | 6 +++--- stack.yaml | 2 +- stack.yaml.lock | 10 +++++----- tools/booster/Proxy.hs | 13 +++++++++++-- 5 files changed, 21 insertions(+), 12 deletions(-) diff --git a/cabal.project b/cabal.project index 1d418f4dd..3835836c9 100644 --- a/cabal.project +++ b/cabal.project @@ -17,7 +17,7 @@ source-repository-package source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: b2bade8ce62e5f3add32d87e98244ceb31790f9f + tag: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 --sha256: subdir: kore kore-rpc-types diff --git a/flake.lock b/flake.lock index 7091e86bb..6f29445f9 100644 --- a/flake.lock +++ b/flake.lock @@ -7,11 +7,11 @@ "z3": "z3" }, "locked": { - "lastModified": 1700818937, - "narHash": "sha256-Bbv9kGWm9kTtHX6BrRbm9zIrahY1rydhbPEffZWMESA=", + "lastModified": 1701188383, + "narHash": "sha256-VWytUWtgTCaEYuRlFdRMQxt+La/xaPbC8KlxemyMBf0=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "b2bade8ce62e5f3add32d87e98244ceb31790f9f", + "rev": "09ac41cb4e6d68b9ef997fa2b36d53784a8254f9", "type": "github" }, "original": { diff --git a/stack.yaml b/stack.yaml index 0c759c214..ccdc5350b 100644 --- a/stack.yaml +++ b/stack.yaml @@ -11,7 +11,7 @@ extra-deps: - typerep-map-0.5.0.0 - monad-validate-1.2.0.1 - git: https://github.com/runtimeverification/haskell-backend.git - commit: b2bade8ce62e5f3add32d87e98244ceb31790f9f + commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index 7f6a607d0..6b732a8da 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,20 +40,20 @@ packages: original: hackage: monad-validate-1.2.0.1 - completed: - commit: b2bade8ce62e5f3add32d87e98244ceb31790f9f + commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: - sha256: 96949eeb2f74b019e43ffac323ec5b2f41394cfcd4dd94f5001a75493c84292c + sha256: 30a502eda589be5af735b1b59760ce3e0235c0cae8961978a46b3564dd8db32b size: 44685 subdir: kore version: 0.60.0.0 original: - commit: b2bade8ce62e5f3add32d87e98244ceb31790f9f + commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: b2bade8ce62e5f3add32d87e98244ceb31790f9f + commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: @@ -62,7 +62,7 @@ packages: subdir: kore-rpc-types version: 0.60.0.0 original: - commit: b2bade8ce62e5f3add32d87e98244ceb31790f9f + commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types snapshots: diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index 82b924a73..f24ab47b6 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -44,7 +44,7 @@ import Kore.JsonRpc.Types qualified as ExecuteRequest (ExecuteRequest (..)) import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..)) import Kore.JsonRpc.Types.Log qualified as RPCLog import Kore.Log qualified -import Kore.Log.DecidePredicateUnknown (DecidePredicateUnknown) +import Kore.Log.DecidePredicateUnknown (DecidePredicateUnknown, externaliseDecidePredicateUnknown) import Kore.Syntax.Definition (SentenceAxiom) import Kore.Syntax.Json.Types qualified as KoreJson import SMT qualified @@ -413,7 +413,16 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re postExecSimplify :: LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res) postExecSimplify logSettings start mbModule def = \case - Execute res -> Execute <$> simplifyResult res `catch` (\(_err :: DecidePredicateUnknown) -> pure res) + Execute res -> do + abortedOrSimplified <- + (Right <$> simplifyResult res) + `catch` ( \(err :: DecidePredicateUnknown) -> + pure . Left $ + res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} + ) + case abortedOrSimplified of + Left aborted -> pure $ Execute aborted + Right simplified -> pure $ Execute simplified other -> pure other where -- timeLog :: TimeDiff -> Maybe [LogEntry] From 966c568ad0d4dde060d3d321e0085956d9868f9f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 29 Nov 2023 12:57:09 +0100 Subject: [PATCH 5/7] Update HB --- cabal.project | 2 +- flake.lock | 6 +++--- stack.yaml | 2 +- stack.yaml.lock | 8 ++++---- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/cabal.project b/cabal.project index 3835836c9..6e9969a5f 100644 --- a/cabal.project +++ b/cabal.project @@ -17,7 +17,7 @@ source-repository-package source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + tag: 0be07d293a1167615ef9342bb1820350f794e893 --sha256: subdir: kore kore-rpc-types diff --git a/flake.lock b/flake.lock index 6f29445f9..0bd547922 100644 --- a/flake.lock +++ b/flake.lock @@ -7,11 +7,11 @@ "z3": "z3" }, "locked": { - "lastModified": 1701188383, - "narHash": "sha256-VWytUWtgTCaEYuRlFdRMQxt+La/xaPbC8KlxemyMBf0=", + "lastModified": 1701257709, + "narHash": "sha256-WoZ+XLi48Uqo558muURSY+SeThu2+VrO699r8UQI81g=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "09ac41cb4e6d68b9ef997fa2b36d53784a8254f9", + "rev": "0be07d293a1167615ef9342bb1820350f794e893", "type": "github" }, "original": { diff --git a/stack.yaml b/stack.yaml index ccdc5350b..6b8cf3221 100644 --- a/stack.yaml +++ b/stack.yaml @@ -11,7 +11,7 @@ extra-deps: - typerep-map-0.5.0.0 - monad-validate-1.2.0.1 - git: https://github.com/runtimeverification/haskell-backend.git - commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + commit: 0be07d293a1167615ef9342bb1820350f794e893 subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index 6b732a8da..82df2a6a9 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,7 +40,7 @@ packages: original: hackage: monad-validate-1.2.0.1 - completed: - commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + commit: 0be07d293a1167615ef9342bb1820350f794e893 git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: @@ -49,11 +49,11 @@ packages: subdir: kore version: 0.60.0.0 original: - commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + commit: 0be07d293a1167615ef9342bb1820350f794e893 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + commit: 0be07d293a1167615ef9342bb1820350f794e893 git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: @@ -62,7 +62,7 @@ packages: subdir: kore-rpc-types version: 0.60.0.0 original: - commit: 09ac41cb4e6d68b9ef997fa2b36d53784a8254f9 + commit: 0be07d293a1167615ef9342bb1820350f794e893 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types snapshots: From 7a2008cdd61fb59af774cbe82a9c662628aac6a3 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 8 Dec 2023 14:01:33 +0100 Subject: [PATCH 6/7] Update tools/booster/Proxy.hs Co-authored-by: Samuel Balco --- tools/booster/Proxy.hs | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index 52d752b65..f024bc1f2 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -420,16 +420,11 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re postExecSimplify :: LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res) postExecSimplify logSettings start mbModule def = \case - Execute res -> do - abortedOrSimplified <- - (Right <$> simplifyResult res) + Execute res -> Execute <$> + (simplifyResult res `catch` ( \(err :: DecidePredicateUnknown) -> - pure . Left $ - res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} - ) - case abortedOrSimplified of - Left aborted -> pure $ Execute aborted - Right simplified -> pure $ Execute simplified + pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} + )) other -> pure other where -- timeLog :: TimeDiff -> Maybe [LogEntry] From 9a5469b92ac36890052aba8eb6b36e4d9e802fe9 Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 8 Dec 2023 13:02:19 +0000 Subject: [PATCH 7/7] Format with fourmolu --- tools/booster/Proxy.hs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs index f024bc1f2..66e2a7d10 100644 --- a/tools/booster/Proxy.hs +++ b/tools/booster/Proxy.hs @@ -420,11 +420,13 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re postExecSimplify :: LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res) postExecSimplify logSettings start mbModule def = \case - Execute res -> Execute <$> - (simplifyResult res - `catch` ( \(err :: DecidePredicateUnknown) -> - pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} - )) + Execute res -> + Execute + <$> ( simplifyResult res + `catch` ( \(err :: DecidePredicateUnknown) -> + pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err} + ) + ) other -> pure other where -- timeLog :: TimeDiff -> Maybe [LogEntry]