MAP.updateAll implementation on concrete arguments (#3899)

Fixes #3898 `MAP.updateAll` was previously returning `notImplemented` (always returning `NotApplicable`) but this causes an error when its arguments are fully-concrete. This change implements the hook for fully-concrete maps, by doing the obvious update of the underlying hash map and special-casing empty maps. --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · May 25, 2024 · 974e293 · 974e293
1 parent 45aaf89
commit 974e293
Show file tree

Hide file tree

Showing 3 changed files with 68 additions and 1 deletion.
diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs
@@ -361,6 +361,28 @@ evalUpdate _ resultSort [_map, _key, value] = do
         & lift
 evalUpdate _ _ _ = Builtin.wrongArity Map.updateKey
 
+evalUpdateAll :: Builtin.Function
+evalUpdateAll _ resultSort [original, updates] =
+    emptyOriginal <|> emptyUpdates <|> concreteUpdates
+  where
+    getHashmap = expectConcreteBuiltinMap Map.updateAllKey
+
+    emptyOriginal = do
+        original' <- getHashmap original
+        Monad.guard $ HashMap.null original'
+        pure $ from updates
+
+    emptyUpdates = do
+        updates' <- getHashmap updates
+        Monad.guard $ HashMap.null updates'
+        pure $ from original
+
+    concreteUpdates = do
+        original' <- getHashmap original
+        updates' <- getHashmap updates
+        lift . returnConcreteMap resultSort $ updates' <> original'
+evalUpdateAll _ _ _ = Builtin.wrongArity Map.updateAllKey
+
 evalInKeys :: Builtin.Function
 evalInKeys sideCondition resultSort arguments@[_key, _map] =
     emptyMap <|> concreteMap <|> symbolicMap
@@ -490,7 +512,7 @@ builtinFunctions key
     | key == Map.elementKey = Just $ Builtin.functionEvaluator evalElement
     | key == Map.unitKey = Just $ Builtin.functionEvaluator evalUnit
     | key == Map.updateKey = Just $ Builtin.functionEvaluator evalUpdate
-    | key == Map.updateAllKey = Just Builtin.notImplemented
+    | key == Map.updateAllKey = Just $ Builtin.functionEvaluator evalUpdateAll
     | key == Map.in_keysKey = Just $ Builtin.functionEvaluator evalInKeys
     | key == Map.keysKey = Just $ Builtin.functionEvaluator evalKeys
     | key == Map.keys_listKey = Just $ Builtin.functionEvaluator evalKeysList

diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs
@@ -460,6 +460,10 @@ updateMapSymbol :: Internal.Symbol
 updateMapSymbol =
     builtinSymbol "updateMap" mapSort [mapSort, intSort, intSort]
         & hook "MAP.update"
+updateAllMapSymbol :: Internal.Symbol
+updateAllMapSymbol =
+    builtinSymbol "updateAllMap" mapSort [mapSort, mapSort]
+        & hook "MAP.updateAll"
 lookupMapSymbol :: Internal.Symbol
 lookupMapSymbol =
     builtinSymbol "lookupMap" intSort [mapSort, intSort]
@@ -510,6 +514,11 @@ updateMap ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName
 updateMap map' key value = mkApplySymbol updateMapSymbol [map', key, value]
+updateAllMap ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+updateAllMap map' updates = mkApplySymbol updateAllMapSymbol [map', updates]
 lookupMap ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName ->
@@ -1553,6 +1562,7 @@ mapModule =
             , hookedSymbolDecl lookupMapSymbol
             , hookedSymbolDecl lookupOrDefaultMapSymbol
             , hookedSymbolDecl updateMapSymbol
+            , hookedSymbolDecl updateAllMapSymbol
             , hookedSymbolDecl inKeysMapSymbol
             , hookedSymbolDecl keysMapSymbol
             , hookedSymbolDecl keysListMapSymbol

diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs
@@ -1,6 +1,7 @@
 module Test.Kore.Builtin.Map (
     test_lookupUnit,
     test_lookupUpdate,
+    test_updateAll,
     test_removeUnit,
     test_sizeUnit,
     test_removeKeyNotIn,
@@ -195,6 +196,40 @@ test_lookupUpdate =
         (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate
     ]
 
+test_updateAll :: [TestTree]
+test_updateAll =
+    [ testPropertyWithoutSolver "Empty maps are neutral elements for MAP.updateAll" $ do
+        aMap <- forAll genMapPattern
+        let update1 = updateAllMap aMap unitMap
+            update2 = updateAllMap unitMap aMap
+            expect = OrPattern.fromTermLike aMap
+        (===) expect =<< evaluateTermT update1
+        (===) expect =<< evaluateTermT update2
+    , testPropertyWithoutSolver "MAP.updateAll adds or updates map assocs" $ do
+        internalMap <- forAll $ genMapInteger genIntegerPattern
+        let theMap :: TermLike RewritingVariableName
+            theMap = asTermLike $ mapKeys Test.Int.asKey internalMap
+            existingKeys = HashMap.keys internalMap
+        -- may or may not collide with existing, but not empty (theMap might be empty)
+        newKeys <- forAll $ Gen.list (Range.linear 1 8) genInteger
+        let allKeys = List.nub $ existingKeys <> newKeys
+            newValues = map Test.Int.asInternal newKeys
+            updates = asTermLike . HashMap.fromList $ zip (map Test.Int.asKey newKeys) newValues
+            newMap = updateAllMap theMap updates
+        let check key = do
+                let keyTerm = Test.Int.asInternal key
+                    expect
+                        | key `elem` newKeys -- updated to key == value
+                            =
+                            OrPattern.fromTermLike keyTerm
+                        | otherwise -- still prior value
+                            =
+                            maybe (error "Prior key not found") OrPattern.fromTermLike $
+                                HashMap.lookup key internalMap
+                (===) expect =<< evaluateTermT (lookupMap newMap keyTerm)
+        mapM_ check allKeys
+    ]
+
 test_removeUnit :: TestTree
 test_removeUnit =
     testPropertyWithSolver