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

Last change on this file since 898 was 898, checked in by campbell, 10 years ago

Update pretty printers and examples.
File size: 9.7 KB
RevLine 
[898]1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4
5
6definition id_search := ident_of_nat 0.
7definition id_search_high := ident_of_nat 10.
8definition id_search_i := ident_of_nat 11.
9definition id_search_low := ident_of_nat 12.
10definition id_search_tab := ident_of_nat 13.
11definition id_search_size := ident_of_nat 14.
12definition id_search_to_find := ident_of_nat 15.
13definition C_cost8 := costlabel_of_nat 9.
14definition C_cost6 := costlabel_of_nat 8.
15definition C_cost4 := costlabel_of_nat 7.
16definition C_cost5 := costlabel_of_nat 6.
17definition C_cost2 := costlabel_of_nat 5.
18definition C_cost3 := costlabel_of_nat 4.
19definition C_cost0 := costlabel_of_nat 3.
20definition C_cost1 := costlabel_of_nat 2.
21definition C_cost7 := costlabel_of_nat 1.
22definition f_search := Internal ? (mk_internal_function
23  (Some ? (ASTint I8 Unsigned))
24  [pair ?? id_search_tab (ASTptr Any); pair ?? id_search_size (ASTint I8 Unsigned); pair ?? id_search_to_find (ASTint I8 Unsigned)]
25  [pair ?? id_search_high (ASTint I8 Unsigned); pair ?? id_search_i (ASTint I8 Unsigned); pair ?? id_search_low (ASTint I8 Unsigned)]
26  0 (
27  St_cost C_cost8 (
28  St_seq (
29    St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0))))
30  ) (
31  St_seq (
32    St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Ocast8unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_size) (Cst (ASTint I8 Unsigned) (Ointconst (repr 1)))))
33  ) (
34  St_seq (
35    St_seq (
36      St_block (
37        St_loop (
38          St_seq (
39            St_ifthenelse I8 Unsigned (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Onotbool (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cge) (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) 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 (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Ocast8unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Odivu (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) id_search_low)) (Cst (ASTint I8 Unsigned) (Ointconst (repr 2)))))
48            ) (
49            St_seq (
50              St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Ceq) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst (repr 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
51                St_cost C_cost4 (
52                St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
53                )
54              ) (
55                St_cost C_cost5 (
56                St_skip                )
57              )
58            ) (
59            St_seq (
60              St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cgt) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst (repr 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
61                St_cost C_cost2 (
62                St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Ocast8unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst (repr 1)))))
63                )
64              ) (
65                St_cost C_cost3 (
66                St_skip                )
67              )
68            ) (
69            St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Clt) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst (repr 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
70              St_cost C_cost0 (
71              St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Ocast8unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (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 ? (dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Op1 (ASTint I8 Signed) (ASTint I8 Signed) Onegint (Cst (ASTint I8 Signed) (Ointconst (repr 1)))))))
91  )
92  )
93  )
94  )
95
96)).
97
98definition id_main := ident_of_nat 16.
99definition id_main_res := ident_of_nat 18.
100definition id_main__tmp0 := ident_of_nat 19.
101definition C_cost9 := costlabel_of_nat 17.
102definition f_main := Internal ? (mk_internal_function
103  (Some ? (ASTint I32 Signed))
104  []
105  [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp0 (ASTint I8 Unsigned)]
106  5 (
107  St_cost C_cost9 (
108  St_seq (
109    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0))))
110  ) (
111  St_seq (
112    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 1))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 18))))
113  ) (
114  St_seq (
115    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 2))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 23))))
116  ) (
117  St_seq (
118    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 3))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 57))))
119  ) (
120  St_seq (
121    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 4))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 120))))
122  ) (
123  St_seq (
124    St_seq (
125      St_call (Some ? id_main__tmp0) (Cst ? (Oaddrsymbol id_search (repr 0))) [dp ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 5)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 57))))]
126    ) (
127    St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp0)
128    )
129  ) (
130  St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) Ocast8unsigned (Id (ASTint I8 Unsigned) id_main_res))))
131  )
132  )
133  )
134  )
135  )
136  )
137  )
138
139)).
140
141
142
143definition myprog : Cminor_program :=
144mk_program ?? [
145  (pair ?? id_search f_search);
146  (pair ?? id_main f_main)
147]  id_main
148[]
149.
150
151   example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
152   normalize  (* you can examine the result here *)
153   @refl qed.
154
155
156include "Cminor/toRTLabs.ma".
157include "RTLabs/semantics.ma".
158
159example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
160normalize  (* you can examine the result here *)
161@refl
162qed.
163
Note: See TracBrowser for help on using the repository browser.