Custom log levels for kore + small tweaks (#368)

* Several new log levels, some of which go through to `kore-rpc` * Refactored term diff, used to display the effect of the kore-rpc simplification run vs booster * Refactored error case for internal simplification * removed 0-step execute request from internal simplification routine (changes expectations for foundry test)
runtimeverification · Nov 15, 2023 · 8ecb99b · 8ecb99b
1 parent 09ea14a
commit 8ecb99b
Show file tree

Hide file tree

Showing 19 changed files with 1,270 additions and 712 deletions.
diff --git a/library/Booster/CLOptions.hs b/library/Booster/CLOptions.hs
@@ -58,8 +58,8 @@ clOptionsParser =
                     <> short 'l'
                     <> help
                         ( "Log level: debug, info (default), warn, error, \
-                          \or a custom level from "
-                            <> show allowedLogLevels
+                          \or a custom level: "
+                            <> intercalate ", " (map fst allowedLogLevels)
                         )
                 )
             )
@@ -93,7 +93,7 @@ clOptionsParser =
         "warn" -> Right LevelWarn
         "error" -> Right LevelError
         other
-            | other `elem` allowedLogLevels -> Right (LevelOther $ pack other)
+            | other `elem` map fst allowedLogLevels -> Right (LevelOther $ pack other)
             | otherwise -> Left $ other <> ": Unsupported log level"
 
     readEventLogTracing :: String -> Either String CustomUserEventType
@@ -103,8 +103,16 @@ clOptionsParser =
             . fromKebab
 
 -- custom log levels that can be selected
-allowedLogLevels :: [String]
-allowedLogLevels = ["Rewrite", "Simplify", "Depth"]
+allowedLogLevels :: [(String, String)]
+allowedLogLevels =
+    [ ("Rewrite", "Log all rewriting in booster")
+    , ("RewriteKore", "Log all rewriting in kore-rpc fall-backs")
+    , ("RewriteSuccess", "Log successful rewrites (booster and kore-rpc)")
+    , ("Simplify", "Log all simplification/evaluation in booster")
+    , ("SimplifyKore", "Log all simplification in kore-rpc")
+    , ("SimplifySuccess", "Log successful simplifications (booster and kore-rpc)")
+    , ("Depth", "Log the current depth of the state")
+    ]
 
 -- Partition provided log levels into standard and custom ones, and
 -- select the lowest standard level. Default to 'LevelInfo' if no

diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -12,6 +12,7 @@ module Booster.JsonRpc (
     runServer,
     RpcTypes.rpcJsonConfig,
     execStateToKoreJson,
+    toExecState,
 ) where
 
 import Control.Applicative ((<|>))
@@ -177,9 +178,9 @@ respond stateVar =
                         (Right newPattern, patternTraces, _) -> do
                             let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
                                 tSort = externaliseSort (sortOfPattern newPattern)
-                                predicate = fromMaybe (KoreJson.KJTop tSort) mbPredicate
-                                substitution = fromMaybe (KoreJson.KJTop tSort) mbSubstitution
-                                result = KoreJson.KJAnd tSort [term, predicate, substitution]
+                                result = case catMaybes [mbPredicate, mbSubstitution] of
+                                    [] -> term
+                                    ps -> KoreJson.KJAnd tSort $ term : ps
                             pure $ Right (addHeader result, patternTraces)
                         (Left ApplyEquations.SideConditionsFalse{}, patternTraces, _) -> do
                             let tSort = fromMaybe (error "unknown sort") $ sortOfJson req.state.term

diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -12,22 +12,30 @@ module Booster.JsonRpc.Utils (
     KoreRpcType (..),
     rpcTypeOf,
     typeString,
-    renderDiff, -- temporary hack
+    diffBy,
 ) where
 
 import Control.Applicative ((<|>))
