Skip to content

Commit 58abe25

Browse files
DavePearceDavePearce
committed
Support SLT, SGT
This adds support for the SLT and SGT bytecodes, along with a minimal number of tests. To do this required adding a method to convert from a "word" to a signed 256 integer. In addition, this fixes a bug related to the ordering of operands for arithmetic operations (ADD/SUB/MUL/DIV). The ordering was the wrong way around!
1 parent cce3096 commit 58abe25

File tree

3 files changed

+175
-51
lines changed

3 files changed

+175
-51
lines changed

‎src/dafny/evm.dfy‎

Lines changed: 42 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -269,8 +269,8 @@ module EVM {
269269
// 0x10
270270
else if opcode == LT then evalLT(vm')
271271
else if opcode == GT then evalGT(vm')
272-
// else if opcode == SLT then evalSLT(vm')
273-
// else if opcode == SGT then evalSGT(vm')
272+
else if opcode == SLT then evalSLT(vm')
273+
else if opcode == SGT then evalSGT(vm')
274274
else if opcode == EQ then evalEQ(vm')
275275
else if opcode == ISZERO then evalISZERO(vm')
276276
// AND
@@ -312,8 +312,8 @@ module EVM {
312312
function method evalADD(vm:T) : Result {
313313
if operands(vm) >= 2
314314
then
315-
var rhs := peek(vm,0) as int;
316-
var lhs := peek(vm,1) as int;
315+
var lhs := peek(vm,0) as int;
316+
var rhs := peek(vm,1) as int;
317317
var sum := (lhs + rhs) % MAX_UINT256;
318318
Result.OK(push(pop(pop(vm)),sum as u256))
319319
else
@@ -326,8 +326,8 @@ module EVM {
326326
function method evalMUL(vm:T) : Result {
327327
if operands(vm) >= 2
328328
then
329-
var rhs := peek(vm,0) as int;
330-
var lhs := peek(vm,1) as int;
329+
var lhs := peek(vm,0) as int;
330+
var rhs := peek(vm,1) as int;
331331
var sum := (lhs * rhs) % MAX_UINT256;
332332
Result.OK(push(pop(pop(vm)),sum as u256))
333333
else
@@ -340,8 +340,8 @@ module EVM {
340340
function method evalSUB(vm:T) : Result {
341341
if operands(vm) >= 2
342342
then
343-
var rhs := peek(vm,0) as int;
344-
var lhs := peek(vm,1) as int;
343+
var lhs := peek(vm,0) as int;
344+
var rhs := peek(vm,1) as int;
345345
var sum := (lhs - rhs) % MAX_UINT256;
346346
Result.OK(push(pop(pop(vm)),sum as u256))
347347
else
@@ -396,6 +396,40 @@ module EVM {
396396
Result.INVALID
397397
}
398398

399+
/**
400+
* Signed less-than comparison.
401+
*/
402+
function method evalSLT(vm:T) : Result {
403+
if operands(vm) >= 2
404+
then
405+
var lhs := Int.wordAsInt256(peek(vm,0));
406+
var rhs := Int.wordAsInt256(peek(vm,1));
407+
if lhs < rhs
408+
then
409+
Result.OK(push(pop(pop(vm)),1))
410+
else
411+
Result.OK(push(pop(pop(vm)),0))
412+
else
413+
Result.INVALID
414+
}
415+
416+
/**
417+
* Signed greater-than comparison.
418+
*/
419+
function method evalSGT(vm:T) : Result {
420+
if operands(vm) >= 2
421+
then
422+
var lhs := Int.wordAsInt256(peek(vm,0));
423+
var rhs := Int.wordAsInt256(peek(vm,1));
424+
if lhs > rhs
425+
then
426+
Result.OK(push(pop(pop(vm)),1))
427+
else
428+
Result.OK(push(pop(pop(vm)),0))
429+
else
430+
Result.INVALID
431+
}
432+
399433
/**
400434
* Equality comparison.
401435
*/

‎src/dafny/util/int.dfy‎

Lines changed: 50 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,28 +13,40 @@
1313
*/
1414
module Int {
1515
// Powers of Two
16+
const TWO_7 : int := 0x0_80;
1617
const TWO_8 : int := 0x1_00;
18+
const TWO_15 : int := 0x0_8000;
1719
const TWO_16 : int := 0x1_0000;
20+
const TWO_31 : int := 0x0_8000_0000;
1821
const TWO_32 : int := 0x1_0000_0000;
22+
const TWO_63 : int := 0x0_8000_0000_0000_0000;
1923
const TWO_64 : int := 0x1_0000_0000_0000_0000;
24+
const TWO_127 : int := 0x0_8000_0000_0000_0000_0000_0000_0000_0000;
2025
const TWO_128 : int := 0x1_0000_0000_0000_0000_0000_0000_0000_0000;
2126
const TWO_160 : int := 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000;
27+
const TWO_255 : int := 0x0_8000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000;
2228
const TWO_256 : int := 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000;
2329

2430
// Signed Integers
25-
const MIN_I8 : int := -0x80;
26-
const MAX_I8 : int := 0x80 - 1;
27-
const MIN_I16 : int := -0x8000;
28-
const MAX_I16 : int := 0x8000 - 1;
29-
const MIN_I32 : int := -0x80000000;
30-
const MAX_I32 : int := 0x80000000 - 1;
31-
const MIN_I64 : int := -0x8000000000000000;
32-
const MAX_I64 : int := 0x8000000000000000 - 1;
31+
const MIN_I8 : int := -TWO_7;
32+
const MAX_I8 : int := TWO_7 - 1;
33+
const MIN_I16 : int := -TWO_15;
34+
const MAX_I16 : int := TWO_15 - 1;
35+
const MIN_I32 : int := -TWO_31;
36+
const MAX_I32 : int := TWO_31 - 1;
37+
const MIN_I64 : int := -TWO_63;
38+
const MAX_I64 : int := TWO_63 - 1;
39+
const MIN_I128 : int := -TWO_127;
40+
const MAX_I128 : int := TWO_127 - 1;
41+
const MIN_I256 : int := -TWO_255;
42+
const MAX_I256 : int := TWO_255 - 1;
3343

3444
newtype{:nativeType "sbyte"} i8 = i:int | MIN_I8 <= i <= MAX_I8
3545
newtype{:nativeType "short"} i16 = i:int | MIN_I16 <= i <= MAX_I16
3646
newtype{:nativeType "int"} i32 = i:int | MIN_I32 <= i <= MAX_I32
3747
newtype{:nativeType "long"} i64 = i:int | MIN_I64 <= i <= MAX_I64
48+
newtype i128 = i:int | MIN_I128 <= i <= MAX_I128
49+
newtype i256 = i:int | MIN_I256 <= i <= MAX_I256
3850

3951
// Unsigned Integers
4052
const MAX_U8 : int := TWO_8 - 1;
@@ -82,4 +94,34 @@ module Int {
8294
var b2 := read_u32(bytes, address+4) as u64;
8395
(b1 * (TWO_32 as u64)) + b2
8496
}
97+
98+
// =========================================================
99+
// Conversion from words (i.e. raw data) to signed data
100+
// =========================================================
101+
102+
// Convert a 256-bit word to a signed 256bit integer. Since words
103+
// are represented as u256, the parameter has type u256. However,
104+
// its important to note that this does not mean the value in
105+
// question represents an unsigned 256 bit integer. Rather, it is a
106+
// signed integer encoded into an unsigned integer.
107+
function method wordAsInt256(w: u256) : i256 {
108+
if w > (MAX_I256 as u256)
109+
then
110+
var v := 1 + MAX_UINT256 - (w as int);
111+
(-v) as i256
112+
else
113+
w as i256
114+
}
115+
116+
117+
// =========================================================
118+
// Sanity Checks
119+
// =========================================================
120+
121+
method test() {
122+
assert wordAsInt256(0) == 0;
123+
assert wordAsInt256(MAX_UINT256 as u256) == -1;
124+
assert wordAsInt256(MAX_I256 as u256) == (MAX_I256 as i256);
125+
assert wordAsInt256((MAX_I256 + 1) as u256) == (MIN_I256 as i256);
126+
}
85127
}

‎src/test/java/dafnyevm/Tests.java‎

Lines changed: 83 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -77,19 +77,19 @@ public void test_mstore_01() {
7777
@Test
7878
public void test_mstore_02() {
7979
// Check can return data from memory.
80-
runExpecting(new int[] { PUSH1, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x7b));
80+
runExpecting(new int[] { PUSH1, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x7b));
8181
}
8282

8383
@Test
8484
public void test_mstore_03() {
8585
// Check can return data from memory.
86-
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x4d7b));
86+
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x4d7b));
8787
}
8888

8989
@Test
9090
public void test_mload_01() {
9191
// Check can read and write data to memory
92-
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x00, MLOAD, PUSH1, 0x20, MSTORE, PUSH1, 0x20, PUSH1, 0x20, RETURN }, UINT32(0x4d7b));
92+
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, MSTORE, PUSH1, 0x00, MLOAD, PUSH1, 0x20, MSTORE, PUSH1, 0x20, PUSH1, 0x20, RETURN }, UINT256(0x4d7b));
9393
}
9494

9595
// ========================================================================
@@ -106,14 +106,14 @@ public void test_mstore8_01() {
106106
public void test_mstore8_02() {
107107
// Check can return data from memory.
108108
runExpecting(new int[] { PUSH1, 0x7b, PUSH1, 0x00, MSTORE8, PUSH1, 0x20, PUSH1, 0x00, RETURN },
109-
shl(UINT32(0x7b), 31));
109+
shl(UINT256(0x7b), 31));
110110
}
111111

112112
@Test
113113
public void test_mstore8_03() {
114114
// Check can return data from memory.
115115
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, MSTORE8, PUSH1, 0x20, PUSH1, 0x00, RETURN },
116-
shl(UINT32(0x7b), 31));
116+
shl(UINT256(0x7b), 31));
117117
}
118118

119119
// ========================================================================
@@ -122,26 +122,26 @@ public void test_mstore8_03() {
122122

123123
@Test
124124
public void test_add_01() {
125-
// Check can add!
126-
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, ADD, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x3));
125+
// 2 + 1 => 3
126+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, ADD, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x3));
127127
}
128128

