Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

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)