+import Control.Monad.Trans.Except
 import Data.Aeson as Json
 import Data.Aeson.Encode.Pretty (encodePretty')
 import Data.Aeson.Types (parseMaybe)
 import Data.ByteString.Lazy.Char8 qualified as BS
+import Data.Functor.Foldable (Corecursive (embed), cata)
 import Data.Maybe (fromMaybe)
+import Data.Set qualified as Set
 import Network.JSONRPC
+import Prettyprinter
 import System.Exit (ExitCode (..))
 import System.FilePath
 import System.IO.Extra (withTempDir)
 import System.IO.Unsafe (unsafePerformIO)
 import System.Process (readProcessWithExitCode)
 
+import Booster.Definition.Base qualified as Internal
+import Booster.Pattern.Base qualified as Internal
+import Booster.Prettyprinter
+import Booster.Syntax.Json.Internalise
 import Kore.JsonRpc.Types
 import Kore.Syntax.Json.Types hiding (Left, Right)
 
@@ -89,12 +97,12 @@ renderResult korefile1 korefile2 = \case
     JsonDiff rpcType first second ->
         BS.unlines
             [ BS.unwords ["Files", file1, "and", file2, "are different", typeString rpcType <> "s"]
-            , renderDiff first second
+            , BS.pack $ fromMaybe (error "Expected difference") $ renderDiff first second
             ]
     TextDiff first second ->
         BS.unlines
             [ BS.unwords ["Files", file1, "and", file2, "are different non-json files"]
-            , renderDiff first second
+            , BS.pack $ fromMaybe (error "Expected difference") $ renderDiff first second
             ]
   where
     file1 = BS.pack korefile1
@@ -205,14 +213,45 @@ rpcTypeOf = \case
 -------------------------------------------------------------------
 -- doing the actual diff when output is requested
 
-renderDiff :: BS.ByteString -> BS.ByteString -> BS.ByteString
+renderDiff :: BS.ByteString -> BS.ByteString -> Maybe String
+renderDiff first second
+    | first == second = Nothing
 renderDiff first second = unsafePerformIO . withTempDir $ \dir -> do
     let path1 = dir </> "diff_file1.txt"
         path2 = dir </> "diff_file2.txt"
     BS.writeFile path1 first
     BS.writeFile path2 second
     (result, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] ""
     case result of
-        ExitSuccess -> error "Unexpected result: identical content"
-        ExitFailure 1 -> pure $ BS.pack str
+        ExitSuccess -> pure Nothing
+        ExitFailure 1 -> pure $ Just str
         ExitFailure n -> error $ "diff process exited with code " <> show n
+
+-------------------------------------------------------------------
+-- compute diff on internalised patterns (to normalise collections etc)
+-- This uses the `pretty` instance for a textual diff.
+diffBy :: Internal.KoreDefinition -> KorePattern -> KorePattern -> Maybe String
+diffBy def pat1 pat2 =
+    renderDiff (internalise pat1) (internalise pat2)
+  where
+    renderBS :: Internal.TermOrPredicate -> BS.ByteString
+    renderBS (Internal.APredicate p) = BS.pack . renderDefault $ pretty p
+    renderBS (Internal.TermAndPredicate p) = BS.pack . renderDefault $ pretty p
+    internalise =
+        either
+            (("Pattern could not be internalised: " <>) . Json.encode)
+            (renderBS . orientEquals)
+            . runExcept
+            . internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def
+
+    orientEquals = \case
+        Internal.APredicate p ->
+            Internal.APredicate $ orient p
+        Internal.TermAndPredicate p ->
+            Internal.TermAndPredicate p{Internal.constraints = Set.map orient p.constraints}
+      where
+        orient :: Internal.Predicate -> Internal.Predicate
+        orient = cata $ \case
+            Internal.EqualsTermF t1 t2
+                | t1 > t2 -> Internal.EqualsTerm t2 t1
+            other -> embed other
diff --git a/library/Booster/Pattern/ApplyEquations.hs b/library/Booster/Pattern/ApplyEquations.hs
@@ -536,7 +536,11 @@ traceRuleApplication ::
     EquationT io ()
 traceRuleApplication t loc lbl uid res = do
     let newTraceItem = EquationTrace t loc lbl uid res
-    logOther (LevelOther "Simplify") (pack . renderDefault . pretty $ newTraceItem)
+        prettyItem = pack . renderDefault . pretty $ newTraceItem
+    logOther (LevelOther "Simplify") prettyItem
+    case res of
+        Success{} -> logOther (LevelOther "SimplifySuccess") prettyItem
+        _ -> pure ()
     config <- getConfig
     when config.doTracing $
         EquationT . lift . lift . modify $
@@ -688,11 +692,11 @@ simplifyConstraint doTracing def mbApi cache p =
 
 -- version for internal nested evaluation
 simplifyConstraint' :: MonadLoggerIO io => Predicate -> EquationT io Predicate
--- We are assuming all predicates are of the form 'P ==Bool true' and
+-- We are assuming all predicates are of the form 'true \equals P' and
 -- evaluating them using simplifyBool if they are concrete.
 -- Non-concrete \equals predicates are simplified using evaluateTerm.
 simplifyConstraint' = \case
-    EqualsTerm t@(Term attributes _) TrueBool
+    EqualsTerm TrueBool t@(Term attributes _)
         | isConcrete t && attributes.canBeEvaluated -> do
             mbApi <- (.llvmApi) <$> getConfig
             case mbApi of
@@ -704,17 +708,17 @@ simplifyConstraint' = \case
                     evalBool t >>= prune
         | otherwise ->
             evalBool t >>= prune
-    EqualsTerm TrueBool t ->
-        -- although "true" is usually 2nd
-        simplifyConstraint' (EqualsTerm t TrueBool)
+    EqualsTerm t TrueBool ->
+        -- normalise to 'true' in first argument (like 'kore-rpc')
+        simplifyConstraint' (EqualsTerm TrueBool t)
     other ->
-        pure other -- should not occur, predicates should be '_ ==Bool true'
+        pure other -- should not occur, predicates should be 'true \equals _'
   where
     prune =
         pure . \case
             TrueBool -> Top
             FalseBool -> Bottom
-            other -> EqualsTerm other TrueBool
+            other -> EqualsTerm TrueBool other
 
     evalBool :: MonadLoggerIO io => Term -> EquationT io Term
     evalBool t = do

diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs
@@ -570,6 +570,7 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa
   where
     logDepth = logOther (LevelOther "Depth")
     logRewrite = logOther (LevelOther "Rewrite")
+    logRewriteSuccess = logOther (LevelOther "RewriteSuccess")
     logSimplify = logOther (LevelOther "Simplify")
 
     prettyText :: Pretty a => a -> Text
@@ -580,7 +581,12 @@ performRewrite doTracing def mLlvmLibrary mbMaxDepth cutLabels terminalLabels pa
     showCounter = (<> " steps.") . pack . show
 
     rewriteTrace t = do
-        logRewrite $ pack $ renderDefault $ pretty t
+        let prettyT = pack $ renderDefault $ pretty t
+        logRewrite prettyT
+        case t of
+            RewriteSingleStep{} -> logRewriteSuccess prettyT
+            RewriteBranchingStep{} -> logRewriteSuccess prettyT
+            _other -> pure ()
         when doTracing $
             modify $
                 \rss@RewriteStepsState{traces} -> rss{traces = traces |> t}

diff --git a/scripts/integration-tests.sh b/scripts/integration-tests.sh
@@ -4,6 +4,11 @@ set -euxo pipefail
 K_VERSION=$(cat deps/k_release)
 PLUGIN_VERSION=$(cat deps/blockchain-k-plugin_release)
 export PATH="$(nix build github:runtimeverification/k/v$K_VERSION#k.openssl.procps --no-link  --print-build-logs --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH"
+
+if [ -f cabal.project.local ]; then
+    echo "[WARN] local cabal project configuration found"
+fi
+
 cabal update
 cabal test llvm-integration
 
@@ -20,21 +25,21 @@ for dir in $(ls -d test-*); do
     name=${dir##test-}
     echo "Running $name..."
     if [ "$name" = "a-to-f" ] || [ "$name" = "diamond" ]; then
-        SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name --time
-        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name --time
-        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time
+        SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name --time $@
+        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name --time $@
+        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
     elif [ "$name" = "vacuous" ]; then
-        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name
-        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name
+        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
+        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
     elif [ "$name" = "substitutions" ]; then
-        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name --time
-        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time
+        SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name --time $@
+        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
     elif [ "$name" = "no-evaluator" ]; then
-        SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name --time
+        SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name --time $@
     elif [ "$name" = "foundry-bug-report" ]; then
-        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time
-        SERVER="$KORE_RPC_BOOSTER --interim-simplification 100" ./runDirectoryTest.sh test-$name --time
+        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
+        SERVER="$KORE_RPC_BOOSTER --interim-simplification 100" ./runDirectoryTest.sh test-$name --time $@
     else
-        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time
+        SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
     fi
 done