From c2b645573e104fba09e6fcd583ea0495758eaecf Mon Sep 17 00:00:00 2001
From: Samuel Balco <goodlyrottenapple@gmail.com>
Date: Tue, 26 Mar 2024 10:31:57 +0000
Subject: [PATCH] Log ceil analysis with `-l Ceil` (#510)

When starting the server with `-l Ceil`, with this change, we will emit
the logs of the ceil analysis of rewrite rules in the given definition
file, e.g.:

```
[Ceil#booster] Partial symbols found in rule /Users/sam/git/hs-backend-booster/bug_reports/concurrency_crash/imp.k :  ( 54
, 8 )
  non-total symbol Lbl_modInt_
rule does NOT preserve definedness. Partially computed ceils:
  _=/=Int_(Rule#VarI2:SortInt{}, "0")
  #Ceil( Rule#VarI2:SortInt{} )
```

---------

Co-authored-by: github-actions <github-actions@github.com>
---
 library/Booster/CLOptions.hs |  1 +
 tools/booster/Server.hs      | 35 ++++++++++++++++++++++++++++++-----
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/library/Booster/CLOptions.hs b/library/Booster/CLOptions.hs
index 80a646f4..2c21c5b4 100644
--- a/library/Booster/CLOptions.hs
+++ b/library/Booster/CLOptions.hs
@@ -134,6 +134,7 @@ allowedLogLevels =
     , ("Depth", "Log the current depth of the state")
     , ("SMT", "Log the SMT-solver interactions")
     , ("ErrorDetails", "Log error conditions with extensive details")
+    , ("Ceil", "Log results of the ceil analysis")
     ]
 
 -- Partition provided log levels into standard and custom ones, and
diff --git a/tools/booster/Server.hs b/tools/booster/Server.hs
index b49e4ce7..07b3b169 100644
--- a/tools/booster/Server.hs
+++ b/tools/booster/Server.hs
@@ -43,10 +43,13 @@ import System.Exit
 import System.IO qualified as IO
 
 import Booster.CLOptions
-import Booster.Definition.Ceil (computeCeilsDefinition)
+import Booster.Definition.Attributes.Base (ComputedAxiomAttributes (notPreservesDefinednessReasons))
+import Booster.Definition.Base (HasSourceRef (sourceRef), RewriteRule (computedAttributes))
+import Booster.Definition.Ceil (ComputeCeilSummary (..), computeCeilsDefinition)
 import Booster.GlobalState
 import Booster.JsonRpc qualified as Booster
 import Booster.LLVM.Internal (mkAPI, withDLib)
+import Booster.Prettyprinter (renderText)
 import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..))
 import Booster.SMT.Interface (SMTOptions (..))
 import Booster.Syntax.ParsedKore (loadDefinition)
@@ -79,6 +82,7 @@ import Kore.Log.Registry qualified as Log
 import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
 import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
 import Options.SMT as KoreSMT (KoreSolverOptions (..), Solver (..))
+import Prettyprinter qualified as Pretty
 import Proxy (KoreServer (..), ProxyConfig (..))
 import Proxy qualified
 import SMT qualified as KoreSMT
@@ -151,17 +155,38 @@ main = do
 
                 withLogger reportDirectory koreLogOptions $ \actualLogAction -> do
                     mLlvmLibrary <- maybe (pure Nothing) (fmap Just . mkAPI) mdl
-                    definitions <-
+                    definitionsWithCeilSummaries <-
                         liftIO $
                             loadDefinition definitionFile
-                                >>= mapM (mapM ((fst <$>) . runNoLoggingT . computeCeilsDefinition mLlvmLibrary))
+                                >>= mapM (mapM (runNoLoggingT . computeCeilsDefinition mLlvmLibrary))
                                 >>= evaluate . force . either (error . show) id
-                    unless (isJust $ Map.lookup mainModuleName definitions) $ do
+                    unless (isJust $ Map.lookup mainModuleName definitionsWithCeilSummaries) $ do
                         flip runLoggingT monadLogger $
                             Logger.logErrorNS "proxy" $
                                 "Main module " <> mainModuleName <> " not found in " <> Text.pack definitionFile
                         liftIO exitFailure
 
+                    flip runLoggingT monadLogger $
+                        forM_ (Map.elems definitionsWithCeilSummaries) $ \(_, summaries) ->
+                            forM_ summaries $ \ComputeCeilSummary{rule, ceils} ->
+                                Logger.logOtherNS "booster" (Logger.LevelOther "Ceil") $
+                                    renderText $
+                                        Pretty.vsep $
+                                            [ "Partial symbols found in rule"
+                                            , Pretty.pretty (sourceRef rule)
+                                            , Pretty.indent 2 . Pretty.vsep $
+                                                map Pretty.pretty rule.computedAttributes.notPreservesDefinednessReasons
+                                            ]
+                                                <> if null ceils
+                                                    then ["discharged all ceils, rule preserves definedness"]
+                                                    else
+                                                        [ "rule does NOT preserve definedness. Partially computed ceils:"
+                                                        , Pretty.indent 2 . Pretty.vsep $
+                                                            map
+                                                                (either Pretty.pretty (\t -> "#Ceil(" Pretty.<+> Pretty.pretty t Pretty.<+> ")"))
+                                                                (Set.toList ceils)
+                                                        ]
+
                     mvarLogAction <- newMVar actualLogAction
                     let logAction = swappableLogger mvarLogAction
 
@@ -172,7 +197,7 @@ main = do
                         liftIO $
                             newMVar
                                 Booster.ServerState
-                                    { definitions
+                                    { definitions = Map.map fst definitionsWithCeilSummaries
                                     , defaultMain = mainModuleName
                                     , mLlvmLibrary
                                     , mSMTOptions = if boosterSMT then smtOptions else Nothing