From abfa9f957cb420b099ad832e9d8899a773d35235 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 10 Jan 2024 23:05:30 +1100
Subject: [PATCH] HOTFIX: restore subsort injections removed by LLVM

Terms returned from the LLVM simplification are wrapped into a
top-level `rawTerm(inj{S, SortKItem{}}(_))` which is removed
when deserialising the result term from the returned string.

However, when the returned term is of a subsort A of the required
sort B, there would be a chain of injections `A -> B -> KItem` which
is shortened out to `A -> KItem` by the LLVM simplifier, apparently.

In `simplifyTerm` we restore the required `A -> B` injection when it
is necessary, checking that `A` is indeed a subsort of `B` beforehand.
If the result sort `A` is not a subsort of the required sort `B`, an
error message is printed and the original unsimplified term is
returned.
---
 library/Booster/LLVM.hs | 28 ++++++++++++++++++++++------
 1 file changed, 22 insertions(+), 6 deletions(-)

diff --git a/library/Booster/LLVM.hs b/library/Booster/LLVM.hs
index 4b1436a00..ec17f899b 100644
--- a/library/Booster/LLVM.hs
+++ b/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