source: src/RTL/RTL_paolo.ma @ 1641

Last change on this file since 1641 was 1641, checked in by tranquil, 9 years ago
  • semanticsUtils_paolo.ma contains code to generate both graph and linear semantics parameters (partially migrated from LIN/semantics.ma)
  • fetch_function is now common to both graph and linear
  • started porting RTL's semantics
File size: 5.0 KB
Line 
1include "joint/Joint_paolo.ma".
2
3inductive rtl_argument : Type[0] ≝
4  | Reg : register → rtl_argument
5  | Imm : Byte → rtl_argument.
6 
7coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
8  on _r : register to rtl_argument.
9
10coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
11  on _b : Byte to rtl_argument.
12
13definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
14 
15coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
16  on _n : nat to rtl_argument.
17
18(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
19  are not sequential. Thus there is a dummy label at the moment in the code.
20  To be fixed once we understand exactly what to do with tail calls. *)
21inductive rtl_statement_extension: Type[0] ≝
22  | rtl_st_ext_stack_address: register → register → rtl_statement_extension
23  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension
24  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
25  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
26
27definition rtl_uns_params ≝ mk_unserialized_params
28  (mk_inst_params
29    (* acc_a_reg ≝ *) register
30    (* acc_b_reg ≝ *) register
31    (* acc_a_arg ≝ *) rtl_argument
32    (* acc_b_arg ≝ *) rtl_argument
33    (* dpl_reg   ≝ *) register
34    (* dph_reg   ≝ *) register
35    (* dpl_arg   ≝ *) rtl_argument
36    (* dph_arg   ≝ *) rtl_argument
37    (* snd_arg   ≝ *) rtl_argument
38    (* pair_move ≝ *) (register × rtl_argument)
39    (* call_args ≝ *) (list rtl_argument)
40    (* call_dest ≝ *) (list register)
41    (* extend_statements ≝ *) rtl_statement_extension
42    (* ext_forall_labels ≝ *) (λP.λes.True))
43  (mk_local_params
44    (mk_funct_params
45      (* resultT ≝ *) (list register)
46      (* paramsT ≝ *) (list register))
47      (* localsT ≝ *) (list register)).
48
49definition rtl_params ≝ mk_graph_params rtl_uns_params.
50definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
51
52interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
53
54(* aid unification *)
55include "hints_declaration.ma".
56unification hint 0 ≔
57(*---------------*) ⊢
58acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
59unification hint 0 ≔
60(*---------------*) ⊢
61acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
62unification hint 0 ≔
63(*---------------*) ⊢
64acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
65unification hint 0 ≔
66(*---------------*) ⊢
67acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
68unification hint 0 ≔
69(*---------------*) ⊢
70dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
71unification hint 0 ≔
72(*---------------*) ⊢
73dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
74unification hint 0 ≔
75(*---------------*) ⊢
76dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
77unification hint 0 ≔
78(*---------------*) ⊢
79dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
80unification hint 0 ≔
81(*---------------*) ⊢
82snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
83unification hint 0 ≔
84(*---------------*) ⊢
85pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
86unification hint 0 ≔
87(*---------------*) ⊢
88call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
89unification hint 0 ≔
90(*---------------*) ⊢
91call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
92
93
94definition rtl_instruction ≝ joint_instruction rtl_uns_params.
95
96definition rtl_statement ≝ joint_statement rtl_params.
97
98definition rtl_internal_function ≝
99  λglobals. joint_internal_function globals rtl_params.
100
101definition rtl_program ≝ joint_program rtl_params.
102
103(************ Same without tail calls ****************)
104
105inductive rtlntc_statement_extension: Type[0] ≝
106  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
107  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
108
109definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
110  (mk_inst_params
111    (* acc_a_reg ≝ *) register
112    (* acc_b_reg ≝ *) register
113    (* acc_a_arg ≝ *) rtl_argument
114    (* acc_b_arg ≝ *) rtl_argument
115    (* dpl_reg   ≝ *) register
116    (* dph_reg   ≝ *) register
117    (* dpl_arg   ≝ *) rtl_argument
118    (* dph_arg   ≝ *) rtl_argument
119    (* snd_arg   ≝ *) rtl_argument
120    (* pair_move ≝ *) (register × rtl_argument)
121    (* call_args ≝ *) (list rtl_argument)
122    (* call_dest ≝ *) (list register)
123    (* extend_statements ≝ *) rtlntc_statement_extension
124    (* ext_forall_labels ≝ *) (λP.λes.True))
125  (mk_local_params
126    (mk_funct_params
127      (* resultT ≝ *) (list register)
128      (* paramsT ≝ *) (list register))
129      (* localsT ≝ *) (list register))).
130
131definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
132
133definition rtlntc_internal_function ≝
134  λglobals. joint_internal_function … globals rtlntc_params.
135
136definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.