source: src/Clight/test/duff.ma @ 779

Last change on this file since 779 was 731, checked in by campbell, 10 years ago

Common definition for animation semantics, and factor out IO definitions.

File size: 21.7 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 (repr 7)) (Tint I32 Signed  )))
13             (Tint I32 Signed  ))
14           (Expr (Econst_int (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 (repr 8)) (Tint I32 Signed  )))
19                  (Tint I32 Signed  )) (
20         (LScase (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (repr 1)) (Tint I32 Signed  )))
207                         (Tpointer Any (Tint I16 Signed  ))))
208                     (Ssequence
209                     (Sassign (Expr (Evar (ident_of_nat 8))
210                                (Tpointer Any (Tint I16 Signed  )))
211                       (Expr (Evar (ident_of_nat 20))
212                         (Tpointer Any (Tint I16 Signed  ))))
213                     (Ssequence
214                     (Sassign (Expr (Evar (ident_of_nat 20))
215                                (Tpointer Any (Tint I16 Signed  )))
216                       (Expr (Ebinop Oadd
217                         (Expr (Evar (ident_of_nat 8))
218                           (Tpointer Any (Tint I16 Signed  )))
219                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
220                         (Tpointer Any (Tint I16 Signed  ))))
221                     (Sassign (Expr (Ederef
222                                (Expr (Evar (ident_of_nat 7))
223                                  (Tpointer Any (Tint I16 Signed  ))))
224                                (Tint I16 Signed  ))
225                       (Expr (Ederef
226                         (Expr (Evar (ident_of_nat 8))
227                           (Tpointer Any (Tint I16 Signed  ))))
228                         (Tint I16 Signed  )))))))
229                     (LScase (repr 2)
230                       (Ssequence
231                       (Sassign (Expr (Evar (ident_of_nat 5))
232                                  (Tpointer Any (Tint I16 Signed  )))
233                         (Expr (Evar (ident_of_nat 19))
234                           (Tpointer Any (Tint I16 Signed  ))))
235                       (Ssequence
236                       (Sassign (Expr (Evar (ident_of_nat 19))
237                                  (Tpointer Any (Tint I16 Signed  )))
238                         (Expr (Ebinop Oadd
239                           (Expr (Evar (ident_of_nat 5))
240                             (Tpointer Any (Tint I16 Signed  )))
241                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
242                           (Tpointer Any (Tint I16 Signed  ))))
243                       (Ssequence
244                       (Sassign (Expr (Evar (ident_of_nat 6))
245                                  (Tpointer Any (Tint I16 Signed  )))
246                         (Expr (Evar (ident_of_nat 20))
247                           (Tpointer Any (Tint I16 Signed  ))))
248                       (Ssequence
249                       (Sassign (Expr (Evar (ident_of_nat 20))
250                                  (Tpointer Any (Tint I16 Signed  )))
251                         (Expr (Ebinop Oadd
252                           (Expr (Evar (ident_of_nat 6))
253                             (Tpointer Any (Tint I16 Signed  )))
254                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
255                           (Tpointer Any (Tint I16 Signed  ))))
256                       (Sassign (Expr (Ederef
257                                  (Expr (Evar (ident_of_nat 5))
258                                    (Tpointer Any (Tint I16 Signed  ))))
259                                  (Tint I16 Signed  ))
260                         (Expr (Ederef
261                           (Expr (Evar (ident_of_nat 6))
262                             (Tpointer Any (Tint I16 Signed  ))))
263                           (Tint I16 Signed  )))))))
264                       (LScase (repr 1)
265                         (Ssequence
266                         (Sassign (Expr (Evar (ident_of_nat 3))
267                                    (Tpointer Any (Tint I16 Signed  )))
268                           (Expr (Evar (ident_of_nat 19))
269                             (Tpointer Any (Tint I16 Signed  ))))
270                         (Ssequence
271                         (Sassign (Expr (Evar (ident_of_nat 19))
272                                    (Tpointer Any (Tint I16 Signed  )))
273                           (Expr (Ebinop Oadd
274                             (Expr (Evar (ident_of_nat 3))
275                               (Tpointer Any (Tint I16 Signed  )))
276                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
277                             (Tpointer Any (Tint I16 Signed  ))))
278                         (Ssequence
279                         (Sassign (Expr (Evar (ident_of_nat 4))
280                                    (Tpointer Any (Tint I16 Signed  )))
281                           (Expr (Evar (ident_of_nat 20))
282                             (Tpointer Any (Tint I16 Signed  ))))
283                         (Ssequence
284                         (Sassign (Expr (Evar (ident_of_nat 20))
285                                    (Tpointer Any (Tint I16 Signed  )))
286                           (Expr (Ebinop Oadd
287                             (Expr (Evar (ident_of_nat 4))
288                               (Tpointer Any (Tint I16 Signed  )))
289                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
290                             (Tpointer Any (Tint I16 Signed  ))))
291                         (Ssequence
292                         (Sassign (Expr (Ederef
293                                    (Expr (Evar (ident_of_nat 3))
294                                      (Tpointer Any (Tint I16 Signed  ))))
295                                    (Tint I16 Signed  ))
296                           (Expr (Ederef
297                             (Expr (Evar (ident_of_nat 4))
298                               (Tpointer Any (Tint I16 Signed  ))))
299                             (Tint I16 Signed  )))
300                         (Ssequence
301                         (Sassign (Expr (Evar (ident_of_nat 2))
302                                    (Tint I32 Signed  ))
303                           (Expr (Ebinop Osub
304                             (Expr (Evar (ident_of_nat 1))
305                               (Tint I32 Signed  ))
306                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
307                             (Tint I32 Signed  )))
308                         (Ssequence
309                         (Sassign (Expr (Evar (ident_of_nat 1))
310                                    (Tint I32 Signed  ))
311                           (Expr (Evar (ident_of_nat 2))
312                             (Tint I32 Signed  )))
313                         (Sifthenelse (Expr (Ebinop Ogt
314                                        (Expr (Evar (ident_of_nat 2))
315                                          (Tint I32 Signed  ))
316                                        (Expr (Econst_int (repr 0))
317                                          (Tint I32 Signed  )))
318                                        (Tint I32 Signed  ))
319                           (Sgoto (ident_of_nat 22))
320                           Sskip))))))))
321                         (LSdefault
322                           Sskip)))))))))
323       )))
324     
325     
326     
327   )〉;
328  〈ident_of_nat 23 (* main *), CL_Internal (
329    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)〉 ]
330      (Ssequence
331      (Sassign (Expr (Ederef
332                 (Expr (Ebinop Oadd
333                   (Expr (Evar (ident_of_nat 24))
334                     (Tarray Any (Tint I16 Signed  ) 3))
335                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
336                   (Tarray Any (Tint I16 Signed  ) 3))) (Tint I16 Signed  ))
337        (Expr (Ecast (Tint I16 Signed  )
338          (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
339          (Tint I16 Signed  )))
340      (Ssequence
341      (Sassign (Expr (Ederef
342                 (Expr (Ebinop Oadd
343                   (Expr (Evar (ident_of_nat 24))
344                     (Tarray Any (Tint I16 Signed  ) 3))
345                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
346                   (Tarray Any (Tint I16 Signed  ) 3))) (Tint I16 Signed  ))
347        (Expr (Ecast (Tint I16 Signed  )
348          (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
349          (Tint I16 Signed  )))
350      (Ssequence
351      (Sassign (Expr (Ederef
352                 (Expr (Ebinop Oadd
353                   (Expr (Evar (ident_of_nat 24))
354                     (Tarray Any (Tint I16 Signed  ) 3))
355                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
356                   (Tarray Any (Tint I16 Signed  ) 3))) (Tint I16 Signed  ))
357        (Expr (Ecast (Tint I16 Signed  )
358          (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
359          (Tint I16 Signed  )))
360      (Ssequence
361      (Scall (None expr) (Expr (Evar (ident_of_nat 0))
362                           (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
363        [(Expr (Evar (ident_of_nat 25))
364           (Tarray Any (Tint I16 Signed  ) 3));
365        (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
366        (Expr (Econst_int (repr 3)) (Tint I32 Signed  ))])
367      (Sreturn (Some expr (Expr (Ebinop Oadd
368                            (Expr (Ebinop Oadd
369                              (Expr (Ecast (Tint I32 Signed  )
370                                (Expr (Ederef
371                                  (Expr (Ebinop Oadd
372                                    (Expr (Evar (ident_of_nat 25))
373                                      (Tarray Any (Tint I16 Signed  ) 3))
374                                    (Expr (Econst_int (repr 0))
375                                      (Tint I32 Signed  )))
376                                    (Tarray Any (Tint I16 Signed  ) 3)))
377                                  (Tint I16 Signed  ))) (Tint I32 Signed  ))
378                              (Expr (Ecast (Tint I32 Signed  )
379                                (Expr (Ederef
380                                  (Expr (Ebinop Oadd
381                                    (Expr (Evar (ident_of_nat 25))
382                                      (Tarray Any (Tint I16 Signed  ) 3))
383                                    (Expr (Econst_int (repr 1))
384                                      (Tint I32 Signed  )))
385                                    (Tarray Any (Tint I16 Signed  ) 3)))
386                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
387                              (Tint I32 Signed  ))
388                            (Expr (Ecast (Tint I32 Signed  )
389                              (Expr (Ederef
390                                (Expr (Ebinop Oadd
391                                  (Expr (Evar (ident_of_nat 25))
392                                    (Tarray Any (Tint I16 Signed  ) 3))
393                                  (Expr (Econst_int (repr 2))
394                                    (Tint I32 Signed  )))
395                                  (Tarray Any (Tint I16 Signed  ) 3)))
396                                (Tint I16 Signed  ))) (Tint I32 Signed  )))
397                            (Tint I32 Signed  ))))))))
398   
399   
400   
401  )〉]
402  (ident_of_nat 23)
403  []
404.
405
406example exec: finishes_with (repr 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
407normalize @refl
408qed.
Note: See TracBrowser for help on using the repository browser.