129129
@Test
130130
public void test_sub_01() {
131-
// Check can subtract!
132-
runExpecting(new int[] { PUSH1, 0x3, PUSH1, 0x1, SUB, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x2));
131+
// 3 - 1 => 2
132+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x3, SUB, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x2));
133133
}
134134

135135
@Test
136136
public void test_mul_01() {
137-
// Check can multiply!
138-
runExpecting(new int[] { PUSH1, 0x3, PUSH1, 0x2, MUL, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x6));
137+
// 2 * 3 => 6
138+
runExpecting(new int[] { PUSH1, 0x3, PUSH1, 0x2, MUL, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x6));
139139
}
140140

141141
@Test
142142
public void test_div_01() {
143-
// Check can divide!
144-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x6, DIV, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x3));
143+
// 6 / 2 => 3
144+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x6, DIV, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x3));
145145
}
146146

147147
// ========================================================================
@@ -150,62 +150,110 @@ public void test_div_01() {
150150

151151
@Test
152152
public void test_lt_01() {
153-
// Check can add!
154-
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
153+
// 2 < 1 = 0
154+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
155155
}
156156

157157
@Test
158158
public void test_lt_02() {
159-
// Check can add!
160-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x1, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x1));
159+
// 1 < 2 = 1
160+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x1, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
161161
}
162162

