Merge remote-tracking branch 'origin/develop'

runtimeverification · Oct 17, 2024 · 035c600 · 035c600
2 parents 84a419e + 7ab1dec
commit 035c600
Show file tree

Hide file tree

Showing 5 changed files with 3,308 additions and 7 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/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/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