Hook: LIST.updateAll (#2275)

Author: andreiburdusa

docs/hooks.md

@@ -704,6 +704,21 @@ The number of elements in the given list.
         [hook{}("LIST.size")]
 ~~~
 
+## LIST.updateAll
+
+`LIST.updateAll(L1, index, L2)` creates a new list using a list `L2` of size `N`
+where the `N` elements of `L1` starting at `index` are replaced with the
+contents of `L2`.
+The result is `\bottom` in these cases:
+
+- `index` is negative
+- `L2` is non-empty and `index + N` exeeds the length of `L1`
+
+~~~
+    hooked-symbol updateAll{}(List{}, Int{}, List{}) : List{}
+        [hook{}("LIST.updateAll")]
+~~~
+
 ## SET
 
 Depends on `BOOL`.

kore/src/Kore/Builtin/List.hs

@@ -194,6 +194,9 @@ symbolVerifiers =
     , ( sizeKey
       , Builtin.verifySymbol Int.assertSort [assertSort]
       )
+    , ( updateAllKey
+      , Builtin.verifySymbol assertSort [assertSort, Int.assertSort, assertSort]
+      )
     ]
 
 {- | Abort function evaluation if the argument is not a List domain value.
@@ -324,6 +327,24 @@ evalSize resultSort [_list] = do
         & return
 evalSize _ _ = Builtin.wrongArity sizeKey
 
+evalUpdateAll :: Builtin.Function
+evalUpdateAll resultSort [_list1, _ix, _list2] = do
+    _list1 <- expectBuiltinList getKey _list1
+    _list2 <- expectBuiltinList getKey _list2
+    _ix <- fromInteger <$> Int.expectBuiltinInt getKey _ix
+    let len1 = Seq.length _list1
+        len2 = Seq.length _list2
+        result
+            | _ix < 0 = return (Pattern.bottomOf resultSort)
+            | len2 == 0 = returnList resultSort _list1
+            | _ix + len2 > len1 = return (Pattern.bottomOf resultSort)
+            | otherwise =
+                let unchanged1 = Seq.take _ix _list1
+                    unchanged2 = Seq.drop (_ix + length _list2) _list1
+                in returnList resultSort (unchanged1 <> _list2 <> unchanged2)
+    result
+evalUpdateAll _ _ = Builtin.wrongArity updateKey
+
 {- | Implement builtin function evaluation.
  -}
 builtinFunctions :: Map Text BuiltinAndAxiomSimplifier
@@ -336,6 +357,7 @@ builtinFunctions =
         , (updateKey, Builtin.functionEvaluator evalUpdate)
         , (inKey, Builtin.functionEvaluator evalIn)
         , (sizeKey, Builtin.functionEvaluator evalSize)
+        , (updateAllKey, Builtin.functionEvaluator evalUpdateAll)
         ]
 
 {- | Simplify the conjunction or equality of two concrete List domain values.

kore/src/Kore/Builtin/List/List.hs

@@ -24,6 +24,7 @@ module Kore.Builtin.List.List
     , updateKey
     , inKey
     , sizeKey
+    , updateAllKey
     ) where
 
 import Prelude.Kore
@@ -197,3 +198,6 @@ inKey = "LIST.in"
 
 sizeKey :: IsString s => s
 sizeKey = "LIST.size"
+
+updateAllKey :: IsString s => s
+updateAllKey = "LIST.updateAll"

kore/test/Test/Kore/Builtin/Definition.hs

@@ -391,6 +391,11 @@ updateListSymbol = builtinSymbol "updateList" listSort
 inListSymbol :: Internal.Symbol
 inListSymbol = builtinSymbol "inList" boolSort [intSort, listSort] & hook "LIST.in"
 
+updateAllListSymbol :: Internal.Symbol
+updateAllListSymbol =
+    builtinSymbol "updateAllList" listSort [listSort, intSort, listSort]
+    & hook "LIST.updateAll"
+
 unitList :: TermLike VariableName
 unitList = mkApplySymbol unitListSymbol []
 
@@ -419,6 +424,13 @@ inList
     -> TermLike VariableName
 inList x list = mkApplySymbol inListSymbol [x, list]
 
+updateAllList
+    :: TermLike VariableName
+    -> TermLike VariableName
+    -> TermLike VariableName
+    -> TermLike VariableName
+updateAllList l1 ix l2 = mkApplySymbol updateAllListSymbol [l1, ix, l2]
+
 -- ** Map
 
 unitMapSymbol :: Internal.Symbol
@@ -1518,6 +1530,7 @@ listModule =
             , hookedSymbolDecl updateListSymbol
             , hookedSymbolDecl inListSymbol
             , hookedSymbolDecl sizeListSymbol
+            , hookedSymbolDecl updateAllListSymbol
             -- A second builtin List sort, to confuse 'asPattern'.
             , listSortDecl2
             , hookedSymbolDecl unitList2Symbol

kore/test/Test/Kore/Builtin/List.hs

@@ -13,6 +13,7 @@ module Test.Kore.Builtin.List
     , test_inUnit
     , test_inElement
     , test_inConcat
+    , test_updateAll
     , hprop_unparse
     , test_size
     --
@@ -417,6 +418,35 @@ test_size =
         (===) Pattern.top    =<< evaluateT predicate
     ]
 
+test_updateAll :: [TestTree]
+test_updateAll =
+    [ testCaseWithoutSMT "updateAll([1, 2, 3], -1, [5]) === \\bottom" $ do
+        result <-
+            evaluate
+            $ updateAllList original (mkInt (-1)) (elementList $ mkInt 5)
+        assertEqual' "" Pattern.bottom result
+    , testCaseWithoutSMT "updateAll([1, 2, 3], 10, []) === [1, 2, 3]" $ do
+        result <-
+            evaluate
+            $ updateAllList original (mkInt 10) unitList
+        assertEqual' "" (Pattern.fromTermLike original) result
+    , testCaseWithoutSMT "updateAll([1, 2, 3], 1, [5]) === [1, 5, 3]" $ do
+        result <-
+            evaluate
+            $ updateAllList original (mkInt 1) (elementList $ mkInt 5)
+        let expect = asInternal . fmap mkInt $ Seq.fromList [1, 5, 3]
+        assertEqual' "" (Pattern.fromTermLike expect) result
+    , testCaseWithoutSMT "updateAll([1, 2, 3], 0, [1, 2, 3, 4] === \\bottom"
+        $ do
+            let new = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3, 4]
+            result <-
+                evaluate
+                $ updateAllList original (mkInt 0) new
+            assertEqual' "" Pattern.bottom result
+    ]
+  where
+    original = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3]
+
 mkInt :: Integer -> TermLike VariableName
 mkInt = Test.Int.asInternal