Skip to content

Conversation

@ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Jul 26, 2021

Fixes #2770

Needs #2766, #2758, #2796 and #2805

The TermLike simplifier does not simplify predicates anymore, removing the complicated loop inside the TermLike simplifier. The interface to the simplifier is now simplifyPattern, which takes care of simplifying the term and condition together. This has resulted in multiple unit tests needing changes, in particular those which had too general test data (TermLikes which contained Predicates).


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.046806 0
test/regression-evm/test-sum-to-n.sh -0.029771 0
test/regression-evm/test-branching-no-invalid.sh -0.048803 0
test/regression-evm/test-straight-line-no-invalid.sh -0.054289 0
test/regression-evm/test-branching-invalid.sh -0.048223 0
test/regression-evm/test-pop1.sh -0.054602 -0.000000
test/regression-evm/test-straight-line.sh -0.053532 0
test/regression-evm/test-sumTo10.sh -0.022996 0.129291
test/regression-wasm/test-locals.sh -0.072147 0.000320
test/regression-wasm/test-simple-arithmetic.sh -0.074850 0.000767
test/regression-wasm/test-wrc20.sh -0.037834 0.022781
test/regression-wasm/test-loops.sh -0.079584 0.000115
test/regression-wasm/test-memory.sh -0.067576 0.000217

@github-actions
Copy link

github-actions bot commented Sep 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016401 0.003227
test/regression-evm/test-branching-no-invalid.sh -0.019207 0.000282
test/regression-evm/test-totalSupply.sh 0.006553 0.126554
test/regression-evm/test-lemmas.sh -0.026305 -0.014124
test/regression-evm/test-and0.sh -0.016411 0.009279
test/regression-evm/test-straight-line.sh -0.021201 -0.000318
test/regression-evm/test-branching-invalid.sh -0.018916 -0.000099
test/regression-evm/test-mul0.sh -0.016257 0.003205
test/regression-evm/test-straight-line-no-invalid.sh -0.021612 -0.014747
test/regression-evm/test-sum-to-n.sh -0.001857 0.010306
test/regression-evm/test-pop1.sh -0.019823 0.000444
test/regression-evm/test-sumTo10.sh -0.001003 0.014707
test/regression-evm/test-sha3_bigSize.sh -0.019385 0.000417
test/regression-evm/test-storagevar03.sh 0.002053 -0.233885
test/regression-wasm/test-locals.sh -0.037353 -0.000200
test/regression-wasm/test-simple-arithmetic.sh -0.028992 0.000369
test/regression-wasm/test-loops.sh 0.059424 0.000576
test/regression-wasm/test-wrc20.sh 0.016888 -0.007237
test/regression-wasm/test-memory.sh -0.025845 0.000548

@github-actions
Copy link

github-actions bot commented Sep 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016399 0.009279
test/regression-evm/test-branching-no-invalid.sh -0.019208 0.005175
test/regression-evm/test-totalSupply.sh 0.006545 0.015244
test/regression-evm/test-lemmas.sh -0.026304 0.068126
test/regression-evm/test-and0.sh -0.016411 0.003229
test/regression-evm/test-straight-line.sh -0.021201 0.005519
test/regression-evm/test-branching-invalid.sh -0.018915 0.006633
test/regression-evm/test-mul0.sh -0.016258 0.003229
test/regression-evm/test-straight-line-no-invalid.sh -0.021615 -0.009742
test/regression-evm/test-sum-to-n.sh -0.001860 0.010307
test/regression-evm/test-pop1.sh -0.019822 0.005522
test/regression-evm/test-sumTo10.sh -0.001003 0.014834
test/regression-evm/test-sha3_bigSize.sh -0.019386 0.000420
test/regression-evm/test-storagevar03.sh 0.002043 -0.233136
test/regression-wasm/test-locals.sh -0.037357 -0.000198
test/regression-wasm/test-simple-arithmetic.sh -0.028966 0.000423
test/regression-wasm/test-loops.sh 0.059426 0.000576
test/regression-wasm/test-wrc20.sh 0.016863 -0.007294
test/regression-wasm/test-memory.sh -0.025810 0.000635

@ana-pantilie
Copy link
Contributor Author

I tested the performance locally and test/regression-wasm/test-loops.sh is actually faster on this branch compared to master.

@ana-pantilie ana-pantilie marked this pull request as ready for review September 6, 2021 13:43
@github-actions
Copy link