163163
@Test
164164
public void test_lt_03() {
165-
// Check can add!
166-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
165+
// 2 < 2 => 0
166+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, LT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
167167
}
168168

169169
@Test
170170
public void test_gt_01() {
171-
// Check can add!
172-
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x1));
171+
// 2 > 1 => 1
172+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
173173
}
174174

175175
@Test
176176
public void test_gt_02() {
177-
// Check can add!
178-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x1, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
177+
// 1 > 2 => 0
178+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x1, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
179179
}
180180

181181
@Test
182182
public void test_gt_03() {
183-
// Check can add!
184-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
183+
// 2 > 2 => 0
184+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, GT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
185+
}
186+
187+
@Test
188+
public void test_slt_01() {
189+
// -2 < 1 => 1
190+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, PUSH1, 0x0, SUB, SLT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
191+
}
192+
193+
@Test
194+
public void test_slt_02() {
195+
// 1 < -2 => 0
196+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x0, SUB, PUSH1, 0x1, SLT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
197+
}
198+
199+
@Test
200+
public void test_slt_03() {
201+
// -2 < -1 => 1
202+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x0, SUB, PUSH1, 0x2, PUSH1, 0x0, SUB, SLT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
203+
}
204+
205+
@Test
206+
public void test_slt_04() {
207+
// -1 < -2 => 0
208+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x0, SUB, PUSH1, 0x1, PUSH1, 0x0, SUB, SLT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
209+
}
210+
211+
@Test
212+
public void test_sgt_01() {
213+
// -2 > 1 => 0
214+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, PUSH1, 0x0, SUB, SGT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
215+
}
216+
217+
@Test
218+
public void test_sgt_02() {
219+
// 1 > -2 => 1
220+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x0, SUB, PUSH1, 0x1, SGT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
221+
}
222+
223+
@Test
224+
public void test_sgt_03() {
225+
// -2 > -1 => 0
226+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x0, SUB, PUSH1, 0x2, PUSH1, 0x0, SUB, SGT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
227+
}
228+
229+
@Test
230+
public void test_sgt_04() {
231+
// -1 > -2 => 1
232+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x0, SUB, PUSH1, 0x1, PUSH1, 0x0, SUB, SGT, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
185233
}
186234

