source: src/ERTL/ERTL.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File size: 6.1 KB
Line 
1include "joint/Joint.ma".
2
3inductive psd_or_hdw : Type[0] ≝
4  | PSD: register → psd_or_hdw
5  | HDW: Register → psd_or_hdw.
6
7definition ertl_hdw_readable : Register → Prop ≝
8λR.match R with
9  [ RegisterA ⇒ False
10  | RegisterB ⇒ False
11  | RegisterDPL ⇒ False
12  | RegisterDPH ⇒ False
13  | RegisterCarry ⇒ False
14  | Register04 (* = RegisterST0 *) ⇒ False
15  | Register05 (* = RegisterST1 *) ⇒ False
16  | _ ⇒ True
17  ].
18
19definition ertl_readable ≝
20λR.match R with
21[ HDW R ⇒ ertl_hdw_readable R
22| _ ⇒ True
23].
24
25definition ertl_hdw_writable : Register → Prop ≝
26λR.match R with
27  [ Register06 (* = RegisterSPL *) ⇒ False
28  | Register07 (* = RegisterSPH *) ⇒ False
29  | RegisterCarry ⇒ False
30  | _ ⇒ True
31  ].
32 
33definition ertl_writable : psd_or_hdw → Prop ≝
34λR.match R with
35[ HDW R ⇒ ertl_hdw_writable R
36| _ ⇒ True
37].
38
39definition move_dst ≝ Σr : psd_or_hdw.ertl_writable r.
40unification hint 0 ≔ ⊢ move_dst ≡ Sig psd_or_hdw (λr.ertl_writable r).
41
42definition move_src ≝ argument (Σr : psd_or_hdw.ertl_readable r).
43
44definition move_src_from_reg :
45  (Σr.ertl_readable r) → move_src ≝ Reg ?.
46coercion reg_to_move_src :
47  ∀r : (Σr : psd_or_hdw.ertl_readable r).move_src ≝
48  move_src_from_reg on _r : Sig psd_or_hdw ? to move_src.
49
50definition psd_argument_move_src : psd_argument → move_src ≝
51  λarg.match arg return λ_.move_src with
52  [ Imm b ⇒ Imm ? b
53  | Reg r ⇒ Reg ? (PSD r)
54  ]. @I qed.
55coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
56  psd_argument_move_src on _a : psd_argument to move_src.
57
58inductive ertl_seq : Type[0] ≝
59  | ertl_frame_size: register → ertl_seq.
60
61definition ERTL_uns ≝ mk_unserialized_params
62    (* acc_a_reg ≝ *) register
63    (* acc_b_reg ≝ *) register
64    (* acc_a_arg ≝ *) psd_argument
65    (* acc_b_arg ≝ *) psd_argument
66    (* dpl_reg   ≝ *) register
67    (* dph_reg   ≝ *) register
68    (* dpl_arg   ≝ *) psd_argument
69    (* dph_arg   ≝ *) psd_argument
70    (* snd_arg   ≝ *) psd_argument
71    (* pair_move ≝ *) (move_dst × move_src)
72    (* call_args ≝ *) ℕ
73    (* call_dest ≝ *) unit
74    (* ext_seq ≝ *) ertl_seq
75    (* ext_seq_labels ≝ *) (λ_.[])
76    (* has_tailcall ≝ *) false
77    (* paramsT ≝ *) unit.
78
79definition regs_from_move_dst : move_dst → list register ≝
80λm. match m with [PSD r ⇒ [r] | HDW _ ⇒ [ ] ].
81
82definition regs_from_move_src : move_src → list register ≝
83λm. match m with [Imm _ ⇒ [ ] | Reg r ⇒ match r with [PSD r1 ⇒ [r1] | HDW _ ⇒ [ ] ] ].
84
85definition ertl_ext_seq_regs : ertl_seq → list register ≝
86λs.match s with [ertl_frame_size r ⇒ [r] | _ ⇒ [ ]].
87
88definition ERTL_functs ≝ mk_get_pseudo_reg_functs ERTL_uns
89(* acc_a_regs *) (λr.[r])
90(* acc_b_regs *) (λr.[r])
91(* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
92(* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
93(* dpl_regs *) (λr.[r])
94(* dph_regs *) (λr.[r])
95(* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
96(* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
97(* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
98(* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x)))
99(* f_call_args *) (λ_.[ ])
100(* f_call_dest *) (λ_.[ ])
101(* ext_seq_regs *) ertl_ext_seq_regs
102(* params_regs *) (λ_.[ ]).
103
104definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs).
105definition ertl_program ≝ joint_program ERTL.
106unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL.
107
108interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
109
110(* aid unification *)
111unification hint 0 ≔
112(*---------------*) ⊢
113pair_move ERTL ≡ move_dst × move_src.
114unification hint 0 ≔
115(*---------------*) ⊢
116acc_a_reg ERTL ≡ register.
117unification hint 0 ≔
118(*---------------*) ⊢
119acc_b_reg ERTL ≡ register.
120unification hint 0 ≔
121(*---------------*) ⊢
122acc_a_arg ERTL ≡ psd_argument.
123unification hint 0 ≔
124(*---------------*) ⊢
125acc_b_arg ERTL ≡ psd_argument.
126unification hint 0 ≔
127(*---------------*) ⊢
128dpl_reg ERTL ≡ register.
129unification hint 0 ≔
130(*---------------*) ⊢
131dph_reg ERTL ≡ register.
132unification hint 0 ≔
133(*---------------*) ⊢
134dpl_arg ERTL ≡ psd_argument.
135unification hint 0 ≔
136(*---------------*) ⊢
137dph_arg ERTL ≡ psd_argument.
138unification hint 0 ≔
139(*---------------*) ⊢
140snd_arg ERTL ≡ psd_argument.
141unification hint 0 ≔
142(*---------------*) ⊢
143call_args ERTL ≡ ℕ.
144unification hint 0 ≔
145(*---------------*) ⊢
146call_dest ERTL ≡ unit.
147
148unification hint 0 ≔
149(*---------------*) ⊢
150ext_seq ERTL ≡ ertl_seq.
151
152coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
153  psd_argument_from_reg
154  on _r : register to snd_arg ERTL.
155coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
156  psd_argument_from_byte
157  on _b : Byte to snd_arg ERTL.
158 
159definition ertl_seq_joint ≝ extension_seq ERTL.
160coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
161  on _s : ertl_seq to joint_seq ERTL ?.
162
163definition ERTL_premain : ∀p : ertl_program.
164  joint_closed_internal_function ERTL (prog_names … p) ≝
165λp.
166let l1 : label ≝ an_identifier … one in
167let l2 : label ≝ an_identifier … (p0 one) in
168let l3 : label ≝ an_identifier … (p1 one) in
169let res ≝
170  mk_joint_internal_function ERTL (prog_names … p)
171  (mk_universe … (p0 (p0 one)))
172  (mk_universe … one)
173  it it 0 0 0 (empty_map …) l1 in
174(* todo: args for main? *)
175let res ≝ add_graph … l1
176  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
177  res in
178let res ≝ add_graph … l2
179  (sequential … (CALL ERTL ? (inl … (prog_main … p)) 0 it) l3)
180  res in
181let res ≝ add_graph … l3
182  (GOTO ? l3)
183  res in
184res.
185%
186[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
187  %
188  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
189  |2: %
190  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
191  ]
192| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
193| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
194| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
195| %{l2} %{(init_cost_label … p)} %
196]
197qed.
Note: See TracBrowser for help on using the repository browser.