Refactoring the branching mechanism #4248

Baltoli · 2024-04-15T09:06:54Z

Transfer of: runtimeverification/pyk#1072

This PR that uses branching information from the backend (for which support was enabled by runtimeverification/pyk#942) to simplify the branching mechanism, potentially making the extract_branches obsolete and only creating NDBranches in the presence of true non-determinism.

I've done a preliminary testing in Kontrol, more info in comments below.

pyk/src/pyk/cterm/symbolic.py

pyk/src/pyk/kcfg/explore.py

pyk/src/pyk/cterm/symbolic.py

pyk/src/pyk/kcfg/explore.py

PetarMax · 2024-04-23T14:57:42Z

As a first example, I have that the KCFG of the CSE execution of ArithmeticCallTest.test_double_add transforms from this

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 0
│   statusCode: STATUSCODE:StatusCode
│
│  (1024 steps)
├─ 7 (split)
│   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 1
│   statusCode: STATUSCODE:StatusCode
┃
┃ (branch)
┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int
┃  │
┃  ├─ 8
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │
┃  │  (73 steps)
┃  └─ 10 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2357
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┗━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   │
   ├─ 9
   │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: STATUSCODE:StatusCode
   │
   │  (413 steps)
   ├─ 11
   │   k: #execute ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: EVMC_SUCCESS
   ┃
   ┃ (1 step)
   ┣━━┓
   ┃  │
   ┃  ├─ 12
   ┃  │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   ┃  │   pc: 550
   ┃  │   callDepth: 1
   ┃  │   statusCode: EVMC_REVERT
   ┃  │
   ┃  │  (72 steps)
   ┃  └─ 14 (leaf, terminal)
   ┃      k: #halt ~> CONTINUATION:K
   ┃      pc: 2474
   ┃      callDepth: 0
   ┃      statusCode: EVMC_REVERT
   ┃
   ┗━━┓
      │
      ├─ 13 (split)
      │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
      │   pc: 128
      │   callDepth: 1
      │   statusCode: EVMC_SUCCESS
      ┃
      ┃ (branch)
      ┣━━┓ constraint: VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
      ┃  │
      ┃  ├─ 20
      ┃  │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
      ┃  │   pc: 128
      ┃  │   callDepth: 1
      ┃  │   statusCode: EVMC_SUCCESS
      ┃  │
      ┃  │  (321 steps)
      ┃  ├─ 18 (terminal)
      ┃  │   k: #halt ~> CONTINUATION:K
      ┃  │   pc: 248
      ┃  │   callDepth: 0
      ┃  │   statusCode: EVMC_SUCCESS
      ┃  │
      ┃  ┊  constraint: true
      ┃  ┊  subst: OMITTED SUBST
      ┃  └─ 6 (leaf, target, terminal)
      ┃      k: #halt ~> CONTINUATION:K
      ┃      pc: PC_CELL_5d410f2a:Int
      ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
      ┃      statusCode: STATUSCODE_FINAL:StatusCode
      ┃
      ┗━━┓ constraint: ( notBool VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) )
         │
         ├─ 21
         │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
         │   pc: 128
         │   callDepth: 1
         │   statusCode: EVMC_SUCCESS
         │
         │  (331 steps)
         └─ 19 (leaf, terminal)
             k: #halt ~> CONTINUATION:K
             pc: 3736
             callDepth: 0
             statusCode: EVMC_REVERT

which is not great, and in which simultaneous applications of multiple specifications of the underlying functions cause non-deterministic branching, to this

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 0
│   statusCode: STATUSCODE:StatusCode
│   src: test/ArithmeticCall.t.sol:6:33
│
│  (1024 steps)
├─ 7 (split)
│   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 1
│   statusCode: STATUSCODE:StatusCode
│   src: test/ArithmeticCall.t.sol:6:33
┃
┃ (branch)
┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int
┃  │
┃  ├─ 9
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (73 steps)
┃  └─ 11 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2357
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┣━━┓ constraints:
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  ┃     ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
┃  │
┃  ├─ 21
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (486 steps)
┃  └─ 15 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2474
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┣━━┓ constraints:
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  ┃     VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  │
┃  ├─ 24
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (735 steps)
┃  ├─ 18 (terminal)
┃  │   k: #halt ~> CONTINUATION:K
┃  │   pc: 248
┃  │   callDepth: 0
┃  │   statusCode: EVMC_SUCCESS
┃  │   src: test/ArithmeticCall.t.sol:9:12
┃  │
┃  ┊  constraint: true
┃  ┊  subst: OMITTED SUBST
┃  └─ 6 (leaf, target, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: PC_CELL_5d410f2a:Int
┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃      statusCode: STATUSCODE_FINAL:StatusCode
┃
┗━━┓ constraints:
   ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
   ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   ┃     ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) <=Int VV0_x_114b9705:Int
   ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   │
   ├─ 25
   │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: STATUSCODE:StatusCode
   │   src: test/ArithmeticCall.t.sol:6:33
   │
   │  (745 steps)
   └─ 19 (leaf, terminal)
       k: #halt ~> CONTINUATION:K
       pc: 3736
       callDepth: 0
       statusCode: EVMC_REVERT

where there are no non-deterministic branches and all branching conditions are present.

