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

Last change on this file since 1224 was 1224, checked in by sacerdot, 9 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.
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  []
6  [〈ident_of_nat 0 (* search *), CL_Internal (
7     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 )〉 ]
8       (Ssequence
9       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
10         (Expr (Ecast (Tint I8 Unsigned )
11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
12           (Tint I8 Unsigned )))
13       (Ssequence
14       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
15         (Expr (Ecast (Tint I8 Unsigned )
16           (Expr (Ebinop Osub
17             (Expr (Ecast (Tint I32 Signed  )
18               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
19               (Tint I32 Signed  ))
20             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
21             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
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)) (Tint I8 Unsigned )))
56                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
57           (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
58                                 (Tint I8 Unsigned ))))
59           Sskip)
60         (Ssequence
61         (Sifthenelse (Expr (Ebinop Ogt
62                        (Expr (Ecast (Tint I32 Signed  )
63                          (Expr (Ederef
64                            (Expr (Ebinop Oadd
65                              (Expr (Evar (ident_of_nat 4))
66                                (Tpointer Any (Tint I8 Unsigned )))
67                              (Expr (Evar (ident_of_nat 3))
68                                (Tint I8 Unsigned )))
69                              (Tpointer Any (Tint I8 Unsigned ))))
70                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
71                        (Expr (Ecast (Tint I32 Signed  )
72                          (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
73                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
74           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
75             (Expr (Ecast (Tint I8 Unsigned )
76               (Expr (Ebinop Osub
77                 (Expr (Ecast (Tint I32 Signed  )
78                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
79                   (Tint I32 Signed  ))
80                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
81                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
82           Sskip)
83         (Sifthenelse (Expr (Ebinop Olt
84                        (Expr (Ecast (Tint I32 Signed  )
85                          (Expr (Ederef
86                            (Expr (Ebinop Oadd
87                              (Expr (Evar (ident_of_nat 4))
88                                (Tpointer Any (Tint I8 Unsigned )))
89                              (Expr (Evar (ident_of_nat 3))
90                                (Tint I8 Unsigned )))
91                              (Tpointer Any (Tint I8 Unsigned ))))
92                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
93                        (Expr (Ecast (Tint I32 Signed  )
94                          (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
95                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
96           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
97             (Expr (Ecast (Tint I8 Unsigned )
98               (Expr (Ebinop Oadd
99                 (Expr (Ecast (Tint I32 Signed  )
100                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
101                   (Tint I32 Signed  ))
102                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
103                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
104           Sskip)))))
105       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
106                             (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
107                                                 (Tint I32 Signed  )))
108                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
109     
110     
111     
112   )〉;
113  〈ident_of_nat 7 (* main *), CL_Internal (
114    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
115      (Ssequence
116      (Sassign (Expr (Ederef
117                 (Expr (Ebinop Oadd
118                   (Expr (Evar (ident_of_nat 4))
119                     (Tarray Any (Tint I8 Unsigned ) 5))
120                   (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
121                   (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
122        (Expr (Ecast (Tint I8 Unsigned )
123          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
124          (Tint I8 Unsigned )))
125      (Ssequence
126      (Sassign (Expr (Ederef
127                 (Expr (Ebinop Oadd
128                   (Expr (Evar (ident_of_nat 4))
129                     (Tarray Any (Tint I8 Unsigned ) 5))
130                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
131                   (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
132        (Expr (Ecast (Tint I8 Unsigned )
133          (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
134          (Tint I8 Unsigned )))
135      (Ssequence
136      (Sassign (Expr (Ederef
137                 (Expr (Ebinop Oadd
138                   (Expr (Evar (ident_of_nat 4))
139                     (Tarray Any (Tint I8 Unsigned ) 5))
140                   (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
141                   (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
142        (Expr (Ecast (Tint I8 Unsigned )
143          (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
144          (Tint I8 Unsigned )))
145      (Ssequence
146      (Sassign (Expr (Ederef
147                 (Expr (Ebinop Oadd
148                   (Expr (Evar (ident_of_nat 4))
149                     (Tarray Any (Tint I8 Unsigned ) 5))
150                   (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
151                   (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
152        (Expr (Ecast (Tint I8 Unsigned )
153          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
154          (Tint I8 Unsigned )))
155      (Ssequence
156      (Sassign (Expr (Ederef
157                 (Expr (Ebinop Oadd
158                   (Expr (Evar (ident_of_nat 4))
159                     (Tarray Any (Tint I8 Unsigned ) 5))
160                   (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
161                   (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
162        (Expr (Ecast (Tint I8 Unsigned )
163          (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
164          (Tint I8 Unsigned )))
165      (Ssequence
166      (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
167        (Expr (Evar (ident_of_nat 0))
168          (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
169        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
170        (Expr (Ecast (Tint I8 Unsigned )
171          (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
172          (Tint I8 Unsigned ));
173        (Expr (Ecast (Tint I8 Unsigned )
174          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
175          (Tint I8 Unsigned ))])
176      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
177                            (Expr (Evar (ident_of_nat 8))
178                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
179   
180   
181   
182  )〉]
183  (ident_of_nat 7)
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.