Skip to content

Commit f20c7a7

Browse files
mojtaba-eshghiemojtaba-eshghie
committed
Feature #67: Adding experiment results for the baseline (light version)
1 parent 9d04584 commit f20c7a7

86 files changed

Lines changed: 26608 additions & 4197 deletions

File tree

Some content is hidden

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

‎use-cases/dynamically-mined-invariant-denoising/analysis.ipynb‎

Lines changed: 60 additions & 41 deletions
Large diffs are not rendered by default.

‎use-cases/dynamically-mined-invariant-denoising/boxplot_invariants_removed.png‎

64 Bytes
Loading

‎use-cases/dynamically-mined-invariant-denoising/combined_reduction_ratios.png‎

-1.17 KB
Loading

‎use-cases/dynamically-mined-invariant-denoising/erc20.json‎

Whitespace-only changes.

‎use-cases/dynamically-mined-invariant-denoising/output/erc20.json‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
[
2+
{
3+
"predicates_before_reduction": 95,
4+
"predicates_after_reduction": 63,
5+
"reduction_ratio": 0.6631578947368421,
6+
"total_parsing_time": 0.0005500316619873047,
7+
"total_reduction_time": 4.150881290435791,
8+
"contract": "./invariants/erc20/0x1600c2e08acb830f2a4ee4d34b48594dade48651-TurexToken.inv.json"
9+
},
10+
{
11+
"predicates_before_reduction": 78,
12+
"predicates_after_reduction": 46,
13+
"reduction_ratio": 0.5897435897435898,
14+
"total_parsing_time": 0.0004525184631347656,
15+
"total_reduction_time": 3.722658634185791,
16+
"contract": "./invariants/erc20/0x1fee5588cb1de19c70b6ad5399152d8c643fae7b-PhunToken.inv.json"
17+
},
18+
{
19+
"predicates_before_reduction": 175,
20+
"predicates_after_reduction": 96,
21+
"reduction_ratio": 0.5485714285714286,
22+
"total_parsing_time": 0.0008111000061035156,
23+
"total_reduction_time": 8.162627458572388,
24+
"contract": "./invariants/erc20/0x28e57c27368d1475a3ce49a25c48c40b85e7f7e1-TetherUS.inv.json"
25+
},
26+
{
27+
"predicates_before_reduction": 158,
28+
"predicates_after_reduction": 96,
29+
"reduction_ratio": 0.6075949367088608,
30+
"total_parsing_time": 0.0007655620574951172,
31+
"total_reduction_time": 7.1824915409088135,
32+
"contract": "./invariants/erc20/0x37a15c92e67686aa268df03d4c881a76340907e8-PIXIUFINANCE.inv.json"
33+
},
34+
{
35+
"predicates_before_reduction": 108,
36+
"predicates_after_reduction": 68,
37+
"reduction_ratio": 0.6296296296296297,
38+
"total_parsing_time": 0.0006222724914550781,
39+
"total_reduction_time": 5.119410514831543,
40+
"contract": "./invariants/erc20/0x3b2833cd4cfce20c04d0279ccbb8cd827c8bcdbf-Soya.inv.json"
41+
},
42+
{
43+
"predicates_before_reduction": 94,
44+
"predicates_after_reduction": 54,
45+
"reduction_ratio": 0.574468085106383,
46+
"total_parsing_time": 0.0005612373352050781,
47+
"total_reduction_time": 4.4623119831085205,
48+
"contract": "./invariants/erc20/0x4d5d3170f407cacaaa328660c2ee2499055e3b07-Token.inv.json"
49+
},
50+
{
51+
"predicates_before_reduction": 163,
52+
"predicates_after_reduction": 95,
53+
"reduction_ratio": 0.5828220858895705,
54+
"total_parsing_time": 0.0008013248443603516,
55+
"total_reduction_time": 7.675647258758545,
56+
"contract": "./invariants/erc20/0x6f2a550259532f7429530dcb93d86269629e3f2a-CloudProtocol.inv.json"
57+
},
58+
{
59+
"predicates_before_reduction": 282,
60+
"predicates_after_reduction": 159,
61+
"reduction_ratio": 0.5638297872340425,
62+
"total_parsing_time": 0.0011723041534423828,
63+
"total_reduction_time": 14.168088674545288,
64+
"contract": "./invariants/erc20/0x8b68591fe802585a9713bd6ebe75d6c285236c54-DOGEVIPER.inv.json"
65+
},
66+
{
67+
"predicates_before_reduction": 145,
68+
"predicates_after_reduction": 93,
69+
"reduction_ratio": 0.6413793103448275,
70+
"total_parsing_time": 0.0007197856903076172,
71+
"total_reduction_time": 6.957494020462036,
72+
"contract": "./invariants/erc20/0x923f3fe77732ec3fc5327eb52327b06be4e472f8-KPopKorea.inv.json"
73+
},
74+
{
75+
"predicates_before_reduction": 79,
76+
"predicates_after_reduction": 47,
77+
"reduction_ratio": 0.5949367088607594,
78+
"total_parsing_time": 0.0005147457122802734,
79+
"total_reduction_time": 3.806112766265869,
80+
"contract": "./invariants/erc20/0x9fdbdd708b6f7247d57e9281e2073d2b88a67a42-FXCO.inv.json"
81+
},
82+
{
83+
"predicates_before_reduction": 111,
84+
"predicates_after_reduction": 67,
85+
"reduction_ratio": 0.6036036036036037,
86+
"total_parsing_time": 0.0005886554718017578,
87+
"total_reduction_time": 5.197048187255859,
88+
"contract": "./invariants/erc20/0xb2923909b5d8bbe01505121f15a4503b6617dae7-WrappedHeC.inv.json"
89+
},
90+
{
91+
"predicates_before_reduction": 535,
92+
"predicates_after_reduction": 311,
93+
"reduction_ratio": 0.5813084112149532,
94+
"total_parsing_time": 0.0018889904022216797,
95+
"total_reduction_time": 25.105873584747314,
96+
"contract": "./invariants/erc20/0xbc7d4fb8595f4b923ec53533f4bbd641c1910aca-YakuzaInu.inv.json"
97+
},
98+
{
99+
"predicates_before_reduction": 181,
100+
"predicates_after_reduction": 102,
101+
"reduction_ratio": 0.56353591160221,
102+
"total_parsing_time": 0.0008447170257568359,
103+
"total_reduction_time": 8.532665967941284,
104+
"contract": "./invariants/erc20/0xc382e04099a435439725bb40647e2b32dc136806-Cogecoin.inv.json"
105+
},
106+
{
107+
"predicates_before_reduction": 164,
108+
"predicates_after_reduction": 96,
109+
"reduction_ratio": 0.5853658536585366,
110+
"total_parsing_time": 0.0007402896881103516,
111+
"total_reduction_time": 8.461816787719727,
112+
"contract": "./invariants/erc20/0xcc494c97a5d4374ec35bda83570c461c6d6f6079-DFV.inv.json"
113+
},
114+
{
115+
"predicates_before_reduction": 182,
116+
"predicates_after_reduction": 99,
117+
"reduction_ratio": 0.5439560439560439,
118+
"total_parsing_time": 0.0009572505950927734,
119+
"total_reduction_time": 8.861835479736328,
120+
"contract": "./invariants/erc20/0xce90d1d98b5ca16b79c7eedada2454c2564da59e-TokenMintERC20MintableToken.inv.json"
121+
},
122+
{
123+
"predicates_before_reduction": 160,
124+
"predicates_after_reduction": 93,
125+
"reduction_ratio": 0.58125,
126+
"total_parsing_time": 0.0008347034454345703,
127+
"total_reduction_time": 7.377439498901367,
128+
"contract": "./invariants/erc20/0xd4ac90e33ac839c29a3d98c807eeef0c4508bee8-YCCToken.inv.json"
129+
},
130+
{
131+
"predicates_before_reduction": 172,
132+
"predicates_after_reduction": 97,
133+
"reduction_ratio": 0.563953488372093,
134+
"total_parsing_time": 0.000843048095703125,
135+
"total_reduction_time": 8.214195966720581,
136+
"contract": "./invariants/erc20/0xeeb690a0c9958e5375eda5694e754b125a6c972c-EnergyEfficientBitcoin.inv.json"
137+
},
138+
{
139+
"predicates_before_reduction": 206,
140+
"predicates_after_reduction": 115,
141+
"reduction_ratio": 0.558252427184466,
142+
"total_parsing_time": 0.0009043216705322266,
143+
"total_reduction_time": 9.881560325622559,
144+
"contract": "./invariants/erc20/0xf61ae54b74a37be4fc11e9f1a35021848d996afc-EmaxClassic.inv.json"
145+
}
146+
]

