Skip to content

Commit fdecda7

Browse files
denis-bogdanasehildenb
denis-bogdanas
authored and
ehildenb
committed
Suhabe benchmarks (#523)
* tests/specs/benchmarks: Added Suhabe benchmarks as tests * tests/specs/benchmarks: Corrected module names. * kevm: Automatically detect smt2 file in prove mode. * kevm: simplified evm.smt2 discovery tests/specs/benchmarks: added readme.md * kevm: restored original *.smt2 discovery. * kevm: Detecting --smt-prelude, using default evm.smt2 when not present.
1 parent 2341c2f commit fdecda7

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

51 files changed

+4487
-1
lines changed

‎kevm

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,20 @@ run_kast() {
5757

5858
run_prove() {
5959
export K_OPTS=-Xmx8G
60-
kprove --directory "$backend_dir" "$run_file" "$@"
60+
61+
# If --smt-prelude is not set and evm.smt2 is present in $run_dir, use it.
62+
smt_prelude_set=
63+
for i in "$@" ; do [[ $i == "--smt-prelude" ]] && smt_prelude_set=true && break ; done
64+
run_dir="$(dirname "$run_file")"
65+
smt_file="$run_dir/evm.smt2"
66+
smt_args=()
67+
if [[ -z $smt_prelude_set ]] && [[ -f "$smt_file" ]]; then
68+
smt_args=(--smt-prelude "$smt_file")
69+
fi
70+
if $debug; then
71+
set -x
72+
fi
73+
kprove --directory "$backend_dir" "${smt_args[@]-}" "$run_file" "$@"
6174
}
6275

6376
run_search() {

‎tests/specs/benchmarks/README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
Specs generated from https://github.com/denis-bogdanas/kevm-verify-benchmarks/tree/jenkins-support
2+
, for all directories starting with `0-`. Originally developed by Suhabe Bugrara.

‎tests/specs/benchmarks/abstract-semantics-segmented-gas.k

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
requires "evm-symbolic.k"
2+
3+
module ABSTRACT-SEMANTICS-SEGMENTED-GAS
4+
imports EVM
5+
imports EVM-SYMBOLIC
6+
7+
// to avoid unnecessary case analyses
8+
rule <k> LT W0 W1 => bool2Word(W0 <Int W1) ~> #push ... </k> [trusted]
9+
rule <k> GT W0 W1 => bool2Word(W0 >Int W1) ~> #push ... </k> [trusted]
10+
rule <k> EQ W0 W1 => bool2Word(W0 ==Int W1) ~> #push ... </k> [trusted]
11+
rule <k> ISZERO W => bool2Word(W ==Int 0 ) ~> #push ... </k> [trusted]
12+
13+
// ########################
14+
// Segmented gas representatioon - #gas construct
15+
// ########################
16+
17+
// accumulate the gas cost and never run out of gas
18+
rule <k> G ~> #deductGas => . ... </k>
19+
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
20+
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
21+
requires #notKLabel(G, "#symCmem")
22+
[trusted, matching(#gas)]
23+
24+
rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>
25+
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM, MEM +Int MEM') </gas>
26+
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
27+
[trusted, matching(#symCmem,#gas)]
28+
29+
rule <k> G ~> #deductGas ... </k>
30+
<gas> INITGAS => #gas(INITGAS, 0, 0) </gas>
31+
requires #notKLabel(INITGAS, "#gas")
32+
[trusted]
33+
34+
rule <k> MU':Int ~> #deductMemory => #symCmem(Cmem(SCHED, MU') -Int Cmem(SCHED, MU)) ~> #deductGas ... </k>
35+
<memoryUsed> MU => MU' </memoryUsed> <schedule> SCHED </schedule>
36+
[trusted]
37+
endmodule

‎tests/specs/benchmarks/abstract-semantics.k

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
requires "abstract-semantics-segmented-gas.k"
2+
requires "evm-symbolic.k"
3+
requires "ecrec-symbolic.k"
4+
5+
module ABSTRACT-SEMANTICS
6+
imports ABSTRACT-SEMANTICS-SEGMENTED-GAS
7+
imports EVM-SYMBOLIC
8+
imports ECREC-SYMBOLIC
9+
imports EVM
10+
11+
12+
// ########################
13+
// Gas - in addition to ABSTRACT-SEMANTICS-COMMON
14+
// ########################
15+
16+
// abstract call gas
17+
// normal functiona call GCAP == GAVAIL
18+
// call chain == 1
19+
rule <k> Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE)
20+
=> #gas(Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE)), 0, 0) ... </k>
21+
requires VALUE ==Int 0
22+
andBool #getKLabelString(GAVAIL) ==String "#gas"
23+
andBool GCAP ==Int GAVAIL
24+
[trusted]
25+
26+
rule <k> Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE)
27+
=> #gas(Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE)) +Int Gcallstipend < SCHED >, 0, 0) ... </k>
28+
requires 0 <Int VALUE
29+
andBool #getKLabelString(GAVAIL) ==String "#gas"
30+
andBool GCAP ==Int GAVAIL
31+
[trusted]
32+
33+
34+
// ########################
35+
// EXTCODESIZE
36+
// ########################
37+
38+
rule <k> EXTCODESIZE ACCT => #extCodeSize(ACCT) ~> #push ... </k> [trusted]
39+
40+
endmodule

‎tests/specs/benchmarks/address00-spec.k

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
requires "abstract-semantics.k"
2+
requires "verification.k"
3+
4+
module ADDRESS00-SPEC
5+
imports ETHEREUM-SIMULATION
6+
imports ABSTRACT-SEMANTICS
7+
imports VERIFICATION
8+
9+
// fn-execute
10+
rule
11+
<k> (#execute => #halt) ~> _ </k>
12+
<exit-code> 1 </exit-code>
13+
<mode> NORMAL </mode>
14+
<schedule> BYZANTIUM </schedule>
15+
<ethereum>
16+
<evm>
17+
<output> _ => #encodeArgs(#address(A0)) </output>
18+
<statusCode> _ => EVMC_SUCCESS </statusCode>
19+
<callStack> _ </callStack>
20+
<interimStates> _ </interimStates>
21+
<touchedAccounts> _ => _ </touchedAccounts>
22+
<callState>
23+
<program> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634b64e492146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505060c4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008190509190505600a165627a7a72305820fef7ba925e24a935e59bb401907893518a66095fa9e2c2506b29051dfdaa6ff80029") </program>
24+
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634b64e492146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505060c4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008190509190505600a165627a7a72305820fef7ba925e24a935e59bb401907893518a66095fa9e2c2506b29051dfdaa6ff80029")) </jumpDests>
25+
<id> #CONTRACT_ID </id> // this
26+
<caller> MSG_SENDER </caller> // msg.sender
27+
<callData> #abiCallData("execute", #address(A0)) </callData> // msg.data
28+
<callValue> 0 </callValue> // msg.value
29+
<wordStack> .WordStack => _ </wordStack>
30+
<localMem> .Map => _ </localMem>
31+
<pc> 0 => _ </pc>
32+
<gas> #gas(INITGAS, 0, 0) => _ </gas>
33+
<memoryUsed> 0 => _ </memoryUsed>
34+
<callGas> _ => _ </callGas>
35+
<static> false </static> // NOTE: non-static call
36+
<callDepth> CD </callDepth>
37+
</callState>
38+
<substate>
39+
<selfDestruct> _ </selfDestruct>
40+
<log> _ </log>
41+
<refund> _ </refund>
42+
</substate>
43+
<gasPrice> _ </gasPrice>
44+
<origin> _ </origin> // tx.origin
45+
<blockhashes> BLOCK_HASHES </blockhashes> // block.blockhash
46+
<block>
47+
<previousHash> _ </previousHash>
48+
<ommersHash> _ </ommersHash>
49+
<coinbase> _ </coinbase> // block.coinbase
50+
<stateRoot> _ </stateRoot>
51+
<transactionsRoot> _ </transactionsRoot>
52+
<receiptsRoot> _ </receiptsRoot>
53+
<logsBloom> _ </logsBloom>
54+
<difficulty> _ </difficulty>
55+
<number> BLOCK_NUM </number> // block.number
56+
<gasLimit> _ </gasLimit>
57+
<gasUsed> _ </gasUsed>
58+
<timestamp> NOW </timestamp> // now = block.timestamp
59+
<extraData> _ </extraData>
60+
<mixHash> _ </mixHash>
61+
<blockNonce> _ </blockNonce>
62+
<ommerBlockHeaders> _ </ommerBlockHeaders>
63+
</block>
64+
</evm>
65+
<network>
66+
<activeAccounts> SetItem(#CONTRACT_ID) SetItem(#CALLEE_ID) SetItem(1) _:Set </activeAccounts>
67+
<accounts>
68+
<account>
69+
<acctID> #CONTRACT_ID </acctID>
70+
<balance> CONTRACT_BAL </balance>
71+
<code> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634b64e492146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505060c4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008190509190505600a165627a7a72305820fef7ba925e24a935e59bb401907893518a66095fa9e2c2506b29051dfdaa6ff80029") </code>
72+
<storage>
73+
_
74+
</storage>
75+
<origStorage>
76+
_
77+
</origStorage>
78+
<nonce> _ </nonce>
79+
</account>
80+
81+
<account>
82+
<acctID> #CALLEE_ID </acctID>
83+
<balance> CALLEE_BAL </balance>
84+
<code> _ </code>
85+
<storage>
86+
_
87+
</storage>
88+
<origStorage>
89+
_
90+
</origStorage>
91+
<nonce> _ </nonce>
92+
</account>
93+
94+
<account>
95+
// precompiled account for ECCREC
96+
<acctID> 1 </acctID>
97+
<balance> 0 </balance>
98+
<code> .WordStack </code>
99+
<storage> .Map </storage>
100+
<origStorage> .Map </origStorage>
101+
<nonce> 0 </nonce>
102+
</account>
103+
104+
105+
...
106+
</accounts>
107+
<txOrder> _ </txOrder>
108+
<txPending> _ </txPending>
109+
<messages> _ </messages>
110+
</network>
111+
</ethereum>
112+
requires
113+
#rangeAddress(#CONTRACT_ID)
114+
andBool #rangeAddress(#CALLEE_ID)
115+
andBool #rangeUInt(256, NOW)
116+
andBool #rangeUInt(128, BLOCK_NUM) // Solidity
117+
118+
// Account address normality
119+
andBool #CONTRACT_ID >Int 0 andBool (notBool #CONTRACT_ID in #precompiledAccounts(BYZANTIUM))
120+
andBool #CALLEE_ID >Int 0 andBool (notBool #CALLEE_ID in #precompiledAccounts(BYZANTIUM))
121+
122+
andBool #rangeUInt(256, CONTRACT_BAL)
123+
andBool #rangeUInt(256, CALLEE_BAL)andBool #range(0 <= CD < 1024)
124+
andBool #rangeAddress(MSG_SENDER)andBool #rangeAddress(A0)
125+
ensures true
126+
127+
128+
129+
130+
endmodule
131+

‎tests/specs/benchmarks/address00.sol

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
pragma solidity 0.4.24;
2+
contract address00 {
3+
function execute(address a0) public returns (address) {
4+
return a0;
5+
}
6+
}
7+

‎tests/specs/benchmarks/bytes00-spec.k

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
requires "abstract-semantics.k"
2+
requires "verification.k"
3+
4+
module BYTES00-SPEC
5+
imports ETHEREUM-SIMULATION
6+
imports ABSTRACT-SEMANTICS
7+
imports VERIFICATION
8+
9+
// fn-execute
10+
rule
11+
<k> (#execute => #halt) ~> _ </k>
12+
<exit-code> 1 </exit-code>
13+
<mode> NORMAL </mode>
14+
<schedule> BYZANTIUM </schedule>
15+
<ethereum>
16+
<evm>
17+
<output> _ => #encodeArgs(#uint256(DATA_LEN)) </output>
18+
<statusCode> _ => EVMC_SUCCESS </statusCode>
19+
<callStack> _ </callStack>
20+
<interimStates> _ </interimStates>
21+
<touchedAccounts> _ => _ </touchedAccounts>
22+
<callState>
23+
<program> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806309c5eabe146044575b600080fd5b348015604f57600080fd5b5060a8600480360381019080803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505060be565b6040518082815260200191505060405180910390f35b6000815190509190505600a165627a7a72305820443b6929f0411657e3b5f5371823da4795cb8ece704713e7934fea316a2af24a0029") </program>
24+
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806309c5eabe146044575b600080fd5b348015604f57600080fd5b5060a8600480360381019080803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505060be565b6040518082815260200191505060405180910390f35b6000815190509190505600a165627a7a72305820443b6929f0411657e3b5f5371823da4795cb8ece704713e7934fea316a2af24a0029")) </jumpDests>
25+
<id> #CONTRACT_ID </id> // this
26+
<caller> MSG_SENDER </caller> // msg.sender
27+
<callData> #abiCallData("execute", #bytes(#buf(DATA_LEN,DATA))) </callData> // msg.data
28+
<callValue> 0 </callValue> // msg.value
29+
<wordStack> .WordStack => _ </wordStack>
30+
<localMem> .Map => _ </localMem>
31+
<pc> 0 => _ </pc>
32+
<gas> #gas(INITGAS, 0, 0) => _ </gas>
33+
<memoryUsed> 0 => _ </memoryUsed>
34+
<callGas> _ => _ </callGas>
35+
<static> false </static> // NOTE: non-static call
36+
<callDepth> CD </callDepth>
37+
</callState>
38+
<substate>
39+
<selfDestruct> _ </selfDestruct>
40+
<log> _ </log>
41+
<refund> _ </refund>
42+
</substate>
43+
<gasPrice> _ </gasPrice>
44+
<origin> _ </origin> // tx.origin
45+
<blockhashes> BLOCK_HASHES </blockhashes> // block.blockhash
46+
<block>
47+
<previousHash> _ </previousHash>
48+
<ommersHash> _ </ommersHash>
49+
<coinbase> _ </coinbase> // block.coinbase
50+
<stateRoot> _ </stateRoot>
51+
<transactionsRoot> _ </transactionsRoot>
52+
<receiptsRoot> _ </receiptsRoot>
53+
<logsBloom> _ </logsBloom>
54+
<difficulty> _ </difficulty>
55+
<number> BLOCK_NUM </number> // block.number
56+
<gasLimit> _ </gasLimit>
57+
<gasUsed> _ </gasUsed>
58+
<timestamp> NOW </timestamp> // now = block.timestamp
59+
<extraData> _ </extraData>
60+
<mixHash> _ </mixHash>
61+
<blockNonce> _ </blockNonce>
62+
<ommerBlockHeaders> _ </ommerBlockHeaders>
63+
</block>
64+
</evm>
65+
<network>
66+
<activeAccounts> SetItem(#CONTRACT_ID) SetItem(#CALLEE_ID) SetItem(1) _:Set </activeAccounts>
67+
<accounts>
68+
<account>
69+
<acctID> #CONTRACT_ID </acctID>
70+
<balance> CONTRACT_BAL </balance>
71+
<code> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806309c5eabe146044575b600080fd5b348015604f57600080fd5b5060a8600480360381019080803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505060be565b6040518082815260200191505060405180910390f35b6000815190509190505600a165627a7a72305820443b6929f0411657e3b5f5371823da4795cb8ece704713e7934fea316a2af24a0029") </code>
72+
<storage>
73+
_
74+
</storage>
75+
<origStorage>
76+
_
77+
</origStorage>
78+
<nonce> _ </nonce>
79+
</account>
80+
81+
<account>
82+
<acctID> #CALLEE_ID </acctID>
83+
<balance> CALLEE_BAL </balance>
84+
<code> _ </code>
85+
<storage>
86+
_
87+
</storage>
88+
<origStorage>
89+
_
90+
</origStorage>
91+
<nonce> _ </nonce>
92+
</account>
93+
94+
<account>
95+
// precompiled account for ECCREC
96+
<acctID> 1 </acctID>
97+
<balance> 0 </balance>
98+
<code> .WordStack </code>
99+
<storage> .Map </storage>
100+
<origStorage> .Map </origStorage>
101+
<nonce> 0 </nonce>
102+
</account>
103+
104+
105+
...
106+
</accounts>
107+
<txOrder> _ </txOrder>
108+
<txPending> _ </txPending>
109+
<messages> _ </messages>
110+
</network>
111+
</ethereum>
112+
requires
113+
#rangeAddress(#CONTRACT_ID)
114+
andBool #rangeAddress(#CALLEE_ID)
115+
andBool #rangeUInt(256, NOW)
116+
andBool #rangeUInt(128, BLOCK_NUM) // Solidity
117+
118+
// Account address normality
119+
andBool #CONTRACT_ID >Int 0 andBool (notBool #CONTRACT_ID in #precompiledAccounts(BYZANTIUM))
120+
andBool #CALLEE_ID >Int 0 andBool (notBool #CALLEE_ID in #precompiledAccounts(BYZANTIUM))
121+
122+
andBool #rangeUInt(256, CONTRACT_BAL)
123+
andBool #rangeUInt(256, CALLEE_BAL)andBool #range(0 <= CD < 1024)
124+
andBool #rangeAddress(MSG_SENDER)andBool #range( 0 <= DATA_LEN < 2 ^Int 16)
125+
ensures true
126+
127+
128+
129+
130+
endmodule
131+

‎tests/specs/benchmarks/bytes00.sol

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
pragma solidity 0.4.24;
2+
contract bytes00 {
3+
function execute(bytes data) public returns (uint) {
4+
return data.length;
5+
}
6+
}
7+

0 commit comments

Comments
 (0)