Skip to content

Commit 68e80be

Browse files
butterunderflowbutterunderflow
authored
support i64 operations (#93)
1 parent a50630d commit 68e80be

File tree

7 files changed

+393
-2
lines changed

7 files changed

+393
-2
lines changed

‎benchmarks/wasm/i64_ops.wat‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
(module
2+
(type (;0;) (func (param i32)))
3+
(type (;1;) (func))
4+
(import "console" "assert" (func (;0;) (type 0)))
5+
6+
(func (;1;) (type 1)
7+
(local i64 i64 i32)
8+
i64.const 42
9+
local.set 0
10+
i64.const 10
11+
local.set 1
12+
i32.const 3
13+
local.set 2
14+
15+
;; arithmetic
16+
local.get 0
17+
local.get 1
18+
i64.add
19+
i64.const 52
20+
i64.eq
21+
call 0
22+
23+
local.get 0
24+
local.get 1
25+
i64.sub
26+
i64.const 32
27+
i64.eq
28+
call 0
29+
30+
local.get 0
31+
local.get 1
32+
i64.mul
33+
i64.const 420
34+
i64.eq
35+
call 0
36+
37+
local.get 0
38+
local.get 1
39+
i64.div_s
40+
i64.const 4
41+
i64.eq
42+
call 0
43+
44+
local.get 0
45+
local.get 1
46+
i64.rem_u
47+
i64.const 2
48+
i64.eq
49+
call 0
50+
51+
;; bitwise
52+
local.get 0
53+
local.get 1
54+
i64.and
55+
i64.const 10
56+
i64.eq
57+
call 0
58+
59+
local.get 0
60+
local.get 1
61+
i64.or
62+
i64.const 42
63+
i64.eq
64+
call 0
65+
66+
local.get 0
67+
local.get 1
68+
i64.xor
69+
i64.const 32
70+
i64.eq
71+
call 0
72+
73+
;; shifts and rotates
74+
local.get 0
75+
local.get 2
76+
i64.extend_i32_u
77+
i64.shl
78+
i64.const 336
79+
i64.eq
80+
call 0
81+
82+
local.get 0
83+
local.get 2
84+
i64.extend_i32_u
85+
i64.shr_s
86+
i64.const 5
87+
i64.eq
88+
call 0
89+
90+
local.get 0
91+
local.get 2
92+
i64.extend_i32_u
93+
i64.rotr
94+
i64.const 4611686018427387909
95+
i64.eq
96+
call 0
97+
98+
;; comparisons
99+
local.get 0
100+
local.get 1
101+
i64.eq
102+
i32.eqz
103+
call 0
104+
105+
local.get 0
106+
local.get 1
107+
i64.lt_s
108+
i32.eqz
109+
call 0
110+
111+
local.get 0
112+
local.get 1
113+
i64.gt_u
114+
call 0
115+
116+
local.get 0
117+
local.get 1
118+
i64.ge_s
119+
call 0
120+
121+
;; integer extension
122+
i32.const -7
123+
i64.extend_i32_s
124+
i64.const -7
125+
i64.eq
126+
call 0
127+
128+
i32.const -7
129+
i64.extend_i32_u
130+
i64.const 4294967289
131+
i64.eq
132+
call 0
133+
)
134+
135+
(export "test_i64" (func 1))
136+
)

‎headers/wasm/concrete_num.hpp‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,36 @@ struct Num {
152152
return res;
153153
}
154154

155+
// i32.rem_s (Signed remainder with traps on division by zero)
156+
inline Num i32_rem_s(const Num &other) const {
157+
int32_t divisor = other.toInt();
158+
int32_t dividend = this->toInt();
159+
if (divisor == 0) {
160+
throw std::runtime_error("i32.rem_s: Division by zero");
161+
}
162+
// WebAssembly defines INT_MIN % -1 == 0
163+
if (dividend == INT32_MIN && divisor == -1) {
164+
Num res(0);
165+
debug_print("i32.rem_s", *this, other, res);
166+
return res;
167+
}
168+
Num res(dividend % divisor);
169+
debug_print("i32.rem_s", *this, other, res);
170+
return res;
171+
}
172+
173+
// i32.rem_u (Unsigned remainder with traps on division by zero)
174+
inline Num i32_rem_u(const Num &other) const {
175+
uint32_t divisor = other.toUInt();
176+
uint32_t dividend = this->toUInt();
177+
if (divisor == 0) {
178+
throw std::runtime_error("i32.rem_u: Division by zero");
179+
}
180+
Num res(static_cast<int32_t>(dividend % divisor));
181+
debug_print("i32.rem_u", *this, other, res);
182+
return res;
183+
}
184+
155185
// i32.shl (Shift Left): *this << other (shift count masked by 31)
156186
inline Num i32_shl(const Num &other) const {
157187
uint32_t shift_amount = other.toUInt() & 0x1F;
@@ -204,6 +234,14 @@ struct Num {
204234
return res;
205235
}
206236

237+
// i64.extend_i32_s: sign-extend low 32 bits to i64
238+
inline Num i32_extend_to_i64() const {
239+
int64_t result_s = static_cast<int64_t>(this->toInt());
240+
Num res(result_s);
241+
debug_print("i32.extend_to_i64", *this, *this, res);
242+
return res;
243+
}
244+
207245
// i64.eq (Equals): *this == other
208246
inline Num i64_eq(const Num &other) const {
209247
Num res = WasmBool(this->toUInt64() == other.toUInt64());
@@ -327,6 +365,36 @@ struct Num {
327365
return res;
328366
}
329367

368+
// i64.rem_s (Signed remainder with traps on division by zero)
369+
inline Num i64_rem_s(const Num &other) const {
370+
int64_t divisor = other.toInt64();
371+
int64_t dividend = this->toInt64();
372+
if (divisor == 0) {
373+
throw std::runtime_error("i64.rem_s: Division by zero");
374+
}
375+
// WebAssembly defines INT64_MIN % -1 == 0
376+
if (dividend == INT64_MIN && divisor == -1) {
377+
Num res(0);
378+
debug_print("i64.rem_s", *this, other, res);
379+
return res;
380+
}
381+
Num res(dividend % divisor);
382+
debug_print("i64.rem_s", *this, other, res);
383+
return res;
384+
}
385+
386+
// i64.rem_u (Unsigned remainder with traps on division by zero)
387+
inline Num i64_rem_u(const Num &other) const {
388+
uint64_t divisor = other.toUInt64();
389+
uint64_t dividend = this->toUInt64();
390+
if (divisor == 0) {
391+
throw std::runtime_error("i64.rem_u: Division by zero");
392+
}
393+
Num res(static_cast<int64_t>(dividend % divisor));
394+
debug_print("i64.rem_u", *this, other, res);
395+
return res;
396+
}
397+
330398
// i64.shl (Shift Left): *this << other (shift count masked by 63)
331399
inline Num i64_shl(const Num &other) const {
332400
uint64_t shift_amount = other.toUInt64() & 0x3F;

‎headers/wasm/symbolic_impl.hpp‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
#define WASM_SYMBOLIC_IMPL_HPP
33

44
#include "symbolic_decl.hpp"
5+
#include "wasm/symval_decl.hpp"
56
#include "wasm/z3_env.hpp"
67

78
inline z3::expr Symbolic::build_z3_expr_aux() {
@@ -59,6 +60,9 @@ inline z3::expr Symbolic::build_z3_expr_aux() {
5960
case SHR_S: {
6061
return z3::ashr(left, right);
6162
}
63+
case REM_U: {
64+
return z3::urem(left, right);
65+
}
6266
case GEQ_BOOL: {
6367
return left >= right;
6468
}

‎headers/wasm/symval_decl.hpp‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ enum BinOperation {
2323
GEU_BOOL, // Unsigned greater than or equal (return a boolean)
2424
SHR_U, // Shift right unsigned
2525
SHR_S, // Shift right signed
26+
REM_U, // Unsigned remainder
2627
B_AND, // Bitwise AND
2728
B_XOR, // Bitwise XOR
2829
B_OR, // Bitwise OR
@@ -31,7 +32,8 @@ enum BinOperation {
3132

3233
enum UnaryOperation {
3334
NOT, // bool not
34-
BOOL2BV, // bool to bitvector
35+
BOOL2BV, // bool to bitvector,
36+
EXTEND, // bitvector extension, extend i32 to i64
3537
};
3638

3739
class Symbolic;
@@ -75,6 +77,8 @@ struct SymVal {
7577
SymVal extract(int high, int low) const;
7678
SymVal bv2bool() const;
7779
SymVal bool2bv() const;
80+
SymVal rem_u(const SymVal &other) const;
81+
SymVal extend_to_i64() const; // only for i32 symbolic values, extend to i64 by sign extension
7882
// TODO: add bitwise operations, and use the underlying bitvector theory
7983

8084
bool is_concrete() const;

‎headers/wasm/symval_impl.hpp‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,10 @@ inline SymVal SymVal::bool2bv() const {
5353
return SVFactory::make_unary(BOOL2BV, *this);
5454
}
5555

56+
inline SymVal SymVal::extend_to_i64() const {
57+
return SVFactory::make_unary(EXTEND, *this);
58+
}
59+
5660
inline SymVal SymVal::lt(const SymVal &other) const {
5761
return SVFactory::make_binary(LT_BOOL, *this, other);
5862
}
@@ -89,6 +93,10 @@ inline SymVal SymVal::shr_s(const SymVal &other) const {
8993
return SVFactory::make_binary(SHR_S, *this, other);
9094
}
9195

96+
inline SymVal SymVal::rem_u(const SymVal &other) const {
97+
return SVFactory::make_binary(REM_U, *this, other);
98+
}
99+
92100
inline SymVal SymVal::is_zero() const {
93101
return SVFactory::make_binary(
94102
EQ_BOOL, *this, SVFactory::make_concrete_bv(I32V(0), symptr->width()));

0 commit comments

Comments
 (0)