Skip to content

Conversation

@JKTKops
Copy link
Contributor

@JKTKops JKTKops commented Jul 23, 2021

Fixes #2740

The problem appears to arise because substitution information isn't carried into the call to simplifyRightHandSide from simplify'. This change makes Kore.Reachability.Claim.simplify' more closely match Kore.Rewrite.Rule.Simplify.simplifyClaimRule.worker.


Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.000457 0
test/regression-evm/test-sum-to-n.sh -0.003909 0
test/regression-evm/test-branching-no-invalid.sh -0.000326 0
test/regression-evm/test-straight-line-no-invalid.sh -0.000283 0.000000
test/regression-evm/test-branching-invalid.sh -0.000331 -0.000000
test/regression-evm/test-pop1.sh -0.000284 0
test/regression-evm/test-straight-line.sh -0.000277 0.005702
test/regression-evm/test-sumTo10.sh -0.000792 0.002084
test/regression-wasm/test-locals.sh -0.000303 0.000005
test/regression-wasm/test-simple-arithmetic.sh -0.000426 0.000012
test/regression-wasm/test-wrc20.sh -0.001744 0.002561
test/regression-wasm/test-loops.sh -0.001062 -0.000067
test/regression-wasm/test-memory.sh -0.000666 -0.000000

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh 0.000000 0.000000
test/regression-evm/test-sum-to-n.sh -0.003625 0
test/regression-evm/test-branching-no-invalid.sh 0.000000 0
test/regression-evm/test-straight-line-no-invalid.sh -0.000000 -0.000000
test/regression-evm/test-branching-invalid.sh -0.000035 0
test/regression-evm/test-pop1.sh 0.000000 0
test/regression-evm/test-straight-line.sh 0.000000 0
test/regression-evm/test-sumTo10.sh -0.000000 0.004570
test/regression-wasm/test-locals.sh 0.000008 -0.000000
test/regression-wasm/test-simple-arithmetic.sh 0.000036 0.000001
test/regression-wasm/test-wrc20.sh 0.000529 0.001500
test/regression-wasm/test-loops.sh 0.000129 0.000001
test/regression-wasm/test-memory.sh 0.000115 0.000000

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh 0.007263 -0.101920
test/regression-evm/test-sum-to-n.sh 0.008898 0
test/regression-evm/test-branching-no-invalid.sh 0.008141 0
test/regression-evm/test-straight-line-no-invalid.sh 0.009629 0
test/regression-evm/test-branching-invalid.sh 0.007983 0
test/regression-evm/test-pop1.sh 0.009479 0
test/regression-evm/test-straight-line.sh 0.009436 -0.005669
test/regression-evm/test-sumTo10.sh 0.001953 -0.002113
test/regression-wasm/test-locals.sh 0.022896 -0.000231
test/regression-wasm/test-simple-arithmetic.sh 0.022016 -0.000219
test/regression-wasm/test-wrc20.sh 0.027975 -0.000721
test/regression-wasm/test-loops.sh 0.020354 -0.000161
test/regression-wasm/test-memory.sh 0.020312 -0.000026

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh 0.000000 0
test/regression-evm/test-sum-to-n.sh -0.003673 0
test/regression-evm/test-branching-no-invalid.sh 0.000006 0
test/regression-evm/test-straight-line-no-invalid.sh -0.000000 0
test/regression-evm/test-branching-invalid.sh -0.000000 0.000000
test/regression-evm/test-pop1.sh 0.000000 0
test/regression-evm/test-straight-line.sh -0.000000 -0.000000
test/regression-evm/test-sumTo10.sh -0.000000 0.000001
test/regression-wasm/test-locals.sh 0.000033 0.000191
test/regression-wasm/test-simple-arithmetic.sh 0.000039 0
test/regression-wasm/test-wrc20.sh 0.000527 0.001335
test/regression-wasm/test-loops.sh 0.000095 -0.000062
test/regression-wasm/test-memory.sh 0.000142 0.000058

