HOTFIX: restore subsort injections removed by LLVM

library/Booster/LLVM.hs

@@ -1,18 +1,17 @@
-{- |
-Copyright   : (c) Runtime Verification, 2023
-License     : BSD-3-Clause
--}
 module Booster.LLVM (simplifyBool, simplifyTerm) where
 
 import Control.Monad.IO.Class (MonadIO (..))
 import Data.Binary.Get
 import Data.ByteString (fromStrict)
+import Data.Map qualified as Map
+import Data.Set qualified as Set
 import System.IO.Unsafe (unsafePerformIO)
 
 import Booster.Definition.Base
 import Booster.LLVM.Internal qualified as Internal
 import Booster.Pattern.Base
 import Booster.Pattern.Binary
+import Booster.Pattern.Util
 import Booster.Trace qualified as Trace
 
 simplifyBool :: Internal.API -> Term -> Bool
@@ -32,5 +31,22 @@ simplifyTerm api def trm sort = unsafePerformIO $ Internal.runLLVM api $ do
     binary <- liftIO $ kore.simplify trmPtr sortPtr
     liftIO kore.collect
     Trace.traceIO $ Internal.LlvmVar (Internal.somePtr trmPtr) trm
-    Trace.timeIO "LLVM.simplifyTerm.decodeTerm" $
-        pure (runGet (decodeTerm def) (fromStrict binary))
+    -- strip away the custom injection added by the LLVM backend
+    Trace.timeIO "LLVM.simplifyTerm.decodeTerm" $ case runGet (decodeTerm def) (fromStrict binary) of
+        result
+            | sortOfTerm result == sort ->
+                pure result
+            | newSort@(SortApp name _) <- sortOfTerm result
+            , Set.member name subsorts ->
+                pure $ Injection newSort sort result
+            | otherwise -> do
+                liftIO . putStrLn $
+                    "[Error] LLVM simplification returned sort  "
+                        <> show (sortOfTerm result)
+                        <> ". Expected sort "
+                        <> show sort
+                pure trm
+  where
+    sortName (SortApp name _) = name
+    sortName (SortVar name) = name
+    subsorts = maybe Set.empty snd $ Map.lookup (sortName sort) def.sorts