Custom hooked Map externalisation

library/Booster/Definition/Util.hs

@@ -24,7 +24,7 @@ import Data.ByteString.Char8 (ByteString)
 import Data.ByteString.Char8 qualified as BS
 import Data.List.Extra (sortOn)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (catMaybes, fromMaybe)
 import Data.Set qualified as Set
 import Data.Text (Text)
 import GHC.Generics (Generic)
@@ -34,13 +34,15 @@ import Prettyprinter.Render.String qualified as Pretty (renderString)
 
 import Booster.Definition.Attributes.Base
 import Booster.Definition.Base
+import Booster.Pattern.Base (Symbol (..), sortName)
 import Booster.Pattern.Index (TermIndex (..))
 import Booster.Prettyprinter
 import Booster.Util
 
 data Summary = Summary
     { file :: FilePath
-    , modNames, sortNames, symbolNames :: [ByteString]
+    , modNames, sortNames :: [ByteString]
+    , symbolSignatures :: [(ByteString, [ByteString], Maybe ByteString)]
     , subSorts :: Map.Map ByteString [ByteString]
     , axiomCount, preserveDefinednessCount, containAcSymbolsCount :: Int
     , functionRuleCount, simplificationCount, predicateSimplificationCount :: Int
@@ -58,7 +60,9 @@ mkSummary file def =
         { file
         , modNames = Map.keys def.modules
         , sortNames = Map.keys def.sorts
-        , symbolNames = Map.keys def.symbols
+        , symbolSignatures =
+            map (\symbol -> (symbol.name, catMaybes (map sortName symbol.argSorts), sortName symbol.resultSort)) $
+                Map.elems def.symbols
         , subSorts = Map.map (Set.toList . snd) def.sorts
         , axiomCount = length $ concat $ concatMap Map.elems (Map.elems def.rewriteTheory)
         , preserveDefinednessCount =
@@ -94,7 +98,7 @@ instance Pretty Summary where
         Pretty.vsep $
             [ list prettyLabel "Modules" summary.modNames
             , list prettyLabel "Sorts" summary.sortNames
-            , list prettyLabel "Symbols" summary.symbolNames
+            , list prettySymbolSignature "Symbols" summary.symbolSignatures
             , "Axioms: " <> pretty summary.axiomCount
             , "Axioms preserving definedness: " <> pretty summary.preserveDefinednessCount
             , "Axioms containing AC symbols: " <> pretty summary.containAcSymbolsCount
@@ -132,6 +136,11 @@ instance Pretty Summary where
 
         prettyLabel = either error (pretty . BS.unpack) . decodeLabel
 
+        prettySymbolSignature (name, argSortNames, resultSortName) =
+            let prettyResultSortName = pretty . BS.unpack $ maybe "" ("->" <>) resultSortName
+                prettyArgSortNames = pretty . BS.unpack $ "{" <> BS.intercalate "," argSortNames <> "}"
+             in prettyLabel name <> prettyArgSortNames <> prettyResultSortName
+
         prettyTermIndex Anything = "Anything"
         prettyTermIndex (TopSymbol sym) = prettyLabel sym
         prettyTermIndex None = "None"

library/Booster/Pattern/Base.hs

@@ -69,6 +69,11 @@ data Sort
 pattern SortBool :: Sort
 pattern SortBool = SortApp "SortBool" []
 
+sortName :: Sort -> Maybe SortName
+sortName = \case
+    SortApp name _args -> Just name
+    SortVar _ -> Nothing
+
 -- | A variable for symbolic execution or for terms in a rule.
 data Variable = Variable
     { variableSort :: Sort
@@ -271,9 +276,21 @@ externaliseKmapUnsafe def keyVals rest =
                 s
                 keyVals
   where
-    unit = SymbolApplication (stripCollectionMetadata $ unitSymbol $ KMapMeta def) [] []
-    k |-> v = SymbolApplication (stripCollectionMetadata $ kmapElementSymbol def) [] [k, v]
-    a `con` b = SymbolApplication (stripCollectionMetadata $ concatSymbol $ KMapMeta def) [] [a, b]
+    -- unit = SymbolApplication (stripCollectionMetadata $ unitSymbol $ KMapMeta def) [] []
+    unit = Term mempty $ SymbolApplicationF (unitSymbol $ KMapMeta def) [] []
+    -- k |-> v =
+    --     SymbolApplication
+    --         (stripCollectionMetadata $ kmapElementSymbol def)
+    --         []
+    --         [k, v]
+    k |-> v =
+        Term mempty $
+            SymbolApplicationF
+                (kmapElementSymbol def)
+                []
+                [k, v]
+    -- a `con` b = SymbolApplication (stripCollectionMetadata $ concatSymbol $ KMapMeta def) [] [a, b]
+    a `con` b = Term mempty $ SymbolApplicationF (concatSymbol $ KMapMeta def) [] [a, b]
 {-# INLINE externaliseKmapUnsafe #-}
 
 stripCollectionMetadata :: Symbol -> Symbol

test/llvm-integration/LLVM.hs

@@ -90,6 +90,10 @@ llvmSpec =
                 it "should work with latin-1strings" $
                     hedgehog . propertyTest . latin1Prop
 
+            describe "LLVM hooked Map simplifications" $
+                it "should preserve singleton maps" $
+                    hedgehog . propertyTest . mapKItemInjProp
+
 --------------------------------------------------
 -- individual hedgehog property tests and helpers
 
@@ -147,6 +151,37 @@ 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 kPrim = intTerm 1
+    let v = wrapIntTerm 2
+    LLVM.simplifyTerm api testDef (update kPrim v) (SortApp "SortMapInt2Int" []) === elem k v
+  where
+    update k v =
+        SymbolApplication
+            (fromMaybe (error "missing symbol") $ Map.lookup "LblMapInt2Val'Coln'primitiveUpdate" defSymbols)
+            []
+            [ SymbolApplication
+                (fromMaybe (error "missing symbol") $ Map.lookup "Lbl'Stop'MapInt2Int" defSymbols)
+                []
+                []
+            , k
+            , v
+            ]
+
+    elem k v =
+        SymbolApplication
+            (kmapElementSymbol sortMapInt2Int)
+            []
+            [k, v]
+
+    wrapIntTerm i =
+        SymbolApplication
+            (fromMaybe (error "missing symbol") $ Map.lookup "LblwrapInt" defSymbols)
+            []
+            [intTerm i]
+
 ------------------------------------------------------------
 
 runKompile :: IO ()
@@ -268,6 +303,20 @@ sortMapKmap =
         , mapSortName = "SortMap"
         }
 
+sortMapInt2Int :: KMapDefinition
+sortMapInt2Int =
+    KMapDefinition
+        { symbolNames =
+            KCollectionSymbolNames
+                { unitSymbolName = "Lbl'Stop'MapInt2Int"
+                , elementSymbolName = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
+                , concatSymbolName = "Lbl'Unds'MapInt2Int'Unds'"
+                }
+        , keySortName = "SortWrappedInt"
+        , elementSortName = "SortInt"
+        , mapSortName = "SortMapInt2Int"
+        }
+
 sortListKList :: KListDefinition
 sortListKList =
     KListDefinition
@@ -390,6 +439,13 @@ defSorts =
                 , Set.fromList ["SortMap"]
                 )
             )
+        ,
+            ( "SortMapInt2Int"
+            ,
+                ( SortAttributes{collectionAttributes = Just (sortMapInt2Int.symbolNames, KMapTag), argCount = 0}
+                , Set.fromList ["SortMapInt2Int"]
+                )
+            )
         ,
             ( "SortNum"
             ,
@@ -563,6 +619,24 @@ defSymbols =
                         }
                 }
             )
