From ac6c5353311bfef7f5b5541cf4f9143e24d5c180 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Jun 2024 18:03:22 +1000 Subject: [PATCH] Hotfix more logging tweaks (#3954) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * include `hook ` log contexts in `-l Simplify` and `-l SimplifySuccess` * log timing statistics with a log context `proxy,timing` Example JSON output for `--log-context proxy`
``` {"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""} {"context":["proxy"],"message":"Starting RPC server"} {"context":["proxy"],"message":"Processing request 4"} {"context":["proxy"],"message":"Starting execute request"} {"context":["proxy"],"message":"Booster Aborted at Depth {getNat = 10}"} {"context":["proxy"],"message":"Simplifying booster state and falling back to Kore"} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":34017.38,"method":"SimplifyM","time":43152.727999999996}} {"context":["proxy"],"message":"Executing fall-back request"} {"context":["proxy","timing","kore"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":37633.786}} {"context":["proxy","abort"],"message":"Booster aborted, kore yields Branching"} {"context":["proxy"],"message":"Kore Branching at Depth {getNat = 0}"} {"context":["proxy"],"message":"Simplifying state in Branching result"} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":33663.381,"method":"SimplifyM","time":43049.642}} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":33558.555,"method":"SimplifyM","time":42640.443}} {"context":["proxy"],"message":"Simplifying execution state"} {"context":["proxy","timing"],"message":{"kore-time":34078.823,"method":"SimplifyM","time":43215.810999999994}} {"context":["proxy","abort","detail"],"message":"Kore simplification: Diff (< before - > after)\n"} {"context":["proxy","timing"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":51747.152}} {"context":["proxy"],"message":"Server shutting down"} {"context":["proxy","timing"],"message":[["ExecuteM",{"average":51747.152,"count":1,"kore-average":37633.786,"kore-max":37633.786,"kore-total":37633.786,"max-val":51747.152,"min-val":51747.152,"stddev":0,"total":51747.152}],["SimplifyM",{"average":43014.655999999995,"count":4,"kore-average":33829.53475,"kore-max":34078.823,"kore-total":135318.139,"max-val":43215.810999999994,"min-val":42640.443,"stddev":224.0460894407471,"total":172058.62399999998}]]} ```
Example text output: (as before)
``` [proxy] Processing request 4 [proxy] Starting execute request [proxy] Booster Aborted at Depth {getNat = 10} [proxy] Simplifying booster state and falling back to Kore [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.907ms (33.585ms kore time) [proxy] Executing fall-back request [proxy][timing][kore] Kore fall-back in 37.303ms [proxy][abort] Booster aborted, kore yields Branching [proxy] Kore Branching at Depth {getNat = 0} [proxy] Simplifying state in Branching result [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.253ms (32.774ms kore time) [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 41.732ms (32.446ms kore time) [proxy] Simplifying execution state [proxy][timing] Performed SimplifyM in 42.379ms (33.301ms kore time) [proxy][abort][detail] Kore simplification: Diff (< before - > after) [proxy][timing] Performed ExecuteM in 50.100ms (37.303ms kore time) [proxy] Server shutting down [proxy][timing] --------------------------- RPC request time statistics --------------------------- ExecuteM: Requests: 1 Total time: 50.100ms Average time per request: 50.100ms (+- 0.0μs), range [50.100ms, 50.100ms] Total time in kore-rpc code: 37.303ms Average time per request in kore-rpc code: 37.303ms, max 37.303ms SimplifyM: Requests: 4 Total time: 0.17s Average time per request: 42.318ms (+- 0.418ms), range [41.732ms, 42.907ms] Total time in kore-rpc code: 0.13s Average time per request in kore-rpc code: 33.027ms, max 33.585ms ```
--------- Co-authored-by: github-actions --- booster/library/Booster/CLOptions.hs | 4 +- booster/library/Booster/Log.hs | 9 ++++ .../simplify-log.txt.golden | 30 ++++++++++++++ .../test-log-simplify-json/test.sh | 2 +- booster/tools/booster/Proxy.hs | 41 ++++++++----------- booster/tools/booster/Server.hs | 16 ++++---- booster/tools/booster/Stats.hs | 25 +++++++++-- .../src/Kore/JsonRpc/Types/ContextLog.hs | 1 + 8 files changed, 91 insertions(+), 37 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index ac18d05157..3e66f31f25 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -244,14 +244,14 @@ levelToContext = [ ( "Simplify" , - [ [ctxt| booster|kore>function*|simplification*,success|failure|abort|detail |] + [ [ctxt| booster|kore>function*|simplification*|hook*,success|failure|abort|detail |] , [ctxt| booster|kore>function*|simplification*,match,failure|abort |] ] ) , ( "SimplifySuccess" , - [ [ctxt| booster|kore>function*|simplification*,success|detail |] + [ [ctxt| booster|kore>function*|simplification*|hook*,success|detail |] ] ) , diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index 82204a97e6..b842166588 100644 --- a/booster/library/Booster/Log.hs +++ b/booster/library/Booster/Log.hs @@ -19,6 +19,7 @@ module Booster.Log ( jsonLogger, textLogger, withContext, + withContexts, withKorePatternContext, withPatternContext, withRuleContext, @@ -83,6 +84,10 @@ instance ToLogFormat Text where toTextualLog t = t toJSONLog t = String t +instance ToLogFormat String where + toTextualLog = pack + toJSONLog = String . pack + instance ToLogFormat Term where toTextualLog t = renderOneLineText $ pretty t toJSONLog t = toJSON $ addHeader $ externaliseTerm t @@ -141,6 +146,10 @@ logPretty = logMessage . renderOneLineText . pretty withContext :: LoggerMIO m => SimpleContext -> m a -> m a withContext c = withContext_ (CLNullary c) +withContexts :: LoggerMIO m => [SimpleContext] -> m a -> m a +withContexts [] m = m +withContexts cs m = foldr withContext m cs + withContext_ :: LoggerMIO m => CLContext -> m a -> m a withContext_ c = withLogger diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index 9d0628ae6e..0a8fee5466 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -5,42 +5,72 @@ {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"} {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\")"} {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"f67b89d"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"2fbed22"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"80d934c"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} \"$n\""} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.not"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"bd6d88b"},{"hook":"BOOL.and"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"b3a22c24b0d945e521d86b44dadfa10beda45b356f9941753e93183cabef0351"},"constraint",{"term":"dbbbb63"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"d9cfe5a"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"5875655"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"4a555cf"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f2fa0db"},{"hook":"BOOL.and"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"5a046bd"},{"rewrite":"45286489d58bcd9b23df3023d9efddcdde80fdfe2603d7a5b07669acd2a1d540"},"constraint",{"term":"f464178"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"9893c04"},{"rewrite":"6b84f401532c1b66bd9dab31a7b06181c1b2a4cee891e9c3936f39ecea75c8fc"},"constraint",{"term":"5b84449"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"} {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"} {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]]}} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"context":["booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} {"context":["kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":["booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"66aa67b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"Eq#VarA","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"EVar","name":"Eq#VarB","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]]}} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} {"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"success",{"term":"f6384ee"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}}} +{"context":["booster","simplify",{"term":"931632b"},{"term":"be686bf"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} +{"context":["booster","simplify",{"term":"931632b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":["proxy"],"message":"Server shutting down"} diff --git a/booster/test/rpc-integration/test-log-simplify-json/test.sh b/booster/test/rpc-integration/test-log-simplify-json/test.sh index 6117bb0bc5..ff59452fa5 100755 --- a/booster/test/rpc-integration/test-log-simplify-json/test.sh +++ b/booster/test/rpc-integration/test-log-simplify-json/test.sh @@ -8,7 +8,7 @@ echo "client=$client" echo "dir=$dir" echo "arguments=$*" -diff="git diff --no-index" +diff="git --no-pager diff --no-index" # remove "--regenerate" and tweak $diff if it is present regenerate () { diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index b490df12d2..93ef9b513c 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -49,7 +49,7 @@ import Kore.Log qualified import Kore.Syntax.Definition (SentenceAxiom) import Kore.Syntax.Json.Types qualified as KoreJson import SMT qualified -import Stats (StatsVar, addStats, microsWithUnit, timed) +import Stats (MethodTiming (..), StatsVar, addStats, microsWithUnit, timed) data KoreServer = KoreServer { serverState :: MVar.MVar Kore.ServerState @@ -64,7 +64,7 @@ data KoreServer = KoreServer } data ProxyConfig = ProxyConfig - { statsVar :: Maybe StatsVar + { statsVar :: StatsVar , forceFallback :: Maybe Depth , boosterState :: MVar.MVar Booster.ServerState , fallbackReasons :: [HaltReason] @@ -83,7 +83,7 @@ respondEither :: Respond (API 'Req) m (API 'Res) -> Respond (API 'Req) m (API 'Res) -> Respond (API 'Req) m (API 'Res) -respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case req of +respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of Execute execReq | isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout -> loggedKore ExecuteM req @@ -252,21 +252,10 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re logStats method (time, time) pure result - logStats method (time, koreTime) - | Just v <- statsVar = do - addStats v method time koreTime - Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage' $ - Text.pack $ - unwords - [ "Performed" - , show method - , "in" - , microsWithUnit time - , "(" <> microsWithUnit koreTime <> " kore time)" - ] - | otherwise = - pure () + logStats method (time, koreTime) = do + let timing = MethodTiming{method, time, koreTime} + addStats cfg.statsVar timing + Booster.Log.withContexts [CtxProxy, CtxTiming] $ Booster.Log.logMessage timing handleExecute :: LogSettings -> @@ -397,11 +386,17 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re , assumeStateDefined = Just True } ) - when (isJust statsVar) $ do - Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage $ - Text.pack $ - "Kore fall-back in " <> microsWithUnit kTime + Booster.Log.withContexts [CtxProxy, CtxTiming, CtxKore] $ + Booster.Log.logMessage $ + WithJsonMessage + ( toJSON + MethodTiming + { method = ExecuteM + , time = kTime + , koreTime = kTime + } + ) + ("Kore fall-back in " <> microsWithUnit kTime) case kResult of Right (Execute koreResult) -> do let diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index a25e690179..da6dd26f34 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE QuasiQuotes #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {- | @@ -13,7 +14,6 @@ import Control.DeepSeq (force) import Control.Exception (AsyncException (UserInterrupt), evaluate, handleJust) import Control.Monad (forM_, unless, void) import Control.Monad.Catch (bracket) -import Control.Monad.Extra (whenJust) import Control.Monad.IO.Class (MonadIO (liftIO)) import Control.Monad.Logger ( LogLevel (..), @@ -58,7 +58,7 @@ import Booster.GlobalState import Booster.JsonRpc qualified as Booster import Booster.LLVM.Internal (mkAPI, withDLib) import Booster.Log hiding (withLogger) -import Booster.Log.Context qualified +import Booster.Log.Context qualified as Ctxt import Booster.Pattern.Base (Predicate (..)) import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..)) @@ -149,6 +149,7 @@ main = do logContextsWithcustomLevelContexts = logContexts <> concatMap (\case LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels + <> [[Ctxt.ctxt| *>timing |] | printStats] contextLoggingEnabled = not (null logContextsWithcustomLevelContexts) koreSolverOptions = translateSMTOpts smtOptions timestampFlag = case timeStampsFormat of @@ -177,7 +178,7 @@ main = do ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c ) ctxt - in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts + in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts ) koreLogEntries = @@ -194,7 +195,7 @@ main = do flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) -> alwaysDisplay || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts - in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts + in any (flip Ctxt.mustMatch ctxt) logContextsWithcustomLevelContexts runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a runBoosterLogger = flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT @@ -303,7 +304,7 @@ main = do , mSMTOptions = if boosterSMT then smtOptions else Nothing , addedModules = mempty } - statsVar <- if printStats then Just <$> Stats.newStats else pure Nothing + statsVar <- Stats.newStats writeGlobalEquationOptions equationOptions @@ -343,8 +344,9 @@ main = do interruptHandler _ = runBoosterLogger . Booster.Log.withContext CtxProxy $ do Booster.Log.logMessage' @_ @Text "Server shutting down" - whenJust statsVar $ \var -> - liftIO (Stats.finaliseStats var) >>= Booster.Log.logMessage' + ( liftIO (Stats.finaliseStats statsVar) + >>= Booster.Log.withContext CtxTiming . Booster.Log.logMessage + ) liftIO exitSuccess handleJust isInterrupt interruptHandler $ runBoosterLogger server where diff --git a/booster/tools/booster/Stats.hs b/booster/tools/booster/Stats.hs index c4e349ab20..6ee058cce7 100644 --- a/booster/tools/booster/Stats.hs +++ b/booster/tools/booster/Stats.hs @@ -6,6 +6,7 @@ module Stats ( microsWithUnit, RequestStats (..), StatsVar, + MethodTiming (..), ) where import Control.Concurrent.MVar (MVar, modifyMVar_, newMVar, readMVar) @@ -13,6 +14,7 @@ import Control.Monad.IO.Class (MonadIO (liftIO)) import Data.Aeson import Data.Map (Map) import Data.Map qualified as Map +import Data.Text (pack) import Deriving.Aeson import GHC.Generics () import Prettyprinter @@ -108,14 +110,29 @@ singleStats' x korePart = type StatsVar = MVar (Map APIMethod (Stats' Double)) +-- helper type mainly for json logging +data MethodTiming a = MethodTiming {method :: APIMethod, time :: a, koreTime :: a} + deriving stock (Eq, Show, Generic) + deriving + (ToJSON, FromJSON) + via CustomJSON '[FieldLabelModifier '[CamelToKebab]] (MethodTiming a) + +instance ToLogFormat (MethodTiming Double) where + toTextualLog mt = + pack $ + printf + "Performed %s in %s (%s kore time)" + (show mt.method) + (microsWithUnit mt.time) + (microsWithUnit mt.koreTime) + toJSONLog = toJSON + addStats :: MonadIO m => MVar (Map APIMethod (Stats' Double)) -> - APIMethod -> - Double -> - Double -> + MethodTiming Double -> m () -addStats statVar method time koreTime = +addStats statVar MethodTiming{method, time, koreTime} = liftIO . modifyMVar_ statVar $ pure . Map.insertWith (<>) method (singleStats' time koreTime) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs index dc87190377..231990053d 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs @@ -47,6 +47,7 @@ data SimpleContext | CtxDetail | CtxSubstitution | CtxDepth + | CtxTiming | -- standard log levels CtxError | CtxWarn