source: src/Clight/test/search.ma @ 816

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File size: 9.7 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef type
5  [〈ident_of_nat 0 (* search *), CL_Internal (
6     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
7       (Ssequence
8       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
9         (Expr (Ecast (Tint I8 Unsigned )
10           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
11           (Tint I8 Unsigned )))
12       (Ssequence
13       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
14         (Expr (Ecast (Tint I8 Unsigned )
15           (Expr (Ebinop Osub
16             (Expr (Ecast (Tint I32 Signed  )
17               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
18               (Tint I32 Signed  ))
19             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
20             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
21       (Ssequence
22       (Ssequence
23       (Swhile (Expr (Ebinop Oge
24                 (Expr (Ecast (Tint I32 Signed  )
25                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
26                   (Tint I32 Signed  ))
27                 (Expr (Ecast (Tint I32 Signed  )
28                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
29                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
30         (Ssequence
31         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
32           (Expr (Ecast (Tint I8 Unsigned )
33             (Expr (Ebinop Odiv
34               (Expr (Ebinop Oadd
35                 (Expr (Ecast (Tint I32 Signed  )
36                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
37                   (Tint I32 Signed  ))
38                 (Expr (Ecast (Tint I32 Signed  )
39                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
40                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
41               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
42               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
43         (Ssequence
44         (Sifthenelse (Expr (Ebinop Oeq
45                        (Expr (Ecast (Tint I32 Signed  )
46                          (Expr (Ederef
47                            (Expr (Ebinop Oadd
48                              (Expr (Evar (ident_of_nat 4))
49                                (Tpointer Any (Tint I8 Unsigned )))
50                              (Expr (Evar (ident_of_nat 3))
51                                (Tint I8 Unsigned )))
52                              (Tpointer Any (Tint I8 Unsigned ))))
53                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
54                        (Expr (Ecast (Tint I32 Signed  )
55                          (Expr (Evar (ident_of_nat 6))
56                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
57                        (Tint I32 Signed  ))
58           (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
59                                 (Tint I8 Unsigned ))))
60           Sskip)
61         (Ssequence
62         (Sifthenelse (Expr (Ebinop Ogt
63                        (Expr (Ecast (Tint I32 Signed  )
64                          (Expr (Ederef
65                            (Expr (Ebinop Oadd
66                              (Expr (Evar (ident_of_nat 4))
67                                (Tpointer Any (Tint I8 Unsigned )))
68                              (Expr (Evar (ident_of_nat 3))
69                                (Tint I8 Unsigned )))
70                              (Tpointer Any (Tint I8 Unsigned ))))
71                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
72                        (Expr (Ecast (Tint I32 Signed  )
73                          (Expr (Evar (ident_of_nat 6))
74                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
75                        (Tint I32 Signed  ))
76           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
77             (Expr (Ecast (Tint I8 Unsigned )
78               (Expr (Ebinop Osub
79                 (Expr (Ecast (Tint I32 Signed  )
80                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
81                   (Tint I32 Signed  ))
82                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
83                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
84           Sskip)
85         (Sifthenelse (Expr (Ebinop Olt
86                        (Expr (Ecast (Tint I32 Signed  )
87                          (Expr (Ederef
88                            (Expr (Ebinop Oadd
89                              (Expr (Evar (ident_of_nat 4))
90                                (Tpointer Any (Tint I8 Unsigned )))
91                              (Expr (Evar (ident_of_nat 3))
92                                (Tint I8 Unsigned )))
93                              (Tpointer Any (Tint I8 Unsigned ))))
94                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
95                        (Expr (Ecast (Tint I32 Signed  )
96                          (Expr (Evar (ident_of_nat 6))
97                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
98                        (Tint I32 Signed  ))
99           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
100             (Expr (Ecast (Tint I8 Unsigned )
101               (Expr (Ebinop Oadd
102                 (Expr (Ecast (Tint I32 Signed  )
103                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
104                   (Tint I32 Signed  ))
105                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
106                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
107           Sskip)))))
108       Sskip)
109       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
110                             (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
111                                                 (Tint I32 Signed  )))
112                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
113     
114     
115     
116   )〉;
117  〈ident_of_nat 7 (* main *), CL_Internal (
118    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
119      (Ssequence
120      (Sassign (Expr (Ederef
121                 (Expr (Ebinop Oadd
122                   (Expr (Evar (ident_of_nat 4))
123                     (Tarray Any (Tint I8 Unsigned ) 5))
124                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
125                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
126        (Expr (Ecast (Tint I8 Unsigned )
127          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
128          (Tint I8 Unsigned )))
129      (Ssequence
130      (Sassign (Expr (Ederef
131                 (Expr (Ebinop Oadd
132                   (Expr (Evar (ident_of_nat 4))
133                     (Tarray Any (Tint I8 Unsigned ) 5))
134                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
135                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
136        (Expr (Ecast (Tint I8 Unsigned )
137          (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
138          (Tint I8 Unsigned )))
139      (Ssequence
140      (Sassign (Expr (Ederef
141                 (Expr (Ebinop Oadd
142                   (Expr (Evar (ident_of_nat 4))
143                     (Tarray Any (Tint I8 Unsigned ) 5))
144                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
145                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
146        (Expr (Ecast (Tint I8 Unsigned )
147          (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
148          (Tint I8 Unsigned )))
149      (Ssequence
150      (Sassign (Expr (Ederef
151                 (Expr (Ebinop Oadd
152                   (Expr (Evar (ident_of_nat 4))
153                     (Tarray Any (Tint I8 Unsigned ) 5))
154                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
155                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
156        (Expr (Ecast (Tint I8 Unsigned )
157          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
158          (Tint I8 Unsigned )))
159      (Ssequence
160      (Sassign (Expr (Ederef
161                 (Expr (Ebinop Oadd
162                   (Expr (Evar (ident_of_nat 4))
163                     (Tarray Any (Tint I8 Unsigned ) 5))
164                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
165                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
166        (Expr (Ecast (Tint I8 Unsigned )
167          (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
168          (Tint I8 Unsigned )))
169      (Ssequence
170      (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
171        (Expr (Evar (ident_of_nat 0))
172          (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
173        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
174        (Expr (Ecast (Tint I8 Unsigned )
175          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
176          (Tint I8 Unsigned ));
177        (Expr (Ecast (Tint I8 Unsigned )
178          (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
179          (Tint I8 Unsigned ))])
180      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
181                            (Expr (Evar (ident_of_nat 8))
182                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
183   
184   
185   
186  )〉]
187  (ident_of_nat 7)
188  []
189.
190
191example exec: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
192normalize  (* you can examine the result here *)
193@refl
194qed.
195
196include "Clight/toCminor.ma".
197include "Cminor/semantics.ma".
198
199example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
200normalize
201@refl
202qed.
203
204include "Cminor/toRTLabs.ma".
205include "RTLabs/semantics.ma".
206
207example e2: finishes_with (repr 3) ? (
208do p1 ← clight_to_cminor myprog;
209do p2 ← cminor_to_rtlabs p1;
210 exec_up_to RTLabs_fullexec p2 1000 [ ]).
211normalize
212@refl
213qed.
Note: See TracBrowser for help on using the repository browser.