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

Author: rv-auditor

booster/cbits/kllvm-c.h

@@ -4,8 +4,10 @@
 #ifndef __cplusplus
 #include <stdbool.h>
 #include <stddef.h>
+#include <stdint.h>
 #else
 #include <cstddef>
+#include <cstdint>
 #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

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

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

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

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

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

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