github-actions bot commented Sep 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016399 -0.001078
test/regression-evm/test-branching-no-invalid.sh -0.019208 0.005175
test/regression-evm/test-totalSupply.sh 0.006546 0.009481
test/regression-evm/test-lemmas.sh -0.026308 0.004211
test/regression-evm/test-and0.sh -0.016412 0.003226
test/regression-evm/test-straight-line.sh -0.021201 0.004682
test/regression-evm/test-branching-invalid.sh -0.018916 0.016488
test/regression-evm/test-mul0.sh -0.016258 0.009279
test/regression-evm/test-straight-line-no-invalid.sh -0.021615 -0.015002
test/regression-evm/test-sum-to-n.sh -0.001861 0.016075
test/regression-evm/test-pop1.sh -0.019822 0.009986
test/regression-evm/test-sumTo10.sh -0.001003 0.011711
test/regression-evm/test-sha3_bigSize.sh -0.019386 0.000419
test/regression-evm/test-storagevar03.sh 0.002060 0.032086
test/regression-wasm/test-locals.sh -0.037357 -0.000198
test/regression-wasm/test-simple-arithmetic.sh -0.028984 0.000358
test/regression-wasm/test-loops.sh 0.059456 0.000577
test/regression-wasm/test-wrc20.sh 0.016852 -0.012649
test/regression-wasm/test-memory.sh -0.025820 0.000571

@github-actions
Copy link

github-actions bot commented Sep 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016392 -0.009777
test/regression-evm/test-branching-no-invalid.sh -0.019197 -0.004982
test/regression-evm/test-totalSupply.sh 0.006551 0.115165
test/regression-evm/test-lemmas.sh -0.026299 -0.008968
test/regression-evm/test-and0.sh -0.016402 -0.010157
test/regression-evm/test-straight-line.sh -0.021175 0.000260
test/regression-evm/test-branching-invalid.sh -0.018898 0.000060
test/regression-evm/test-mul0.sh -0.016246 -0.005977
test/regression-evm/test-straight-line-no-invalid.sh -0.021595 -0.000347
test/regression-evm/test-sum-to-n.sh -0.001854 0.010007
test/regression-evm/test-pop1.sh -0.019822 -0.011599
test/regression-evm/test-addu48u48.sh 0.014902 -0.003994
test/regression-evm/test-sumTo10.sh -0.001002 0.060378
test/regression-evm/test-sha3_bigSize.sh -0.019377 0.009102
test/regression-evm/test-storagevar03.sh 0.002051 -0.228706
test/regression-wasm/test-locals.sh -0.037263 0.000645
test/regression-wasm/test-simple-arithmetic.sh -0.028927 -0.000000
test/regression-wasm/test-loops.sh 0.058787 -0.000067
test/regression-wasm/test-wrc20.sh 0.016856 -0.020679
test/regression-wasm/test-memory.sh -0.025764 -0.000007

simplifiedTerm <- simplifyConditionalTerm sideCondition rewritingTerm
simplifyCondition sideCondition $
Pattern.andCondition simplifiedTerm rewritingCondition
reevaluateFunctions = simplifyPattern
Copy link
Contributor

Choose a reason for hiding this comment

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

Do you think it's useful to keep reevaluateFunctions since it's just another name for simplifyPattern?

@github-actions
Copy link

github-actions bot commented Sep 8, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016391 -0.005977
test/regression-evm/test-branching-no-invalid.sh -0.019196 -0.004982
test/regression-evm/test-totalSupply.sh 0.006551 0.007993
test/regression-evm/test-lemmas.sh -0.026188 0.066946
test/regression-evm/test-and0.sh -0.016403 -0.005978
test/regression-evm/test-straight-line.sh -0.021182 -0.005350
test/regression-evm/test-branching-invalid.sh -0.018899 -0.015194
test/regression-evm/test-mul0.sh -0.016246 -0.010156
test/regression-evm/test-straight-line-no-invalid.sh -0.021600 0.004492
test/regression-evm/test-sum-to-n.sh -0.001863 0.008592
test/regression-evm/test-pop1.sh -0.019809 -0.005139
test/regression-evm/test-addu48u48.sh 0.014898 -0.003994
test/regression-evm/test-sumTo10.sh -0.001002 0.006837
test/regression-evm/test-sha3_bigSize.sh -0.019377 -0.009986
test/regression-evm/test-storagevar03.sh 0.002037 -0.185021
test/regression-wasm/test-locals.sh -0.037263 -0.000002
test/regression-wasm/test-simple-arithmetic.sh -0.028940 -0.000002
test/regression-wasm/test-loops.sh 0.058735 0
test/regression-wasm/test-wrc20.sh 0.016828 -0.001820
test/regression-wasm/test-memory.sh -0.025781 0.000000

@github-actions
Copy link

