From 974e29352c66423e1064081abbbbe42d4aedb6ff Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 25 May 2024 23:00:21 +1000 Subject: [PATCH] `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 --- kore/src/Kore/Builtin/Map.hs | 24 +++++++++++++++- kore/test/Test/Kore/Builtin/Definition.hs | 10 +++++++ kore/test/Test/Kore/Builtin/Map.hs | 35 +++++++++++++++++++++++ 3 files changed, 68 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index a9e76c1509..926957a4e3 100644 --- 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 index 90293187c6..ba78ac8bdf 100644 --- 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 index 3dddf4f43d..2cfacab9dc 100644 --- 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