source: src/RTL/RTL_paolo.ma @ 2183

Last change on this file since 2183 was 2155, checked in by tranquil, 9 years ago

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now
File size: 5.1 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
18inductive rtl_seq : Type[0] ≝
19  | rtl_stack_address: register → register → rtl_seq.
20 
21inductive rtl_call : Type[0] ≝
22  | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
23
24inductive rtl_tailcall : Type[0] ≝
25  | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
26  | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
27
28definition rtl_uns_params ≝ mk_unserialized_params
29  (mk_step_params
30    (* acc_a_reg ≝ *) register
31    (* acc_b_reg ≝ *) register
32    (* acc_a_arg ≝ *) rtl_argument
33    (* acc_b_arg ≝ *) rtl_argument
34    (* dpl_reg   ≝ *) register
35    (* dph_reg   ≝ *) register
36    (* dpl_arg   ≝ *) rtl_argument
37    (* dph_arg   ≝ *) rtl_argument
38    (* snd_arg   ≝ *) rtl_argument
39    (* pair_move ≝ *) (register × rtl_argument)
40    (* call_args ≝ *) (list rtl_argument)
41    (* call_dest ≝ *) (list register)
42    (* ext_seq ≝ *) rtl_seq
43    (* ext_call ≝ *) rtl_call
44    (* ext_tailcall ≝ *) rtl_tailcall
45  )
46  (mk_local_params
47    (mk_funct_params
48      (* resultT ≝ *) (list register)
49      (* paramsT ≝ *) (list register))
50      (* localsT ≝ *) register).
51
52definition rtl_params ≝ mk_graph_params rtl_uns_params.
53definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
54definition rtl_internal_function ≝
55  λglobals. joint_internal_function globals rtl_params.
56definition rtl_program ≝ joint_program rtl_params.
57definition rtl_step ≝ joint_step rtl_params.
58definition rtl_seq ≝ joint_seq rtl_params.
59definition rtl_statement ≝ joint_statement rtl_params.
60
61interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
62
63(* aid unification *)
64include "hints_declaration.ma".
65unification hint 0 ≔
66(*---------------*) ⊢
67acc_a_reg rtl_params ≡ register.
68unification hint 0 ≔
69(*---------------*) ⊢
70acc_b_reg rtl_params ≡ register.
71unification hint 0 ≔
72(*---------------*) ⊢
73acc_a_arg rtl_params ≡ rtl_argument.
74unification hint 0 ≔
75(*---------------*) ⊢
76acc_b_arg rtl_params ≡ rtl_argument.
77unification hint 0 ≔
78(*---------------*) ⊢
79dpl_reg rtl_params ≡ register.
80unification hint 0 ≔
81(*---------------*) ⊢
82dph_reg rtl_params ≡ register.
83unification hint 0 ≔
84(*---------------*) ⊢
85dpl_arg rtl_params ≡ rtl_argument.
86unification hint 0 ≔
87(*---------------*) ⊢
88dph_arg rtl_params ≡ rtl_argument.
89unification hint 0 ≔
90(*---------------*) ⊢
91snd_arg rtl_params ≡ rtl_argument.
92unification hint 0 ≔
93(*---------------*) ⊢
94pair_move rtl_params ≡ register × rtl_argument.
95unification hint 0 ≔
96(*---------------*) ⊢
97call_args rtl_params ≡ list rtl_argument.
98unification hint 0 ≔
99(*---------------*) ⊢
100call_dest rtl_params ≡ list register.
101
102unification hint 0 ≔
103(*---------------*) ⊢
104ext_seq rtl_params ≡ rtl_seq.
105unification hint 0 ≔
106(*---------------*) ⊢
107ext_call rtl_params ≡ rtl_call.
108unification hint 0 ≔
109(*---------------*) ⊢
110ext_tailcall rtl_params ≡ rtl_tailcall.
111unification hint 0 ≔ globals
112(*---------------*) ⊢
113joint_step rtl_params globals ≡ rtl_step globals.
114
115unification hint 0 ≔ globals
116(*---------------*) ⊢
117joint_seq rtl_params globals ≡ rtl_seq globals.
118unification hint 0 ≔ globals
119(*---------------*) ⊢
120joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
121
122coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
123  on _r : register to snd_arg rtl_params.
124coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
125  on _b : Byte to snd_arg rtl_params.
126
127
128(************ Same without tail calls ****************)
129
130definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
131  (mk_step_params
132    (* acc_a_reg ≝ *) register
133    (* acc_b_reg ≝ *) register
134    (* acc_a_arg ≝ *) rtl_argument
135    (* acc_b_arg ≝ *) rtl_argument
136    (* dpl_reg   ≝ *) register
137    (* dph_reg   ≝ *) register
138    (* dpl_arg   ≝ *) rtl_argument
139    (* dph_arg   ≝ *) rtl_argument
140    (* snd_arg   ≝ *) rtl_argument
141    (* pair_move ≝ *) (register × rtl_argument)
142    (* call_args ≝ *) (list rtl_argument)
143    (* call_dest ≝ *) (list register)
144    (* ext_seq ≝ *) rtl_seq
145    (* ext_call ≝ *) rtl_call
146    (* ext_tailcall ≝ *) void
147  )
148  (mk_local_params
149    (mk_funct_params
150      (* resultT ≝ *) (list register)
151      (* paramsT ≝ *) (list register))
152      (* localsT ≝ *) register)).
153
154definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
155
156definition rtlntc_internal_function ≝
157  λglobals. joint_internal_function … globals rtlntc_params.
158
159definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.