Add int-to-int Map to the LLVM integration test definition

runtimeverification · Nov 14, 2023 · 7ab269b · 7ab269b
1 parent c4608e8
commit 7ab269b
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 2 deletions.
diff --git a/test/llvm-integration/LLVM.hs b/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,18 @@ 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 = intTerm 2
+    let v = intTerm 2
+    LLVM.simplifyTerm api testDef (elem k v) (SortApp "SortMapInt2Int" []) === elem k v
+  where
+    elem k v =
+        SymbolApplication
+            (kmapElementSymbol sortMapInt2Int)
+            []
+            [k, v]
+
 ------------------------------------------------------------
 
 runKompile :: IO ()
@@ -277,7 +293,7 @@ sortMapInt2Int =
                 , elementSymbolName = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
                 , concatSymbolName = "Lbl'Unds'MapInt2Int'Unds'"
                 }
-        , keySortName = "SortInt"
+        , keySortName = "SortWrappedInt"
         , elementSortName = "SortInt"
         , mapSortName = "SortMapInt2Int"
         }
@@ -1363,7 +1379,7 @@ defSymbols =
             , Symbol
                 { name = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'"
                 , sortVars = []
-                , argSorts = [SortApp "SortInt" [], SortApp "SortInt" []]
+                , argSorts = [SortApp "SortWrappedInt" [], SortApp "SortInt" []]
                 , resultSort = SortApp "SortMapInt2Int" []
                 , attributes =
                     SymbolAttributes

diff --git a/test/llvm-integration/definition/llvm.k b/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,30 @@ 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
+         ]
+
+endmodule