source: src/Cminor/test/null-op.Cminor.ma @ 1351

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

Update Cminor pretty printer and some examples.

File size: 3.6 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4
5
6definition id_main := ident_of_nat 0.
7definition id_main_p := ident_of_nat 6.
8definition id_main_q := ident_of_nat 7.
9definition C_cost4 := costlabel_of_nat 5.
10definition C_cost2 := costlabel_of_nat 4.
11definition C_cost3 := costlabel_of_nat 3.
12definition C_cost0 := costlabel_of_nat 2.
13definition C_cost1 := costlabel_of_nat 1.
14definition f_main := Internal ? (mk_internal_function
15  (Some ? (ASTint I32 Signed))
16  []
17  [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)]
18  1 (
19  St_cost C_cost4 (
20  St_seq (
21    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
22  ) (
23  St_seq (
24    St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0))))
25  ) (
26  St_seq (
27    St_ifthenelse I32 Signed (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_q)) (
28      St_cost C_cost2 (
29      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
30      )
31    ) (
32      St_cost C_cost3 (
33      St_skip      )
34    )
35  ) (
36  St_seq (
37    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Osubpp I32) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
38      St_cost C_cost0 (
39      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
40      )
41    ) (
42      St_cost C_cost1 (
43      St_skip      )
44    )
45  ) (
46  St_seq (
47    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
48  ) (
49  St_seq (
50    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
51  ) (
52  St_seq (
53    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
54  ) (
55  St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0)))))))
56  )
57  )
58  )
59  )
60  )
61  )
62  )
63  )
64
65)).
66
67
68
69definition myprog : Cminor_program :=
70mk_program ?? [
71  (pair ?? id_main f_main)
72]  id_main
73[]
74.
75
76example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
77normalize  (* you can examine the result here *)
78@refl
79qed.
80
81include "Cminor/toRTLabs.ma".
82include "RTLabs/semantics.ma".
83
84example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
85normalize  (* you can examine the result here *)
86@refl
87qed.
88
Note: See TracBrowser for help on using the repository browser.