Fix incorrect KMap injections, received from the LLVM library

library/Booster/Pattern/Binary.hs

@@ -192,21 +192,21 @@ popStackSorts n =
         BSort s -> pure s
         _ -> fail "popping a non sort"
 
-lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Maybe Symbol)
+lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Either Symbol (Maybe Symbol))
 lookupKoreDefinitionSymbol name = DecodeM $ do
     (_, mDef) <- ask
     pure $ case mDef of
         -- return a symbol with dummy attributes if no definition is supplied.
         -- this should be used for testing ONLY!
         Nothing ->
-            Just $
+            Left $
                 Symbol
                     name
                     []
                     []
                     (SortApp "UNKNOWN" [])
                     (SymbolAttributes PartialFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CannotBeEvaluated Nothing)
-        Just def -> Map.lookup name $ symbols def
+        Just def -> Right $ Map.lookup name $ symbols def
 
 {- | Successively decodes items from the given "block" of bytes,
   branching on the initial tag of the item.
@@ -299,12 +299,20 @@ decodeBlock mbSize = do
     mkSymbolApplication "inj" _ bs = argError "Injection" [BTerm undefined] bs
     mkSymbolApplication name sorts bs =
         lookupKoreDefinitionSymbol name >>= \case
-            Just symbol@Symbol{sortVars} -> do
+            -- testing case when we don't have a KoreDefinition
+            Left symbol@Symbol{sortVars} -> do
                 args <- forM bs $ \case
                     BTerm trm -> pure trm
                     _ -> fail "Expecting term"
                 pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
-            Nothing -> fail $ "Unknown symbol " <> show name
+            Right (Just symbol@Symbol{sortVars, argSorts}) -> do
+                args <- forM (zip argSorts bs) $ \case
+                    -- temporarily fix injections until https://github.com/runtimeverification/llvm-backend/issues/886 is closed
+                    (srt, BTerm (Injection from _to trm)) -> pure $ Injection from srt trm
+                    (srt, BTerm trm) -> if sortOfTerm trm /= srt then fail "Term has incorrect sort" else pure trm
+                    _ -> fail "Expecting term"
+                pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
+            Right Nothing -> fail $ "Unknown symbol " <> show name
 
     argError cons expectedArgs receivedArgs =
         fail $

test/llvm-integration/LLVM.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QuasiQuotes #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2023
@@ -41,7 +42,7 @@ import Booster.Pattern.Base
 import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Syntax.Json.Internalise (pattern AllowAlias, pattern IgnoreSubsorts)
 import Booster.Syntax.Json.Internalise qualified as Syntax
-import Booster.Syntax.ParsedKore.Internalise (buildDefinitions)
+import Booster.Syntax.ParsedKore.Internalise (buildDefinitions, symb)
 import Booster.Syntax.ParsedKore.Parser (parseDefinition)
 import Kore.Syntax.Json.Types qualified as Syntax
 import System.Info (os)
@@ -90,6 +91,10 @@ llvmSpec =
                 it "should work with latin-1strings" $
                     hedgehog . propertyTest . latin1Prop
 
+            describe "Correct sort injections in non KItem maps" $
+                it "should work with latin-1strings" $
+                    hedgehog . propertyTest . mapKItemInjProp
+
 --------------------------------------------------
 -- individual hedgehog property tests and helpers
 
@@ -147,6 +152,41 @@ latin1Prop api = property $ do
                 | otherwise -> error $ "Unexpected sort " <> show s
             otherTerm -> error $ "Unexpected term " <> show otherTerm
 
+mapKItemInjProp :: Internal.API -> Property
+mapKItemInjProp api = property $ do
+    let k = wrapIntTerm 1
+    let v = wrapIntTerm 2
+    LLVM.simplifyTerm api testDef (update k v) (SortApp "SortMapValToVal" []) === singleton k v
+  where
+    update k v =
+        SymbolApplication
+            (defSymbols Map.! "LblMapValToVal'Coln'primitiveUpdate")
+            []
+            [ SymbolApplication
+                (defSymbols Map.! "Lbl'Stop'MapValToVal")
+                []
+                []
+            , k
+            , v
+            ]
+
+    singleton k v =
+        SymbolApplication
+            (defSymbols Map.! "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'")
+            []
+            [k, v]
+
+    wrapIntTerm :: Int -> Term
+    wrapIntTerm i =
+        SymbolApplication
+            (defSymbols Map.! "inj")
+            [SortApp "SortWrappedInt" [], SortApp "SortVal" []]
+            [ SymbolApplication
+                (defSymbols Map.! "LblwrapInt")
+                []
+                [intTerm i]
+            ]
+
 ------------------------------------------------------------
 
 runKompile :: IO ()
@@ -3470,4 +3510,20 @@ defSymbols =
                         }
                 }
             )
