mop up workaround code removing a KItem injection added by LLVM

runtimeverification · Dec 20, 2023 · fdb2f6b · fdb2f6b
1 parent 49d7a78
commit fdb2f6b
Showing 1 changed file with 2 additions and 24 deletions.
diff --git a/library/Booster/LLVM.hs b/library/Booster/LLVM.hs
@@ -3,15 +3,12 @@ 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
@@ -31,24 +28,5 @@ 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
-    -- strip away the custom injection added by the LLVM backend
-    Trace.timeIO "LLVM.simplifyTerm.decodeTerm" $ case runGet (decodeTerm def) (fromStrict binary) of
-        Injection newSort (SortApp "SortKItem" _) result
-            | newSort == sort ->
-                pure result
-            | Set.member (sortName newSort) subsorts ->
-                pure $ Injection newSort sort result
-        someTerm
-            | sortOfTerm someTerm == sort ->
-                pure someTerm
-        other -> do
-            liftIO . putStrLn $
-                "[Error] Unexpected sort after LLVM simplification: "
-                    <> show other
-                    <> " 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
+    Trace.timeIO "LLVM.simplifyTerm.decodeTerm" $
+        pure (runGet (decodeTerm def) (fromStrict binary))