Only emitting side_conditions if all occurrences of the same variable…

… are equal (#1155) In this PR, we inverse the order in which we create the decision tree when a rule has a side condition. Previously, even when we had 2 or more variables with the same name having different values, the side condition decision trees were generated, and we only evaluated the variables matching after evaluating the side condition. After this PR, we inverse this order and evaluate the variables matching first and then the side condition. This issue was discovered in the context of side conditions proof events being emitted and being true but without ever being applied, as we have a mismatch in the variable names and values. This PR fixes: Pi-Squared-Inc/pi2#2124 We added a regression test that reproduced this issue, and it's now fixed!
runtimeverification · Oct 17, 2024 · 7ab1dec · 7ab1dec
1 parent fc9602c
commit 7ab1dec
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