‎use-cases/dynamically-mined-invariant-denoising/output/erc20/0x1600c2e08acb830f2a4ee4d34b48594dade48651.json‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,19 +95,23 @@
9595
"executionType": "TxType.NORMAL",
9696
"preconditions": [
9797
"msg.sender != 0",
98+
"ori(Sum(balances[...])) > 0",
9899
"ori(Sum(balances[...])) == 5000000000000000000000000",
99100
"ori(Sum(balances[...])) one of [5000000000000000000000000]",
100101
"msg.value == 0",
101102
"msg.value one of [0]",
103+
"ori(totalSupply_) > 0",
102104
"ori(totalSupply_) == 5000000000000000000000000",
103105
"ori(totalSupply_) one of [5000000000000000000000000]",
104106
"ori(unfrozen) == false",
105107
"ori(owner) != 0",
106108
"msg.sender == ori(owner)"
107109
],
108110
"postconditions": [
111+
"Sum(balances[...]) > 0",
109112
"Sum(balances[...]) == 5000000000000000000000000",
110113
"Sum(balances[...]) one of [5000000000000000000000000]",
114+
"totalSupply_ > 0",
111115
"totalSupply_ == 5000000000000000000000000",
112116
"totalSupply_ one of [5000000000000000000000000]",
113117
"unfrozen == true",
@@ -116,6 +120,8 @@
116120
"Sum(balances[...]) == ori(Sum(balances[...]))",
117121
"msg.sender == owner",
118122
"ori(totalSupply_) == totalSupply_",
123+
"ori(totalSupply_) >= totalSupply_",
124+
"ori(totalSupply_) <= totalSupply_",
119125
"unfrozen != ori(unfrozen)",
120126
"ori(owner) == owner"
121127
],
@@ -175,25 +181,31 @@
175181
"msg.sender != 0",
176182
"_value > 0",
177183
"_to != 0",
184+
"ori(Sum(balances[...])) > 0",
178185
"ori(Sum(balances[...])) == 5000000000000000000000000",
179186
"ori(Sum(balances[...])) one of [5000000000000000000000000]",
180187
"msg.value == 0",
181188
"msg.value one of [0]",
189+
"ori(totalSupply_) > 0",
182190
"ori(totalSupply_) == 5000000000000000000000000",
183191
"ori(totalSupply_) one of [5000000000000000000000000]",
184192
"ori(unfrozen) == true",
185193
"ori(owner) != 0"
186194
],
187195
"postconditions": [
196+
"Sum(balances[...]) > 0",
188197
"Sum(balances[...]) == 5000000000000000000000000",
189198
"Sum(balances[...]) one of [5000000000000000000000000]",
199+
"totalSupply_ > 0",
190200
"totalSupply_ == 5000000000000000000000000",
191201
"totalSupply_ one of [5000000000000000000000000]",
192202
"unfrozen == true",
193203
"elem of balances[...] is one of [5000000000000000000000000]",
194204
"owner != 0",
195205
"Sum(balances[...]) == ori(Sum(balances[...]))",
196206
"ori(totalSupply_) == totalSupply_",
207+
"ori(totalSupply_) >= totalSupply_",
208+
"ori(totalSupply_) <= totalSupply_",
197209
"unfrozen == ori(unfrozen)",
198210
"ori(owner) == owner"
199211
],
@@ -268,16 +280,20 @@
268280
"type": "PptType.CONTRACT",
269281
"executionType": "TxType.NORMAL",
270282
"preconditions": [
283+
"ori(Sum(balances[...])) > 0",
271284
"ori(Sum(balances[...])) == 5000000000000000000000000",
272285
"ori(Sum(balances[...])) one of [5000000000000000000000000]",
286+
"ori(totalSupply_) > 0",
273287
"ori(totalSupply_) == 5000000000000000000000000",
274288
"ori(totalSupply_) one of [5000000000000000000000000]",
275289
"ori(owner) != 0",
276290
"ori(Sum(balances[...])) == ori(totalSupply_)"
277291
],
278292
"postconditions": [
293+
"Sum(balances[...]) > 0",
279294
"Sum(balances[...]) == 5000000000000000000000000",
280295
"Sum(balances[...]) one of [5000000000000000000000000]",
296+
"totalSupply_ > 0",
281297
"totalSupply_ == 5000000000000000000000000",
282298
"totalSupply_ one of [5000000000000000000000000]",
283299
"unfrozen == true",
@@ -288,6 +304,8 @@
288304
"Sum(balances[...]) == totalSupply_",
289305
"ori(Sum(balances[...])) == totalSupply_",
290306
"ori(totalSupply_) == totalSupply_",
307+
"ori(totalSupply_) >= totalSupply_",
308+
"ori(totalSupply_) <= totalSupply_",
291309
"ori(owner) == owner"
292310
],
293311
"falsified_preconditions": [],

0 commit comments

Comments
 (0)