Stop simplifying the left-hand side of equations #2392

emarzion · 2021-02-05T17:00:47Z

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!

ttuegel · 2021-02-06T02:05:31Z

kore/src/Kore/Equation/Simplification.hs

+        Monad.unless
+            ((isTop . predicate) simplifiedCond)


The problem is this: Before, we would return early if any of the simplifiedResults (i.e. any branch) had a predicate which was not \top. Now, we only return early on that branch. If you swap the order of Logic.observeAllT and returnOriginalIfAborted below (changing the order of nesting LogicT and ExceptT) then all will be well: the entire computation will exit early if any branch exits early.

This reverts commit b395875.

This reverts commit 2a67a33.

This reverts commit dc2e22b.

This reverts commit 571268d.

This reverts commit cd162fd.

emarzion · 2021-02-23T15:15:33Z

I'm getting the following error:

./kwasm prove --backend haskell tests/proofs/wrc20-spec.k WRC20-LEMMAS --format-failures \
	--concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive,WASM-DATA.get-Existing,WASM-DATA.set-Extend
kore-exec: [237865963] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /Users/emarzion/wasm-semantics/././tests/proofs/wrc20-spec.k:10:11-46:84
  #Not ( {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 1 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 6 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 2 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 5 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 3 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 4 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 4 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 3 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 5 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 2 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 6 , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 1 , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR +Int 7 , 1 )
    #Equals
      #getRange ( BM , ADDR , 1 )
    }
  #And
    {
      #getRange ( #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 ) , ADDR , 1 )
    #Equals
      #getRange ( BM , ADDR +Int 7 , 1 )
    } )
#And
  <wasm>
    <instrs>
      _DotVar2
    </instrs>
    <valstack>
      _37
    </valstack>
    <curFrame>
      <locals>
        _DotVar10
      </locals>
      <curModIdx>
        CUR:Int
      </curModIdx>
    </curFrame>
    <moduleRegistry>
      _38
    </moduleRegistry>
    <moduleIds>
      _39
    </moduleIds>
    <moduleInstances>
      <moduleInst>
        <modIdx>
          CUR
        </modIdx>
        <exports>
          _25
        </exports>
        <types>
          1 |-> [ i64  .ValTypes ] -> [ i64  .ValTypes ]
        </types>
        <nextTypeIdx>
          _26
        </nextTypeIdx>
        <funcAddrs>
          _0 [ NEXTFUNCIDX:Int <- NEXTADDR:Int ]
        </funcAddrs>
        <nextFuncIdx>
          NEXTFUNCIDX +Int 1
        </nextFuncIdx>
        <tabIds>
          _27
        </tabIds>
        <tabAddrs>
          _28
        </tabAddrs>
        <memIds>
          _29
        </memIds>
        <memAddrs>
          0 |-> MEMADDR:Int
        </memAddrs>
        <globIds>
          _30
        </globIds>
        <globalAddrs>
          _31
        </globalAddrs>
        <nextGlobIdx>
          _32
        </nextGlobIdx>
        <moduleMetadata>
          <moduleFileName>
            _33
          </moduleFileName>
          <moduleId>
            _34
          </moduleId>
          <funcIds>
            _35
          </funcIds>
          <typeIds>
            _36
          </typeIds>
        </moduleMetadata>
      </moduleInst> _DotVar7
    </moduleInstances>
    <nextModuleIdx>
      _40
    </nextModuleIdx>
    <mainStore>
      <funcs>
        <funcDef>
          <fAddr>
            NEXTADDR
          </fAddr>
          <fCode>
            #block ( [ .ValTypes ] , #loop ( [ .ValTypes ] , #local.get ( 1 )  i64 . const 8  i64 . ge_u  #br_if ( 1 )  #local.get ( 0 )  i64 . const 56  #local.get ( 1 )  i64 . const 8  i64 . mul  i64 . sub  i64 . shl  i64 . const 56  i64 . shr_u  i64 . const 56  i64 . const 8  #local.get ( 1 )  i64 . mul  i64 . sub  i64 . shl  #local.get ( 2 )  i64 . add  #local.set ( 2 )  #local.get ( 1 )  i64 . const 1  i64 . add  #local.set ( 1 )  #br ( 0 )  .EmptyStmts )  .EmptyStmts )  #local.get ( 2 )  .EmptyStmts
          </fCode>
          <fType>
            [ i64  .ValTypes ] -> [ i64  .ValTypes ]
          </fType>
          <fLocal>
            [ i64  i64  .ValTypes ]
          </fLocal>
          <fModInst>
            CUR
          </fModInst>
          <funcMetadata>
            <funcId>
              $i64.reverse_bytes
            </funcId>
            <localIds>
              .Map
            </localIds>
          </funcMetadata>
        </funcDef>
      </funcs>
      <nextFuncAddr>
        NEXTADDR +Int 1
      </nextFuncAddr>
      <tabs>
        _20
      </tabs>
      <nextTabAddr>
        _21
      </nextTabAddr>
      <mems>
        <memInst>
          <mAddr>
            MEMADDR
          </mAddr>
          <mmax>
            _DotVar9
          </mmax>
          <msize>
            SIZE
          </msize>
          <mdata>
            #setRange ( BM , ADDR , #getRange ( BM , ADDR +Int 7 , 1 ) +Int ( #getRange ( BM , ADDR +Int 6 , 1 ) +Int ( #getRange ( BM , ADDR +Int 5 , 1 ) +Int ( #getRange ( BM , ADDR +Int 4 , 1 ) +Int ( #getRange ( BM , ADDR +Int 3 , 1 ) +Int ( #getRange ( BM , ADDR +Int 2 , 1 ) +Int ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) <<Int 8 ) , 8 )
          </mdata>
        </memInst> _DotVar4
      </mems>
      <nextMemAddr>
        _22
      </nextMemAddr>
      <globals>
        _23
      </globals>
      <nextGlobAddr>
        _24
      </nextGlobAddr>
    </mainStore>
    <deterministicMemoryGrowth>
      _41
    </deterministicMemoryGrowth>
  </wasm>