+        ,
+            ( "LblwrapInt"
+            , [symb| symbol LblwrapInt{}(SortInt{}) : SortWrappedInt{} [constructor{}(), functional{}(), injective{}()] |]
+            )
+        ,
+            ( "Lbl'Stop'MapValToVal"
+            , [symb| symbol Lbl'Stop'MapValToVal{}() : SortMapValToVal{} [function{}(), functional{}(), total{}()] |]
+            )
+        ,
+            ( "LblMapValToVal'Coln'primitiveUpdate"
+            , [symb| symbol LblMapValToVal'Coln'primitiveUpdate{}(SortMapValToVal{}, SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("MapValToVal:primitiveUpdate"), total{}()] |]
+            )
+        ,
+            ( "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'"
+            , [symb| symbol Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'{}(SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("_Val2Val|->_"), total{}()] |]
+            )
         ]

test/llvm-integration/definition/llvm.k

@@ -5,6 +5,7 @@ module LLVM
   imports MAP
   imports SET
   imports K-EQUAL
+  imports MAP-VAL-TO-VAL
 
   syntax Num ::= Even | Odd
   syntax Even ::= Zero() | Two() | Four() | Six() | Eight() | Ten()
@@ -39,3 +40,45 @@ module LLVM
   rule div2(Ten()) => Five()
 
 endmodule
+
+module MAP-VAL-TO-VAL
+  imports WRAPPED-INT
+
+  syntax Val ::= WrappedInt
+ // -----------------------
+
+  syntax MapValToVal [hook(MAP.Map)]
+  syntax MapValToVal ::= MapValToVal MapValToVal
+         [ left, function, hook(MAP.concat), klabel(_MapValToVal_),
+           symbol, assoc, comm, unit(.MapValToVal), element(_Val2Val|->_)
+         ]
+  syntax MapValToVal ::= ".MapValToVal"
+         [function, total, hook(MAP.unit),klabel(.MapValToVal), symbol]
+  syntax MapValToVal ::= Val "Val2Val|->" Val
+         [function, total, hook(MAP.element), klabel(_Val2Val|->_), symbol]
+
+  syntax MapValToVal ::= MapValToVal "[" key: Val "<-" value: Val "]" [function, total, klabel(MapVal2Val:update), symbol, hook(MAP.update), prefer]
+
+  syntax priorities _Val2Val|->_ > _MapValToVal_ .MapValToVal
+  syntax non-assoc _Val2Val|->_
+
+  syntax MapValToVal ::= MapValToVal "{{" key: Val "<-" value: Val "}}"
+                 [ function, total, klabel(MapValToVal:primitiveUpdate), symbol,
+                   prefer
+                 ]
+  rule M:MapValToVal {{ Key:Val <- Value:Val }}
+      => M[Key <- Value]
+
+endmodule
+
+module WRAPPED-INT
+  imports INT
+
+  syntax WrappedInt ::= wrap(Int)  [symbol, klabel(wrapInt)]
+  // -------------------------------------------------------
+
+  syntax Int ::= unwrap(WrappedInt)  [function, total, injective, symbol, klabel(unwrapInt)]
+  // ---------------------------------------------------------------------------------------
+  rule unwrap(wrap(A:Int)) => A
+endmodule
+