+        ,
+            ( "Lbl'Stop'MapInt2Int"
+            , Symbol
+                { name = "Lbl'Stop'MapInt2Int"
+                , sortVars = []
+                , argSorts = []
+                , resultSort = SortApp "SortMapInt2Int" []
+                , attributes =
+                    SymbolAttributes
+                        { collectionMetadata = Just $ KMapMeta sortMapInt2Int
+                        , symbolType = TotalFunction
+                        , isIdem = IsNotIdem
+                        , isAssoc = IsNotAssoc
+                        , isMacroOrAlias = IsNotMacroOrAlias
+                        , hasEvaluators = CanBeEvaluated
+                        }
+                }
+            )
         ,
             ( "Lbl'Stop'Set"
             , Symbol
@@ -671,6 +745,24 @@ defSymbols =
                         }
                 }
             )
+        ,
+            ( "Lbl'Unds'MapInt2Int'Unds'"
+            , Symbol
+                { name = "Lbl'Unds'MapInt2Int'Unds'"
+                , sortVars = []
+                , argSorts = [SortApp "SortMapInt2Int" [], SortApp "SortMapInt2Int" []]
+                , resultSort = SortApp "SortMapInt2Int" []
+                , attributes =
+                    SymbolAttributes
+                        { collectionMetadata = Just $ KMapMeta sortMapInt2Int
+                        , symbolType = PartialFunction
+                        , isIdem = IsNotIdem
+                        , isAssoc = IsAssoc
+                        , isMacroOrAlias = IsNotMacroOrAlias
+                        , hasEvaluators = CanBeEvaluated
+                        }
+                }
+            )
         ,
             ( "Lbl'Unds'Set'Unds'"
             , Symbol
@@ -1301,6 +1393,60 @@ defSymbols =
                         }
                 }
             )
