Handle list random access patterns in frontend (#4634)

This PR adds support for the `L [ I <- X ]` syntax on the LHS of rules, which allows you to pattern match on an arbitrary element of a list. The code is not fully polished; it is not integrated with configuration abstraction or cell collections. It is not likely to be further improved upon presently because the code it was intended to support ended up not proving worth merging. However, it is broadly useful functionality (along with the accompanying LLVM backend PR) and thus ought to be merged. --------- Co-authored-by: Dwight Guth <[email protected]>
runtimeverification · Sep 17, 2024 · 861cda4 · 861cda4
1 parent b4cc055
commit 861cda4
Show file tree

Hide file tree

Showing 19 changed files with 107 additions and 26 deletions.
diff --git a/docs/user_manual.md b/docs/user_manual.md
@@ -2225,6 +2225,9 @@ ListItem(E1) ListItem(E2) L:List ListItem(E3) ListItem(E4)
 // the empty list
 .List
 
+// 1 or more list update operations applied to a variable
+L:List [ K1 <- E1 ] [ K2 <- E2 ]
+
 // 0 or more elements in any order plus 0 or 1 variables of sort Set
 // in any order
 SetItem(K1) SetItem(K2) S::Set SetItem(K3) SetItem(K4)
@@ -2255,9 +2258,10 @@ though E3 is itself unbound.
 In the above examples, E1, E2, E3, and E4 can be any pattern that is normally
 allowed on the lhs of a rule.
 
-When a map or set key contains function symbols, we know that the variables in
-that key are bound (because of the above restriction), so it is possible to
-evaluate the function to a concrete term prior to performing the lookup.
+When a map, set, or list key contains function symbols, we know that the
+variables in that key are bound (because of the above restriction), so it is
+possible to evaluate the function to a concrete term prior to performing the
+lookup.
 
 Indeed, this is the precise semantics which occurs; the function is evaluated
 and the result is looked up in the collection.

diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
@@ -926,7 +926,7 @@ side, it is O(N), where N is the number of elements matched on the front and
 back of the list.
 
 ```k
-  syntax List ::= List List               [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), format(%1%n%2)]
+  syntax List ::= List List               [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), update(List:set), format(%1%n%2)]
 ```
 
 ### List unit

diff --git a/k-distribution/tests/regression-new/list-set/00.test b/k-distribution/tests/regression-new/list-set/00.test
@@ -0,0 +1 @@
+l(0, 0)
diff --git a/k-distribution/tests/regression-new/list-set/00.test.out b/k-distribution/tests/regression-new/list-set/00.test.out
@@ -0,0 +1,10 @@
+<generatedTop>
+  <k>
+    .K
+  </k>
+  <list>
+    ListItem ( 0 )
+    ListItem ( 1 )
+    ListItem ( 2 )
+  </list>
+</generatedTop>
diff --git a/k-distribution/tests/regression-new/list-set/01.test b/k-distribution/tests/regression-new/list-set/01.test
@@ -0,0 +1 @@
+l(0, 1)
diff --git a/k-distribution/tests/regression-new/list-set/01.test.out b/k-distribution/tests/regression-new/list-set/01.test.out
@@ -0,0 +1,10 @@
+<generatedTop>
+  <k>
+    l ( 0 , 1 ) ~> .K
+  </k>
+  <list>
+    ListItem ( 0 )
+    ListItem ( 1 )
+    ListItem ( 2 )
+  </list>
+</generatedTop>
diff --git a/k-distribution/tests/regression-new/list-set/11.test b/k-distribution/tests/regression-new/list-set/11.test
@@ -0,0 +1 @@
+l(1, 1)
diff --git a/k-distribution/tests/regression-new/list-set/11.test.out b/k-distribution/tests/regression-new/list-set/11.test.out
@@ -0,0 +1,10 @@
+<generatedTop>
+  <k>
+    .K
+  </k>
+  <list>
+    ListItem ( 0 )
+    ListItem ( 1 )
+    ListItem ( 2 )
+  </list>
+</generatedTop>
diff --git a/k-distribution/tests/regression-new/list-set/22.test b/k-distribution/tests/regression-new/list-set/22.test
@@ -0,0 +1 @@
+l(2, 2)
diff --git a/k-distribution/tests/regression-new/list-set/22.test.out b/k-distribution/tests/regression-new/list-set/22.test.out
@@ -0,0 +1,10 @@
+<generatedTop>
+  <k>
+    .K
+  </k>
+  <list>
+    ListItem ( 0 )
+    ListItem ( 1 )
+    ListItem ( 2 )
+  </list>
+</generatedTop>
diff --git a/k-distribution/tests/regression-new/list-set/Makefile b/k-distribution/tests/regression-new/list-set/Makefile
@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/list-set/test.k b/k-distribution/tests/regression-new/list-set/test.k
@@ -0,0 +1,11 @@
+module TEST
+  imports LIST
+  imports INT
+
+  configuration <k> $PGM:K </k> <list> ListItem(0) ListItem(1) ListItem(2) </list>
+
+  syntax KItem ::= l(Int, Int)
+
+  rule <k> l(I, J) => .K ...</k>
+       <list> _ [ I <- J ] </list>
+endmodule
diff --git a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -427,6 +427,10 @@ private void translateSorts(
               att.add(Att.ELEMENT(), K.class, KApply(KLabel(concatProd.att().get(Att.ELEMENT()))));
           att = att.add(Att.CONCAT(), K.class, KApply(concatProd.klabel().get()));
           att = att.add(Att.UNIT(), K.class, KApply(KLabel(concatProd.att().get(Att.UNIT()))));
+          if (concatProd.att().contains(Att.UPDATE())) {
+            att =
+                att.add(Att.UPDATE(), K.class, KApply(KLabel(concatProd.att().get(Att.UPDATE()))));
+          }
           sb.append("hooked-");
         } else {
           sb.append("hooked-");
@@ -2102,7 +2106,7 @@ private void convert(
           convertStringVarList(location, freeVarsMap, strVal, sb);
         } else {
           switch (strKey) {
-            case "unit", "element" -> {
+            case "unit", "element", "update" -> {
               Production prod = production(KApply(KLabel(strVal)));
               convert(prod.klabel().get(), prod.params(), sb);
               sb.append("()");

diff --git a/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java
@@ -56,6 +56,7 @@ && isLHS()
             && !(hook.equals("LIST.element")
                 || hook.equals("LIST.concat")
                 || hook.equals("LIST.unit")
+                || hook.equals("LIST.update")
                 || hook.equals("SET.element")
                 || hook.equals("SET.concat")
                 || hook.equals("SET.unit")
@@ -79,6 +80,11 @@ && isLHS()
           apply(k.items().get(1));
           return;
         }
+        if (hook.equals("LIST.update")) {
+          apply(k.items().get(0));
+          apply(k.items().get(2));
+          return;
+        }
         super.apply(k);
       }
     }.apply(body);

diff --git a/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java
@@ -19,7 +19,7 @@ public class KEMException extends RuntimeException {
 
   public final KException exception;
 
-  KEMException(KException e) {
+  public KEMException(KException e) {
     super(e.toString(), e.getException());
     this.exception = e;
   }

diff --git a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
@@ -442,6 +442,8 @@ object Att {
     Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
   final val UNUSED =
     Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
+  final val UPDATE =
+    Key.builtin("update", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline)
   final val WRAP_ELEMENT =
     Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
 

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -65,22 +65,26 @@ public void accept(Backend.Holder h) {
     MutableInt warnings = new MutableInt();
     boolean optimize =
         kompileOptions.optimize1 || kompileOptions.optimize2 || kompileOptions.optimize3;
-    Matching.writeDecisionTreeToFile(
-        files.resolveKompiled("definition.kore"),
-        options.heuristic,
-        files.resolveKompiled("dt"),
-        Matching.getThreshold(getThreshold()),
-        !optimize,
-        globalOptions.includesExceptionType(ExceptionType.USELESS_RULE),
-        options.enableSearch,
-        ex -> {
-          var translated = translateError(ex, hookAtts);
-          kem.addKException(translated);
-          if (globalOptions.includesExceptionType(translated.getType())) {
-            warnings.increment();
-          }
-          return null;
-        });
+    try {
+      Matching.writeDecisionTreeToFile(
+          files.resolveKompiled("definition.kore"),
+          options.heuristic,
+          files.resolveKompiled("dt"),
+          Matching.getThreshold(getThreshold()),
+          !optimize,
+          globalOptions.includesExceptionType(ExceptionType.USELESS_RULE),
+          options.enableSearch,
+          ex -> {
+            var translated = translateError(ex, hookAtts);
+            kem.addKException(translated);
+            if (globalOptions.includesExceptionType(translated.getType())) {
+              warnings.increment();
+            }
+            return null;
+          });
+    } catch (MatchingException e) {
+      throw new KEMException(translateError(e, hookAtts));
+    }
     sw.printIntermediate("  Write decision tree");
     if (warnings.intValue() > 0 && kem.options.warnings2errors) {
       throw KEMException.compilerError("Had " + warnings.intValue() + " pattern matching errors.");

diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py
@@ -349,6 +349,7 @@ class Atts:
     UNIT: Final = AttKey('unit', type=_STR)
     UNIQUE_ID: Final = AttKey('UNIQUE_ID', type=_ANY)
     UNPARSE_AVOID: Final = AttKey('unparseAvoid', type=_NONE)
+    UPDATE: Final = AttKey('update', type=_ANY)
     USER_LIST: Final = AttKey('userList', type=_ANY)
     WRAP_ELEMENT: Final = AttKey('wrapElement', type=_ANY)
 

diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py
@@ -187,14 +187,11 @@ def _parse_special_att_value(key: AttKey, value: Any) -> tuple[tuple[Sort, ...],
     if key == Atts.FORMAT:
         assert isinstance(value, Format)
         return (), (String(value.unparse()),)
-    if key == Atts.ELEMENT:
+    if key == Atts.ELEMENT or key == Atts.UNIT or key == Atts.UPDATE:
         # TODO avoid special casing by pre-processing the attribute into a KApply
         # This should be handled by the frontend
         assert isinstance(value, str)
         return (), (App(_label_name(value)),)
-    if key == Atts.UNIT:  # TODO same here
-        assert isinstance(value, str)
-        return (), (App(_label_name(value)),)
     return None
 
 
@@ -891,6 +888,7 @@ def _update(syntax_sort: KSyntaxSort, concat_atts: Mapping[KSort, KAtt]) -> KSyn
                     Atts.ELEMENT(concat_att[Atts.ELEMENT]),
                     Atts.UNIT(concat_att[Atts.UNIT]),
                 ]
+                + ([Atts.UPDATE(concat_att[Atts.UPDATE])] if Atts.UPDATE in concat_att else [])
             )
         )