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

Last change on this file since 965 was 965, checked in by campbell, 9 years ago

Update some Clight examples.

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