+        ,
+            ( "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
+            , Symbol
+                { name = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
+                , sortVars = []
+                , argSorts = [SortApp "SortWrappedInt" [], SortApp "SortInt" []]
+                , resultSort = SortApp "SortMapInt2Int" []
+                , attributes =
+                    SymbolAttributes
+                        { collectionMetadata = Just $ KMapMeta sortMapInt2Int
+                        , symbolType = TotalFunction
+                        , isIdem = IsNotIdem
+                        , isAssoc = IsNotAssoc
+                        , isMacroOrAlias = IsNotMacroOrAlias
+                        , hasEvaluators = CanBeEvaluated
+                        }
+                }
+            )
+        ,
+            ( "LblwrapInt"
+            , Symbol
+                { name = "LblwrapInt"
+                , sortVars = []
+                , argSorts = [SortApp "SortInt" []]
+                , resultSort = SortApp "SortWrappedInt" []
+                , attributes =
+                    SymbolAttributes
+                        { collectionMetadata = Nothing
+                        , symbolType = TotalFunction
+                        , isIdem = IsNotIdem
+                        , isAssoc = IsNotAssoc
+                        , isMacroOrAlias = IsNotMacroOrAlias
+                        , hasEvaluators = CanBeEvaluated
+                        }
+                }
+            )
+        ,
+            ( "LblMapInt2Val'Coln'primitiveUpdate"
+            , Symbol
+                { name = "LblMapInt2Val'Coln'primitiveUpdate"
+                , sortVars = []
+                , argSorts = [SortApp "MapInt2Int" [], SortApp "SortInt" [], SortApp "SortWrappedInt" []]
+                , resultSort = SortApp "MapInt2Int" []
+                , attributes =
+                    SymbolAttributes
+                        { collectionMetadata = Nothing
+                        , symbolType = TotalFunction
+                        , isIdem = IsNotIdem
+                        , isAssoc = IsNotAssoc
+                        , isMacroOrAlias = IsNotMacroOrAlias
+                        , hasEvaluators = CanBeEvaluated
+                        }
+                }
+            )
         ,
             ( "Lbl'UndsPipe'Int'Unds'"
             , Symbol

test/llvm-integration/definition/llvm.k

@@ -5,6 +5,7 @@ module LLVM
   imports MAP
   imports SET
   imports K-EQUAL
+  imports MAP-INT2INT
 
   syntax Num ::= Even | Odd
   syntax Even ::= Zero() | Two() | Four() | Six() | Eight() | Ten()
@@ -39,3 +40,40 @@ module LLVM
   rule div2(Ten()) => Five()
 
 endmodule
+
+module MAP-INT2INT
+  imports INT
+
+  syntax WrappedInt
+
+  syntax WrappedInt ::= wrap(Int)  [symbol, klabel(wrapInt)]
+  syntax Int ::= unwrap(WrappedInt)  [function, total, injective, symbol, klabel(unwrapInt)]
+  rule unwrap(wrap(A:Int)) => A
+
+  syntax MapInt2Int [hook(MAP.Map)]
+  syntax MapInt2Int ::= MapInt2Int MapInt2Int
+         [ left, function, hook(MAP.concat), klabel(_MapInt2Int_),
+           symbol, assoc, comm, unit(.MapInt2Int), element(_Int2Int|->_),
+           index(0), format(%1%n%2)
+         ]
+  syntax MapInt2Int ::= ".MapInt2Int"
+         [ function, total, hook(MAP.unit),
+           klabel(.MapInt2Int), symbol, latex(\dotCt{MapInt2Int})
+         ]
+  syntax MapInt2Int ::= WrappedInt "Int2Int|->" WrappedInt
+         [ function, total, hook(MAP.element),
+           klabel(_Int2Int|->_), symbol,
+           latex({#1}\mapsto{#2}), injective
+         ]
+
+  syntax MapInt2Int ::= MapInt2Int "[" key: WrappedInt "<-" value: WrappedInt "]" 
+         [function, total, klabel(MapInt2Val:update), symbol, hook(MAP.update), prefer]
+
+
+  syntax MapInt2Int ::= MapInt2Int "{{" key: Int "<-" value: WrappedInt "}}"
+                 [ function, total, klabel(MapInt2Val:primitiveUpdate), symbol,
+                   prefer
+                 ]
+  rule M:MapInt2Int {{ Key:Int <- Value:WrappedInt }}
+      => M[wrap(Key) <- Value]
+endmodule

test/rpc-integration/resources/wasm-maps.k

@@ -0,0 +1,56 @@
+module WASM-MAPS
+  imports MAP-VAL-TO-VAL
+
+  configuration
+        <wasm>
+          <instrs> $PGM </instrs>
+          <locals> .MapValToVal </locals>
+        </wasm>
+
+  syntax Instr ::= "init_local"  Int Int
+  // -----------------------------------
+  rule <instrs> init_local INDEX VALUE => . ... </instrs>
+       <locals> LOCALS => LOCALS {{ wrap(INDEX) <- wrap(VALUE) }} </locals>
+
+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