Matching Lists with opaque rests (#3751)

Fixes #3749 We change the pattern matching algorithm, implemented by `Kore.Rewrite.Axiom.Matcher.patternMatch'`, in two ways: * list concatenation symbols are handled separately from all other symbol applications * lists are allowed to match when both pattern and subject have an opaque rest Minor clean-up: * `Builtin.IndexedModule.MetadataTools.sortAttributes` is made total, the original partial version renamed to `unsafeSortAttributes` * same goes for `getSortAttributes` The PR is ready for review, but the following is left to be done before we can merge: - [x] add the K definition from #3749 as a test for `kore-rpc`
runtimeverification · Mar 26, 2024 · e7ba3c7 · e7ba3c7
1 parent 8f97e95
commit e7ba3c7
Show file tree

Hide file tree

Showing 19 changed files with 2,916 additions and 60 deletions.
diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs
@@ -373,7 +373,7 @@ lookupSymbolUnit tools builtinSort =
         , symbolSorts
         }
   where
-    unit = Attribute.unit (MetadataTools.sortAttributes tools builtinSort)
+    unit = Attribute.unit (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getUnit unit
             & fromMaybe missingUnitAttribute
@@ -409,7 +409,7 @@ lookupSymbolElement tools builtinSort =
         , symbolSorts
         }
   where
-    element = Attribute.element (MetadataTools.sortAttributes tools builtinSort)
+    element = Attribute.element (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getElement element
             & fromMaybe missingElementAttribute
@@ -445,7 +445,7 @@ lookupSymbolConcat tools builtinSort =
         , symbolSorts
         }
   where
-    concat' = Attribute.concat (MetadataTools.sortAttributes tools builtinSort)
+    concat' = Attribute.concat (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getConcat concat'
             & fromMaybe missingConcatAttribute
@@ -477,9 +477,11 @@ isSort :: Text -> SmtMetadataTools attr -> Sort -> Maybe Bool
 isSort builtinName tools sort
     | SortVariableSort _ <- sort = Nothing
     | otherwise =
-        let sortAttributes = MetadataTools.sortAttributes tools
-            Attribute.Sort{hook} = sortAttributes sort
-         in Just (getHook hook == Just builtinName)
+        case MetadataTools.sortAttributes tools sort of
+            Right sortAttributes ->
+                let Attribute.Sort{hook} = sortAttributes
+                 in Just (getHook hook == Just builtinName)
+            Left _err -> Just False
 
 -- | Run a function evaluator that can terminate early.
 getAttemptedAxiom ::

diff --git a/kore/src/Kore/Builtin/Symbols.hs b/kore/src/Kore/Builtin/Symbols.hs
@@ -85,7 +85,7 @@ lookupSymbolUnit tools builtinSort =
         , symbolSorts
         }
   where
-    unit = Attribute.unit (MetadataTools.sortAttributes tools builtinSort)
+    unit = Attribute.unit (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getUnit unit
             & fromMaybe missingUnitAttribute
@@ -121,7 +121,7 @@ lookupSymbolElement tools builtinSort =
         , symbolSorts
         }
   where
-    element = Attribute.element (MetadataTools.sortAttributes tools builtinSort)
+    element = Attribute.element (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getElement element
             & fromMaybe missingElementAttribute
@@ -157,7 +157,7 @@ lookupSymbolConcat tools builtinSort =
         , symbolSorts
         }
   where
-    concat' = Attribute.concat (MetadataTools.sortAttributes tools builtinSort)
+    concat' = Attribute.concat (MetadataTools.unsafeSortAttributes tools builtinSort)
     symbolOrAlias =
         Attribute.Sort.getConcat concat'
             & fromMaybe missingConcatAttribute

diff --git a/kore/src/Kore/IndexedModule/MetadataTools.hs b/kore/src/Kore/IndexedModule/MetadataTools.hs
@@ -16,6 +16,7 @@ module Kore.IndexedModule.MetadataTools (
     extractMetadataTools,
     findSortConstructors,
     sortAttributes,
+    unsafeSortAttributes,
     applicationSorts,
     symbolAttributes,
 ) where
@@ -119,10 +120,19 @@ findSortConstructors
 sortAttributes ::
     MetadataTools sortConstructors smt attributes ->
     Sort ->
-    Attribute.Sort
+    Either String Attribute.Sort
 sortAttributes MetadataTools{syntax = MetadataSyntaxData sdata} =
     getSortAttributes sdata
 sortAttributes MetadataTools{syntax = MetadataSyntaxDataTable sdata} =
+    lookupThingIn (sortAttributeTable sdata)
+
+unsafeSortAttributes ::
+    MetadataTools sortConstructors smt attributes ->
+    Sort ->
+    Attribute.Sort
+unsafeSortAttributes MetadataTools{syntax = MetadataSyntaxData sdata} =
+    unsafeGetSortAttributes sdata
+unsafeSortAttributes MetadataTools{syntax = MetadataSyntaxDataTable sdata} =
     either error id . lookupThingIn (sortAttributeTable sdata)
 
 applicationSorts ::

