source: LTS/monostack_to_asm_pass.ma @ 3574

Last change on this file since 3574 was 3574, checked in by piccolo, 4 years ago

assembly pass in place

File size: 10.7 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "asm.ma".
16
17let rec post_labelled_return_instr (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : Prop ≝
18match i with
19[ EMPTY ⇒ True
20| RETURN _ ⇒ True
21| SEQ _ _ instr ⇒ post_labelled_return_instr … instr
22| COND _ _ i_true _ i_false instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … i_false ∧
23       post_labelled_return_instr … instr
24| LOOP _ _ i_true _ instr ⇒ post_labelled_return_instr … i_true ∧ post_labelled_return_instr … instr
25| CALL _ _ opt_l instr ⇒ opt_l ≠ None ? ∧ post_labelled_return_instr … instr
26| IO _ _ _ instr ⇒ post_labelled_return_instr … instr
27].
28
29definition post_labelled_return_program : ∀p,p',l_p.Program p p' l_p → Prop ≝
30λp,p',l_p,prog.post_labelled_return_instr … (main … prog) ∧ All … (λx.post_labelled_return_instr … (f_body … x)) (env … prog).
31
32let rec trans_mono_stack_instr (i : mono_stack_Instructions)
33(pc : ℕ) : post_labelled_return_instr … i → (list asm_instructions) × (list (ℕ × (ReturnPostCostLabel flat_labels))) ≝
34match i return λx.(post_labelled_return_instr ?? x) → ? with
35[ EMPTY ⇒ λ_.〈nil ?,nil ?〉
36| RETURN _ ⇒ λ_.〈[(Seq asm_assembler_params ? asm_pop_frame (None ?)) ; (Iret …)],nil ?〉
37| SEQ i opt_l instr ⇒ λprf.
38     let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S pc) prf) in
39     〈(Seq asm_assembler_params ? (asm_seq i) opt_l) :: t_instr , ret_list 〉
40| CALL f act_p opt_l instr ⇒ λprf.
41    let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (S (S pc)) (proj2 … prf)) in
42    〈(Seq asm_assembler_params ? (asm_push_frame) (None ?)):: (Icall … f) :: t_instr,
43     (〈(S (S pc)),opt_safe … (proj1 … prf)〉) :: ret_list 〉
44| COND cond ltrue i_true lfalse i_false instr ⇒ λprf.
45  let 〈t_i_false,ret_ifalse〉 ≝ (trans_mono_stack_instr i_false (S pc) (proj2 ?? (proj1 … prf))) in
46  let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true ((S pc) + ((|t_i_false|) + 1)) (proj1 … (proj1 … prf))) in
47  let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|)) (proj2 … prf)) in
48  〈CJump asm_assembler_params ? it ((S pc) + ((|t_i_false|) + 1)) ltrue lfalse ::
49    (t_i_false @ [Ijmp asm_assembler_params ?  ((S pc) + ((|t_i_false|) + 1) + (|t_i_true|))] @ t_i_true @ t_instr),
50  ret_ifalse @ ret_itrue @ ret_list
51  〉
52| LOOP cond ltrue i_true lfalse instr ⇒ λprf.
53   let trans_cond ≝ foldr … (λc,tail.(Seq asm_assembler_params ? (asm_seq (push c)) (None ?)) :: tail) (nil ?) cond in
54   let 〈t_i_true,ret_itrue〉 ≝ (trans_mono_stack_instr i_true (pc + (|trans_cond|) + 3) (proj1 … prf)) in
55   let 〈t_instr,ret_list〉 ≝ (trans_mono_stack_instr instr (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) (proj2 … prf)) in
56   〈trans_cond @
57    [Seq asm_assembler_params ? (asm_seq (push push_not)) (None ?) ;
58     Seq asm_assembler_params ? (pop_cond) (None ?);
59     CJump asm_assembler_params ? it (pc + (|trans_cond|) + 3 + (|t_i_true|) + 1) ltrue lfalse] @ t_i_true @
60    [Ijmp asm_assembler_params ? pc] @ t_instr,
61   ret_itrue @ ret_list 〉
62| IO _ io _ _ ⇒ ?
63].
64cases io qed.
65
66record asm_env_trans_info : Type[0] ≝
67{ asm_instr : list asm_instructions
68; asm_entry_fun : FunctionName → ℕ
69; asm_call_label_fun : list (ℕ × (CallCostLabel flat_labels))
70; asm_ret_label_fun :list (ℕ × (ReturnPostCostLabel flat_labels))
71}.
72
73let rec trans_mono_stack_env_prog (env : list mono_stack_envitem) (pc : ℕ)
74(entry_f : FunctionName → ℕ) on env : All … (λx.post_labelled_return_instr … (f_body … x)) env → asm_env_trans_info ≝
75match env return λx.All ?? x → ? with
76[ nil ⇒ λ_.mk_asm_env_trans_info (nil ?) entry_f (nil ?) (nil ?)
77| cons hd tl ⇒ λprf.let 〈t_body,list_ret〉 ≝ trans_mono_stack_instr (f_body … hd) (S pc) (proj1 … prf) in
78                    let ih_info ≝ trans_mono_stack_env_prog tl (pc + 1 + |t_body|) entry_f (proj2 … prf) in
79                    mk_asm_env_trans_info
80                     ((Seq asm_assembler_params ? (asm_alloc_frame (f_pars … (f_sig … hd))) (None ?))::(t_body @ (asm_instr … ih_info)))
81                     (update_fun … (asm_entry_fun … ih_info) (f_name … (f_sig … hd)) pc)
82                     (〈pc,f_lab … hd〉::asm_call_label_fun … ih_info)
83                     (list_ret @ asm_ret_label_fun … ih_info)
84].
85
86definition trans_mono_stack_prog : ∀prog : Program stack_env_params stack_instr_params flat_labels.
87no_duplicates_labels … prog → post_labelled_return_program … prog → asm_program ≝
88λprog,no_dup,post_lab.
89let 〈t_main,main_ret_lab〉 ≝ trans_mono_stack_instr (main … prog) O (proj1 … post_lab) in
90let trans_env_info ≝ trans_mono_stack_env_prog (env … prog) (|t_main|) (λ_.O) (proj2 … post_lab) in
91mk_AssemblerProgram ?? (t_main @ (asm_instr … trans_env_info)) (pred (|t_main|)) ? (asm_entry_fun … trans_env_info)
92 (asm_call_label_fun … trans_env_info) (main_ret_lab @ (asm_ret_label_fun … trans_env_info)) ??.
93try @hide_prf cases daemon (*init_act to fix on language*)
94qed.
95
96
97
98let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT)
99(post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack :
100All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝
101match s_stack return λx.All ?? x → ? with
102[ nil ⇒ λ_.stack_t = nil ? (*stati finali to be fixed*)
103| cons hd tl ⇒ λprf.
104  (match hd return λx.hd = x → ? with
105  [ mk_Prod act code ⇒ λEQ.
106    match act with
107    [ call_act f lab ⇒ False
108    | ret_act opt_l ⇒ ∃pc :ℕ.∃stl : list ℕ.stack_t = pc :: stl ∧
109                    let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code pc ? in
110                    ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = pc ∧
111                    mono_asm_state_rel_aux tl stl post_pc t_code (pc + |ts_code|) (proj2 … prf)
112    | cost_act opt_l ⇒ let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr code post_t_pc ? in
113                     (∃post_pc.post_t = ts_code @ post_pc ∧
114                         mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf))
115                     ∨
116                     (∃new_pc.option_hd … post_t = return (Ijmp … new_pc) ∧
117                      ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧
118                      mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf))
119    ]
120  ])(refl …)
121].
122@hide_prf >EQ in prf; * // qed.
123
124definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions.
125∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions).
126ℕ → stackT → list asm_instructions → post_labelled_return_instr … s_code →
127All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝ 
128λs_code,s_stack,pc,t_stack,t_code,prf1,prf2.
129let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in
130∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧
131 (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) s_stack) ∧
132 mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2.
133 
134definition monostack_asm_pass_rel :
135∀prog : Program stack_env_params stack_instr_params flat_labels.
136∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
137let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
138∀bound.
139relations flat_labels
140(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
141(asm_operational_semantics … (asm_sem_params) t_prog) ≝
142λprog,no_dup,prf,bound.
143let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
144(mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
145 (asm_operational_semantics … (asm_sem_params) t_prog)
146 (λs1,s2.∃s2'.s2 = STATE … s2' ∧ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
147   ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
148   mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) prf1 prf2
149  )
150 (λ_.λ_.True)).
151
152
153definition mono_stack_asm_pass : ∀prog : Program stack_env_params stack_instr_params flat_labels.
154∀no_dup : no_duplicates_labels … prog.∀prf : post_labelled_return_program … prog.
155let t_prog ≝ trans_mono_stack_prog prog no_dup prf in
156∀bound.simulation_conditions … (monostack_asm_pass_rel prog no_dup prf bound) ≝
157λprog,no_dup,prf,bound.mk_simulation_conditions ….
158[4: #s1 #s1' #s2 #H inversion H
159  [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2
160    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); * #st2' ** #EQ destruct #EQstore1
161    * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 >EQcode_st1
162    * whd in match (trans_mono_stack_instr ???); normalize nodelta
163    * #pre_pc * #post_t *** #EQinstructions #EQpc lapply post_label2
164    -post_label2 >EQcont_st1 * #post_code_st2 #post_tail * #_ #Hcont_cost
165    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 whd in match (length ??);
166    <plus_n_O #EQt_code_st2
167    *
168    [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *]
169      whd %{st2'} % [ %{(refl …)} <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
170      normalize nodelta %{pre_pc} %{post_pc1} % [ % // % // >EQinstructions %] assumption
171    | cases daemon
172    ]
173  |*: cases daemon
174  ]
175]
176cases daemon
177qed.
Note: See TracBrowser for help on using the repository browser.