From d2e94cc9b17d5806552612947f743acb2873538c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 30 Jun 2025 11:45:13 +1000 Subject: [PATCH 1/7] quick test calling kore.collect (kllvm_free_all_memory) after simplifyBool calls --- booster/library/Booster/LLVM.hs | 4 +++- booster/library/Booster/LLVM/Internal.hs | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/LLVM.hs b/booster/library/Booster/LLVM.hs index 384edccf87..c261e82eb6 100644 --- a/booster/library/Booster/LLVM.hs +++ b/booster/library/Booster/LLVM.hs @@ -26,7 +26,9 @@ simplifyBool :: LoggerMIO io => Internal.API -> Term -> io (Either Internal.Llvm simplifyBool api trm = ioWithTiming $ Internal.runLLVM api $ do kore <- Internal.ask trmPtr <- Internal.marshallTerm trm - liftIO $ kore.simplifyBool trmPtr + result <- liftIO $ kore.simplifyBool trmPtr + liftIO kore.collect + pure result simplifyTerm :: LoggerMIO io => diff --git a/booster/library/Booster/LLVM/Internal.hs b/booster/library/Booster/LLVM/Internal.hs index efea368e6c..e982dded49 100644 --- a/booster/library/Booster/LLVM/Internal.hs +++ b/booster/library/Booster/LLVM/Internal.hs @@ -118,7 +118,7 @@ withDLib dlib = Linker.withDL dlib [Linker.RTLD_LAZY] runLLVM :: API -> LLVM a -> IO a runLLVM api (LLVM m) = - withMVar api.mutex $ const $ runReaderT m api + withMVar api.mutex $ const $ runReaderT m api -- TODO add <* api.collect here mkAPI :: Linker.DL -> IO API mkAPI dlib = flip runReaderT dlib $ do From 2db923c170721c34739077a1b0ed120f36d651cd Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 12:53:42 +1000 Subject: [PATCH 2/7] Update kllvm-c.h and binding processing --- booster/cbits/kllvm-c.h | 23 +++++++- booster/cbits/stdint.h | 71 ++++++++++++++++++++++++ booster/hs-backend-booster.cabal | 3 +- booster/library/Booster/LLVM/Internal.hs | 4 +- 4 files changed, 96 insertions(+), 5 deletions(-) create mode 100644 booster/cbits/stdint.h diff --git a/booster/cbits/kllvm-c.h b/booster/cbits/kllvm-c.h index 6e816e2eee..819d762272 100644 --- a/booster/cbits/kllvm-c.h +++ b/booster/cbits/kllvm-c.h @@ -4,8 +4,10 @@ #ifndef __cplusplus #include #include +#include #else #include +#include #endif #ifdef __cplusplus @@ -75,7 +77,7 @@ typedef struct kore_sort kore_sort; typedef struct kore_symbol kore_symbol; typedef struct block block; -/* KOREPattern */ +/* kore_pattern */ char *kore_pattern_dump(kore_pattern const *); @@ -127,8 +129,11 @@ void kore_simplify( void kore_simplify_binary( kore_error *, char *, size_t, kore_sort const *, char **, size_t *); +block *take_steps(int64_t depth, block *term); -/* KORESort */ +void init_static_objects(void); + +/* kore_sort */ char *kore_sort_dump(kore_sort const *); @@ -142,7 +147,7 @@ bool kore_sort_is_k(kore_sort const *); kore_sort *kore_composite_sort_new(char const *); void kore_composite_sort_add_argument(kore_sort const *, kore_sort const *); -/* KORESymbol */ +/* kore_symbol */ kore_symbol *kore_symbol_new(char const *); @@ -159,6 +164,18 @@ void kllvm_free_all_memory(void); bool kllvm_mutable_bytes_enabled(void); +/* Definitions */ + +/** + * Parse the given KORE definition, then if any of its axioms have a `label` + * attribute that matches the supplied label, return the name of the function + * symbol that attempts matching a pattern against that axiom (and will + * therefore populate the backend's global matching log). + * + * If no such axiom exists, return `nullptr`. + */ +char *kore_match_function_name(char const *defn_path, char const *label); + #ifdef __cplusplus } #endif diff --git a/booster/cbits/stdint.h b/booster/cbits/stdint.h new file mode 100644 index 0000000000..c0c4fbffbc --- /dev/null +++ b/booster/cbits/stdint.h @@ -0,0 +1,71 @@ +/* minimal stdint.h according to POSIX, see + https://pubs.opengroup.org/onlinepubs/009695399/basedefs/stdint.h.html +*/ + +#ifndef _STDINT_H +#define _STDINT_H + +typedef signed char int8_t; +typedef short int int16_t; +typedef int int32_t; +typedef long long int int64_t; + +typedef unsigned char uint8_t; +typedef unsigned short int uint16_t; +typedef unsigned int uint32_t; +typedef unsigned long long int uint64_t; + +typedef int8_t int_least8_t; +typedef int16_t int_least16_t; +typedef int32_t int_least32_t; +typedef int64_t int_least64_t; + +typedef uint8_t uint_least8_t; +typedef uint16_t uint_least16_t; +typedef uint32_t uint_least32_t; +typedef uint64_t uint_least64_t; + +typedef int8_t int_fast8_t; +typedef int16_t int_fast16_t; +typedef int32_t int_fast32_t; +typedef int64_t int_fast64_t; + +typedef uint8_t uint_fast8_t; +typedef uint16_t uint_fast16_t; +typedef uint32_t uint_fast32_t; +typedef uint64_t uint_fast64_t; + +#ifdef _WIN64 +typedef signed __int64 intptr_t; +typedef unsigned __int64 uintptr_t; +#else +typedef signed int intptr_t; +typedef unsigned int uintptr_t; +#endif + +typedef int64_t intmax_t; +typedef uint64_t uintmax_t; + +#define INT8_MIN (-127 - 1) +#define INT16_MIN (-32767 - 1) +#define INT32_MIN (-2147483647 - 1) +#define INT64_MIN (-9223372036854775807LL - 1) + +#define INT8_MAX 127 +#define INT16_MAX 32767 +#define INT32_MAX 2147483647 +#define INT64_MAX 9223372036854775807LL + +#define UINT8_MAX 255 +#define UINT16_MAX 65535 +#define UINT32_MAX 4294967295U +#define UINT64_MAX 18446744073709551615ULL + +#define INTPTR_MIN INT64_MIN +#define INTPTR_MAX INT64_MAX +#define UINTPTR_MAX UINT64_MAX +#define INTMAX_MIN INT64_MIN +#define INTMAX_MAX INT64_MAX +#define UINTMAX_MAX UINT64_MAX + +#endif diff --git a/booster/hs-backend-booster.cabal b/booster/hs-backend-booster.cabal index b06865736b..e3722ab1fb 100644 --- a/booster/hs-backend-booster.cabal +++ b/booster/hs-backend-booster.cabal @@ -1,6 +1,6 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.36.0. +-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack @@ -217,6 +217,7 @@ extra-source-files: cbits/kllvm-c.h cbits/stdbool.h cbits/stddef.h + cbits/stdint.h source-repository head type: git diff --git a/booster/library/Booster/LLVM/Internal.hs b/booster/library/Booster/LLVM/Internal.hs index e982dded49..b5de9d2598 100644 --- a/booster/library/Booster/LLVM/Internal.hs +++ b/booster/library/Booster/LLVM/Internal.hs @@ -33,7 +33,7 @@ import Data.Data (Data) import Data.HashMap.Strict (HashMap) import Data.HashMap.Strict qualified as HM import Data.IORef (IORef, modifyIORef', newIORef, readIORef) -import Foreign (ForeignPtr, finalizeForeignPtr, newForeignPtr, withForeignPtr) +import Foreign (ForeignPtr, Int64, finalizeForeignPtr, newForeignPtr, withForeignPtr) import Foreign qualified import Foreign.C qualified as C import Foreign.C.Types (CSize (..)) @@ -52,12 +52,14 @@ data KoreSymbol data KoreError data Block type SizeT = CSize +type Int64T = Foreign.Int64 type KorePatternPtr = ForeignPtr KorePattern type KoreSymbolPtr = ForeignPtr KoreSymbol type KoreSortPtr = ForeignPtr KoreSort type KoreErrorPtr = ForeignPtr KoreError + $(dynamicBindings "./cbits/kllvm-c.h") newtype KoreStringPatternAPI = KoreStringPatternAPI From 6ff100797326870b32f166ca31664d849c73655c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 12:54:34 +1000 Subject: [PATCH 3/7] EXPERIMENT: add reset_munmap_all_arenas to LLVM API and call it after each request --- booster/cbits/kllvm-c.h | 1 + booster/library/Booster/JsonRpc.hs | 8 ++++++-- booster/library/Booster/LLVM.hs | 4 ++++ booster/library/Booster/LLVM/Internal.hs | 5 ++++- 4 files changed, 15 insertions(+), 3 deletions(-) diff --git a/booster/cbits/kllvm-c.h b/booster/cbits/kllvm-c.h index 819d762272..27a5c8813d 100644 --- a/booster/cbits/kllvm-c.h +++ b/booster/cbits/kllvm-c.h @@ -159,6 +159,7 @@ void kore_symbol_add_formal_argument(kore_symbol *, kore_sort const *); void kllvm_init(void); void kllvm_free_all_memory(void); +void reset_munmap_all_arenas(void); /* Sort-specific functions */ diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 0b1a2102f4..aeb1b2fcb1 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -19,6 +19,7 @@ module Booster.JsonRpc ( import Control.Applicative ((<|>)) import Control.Concurrent (MVar, putMVar, readMVar, takeMVar) import Control.Monad +import Control.Monad.Extra (whenJust) import Control.Monad.IO.Class import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT) import Crypto.Hash (SHA256 (..), hashWith) @@ -41,7 +42,7 @@ import Booster.CLOptions (RewriteOptions (..)) import Booster.Definition.Attributes.Base (getUniqueId, uniqueId) import Booster.Definition.Base (KoreDefinition (..)) import Booster.Definition.Base qualified as Definition (RewriteRule (..)) -import Booster.LLVM as LLVM (API) +import Booster.LLVM as LLVM (API, llvmReset) import Booster.Log import Booster.Pattern.ApplyEquations qualified as ApplyEquations import Booster.Pattern.Base (Pattern (..), Sort (SortApp)) @@ -435,9 +436,12 @@ respond stateVar request = withModule mbMainModule action = do state <- liftIO $ readMVar stateVar let mainName = fromMaybe state.defaultMain mbMainModule + purgeLlvmLib = whenJust state.mLlvmLibrary llvmReset case Map.lookup mainName state.definitions of Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName - Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions) + Just d -> + action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions) <* purgeLlvmLib + handleSmtError :: JsonRpcHandler handleSmtError = JsonRpcHandler $ \case diff --git a/booster/library/Booster/LLVM.hs b/booster/library/Booster/LLVM.hs index c261e82eb6..c8a8422145 100644 --- a/booster/library/Booster/LLVM.hs +++ b/booster/library/Booster/LLVM.hs @@ -1,4 +1,5 @@ module Booster.LLVM ( + llvmReset, simplifyBool, simplifyTerm, Internal.API, @@ -22,6 +23,9 @@ import Booster.Pattern.Binary import Booster.Pattern.Util import Booster.Util (secWithUnit, timed) +llvmReset :: LoggerMIO io => Internal.API -> io () +llvmReset api = liftIO api.munmap -- releases thread-local mmap'ed memory in the LLVM backend + simplifyBool :: LoggerMIO io => Internal.API -> Term -> io (Either Internal.LlvmError Bool) simplifyBool api trm = ioWithTiming $ Internal.runLLVM api $ do kore <- Internal.ask diff --git a/booster/library/Booster/LLVM/Internal.hs b/booster/library/Booster/LLVM/Internal.hs index b5de9d2598..488fb2830f 100644 --- a/booster/library/Booster/LLVM/Internal.hs +++ b/booster/library/Booster/LLVM/Internal.hs @@ -106,6 +106,7 @@ data API = API , simplifyBool :: KorePatternPtr -> IO (Either LlvmError Bool) , simplify :: KorePatternPtr -> KoreSortPtr -> IO (Either LlvmError ByteString) , collect :: IO () + , munmap :: IO () , mutex :: MVar () } @@ -276,6 +277,8 @@ mkAPI dlib = flip runReaderT dlib $ do pure $ Right result else Left . LlvmError <$> errorMessage errPtr + munmap <- resetMunmapAllArenas -- HACK. Adjust name after llvm-backend dependency upgrade + mutableBytesEnabled <- kllvmMutableBytesEnabled `catch` \(_ :: IOException) -> pure (pure 0) liftIO $ @@ -285,7 +288,7 @@ mkAPI dlib = flip runReaderT dlib $ do "[Warn] Using an LLVM backend compiled with --llvm-mutable-bytes (unsound byte array semantics)" mutex <- liftIO $ newMVar () - pure API{patt, symbol, sort, simplifyBool, simplify, collect, mutex} + pure API{patt, symbol, sort, simplifyBool, simplify, collect, munmap, mutex} ask :: LLVM API ask = LLVM Reader.ask From 6dea5d5e406d7b32a71c8121e7e80170e2371cbb Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 15:15:32 +1000 Subject: [PATCH 4/7] include LLVMAPI.collect in runLLVM routine --- booster/library/Booster/LLVM.hs | 5 +---- booster/library/Booster/LLVM/Internal.hs | 2 +- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/booster/library/Booster/LLVM.hs b/booster/library/Booster/LLVM.hs index c8a8422145..5f379ec649 100644 --- a/booster/library/Booster/LLVM.hs +++ b/booster/library/Booster/LLVM.hs @@ -30,9 +30,7 @@ simplifyBool :: LoggerMIO io => Internal.API -> Term -> io (Either Internal.Llvm simplifyBool api trm = ioWithTiming $ Internal.runLLVM api $ do kore <- Internal.ask trmPtr <- Internal.marshallTerm trm - result <- liftIO $ kore.simplifyBool trmPtr - liftIO kore.collect - pure result + liftIO $ kore.simplifyBool trmPtr simplifyTerm :: LoggerMIO io => @@ -46,7 +44,6 @@ simplifyTerm api def trm sort = ioWithTiming $ Internal.runLLVM api $ do trmPtr <- Internal.marshallTerm trm sortPtr <- Internal.marshallSort sort mbinary <- liftIO $ kore.simplify trmPtr sortPtr - liftIO kore.collect case mbinary of Left err -> pure $ Left err Right binary -> do diff --git a/booster/library/Booster/LLVM/Internal.hs b/booster/library/Booster/LLVM/Internal.hs index 488fb2830f..da55cec847 100644 --- a/booster/library/Booster/LLVM/Internal.hs +++ b/booster/library/Booster/LLVM/Internal.hs @@ -121,7 +121,7 @@ withDLib dlib = Linker.withDL dlib [Linker.RTLD_LAZY] runLLVM :: API -> LLVM a -> IO a runLLVM api (LLVM m) = - withMVar api.mutex $ const $ runReaderT m api -- TODO add <* api.collect here + withMVar api.mutex $ const (runReaderT m api <* api.collect) mkAPI :: Linker.DL -> IO API mkAPI dlib = flip runReaderT dlib $ do From 8e88cd595a69b887f9a0a89293922c997fb25267 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 15:16:17 +1000 Subject: [PATCH 5/7] fml --- booster/library/Booster/JsonRpc.hs | 1 - booster/library/Booster/LLVM/Internal.hs | 2 -- 2 files changed, 3 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index aeb1b2fcb1..44f9180a60 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -442,7 +442,6 @@ respond stateVar request = Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions) <* purgeLlvmLib - handleSmtError :: JsonRpcHandler handleSmtError = JsonRpcHandler $ \case SMT.GeneralSMTError err -> runtimeError "problem" err diff --git a/booster/library/Booster/LLVM/Internal.hs b/booster/library/Booster/LLVM/Internal.hs index da55cec847..694483e2a2 100644 --- a/booster/library/Booster/LLVM/Internal.hs +++ b/booster/library/Booster/LLVM/Internal.hs @@ -59,7 +59,6 @@ type KoreSymbolPtr = ForeignPtr KoreSymbol type KoreSortPtr = ForeignPtr KoreSort type KoreErrorPtr = ForeignPtr KoreError - $(dynamicBindings "./cbits/kllvm-c.h") newtype KoreStringPatternAPI = KoreStringPatternAPI @@ -278,7 +277,6 @@ mkAPI dlib = flip runReaderT dlib $ do else Left . LlvmError <$> errorMessage errPtr munmap <- resetMunmapAllArenas -- HACK. Adjust name after llvm-backend dependency upgrade - mutableBytesEnabled <- kllvmMutableBytesEnabled `catch` \(_ :: IOException) -> pure (pure 0) liftIO $ From 6e813d2c278d0b035d27538d375228e58cdd05dc Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 15:49:36 +1000 Subject: [PATCH 6/7] work around missing git in kontrol performance script, remove stray fi --- scripts/performance-tests-kontrol.sh | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scripts/performance-tests-kontrol.sh b/scripts/performance-tests-kontrol.sh index 239895e593..30f3e034fe 100755 --- a/scripts/performance-tests-kontrol.sh +++ b/scripts/performance-tests-kontrol.sh @@ -96,11 +96,11 @@ sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/test uv lock feature_shell() { - GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend $SCRIPT_DIR/../ --ignore-environment --command bash -c "$1" + GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend $SCRIPT_DIR/../ --command bash -c "$1" } master_shell() { - GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend github:runtimeverification/haskell-backend/$MASTER_COMMIT --ignore-environment --command bash -c "$1" + GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend github:runtimeverification/haskell-backend/$MASTER_COMMIT --command bash -c "$1" } # kompile Kontrol's K dependencies @@ -149,4 +149,3 @@ fi cd $SCRIPT_DIR python3 compare.py logs/kontrol-$KONTROL_VERSION-$FEATURE_BRANCH_NAME.log logs/kontrol-$KONTROL_VERSION-master-$MASTER_COMMIT_SHORT.log > logs/kontrol-$KONTROL_VERSION-master-$MASTER_COMMIT_SHORT-$FEATURE_BRANCH_NAME-compare -fi From fc58e10f090f99cf047e300e7d10853aef59e0b0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 2 Jul 2025 20:17:28 +1000 Subject: [PATCH 7/7] add back --ignore-environment to performance test script --- scripts/performance-tests-kontrol.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/performance-tests-kontrol.sh b/scripts/performance-tests-kontrol.sh index 30f3e034fe..2fcb244e68 100755 --- a/scripts/performance-tests-kontrol.sh +++ b/scripts/performance-tests-kontrol.sh @@ -96,11 +96,11 @@ sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/test uv lock feature_shell() { - GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend $SCRIPT_DIR/../ --command bash -c "$1" + GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend $SCRIPT_DIR/../ --ignore-environment --command bash -c "$1" } master_shell() { - GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend github:runtimeverification/haskell-backend/$MASTER_COMMIT --command bash -c "$1" + GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend github:runtimeverification/haskell-backend/$MASTER_COMMIT --ignore-environment --command bash -c "$1" } # kompile Kontrol's K dependencies