source: src/Clight/test/search.c.ma @ 978

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

Update remaining Clight examples.

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