Tests for value constraint simplifier.

This commit is contained in:
chriseth
2019-03-25 17:16:12 +01:00
parent 061276b28a
commit cf09cd51f0
13 changed files with 580 additions and 3 deletions
@@ -0,0 +1,48 @@
{
let a := and(calldataload(0), 0xffff)
let b := and(calldataload(1), 0xffff)
let c := add(a, b)
let d := add(a, calldataload(7))
let e := sub(add(a, 0x1000000), b)
let f := sub(add(a, 7), 1)
}
// ----
// valueConstraintBasedSimplifier
// a:
// min: 0
// max: 65535
// minB: 0
// maxB: 65535
// b:
// min: 0
// max: 65535
// minB: 0
// maxB: 65535
// c:
// min: 0
// max: 131070
// minB: 0
// maxB: 131071
// d:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// e:
// min: 16711681
// max: 0x0100ffff
// minB: 0
// maxB: 0x02 * 2**24 - 1
// f:
// min: 6
// max: 65541
// minB: 0
// maxB: 131071
// {
// let a := and(calldataload(0), 0xffff)
// let b := and(calldataload(1), 0xffff)
// let c := add(a, b)
// let d := add(a, calldataload(7))
// let e := sub(add(a, 0x1000000), b)
// let f := sub(add(a, 7), 1)
// }
@@ -0,0 +1,46 @@
{
let a := 0xffff
let b := or(shl(20, a), and(calldataload(0), 0xff))
let c := shl(add(300, lt(a, b)), calldataload(0))
let d := shr(add(300, lt(a, b)), calldataload(0))
let e := and(b, 0xff)
let f := not(b)
let g := byte(calldataload(0), 2)
}
// ----
// valueConstraintBasedSimplifier
// a:
// = 65535
// b:
// min: 0
// max: 0x10 * 2**32 - 1
// minB: 0x0fFFF00000
// maxB: 0x0fFFF000ff
// c:
// = 0
// d:
// = 0
// e:
// min: 0
// max: 255
// minB: 0
// maxB: 255
// f:
// min: 0
// max: 2**256 - 1
// minB: 0xFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFfff0000Fff00
// maxB: 0xFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFfff0000Fffff
// g:
// min: 0
// max: 255
// minB: 0
// maxB: 255
// {
// let a := 0xffff
// let b := or(0x0ffff00000, and(calldataload(0), 0xff))
// let c := 0
// let d := 0
// let e := and(b, 0xff)
// let f := not(b)
// let g := byte(calldataload(0), 2)
// }
@@ -0,0 +1,205 @@
{
// restricted to 160 bits
let a := address()
let b := origin()
let c := caller()
let d := coinbase()
let e := create(0, 0, 0)
let f := create2(0, 0, 0, 0)
// restricted to bool
let gb := call(0, 0, 0, 0, 0, 0, 0)
let hb := callcode(0, 0, 0, 0, 0, 0, 0)
let ib := delegatecall(0, 0, 0, 0, 0, 0)
let jb := staticcall(0, 0, 0, 0, 0, 0)
// No restriction starting from here
let k_ := keccak256(0, 0)
let l_ := extcodehash(0)
let m_ := blockhash(0)
let n_ := mload(0)
let o_ := sload(0)
let p_ := balance(0)
let q_ := callvalue()
let r_ := calldatasize()
let s_ := gasprice()
let t_ := extcodesize(0)
let u_ := returndatasize()
let v_ := timestamp()
let w_ := number()
let x_ := difficulty()
let y_ := gaslimit()
let z_ := pc()
let z1_ := msize()
let z2_ := gas()
}
// ----
// valueConstraintBasedSimplifier
// a:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// b:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// c:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// d:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// e:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// f:
// min: 0
// max: 2**160 - 1
// minB: 0
// maxB: 2**160 - 1
// gb:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// hb:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// ib:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// jb:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// k_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// l_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// m_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// n_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// o_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// p_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// q_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// r_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// s_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// t_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// u_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// v_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// w_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// x_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// y_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// z_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// z1_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// z2_:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// {
// let a := address()
// let b := origin()
// let c := caller()
// let d := coinbase()
// let e := create(0, 0, 0)
// let f := create2(0, 0, 0, 0)
// let gb := call(0, 0, 0, 0, 0, 0, 0)
// let hb := callcode(0, 0, 0, 0, 0, 0, 0)
// let ib := delegatecall(0, 0, 0, 0, 0, 0)
// let jb := staticcall(0, 0, 0, 0, 0, 0)
// let k_ := keccak256(0, 0)
// let l_ := extcodehash(0)
// let m_ := blockhash(0)
// let n_ := mload(0)
// let o_ := sload(0)
// let p_ := balance(0)
// let q_ := callvalue()
// let r_ := calldatasize()
// let s_ := gasprice()
// let t_ := extcodesize(0)
// let u_ := returndatasize()
// let v_ := timestamp()
// let w_ := number()
// let x_ := difficulty()
// let y_ := gaslimit()
// let z_ := pc()
// let z1_ := msize()
// let z2_ := gas()
// }
@@ -0,0 +1,74 @@
{
let a := and(calldataload(0), 0xf)
let b := and(calldataload(1), 0xf)
let c := add(b, 2) // overlaps with a
let d := add(b, 0x100) // does not overlap with a
let e := lt(a, c)
let f := lt(a, d)
let g := lt(c, a)
let h := lt(d, a)
let r := lt(a, a) // currently unknown, might change later.
let x := gt(d, a)
let y := gt(c, a)
}
// ----
// valueConstraintBasedSimplifier
// a:
// min: 0
// max: 15
// minB: 0
// maxB: 15
// b:
// min: 0
// max: 15
// minB: 0
// maxB: 15
// c:
// min: 2
// max: 17
// minB: 0
// maxB: 31
// d:
// min: 256
// max: 271
// minB: 0
// maxB: 511
// e:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// f:
// = 1
// g:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// h:
// = 0
// r:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// x:
// = 1
// y:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// {
// let a := and(calldataload(0), 0xf)
// let b := and(calldataload(1), 0xf)
// let c := add(b, 2)
// let d := add(b, 0x100)
// let e := lt(a, c)
// let f := 1
// let g := lt(c, a)
// let h := 0
// let r := lt(a, a)
// let x := 1
// let y := gt(c, a)
// }
@@ -0,0 +1,25 @@
{
let x := 7
let a := eq(x, x)
let b := eq(x, and(calldataload(0), 1)) // not equal
let c := eq(calldataload(0), calldataload(1))
}
// ----
// valueConstraintBasedSimplifier
// x:
// = 7
// a:
// = 1
// b:
// = 0
// c:
// min: 0
// max: 1
// minB: 0
// maxB: 1
// {
// let x := 7
// let a := 1
// let b := 0
// let c := eq(calldataload(0), calldataload(1))
// }
@@ -9,6 +9,8 @@
}
// ----
// valueConstraintBasedSimplifier
// x:
// = 2
// {
// let x := 2
// if 1
@@ -5,6 +5,11 @@
}
// ----
// valueConstraintBasedSimplifier
// x:
// min: 0
// max: 255
// minB: 0
// maxB: 255
// {
// let x := and(callvalue(), 0xff)
// if 1
@@ -0,0 +1,54 @@
{
function f() -> x, y {}
let a, b := f()
let d := a
let e := b
a := 1
b := 3
a, b := f()
let s := a
let t := b
}
// ----
// valueConstraintBasedSimplifier
// x:
// = 0
// y:
// = 0
// d:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// e:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// a:
// = 1
// b:
// = 3
// s:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// t:
// min: 0
// max: 2**256 - 1
// minB: 0
// maxB: 2**256 - 1
// {
// function f() -> x, y
// {
// }
// let a, b := f()
// let d := a
// let e := b
// a := 1
// b := 3
// a, b := f()
// let s := a
// let t := b
// }