github-actions bot commented Sep 8, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016391 -0.005977
test/regression-evm/test-branching-no-invalid.sh -0.019197 -0.004982
test/regression-evm/test-totalSupply.sh 0.006548 0.007993
test/regression-evm/test-lemmas.sh -0.026300 -0.002240
test/regression-evm/test-and0.sh -0.016402 -0.010154
test/regression-evm/test-straight-line.sh -0.021182 0.004994
test/regression-evm/test-branching-invalid.sh -0.018898 -0.015912
test/regression-evm/test-mul0.sh -0.016246 -0.005977
test/regression-evm/test-straight-line-no-invalid.sh -0.021591 -0.000867
test/regression-evm/test-sum-to-n.sh -0.001856 0.010008
test/regression-evm/test-pop1.sh -0.019810 -0.005140
test/regression-evm/test-addu48u48.sh 0.014898 -0.003993
test/regression-evm/test-sumTo10.sh -0.001002 0.006411
test/regression-evm/test-sha3_bigSize.sh -0.019377 -0.005937
test/regression-evm/test-storagevar03.sh 0.002071 0.008649
test/regression-wasm/test-locals.sh -0.037263 0.000000
test/regression-wasm/test-simple-arithmetic.sh -0.028931 -0.000000
test/regression-wasm/test-loops.sh 0.058800 0
test/regression-wasm/test-wrc20.sh 0.016887 0.003776
test/regression-wasm/test-memory.sh -0.025769 0

SideCondition variable ->
Bool
areIncludedIn predicates sideCondition =
all (flip isIncludedIn sideCondition) predicates
Copy link
Contributor

Choose a reason for hiding this comment

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

If isIncludedIn is only used here, does it make sense to flip the arguments here instead of simply flipping the arguments in the definition? Of course the name would need to be modified.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I wanted it to be similar to the elem function, so that the order of the arguments is intuitive.

@github-actions
Copy link

github-actions bot commented Sep 9, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016390 -0.006230
test/regression-evm/test-branching-no-invalid.sh -0.019202 -0.010605
test/regression-evm/test-totalSupply.sh 0.006542 0.009321
test/regression-evm/test-lemmas.sh -0.026302 0.003562
test/regression-evm/test-and0.sh -0.016402 -0.010154
test/regression-evm/test-straight-line.sh -0.021193 -0.001116
test/regression-evm/test-branching-invalid.sh -0.018896 -0.092401
test/regression-evm/test-mul0.sh -0.016246 -0.010157
test/regression-evm/test-straight-line-no-invalid.sh -0.021595 -0.052577
test/regression-evm/test-sum-to-n.sh -0.001853 0.010008
test/regression-evm/test-pop1.sh -0.019810 -0.016208
test/regression-evm/test-addu48u48.sh 0.014896 -0.003994
test/regression-evm/test-sumTo10.sh -0.001002 0.010159
test/regression-evm/test-sha3_bigSize.sh -0.019377 -0.006334
test/regression-evm/test-storagevar03.sh 0.002082 -0.240839
test/regression-wasm/test-locals.sh -0.037317 0.045717
test/regression-wasm/test-simple-arithmetic.sh -0.028924 0.000000
test/regression-wasm/test-loops.sh 0.058839 0
test/regression-wasm/test-wrc20.sh 0.016875 -0.002907
test/regression-wasm/test-memory.sh -0.025778 -0.000000

@github-actions
Copy link

github-actions bot commented Sep 9, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-add0.sh -0.016391 -0.010155
test/regression-evm/test-branching-no-invalid.sh -0.019197 -0.004982
test/regression-evm/test-totalSupply.sh 0.006547 0.007993
test/regression-evm/test-lemmas.sh -0.026257 0.026182
test/regression-evm/test-and0.sh -0.016402 -0.010156
test/regression-evm/test-straight-line.sh -0.021182 0.004994
test/regression-evm/test-branching-invalid.sh -0.018898 -0.015194
test/regression-evm/test-mul0.sh -0.016246 -0.010154
test/regression-evm/test-straight-line-no-invalid.sh -0.021595 -0.066687
test/regression-evm/test-sum-to-n.sh -0.001862 0.010008
test/regression-evm/test-pop1.sh -0.019810 -0.016209
test/regression-evm/test-addu48u48.sh 0.014904 -0.003994
test/regression-evm/test-sumTo10.sh -0.001002 0.009930
test/regression-evm/test-sha3_bigSize.sh -0.019377 0.009077
test/regression-evm/test-storagevar03.sh 0.002052 0.015229
test/regression-wasm/test-locals.sh -0.037262 0.000003
test/regression-wasm/test-simple-arithmetic.sh -0.028934 0.000001
test/regression-wasm/test-loops.sh 0.058809 0.000001
test/regression-wasm/test-wrc20.sh 0.016877 -0.000466
test/regression-wasm/test-memory.sh -0.025772 0.000000

@rv-jenkins rv-jenkins merged commit 465dc59 into master Sep 9, 2021
@rv-jenkins rv-jenkins deleted the remove-old-term-simplifier branch September 9, 2021 14:40
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.

Uses of simplifyCondition: remove call from TermLike simplifier

5 participants