1 | include "RTLabs/import.ma". |
---|
2 | include "common/Animation.ma". |
---|
3 | |
---|
4 | |
---|
5 | |
---|
6 | |
---|
7 | definition id__div32u := ident_of_nat 0. |
---|
8 | definition lbl__div32u9 := 15. |
---|
9 | definition lbl__div32u8 := 14. |
---|
10 | definition lbl__div32u7 := 13. |
---|
11 | definition lbl__div32u6 := 12. |
---|
12 | definition lbl__div32u5 := 11. |
---|
13 | definition lbl__div32u4 := 10. |
---|
14 | definition lbl__div32u3 := 9. |
---|
15 | definition lbl__div32u2 := 8. |
---|
16 | definition lbl__div32u15 := 7. |
---|
17 | definition lbl__div32u14 := 6. |
---|
18 | definition lbl__div32u13 := 5. |
---|
19 | definition lbl__div32u12 := 4. |
---|
20 | definition lbl__div32u11 := 3. |
---|
21 | definition lbl__div32u10 := 2. |
---|
22 | definition lbl__div32u1 := 1. |
---|
23 | definition lbl__div32u0 := 0. |
---|
24 | definition C_cost0 := costlabel_of_nat 2. |
---|
25 | definition C_cost1 := costlabel_of_nat 1. |
---|
26 | definition C_cost2 := costlabel_of_nat 0. |
---|
27 | |
---|
28 | |
---|
29 | definition pre__div32u := mk_pre_internal_function |
---|
30 | (Some ? (pair ?? 4 (ASTint I32 Unsigned))) |
---|
31 | [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))] |
---|
32 | [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))] |
---|
33 | 0 |
---|
34 | [ |
---|
35 | (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8)); |
---|
36 | (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7)); |
---|
37 | (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6)); |
---|
38 | (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5)); |
---|
39 | (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4)); |
---|
40 | (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3)); |
---|
41 | (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11)); |
---|
42 | (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1)); |
---|
43 | (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14)); |
---|
44 | (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13)); |
---|
45 | (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12)); |
---|
46 | (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3)); |
---|
47 | (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10)); |
---|
48 | (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9)); |
---|
49 | (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0)); |
---|
50 | (pair ?? lbl__div32u0 (make_St_return)) |
---|
51 | ] |
---|
52 | |
---|
53 | lbl__div32u15 |
---|
54 | lbl__div32u0. |
---|
55 | |
---|
56 | definition id__div32s := ident_of_nat 1. |
---|
57 | definition lbl__div32s9 := 25. |
---|
58 | definition lbl__div32s8 := 24. |
---|
59 | definition lbl__div32s7 := 23. |
---|
60 | definition lbl__div32s6 := 22. |
---|
61 | definition lbl__div32s5 := 21. |
---|
62 | definition lbl__div32s4 := 20. |
---|
63 | definition lbl__div32s3 := 19. |
---|
64 | definition lbl__div32s25 := 18. |
---|
65 | definition lbl__div32s24 := 17. |
---|
66 | definition lbl__div32s23 := 16. |
---|
67 | definition lbl__div32s22 := 15. |
---|
68 | definition lbl__div32s21 := 14. |
---|
69 | definition lbl__div32s20 := 13. |
---|
70 | definition lbl__div32s2 := 12. |
---|
71 | definition lbl__div32s19 := 11. |
---|
72 | definition lbl__div32s18 := 10. |
---|
73 | definition lbl__div32s17 := 9. |
---|
74 | definition lbl__div32s16 := 8. |
---|
75 | definition lbl__div32s15 := 7. |
---|
76 | definition lbl__div32s14 := 6. |
---|
77 | definition lbl__div32s13 := 5. |
---|
78 | definition lbl__div32s12 := 4. |
---|
79 | definition lbl__div32s11 := 3. |
---|
80 | definition lbl__div32s10 := 2. |
---|
81 | definition lbl__div32s1 := 1. |
---|
82 | definition lbl__div32s0 := 0. |
---|
83 | definition C_cost3 := costlabel_of_nat 4. |
---|
84 | definition C_cost4 := costlabel_of_nat 3. |
---|
85 | definition C_cost7 := costlabel_of_nat 2. |
---|
86 | definition C_cost5 := costlabel_of_nat 1. |
---|
87 | definition C_cost6 := costlabel_of_nat 0. |
---|
88 | |
---|
89 | |
---|
90 | definition pre__div32s := mk_pre_internal_function |
---|
91 | (Some ? (pair ?? 7 (ASTint I32 Signed))) |
---|
92 | [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))] |
---|
93 | [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))] |
---|
94 | 0 |
---|
95 | [ |
---|
96 | (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8)); |
---|
97 | (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7)); |
---|
98 | (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6)); |
---|
99 | (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4)); |
---|
100 | (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4)); |
---|
101 | (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3)); |
---|
102 | (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2)); |
---|
103 | (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24)); |
---|
104 | (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23)); |
---|
105 | (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22)); |
---|
106 | (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21)); |
---|
107 | (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20)); |
---|
108 | (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19)); |
---|
109 | (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1)); |
---|
110 | (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18)); |
---|
111 | (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13)); |
---|
112 | (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16)); |
---|
113 | (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15)); |
---|
114 | (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14)); |
---|
115 | (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12)); |
---|
116 | (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12)); |
---|
117 | (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11)); |
---|
118 | (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10)); |
---|
119 | (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5)); |
---|
120 | (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0)); |
---|
121 | (pair ?? lbl__div32s0 (make_St_return)) |
---|
122 | ] |
---|
123 | |
---|
124 | lbl__div32s25 |
---|
125 | lbl__div32s0. |
---|
126 | |
---|
127 | definition id_search := ident_of_nat 2. |
---|
128 | definition lbl_search9 := 65. |
---|
129 | definition lbl_search8 := 64. |
---|
130 | definition lbl_search7 := 63. |
---|
131 | definition lbl_search65 := 62. |
---|
132 | definition lbl_search64 := 61. |
---|
133 | definition lbl_search63 := 60. |
---|
134 | definition lbl_search62 := 59. |
---|
135 | definition lbl_search61 := 58. |
---|
136 | definition lbl_search60 := 57. |
---|
137 | definition lbl_search6 := 56. |
---|
138 | definition lbl_search59 := 55. |
---|
139 | definition lbl_search58 := 54. |
---|
140 | definition lbl_search57 := 53. |
---|
141 | definition lbl_search56 := 52. |
---|
142 | definition lbl_search55 := 51. |
---|
143 | definition lbl_search54 := 50. |
---|
144 | definition lbl_search53 := 49. |
---|
145 | definition lbl_search52 := 48. |
---|
146 | definition lbl_search51 := 47. |
---|
147 | definition lbl_search50 := 46. |
---|
148 | definition lbl_search5 := 45. |
---|
149 | definition lbl_search49 := 44. |
---|
150 | definition lbl_search48 := 43. |
---|
151 | definition lbl_search47 := 42. |
---|
152 | definition lbl_search46 := 41. |
---|
153 | definition lbl_search45 := 40. |
---|
154 | definition lbl_search44 := 39. |
---|
155 | definition lbl_search43 := 38. |
---|
156 | definition lbl_search42 := 37. |
---|
157 | definition lbl_search41 := 36. |
---|
158 | definition lbl_search40 := 35. |
---|
159 | definition lbl_search4 := 34. |
---|
160 | definition lbl_search39 := 33. |
---|
161 | definition lbl_search38 := 32. |
---|
162 | definition lbl_search37 := 31. |
---|
163 | definition lbl_search36 := 30. |
---|
164 | definition lbl_search35 := 29. |
---|
165 | definition lbl_search34 := 28. |
---|
166 | definition lbl_search33 := 27. |
---|
167 | definition lbl_search32 := 26. |
---|
168 | definition lbl_search31 := 25. |
---|
169 | definition lbl_search30 := 24. |
---|
170 | definition lbl_search3 := 23. |
---|
171 | definition lbl_search29 := 22. |
---|
172 | definition lbl_search28 := 21. |
---|
173 | definition lbl_search27 := 20. |
---|
174 | definition lbl_search26 := 19. |
---|
175 | definition lbl_search25 := 18. |
---|
176 | definition lbl_search24 := 17. |
---|
177 | definition lbl_search23 := 16. |
---|
178 | definition lbl_search22 := 15. |
---|
179 | definition lbl_search21 := 14. |
---|
180 | definition lbl_search20 := 13. |
---|
181 | definition lbl_search2 := 12. |
---|
182 | definition lbl_search19 := 11. |
---|
183 | definition lbl_search18 := 10. |
---|
184 | definition lbl_search17 := 9. |
---|
185 | definition lbl_search16 := 8. |
---|
186 | definition lbl_search15 := 7. |
---|
187 | definition lbl_search14 := 6. |
---|
188 | definition lbl_search13 := 5. |
---|
189 | definition lbl_search12 := 4. |
---|
190 | definition lbl_search11 := 3. |
---|
191 | definition lbl_search10 := 2. |
---|
192 | definition lbl_search1 := 1. |
---|
193 | definition lbl_search0 := 0. |
---|
194 | definition C_cost16 := costlabel_of_nat 8. |
---|
195 | definition C_cost9 := costlabel_of_nat 7. |
---|
196 | definition C_cost14 := costlabel_of_nat 6. |
---|
197 | definition C_cost15 := costlabel_of_nat 5. |
---|
198 | definition C_cost12 := costlabel_of_nat 4. |
---|
199 | definition C_cost13 := costlabel_of_nat 3. |
---|
200 | definition C_cost10 := costlabel_of_nat 2. |
---|
201 | definition C_cost11 := costlabel_of_nat 1. |
---|
202 | definition C_cost8 := costlabel_of_nat 0. |
---|
203 | |
---|
204 | |
---|
205 | definition pre_search := mk_pre_internal_function |
---|
206 | (Some ? (pair ?? 8 (ASTint I8 Unsigned))) |
---|
207 | [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))] |
---|
208 | [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))] |
---|
209 | 0 |
---|
210 | [ |
---|
211 | (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8)); |
---|
212 | (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7)); |
---|
213 | (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5)); |
---|
214 | (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64)); |
---|
215 | (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63)); |
---|
216 | (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62)); |
---|
217 | (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61)); |
---|
218 | (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60)); |
---|
219 | (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59)); |
---|
220 | (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5)); |
---|
221 | (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5)); |
---|
222 | (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57)); |
---|
223 | (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56)); |
---|
224 | (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55)); |
---|
225 | (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54)); |
---|
226 | (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53)); |
---|
227 | (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52)); |
---|
228 | (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51)); |
---|
229 | (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50)); |
---|
230 | (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49)); |
---|
231 | (pair ?? lbl_search5 (make_St_skip lbl_search58)); |
---|
232 | (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48)); |
---|
233 | (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47)); |
---|
234 | (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46)); |
---|
235 | (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45)); |
---|
236 | (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44)); |
---|
237 | (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43)); |
---|
238 | (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42)); |
---|
239 | (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41)); |
---|
240 | (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40)); |
---|
241 | (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39)); |
---|
242 | (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3)); |
---|
243 | (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38)); |
---|
244 | (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37)); |
---|
245 | (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34)); |
---|
246 | (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35)); |
---|
247 | (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0)); |
---|
248 | (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33)); |
---|
249 | (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32)); |
---|
250 | (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31)); |
---|
251 | (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30)); |
---|
252 | (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29)); |
---|
253 | (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2)); |
---|
254 | (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28)); |
---|
255 | (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27)); |
---|
256 | (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26)); |
---|
257 | (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20)); |
---|
258 | (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24)); |
---|
259 | (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23)); |
---|
260 | (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22)); |
---|
261 | (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21)); |
---|
262 | (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19)); |
---|
263 | (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19)); |
---|
264 | (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1)); |
---|
265 | (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18)); |
---|
266 | (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17)); |
---|
267 | (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16)); |
---|
268 | (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15)); |
---|
269 | (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14)); |
---|
270 | (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13)); |
---|
271 | (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12)); |
---|
272 | (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6)); |
---|
273 | (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10)); |
---|
274 | (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9)); |
---|
275 | (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0)); |
---|
276 | (pair ?? lbl_search0 (make_St_return)) |
---|
277 | ] |
---|
278 | |
---|
279 | lbl_search65 |
---|
280 | lbl_search0. |
---|
281 | |
---|
282 | definition id_main := ident_of_nat 3. |
---|
283 | definition lbl_main9 := 61. |
---|
284 | definition lbl_main8 := 60. |
---|
285 | definition lbl_main7 := 59. |
---|
286 | definition lbl_main61 := 58. |
---|
287 | definition lbl_main60 := 57. |
---|
288 | definition lbl_main6 := 56. |
---|
289 | definition lbl_main59 := 55. |
---|
290 | definition lbl_main58 := 54. |
---|
291 | definition lbl_main57 := 53. |
---|
292 | definition lbl_main56 := 52. |
---|
293 | definition lbl_main55 := 51. |
---|
294 | definition lbl_main54 := 50. |
---|
295 | definition lbl_main53 := 49. |
---|
296 | definition lbl_main52 := 48. |
---|
297 | definition lbl_main51 := 47. |
---|
298 | definition lbl_main50 := 46. |
---|
299 | definition lbl_main5 := 45. |
---|
300 | definition lbl_main49 := 44. |
---|
301 | definition lbl_main48 := 43. |
---|
302 | definition lbl_main47 := 42. |
---|
303 | definition lbl_main46 := 41. |
---|
304 | definition lbl_main45 := 40. |
---|
305 | definition lbl_main44 := 39. |
---|
306 | definition lbl_main43 := 38. |
---|
307 | definition lbl_main42 := 37. |
---|
308 | definition lbl_main41 := 36. |
---|
309 | definition lbl_main40 := 35. |
---|
310 | definition lbl_main4 := 34. |
---|
311 | definition lbl_main39 := 33. |
---|
312 | definition lbl_main38 := 32. |
---|
313 | definition lbl_main37 := 31. |
---|
314 | definition lbl_main36 := 30. |
---|
315 | definition lbl_main35 := 29. |
---|
316 | definition lbl_main34 := 28. |
---|
317 | definition lbl_main33 := 27. |
---|
318 | definition lbl_main32 := 26. |
---|
319 | definition lbl_main31 := 25. |
---|
320 | definition lbl_main30 := 24. |
---|
321 | definition lbl_main3 := 23. |
---|
322 | definition lbl_main29 := 22. |
---|
323 | definition lbl_main28 := 21. |
---|
324 | definition lbl_main27 := 20. |
---|
325 | definition lbl_main26 := 19. |
---|
326 | definition lbl_main25 := 18. |
---|
327 | definition lbl_main24 := 17. |
---|
328 | definition lbl_main23 := 16. |
---|
329 | definition lbl_main22 := 15. |
---|
330 | definition lbl_main21 := 14. |
---|
331 | definition lbl_main20 := 13. |
---|
332 | definition lbl_main2 := 12. |
---|
333 | definition lbl_main19 := 11. |
---|
334 | definition lbl_main18 := 10. |
---|
335 | definition lbl_main17 := 9. |
---|
336 | definition lbl_main16 := 8. |
---|
337 | definition lbl_main15 := 7. |
---|
338 | definition lbl_main14 := 6. |
---|
339 | definition lbl_main13 := 5. |
---|
340 | definition lbl_main12 := 4. |
---|
341 | definition lbl_main11 := 3. |
---|
342 | definition lbl_main10 := 2. |
---|
343 | definition lbl_main1 := 1. |
---|
344 | definition lbl_main0 := 0. |
---|
345 | definition C_cost17 := costlabel_of_nat 0. |
---|
346 | |
---|
347 | |
---|
348 | definition pre_main := mk_pre_internal_function |
---|
349 | (Some ? (pair ?? 2 (ASTint I32 Signed))) |
---|
350 | [] |
---|
351 | [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))] |
---|
352 | 5 |
---|
353 | [ |
---|
354 | (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8)); |
---|
355 | (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7)); |
---|
356 | (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6)); |
---|
357 | (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60)); |
---|
358 | (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59)); |
---|
359 | (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5)); |
---|
360 | (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58)); |
---|
361 | (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57)); |
---|
362 | (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56)); |
---|
363 | (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55)); |
---|
364 | (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54)); |
---|
365 | (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53)); |
---|
366 | (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52)); |
---|
367 | (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51)); |
---|
368 | (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50)); |
---|
369 | (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49)); |
---|
370 | (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4)); |
---|
371 | (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48)); |
---|
372 | (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47)); |
---|
373 | (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46)); |
---|
374 | (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45)); |
---|
375 | (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44)); |
---|
376 | (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43)); |
---|
377 | (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42)); |
---|
378 | (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41)); |
---|
379 | (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40)); |
---|
380 | (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39)); |
---|
381 | (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3)); |
---|
382 | (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38)); |
---|
383 | (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37)); |
---|
384 | (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36)); |
---|
385 | (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35)); |
---|
386 | (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34)); |
---|
387 | (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33)); |
---|
388 | (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32)); |
---|
389 | (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31)); |
---|
390 | (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30)); |
---|
391 | (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29)); |
---|
392 | (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2)); |
---|
393 | (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28)); |
---|
394 | (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27)); |
---|
395 | (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26)); |
---|
396 | (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25)); |
---|
397 | (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24)); |
---|
398 | (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23)); |
---|
399 | (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22)); |
---|
400 | (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21)); |
---|
401 | (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20)); |
---|
402 | (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19)); |
---|
403 | (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1)); |
---|
404 | (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18)); |
---|
405 | (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17)); |
---|
406 | (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16)); |
---|
407 | (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15)); |
---|
408 | (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14)); |
---|
409 | (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13)); |
---|
410 | (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12)); |
---|
411 | (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11)); |
---|
412 | (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10)); |
---|
413 | (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9)); |
---|
414 | (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0)); |
---|
415 | (pair ?? lbl_main0 (make_St_return)) |
---|
416 | ] |
---|
417 | |
---|
418 | lbl_main61 |
---|
419 | lbl_main0. |
---|
420 | |
---|
421 | |
---|
422 | |
---|
423 | definition prog : res RTLabs_program := |
---|
424 | do f_main \larr make_internal_function pre_main; |
---|
425 | do f_search \larr make_internal_function pre_search; |
---|
426 | do f__div32s \larr make_internal_function pre__div32s; |
---|
427 | do f__div32u \larr make_internal_function pre__div32u; |
---|
428 | |
---|
429 | OK ? (mk_program ?? |
---|
430 | ( (pair ?? id_main f_main):: |
---|
431 | (pair ?? id_search f_search):: |
---|
432 | (pair ?? id__div32s f__div32s):: |
---|
433 | (pair ?? id__div32u f__div32u):: |
---|
434 | (nil ?)) |
---|
435 | id_main |
---|
436 | (*globals:*) |
---|
437 | [] |
---|
438 | ). |
---|
439 | |
---|
440 | example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r). |
---|
441 | normalize (* you can examine the result here *) |
---|
442 | @refl qed. |
---|