Skip to content

Commit 8b2eff1

Browse files
butterunderflowbutterunderflow
authored
Support float points (#95)
* reorg * simplification: remove a class smallbv * support float points operation when all operands are concrete * support float point symbolic operations
1 parent 0e2f5ef commit 8b2eff1

File tree

13 files changed

+760
-179
lines changed

13 files changed

+760
-179
lines changed

‎benchmarks/wasm/fp_ops copy.wat‎

Lines changed: 209 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,209 @@
1+
(module
2+
(type (;0;) (func (param i32)))
3+
(type (;1;) (func))
4+
(type (;2;) (func (param f32)))
5+
(type (;3;) (func (param f64)))
6+
(import "console" "assert" (func (;0;) (type 0)))
7+
8+
(func (;1;) (type 1)
9+
(local f32 f32 f64 f64)
10+
11+
f32.const 3.5
12+
local.set 0
13+
f32.const 2.0
14+
local.set 1
15+
16+
f64.const 10.25
17+
local.set 2
18+
f64.const 0.5
19+
local.set 3
20+
21+
;; f32 arithmetic
22+
local.get 0
23+
local.get 1
24+
f32.add
25+
f32.const 5.5
26+
f32.eq
27+
call 0
28+
29+
local.get 0
30+
local.get 1
31+
f32.sub
32+
f32.const 1.5
33+
f32.eq
34+
call 0
35+
36+
local.get 0
37+
local.get 1
38+
f32.mul
39+
f32.const 7.0
40+
f32.eq
41+
call 0
42+
43+
local.get 0
44+
local.get 1
45+
f32.div
46+
f32.const 1.75
47+
f32.eq
48+
call 0
49+
50+
;; f32 comparisons
51+
local.get 0
52+
local.get 1
53+
f32.eq
54+
i32.eqz
55+
call 0
56+
57+
local.get 0
58+
local.get 1
59+
f32.ne
60+
call 0
61+
62+
local.get 0
63+
local.get 1
64+
f32.gt
65+
call 0
66+
67+
local.get 0
68+
local.get 1
69+
f32.ge
70+
call 0
71+
72+
local.get 0
73+
local.get 1
74+
f32.lt
75+
i32.eqz
76+
call 0
77+
78+
local.get 0
79+
local.get 1
80+
f32.le
81+
i32.eqz
82+
call 0
83+
84+
;; f64 arithmetic
85+
local.get 2
86+
local.get 3
87+
f64.add
88+
f64.const 10.75
89+
f64.eq
90+
call 0
91+
92+
local.get 2
93+
local.get 3
94+
f64.sub
95+
f64.const 9.75
96+
f64.eq
97+
call 0
98+
99+
local.get 2
100+
local.get 3
101+
f64.mul
102+
f64.const 5.125
103+
f64.eq
104+
call 0
105+
106+
local.get 2
107+
local.get 3
108+
f64.div
109+
f64.const 20.5
110+
f64.eq
111+
call 0
112+
113+
;; f64 comparisons
114+
local.get 2
115+
local.get 3
116+
f64.eq
117+
i32.eqz
118+
call 0
119+
120+
local.get 2
121+
local.get 3
122+
f64.ne
123+
call 0
124+
125+
local.get 2
126+
local.get 3
127+
f64.gt
128+
call 0
129+
130+
local.get 2
131+
local.get 3
132+
f64.ge
133+
call 0
134+
135+
local.get 2
136+
local.get 3
137+
f64.lt
138+
i32.eqz
139+
call 0
140+
141+
local.get 2
142+
local.get 3
143+
f64.le
144+
i32.eqz
145+
call 0
146+
)
147+
148+
;; symbolic branch guard for f32
149+
;; pseudo:
150+
;; if (x > 1.0) {
151+
;; if (x < 2.0) {
152+
;; assert(false); // forbidden range: (1.0, 2.0)
153+
;; }
154+
;; }
155+
(func (;2;) (type 2)
156+
local.get 0
157+
f32.const 1.0
158+
f32.gt
159+
if
160+
local.get 0
161+
f32.const 2.0
162+
f32.lt
163+
if
164+
i32.const 0
165+
call 0
166+
end
167+
end
168+
)
169+
170+
;; symbolic branch guard for f64
171+
;; if (y > 10.0) {
172+
;; if (y < 11.0) {
173+
;; assert(false); // forbidden range: (10.0, 11.0)
174+
;; }
175+
;; }
176+
(func (;3;) (type 3)
177+
local.get 0
178+
f64.const 10.0
179+
f64.gt
180+
if
181+
local.get 0
182+
f64.const 11.0
183+
f64.lt
184+
if
185+
i32.const 0
186+
call 0
187+
end
188+
end
189+
)
190+
191+
;; symbolic float entry
192+
;; pseudo:
193+
;; x := symbolic_f32()
194+
;; check_f32_guard(x)
195+
;; y := symbolic_f64()
196+
;; check_f64_guard(y)
197+
(func (;4;) (type 1)
198+
i32.const 0
199+
f32.symbolic
200+
call 2
201+
202+
;; i32.const 1
203+
;; f64.symbolic
204+
;; call 3
205+
)
206+
207+
(export "test_fp" (func 1))
208+
(export "real_main" (func 4))
209+
)

‎benchmarks/wasm/fp_ops.wat‎

Lines changed: 175 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
(module
2+
(type (;0;) (func (param i32)))
3+
(type (;1;) (func))
4+
(type (;2;) (func (param f32)))
5+
(type (;3;) (func (param f64)))
6+
(import "console" "assert" (func (;0;) (type 0)))
7+
(func (;1;) (type 1)
8+
(local f32 f32 f64 f64)
9+
f32.const 0x1.cp+1 (;=3.5;)
10+
local.set 0
11+
f32.const 0x1p+1 (;=2;)
12+
local.set 1
13+
f64.const 0x1.48p+3 (;=10.25;)
14+
local.set 2
15+
f64.const 0x1p-1 (;=0.5;)
16+
local.set 3
17+
local.get 0
18+
local.get 1
19+
f32.add
20+
f32.const 0x1.6p+2 (;=5.5;)
21+
f32.eq
22+
call 0
23+
local.get 0
24+
local.get 1
25+
f32.sub
26+
f32.const 0x1.8p+0 (;=1.5;)
27+
f32.eq
28+
call 0
29+
local.get 0
30+
local.get 1
31+
f32.mul
32+
f32.const 0x1.cp+2 (;=7;)
33+
f32.eq
34+
call 0
35+
local.get 0
36+
local.get 1
37+
f32.div
38+
f32.const 0x1.cp+0 (;=1.75;)
39+
f32.eq
40+
call 0
41+
local.get 0
42+
local.get 1
43+
f32.eq
44+
i32.eqz
45+
call 0
46+
local.get 0
47+
local.get 1
48+
f32.ne
49+
call 0
50+
local.get 0
51+
local.get 1
52+
f32.gt
53+
call 0
54+
local.get 0
55+
local.get 1
56+
f32.ge
57+
call 0
58+
local.get 0
59+
local.get 1
60+
f32.lt
61+
i32.eqz
62+
call 0
63+
local.get 0
64+
local.get 1
65+
f32.le
66+
i32.eqz
67+
call 0
68+
local.get 2
69+
local.get 3
70+
f64.add
71+
f64.const 0x1.58p+3 (;=10.75;)
72+
f64.eq
73+
call 0
74+
local.get 2
75+
local.get 3
76+
f64.sub
77+
f64.const 0x1.38p+3 (;=9.75;)
78+
f64.eq
79+
call 0
80+
local.get 2
81+
local.get 3
82+
f64.mul
83+
f64.const 0x1.48p+2 (;=5.125;)
84+
f64.eq
85+
call 0
86+
local.get 2
87+
local.get 3
88+
f64.div
89+
f64.const 0x1.48p+4 (;=20.5;)
90+
f64.eq
91+
call 0
92+
local.get 2
93+
local.get 3
94+
f64.eq
95+
i32.eqz
96+
call 0
97+
local.get 2
98+
local.get 3
99+
f64.ne
100+
call 0
101+
local.get 2
102+
local.get 3
103+
f64.gt
104+
call 0
105+
local.get 2
106+
local.get 3
107+
f64.ge
108+
call 0
109+
local.get 2
110+
local.get 3
111+
f64.lt
112+
i32.eqz
113+
call 0
114+
local.get 2
115+
local.get 3
116+
f64.le
117+
i32.eqz
118+
call 0)
119+
120+
;; symbolic branch guard for f32
121+
;; pseudo:
122+
;; if (x > 1.0) {
123+
;; if (x < 2.0) {
124+
;; assert(false); // forbidden range: (1.0, 2.0)
125+
;; }
126+
;; }
127+
(func (;2;) (type 2) (param f32)
128+
local.get 0
129+
f32.const 0x1p+0 (;=1;)
130+
f32.gt
131+
if ;; label = @1
132+
local.get 0
133+
f32.const 0x1p+1 (;=2;)
134+
f32.lt
135+
if ;; label = @2
136+
i32.const 0
137+
call 0
138+
end
139+
end)
140+
141+
;; if (y > 10.0) {
142+
;; if (y < 11.0) {
143+
;; assert(false); // forbidden range: (10.0, 11.0)
144+
;; }
145+
;; }
146+
(func (;3;) (type 3) (param f64)
147+
local.get 0
148+
f64.const 0x1.4p+3 (;=10;)
149+
f64.gt
150+
if ;; label = @1
151+
local.get 0
152+
f64.const 0x1.6p+3 (;=11;)
153+
f64.lt
154+
if ;; label = @2
155+
i32.const 0
156+
call 0
157+
end
158+
end)
159+
160+
;; x := symbolic_f32()
161+
;; check_f32_guard(x)
162+
;; y := symbolic_f64()
163+
;; check_f64_guard(y)
164+
(func (;4;) (type 1)
165+
i32.const 0
166+
f32.symbolic
167+
call 2
168+
169+
;; i32.const 1
170+
;; f64.symbolic
171+
;; call 3
172+
)
173+
174+
(export "test_fp" (func 1))
175+
(export "real_main" (func 4)))

0 commit comments

Comments
 (0)