Merge branch 'develop' into ordinal

runtimeverification · Oct 29, 2024 · 7b225d5 · 7b225d5
2 parents 2e9de7f + f6b18d4
commit 7b225d5
Show file tree

Hide file tree

Showing 11 changed files with 3,740 additions and 274 deletions.
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
@@ -766,12 +766,9 @@ class Matrix private (
       Leaf(row.clause.action.ordinal, newVars)
     }
     // check that all occurrences of the same variable are equal
-    val nonlinearLeaf = nonlinearPairs.foldRight[DecisionTree](atomicLeaf)((e, dt) =>
-      e._2.foldRight(dt)((os, dt2) => makeEquality(os._1._1, (os._1._2, os._2._2), dt2))
-    )
-    val sc = row.clause.action.scVars match {
+    val sc: DecisionTree = row.clause.action.scVars match {
       // if there is no side condition, continue
-      case None => nonlinearLeaf
+      case None => atomicLeaf
       case Some(cond) =>
         val condVars = cond.map(v => (grouped(v).head._2, grouped(v).head._1.hookAtt))
         val newO     = SC(row.clause.action.ordinal)
@@ -785,13 +782,16 @@ class Matrix private (
             newO,
             "BOOL.Bool",
             1,
-            immutable.Seq(("1", immutable.Seq(), nonlinearLeaf), ("0", immutable.Seq(), child)),
+            immutable.Seq(("1", immutable.Seq(), atomicLeaf), ("0", immutable.Seq(), child)),
             None
           )
         )
     }
+    val nonlinearLeaf = nonlinearPairs.foldRight[DecisionTree](sc)((e, dt) =>
+      e._2.foldRight(dt)((os, dt2) => makeEquality(os._1._1, (os._1._2, os._2._2), dt2))
+    )
     // fill out the bindings for list range variables
