source: Deliverables/D3.3/Cminor-experiment/test/search.ma @ 755

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

An experimental branch of the Cminor semantics.

File size: 5.3 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 ? (FO ?)
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.