@JKTKops JKTKops marked this pull request as ready for review July 26, 2021 19:17
@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh 0.000000 0
test/regression-evm/test-sum-to-n.sh -0.003667 0
test/regression-evm/test-branching-no-invalid.sh 0 -0.000000
test/regression-evm/test-straight-line-no-invalid.sh 0 0.000000
test/regression-evm/test-branching-invalid.sh 0.000015 0
test/regression-evm/test-pop1.sh 0 0
test/regression-evm/test-straight-line.sh 0.000000 0
test/regression-evm/test-sumTo10.sh 0.000000 -0.000001
test/regression-wasm/test-locals.sh 0.000008 0
test/regression-wasm/test-simple-arithmetic.sh 0.000049 0.000001
test/regression-wasm/test-wrc20.sh 0.000555 0.002377
test/regression-wasm/test-loops.sh 0.000150 -0.000002
test/regression-wasm/test-memory.sh 0.000144 0

Copy link
Contributor

@ana-pantilie ana-pantilie left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just left a couple of minor comments.

@ana-pantilie ana-pantilie requested a review from geo2a July 27, 2021 14:27
@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.000000 0
test/regression-evm/test-sum-to-n.sh -0.003670 0
test/regression-evm/test-branching-no-invalid.sh -0.000000 0.000000
test/regression-evm/test-straight-line-no-invalid.sh 0 0
test/regression-evm/test-branching-invalid.sh 0.000013 -0.000000
test/regression-evm/test-pop1.sh 0.000000 0.000000
test/regression-evm/test-straight-line.sh 0.000000 0.000000
test/regression-evm/test-sumTo10.sh -0.000000 0.000000
test/regression-wasm/test-locals.sh 0.000008 0
test/regression-wasm/test-simple-arithmetic.sh 0.000049 0
test/regression-wasm/test-wrc20.sh 0.000548 0.004098
test/regression-wasm/test-loops.sh 0.000136 0
test/regression-wasm/test-memory.sh 0.000131 0

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.000005 0
test/regression-evm/test-sum-to-n.sh -0.003665 0
test/regression-evm/test-branching-no-invalid.sh 0.000000 0
test/regression-evm/test-straight-line-no-invalid.sh 0 0
test/regression-evm/test-branching-invalid.sh 0.000001 0
test/regression-evm/test-pop1.sh -0.000013 -0.000000
test/regression-evm/test-straight-line.sh 0 0.005702
test/regression-evm/test-sumTo10.sh -0.000000 0.000001
test/regression-wasm/test-locals.sh 0.000008 0
test/regression-wasm/test-simple-arithmetic.sh 0.000037 -0.000001
test/regression-wasm/test-wrc20.sh 0.000511 0.000577
test/regression-wasm/test-loops.sh 0.000120 0
test/regression-wasm/test-memory.sh 0.000135 0

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-pop1.sh 0.000000 0
test/regression-evm/test-straight-line.sh 0.000000 0
test/regression-evm/test-straight-line-no-invalid.sh 0.000000 0
test/regression-evm/test-branching-invalid.sh -0.000022 0
test/regression-evm/test-sum-to-n.sh -0.003756 0
test/regression-evm/test-branching-no-invalid.sh -0.000000 0
test/regression-evm/test-add0.sh -0.000000 0
test/regression-evm/test-sumTo10.sh -0.000001 -0.000251
test/regression-wasm/test-memory.sh 0.000133 0
test/regression-wasm/test-locals.sh 0.000009 0
test/regression-wasm/test-wrc20.sh 0.000560 -0.000100
test/regression-wasm/test-loops.sh 0.000151 0
test/regression-wasm/test-simple-arithmetic.sh 0.000044 0

@rv-jenkins rv-jenkins merged commit da2c7f8 into master Jul 29, 2021
@rv-jenkins rv-jenkins deleted the issue-2740 branch July 29, 2021 16:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Apply claim LHS substitution to RHS after simplification

5 participants