source: src/RTLabs/test/search.RTLabs.ma @ 1157

Last change on this file since 1157 was 1157, checked in by campbell, 8 years ago

Update pretty printers and examples.

File size: 24.1 KB
Line 
1include "RTLabs/import.ma".
2include "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
423definition 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
429OK ? (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.
Note: See TracBrowser for help on using the repository browser.