187235
@Test
188236
public void test_eq_01() {
189-
// Check can add!
190-
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, EQ, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
237+
// 2 = 1 => 0
238+
runExpecting(new int[] { PUSH1, 0x1, PUSH1, 0x2, EQ, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
191239
}
192240

193241
@Test
194242
public void test_eq_02() {
195-
// Check can add!
196-
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, EQ, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x1));
243+
// 2 = 2 => 1
244+
runExpecting(new int[] { PUSH1, 0x2, PUSH1, 0x2, EQ, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
197245
}
198246

199247
@Test
200248
public void test_iszero_01() {
201-
// Check can add!
202-
runExpecting(new int[] { PUSH1, 0x2, ISZERO, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x0));
249+
// 2 = 0 => 0
250+
runExpecting(new int[] { PUSH1, 0x2, ISZERO, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x0));
203251
}
204252

205253
@Test
206254
public void test_iszero_02() {
207-
// Check can add!
208-
runExpecting(new int[] { PUSH1, 0x0, ISZERO, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x1));
255+
// 0 = 0 => 1
256+
runExpecting(new int[] { PUSH1, 0x0, ISZERO, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x1));
209257
}
210258

211259
// ========================================================================
@@ -221,7 +269,7 @@ public void test_sstore_01() {
221269

222270
@Test
223271
public void test_sstore_02() {
224-
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, SSTORE, PUSH1, 0x00, SLOAD, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT32(0x4d7b));
272+
runExpecting(new int[] { PUSH2, 0x4d, 0x7b, PUSH1, 0x00, SSTORE, PUSH1, 0x00, SLOAD, PUSH1, 0x00, MSTORE, PUSH1, 0x20, PUSH1, 0x00, RETURN }, UINT256(0x4d7b));
225273
}
226274

227275
// ========================================================================
@@ -330,7 +378,7 @@ private byte[] toBytes(int... words) {
330378
* @param x
331379
* @return
332380
*/
333-
private byte[] UINT32(int x) {
381+
private byte[] UINT256(int x) {
334382
if(x < 0) {
335383
throw new IllegalArgumentException("Argument cannot be negative");
336384
}

0 commit comments

Comments
 (0)