Emit Fallback trace when kore-rpc-booster aborts in Booster and f…

…alls back to Kore (#313)

Closes
#295

Needs runtimeverification/haskell-backend#3657

Note that the `Fallback` entry changes its level of detail in presence
of `logSuccessfulRewrites`/logFailedRewrites`:
* If only `logFallbacks` is supplied, then the log entry will only
contain the pre- and post-state
* If `logFailingRewtires` is given too, the log entry will additionally
contain the rule id that caused the fallback and the fallback reason
* If `logSuccessfulRewrites` is given too, the log entry will
additionally contain the the rule log in Kore

library/Booster/JsonRpc.hs

@@ -14,6 +14,7 @@ module Booster.JsonRpc (
     execStateToKoreJson,
 ) where
 
+import Control.Applicative ((<|>))
 import Control.Concurrent (MVar, newMVar, putMVar, readMVar, takeMVar)
 import Control.Monad
 import Control.Monad.IO.Class
@@ -97,6 +98,7 @@ respond stateVar =
                                 , req.logFailedRewrites
                                 , req.logSuccessfulSimplifications
                                 , req.logFailedSimplifications
+                                , req.logFallbacks
                                 ]
                     result <- performRewrite doTracing def mLlvmLibrary mbDepth cutPoints terminals pat
                     stop <- liftIO $ getTime Monotonic
@@ -355,13 +357,19 @@ execResponse mbDuration req (d, traces, rr) = case rr of
                     , nextStates = Nothing
                     , rule = Nothing
                     }
-    RewriteAborted p ->
+    RewriteAborted failure p -> do
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.Aborted
                     , depth
-                    , logs
+                    , logs =
+                        let abortRewriteLog =
+                                mkLogRewriteTrace
+                                    (logSuccessfulRewrites, logFailedRewrites)
+                                    (logSuccessfulSimplifications, logFailedSimplifications)
+                                    (RewriteStepFailed failure)
+                         in logs <|> abortRewriteLog
                     , state = toExecState p
                     , nextStates = Nothing
                     , rule = Nothing

library/Booster/Pattern/Rewrite.hs

@@ -397,7 +397,7 @@ data RewriteResult pat
       RewriteFinished (Maybe Text) (Maybe UniqueId) pat
     | -- | unable to handle the current case with this rewriter
       -- (signalled by exceptions)
-      RewriteAborted pat
+      RewriteAborted (RewriteFailed "Rewrite") pat
     | -- | All applicable rules returned a pattern with a False
       -- ensures clause
       RewriteTrivial pat
@@ -637,8 +637,8 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa
             maybe (RewriteTrivial orig) (RewriteTerminal lbl uId) <$> simplifyP p
         RewriteFinished lbl uId p ->
             maybe (RewriteTrivial orig) (RewriteFinished lbl uId) <$> simplifyP p
-        RewriteAborted p ->
-            maybe (RewriteTrivial orig) RewriteAborted <$> simplifyP p
+        RewriteAborted reason p ->
+            maybe (RewriteTrivial orig) (RewriteAborted reason) <$> simplifyP p
 
     logTraces =
         mapM_ (logSimplify . pack . renderDefault . pretty)
@@ -719,8 +719,8 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa
                         rewriteTrace $ RewriteStepFailed failure
                         let msg = "Aborted after " <> showCounter counter
                         if wasSimplified
-                            then logRewrite msg >> pure (RewriteAborted pat')
-                            else withSimplified pat' msg (pure . RewriteAborted)
+                            then logRewrite msg >> pure (RewriteAborted failure pat')
+                            else withSimplified pat' msg (pure . RewriteAborted failure)
       where
         withSimplified p msg cont = do
             simplifyP p >>= \case

test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-and-successful-rewrites.json

@@ -0,0 +1,9 @@
+{
+    "log-fallbacks": true,
+    "log-failed-rewrites": true,
+    "log-successful-rewrites": true,
+    "terminal-rules": [
+        "TEST.EG",
+        "TEST.FG"
+    ]
+}

test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks-and-failed-rewrites.json

@@ -0,0 +1,8 @@
+{
+    "log-fallbacks": true,
+    "log-failed-rewrites": true,
+    "terminal-rules": [
+        "TEST.EG",
+        "TEST.FG"
+    ]
+}

test/rpc-integration/test-diamond/params-mutual-constraints-terminal-log-fallbacks.json

@@ -0,0 +1,7 @@
+{
+    "log-fallbacks": true,
+    "terminal-rules": [
+        "TEST.EG",
+        "TEST.FG"
+    ]
+}