source: src/Clight/test/duff.c.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 6 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 22.4 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [][〈ident_of_nat 0 (* copy *), CL_Internal (
6       mk_function Tvoid [〈ident_of_nat 19, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer (Tint I16 Signed  ))〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
9           (Expr (Ebinop Odiv
10             (Expr (Ebinop Oadd
11               (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
12               (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
13               (Tint I32 Signed  ))
14             (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
15             (Tint I32 Signed  )))
16         (Sswitch (Expr (Ebinop Omod
17                    (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
18                    (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
19                    (Tint I32 Signed  )) (
20           (LScase I32 (repr ? 0)
21             (Slabel (ident_of_nat 22)
22             (Ssequence
23             (Ssequence
24             (Sassign (Expr (Evar (ident_of_nat 17))
25                        (Tpointer (Tint I16 Signed  )))
26               (Expr (Evar (ident_of_nat 19)) (Tpointer (Tint I16 Signed  ))))
27             (Sassign (Expr (Evar (ident_of_nat 19))
28                        (Tpointer (Tint I16 Signed  )))
29               (Expr (Ebinop Oadd
30                 (Expr (Evar (ident_of_nat 17))
31                   (Tpointer (Tint I16 Signed  )))
32                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
33                 (Tpointer (Tint I16 Signed  )))))
34             (Ssequence
35             (Ssequence
36             (Sassign (Expr (Evar (ident_of_nat 18))
37                        (Tpointer (Tint I16 Signed  )))
38               (Expr (Evar (ident_of_nat 20)) (Tpointer (Tint I16 Signed  ))))
39             (Sassign (Expr (Evar (ident_of_nat 20))
40                        (Tpointer (Tint I16 Signed  )))
41               (Expr (Ebinop Oadd
42                 (Expr (Evar (ident_of_nat 18))
43                   (Tpointer (Tint I16 Signed  )))
44                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
45                 (Tpointer (Tint I16 Signed  )))))
46             (Sassign (Expr (Ederef
47                        (Expr (Evar (ident_of_nat 17))
48                          (Tpointer (Tint I16 Signed  ))))
49                        (Tint I16 Signed  ))
50               (Expr (Ederef
51                 (Expr (Evar (ident_of_nat 18))
52                   (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
53             (LScase I32 (repr ? 7)
54               (Ssequence
55               (Sassign (Expr (Evar (ident_of_nat 15))
56                          (Tpointer (Tint I16 Signed  )))
57                 (Expr (Evar (ident_of_nat 19))
58                   (Tpointer (Tint I16 Signed  ))))
59               (Ssequence
60               (Sassign (Expr (Evar (ident_of_nat 19))
61                          (Tpointer (Tint I16 Signed  )))
62                 (Expr (Ebinop Oadd
63                   (Expr (Evar (ident_of_nat 15))
64                     (Tpointer (Tint I16 Signed  )))
65                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
66                   (Tpointer (Tint I16 Signed  ))))
67               (Ssequence
68               (Sassign (Expr (Evar (ident_of_nat 16))
69                          (Tpointer (Tint I16 Signed  )))
70                 (Expr (Evar (ident_of_nat 20))
71                   (Tpointer (Tint I16 Signed  ))))
72               (Ssequence
73               (Sassign (Expr (Evar (ident_of_nat 20))
74                          (Tpointer (Tint I16 Signed  )))
75                 (Expr (Ebinop Oadd
76                   (Expr (Evar (ident_of_nat 16))
77                     (Tpointer (Tint I16 Signed  )))
78                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
79                   (Tpointer (Tint I16 Signed  ))))
80               (Sassign (Expr (Ederef
81                          (Expr (Evar (ident_of_nat 15))
82                            (Tpointer (Tint I16 Signed  ))))
83                          (Tint I16 Signed  ))
84                 (Expr (Ederef
85                   (Expr (Evar (ident_of_nat 16))
86                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
87               (LScase I32 (repr ? 6)
88                 (Ssequence
89                 (Sassign (Expr (Evar (ident_of_nat 13))
90                            (Tpointer (Tint I16 Signed  )))
91                   (Expr (Evar (ident_of_nat 19))
92                     (Tpointer (Tint I16 Signed  ))))
93                 (Ssequence
94                 (Sassign (Expr (Evar (ident_of_nat 19))
95                            (Tpointer (Tint I16 Signed  )))
96                   (Expr (Ebinop Oadd
97                     (Expr (Evar (ident_of_nat 13))
98                       (Tpointer (Tint I16 Signed  )))
99                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
100                     (Tpointer (Tint I16 Signed  ))))
101                 (Ssequence
102                 (Sassign (Expr (Evar (ident_of_nat 14))
103                            (Tpointer (Tint I16 Signed  )))
104                   (Expr (Evar (ident_of_nat 20))
105                     (Tpointer (Tint I16 Signed  ))))
106                 (Ssequence
107                 (Sassign (Expr (Evar (ident_of_nat 20))
108                            (Tpointer (Tint I16 Signed  )))
109                   (Expr (Ebinop Oadd
110                     (Expr (Evar (ident_of_nat 14))
111                       (Tpointer (Tint I16 Signed  )))
112                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
113                     (Tpointer (Tint I16 Signed  ))))
114                 (Sassign (Expr (Ederef
115                            (Expr (Evar (ident_of_nat 13))
116                              (Tpointer (Tint I16 Signed  ))))
117                            (Tint I16 Signed  ))
118                   (Expr (Ederef
119                     (Expr (Evar (ident_of_nat 14))
120                       (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
121                 (LScase I32 (repr ? 5)
122                   (Ssequence
123                   (Sassign (Expr (Evar (ident_of_nat 11))
124                              (Tpointer (Tint I16 Signed  )))
125                     (Expr (Evar (ident_of_nat 19))
126                       (Tpointer (Tint I16 Signed  ))))
127                   (Ssequence
128                   (Sassign (Expr (Evar (ident_of_nat 19))
129                              (Tpointer (Tint I16 Signed  )))
130                     (Expr (Ebinop Oadd
131                       (Expr (Evar (ident_of_nat 11))
132                         (Tpointer (Tint I16 Signed  )))
133                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
134                       (Tpointer (Tint I16 Signed  ))))
135                   (Ssequence
136                   (Sassign (Expr (Evar (ident_of_nat 12))
137                              (Tpointer (Tint I16 Signed  )))
138                     (Expr (Evar (ident_of_nat 20))
139                       (Tpointer (Tint I16 Signed  ))))
140                   (Ssequence
141                   (Sassign (Expr (Evar (ident_of_nat 20))
142                              (Tpointer (Tint I16 Signed  )))
143                     (Expr (Ebinop Oadd
144                       (Expr (Evar (ident_of_nat 12))
145                         (Tpointer (Tint I16 Signed  )))
146                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
147                       (Tpointer (Tint I16 Signed  ))))
148                   (Sassign (Expr (Ederef
149                              (Expr (Evar (ident_of_nat 11))
150                                (Tpointer (Tint I16 Signed  ))))
151                              (Tint I16 Signed  ))
152                     (Expr (Ederef
153                       (Expr (Evar (ident_of_nat 12))
154                         (Tpointer (Tint I16 Signed  ))))
155                       (Tint I16 Signed  )))))))
156                   (LScase I32 (repr ? 4)
157                     (Ssequence
158                     (Sassign (Expr (Evar (ident_of_nat 9))
159                                (Tpointer (Tint I16 Signed  )))
160                       (Expr (Evar (ident_of_nat 19))
161                         (Tpointer (Tint I16 Signed  ))))
162                     (Ssequence
163                     (Sassign (Expr (Evar (ident_of_nat 19))
164                                (Tpointer (Tint I16 Signed  )))
165                       (Expr (Ebinop Oadd
166                         (Expr (Evar (ident_of_nat 9))
167                           (Tpointer (Tint I16 Signed  )))
168                         (Expr (Econst_int I32 (repr ? 1))
169                           (Tint I32 Signed  )))
170                         (Tpointer (Tint I16 Signed  ))))
171                     (Ssequence
172                     (Sassign (Expr (Evar (ident_of_nat 10))
173                                (Tpointer (Tint I16 Signed  )))
174                       (Expr (Evar (ident_of_nat 20))
175                         (Tpointer (Tint I16 Signed  ))))
176                     (Ssequence
177                     (Sassign (Expr (Evar (ident_of_nat 20))
178                                (Tpointer (Tint I16 Signed  )))
179                       (Expr (Ebinop Oadd
180                         (Expr (Evar (ident_of_nat 10))
181                           (Tpointer (Tint I16 Signed  )))
182                         (Expr (Econst_int I32 (repr ? 1))
183                           (Tint I32 Signed  )))
184                         (Tpointer (Tint I16 Signed  ))))
185                     (Sassign (Expr (Ederef
186                                (Expr (Evar (ident_of_nat 9))
187                                  (Tpointer (Tint I16 Signed  ))))
188                                (Tint I16 Signed  ))
189                       (Expr (Ederef
190                         (Expr (Evar (ident_of_nat 10))
191                           (Tpointer (Tint I16 Signed  ))))
192                         (Tint I16 Signed  )))))))
193                     (LScase I32 (repr ? 3)
194                       (Ssequence
195                       (Sassign (Expr (Evar (ident_of_nat 7))
196                                  (Tpointer (Tint I16 Signed  )))
197                         (Expr (Evar (ident_of_nat 19))
198                           (Tpointer (Tint I16 Signed  ))))
199                       (Ssequence
200                       (Sassign (Expr (Evar (ident_of_nat 19))
201                                  (Tpointer (Tint I16 Signed  )))
202                         (Expr (Ebinop Oadd
203                           (Expr (Evar (ident_of_nat 7))
204                             (Tpointer (Tint I16 Signed  )))
205                           (Expr (Econst_int I32 (repr ? 1))
206                             (Tint I32 Signed  )))
207                           (Tpointer (Tint I16 Signed  ))))
208                       (Ssequence
209                       (Sassign (Expr (Evar (ident_of_nat 8))
210                                  (Tpointer (Tint I16 Signed  )))
211                         (Expr (Evar (ident_of_nat 20))
212                           (Tpointer (Tint I16 Signed  ))))
213                       (Ssequence
214                       (Sassign (Expr (Evar (ident_of_nat 20))
215                                  (Tpointer (Tint I16 Signed  )))
216                         (Expr (Ebinop Oadd
217                           (Expr (Evar (ident_of_nat 8))
218                             (Tpointer (Tint I16 Signed  )))
219                           (Expr (Econst_int I32 (repr ? 1))
220                             (Tint I32 Signed  )))
221                           (Tpointer (Tint I16 Signed  ))))
222                       (Sassign (Expr (Ederef
223                                  (Expr (Evar (ident_of_nat 7))
224                                    (Tpointer (Tint I16 Signed  ))))
225                                  (Tint I16 Signed  ))
226                         (Expr (Ederef
227                           (Expr (Evar (ident_of_nat 8))
228                             (Tpointer (Tint I16 Signed  ))))
229                           (Tint I16 Signed  )))))))
230                       (LScase I32 (repr ? 2)
231                         (Ssequence
232                         (Sassign (Expr (Evar (ident_of_nat 5))
233                                    (Tpointer (Tint I16 Signed  )))
234                           (Expr (Evar (ident_of_nat 19))
235                             (Tpointer (Tint I16 Signed  ))))
236                         (Ssequence
237                         (Sassign (Expr (Evar (ident_of_nat 19))
238                                    (Tpointer (Tint I16 Signed  )))
239                           (Expr (Ebinop Oadd
240                             (Expr (Evar (ident_of_nat 5))
241                               (Tpointer (Tint I16 Signed  )))
242                             (Expr (Econst_int I32 (repr ? 1))
243                               (Tint I32 Signed  )))
244                             (Tpointer (Tint I16 Signed  ))))
245                         (Ssequence
246                         (Sassign (Expr (Evar (ident_of_nat 6))
247                                    (Tpointer (Tint I16 Signed  )))
248                           (Expr (Evar (ident_of_nat 20))
249                             (Tpointer (Tint I16 Signed  ))))
250                         (Ssequence
251                         (Sassign (Expr (Evar (ident_of_nat 20))
252                                    (Tpointer (Tint I16 Signed  )))
253                           (Expr (Ebinop Oadd
254                             (Expr (Evar (ident_of_nat 6))
255                               (Tpointer (Tint I16 Signed  )))
256                             (Expr (Econst_int I32 (repr ? 1))
257                               (Tint I32 Signed  )))
258                             (Tpointer (Tint I16 Signed  ))))
259                         (Sassign (Expr (Ederef
260                                    (Expr (Evar (ident_of_nat 5))
261                                      (Tpointer (Tint I16 Signed  ))))
262                                    (Tint I16 Signed  ))
263                           (Expr (Ederef
264                             (Expr (Evar (ident_of_nat 6))
265                               (Tpointer (Tint I16 Signed  ))))
266                             (Tint I16 Signed  )))))))
267                         (LScase I32 (repr ? 1)
268                           (Ssequence
269                           (Sassign (Expr (Evar (ident_of_nat 3))
270                                      (Tpointer (Tint I16 Signed  )))
271                             (Expr (Evar (ident_of_nat 19))
272                               (Tpointer (Tint I16 Signed  ))))
273                           (Ssequence
274                           (Sassign (Expr (Evar (ident_of_nat 19))
275                                      (Tpointer (Tint I16 Signed  )))
276                             (Expr (Ebinop Oadd
277                               (Expr (Evar (ident_of_nat 3))
278                                 (Tpointer (Tint I16 Signed  )))
279                               (Expr (Econst_int I32 (repr ? 1))
280                                 (Tint I32 Signed  )))
281                               (Tpointer (Tint I16 Signed  ))))
282                           (Ssequence
283                           (Sassign (Expr (Evar (ident_of_nat 4))
284                                      (Tpointer (Tint I16 Signed  )))
285                             (Expr (Evar (ident_of_nat 20))
286                               (Tpointer (Tint I16 Signed  ))))
287                           (Ssequence
288                           (Sassign (Expr (Evar (ident_of_nat 20))
289                                      (Tpointer (Tint I16 Signed  )))
290                             (Expr (Ebinop Oadd
291                               (Expr (Evar (ident_of_nat 4))
292                                 (Tpointer (Tint I16 Signed  )))
293                               (Expr (Econst_int I32 (repr ? 1))
294                                 (Tint I32 Signed  )))
295                               (Tpointer (Tint I16 Signed  ))))
296                           (Ssequence
297                           (Sassign (Expr (Ederef
298                                      (Expr (Evar (ident_of_nat 3))
299                                        (Tpointer (Tint I16 Signed  ))))
300                                      (Tint I16 Signed  ))
301                             (Expr (Ederef
302                               (Expr (Evar (ident_of_nat 4))
303                                 (Tpointer (Tint I16 Signed  ))))
304                               (Tint I16 Signed  )))
305                           (Ssequence
306                           (Sassign (Expr (Evar (ident_of_nat 2))
307                                      (Tint I32 Signed  ))
308                             (Expr (Ebinop Osub
309                               (Expr (Evar (ident_of_nat 1))
310                                 (Tint I32 Signed  ))
311                               (Expr (Econst_int I32 (repr ? 1))
312                                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
313                           (Ssequence
314                           (Sassign (Expr (Evar (ident_of_nat 1))
315                                      (Tint I32 Signed  ))
316                             (Expr (Evar (ident_of_nat 2))
317                               (Tint I32 Signed  )))
318                           (Sifthenelse (Expr (Ebinop Ogt
319                                          (Expr (Evar (ident_of_nat 2))
320                                            (Tint I32 Signed  ))
321                                          (Expr (Econst_int I32 (repr ? 0))
322                                            (Tint I32 Signed  )))
323                                          (Tint I32 Signed  ))
324                             (Sgoto (ident_of_nat 22))
325                             Sskip))))))))
326                           (LSdefault
327                             Sskip)))))))))
328         )))
329       
330       
331       
332     )〉;
333    〈ident_of_nat 23 (* main *), CL_Internal (
334      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray (Tint I16 Signed  ) 3)〉 ]
335        (Ssequence
336        (Sassign (Expr (Ederef
337                   (Expr (Ebinop Oadd
338                     (Expr (Evar (ident_of_nat 24))
339                       (Tarray (Tint I16 Signed  ) 3))
340                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
341                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
342          (Expr (Ecast (Tint I16 Signed  )
343            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
344            (Tint I16 Signed  )))
345        (Ssequence
346        (Sassign (Expr (Ederef
347                   (Expr (Ebinop Oadd
348                     (Expr (Evar (ident_of_nat 24))
349                       (Tarray (Tint I16 Signed  ) 3))
350                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
351                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
352          (Expr (Ecast (Tint I16 Signed  )
353            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
354            (Tint I16 Signed  )))
355        (Ssequence
356        (Sassign (Expr (Ederef
357                   (Expr (Ebinop Oadd
358                     (Expr (Evar (ident_of_nat 24))
359                       (Tarray (Tint I16 Signed  ) 3))
360                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
361                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
362          (Expr (Ecast (Tint I16 Signed  )
363            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
364            (Tint I16 Signed  )))
365        (Ssequence
366        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
367                             (Tfunction (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
368          [(Expr (Evar (ident_of_nat 25)) (Tarray (Tint I16 Signed  ) 3));
369          (Expr (Evar (ident_of_nat 24)) (Tarray (Tint I16 Signed  ) 3));
370          (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
371        (Sreturn (Some expr (Expr (Ebinop Oadd
372                              (Expr (Ebinop Oadd
373                                (Expr (Ecast (Tint I32 Signed  )
374                                  (Expr (Ederef
375                                    (Expr (Ebinop Oadd
376                                      (Expr (Evar (ident_of_nat 25))
377                                        (Tarray (Tint I16 Signed  ) 3))
378                                      (Expr (Econst_int I32 (repr ? 0))
379                                        (Tint I32 Signed  )))
380                                      (Tpointer (Tint I16 Signed  ))))
381                                    (Tint I16 Signed  )))
382                                  (Tint I32 Signed  ))
383                                (Expr (Ecast (Tint I32 Signed  )
384                                  (Expr (Ederef
385                                    (Expr (Ebinop Oadd
386                                      (Expr (Evar (ident_of_nat 25))
387                                        (Tarray (Tint I16 Signed  ) 3))
388                                      (Expr (Econst_int I32 (repr ? 1))
389                                        (Tint I32 Signed  )))
390                                      (Tpointer (Tint I16 Signed  ))))
391                                    (Tint I16 Signed  )))
392                                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
393                              (Expr (Ecast (Tint I32 Signed  )
394                                (Expr (Ederef
395                                  (Expr (Ebinop Oadd
396                                    (Expr (Evar (ident_of_nat 25))
397                                      (Tarray (Tint I16 Signed  ) 3))
398                                    (Expr (Econst_int I32 (repr ? 2))
399                                      (Tint I32 Signed  )))
400                                    (Tpointer (Tint I16 Signed  ))))
401                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
402                              (Tint I32 Signed  ))))))))
403     
404     
405     
406    )〉]
407  (ident_of_nat 23)
408 
409.
410
411(*
412example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
413normalize  (* you can examine the result here *)
414*)
Note: See TracBrowser for help on using the repository browser.