diff --git a/booster/cbits/kllvm-c.h b/booster/cbits/kllvm-c.h index 6e816e2eee..27a5c8813d 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 *); @@ -154,11 +159,24 @@ 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 */ 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/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 0b1a2102f4..44f9180a60 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,11 @@ 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 384edccf87..5f379ec649 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 @@ -40,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 efea368e6c..694483e2a2 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,6 +52,7 @@ data KoreSymbol data KoreError data Block type SizeT = CSize +type Int64T = Foreign.Int64 type KorePatternPtr = ForeignPtr KorePattern type KoreSymbolPtr = ForeignPtr KoreSymbol @@ -104,6 +105,7 @@ data API = API , simplifyBool :: KorePatternPtr -> IO (Either LlvmError Bool) , simplify :: KorePatternPtr -> KoreSortPtr -> IO (Either LlvmError ByteString) , collect :: IO () + , munmap :: IO () , mutex :: MVar () } @@ -118,7 +120,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 <* api.collect) mkAPI :: Linker.DL -> IO API mkAPI dlib = flip runReaderT dlib $ do @@ -274,6 +276,7 @@ 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 $ @@ -283,7 +286,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 diff --git a/scripts/performance-tests-kontrol.sh b/scripts/performance-tests-kontrol.sh index 239895e593..2fcb244e68 100755 --- a/scripts/performance-tests-kontrol.sh +++ b/scripts/performance-tests-kontrol.sh @@ -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