Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 17, 2024 · 732aa25 · 732aa25
2 parents 6e23a83 + 861cda4
commit 732aa25
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 [])
             )
         )