Only send unevaluated functions to LLVM (#4018)

This change steps away from maximising the terms we send to the LLVM
backend for evaluation, and only sends terms with an unevaluated
function call at the top. It addresses a particular constellation that
has been observed in downstream semantics/proofs:
* a configuration containing large data structures in cells that remain
unchanged
* a long-running sequence of rewrites that keep inserting concrete
function applications into cells required for the next rewrite step,
* and therefore require frequent configuration simplifications

Each time the configuration is simplified, the large unchanged data
structure is sent to the LLVM backend, which incurs considerable
overhead.

On the flip side, we will send each function that needs to be evaluated
individually. However, rewrites or equations will usually not create
more than a handful of new unevaluated function calls at one time, and
we will still send _nested_ unevaluated expressions together.

Also includes a logging call to measure the duration of LLVM
interactions (including argument/result conversion), and necessary code
restructuring.

---------

Co-authored-by: github-actions <[email protected]>

Author: jberthold

booster/library/Booster/LLVM.hs

@@ -6,27 +6,36 @@ module Booster.LLVM (
 ) where
 
 import Control.Monad.IO.Class (MonadIO (..))
+import Data.Aeson
 import Data.Binary.Get
 import Data.ByteString (fromStrict)
+import Data.ByteString.Char8 qualified as BS
 import Data.Map qualified as Map
 import Data.Set qualified as Set
+import Data.Text qualified as T
 
 import Booster.Definition.Base
 import Booster.LLVM.Internal qualified as Internal
+import Booster.Log
 import Booster.Pattern.Base
 import Booster.Pattern.Binary
 import Booster.Pattern.Util
-import Data.ByteString.Char8 qualified as BS
+import Booster.Util (secWithUnit, timed)
 
-simplifyBool :: MonadIO io => Internal.API -> Term -> io (Either Internal.LlvmError Bool)
-simplifyBool api trm = liftIO $ Internal.runLLVM api $ do
+simplifyBool :: LoggerMIO io => Internal.API -> Term -> io (Either Internal.LlvmError Bool)
+simplifyBool api trm = ioWithTiming $ Internal.runLLVM api $ do
     kore <- Internal.ask
     trmPtr <- Internal.marshallTerm trm
     liftIO $ kore.simplifyBool trmPtr
 
 simplifyTerm ::
-    MonadIO io => Internal.API -> KoreDefinition -> Term -> Sort -> io (Either Internal.LlvmError Term)
-simplifyTerm api def trm sort = liftIO $ Internal.runLLVM api $ do
+    LoggerMIO io =>
+    Internal.API ->
+    KoreDefinition ->
+    Term ->
+    Sort ->
+    io (Either Internal.LlvmError Term)
+simplifyTerm api def trm sort = ioWithTiming $ Internal.runLLVM api $ do
     kore <- Internal.ask
     trmPtr <- Internal.marshallTerm trm
     sortPtr <- Internal.marshallSort sort
@@ -56,3 +65,11 @@ simplifyTerm api def trm sort = liftIO $ Internal.runLLVM api $ do
     sortName (SortApp name _) = name
     sortName (SortVar name) = name
     subsorts = maybe Set.empty snd $ Map.lookup (sortName sort) def.sorts
+
+ioWithTiming :: LoggerMIO io => IO a -> io a
+ioWithTiming action = do
+    (result, time) <- liftIO $ timed action
+    withContext CtxTiming . logMessage $
+        WithJsonMessage (object ["time" .= time]) $
+            "Performed LLVM call in " <> T.pack (secWithUnit time)
+    pure result

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -395,7 +395,9 @@ llvmSimplify term = do
   where
     evalLlvm definition api cb t@(Term attributes _)
         | attributes.isEvaluated = pure t
-        | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm . withTermContext t $ do
+        | isConcrete t
+        , attributes.canBeEvaluated
+        , isFunctionApp t = withContext CtxLlvm . withTermContext t $ do
             LLVM.simplifyTerm api definition t (sortOfTerm t)
                 >>= \case
                     Left (LlvmError e) -> do
@@ -413,6 +415,10 @@ llvmSimplify term = do
         | otherwise =
             cb t
 
+    isFunctionApp :: Term -> Bool
+    isFunctionApp (SymbolApplication sym _ _) = isFunctionSymbol sym
+    isFunctionApp _ = False
+
 ----------------------------------------
 -- Interface functions
 
@@ -1065,11 +1071,11 @@ simplifyConstraint' :: LoggerMIO io => Bool -> Term -> EquationT io Term
 -- evaluateTerm.
 simplifyConstraint' recurseIntoEvalBool = \case
     t@(Term TermAttributes{canBeEvaluated} _)
-        | isConcrete t && canBeEvaluated -> withTermContext t $ do
+        | isConcrete t && canBeEvaluated -> do
             mbApi <- (.llvmApi) <$> getConfig
             case mbApi of
                 Just api ->
-                    withContext CtxLlvm $
+                    withContext CtxLlvm . withTermContext t $
                         LLVM.simplifyBool api t >>= \case
                             Left (LlvmError e) -> do
                                 withContext CtxAbort $
@@ -1086,11 +1092,10 @@ simplifyConstraint' recurseIntoEvalBool = \case
                                         pure result
                 Nothing -> if recurseIntoEvalBool then evalBool t else pure t
         | otherwise ->
-            withTermContext t $
-                if recurseIntoEvalBool then evalBool t else pure t
+            if recurseIntoEvalBool then evalBool t else pure t
   where
     evalBool :: LoggerMIO io => Term -> EquationT io Term
-    evalBool t = do
+    evalBool t = withTermContext t $ do
         prior <- getState -- save prior state so we can revert
         eqState $ put prior{termStack = mempty, changed = False}
         result <- iterateEquations BottomUp PreferFunctions t

booster/library/Booster/Util.hs

@@ -14,11 +14,14 @@ module Booster.Util (
     newTimeCache,
     pattern PrettyTimestamps,
     pattern NoPrettyTimestamps,
+    timed,
+    secWithUnit,
 ) where
 
 import Control.AutoUpdate (defaultUpdateSettings, mkAutoUpdate, updateAction, updateFreq)
 import Control.DeepSeq (NFData (..))
 import Control.Exception (bracket, catch, throwIO)
+import Control.Monad.IO.Class (MonadIO (liftIO))
 import Data.ByteString (ByteString)
 import Data.ByteString.Char8 qualified as BS
 import Data.Coerce (coerce)
@@ -31,6 +34,7 @@ import Data.Time.Clock.System (SystemTime (..), getSystemTime, systemToUTCTime)
 import Data.Time.Format
 import GHC.Generics (Generic)
 import Language.Haskell.TH.Syntax (Lift)
+import System.Clock
 import System.Directory (removeFile)
 import System.IO.Error (isDoesNotExistError)
 import System.Log.FastLogger (
@@ -42,6 +46,7 @@ import System.Log.FastLogger (
     newTimedFastLogger,
  )
 import System.Log.FastLogger.Types (FormattedTime)
+import Text.Printf
 
 newtype Flag (name :: k) = Flag Bool
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
@@ -185,14 +190,32 @@ pattern NoPrettyTimestamps = Flag False
 -- | Format time either as a human-readable date and time or as nanoseconds
 formatSystemTime :: Flag "PrettyTimestamp" -> SystemTime -> ByteString
 formatSystemTime prettyTimestamp =
-    let formatString = "%Y-%m-%dT%H:%M:%S%6Q"
+    let formatStr = "%Y-%m-%dT%H:%M:%S%6Q"
         formatter =
             if coerce prettyTimestamp
-                then formatTime defaultTimeLocale formatString . systemToUTCTime
+                then formatTime defaultTimeLocale formatStr . systemToUTCTime
                 else show . toNanoSeconds
      in BS.pack . formatter
   where
     toNanoSeconds :: SystemTime -> Integer
     toNanoSeconds MkSystemTime{systemSeconds, systemNanoseconds} =
         fromIntegral @_ @Integer systemSeconds * (10 :: Integer) ^ (9 :: Integer)
             + fromIntegral @_ @Integer systemNanoseconds
+
+------------------------------------------------------------
+-- helper for measuring durations
+
+-- returns time taken by the given action (in seconds)
+timed :: MonadIO m => m a -> m (a, Double)
+timed action = do
+    start <- liftIO $ getTime Monotonic
+    result <- action
+    stop <- liftIO $ getTime Monotonic
+    let time = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 10 ** 9
+    pure (result, time)
+
+secWithUnit :: (Floating a, Ord a, PrintfArg a) => a -> String
+secWithUnit x
+    | x > 0.1 = printf "%.2fs" x
+    | x > 0.0001 = printf "%.3fms" $ x * 10 ** 3
+    | otherwise = printf "%.1fμs" $ x * 10 ** 6

booster/test/llvm-integration/LLVM.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 
+{-# OPTIONS -fno-warn-orphans #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2023
 License     : BSD-3-Clause
@@ -19,6 +21,7 @@ import Data.List (foldl1', isInfixOf, nub)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
+import Data.Proxy
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
@@ -40,7 +43,9 @@ import Booster.Definition.Attributes.Base
 import Booster.Definition.Base
 import Booster.LLVM qualified as LLVM
 import Booster.LLVM.Internal qualified as Internal
+import Booster.Log
 import Booster.Pattern.Base
+import Booster.Pattern.Pretty
 import Booster.SMT.Base (SExpr (..), SMTId (..))
 import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Syntax.Json.Internalise (pattern AllowAlias, pattern IgnoreSubsorts)
@@ -109,6 +114,11 @@ llvmSpec =
 --------------------------------------------------
 -- individual hedgehog property tests and helpers
 
+instance LoggerMIO (PropertyT IO) where
+    getLogger = pure $ Logger $ \_ -> pure ()
+    getPrettyModifiers = pure $ ModifiersRep @'[] Proxy
+    withLogger _ = id
+
 boolsRemainProp
     , compareNumbersProp
     , simplifyComparisonProp ::

booster/tools/booster/Stats.hs

@@ -2,11 +2,12 @@ module Stats (
     newStats,
     addStats,
     finaliseStats,
-    timed,
-    secWithUnit,
     RequestStats (..),
     StatsVar,
     MethodTiming (..),
+    -- re-export
+    timed,
+    secWithUnit,
 ) where
 
 import Control.Concurrent.MVar (MVar, modifyMVar_, newMVar, readMVar)
@@ -18,11 +19,11 @@ import Data.Text (pack)
 import Deriving.Aeson
 import GHC.Generics ()
 import Prettyprinter
-import System.Clock
 import Text.Printf
 
 import Booster.Log
 import Booster.Prettyprinter
+import Booster.Util (secWithUnit, timed)
 import Kore.JsonRpc.Types (APIMethod)
 
 -- | Statistics for duration measurement time series (in seconds)
@@ -62,12 +63,6 @@ instance (Floating a, PrintfArg a, Ord a) => Pretty (RequestStats a) where
       where
         withUnit = pretty . secWithUnit
 
-secWithUnit :: (Floating a, Ord a, PrintfArg a) => a -> String
-secWithUnit x
-    | x > 0.1 = printf "%.2fs" x
-    | x > 0.0001 = printf "%.3fms" $ x * 10 ** 3
-    | otherwise = printf "%.1fμs" $ x * 10 ** 6
-
 -- internal helper type
 -- all values are in seconds
 data Stats' = Stats'
@@ -138,15 +133,6 @@ addStats statVar MethodTiming{method, time, koreTime} =
 newStats :: MonadIO m => m (MVar (Map APIMethod Stats'))
 newStats = liftIO $ newMVar Map.empty
 
--- returns time taken by the given action (in seconds)
-timed :: MonadIO m => m a -> m (a, Double)
-timed action = do
-    start <- liftIO $ getTime Monotonic
-    result <- action
-    stop <- liftIO $ getTime Monotonic
-    let time = fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 10 ** 9
-    pure (result, time)
-
 newtype FinalStats = FinalStats (Map APIMethod (RequestStats Double))
     deriving stock (Eq, Show)
     deriving newtype (FromJSON, ToJSON)