source: src/Cminor/test/search.ma @ 751

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

Initial version of the Cminor syntax and semantics.

File size: 5.2 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition id_search := ident_of_nat 0.
5definition id_search_tmp0 := ident_of_nat 10.
6definition id_search_low := ident_of_nat 11.
7definition id_search_high := ident_of_nat 12.
8definition id_search_i := ident_of_nat 13.
9definition id_search_tab := ident_of_nat 14.
10definition id_search_size := ident_of_nat 15.
11definition id_search_to_find := ident_of_nat 16.
12definition C_cost8 := costlabel_of_nat 9.
13definition C_cost6 := costlabel_of_nat 8.
14definition C_cost4 := costlabel_of_nat 7.
15definition C_cost5 := costlabel_of_nat 6.
16definition C_cost2 := costlabel_of_nat 5.
17definition C_cost3 := costlabel_of_nat 4.
18definition C_cost0 := costlabel_of_nat 3.
19definition C_cost1 := costlabel_of_nat 2.
20definition C_cost7 := costlabel_of_nat 1.
21definition f_search := Internal ? (mk_internal_function
22  (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
23  [id_search_tab; id_search_size; id_search_to_find]
24  [id_search_tmp0; id_search_low; id_search_high; id_search_i]
25  [id_search_tab]
26  0 (
27  St_cost C_cost8 (
28  St_seq (
29    St_assign id_search_low (Cst (Ointconst (repr 0)))
30  ) (
31  St_seq (
32    St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_size)) (Cst (Ointconst (repr 1))))
33  ) (
34  St_seq (
35    St_seq (
36      St_block (
37        St_loop (
38          St_seq (
39            St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cge) (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low)))) (
40              St_exit 0
41            ) (
42              St_skip            )
43          ) (
44          St_block (
45            St_cost C_cost6 (
46            St_seq (
47              St_assign id_search_i (Op2 Odiv (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low))) (Cst (Ointconst (repr 2))))
48            ) (
49            St_seq (
50              St_ifthenelse (Op2 (Ocmp Ceq) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
51                St_cost C_cost4 (
52                St_return (Some ? (Id id_search_i))
53                )
54              ) (
55                St_cost C_cost5 (
56                St_skip                )
57              )
58            ) (
59            St_seq (
60              St_ifthenelse (Op2 (Ocmp Cgt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
61                St_cost C_cost2 (
62                St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1))))
63                )
64              ) (
65                St_cost C_cost3 (
66                St_skip                )
67              )
68            ) (
69            St_ifthenelse (Op2 (Ocmp Clt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (
70              St_cost C_cost0 (
71              St_assign id_search_low (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1))))
72              )
73            ) (
74              St_cost C_cost1 (
75              St_skip              )
76            )
77            )
78            )
79            )
80            )
81          )
82          )
83        )
84      )
85    ) (
86    St_cost C_cost7 (
87    St_skip    )
88    )
89  ) (
90  St_return (Some ? (Op1 Onegint (Cst (Ointconst (repr 1)))))
91  )
92  )
93  )
94  )
95
96)).
97
98definition id_main := ident_of_nat 17.
99definition id_main_tmp0 := ident_of_nat 19.
100definition id_main_res := ident_of_nat 20.
101definition C_cost9 := costlabel_of_nat 18.
102definition f_main := Internal ? (mk_internal_function
103  (mk_signature [] (Some ? ASTint))
104  []
105  [id_main_tmp0; id_main_res]
106  []
107  5 (
108  St_cost C_cost9 (
109  St_seq (
110    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 0)))
111  ) (
112  St_seq (
113    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 1))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 18)))
114  ) (
115  St_seq (
116    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 2))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 23)))
117  ) (
118  St_seq (
119    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 3))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 57)))
120  ) (
121  St_seq (
122    St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 4))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 120)))
123  ) (
124  St_seq (
125    St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
126  ) (
127  St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res)))
128  )
129  )
130  )
131  )
132  )
133  )
134  )
135
136)).
137
138
139
140definition myprog : Cminor_program :=
141mk_program ?? [
142  (pair ?? id_search f_search);
143  (pair ?? id_main f_main)
144]  id_main
145[]
146.
147
148   example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
149   normalize  (* you can examine the result here *)
150   @refl qed.
Note: See TracBrowser for help on using the repository browser.