-    val withRanges = row.clause.listRanges.foldRight(sc) {
+    val withRanges = row.clause.listRanges.foldRight(nonlinearLeaf) {
       case ((o @ Num(_, o2), hd, tl), dt) =>
         Function(
           "hook_LIST_range_long",

diff --git a/runtime/collections/hash.cpp b/runtime/collections/hash.cpp
@@ -134,6 +134,12 @@ void k_hash(block *arg, void *h) {
             add_hash64(h, *intptr);
             break;
           }
+          case MINT_LAYOUT + 128: {
+            auto *intptr = (uint64_t *)(argintptr + offset);
+            add_hash64(h, intptr[0]);
+            add_hash64(h, intptr[1]);
+            break;
+          }
           case MINT_LAYOUT + 160: {
             auto *intptr = (uint64_t *)(argintptr + offset);
             add_hash64(h, intptr[0]);

diff --git a/runtime/collections/kelemle.cpp b/runtime/collections/kelemle.cpp
@@ -143,6 +143,16 @@ bool hook_KEQUAL_eq(block *arg1, block *arg2) {
           }
           break;
         }
+        case MINT_LAYOUT + 128: {
+          auto *child1ptr = (int64_t *)(child1intptr);
+          auto *child2ptr = (int64_t *)(child2intptr);
+          bool cmp
+              = child1ptr[0] == child2ptr[0] && child1ptr[1] == child2ptr[1];
+          if (!cmp) {
+            return false;
+          }
+          break;
+        }
         case MINT_LAYOUT + 160: {
           auto *child1ptr = (int64_t *)(child1intptr);
           auto *child2ptr = (int64_t *)(child2intptr);

diff --git a/test/defn/hash-mint.kore b/test/defn/hash-mint.kore
diff --git a/test/defn/k-files/hash-mint.k b/test/defn/k-files/hash-mint.k
@@ -3,15 +3,18 @@ module HASH-MINT
 
   syntax MInt{160}
   syntax MInt{256}
+  syntax MInt{128}
 
   configuration <k> $PGM:K </k>
-                <state> 0p256 |-> 1p256 0p160 |-> 1p160 </state>
+                <state> 0p256 |-> 1p256 0p160 |-> 1p160 0p128 |-> 1p128 </state>
 
-  syntax KItem ::= foo() | bar()
+  syntax KItem ::= foo() | bar() | baz()
 
   rule <k> foo() => bar() ~> State [ 0p256 ] ...</k>
        <state> State </state>
-  rule <k> bar() => State [ 0p160 ] ...</k>
+  rule <k> bar() => baz() ~> State [ 0p160 ] ...</k>
+       <state> State </state>
+  rule <k> baz() => State [ 0p128 ] ...</k>
        <state> State </state>
 
 endmodule
diff --git a/test/input/hash-mint.in b/test/input/hash-mint.in
@@ -1 +1 @@
-LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'TEST'Unds'KItem{}())))
+LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}())))
diff --git a/test/input/same-name-diff-value/transferFunds.in b/test/input/same-name-diff-value/transferFunds.in
@@ -0,0 +1,2 @@
+LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortOps{}, SortKItem{}}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),inj{SortOp{}, SortOps{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))))))
+
diff --git a/test/output/hash-mint.out.diff b/test/output/hash-mint.out.diff
@@ -1 +1 @@
-Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))),Lbl'-LT-'state'-GT-'{}(\left-assoc{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256")),inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160")),inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))
+Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("1p128")),kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))))
diff --git a/test/output/same-name-diff-value/transferFunds.proof.out.diff b/test/output/same-name-diff-value/transferFunds.proof.out.diff
@@ -0,0 +1,29 @@
+version: 13
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
+  arg: kore[Lbl'Stop'Map{}()]
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))]
+function: LblinitGeneratedTopCell{} ()
+rule: 231 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))]
+function: LblinitKCell{} (0)
+rule: 232 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))]
+hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))]
+  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
+hook result: kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))]
+function: Lblproject'Coln'Ops{} (0:0)
+rule: 313 1
+  VarK = kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))]
+function: LblinitAccountsCell{} (1)
+rule: 227 0
+function: LblinitGeneratedCounterCell{} (2)
+rule: 230 0
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(Lbl'Stop'AccountCellMap{}()),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
+rule: 191 4
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  VarACCT = kore[\dv{SortInt{}}("0")]
+  VarO = kore[Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))]
+  VarVALUE = kore[\dv{SortInt{}}("5")]
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'balance'-GT-'{}(\dv{SortInt{}}("5"))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
diff --git a/test/proof/k-files/same-name-diff-value.k b/test/proof/k-files/same-name-diff-value.k
@@ -0,0 +1,64 @@
+module SAME-NAME-DIFF-VALUE
+    imports INT
+    imports K-EQUAL
+    imports BOOL
+
+    configuration <k> $PGM:Ops </k>
+                  <accounts>
+                    <account multiplicity="*" type="Map">
+                        <acctID>   0   </acctID>
+                        <balance>  0   </balance>
+                    </account>
+                  </accounts>
+
+    syntax Ops ::= Op ";" Ops [symbol(seq)]
+                | Op 
+
+    syntax Op ::= "#transferFunds" Int Int Int
+                | "#init" Int Int
+
+    syntax NoOp ::= "#finish" 
+
+
+    rule <k> #init ACCT VALUE ; O:Op => O </k>
+         <accounts>
+            ( .Bag
+                  =>
+                 <account>
+                    <acctID> ACCT </acctID>
+                    <balance> VALUE </balance>
+                </account>
+            )
+         </accounts>
+
+     rule <k> #transferFunds ACCT ACCT VALUE => .K ... </k>
+         <account>
+           <acctID> ACCT </acctID>
+           <balance> ORIGFROM </balance>
+         </account>
+      requires VALUE <=Int ORIGFROM
+
+
+      rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
+         <account>
+           <acctID> ACCTFROM </acctID>
+           <balance> ORIGFROM => ORIGFROM -Int VALUE </balance>
+           ...
+         </account>
+         <account>
+           <acctID> ACCTTO </acctID>
+           <balance> ORIGTO => ORIGTO +Int VALUE </balance>
+           ...
+         </account>
+      requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
+      [preserves-definedness]
+
+    rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => .K ... </k>
+         <account>
+           <acctID> ACCTFROM </acctID>
+           <balance> ORIGFROM </balance>
+           ...
+         </account>
+      requires VALUE >Int ORIGFROM
+
+endmodule