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

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 9.8 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef ((list init_data) × 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.