#And
  {
    false
  #Equals
    <mAddr>
      MEMADDR
    </mAddr> in_keys ( _DotVar4 )
  }
#And
  {
    false
  #Equals
    <modIdx>
      CUR
    </modIdx> in_keys ( _DotVar7 )
  }
#And
  {
    true
  #Equals
    0 <=Int ADDR
  }
#And
  {
    true
  #Equals
    ADDR +Int 8 <=Int SIZE *Int 65536
  }
#And
  {
    true
  #Equals
    ADDR <Int 4294967296
  }

kore/src/Kore/Equation/Simplification.hs

Co-authored-by: Octavian Mircea Sebe <[email protected]>

Request addressed.

emarzion added 2 commits February 4, 2021 23:07

rewriting simplifyEquation

65cff08

observeT -> lift

efbdade

ttuegel reviewed Feb 6, 2021

View reviewed changes

emarzion added 3 commits February 8, 2021 01:44

switching order of LogicT and ExceptT

1c6663d

Merge branch 'master' into no-simplify-lhs

b296540

restoring pointfree style

77b99da

emarzion force-pushed the no-simplify-lhs branch from 10509b3 to 77b99da Compare February 9, 2021 07:12

emarzion added 23 commits February 9, 2021 01:13

updating regression tests

571268d

updating regressions + goldens

dc2e22b

wasm regression tests

2a67a33

fixing wrc20 test

b395875

Merge branch 'master' into no-simplify-lhs

16f6342

test

cd162fd

adding simplification attribute

389976c

adding simplification attribute

4d9ef61

adding simplification attribute

e8eb5df

trigger build

be0eaac

adding simplification attribute

170e019

adding simplification attribute

f7df8d2

trigger build

11848c8

adding simplification attribute

393116f

adding simplification attribute

2ba80e7

adding simplification attribute

90ca692

adding simplification attribute

77231e4

removing test-issue-2095

dd3e4fe

Revert "fixing wrc20 test"

99908ee

This reverts commit b395875.

Revert "wasm regression tests"

46aa6c7

This reverts commit 2a67a33.

Revert "updating regressions + goldens"

fcc73bf

This reverts commit dc2e22b.

Revert "updating regression tests"

3b44beb

This reverts commit 571268d.

Revert "test"

e72afce

This reverts commit cd162fd.

emarzion added 2 commits February 19, 2021 17:15

Merge branch 'master' into no-simplify-lhs

ede6d19

Update Simplification.hs

b2f7eb5

emarzion and others added 6 commits March 8, 2021 12:25

fixing merge conflict

2af0464

import fix

bb2cd38

typo

ddff2b5

Format with stylish-haskell

9e0588c

fixing merge

8761783

fix import

b37f401

emarzion marked this pull request as ready for review March 8, 2021 19:29

MirceaS reviewed Mar 9, 2021

View reviewed changes

kore/src/Kore/Equation/Simplification.hs Show resolved Hide resolved

ttuegel requested review from ttuegel and MirceaS March 9, 2021 15:25

emarzion added 2 commits March 9, 2021 15:27

returning Equation pattern match check

6119b75

Merge branch 'master' into no-simplify-lhs

1cb4fc5

MirceaS previously requested changes Mar 9, 2021

View reviewed changes

kore/src/Kore/Equation/Simplification.hs Outdated Show resolved Hide resolved

ttuegel approved these changes Mar 10, 2021

View reviewed changes

emarzion and others added 2 commits March 10, 2021 09:30

Update kore/src/Kore/Equation/Simplification.hs

1c682b9

Co-authored-by: Octavian Mircea Sebe <[email protected]>

Merge branch 'master' into no-simplify-lhs

7a12cbf

emarzion requested a review from MirceaS March 10, 2021 16:13

emarzion merged commit 95b6c10 into master Mar 10, 2021

emarzion deleted the no-simplify-lhs branch March 10, 2021 16:29

MirceaS mentioned this pull request Mar 10, 2021

Simplification rule for in_keys breaks map ceil #2384

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Stop simplifying the left-hand side of equations #2392

Stop simplifying the left-hand side of equations #2392

Uh oh!

emarzion commented Feb 5, 2021

Uh oh!

ttuegel Feb 6, 2021

Uh oh!

emarzion commented Feb 23, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Stop simplifying the left-hand side of equations #2392

Stop simplifying the left-hand side of equations #2392

Uh oh!

Conversation

emarzion commented Feb 5, 2021

Review checklist

Uh oh!

ttuegel Feb 6, 2021

Choose a reason for hiding this comment

Uh oh!

emarzion commented Feb 23, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!