search

runtimeverification / hs-backend-booster

Accelerates K Framework's Haskell backend
BSD 3-Clause "New" or "Revised" License
7 stars 0 forks source link

Incorrect rule application from booster #558

Closed PetarMax closed 7 months ago

PetarMax commented 8 months ago

I am in a configuration where I’m getting this with the booster

┃  ┃  ┃  ┃  ┃  ┃  │  (1 step)
┃  ┃  ┃  ┃  ┃  ┃  ├─ 331
┃  ┃  ┃  ┃  ┃  ┃  │   k: #checkRevert ~> #updateRevertOutput 740 0 ~> #execute ~> CONTINUATION:K
┃  ┃  ┃  ┃  ┃  ┃  │   pc: 3336
┃  ┃  ┃  ┃  ┃  ┃  │   callDepth: 0
┃  ┃  ┃  ┃  ┃  ┃  │   statusCode: EVMC_REVERT
┃  ┃  ┃  ┃  ┃  ┃  │   src: lib/forge-std/src/StdInvariant.sol:72:73
┃  ┃  ┃  ┃  ┃  ┃  │
┃  ┃  ┃  ┃  ┃  ┃  │  (1 step)
┃  ┃  ┃  ┃  ┃  ┃  ├─ 332
┃  ┃  ┃  ┃  ┃  ┃  │   k: #markAsFailed ~> #clearExpectRevert ~> #updateRevertOutput 740 0 ~> #execute ~>  ...
┃  ┃  ┃  ┃  ┃  ┃  │   pc: 3336
┃  ┃  ┃  ┃  ┃  ┃  │   callDepth: 0
┃  ┃  ┃  ┃  ┃  ┃  │   statusCode: EVMC_REVERT
┃  ┃  ┃  ┃  ┃  ┃  │   src: lib/forge-std/src/StdInvariant.sol:72:73

and this with the Haskell backend

┃  ┃  ┃  ┃  ┃  ┃  │  (1 step)
┃  ┃  ┃  ┃  ┃  ┃  ├─ 331
┃  ┃  ┃  ┃  ┃  ┃  │   k: #checkRevert ~> #updateRevertOutput 740 0 ~> #execute ~> CONTINUATION:K
┃  ┃  ┃  ┃  ┃  ┃  │   pc: 3336
┃  ┃  ┃  ┃  ┃  ┃  │   callDepth: 0
┃  ┃  ┃  ┃  ┃  ┃  │   statusCode: EVMC_REVERT
┃  ┃  ┃  ┃  ┃  ┃  │   src: lib/forge-std/src/StdInvariant.sol:72:73
┃  ┃  ┃  ┃  ┃  ┃  │
┃  ┃  ┃  ┃  ┃  ┃  │  (1 step)
┃  ┃  ┃  ┃  ┃  ┃  └─ 335 (leaf, pending)
┃  ┃  ┃  ┃  ┃  ┃      k: #clearExpectRevert ~> #updateRevertOutput 740 0 ~> #execute ~> CONTINUATION:K
┃  ┃  ┃  ┃  ┃  ┃      pc: 3336
┃  ┃  ┃  ┃  ┃  ┃      callDepth: 0
┃  ┃  ┃  ┃  ┃  ┃      statusCode: EVMC_SUCCESS
┃  ┃  ┃  ┃  ┃  ┃      src: lib/forge-std/src/StdInvariant.sol:72:73

with the Haskell backend being correct. The bug reports from both are attached. The rule in question is this:

rule 
  <k> #checkRevert => #clearExpectRevert ... </k>
  <statusCode> SC => EVMC_SUCCESS </statusCode>
  <wordStack> 0 : WS => 1 : WS </wordStack>
  <output> OUT => #buf (512, 0) </output>
  <callDepth> CD </callDepth>
  <expectedRevert>
    <isRevertExpected> true </isRevertExpected>
    <expectedDepth> CD </expectedDepth>
    <expectedReason> REASON </expectedReason>
</expectedRevert>
requires SC =/=K EVMC_SUCCESS
 andBool #matchReason(REASON, #encodeOutput(OUT))

the relevant configuration is this

<k> #checkRevert ~> ... </k>
<statusCode> EVMC_REVERT </statusCode>
<wordStack> 0 : WS </wordStack>
<output> b"\xe5\xe6/\xdd" </output>
 <callDepth> 0 </callDepth>
<expectedRevert>
    <isRevertExpected> true </isRevertExpected>
    <expectedReason>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x04\xe5\xe6/\xdd\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
    </expectedReason>
    <expectedDepth> 0 </expectedDepth>
</expectedRevert>

and I have a claim, proven using kprove, which confirms that #matchReason(REASON, #encodeOutput(OUT)) holds.

bug-hb.tar.gz bug-booster.tar.gz

PetarMax commented 8 months ago

I can confirm that this issue persists in the latest version of the booster that's made its way into K (88ffab54a7266d8c98d5c039ef81143d1d24f3f0).

jberthold commented 8 months ago

Important to know: There is a 2nd rule that produces the #markAsFailed ~> ... which has the dual side condition notBool #matchReason(REASON, #encodeOutput(OUT)). Therefore it was relatively easy to narrow this down to differences in the evaluation of #matchReason, and ultimately #encodeOutput.

A request to simplify (i.e., evaluate) the `#encodeOutput(b"\xe5\xe6/\xdd")`
``` { "format": "KORE", "version": 1, "term": { "tag": "App", "name": "Lbl'Hash'encodeOutput'LParUndsRParUnds'FOUNDRY-CHEAT-CODES'Unds'Bytes'Unds'Bytes", "sorts": [], "args": [ { "tag": "DV", "sort": { "tag": "SortApp", "name": "SortBytes", "args": []}, "value": "\u00e5\u00e6/\u00dd" } ] } } ```
produces a shorter byte array with `booster` (LLVM libnrary)
`"value": "ò\141γ\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0004åæ/Ý\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000"`
than with legacy kore
`"value": "ò\141γ\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000 \u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0004åæ/Ý\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000"`

Note the leading sequence of \u0000 (x 31) in the kore value, followed by a space (char 32 ), followed by the suffix produced by booster

jberthold commented 7 months ago

I tested by evaluating encodeOutput manually and sending a number of its sub-expressions to the simplifier, then I discovered what is probably happening here:

While evaluating encodeArgs(#bytes(...)) (as part of the call to encodeOutput), we have two rules for encodeArgsAux, depending on whether an argument is of static or dynamic type:

https://github.com/runtimeverification/evm-semantics/blob/e3e21b5d1bf3f12b39fd65f6e667f6dfd10206bd/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md?plain=1#L278-L284

However, the definition of #isStaticType appears to be lacking an [owise] on the last equation.

https://github.com/runtimeverification/evm-semantics/blob/e3e21b5d1bf3f12b39fd65f6e667f6dfd10206bd/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md?plain=1#L305-L311

The LLVM backend will arbitrarily choose one of the alternatives (I am not sure how, actually), and apparently is choosing the wrong one in this particular case.

jberthold commented 7 months ago

Would it be possible to re-test this with an evm-semantics from https://github.com/runtimeverification/evm-semantics/pull/2371 ?

PetarMax commented 7 months ago

I can confirm that the rule is correctly applied now. Thank you, @jberthold!