PetarMax · 2024-04-23T14:58:00Z

In a recent proof, also, the two branchings below were characterised as non-deterministic, but their constraints are now fully captured:

┃
┃ (branch)
┣━━┓ constraint: ( X:Int ==Int ( X:Int *Int Y:Int ) /Word Y:Int orBool Y:Int ==Int 0 )
┃  │
┃  ├─ 65
┃  │   k: JUMPI --- bool2Word ( ( X:Int ==Int ( X:Int *Int Y:Int ) /Word ...
┃  │   pc: ---
┃  │   callDepth: ---
┃  │   statusCode: EVMC_SUCCESS
┃  │
┃  ...
┃  ┃
┃  ┃ (branch)
┃  ┣━━┓ constraint: ( Z:Int ==Int ( Z:Int *Int T:Int ) /Word T:Int orBool T:Int ==Int 0 )
┃  ┃  │
┃  ┃  └─ 75 (leaf, refuted)
┃  ┃      k: JUMPI --- bool2Word ( ( Z:Int ==Int ( Z:Int *Int T:Int ) /Word ...
┃  ┃      pc: ---
┃  ┃      callDepth: ---
┃  ┃      statusCode: EVMC_SUCCESS
┃  ┃
┃  ┗━━┓ constraints:
┃     ┃     ( notBool T:Int ==K 0 )
┃     ┃     ( notBool Z:Int ==K ( Z:Int *Int T:Int ) /Word T:Int )
┃     │
┃     ...
┃
┗━━┓ constraints:
	 ┃     ( notBool Y:Int ==K 0 )
	 ┃     ( notBool X:Int ==K ( X:Int *Int Y:Int ) /Word Y:Int )
	 │
	 ├─ 66
	 │   k: JUMPI --- bool2Word ( ( X:Int ==Int ( X:Int *Int Y:Int ) /Word ...
	 │   pc: ---
	 │   callDepth: ---
	 │   statusCode: EVMC_SUCCESS
	 │
	 ...

ehildenb · 2024-04-23T15:12:42Z

It looks great! It would be good to also run it on the entire KEVM and Kontrol test-suite, and update expected outputs there, and post draft PRs to those pull requests. This will change output there, so we need to make sure we know that it will work before merging this, so that we don't end up blocking other merges to KEVM and Kontrol.

PetarMax · 2024-04-24T14:45:39Z

@ehildenb @tothtamas28 This PR, together with the accompanying KEVM and Kontrol draft PRs, is passing CI. There were no changes required to KEVM, and an update of a few expected outputs in Kontrol. The update shows that the resulting KCFGs are more readable and that there are no more NDBranches.

ehildenb

Approving, but consider Tamas suggestion.

PetarMax added 2 commits April 15, 2024 10:05

refactoring the branching mechanism

640ebe5

removing prints

1247b6e

Baltoli added the pyk label Apr 15, 2024

Baltoli assigned PetarMax Apr 15, 2024

Baltoli mentioned this pull request Apr 15, 2024

Refactoring the branching mechanism runtimeverification/pyk#1072

Closed

PetarMax added the enhancement label Apr 16, 2024

PetarMax added 3 commits April 16, 2024 17:11

Merge branch 'develop' into petar/efficient-branching

d6ddc21

Merge branch 'develop' into petar/efficient-branching

eb269d1

Merge branch 'develop' into petar/efficient-branching

f3819de

PetarMax requested review from tothtamas28 and ehildenb April 23, 2024 08:20

tothtamas28 reviewed Apr 23, 2024

View reviewed changes

PetarMax and others added 3 commits April 23, 2024 12:18

adding NextState, removing extract_branches

95535fa

Merge branch 'develop' into petar/efficient-branching

55c196f

adjusting expected outputs

6b445fc

PetarMax marked this pull request as ready for review April 23, 2024 14:41

Merge branch 'develop' into petar/efficient-branching

982d56b

ehildenb approved these changes Apr 24, 2024

View reviewed changes

PetarMax added the automerge label Apr 24, 2024

tothtamas28 approved these changes Apr 24, 2024

View reviewed changes

rv-jenkins merged commit b896d78 into develop Apr 24, 2024
19 checks passed

rv-jenkins deleted the petar/efficient-branching branch April 24, 2024 15:24

This was referenced Apr 25, 2024

Test:pyk #4248 runtimeverification/evm-semantics#2403

Closed

Test: pyk #4248 runtimeverification/kontrol#528

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactoring the branching mechanism #4248

Refactoring the branching mechanism #4248

Baltoli commented Apr 15, 2024 •

edited by PetarMax

Loading

PetarMax commented Apr 23, 2024

PetarMax commented Apr 23, 2024

ehildenb commented Apr 23, 2024

PetarMax commented Apr 24, 2024

ehildenb left a comment

Refactoring the branching mechanism #4248

Refactoring the branching mechanism #4248

Conversation

Baltoli commented Apr 15, 2024 • edited by PetarMax Loading

PetarMax commented Apr 23, 2024

PetarMax commented Apr 23, 2024

ehildenb commented Apr 23, 2024

PetarMax commented Apr 24, 2024

ehildenb left a comment

Choose a reason for hiding this comment

Baltoli commented Apr 15, 2024 •

edited by PetarMax

Loading