source: src/Cminor/test/switcher.ma @ 816

Last change on this file since 816 was 816, checked in by campbell, 9 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: 4.8 KB
Line 
1
2(* NB: this was produced via compcert, acc and some hand mangling because acc
3       doesn't yet implement switch correctly in the clight → cminor phase. *)
4
5include "Cminor/semantics.ma".
6include "common/Animation.ma".
7
8definition id_get := ident_of_nat 99.
9definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? ASTint))).
10
11
12definition id_main := ident_of_nat 0.
13definition id_main_i := ident_of_nat 1.
14definition id_main_x1 := ident_of_nat 2.
15definition f_main := Internal ? (mk_internal_function
16  (mk_signature [] (Some ? ASTint))
17  []
18  [id_main_i; id_main_x1]
19  []
20  0 (
21  St_seq (
22    St_assign id_main_i (Op1 Ocast8unsigned (Cst (Ointconst (repr 0))))
23  ) (
24  St_seq (
25    St_call (Some ? id_main_x1) (Cst (Oaddrsymbol id_get zero)) []
26  ) (
27  St_seq (
28    St_block (
29      St_seq (
30        St_block (
31          St_seq (
32            St_block (
33              St_seq (
34                St_block (
35                  St_seq (
36                    St_block (
37                      St_seq (
38                        St_block (
39                          St_seq (
40                            St_switch (Id id_main_x1) [
41                              (pair ?? (repr 1) 0);
42                              (pair ?? (repr 3) 1);
43                              (pair ?? (repr 5) 2);
44                              (pair ?? (repr 7) 3)] 4
45                          ) (
46                          St_skip                          )
47                        )
48                      ) (
49                      St_seq (
50                        St_exit 4
51                      ) (
52                      St_skip                      )
53                      )
54                    )
55                  ) (
56                  St_seq (
57                    St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 1)))))
58                  ) (
59                  St_seq (
60                    St_exit 3
61                  ) (
62                  St_skip                  )
63                  )
64                  )
65                )
66              ) (
67              St_seq (
68                St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 2)))))
69              ) (
70              St_skip              )
71              )
72            )
73          ) (
74          St_seq (
75            St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 3)))))
76          ) (
77          St_seq (
78            St_exit 1
79          ) (
80          St_skip          )
81          )
82          )
83        )
84      ) (
85      St_seq (
86        St_assign id_main_i (Op1 Ocast8unsigned (Op2 Oadd (Id id_main_i) (Cst (Ointconst (repr 16)))))
87      ) (
88      St_skip      )
89      )
90    )
91  ) (
92  St_seq (
93    St_return (Some ? (Id id_main_i))
94  ) (
95  St_skip  )
96  )
97  )
98  )
99
100)).
101
102
103
104definition myprog : Cminor_program :=
105mk_program ?? [
106  (pair ?? id_main f_main);
107  (pair ?? id_get f_get)
108]  id_main
109[]
110.
111
112
113example exec0: finishes_with (repr 16) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 0)]).
114normalize  (* you can examine the result here *)
115@refl qed.
116
117example exec1: finishes_with (repr 0) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 1)]).
118normalize  (* you can examine the result here *)
119@refl qed.
120
121example exec3: finishes_with (repr 1) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 3)]).
122normalize  (* you can examine the result here *)
123@refl qed.
124
125example exec5: finishes_with (repr 5) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 5)]).
126normalize  (* you can examine the result here *)
127@refl qed.
128
129example exec7: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 7)]).
130normalize  (* you can examine the result here *)
131@refl qed.
132
133include "Cminor/toRTLabs.ma".
134include "RTLabs/semantics.ma".
135
136example execRTL0: finishes_with (repr 16) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 0)]).
137normalize  (* you can examine the result here *)
138@refl
139qed.
140
141example execRTL1: finishes_with (repr 0) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 1)]).
142normalize  (* you can examine the result here *)
143@refl
144qed.
145
146example execRTL3: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 3)]).
147normalize  (* you can examine the result here *)
148@refl
149qed.
150
151example execRTL5: finishes_with (repr 5) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
152normalize  (* you can examine the result here *)
153@refl
154qed.
155
156example execRTL7: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 7)]).
157normalize  (* you can examine the result here *)
158@refl
159qed.
Note: See TracBrowser for help on using the repository browser.