search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
449 stars 149 forks source link

Error while matching rule pattern (Java backend) #766

Closed hjorthjort closed 3 years ago

hjorthjort commented 5 years ago

Trying to prove a fairly simple spec, the prover runs into to some issue. Output:


==========================================
Top term when exception was thrown:
==========================================

<wasm>(<k>(DotVar1_81:K),, <valstack>(_:__KWASM-LEMMAS(<_>_(SIZE_79:Int),, _:__KWASM-LEMMAS(<_>_(EA_77:Int),, _:__KWASM-LEMMAS(<_>_(ADDR_78:Int),, R_VALSTACK_102:ValStack)))))
/\
ConjunctiveFormula(
  new substitutions:
    _==K_(DotVar0_80:K,, <valstack>(R_VALSTACK_102:ValStack))
)

SPEC ERROR: /home/hjorthjort/polkadot-verification/deps/wasm-semantics/tests/proofs/memory-spec.k Location(7,10,7,78)
==================================
Success execution paths: 0
Failed execution paths: 0
Paths in progress: 1
Longest path: 10 steps
Stats for each phase, time, used memory, implicit main GC time percentage:
Total                 :    4.199 s,        73 MB, gc:  2.929 %
  Parsing             :    4.104 s,        65 MB, gc:  2.997 %
  Init                :    0.045 s,        68 MB, gc:  0.000 %
  Execution           :    0.050 s,        73 MB, gc:  0.000 %

Init+Execution time:       0.096 s
  query build time                 :    0.002 s,      #          6

  Time and top-level event counts:
  resolveFunctionAndAnywhere time  :    0.016 s,      #        250
    evaluateFunction time            :    0.012 s,      #          7
      builtin evaluation               :           ,      #          3
      function rule                    :           ,      #          2
      no function rules                :           ,      #          2
    applyAnywhereRules time          :    0.000 s,      #        135
      no anywhere rules                :           ,      #        135
    remaining time & # cached        :    0.003 s,      #        108
  impliesSMT time                  :    0.002 s,      #          6

  Recursive event counts:
  resolveFunctionAndAnywhere time  :           ,      #          4
    evaluateFunction time            :           ,      #          4
      builtin evaluation               :           ,      #          0
      function rule                    :           ,      #          0
      no function rules                :           ,      #          2
    applyAnywhereRules time          :           ,      #          0
      no anywhere rules                :           ,      #          0
    # cached                         :           ,      #          0

Max memory : 8192 MB
==================================

[Error] Critical:  (Index 4 out of bounds for length 4)
  while matching rule pattern:
    Subject: DotVar1_81:K
    Pattern: #KRewrite(#KSequence( OR (i32.const__KWASM-LEMMAS(R_VAL:Int),{ 0})
OR (listStmt(R_S:Stmt,,  OR (.List{"listStmt"}(.KList),{ 2}) OR (R_SS:Stmts,{
3})),{ 2, 3}) OR (R_V:Val,{ 1}), R_DotVar1:K),, InnerRHSRewrite{
[#KSequence(<_>_(R_VAL:Int), R_DotVar1:K), R_DotVar1:K, #KSequence(R_S:Stmt,
R_DotVar1:K), #KSequence(R_S:Stmt, R_SS:Stmts, R_DotVar1:K)] })
  while matching rule pattern:
    Subject: <k>(DotVar1_81:K)
    Pattern: <k>(#KRewrite(#KSequence( OR (i32.const__KWASM-LEMMAS(R_VAL:Int),{
0}) OR (listStmt(R_S:Stmt,,  OR (.List{"listStmt"}(.KList),{ 2}) OR
(R_SS:Stmts,{ 3})),{ 2, 3}) OR (R_V:Val,{ 1}), R_DotVar1:K),, InnerRHSRewrite{
[#KSequence(<_>_(R_VAL:Int), R_DotVar1:K), R_DotVar1:K, #KSequence(R_S:Stmt,
R_DotVar1:K), #KSequence(R_S:Stmt, R_SS:Stmts, R_DotVar1:K)] }))
  while matching rule pattern:
    Subject: <wasm>(<k>(DotVar1_81:K),,
<valstack>(_:__KWASM-LEMMAS(<_>_(SIZE_79:Int),,
_:__KWASM-LEMMAS(<_>_(EA_77:Int),, _:__KWASM-LEMMAS(<_>_(ADDR_78:Int),,
R_VALSTACK_102:ValStack)))))
    Pattern: <wasm>(<k>(#KRewrite(#KSequence( OR
(i32.const__KWASM-LEMMAS(R_VAL:Int),{ 0}) OR (listStmt(R_S:Stmt,,  OR
(.List{"listStmt"}(.KList),{ 2}) OR (R_SS:Stmts,{ 3})),{ 2, 3}) OR (R_V:Val,{
1}), R_DotVar1:K),, InnerRHSRewrite{ [#KSequence(<_>_(R_VAL:Int), R_DotVar1:K),
R_DotVar1:K, #KSequence(R_S:Stmt, R_DotVar1:K), #KSequence(R_S:Stmt,
R_SS:Stmts, R_DotVar1:K)] })),,  OR (<valstack>(#KRewrite(R_VALSTACK:ValStack,,
InnerRHSRewrite{ [null, _:__KWASM-LEMMAS(R_V:Val,, R_VALSTACK:ValStack), null,
null] })),{ 1}) OR (THE_VARIABLE:K,{ 0, 2, 3}))
[Warning] Internal: execution phase: missing SMTLib translation for #KSequence
. Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for #KSequence)
[Warning] Internal: execution phase: missing SMTLib translation for
.List{"listStmt"} . Please re-run with the --debug-z3 flag. Search the logs
starting with 'Z3 warning' to see the Z3 implication that generated the
warning. (missing SMTLib translation for .List{"listStmt"})
[Warning] Internal: execution phase: missing SMTLib translation for <valstack>
. Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for <valstack>)
Makefile:180: recipe for target 'tests/proofs/memory-spec.k.prove' failed
make: *** [tests/proofs/memory-spec.k.prove] Error 113