diff --git a/kore/src/Kore/IndexedModule/Resolvers.hs b/kore/src/Kore/IndexedModule/Resolvers.hs
@@ -9,6 +9,7 @@ Portability : POSIX
 -}
 module Kore.IndexedModule.Resolvers (
     getSortAttributes,
+    unsafeGetSortAttributes,
     getSymbolAttributes,
     resolveSort,
     resolveAlias,
@@ -109,15 +110,22 @@ getHeadApplicationSorts m patternHead =
         assertRight $ symbolOrAliasSorts sortParameters sentence
 
 getSortAttributes ::
-    HasCallStack =>
     IndexedModuleSyntax patternType declAtts ->
     Sort ->
-    Attribute.Sort
+    Either String Attribute.Sort
 getSortAttributes m (SortActualSort (SortActual sortId _)) =
     case resolveSort m sortId of
-        Right (atts, _) -> atts
-        Left _ -> error $ noSort sortId
-getSortAttributes _ _ = error "Can't lookup attributes for sort variables"
+        Right (atts, _) -> Right atts
+        Left _ -> Left $ noSort sortId
+getSortAttributes _ _ = Left "Can't lookup attributes for sort variables"
+
+unsafeGetSortAttributes ::
+    HasCallStack =>
+    IndexedModuleSyntax patternType declAtts ->
+    Sort ->
+    Attribute.Sort
+unsafeGetSortAttributes m s = either error id (getSortAttributes m s)
+
 getSymbolAttributes ::
     HasCallStack =>
     IndexedModuleSyntax patternType declAtts ->

diff --git a/kore/src/Kore/Rewrite/Axiom/Matcher.hs b/kore/src/Kore/Rewrite/Axiom/Matcher.hs
@@ -24,6 +24,7 @@ import Data.PQueue.Min (
     MinQueue,
  )
 import Data.PQueue.Min qualified as MinQueue
+import Data.Sequence (Seq ((:|>)))
 import Data.Sequence qualified as Seq
 import Data.Set (
     Set,
@@ -393,12 +394,69 @@ patternMatch' sideCondition ((MatchItem pat subject boundVars boundSet) : rest)
             decomposeBinder (inject variable1) term1 (inject variable2) term2
         (Exists_ _ variable1 term1, Exists_ _ variable2 term2) ->
             decomposeBinder (inject variable1) term1 (inject variable2) term2
-        (App_ symbol1 children1, App_ symbol2 children2) ->
-            if symbol1 == symbol2
-                then decomposeList (zip children1 children2)
-                else
-                    failMatch $
-                        "distinct application symbols: " <> (unparseToText symbol1) <> ", " <> (unparseToText symbol2)
+        (_, _)
+            | Just False <- List.isListSort tools sort
+            , (App_ symbol1 children1, App_ symbol2 children2) <- (pat, subject) ->
+                if symbol1 == symbol2
+                    then decomposeList (zip children1 children2)
+                    else
+                        failMatch $
+                            "distinct application symbols: " <> (unparseToText symbol1) <> ", " <> (unparseToText symbol2)
+            | Just True <- List.isListSort tools sort ->
+                case (List.normalize pat, List.normalize subject) of
+                    (Var_ var1, Var_ var2)
+                        | var1 == var2 ->
+                            discharge
+                    (ElemVar_ var1, _)
+                        | isFunctionPattern subject ->
+                            bind (inject var1) subject
+                    (SetVar_ var1, _) ->
+                        bind (inject var1) subject
+                    ( InternalList_ InternalList{internalListChild = l1}
+                        , InternalList_ InternalList{internalListChild = l2}
+                        ) ->
+                            if length l1 == length l2
+                                then decomposeList $ zip (toList l1) (toList l2)
+                                else failMatch "list lengths are not equal"
+                    ( App_ symbol [InternalList_ InternalList{internalListChild = l1}, var@(ElemVar_ _)]
+                        , InternalList_ InternalList{internalListChild = l2}
+                        )
+                            | List.isSymbolConcat symbol ->
+                                if length l1 <= length l2
+                                    then
+                                        let (start, l2') = Seq.splitAt (length l1) l2
+                                         in decomposeList $ (var, List.asInternal tools sort l2') : zip (toList l1) (toList start)
+                                    else failMatch "subject list is too short"
+                    ( App_ symbol [var@(ElemVar_ _), InternalList_ InternalList{internalListChild = l1}]
+                        , InternalList_ InternalList{internalListChild = l2}
+                        )
+                            | List.isSymbolConcat symbol ->
+                                if length l1 <= length l2
+                                    then
+                                        let (l2', end) = Seq.splitAt (length l2 - length l1) l2
+                                         in decomposeList $ (var, List.asInternal tools sort l2') : zip (toList l1) (toList end)
+                                    else failMatch "subject list is too short"
+                    ( App_ symbol1 [InternalList_ InternalList{internalListChild = l1}, var1@(ElemVar_ _)]
+                        , App_ symbol2 [InternalList_ InternalList{internalListChild = l2}, var2@(ElemVar_ _)]
+                        ) -- NB: may need to add the symmetric case in future, i.e. VAR _List_ ListItem(X)
+                            | List.isSymbolConcat symbol1
+                            , symbol1 == symbol2 ->
+                                if length l1 <= length l2
+                                    then
+                                        let (start, l2') = Seq.splitAt (length l1) l2
+                                         in decomposeList $
+                                                (var1, List.asInternal tools sort (l2' :|> var2))
+                                                    : zip (toList l1) (toList start)
+                                    else failMatch "subject list is too short"
+                    (App_ symbol1 children1, App_ symbol2 children2) ->
+                        if symbol1 == symbol2
+                            then decomposeList (zip children1 children2)
+                            else
+                                failMatch $
+                                    "distinct application symbols: " <> (unparseToText symbol1) <> ", " <> (unparseToText symbol2)
+                    _ ->
+                        failMatch
+                            "unimplemented list matching case"
         (Inj_ inj1, Inj_ inj2)
             | Just unifyData <- matchInjs inj1 inj2 ->
                 case unifyData of
@@ -436,42 +494,6 @@ patternMatch' sideCondition ((MatchItem pat subject boundVars boundSet) : rest)
                         (Application secondHead secondChildren)
                         inj1{injChild = ()} ->
                     decomposeOverload unifyData
-        (_, _)
-            | Just True <- List.isListSort tools sort ->
-                case (List.normalize pat, List.normalize subject) of
-                    (Var_ var1, Var_ var2)
-                        | var1 == var2 ->
-                            discharge
-                    (ElemVar_ var1, _)
-                        | isFunctionPattern subject ->
-                            bind (inject var1) subject
-                    (SetVar_ var1, _) ->
-                        bind (inject var1) subject
-                    ( InternalList_ InternalList{internalListChild = l1}
-                        , InternalList_ InternalList{internalListChild = l2}
-                        ) ->
-                            if length l1 == length l2
-                                then decomposeList $ zip (toList l1) (toList l2)
-                                else failMatch "list lengths are not equal"
-                    ( App_ symbol [InternalList_ InternalList{internalListChild = l1}, var@(ElemVar_ _)]
-                        , InternalList_ InternalList{internalListChild = l2}
-                        )
-                            | List.isSymbolConcat symbol ->
-                                if length l1 <= length l2
-                                    then
-                                        let (start, l2') = Seq.splitAt (length l1) l2
-                                         in decomposeList $ (var, List.asInternal tools sort l2') : zip (toList l1) (toList start)
-                                    else failMatch "subject list is too short"
-                    ( App_ symbol [var@(ElemVar_ _), InternalList_ InternalList{internalListChild = l1}]
-                        , InternalList_ InternalList{internalListChild = l2}
-                        )
-                            | List.isSymbolConcat symbol ->
-                                if length l1 <= length l2
-                                    then
-                                        let (l2', end) = Seq.splitAt (length l2 - length l1) l2
-                                         in decomposeList $ (var, List.asInternal tools sort l2') : zip (toList l1) (toList end)
-                                    else failMatch "subject list is too short"
-                    _ -> failMatch "unimplemented list matching case"
         (InternalMap_ _, InternalMap_ _) ->
             defer
         (InternalSet_ _, InternalSet_ _) ->

diff --git a/kore/src/Kore/Rewrite/SMT/Translate.hs b/kore/src/Kore/Rewrite/SMT/Translate.hs
@@ -240,7 +240,7 @@ translatePredicateWith tools sideCondition translateTerm predicate =
                     | builtinSort == Builtin.Int.sort -> pure SMT.tInt
                 _ -> translateSort tools variableSort & maybeToTranslator
         Attribute.Sort{hook = Hook{getHook}} =
-            sortAttributes tools variableSort
+            unsafeSortAttributes tools variableSort
 
 {- | Attempt to translate an arbitrary ML pattern for the solver.
  It should only be used in the 'Predicate' translator or in
@@ -270,7 +270,7 @@ translatePattern tools sideCondition translateTerm sort pat =
             _ -> empty
   where
     Attribute.Sort{hook = Hook{getHook}} =
-        sortAttributes tools sort
+        unsafeSortAttributes tools sort
 
     translateInt :: TermLike variable -> Translator variable monad SExpr
     translateInt pat'

diff --git a/kore/src/Kore/Validate/AttributesVerifier.hs b/kore/src/Kore/Validate/AttributesVerifier.hs
@@ -150,7 +150,7 @@ verifyNoHookedSupersort indexedModule axiom subsorts = do
     let isHooked =
             getHasDomainValues
                 . hasDomainValues
-                . getSortAttributes (indexedModuleSyntax indexedModule)
+                . (unsafeGetSortAttributes (indexedModuleSyntax indexedModule))
                 . Subsort.supersort
         hookedSubsort = find isHooked subsorts
     for_ hookedSubsort $ \sort ->

diff --git a/test/rpc-server/execute/list-matching/README.md b/test/rpc-server/execute/list-matching/README.md
@@ -0,0 +1,5 @@
+# Simplifying a list concatenation expression
+
+The rewrite rule in `test.k` introduces a symbolic list expression into the path condition, that is immediately simplified to `true` by the `simplify-size` simplification.
+
+See the original issue for context: https://github.com/runtimeverification/haskell-backend/issues/3749