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

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 9.9 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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (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 I32 (repr ? 5)) (Tint I32 Signed  )))
176          (Tint I8 Unsigned ));
177        (Expr (Ecast (Tint I8 Unsigned )
178          (Expr (Econst_int I32 (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 I32 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 I32 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.