Here's a minimal example. Kompile the following module with the java backend (kompile --backend java kwasm-lemmas.k) and try to prove the following spec (kprove memory-spec.k)

Module:

module KWASM-LEMMAS
    imports INT
    imports LIST

    syntax Val ::= "<" "i32" ">" Int    [klabel(<_>_)]
 // --------------------------------------------------

    syntax ValStack ::= ".ValStack"
                   | Val      ":"  ValStack
 // ---------------------------------------

    configuration
      <wasm>
        <k> $PGM:Stmts </k>
        <valstack> .ValStack </valstack>
      </wasm>

    syntax Stmts      ::= List{Stmt      , ""} [klabel(listStmt)]
 // -------------------------------------------------------------
    rule          <k> (S:Stmt .Stmts) => S       ... </k>
    rule [step] : <k> (S:Stmt SS)     => S ~> SS ... </k> requires SS =/=K .Stmts

    syntax Stmt ::= "i32" "." "const" Int
 // -----------------------------------------
    rule <k> i32 . const VAL => < i32 > VAL ... </k>

    rule <k>        V:Val    => .        ... </k>
         <valstack> VALSTACK => V : VALSTACK </valstack>
endmodule

Spec:

requires "kwasm-lemmas.k"

module MEMORY-SPEC
    imports KWASM-LEMMAS

    rule <k> (i32.const ADDR i32.const EA i32.const SIZE):Stmts => . ... </k>

endmodule
hjorthjort commented 5 years ago

I found the offending Java file and managed to produce the following stack trace before the error get thrown further up.

Got exception of type class java.lang.ArrayIndexOutOfBoundsException
java.lang.ArrayIndexOutOfBoundsException: 4
    at org.kframework.backend.java.symbolic.FastRuleMatcher$2.transform(FastRuleMatcher.java:694)
    at org.kframework.backend.java.symbolic.FastRuleMatcher$2.transform(FastRuleMatcher.java:676)
    at org.kframework.backend.java.kil.KItem.accept(KItem.java:869)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.getRightHandSide(FastRuleMatcher.java:676)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.addUnification(FastRuleMatcher.java:628)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:335)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAndLog(FastRuleMatcher.java:288)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:429)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAndLog(FastRuleMatcher.java:288)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:429)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAndLog(FastRuleMatcher.java:288)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchWithAutomaton(FastRuleMatcher.java:203)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:130)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:181)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:739)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.lambda$prove$1(InitializeRewriter.java:252)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
    at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1382)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:482)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:472)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:566)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.prove(InitializeRewriter.java:255)
    at org.kframework.kprove.KProve.run(KProve.java:60)
    at org.kframework.kprove.KProveFrontEnd.run(KProveFrontEnd.java:92)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:59)
    at org.kframework.main.Main.runApplication(Main.java:119)
    at org.kframework.main.Main.runApplication(Main.java:108)
    at org.kframework.main.Main.main(Main.java:54)
Got KEMException
hjorthjort commented 5 years ago

Adding the flag --boundary-cells k makes the issue go away, unclear why, but good enough for me for now.

ehildenb commented 3 years ago

Closing this because --boundary-cells fixes the issue. If it's reproducable on teh Haskell backend, please open a new bug report with reproduction steps targeting that backend.