- Timestamp:
- Apr 6, 2012, 8:02:10 PM (8 years ago)
- Location:
- src/joint
- Files:
-
- 2 added
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/BEMem.ma
r1419 r1882 44 44 mk_mem … blocks (nextblock … m) (nextblock_pos … m)). 45 45 46 definition is_addressable : region → bool ≝ λr.match r with 47 [ XData ⇒ true | Code ⇒ true | _ ⇒ false ]. 48 49 50 definition is_address : (beval × beval) → Prop ≝ λa. 51 ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1. 52 \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧ 53 \snd a = BVptr p p1 ∧ part_no ? p1 = 1. 54 55 definition is_addressb : (beval × beval) → bool ≝ λa. 56 match a with 57 [ mk_Prod a0 a1 ⇒ 58 match a0 with 59 [ BVptr p0 part0 ⇒ 60 is_addressable (ptype p0) ∧ eqb part0 0 ∧ 61 match a1 with 62 [ BVptr p1 part1 ⇒ 63 eq_pointer p0 p1 ∧ eqb part1 1 64 | _ ⇒ false 65 ] 66 | _ ⇒ false 67 ] 68 ]. 69 70 lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval. 71 (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a). 72 #P * * 73 [4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)] 74 #p0 #part0 #a1 75 whd in match is_addressb; normalize nodelta 76 elim (true_or_false_Prop (is_addressable (ptype p0))) 77 #H >H 78 [ @(eqb_elim part0 0) #Heq 79 [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?); 80 [4: @eq_pointer_elim #Heq' 81 [ @(eqb_elim part1 1) #Heq'' 82 [ #Ptrue #_ @Ptrue destruct 83 %{p1} [assumption] %{part0} %{part1} 84 % [ % [ % ]] try % assumption 85 ] 86 ] 87 ] 88 ] 89 ] 90 #_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' *** 91 #H0 #H1 #H2 #H3 destruct /2 by absurd/ 92 qed. 93 46 94 (* CSC: only pointers to XRAM or code memory ATM *) 47 95 definition address ≝ beval × beval. 96 definition safe_address ≝ Sig address is_address. 97 unification hint 0 ≔ ; 98 P ≟ Prod beval beval 99 (*------------------*)⊢ 100 safe_address ≡ Sig P is_address. 48 101 49 102 definition eq_address: address → address → bool ≝ … … 53 106 definition pointer_of_address: address → res pointer ≝ 54 107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2]. 55 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer. 56 57 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair. 108 109 definition pointer_of_address_safe : safe_address → pointer ≝ 110 λp.match \fst p return λx.\fst p = x → ? with 111 [ BVptr ptr _ ⇒ λ_.ptr 112 | _ ⇒ λabs.⊥ 113 ] (refl …). 114 lapply abs -abs cases p 115 * #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4 116 destruct(H0 H4) 117 qed. 118 119 definition pointer_compat' ≝ λb,r. 120 match b with 121 [ mk_block r' z ⇒ 122 if eq_region r' r then True 123 else 124 match r with 125 [ Any ⇒ True 126 | XData ⇒ match r' with 127 [ PData ⇒ True 128 | _ ⇒ False 129 ] 130 | _ ⇒ False 131 ] 132 ]. 133 134 lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r. 135 ** #z ** // 136 qed. 137 138 lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r. 139 #b #r #H inversion H 140 [ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region % 141 | #id #EQ1 #EQ2 #EQ3 % 142 | #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) % 143 ] 144 qed. 145 146 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a). 147 ** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr) 148 cases r in Hr ⊢ %; #Hr * 149 ** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1 150 destruct normalize 151 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))] 152 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))] 153 #_ #_ normalize % 154 qed. 155 156 definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer. 157 158 example address_of_pointer_OK_to_safe : 159 ∀p,a.address_of_pointer p = OK … a → is_address a. 160 #p 161 lapply (refl … p) 162 generalize in match p in ⊢ (???%→%); ** 163 whd in match (address_of_pointer ?); 164 #b #H #o #EQp * #a0 #a1 165 normalize #EQ destruct(EQ) 166 %{p} >EQp [1,3: %] 167 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] % 168 qed. 169 170 definition safe_address_of_pointer: pointer → res safe_address ≝ λp. 171 do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ». 172 173 lemma address_of_pointer_is_safe : 174 ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address). 175 ****#z #H 176 lapply (pointer_compat_from_ind ?? H) * #o 177 normalize % 178 qed. 179 180 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ 181 code_pointer_of_beval_pair. 182 58 183 definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer. 59 184 185 definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer. 186 cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H 187 lapply (pointer_compat_from_ind … H) -H cases b * #z * #H 188 %{«mk_pointer ? (mk_block Code z) H o,I»} 189 % [2: % [2: % [ % [ % ]] % |]|] 190 qed. 191 192 (* Paolo: why only code pointers and not XRAM too? *) 60 193 definition addr_add: address → nat → res address ≝ 61 194 λaddr,n. … … 65 198 qed. 66 199 200 definition safe_addr_add: safe_address → nat → res safe_address ≝ 201 λaddr,n. 202 do ptr ← code_pointer_of_address addr ; 203 OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))). 204 normalize cases ptr #p #E @E 205 qed. 206 67 207 definition addr_sub: address → nat → res address ≝ 68 208 λaddr,n. … … 71 211 normalize cases ptr #p #E @E 72 212 qed. 213 214 definition safe_addr_sub: safe_address → nat → res safe_address ≝ 215 λaddr,n. 216 do ptr ← code_pointer_of_address addr ; 217 OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))). 218 normalize cases ptr #p #E @E 219 qed. -
src/joint/Joint_paolo.ma
r1644 r1882 4 4 include "common/Registers.ma". 5 5 include "common/Graphs.ma". 6 include "utilities/lists.ma". 7 include "common/LabelledObjects.ma". 8 include "ASM/Util.ma". 6 9 7 10 (* Here is the structure of parameter records (downward edges are coercions, … … 12 15 13 16 lin_params graph_params 14 | \_____ /____ | 15 | / \ | 16 \_______ / ↓ ↓ 17 \ _\____ params 18 \_/ \ | 19 / \ \ ↓ 20 _____/ unserialized_params 21 / _______/ | 22 / / | 23 stmt_params / local_params 24 | __/ | 25 inst_params funct_params 26 27 inst_params : types needed to define instructions 17 | \_____ /____ | 18 | / \ | 19 | / ↓ ↓ 20 | | params 21 | | | 22 | | stmt_params 23 | | / 24 unserialized_params 25 | \ 26 | \ 27 | local_params 28 | | 29 step_params funct_params 30 31 step_params : types needed to define steps (stmts with a default fallthrough) 28 32 stmt_params : adds successor type needed to define statements 29 33 funct_params : types of result register and parameters of function 30 34 local_params : adds types of local registers 31 params : adds type of code and lookup function 32 graph_params : is made just of inst_params and local_params, and the coercion 33 to params adds structure common to graph languages *) 34 35 record inst_params : Type[1] ≝ 35 params : adds type of code and related properties *) 36 37 record step_params : Type[1] ≝ 36 38 { acc_a_reg: Type[0] (* registers that will eventually need to be A *) 37 39 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) … … 46 48 ; call_args: Type[0] (* arguments of function calls *) 47 49 ; call_dest: Type[0] (* possible destination of function computation *) 48 ; ext_ instruction: Type[0] (* other instructions not fitting in the general framework *)49 ; ext_ forall_labels : (label → Prop) → ext_instruction → Prop50 ; ext_fin_ instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)51 ; ext_fin_ forall_labels : (label → Prop) → ext_fin_instruction → Prop50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *) 51 ; ext_step_labels : ext_step → list label 52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *) 53 ; ext_fin_stmt_labels : ext_fin_stmt → list label 52 54 }. 53 55 54 inductive joint_ instruction (p:inst_params) (globals: list ident): Type[0] ≝55 | COMMENT: String → joint_ instructionp globals56 | COST_LABEL: costlabel → joint_ instructionp globals57 | MOVE: pair_move p → joint_ instructionp globals58 | POP: acc_a_reg p → joint_ instructionp globals59 | PUSH: acc_a_arg p → joint_ instructionp globals60 | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_ instructionp globals61 | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_ instructionp globals62 | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_ instructionp globals63 | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_ instructionp globals56 inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝ 57 | COMMENT: String → joint_step p globals 58 | COST_LABEL: costlabel → joint_step p globals 59 | MOVE: pair_move p → joint_step p globals 60 | POP: acc_a_reg p → joint_step p globals 61 | PUSH: acc_a_arg p → joint_step p globals 62 | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals 63 | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals 64 | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals 65 | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals 64 66 (* int done with generic move *) 65 (*| INT: generic_reg p → Byte → joint_instruction p globals *) 66 | CLEAR_CARRY: joint_instruction p globals 67 | SET_CARRY: joint_instruction p globals 68 | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals 69 | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals 70 | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals 71 | COND: acc_a_reg p → label → joint_instruction p globals 72 | extension: ext_instruction p → joint_instruction p globals. 73 74 coercion extension_to_instruction : 75 ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝ 76 extension 77 on _c : ext_instruction ? to joint_instruction ??. 78 79 notation "r ← a1 .op. a2" with precedence 50 for 67 (*| INT: generic_reg p → Byte → joint_step p globals *) 68 | CLEAR_CARRY: joint_step p globals 69 | SET_CARRY: joint_step p globals 70 | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals 71 | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals 72 | CALL_ID: ident → call_args p → call_dest p → joint_step p globals 73 | COND: acc_a_reg p → label → joint_step p globals 74 | extension: ext_step p → joint_step p globals. 75 76 notation "r ← a1 .op. a2" with precedence 55 for 80 77 @{'op2 $op $r $a1 $a2}. 81 notation "r ← . op . a" with precedence 5 0for78 notation "r ← . op . a" with precedence 55 for 82 79 @{'op1 $op $r $a}. 83 notation "r ← a" with precedence 5 0for80 notation "r ← a" with precedence 55 for 84 81 @{'mov $r $a}. (* to be set in individual languages *) 85 82 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for … … 90 87 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 91 88 92 93 definition inst_forall_labels : ∀p : inst_params.∀globals. 94 (label → Prop) → joint_instruction p globals → Prop ≝ 95 λp,g,P,inst. match inst with 96 [ COND _ l ⇒ P l 97 | extension ext_s ⇒ ext_forall_labels p P ext_s 98 | _ ⇒ True 99 ]. 100 89 coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝ 90 extension on _s : ext_step ? to joint_step ??. 91 92 definition step_labels ≝ 93 λp, globals.λs : joint_step p globals. 94 match s with 95 [ COND _ l ⇒ [l] 96 | extension ext_s ⇒ ext_step_labels ? ext_s 97 | _ ⇒ [ ] 98 ]. 99 100 definition step_forall_labels : ∀p : step_params.∀globals. 101 (label → Prop) → joint_step p globals → Prop ≝ 102 λp,g,P,inst. All … P (step_labels … inst). 103 101 104 record funct_params : Type[1] ≝ 102 105 { resultT : Type[0] … … 109 112 }. 110 113 114 111 115 record unserialized_params : Type[1] ≝ 112 { u_inst_pars :> inst_params116 { u_inst_pars :> step_params 113 117 ; u_local_pars :> local_params 114 118 }. 115 119 116 120 record stmt_params : Type[1] ≝ 117 { uns erialized_pars :> unserialized_params121 { uns_pars :> unserialized_params 118 122 ; succ : Type[0] 119 ; succ_ forall_labels : (label → Prop) → succ → Prop123 ; succ_label : succ → option label 120 124 }. 121 125 122 126 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 123 | sequential: joint_ instructionp globals → succ p → joint_statement p globals127 | sequential: joint_step p globals → succ p → joint_statement p globals 124 128 | GOTO: label → joint_statement p globals 125 129 | RETURN: joint_statement p globals 126 | extension_fin : ext_fin_instruction p → joint_statement p globals. 127 128 coercion extension_fin_to_statement : 129 ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝ 130 extension_fin 131 on _c : ext_fin_instruction ? to joint_statement ??. 130 | extension_fin : ext_fin_stmt p → joint_statement p globals. 131 132 coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝ 133 extension_fin on _s : ext_fin_stmt ? to joint_statement ??. 134 135 definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals. 136 match s with 137 [ sequential _ _ ⇒ False 138 | _ ⇒ True 139 ]. 132 140 133 141 record params : Type[1] ≝ 134 142 { stmt_pars :> stmt_params 135 143 ; codeT: list ident → Type[0] 136 ; code_has_label: ∀globals.codeT globals → label → Prop 137 ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) → 138 codeT globals → Prop 144 ; code_point : Type[0] 145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals) 146 ; point_of_label : ∀globals.codeT globals → label → option code_point 147 ; point_of_succ : code_point → succ stmt_pars → code_point 139 148 }. 140 149 141 142 definition stmt_forall_labels : ∀p : stmt_params.∀globals. 143 (label → Prop) → joint_statement p globals → Prop ≝ 144 λp,g,P,stmt. match stmt with 145 [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next 146 | GOTO l ⇒ P l 147 | RETURN ⇒ True 148 | extension_fin c ⇒ ext_fin_forall_labels … P c 150 definition code_has_point ≝ 151 λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false]. 152 153 interpretation "code membership" 'mem p c = (code_has_point ?? c p). 154 155 definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). 156 unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)). 157 158 definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code. 159 match pt with 160 [ mk_Sig pt' pt_prf ⇒ 161 match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with 162 [ Some x ⇒ λ_.x 163 | None ⇒ λabs.⊥ 164 ] (refl …) 165 ]. normalize in pt_prf; 166 >abs in pt_prf; // qed. 167 168 definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals) ≝ 169 λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s. 170 171 definition forall_statements_i : 172 ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) → 173 codeT p globals → Prop ≝ 174 λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s. 175 176 lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals). 177 #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. 178 179 lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) → 180 ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c. 181 #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. 182 183 definition code_has_label ≝ λp,globals,c,l. 184 match point_of_label p globals c l with 185 [ Some pt ⇒ code_has_point … c pt 186 | None ⇒ false 149 187 ]. 188 189 definition stmt_explicit_labels : 190 ∀p,globals. 191 joint_statement p globals → list label ≝ 192 λp,globals,stmt. match stmt with 193 [ sequential c _ ⇒ step_labels … c 194 | GOTO l ⇒ [ l ] 195 | RETURN ⇒ [ ] 196 | extension_fin c ⇒ ext_fin_stmt_labels … c 197 ]. 198 199 definition stmt_implicit_label : ∀p,globals.joint_statement p globals → 200 option label ≝ 201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?]. 202 203 definition stmt_labels : ∀p : stmt_params.∀globals. 204 joint_statement p globals → list label ≝ 205 λp,g,stmt. 206 (match stmt_implicit_label … stmt with 207 [ Some l ⇒ [l] 208 | None ⇒ [ ] 209 ]) @ stmt_explicit_labels … stmt. 210 211 definition stmt_forall_labels ≝ 212 λp, globals.λ P : label → Prop.λs : joint_statement p globals. 213 All … P (stmt_labels … s). 214 215 lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals. 216 stmt_forall_labels … P s → All … P (stmt_explicit_labels … s). 217 #p#globals#P #s 218 whd in ⊢ (% → ?); 219 whd in ⊢ (???% → ?); 220 elim (stmt_implicit_label ???) [2: #next * #_] // 221 qed. 222 223 lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals. 224 stmt_forall_labels … P s → 225 opt_All … P (stmt_implicit_label … s). 226 #p#globals#P#s 227 whd in ⊢ (% → ?); 228 whd in ⊢ (???% → ?); 229 elim (stmt_implicit_label ???) 230 [ // 231 | #next * #Pnext #_ @Pnext 232 ] 233 qed. 234 235 definition code_forall_labels ≝ 236 λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c. 237 238 lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) → 239 ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝ 240 λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?). 150 241 151 242 record lin_params : Type[1] ≝ 152 243 { l_u_pars :> unserialized_params }. 153 154 include "utilities/option.ma". 244 245 lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|). 246 #tag #A #lbl #l elim l [*] 247 ** [2: #id] #a #tl #IH 248 [ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????); 249 change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????); 250 @eq_identifier_elim #Heq normalize nodelta 251 [ #_ normalize / by /] 252 | whd in ⊢ (?%→?%?); 253 ] 254 #H >(index_of_label_from_internal … H) 255 @le_S_S @(IH H) 256 qed. 257 258 (* mv *) 259 lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|. 260 #A #l elim l normalize [ #n #x #ABS destruct(ABS)] 261 #hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by / 262 qed. 263 264 lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|. 265 #A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)] 266 #n' #H @le_S_S @(IH … H) 267 qed. 268 269 lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf). 270 #A #l elim l 271 [ #n #ABS @⊥ /2 by absurd/ 272 | #hd #tl #IH * normalize // 273 ] 274 qed. 155 275 156 276 definition lin_params_to_params ≝ 157 277 λlp : lin_params. 158 278 mk_params 159 (mk_stmt_params lp unit (λ_. λ_.True))279 (mk_stmt_params lp unit (λ_.None ?)) 160 280 (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) 161 (* code_has_label ≝ *)(λglobals,code,lbl.Exists ? 162 (λl_stmt. \fst l_stmt = Some ? lbl) code) 163 (* forall_statements ≝ *)(λglobals,P,code.All ? 164 (λl_stmt. P (\snd l_stmt)) code). 281 (* code_point ≝ *)ℕ 282 (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls) 283 (* point_of_label ≝ *)(λglobals,c,lbl. 284 If occurs_exactly_once ?? lbl c then with prf do 285 return index_of_label ?? lbl c 286 else 287 None ?) 288 (* point_of_succ ≝ *)(λcurrent.λ_.S (current)). 165 289 166 290 coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params 167 291 on _lp : lin_params to params. 292 293 lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals. 294 ∀pt.pt ∈ code = leb (S pt) (|code|). 295 #lp #globals #code elim code 296 [ #pt % 297 | #hd #tl #IH * [%] 298 #n @IH 299 ]qed. 300 301 lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals. 302 ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code. 303 #lp #globals #code #lbl 304 whd in match (code_has_label ????); 305 whd in match (point_of_label ????); 306 elim (true_or_false_Prop (occurs_exactly_once ?? lbl code)) 307 #Heq >Heq normalize nodelta 308 [ >lin_code_has_point @(leb_elim (S ?)) [#_ | 309 #ABS elim(absurd ?? ABS) -ABS 310 @index_of_label_length assumption ]] % 311 qed. 168 312 169 313 record graph_params : Type[1] ≝ 170 314 { g_u_pars :> unserialized_params }. 315 316 (* move *) 317 definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝ 318 λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with 319 [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with 320 [ an_identifier i' ⇒ 321 match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with 322 [ Some y ⇒ λ_.y 323 | None ⇒ Ⓧ 324 ] 325 ] 326 ]. 327 328 lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf. 329 (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf). 330 #tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize 331 [ * ] 332 #s * #H @H % 333 qed. 171 334 172 335 (* One common instantiation of params via Graphs of joint_statements … … 175 338 λgp : graph_params. 176 339 mk_params 177 (mk_stmt_params gp label ( λP.P))340 (mk_stmt_params gp label (Some ?)) 178 341 (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) 179 (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?) 180 (* forall_statements ≝ *)(λglobals,P,code. 181 ∀l,s.lookup … code l = Some ? s → P s). 182 342 (* code_point ≝ *)label 343 (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code) 344 (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl) 345 (* point_of_succ ≝ *)(λ_.λlbl.lbl). 346 183 347 coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params 184 348 on _gp : graph_params to params. 185 186 187 definition labels_present : ∀globals.∀p : params. 188 codeT p globals → (joint_statement p globals) → Prop ≝ 189 λglobals,p,code,s. stmt_forall_labels p globals 190 (λl.code_has_label ?? code l) s. 349 350 lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals. 351 ∀pt.code_has_point … code pt = mem_set … code pt. 352 #gp#globals*#m*#i % qed. 353 354 lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals. 355 ∀lbl.code_has_label … code lbl = mem_set … code lbl. 356 #gp #globals * #m * #i % qed. 357 358 definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop. 359 λs : joint_statement p globals. 360 match s with 361 [ sequential _ n ⇒ P n 362 | _ ⇒ True 363 ]. 364 365 definition statement_closed : ∀globals.∀p : params. 366 codeT p globals → code_point p → (joint_statement p globals) → Prop ≝ 367 λglobals,p,code,pt,s. 368 All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧ 369 stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s. 191 370 192 371 definition code_closed : ∀p : params.∀globals. 193 372 codeT p globals → Prop ≝ λp,globals,code. 194 forall_statements … (labels_present… code) code.373 forall_statements_i … (statement_closed … code) code. 195 374 196 375 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *) 197 376 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars. 198 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).377 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))). 199 378 200 379 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝ … … 206 385 joint_if_result : resultT p; 207 386 joint_if_params : paramsT p; 208 joint_if_locals : l ocalsT p;387 joint_if_locals : list (localsT p); (* use void where no locals are present *) 209 388 (*CSC: XXXXX stacksize unused for LTL-...*) 210 389 joint_if_stacksize: nat; 211 390 joint_if_code : codeT p globals ; 212 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) 213 joint_if_entry : Σl: label. code_has_label … joint_if_code l; 214 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) 215 joint_if_exit : Σl: label. code_has_label … … joint_if_code l 391 joint_if_entry : point_in_code … joint_if_code ; 392 joint_if_exit : point_in_code … joint_if_code 216 393 }. 217 394 … … 219 396 λglobals,p. 220 397 Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def). 221 222 (* Currified form *)223 definition set_joint_if_exit ≝224 λglobals,pars.225 λexit: label.226 λp:joint_internal_function globals pars.227 λprf: code_has_label … (joint_if_code … p) exit.228 mk_joint_internal_function globals pars229 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)230 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)231 (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).232 398 233 399 definition set_joint_code ≝ … … 244 410 245 411 definition set_joint_if_graph ≝ 246 λglobals ,pars.412 λglobals.λpars : graph_params. 247 413 λgraph. 248 414 λp:joint_internal_function globals pars. 249 λentry_prf : code_has_label … graph (joint_if_entry … p).250 λexit_prf : code_has_label … graph (joint_if_exit … p).415 λentry_prf. 416 λexit_prf. 251 417 set_joint_code globals pars p 252 418 graph 253 (mk_Sig … (joint_if_entry …p) entry_prf)254 (mk_Sig … (joint_if_exit …p) exit_prf).419 (mk_Sig ?? (joint_if_entry ?? p) entry_prf) 420 (mk_Sig … (joint_if_exit ?? p) exit_prf). 255 421 256 422 definition set_luniverse ≝ … … 272 438 (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). 273 439 274 (* Paolo: probably should move these elsewhere *)275 definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.276 definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.277 graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.278 mk_Sig … (pi1 ?? sig_l) ?.279 @graph_add_lookup280 @(pi2 … sig_l)281 qed.282 283 440 (* Specialized for graph_params *) 284 441 definition add_graph ≝ … … 290 447 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) 291 448 code 292 (graph_dom_add_incl … (joint_if_entry … p)) 293 (graph_dom_add_incl … (joint_if_exit … p)). 449 (pi1 … (joint_if_entry … p)) 450 (pi1 … (joint_if_exit … p)). 451 >graph_code_has_point whd in match code; >mem_set_add 452 @orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ] 453 #x #H <graph_code_has_point @H 454 qed. 294 455 295 456 definition set_locals ≝ -
src/joint/TranslateUtils_paolo.ma
r1643 r1882 5 5 (* type T is the syntactic type of the generated things *) 6 6 (* (sig for RTLabs registers, unit in others ) *) 7 definition freshT ≝ λg.λpars : params.λX,T : Type[0]. 8 T → state_monad (joint_internal_function … g pars) X. 7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars). 9 8 10 9 definition rtl_ertl_fresh_reg: 11 10 ∀inst_pars,funct_pars,globals. 12 freshT globals (rtl_ertl_params inst_pars funct_pars) register unit≝13 λinst_pars,var_pars,globals, it,def.11 freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝ 12 λinst_pars,var_pars,globals,def. 14 13 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 15 14 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 16 15 16 include alias "basics/lists/list.ma". 17 17 let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n : 18 freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝ 19 match n with 20 [ O ⇒ λ_. return [ ] 21 | S n' ⇒ λ_. 22 ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it; 23 ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it; 24 return (reg :: regs') 25 ]. 26 27 lemma rtl_ertl_fresh_regs_length: 28 ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals 29 (rtl_ertl_params i_pars f_pars). ∀n: nat. 30 |(\snd (rtl_ertl_fresh_regs … n it def))| = n. 31 #ipars#fpars #globals #def #n elim n 32 [ % 33 | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim 34 #def' #regs #EQ>EQ 35 whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ] 36 qed. 37 38 definition rtl_ertl_fresh_regs_strong: 39 ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) → 40 ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝ 41 λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. // 42 qed. 18 freshT globals (rtl_ertl_params inst_pars funct_pars) 19 (Σl : list register. |l| = n) ≝ 20 let ret_type ≝ (Σl : list register. |l| = n) in 21 match n return λx.x = n → freshT … ret_type with 22 [ O ⇒ λeq'.return (mk_Sig … [ ] ?) 23 | S n' ⇒ λeq'. 24 ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n'; 25 ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals; 26 return (mk_Sig … (reg :: regs') ?) 27 ](refl …). <eq' normalize [//] elim regs' #l #eql >eql // 28 qed. 43 29 44 30 definition fresh_label: 45 ∀g_pars,globals.freshT globals g_pars label unit≝46 λg_pars,globals, it,def.31 ∀g_pars,globals.freshT globals g_pars label ≝ 32 λg_pars,globals,def. 47 33 let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in 48 34 〈set_luniverse … def luniverse, r〉. … … 52 38 (g_pars: graph_params) 53 39 (globals: list ident) 54 (insts: list (joint_ instructiong_pars globals))40 (insts: list (joint_step g_pars globals)) 55 41 (src : label) 56 42 (dest : label) … … 63 49 add_graph … src (sequential … instr dest) def 64 50 | _ ⇒ (* need to generate label *) 65 let 〈def, tmp_lbl〉 ≝ fresh_label … itdef in51 let 〈def, tmp_lbl〉 ≝ fresh_label … def in 66 52 adds_graph g_pars globals others tmp_lbl dest 67 53 (add_graph … src (sequential … instr tmp_lbl) def) … … 72 58 ∀g_pars: graph_params. 73 59 ∀globals: list ident. 74 (* type of allocatable registers and of their types (unit if not in RTLabs) *)75 ∀R,T : Type[0].76 60 (* fresh register creation *) 77 freshT globals g_pars R T→78 ∀insts: bind_list R T (joint_instructiong_pars globals).61 freshT globals g_pars (localsT … g_pars) → 62 ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals). 79 63 ∀src : label. 80 64 ∀dest : label. 81 65 joint_internal_function globals g_pars → 82 66 joint_internal_function globals g_pars ≝ 83 λg_pars,globals, T,R,fresh_r,insts,src,dest,def.67 λg_pars,globals,fresh_r,insts,src,dest,def. 84 68 let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in 85 69 adds_graph … stmts src dest def'. … … 89 73 ∀src_g_pars,dst_g_pars : graph_params. 90 74 ∀globals: list ident. 91 (* type of allocatable registers (unit if not in RTLabs) *)92 ∀T : Type[0].93 75 (* fresh register creation *) 94 freshT globals dst_g_pars (localsT dst_g_pars) T→76 freshT globals dst_g_pars (localsT dst_g_pars) → 95 77 (* function dictating the translation *) 96 (label → joint_ instructionsrc_g_pars globals →97 bind_list (localsT dst_g_pars) T (joint_instructiondst_g_pars globals)78 (label → joint_step src_g_pars globals → 79 bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals) 98 80 (* this can be added to allow redirections: × label *)) → 99 (label → ext_fin_instruction src_g_pars → 100 (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)) 101 × 102 (joint_statement dst_g_pars globals)) → 81 (label → ext_fin_stmt src_g_pars → 82 bind_new (localsT dst_g_pars) 83 ((list (joint_step dst_g_pars globals)) 84 × 85 (joint_statement dst_g_pars globals))) → 103 86 (* initialized function definition with empty graph *) 104 87 joint_internal_function globals dst_g_pars → … … 107 90 (* destination function *) 108 91 joint_internal_function globals dst_g_pars ≝ 109 λsrc_g_pars,dst_g_pars,globals, registerT,fresh_reg,trans,trans',empty,def.92 λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def. 110 93 let f : label → joint_statement (src_g_pars : params) globals → 111 94 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ … … 115 98 | GOTO next ⇒ add_graph … lbl (GOTO … next) def 116 99 | RETURN ⇒ add_graph … lbl (RETURN …) def 117 | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in 118 let 〈def, tmp_lbl〉 ≝ fresh_label … it def in 119 b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def) 100 | extension_fin c ⇒ 101 let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in 102 let 〈insts, fin〉 ≝ p in 103 let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in 104 adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def) 120 105 ] in 121 106 foldi … f (joint_if_code … def) empty. 122 123 definition b_graph_translate_no_fin :124 ∀src_g_pars : graph_params.125 ext_fin_instruction src_g_pars = void →126 ∀dst_g_pars : graph_params.127 ∀globals: list ident.128 (* type of allocatable registers (unit if not in RTLabs) *)129 ∀T : Type[0].130 (* fresh register creation *)131 freshT globals dst_g_pars (localsT dst_g_pars) T →132 (* function dictating the translation *)133 (label → joint_instruction src_g_pars globals →134 bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)135 (* this can be added to allow redirections: × label *)) →136 (* initialized function definition with empty graph *)137 joint_internal_function globals dst_g_pars →138 (* source function *)139 joint_internal_function globals src_g_pars →140 (* destination function *)141 joint_internal_function globals dst_g_pars ≝142 λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.143 b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg144 trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.145 107 146 108 (* translation without register allocation *) … … 149 111 ∀globals: list ident. 150 112 (* function dictating the translation *) 151 (label → joint_ instructionsrc_g_pars globals →152 list (joint_ instructiondst_g_pars globals)) →153 (label → ext_fin_ instructionsrc_g_pars →154 (list (joint_ instructiondst_g_pars globals))113 (label → joint_step src_g_pars globals → 114 list (joint_step dst_g_pars globals)) → 115 (label → ext_fin_stmt src_g_pars → 116 (list (joint_step dst_g_pars globals)) 155 117 × 156 118 (joint_statement dst_g_pars globals)) → … … 171 133 | RETURN ⇒ add_graph … lbl (RETURN …) def 172 134 | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in 173 let 〈def, tmp_lbl〉 ≝ fresh_label … itdef in135 let 〈def, tmp_lbl〉 ≝ fresh_label … def in 174 136 adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def) 175 137 ] in 176 138 foldi ??? f (joint_if_code ?? def) empty. 139 140 definition graph_to_lin_statement : 141 ∀p : unserialized_params.∀globals. 142 joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ 143 λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with 144 [ sequential c _ ⇒ sequential … c it 145 | GOTO l ⇒ GOTO … l 146 | RETURN ⇒ RETURN … 147 | extension_fin c ⇒ extension_fin … c 148 ]. 149 150 lemma graph_to_lin_labels : 151 ∀p : unserialized_params.∀globals,s. 152 stmt_labels … (graph_to_lin_statement p globals s) = 153 stmt_explicit_labels … s. 154 #p#globals * // 155 qed. 156 157 (* in order to make the coercion from lists to sets to work, one needs these hints *) 158 unification hint 0 ≔ ; 159 X ≟ identifier LabelTag 160 ⊢ 161 list label ≡ list X. 162 163 unification hint 0 ≔ ; 164 X ≟ identifier RegisterTag 165 ⊢ 166 list register ≡ list X. 167 168 169 definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf. 170 definition hide_Prop : Prop → Prop ≝ λP.P. 171 172 interpretation "hide proof" 'hide p = (hide_prf ? p). 173 interpretation "hide Prop" 'hide p = (hide_Prop p). 174 175 (* discard all elements failing test, return first element succeeding it *) 176 (* and the rest of the list, if any. *) 177 let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝ 178 match l with 179 [ nil ⇒ None ? 180 | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l' 181 ]. 182 183 lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr → 184 let x ≝ \fst pr in 185 let post ≝ \snd pr in 186 ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x). 187 #A#f#l elim l 188 [ normalize * #x #post #EQ destruct 189 | #y #l' #Hi * #x #post 190 normalize elim (true_or_false_Prop (f y)) #fy >fy normalize 191 #EQ 192 [ destruct >fy %{[ ]} /3 by refl, conj, I/ 193 | elim (Hi … EQ) #pre ** #prefalse #chopd #fx 194 %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx] 195 ] 196 ] 197 qed. 198 199 lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l. 200 #A#f#l elim l 201 [ normalize #_ % 202 | #y #l' #Hi normalize 203 elim (true_or_false_Prop (f y)) #fy >fy normalize 204 #EQ 205 [ destruct 206 | /3 by conj, nmk/ 207 ] 208 ] 209 qed. 210 211 unification hint 0 ≔ p, globals; 212 lp ≟ lin_params_to_params p, 213 sp ≟ stmt_pars lp, 214 js ≟ joint_statement sp globals, 215 lo ≟ labelled_obj LabelTag js 216 (*----------------------------*)⊢ 217 list lo ≡ codeT lp globals. 218 219 definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. 220 λentry : label. 221 (Σ〈visited' : identifier_map LabelTag ℕ, 222 required' : identifier_set LabelTag, 223 generated' : codeT (mk_lin_params p) globals〉.'hide ( 224 And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited')) 225 (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated')) 226 (∀l,n.lookup ?? visited' l = Some ? n → 227 And (code_has_label … (rev ? generated') l) 228 (∃s.And (And 229 (lookup … g l = Some ? s) 230 (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) 231 (opt_All ? 232 (λnext.Or (lookup … visited' next = Some ? (S n)) 233 (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉)) 234 (stmt_implicit_label … s)))))). 235 236 unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit. 237 238 let rec graph_visit 239 (p : unserialized_params) 240 (globals: list ident) 241 (g : codeT (mk_graph_params p) globals) 242 (* = graph (joint_statement (mk_graph_params p) globals *) 243 (required: identifier_set LabelTag) 244 (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *) 245 (generated: codeT (mk_lin_params p) globals) 246 (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *) 247 (visiting: list label) 248 (gen_length : ℕ) 249 (n: nat) 250 (entry : label) 251 (g_prf : code_closed … g) 252 (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited))) 253 (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated) 254 (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop ( 255 And (code_has_label … (rev ? generated) l) 256 (∃s.And (And 257 (lookup … g l = Some ? s) 258 (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉)) 259 (opt_All ? (λnext.match lookup … visited next with 260 [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉) 261 | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s))))) 262 (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated)) 263 (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting) 264 (gen_length_prf : gen_length = length ? generated) 265 (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited)))) 266 (lookup … visited entry = Some ? 0)) 267 (n_prf : le (id_map_size … g) (plus n (id_map_size … visited))) 268 on n 269 : graph_visit_ret_type … g entry ≝ 270 match chop ? (λx.¬x∈visited) visiting 271 return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with 272 [ None ⇒ λeq_chop. 273 let H ≝ chop_miss … eq_chop in 274 mk_Sig … 〈visited, required, generated〉 ? 275 | Some pr ⇒ λeq_chop. 276 let vis_hd ≝ \fst pr in 277 let vis_tl ≝ \snd pr in 278 let H ≝ chop_hit ???? eq_chop in 279 match n return λx.x = n → graph_visit_ret_type … g entry with 280 [ O ⇒ λeq_n.⊥ 281 | S n' ⇒ λeq_n. 282 (* add the label to the visited ones *) 283 let visited' ≝ add … visited vis_hd gen_length in 284 (* take l's statement *) 285 let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 286 (* translate it to its linear version *) 287 let translated_statement ≝ graph_to_lin_statement p globals statement in 288 (* add the translated statement to the code (which will be reversed later) *) 289 let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in 290 let required' ≝ stmt_explicit_labels … statement ∪ required in 291 (* put successors in the visiting worklist *) 292 let visiting' ≝ stmt_labels … statement @ vis_tl in 293 (* finally, check the implicit successor *) 294 (* if it has been already visited, we need to add a GOTO *) 295 let add_req_gen ≝ match stmt_implicit_label … statement with 296 [ Some next ⇒ 297 if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉 298 | None ⇒ 〈0, ∅, [ ]〉 299 ] in 300 graph_visit ??? 301 (\snd (\fst add_req_gen) ∪ required') 302 visited' 303 (\snd add_req_gen @ generated') 304 visiting' 305 (\fst (\fst add_req_gen) + S(gen_length)) 306 n' entry g_prf ???????? 307 ] (refl …) 308 ] (refl …). 309 whd 310 [ (* base case, visiting is all visited *) 311 %[ 312 %[ 313 %[ 314 elim entry_prf 315 [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis 316 * #ABS elim (ABS I) 317 | // 318 ] 319 | #l #l_req 320 elim (required_prf1 … l_req) #G 321 [ lapply (All_In … H G) #H >(notb_false ? H) % 322 | assumption 323 ] 324 ] 325 | assumption 326 ] 327 | #l #n #H elim (generated_prf1 … H) 328 #H1 * #s ** #H2 #H3 #H4 329 % [assumption] %{s} % 330 [% assumption 331 | @(opt_All_mp … H4) -l #l 332 lapply (in_map_domain … visited l) 333 elim (true_or_false (l∈visited)) #l_vis >l_vis 334 normalize nodelta [ * #n' ] #EQlookup >EQlookup 335 normalize nodelta * 336 [ #EQn' % >EQn' % 337 | #H %2{H} 338 | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I) 339 ] 340 ] 341 ] 342 |*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ] 343 (* first, close goals where add_gen_req plays no role *) 344 [10: (* vis_hd is in g *) @(All_split … visiting_prf … H2) 345 |1: (* n = 0 absrud *) 346 @(absurd … n_prf) 347 @lt_to_not_le 348 <eq_n 349 lapply (add_size … visited vis_hd 0 (* dummy value *)) 350 >(notb_true … H3) 351 whd in match (if ? then ? else ?); 352 whd in match (? + ?); 353 whd in match (lt ? ?); 354 #EQ <EQ @subset_card @add_subset 355 [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf) 356 #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) % 357 | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H) 358 generalize in match (opt_safe ???); #n #l_is_n 359 elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g 360 elim g #mg whd in ⊢ (?→?%); #H >H whd % 361 ] 362 |6: 363 @All_append 364 [ @(g_prf … vis_hd) <opt_to_opt_safe % 365 | >H2 in visiting_prf; 366 #H' lapply (All_append_r … H') -H' * #_ // 367 ] 368 |8: 369 %2 elim entry_prf 370 [ ** >H2 cases pre 371 [2: #x' #pre' #ABS normalize in ABS; destruct(ABS) 372 cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS') 373 |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_ 374 >lookup_add_hit >eq_gen_length % 375 ] 376 | #lookup_entry cut (entry ≠ vis_hd) 377 [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis 378 lapply (in_map_domain … visited entry) >(notb_true … entry_vis) 379 normalize nodelta >lookup_entry #ABS destruct(ABS)] 380 #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption 381 ] 382 |9: 383 >commutative_plus 384 >add_size >(notb_true … H3) normalize nodelta 385 whd in match (? + ?); 386 >commutative_plus 387 change with (? ≤ S(?) + ?) 388 >eq_n assumption 389 |*: (* where add_gen_req does matter, expand the three possible cases *) 390 lapply (refl … add_req_gen) 391 whd in ⊢ (???%→?); 392 lapply (refl … (stmt_implicit_label … statement)) 393 (* BUG *) 394 [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); 395 | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); 396 | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); 397 | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); 398 | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%); 399 ] 400 *[2,4,6,8,10: #next] 401 #EQimpl 402 whd in ⊢ (???%→?); 403 [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis 404 whd in ⊢ (???%→?);] 405 #EQ_req_gen >EQ_req_gen 406 (* these are the cases, reordering them *) 407 [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ] 408 [1,2,3: #i >mem_set_union 409 [ #H elim (orb_Prop_true … H) -H 410 [ #H >(mem_set_singl_to_eq … H) %2{next_vis}] 411 |*: >mem_set_empty whd in match (false ∨ ?); 412 ] 413 >mem_set_union 414 #H elim(orb_Prop_true … H) -H 415 [1,3,5: (* i is an explicit successor *) 416 #i_succ 417 (* if it's visited it's ok *) 418 elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis 419 [1,3,5: %2 % 420 |*: % 421 @Exists_append_l 422 whd in match (stmt_labels ???); 423 @Exists_append_r 424 @mem_list_as_set 425 @i_succ 426 ] 427 |2,4,6: (* i was already required *) 428 #i_req 429 elim (required_prf1 … i_req) 430 [1,3,5: >H2 #H elim (Exists_append … H) -H 431 [1,3,5: (* i in preamble → i∈visited *) 432 #i_pre %2 >mem_set_add @orb_Prop_r 433 lapply (All_In … H1 i_pre) 434 #H >(notb_false … H) % 435 |*: * 436 [1,3,5: (* i is vis_hd *) 437 #eq_i >eq_i %2 @mem_set_add_id 438 |*: (* i in vis_tl → i∈visiting' *) 439 #i_post % @Exists_append_r assumption 440 ] 441 ] 442 |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption 443 ] 444 ] 445 |4,5,6: 446 [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]] 447 whd in match (? @ ?); % 448 [1,3,5: 449 whd 450 >graph_to_lin_labels 451 change with (All ?? (stmt_explicit_labels ?? statement)) 452 whd in match required'; 453 generalize in match (stmt_explicit_labels … statement); 454 #l @list_as_set_All 455 #i >mem_set_union >mem_set_union 456 #i_l @orb_Prop_r @orb_Prop_l @i_l 457 |*: @(All_mp … required_prf2) 458 * #l_opt #s @All_mp 459 #l #l_req >mem_set_union @orb_Prop_r 460 >mem_set_union @orb_Prop_r @l_req 461 ] 462 |7,8,9: 463 #i whd in match visited'; 464 @(eq_identifier_elim … i vis_hd) 465 [1,3,5: #EQi >EQi #pos 466 >lookup_add_hit #EQpos cut (gen_length = pos) 467 [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %] 468 -EQpos #EQpos <EQpos -pos 469 % 470 [1,3,5: whd in match (rev ? ?); 471 >rev_append_def 472 whd 473 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 474 <associative_append >occurs_exactly_once_None] 475 >occurs_exactly_once_Some_eq >eq_identifier_refl 476 normalize nodelta 477 @generated_prf2 478 lapply (in_map_domain … visited vis_hd) 479 >(notb_true … H3) normalize nodelta // 480 |*: %{statement} 481 % 482 [1,3,5: % 483 [1,3,5: 484 change with (? = Some ? (opt_safe ???)) 485 @opt_safe_elim #s // 486 |*: whd in match (rev ? ?); 487 >rev_append_def 488 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 489 <associative_append @nth_opt_append_hit_l ] 490 >nth_opt_append_r 491 >rev_length 492 <gen_length_prf 493 [1,3,5: <minus_n_n] % 494 ] 495 |*: >EQimpl whd [3: %] 496 >mem_set_add in next_vis; 497 @eq_identifier_elim 498 [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)] 499 >lookup_add_hit 500 |*: #NEQ >(lookup_add_miss … visited … NEQ) 501 whd in match (false ∨ ?); 502 #next_vis lapply(in_map_domain … visited next) >next_vis 503 whd in ⊢ (% → ?); [ * #s ] 504 #EQlookup >EQlookup 505 ] whd 506 [1,2: %2 507 >rev_append >nth_opt_append_r 508 >rev_length whd in match generated'; 509 whd in match (|? :: ?|); <gen_length_prf 510 [1,3: <minus_n_n ] % 511 |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement); 512 >EQimpl % 513 ] 514 ] 515 ] 516 |*: 517 #NEQ #n_i >(lookup_add_miss … visited … NEQ) 518 #Hlookup elim (generated_prf1 … Hlookup) 519 #G1 * #s ** #G2 #G3 #G4 520 % 521 [1,3,5: whd in match (rev ??); 522 >rev_append_def whd 523 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 524 <associative_append >occurs_exactly_once_None] 525 >occurs_exactly_once_Some_eq 526 >eq_identifier_false 527 [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %] 528 normalize nodelta 529 assumption 530 |*: %{s} 531 % 532 [1,3,5: % 533 [1,3,5: assumption 534 |*: whd in match (rev ??); >rev_append_def 535 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 536 <associative_append @nth_opt_append_hit_l ] 537 @nth_opt_append_hit_l assumption 538 ] 539 |*: @(opt_All_mp … G4) 540 #x 541 @(eq_identifier_elim … x vis_hd) #Heq 542 [1,3,5: >Heq 543 lapply (in_map_domain … visited vis_hd) 544 >(notb_true … H3) 545 normalize nodelta #EQlookup >EQlookup normalize nodelta 546 * #nth_opt_visiting #gen_length_eq 547 >lookup_add_hit normalize nodelta % 548 >gen_length_eq % 549 |*: >(lookup_add_miss ?????? Heq) 550 lapply (in_map_domain … visited x) 551 elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta 552 [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta * 553 [1,3,5: #G %{G} 554 |2,4,6: #G %2 whd in match (rev ??); >rev_append_def 555 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 556 <associative_append @nth_opt_append_hit_l ] 557 @nth_opt_append_hit_l assumption 558 |*: #G elim(absurd ?? Heq) 559 (* BUG (but useless): -required -g -generated *) 560 >H2 in G; #G 561 lapply (refl … (nth_opt ? 0 pre)) 562 (* BUG *) 563 [generalize in ⊢ (???%→?); 564 |generalize in ⊢ (???%→?); 565 |generalize in ⊢ (???%→?); 566 ] * 567 [1,3,5: #G' >(nth_opt_append_miss_l … G') in G; 568 change with (Some ? vis_hd = ? → ?) 569 #EQvis_hd' destruct(EQvis_hd') % 570 |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G; 571 #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G') 572 >x_vis * #ABS elim (ABS I) 573 ] 574 ] 575 ] 576 ] 577 ] 578 ] 579 |10,11,12: 580 #i whd in match visited'; 581 lapply (in_map_domain … visited' i) 582 >mem_set_add 583 elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd 584 >eq_identifier_sym >i_vis_hd 585 [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis] 586 [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)] 587 #_ #EQlookup >lookup_add_miss in EQlookup; 588 [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *] 589 #EQlookup 590 [1,2,3: @EQlookup %] 591 whd in match (rev ??); >rev_append_def 592 [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); 593 <associative_append >does_not_occur_None] 594 >(does_not_occur_Some ?????? (i_vis_hd)) 595 @generated_prf2 assumption 596 |13,14,15: 597 whd in match generated'; normalize <gen_length_prf % 598 ] 599 ] 600 qed. 601 602 (* CSC: The branch compression (aka tunneling) optimization is not implemented 603 in Matita *) 604 definition branch_compress 605 ≝ λp: graph_params.λglobals.λg:codeT p globals. 606 λentry : Σl.code_has_label … g l.g. 177 607 178 definition graph_translate_no_fin : 179 ∀src_g_pars : graph_params. 180 ext_fin_instruction src_g_pars = void → 181 ∀dst_g_pars : graph_params. 182 ∀globals: list ident. 183 (* type of allocatable registers (unit if not in RTLabs) *) 184 (* function dictating the translation *) 185 (label → joint_instruction src_g_pars globals → 186 list (joint_instruction dst_g_pars globals) 187 (* this can be added to allow redirections: × label *)) → 188 (* initialized function definition with empty graph *) 189 joint_internal_function globals dst_g_pars → 190 (* source function *) 191 joint_internal_function globals src_g_pars → 192 (* destination function *) 193 joint_internal_function globals dst_g_pars ≝ 194 λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans. 195 graph_translate src_g_pars dst_g_pars globals 196 trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed. 608 lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g → 609 code_closed … (branch_compress p globals g l). 610 #p#globals#g#l#H @H qed. 611 612 lemma branch_compress_has_entry : ∀p,globals,g,l. 613 code_has_label … (branch_compress p globals g l) l. 614 #p#globals#g*#l#l_prf @l_prf qed. 615 616 definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A). 617 map ?? 618 (λs. let 〈l_opt,x〉 ≝ s in 619 〈! l ← l_opt ; if test l then return l else None ?, x〉) c. 620 621 lemma does_not_occur_filter_labels : 622 ∀tag,A,test,id,c. 623 does_not_occur ?? id (filter_labels tag A test c) = 624 (does_not_occur ?? id c ∨ ¬ test id). 625 #tag #A #test #id #c elim c 626 [ // 627 | ** [2: #lbl] #s #tl #IH 628 whd in match (filter_labels ????); normalize nodelta 629 whd in match (does_not_occur ????) in ⊢ (??%%); 630 [2: @IH] 631 normalize in match (! l ← ? ; ?); >IH 632 @(eq_identifier_elim ?? lbl id) #Heq [<Heq] 633 elim (test lbl) normalize nodelta 634 change with (eq_identifier ???) in match (instruction_matches_identifier ????); 635 [1,2: >eq_identifier_refl [2: >commutative_orb] normalize % 636 |*: >(eq_identifier_false ??? Heq) normalize nodelta % 637 ] 638 ] 639 qed. 640 641 lemma occurs_exactly_once_filter_labels : 642 ∀tag,A,test,id,c. 643 occurs_exactly_once ?? id (filter_labels tag A test c) = 644 (occurs_exactly_once ?? id c ∧ test id). 645 #tag #A #test #id #c elim c 646 [ // 647 | ** [2: #lbl] #s #tl #IH 648 whd in match (filter_labels ????); normalize nodelta 649 whd in match (occurs_exactly_once ????) in ⊢ (??%%); 650 [2: @IH] 651 normalize in match (! l ← ? ; ?); >IH 652 >does_not_occur_filter_labels 653 @(eq_identifier_elim ?? lbl id) #Heq [<Heq] 654 elim (test lbl) normalize nodelta 655 change with (eq_identifier ???) in match (instruction_matches_identifier ????); 656 [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize % 657 |*: >(eq_identifier_false ??? Heq) normalize nodelta % 658 ] 659 ] 660 qed. 661 662 lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n. 663 nth_opt ? n (filter_labels tag A test instrs) = 664 ! 〈lopt, s〉 ← nth_opt ? n instrs ; 665 return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉. 666 #tag #A #test #instrs elim instrs 667 [ * [2: #n'] % 668 | * #lopt #s #tl #IH * [2: #n'] 669 whd in match (filter_labels ????); normalize nodelta 670 whd in match (nth_opt ???) in ⊢ (??%%); [>IH] % 671 ] 672 qed. 673 674 definition linearize_code: 675 ∀p : unserialized_params.∀globals. 676 ∀g : codeT (mk_graph_params p) globals.code_closed … g → 677 ∀entry : (Σl. code_has_label … g l). 678 (Σc : codeT (mk_lin_params p) globals. 679 code_closed … c ∧ 680 ∃ sigma : identifier_map LabelTag ℕ. 681 lookup … sigma entry = Some ? 0 ∧ 682 ∀l,n.lookup … sigma l = Some ? n → 683 ∃s. lookup … g l = Some ? s ∧ 684 opt_Exists ? 685 (λls.let 〈lopt, ts〉 ≝ ls in 686 opt_All ? (eq ? l) lopt ∧ 687 ts = graph_to_lin_statement … s ∧ 688 opt_All ? 689 (λnext.Or (lookup … sigma next = Some ? (S n)) 690 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 691 (stmt_implicit_label … s)) (nth_opt … n c)) 692 ≝ 693 λp,globals,g,g_prf,entry_sig. 694 let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in 695 let g_prf ≝ branch_compress_closed … g entry_sig g_prf in 696 let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in 697 match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|) 698 (entry_sig) g_prf ???????? 699 with 700 [ mk_Sig triple H ⇒ 701 let sigma ≝ \fst (\fst triple) in 702 let required ≝ \snd (\fst triple) in 703 let crev ≝ \snd triple in 704 let lbld_code ≝ rev ? crev in 705 mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ]. 706 [ (* done later *) 707 | #i >mem_set_empty * 708 | % 709 |#l #n normalize in ⊢ (%→?); #ABS destruct(ABS) 710 | #l #_ % 711 | % [2: %] @(pi2 … entry_sig') 712 | % 713 | % % [% %] cases (pi1 … entry_sig) normalize #_ % // 714 | >commutative_plus change with (? ≤ |g|) % 715 ] 716 lapply (refl … triple) 717 generalize in match triple in ⊢ (???%→%); ** 718 #visited #required #generated #EQtriple 719 >EQtriple in H ⊢ %; normalize nodelta *** 720 #entry_O #req_vis #labels_in_req #sigma_prop 721 % >EQtriple 722 [ (* code closed *) 723 @All_map 724 [2: @All_rev 725 @(All_mp … labels_in_req) #ls #H @H 726 |1: (* side-effect close *) 727 |3: * #lopt #s @All_mp 728 #lbl #lbl_req whd in match (code_has_label ????); 729 >occurs_exactly_once_filter_labels 730 @andb_Prop [2: assumption] 731 lapply (in_map_domain … visited lbl) 732 >(req_vis … lbl_req) * #n #eq_lookup 733 elim (sigma_prop ?? eq_lookup) #H #_ @H 734 ] 735 ] 736 %{visited} % [assumption] 737 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 738 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 739 % [2: % [ assumption ] |] 740 >nth_opt_filter_labels in ⊢ (???%); 741 >nth_opt_is_stmt 742 whd in match (! 〈lopt, s〉 ← Some ??; ?); 743 whd 744 whd in match (! lbl0 ← Some ??; ?); 745 % [ % [ elim (lbl ∈ required) ] % ] 746 whd 747 lapply (refl … (stmt_implicit_label … stmt)) 748 generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next] 749 #eq_impl_lbl normalize nodelta [2: %] 750 >eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H 751 [ %{H} 752 | %2 >nth_opt_filter_labels >H 753 whd in match (! 〈lopt, s〉 ← ?; ?); 754 whd in match (! lbl0 ← ?; ?); 755 % 756 ] 757 qed. 758 759 definition graph_linearize : 760 ∀p : unserialized_params. 761 ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p). 762 Σfout : joint_closed_internal_function globals (mk_lin_params p). 763 ∃sigma : identifier_map LabelTag ℕ. 764 let g ≝ joint_if_code ?? (pi1 … fin) in 765 let c ≝ joint_if_code ?? (pi1 … fout) in 766 let entry ≝ joint_if_entry ?? (pi1 … fin) in 767 lookup … sigma entry = Some ? 0 ∧ 768 ∀l,n.lookup … sigma l = Some ? n → 769 ∃s. lookup … g l = Some ? s ∧ 770 opt_Exists ? 771 (λls.let 〈lopt, ts〉 ≝ ls in 772 opt_All ? (eq ? l) lopt ∧ 773 ts = graph_to_lin_statement … s ∧ 774 opt_All ? 775 (λnext.Or (lookup … sigma next = Some ? (S n)) 776 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 777 (stmt_implicit_label … s)) (nth_opt … n c) ≝ 778 λp,globals,f_sig. 779 mk_Sig ?? (match f_sig with 780 [ mk_Sig f f_prf ⇒ 781 mk_joint_internal_function globals (mk_lin_params p) 782 (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) 783 (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f) 784 (joint_if_stacksize ?? f) 785 (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f)) 786 (mk_Sig ?? it I) (mk_Sig ?? it I) 787 ]) ?. 788 elim f_sig 789 normalize nodelta #f_in #f_in_prf 790 elim (linearize_code ?????) 791 #f_out * #f_out_closed #H assumption 792 qed. 793 197 794 198 795 -
src/joint/semanticsUtils_paolo.ma
r1641 r1882 21 21 (******************************** GRAPHS **************************************) 22 22 23 definition graph_pointer_of_label0: 24 pointer → label → Σp:pointer. ptype p = Code ≝ 25 λoldpc,l. 26 mk_pointer Code 27 (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))). 28 // qed. 29 30 definition graph_pointer_of_label : 31 ∀pars : graph_params.∀globals. genv globals pars → pointer → label → 32 res (Σp:pointer. ptype p = Code) ≝ 33 λ_.λ_.λ_.λoldpc,l. 34 OK ? (graph_pointer_of_label0 oldpc l). 23 definition graph_pointer_of_label : cpointer → label → res cpointer ≝ 24 λoldpc,l. 25 return (mk_pointer Code 26 (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer). 27 % qed. 35 28 36 29 definition graph_label_of_pointer: pointer → res label ≝ 37 30 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). 38 39 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.40 But I can't use it directly because this one uses a concrete definition of41 pointer_of_label and it is used to istantiate the more_sem_params record42 where the abstract version is declared as a field. Is there a better way43 to organize the code? *)44 definition graph_succ_p: label → address → res address ≝45 λl,old.46 do ptr ← pointer_of_address old ;47 let newptr ≝ graph_pointer_of_label0 ptr l in48 address_of_pointer newptr.49 31 50 32 definition graph_fetch_statement: … … 53 35 ∀globals. 54 36 genv globals pars → 55 state sem_pars→37 cpointer → 56 38 res (joint_statement pars globals) ≝ 57 λpars,sem_pars,globals,ge,st. 58 do p ← code_pointer_of_address (pc … st) ; 39 λpars,sem_pars,globals,ge,p. 59 40 do f ← fetch_function … ge p ; 60 41 do l ← graph_label_of_pointer p; … … 71 52 pars 72 53 g_pars 73 graph_ succ_p74 ( graph_pointer_of_label ?)75 (graph_fetch_statement ? ?)54 graph_pointer_of_label 55 (λ_.λ_.graph_pointer_of_label) 56 (graph_fetch_statement ? g_pars) 76 57 ). 77 58 78 59 (******************************** LINEAR **************************************) 79 80 definition lin_succ_p: unit → address → res address:=81 λ _.λaddr. addr_add addr 1.82 60 check mk_pointer 61 definition lin_succ_p: cpointer → unit → res cpointer := 62 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?». 63 [%| cases ptr //] qed. 83 64 84 65 axiom BadLabel: String. … … 86 67 definition lin_pointer_of_label: 87 68 ∀pars : lin_params. 88 ∀globals. genv globals pars → pointer → label → 89 res (Σp:pointer. ptype p = Code) ≝ 69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝ 90 70 λpars,globals,ge,old,l. 91 71 do fn ← fetch_function … ge old ; … … 97 77 (joint_if_code … pars fn)) ; 98 78 OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). 99 //qed.79 % qed. 100 80 101 81 definition lin_fetch_statement: … … 103 83 ∀sem_pars : sem_state_params. 104 84 ∀globals. 105 genv globals pars → state sem_pars → res (joint_statement pars globals) ≝ 106 λpars,sem_pars,globals,ge,st. 107 do ppc ← pointer_of_address (pc … st) ; 85 genv globals pars → cpointer → res (joint_statement pars globals) ≝ 86 λpars,sem_pars,globals,ge,ppc. 108 87 do fn ← fetch_function … ge ppc ; 109 88 let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *) … … 123 102 lin_succ_p 124 103 (lin_pointer_of_label ?) 125 (lin_fetch_statement ? ?)104 (lin_fetch_statement ? g_pars) 126 105 ). 127 106 128 107 definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝ 108 λp,globals,stp.match stp with 109 [ COND _ _ ⇒ false 110 | CALL_ID _ _ _ ⇒ false 111 | extension c' ⇒ (* FIXME: does not care about calling extensions!! *) 112 match ext_step_labels … c' with 113 [ nil ⇒ true 114 | _ ⇒ false 115 ] 116 | _ ⇒ true 117 ]. 118 119 definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝ 120 λp,globals,stp.match stp with 121 [ sequential _ _ ⇒ false 122 | _ ⇒ true 123 ]. 124 125 inductive s_block (p : params) (globals : list ident) : Type[0] ≝ 126 | Skip : s_block p globals 127 | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals 128 | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals 129 | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals. 130 131 include "utilities/bind_new.ma". 132 133 definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals). 134 135 definition Bcons ≝ λp : params.λglobals. 136 λs : Σs.bool_to_Prop (step_unbranching p globals s). 137 λB : Block p globals. 138 ! b ← B ; return Cons ?? s b. 139 140 interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl). 141 142 let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝ 143 match b1 with 144 [ Skip ⇒ true 145 | FinStep _ ⇒ false 146 | FinStmt _ ⇒ false 147 | Cons _ tl ⇒ is_unbranching ?? tl 148 ]. 149 150 let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝ 151 match b1 with 152 [ bret b ⇒ bool_to_Prop (is_unbranching … b) 153 | bnew f ⇒ ∀x.Is_unbranching … (f x) 154 ]. 155 156 let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝ 157 match b1 return λx.is_unbranching ?? x → ? with 158 [ Skip ⇒ λ_.b2 159 | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf) 160 | _ ⇒ Ⓧ 161 ]. 162 163 definition s_block_append ≝ 164 λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2. 165 match b1 with 166 [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ]. 167 168 definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) → 169 bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝ 170 λp,globals. ?. 171 * #b elim b -b 172 [ #b #H @bret @b @H 173 | #f #IH #H @bnew #x @(IH x) @H 174 ] 175 qed. 176 177 lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B. 178 #p #globals * #b elim b 179 [ // 180 | #f #IH #H @bnew_proper 181 #x @IH 182 ] 183 qed. 184 185 definition Block_append ≝ 186 λp,globals.λB : Σb.Is_unbranching … b.λB'. 187 ! b1 ← Is_to_is_unbr … B; 188 ! b2 ← B'; 189 return s_block_append p globals b1 b2. 190 191 definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)). 192 193 let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l : 194 s_block p globals ≝ 195 match l with 196 [ nil ⇒ Skip ?? 197 | cons hd tl ⇒ 198 If step_unbranching … hd then with prf do 199 Cons ?? hd (step_list_to_s_block ?? tl) 200 else with prf do 201 FinStep ?? hd 202 ]. [assumption | >prf % ] qed. 203 204 definition step_list_to_block : ∀R,p,g.? → Block R p g ≝ 205 λR,p,globals,l.bret R ? (step_list_to_s_block p globals l). 206 207 record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝ 208 { function_rel : joint_function globals p1 → joint_function globals p2 → Prop 209 ; genv_rel : genv globals p1 → genv globals p2 → Prop 210 ; pc_rel : cpointer → cpointer → Prop 211 ; st_rel : state p1 → state p2 → Prop 212 ; stmt_rel : joint_statement p1 globals → Block 213 (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *) 214 ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2) 215 }. 216 217 (* move *) 218 definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝ 219 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒ 220 match pty return λpty. ? → pty = XData → ? with 221 [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ? 222 | _ ⇒ λpok'.λabs. ⊥] pok] ?. 223 [@(pi2 … p) |6: // |7: %] destruct (abs) 224 qed. 225 226 definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer. 227 cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H 228 lapply (pointer_compat_from_ind … H) -H cases b * #z * #H 229 %{«mk_pointer ? (mk_block ? z) H o,I»} 230 % [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:] 231 qed. 232 233 definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝ 234 λp1,p2,R,st1,st2. 235 frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧ 236 pc_rel p1 p2 R (pc … st1) (pc … st2) ∧ 237 sp_rel p1 p2 R 238 (safe_address_of_xdata_pointer (sp … st1)) 239 (safe_address_of_xdata_pointer (sp … st2)) ∧ 240 isp_rel p1 p2 R 241 (safe_address_of_xdata_pointer (isp … st1)) 242 (safe_address_of_xdata_pointer (isp … st2)) ∧ 243 sp_rel p1 p2 R 244 (safe_address_of_xdata_pointer (sp … st1)) 245 (safe_address_of_xdata_pointer (sp … st2)) ∧ 246 carry … st1 = carry … st2 ∧ 247 regs_rel p1 p2 R (regs … st1) (regs … st2) ∧ 248 mem_rel p1 p2 R (m … st1) (m … st2). 249 elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1 250 elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2 251 assumption 252 qed. 253 elim st2 254 -st1 -st2 #st2 ** #good_pc2 # ∧ 255 frames_rel … R (st_frms … st1) (st_frms … st2) ∧ 256 frames_rel … R (st_frms … st1) (st_frms … st2) ∧ 257 frames_rel … R (st_frms … st1) (st_frms … st2) ∧ 258 259 260 -
src/joint/semantics_paolo.ma
r1709 r1882 12 12 13 13 definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p). 14 definition cpointer ≝ Σp.ptype p = Code. 15 definition xpointer ≝ Σp.ptype p = XData. 16 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). 17 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). 14 18 15 19 record sem_state_params : Type[1] ≝ … … 17 21 ; empty_framesT: framesT 18 22 ; regsT : Type[0] 19 ; empty_regsT: address→ regsT (* Stack pointer *)23 ; empty_regsT: xpointer → regsT (* Stack pointer *) 20 24 }. 21 25 22 26 record state (semp: sem_state_params): Type[0] ≝ 23 27 { st_frms: framesT semp 24 ; pc: address 25 ; sp: pointer 26 ; isp: pointer 28 ; sp: xpointer 29 ; isp: xpointer 27 30 ; carry: beval 28 31 ; regs: regsT semp 29 32 ; m: bemem 30 33 }. 31 34 35 record state_pc (semp : sem_state_params) : Type[0] ≝ 36 { st_no_pc :> state semp 37 ; pc : cpointer 38 }. 39 32 40 definition set_m: ∀p. bemem → state p → state p ≝ 33 λp,m,st. mk_state p (st_frms … st) (pc …st) (sp … st) (isp … st) (carry … st) (regs … st) m.41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m. 34 42 35 43 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝ 36 λp,regs,st. mk_state p (st_frms … st) ( pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).37 38 definition set_sp: ∀p. pointer→ state p → state p ≝39 λp,sp,st. mk_state … (st_frms … st) (pc … st)sp (isp … st) (carry … st) (regs … st) (m … st).40 41 definition set_isp: ∀p. pointer→ state p → state p ≝42 λp,isp,st. mk_state … (st_frms … st) ( pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st). 45 46 definition set_sp: ∀p. ? → state p → state p ≝ 47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st). 48 49 definition set_isp: ∀p. ? → state p → state p ≝ 50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st). 43 51 44 52 definition set_carry: ∀p. beval → state p → state p ≝ 45 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st). 46 47 definition set_pc: ∀p. address → state p → state p ≝ 48 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st). 53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st). 54 55 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ 56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc. 57 58 definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝ 59 λp,s,st. mk_state_pc … s (pc … st). 49 60 50 61 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ 51 λp,frms,st. mk_state … frms ( pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st). 52 63 53 64 axiom BadProgramCounter : String. … … 57 68 ∀globals. 58 69 genv globals pars → 59 pointer →70 cpointer → 60 71 res (joint_internal_function … pars) ≝ 61 72 λpars,globals,ge,p. … … 65 76 [ Internal def' ⇒ OK … def' 66 77 | External _ ⇒ Error … [MSG BadProgramCounter]]. 67 78 79 inductive step_flow (p : params) (globals : list ident) : Type[0] ≝ 80 | Redirect : label → step_flow p globals (* used for goto-like flow alteration *) 81 | Init : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *) 82 | Proceed : step_flow p globals. (* go to implicit successor *) 83 84 inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝ 85 | SRedirect : label → stmt_flow p globals 86 | SProceed : succ p → stmt_flow p globals 87 | SInit : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals 88 | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals 89 | SEnd : stmt_flow p globals. (* end flow *) 90 91 68 92 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝ 69 93 { st_pars :> sem_state_params … … 82 106 ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval 83 107 ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) 84 ; fetch_ra: state st_pars → 85 res ((state st_pars) × address) 86 87 ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars 108 ; fetch_ra: state st_pars → res ((state st_pars) × cpointer) 109 110 ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars 88 111 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 89 ; save_frame: address → call_dest uns_pars → state st_pars → statest_pars112 ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars 90 113 (*CSC: setup_call returns a res only because we can call a function with the wrong number and 91 114 type of arguments. To be fixed using a dependent type *) … … 94 117 ; fetch_external_args: external_function → state st_pars → 95 118 res (list val) 96 ; set_result: list val → state st_pars → 97 res (state st_pars) 119 ; set_result: list val → state st_pars → res (state st_pars) 98 120 ; call_args_for_main: call_args uns_pars 99 121 ; call_dest_for_main: call_dest uns_pars … … 111 133 (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) → 112 134 ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝ 113 λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).135 λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st. 114 136 115 137 definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_. … … 126 148 definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_. 127 149 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. 128 definition pair_reg_move : ?→?→?→?→ res ?≝150 definition pair_reg_move : ?→?→?→?→? ≝ 129 151 λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up. 130 152 ! r ← pair_reg_move_ ? p (regs ? st) pm; 131 return (set_regs ? r st). 132 153 return set_regs ? r st. 154 155 133 156 axiom BadPointer : String. 134 157 135 158 (* this is preamble to all calls (including tail ones). The optional argument in 136 159 input tells the function whether it has to save the frame for internal 137 160 calls. 138 the first element of the triple is the label at the start of the function139 i n case of an internal call, or None in case of an external one.161 the first element of the triple is the entry point of the function if 162 it is an internal one, or false in case of an external one. 140 163 The actual update of the pc is left to later, as it depends on 141 164 serialization and on whether the call is a tail one. *) 142 definition eval_call_block _preamble:165 definition eval_call_block: 143 166 ∀globals.∀p : params.∀p':more_sem_unserialized_params p. 144 genv globals p → state p' → block → call_args p → option ((call_dest p) × address)→145 IO io_out io_in (( option label)×trace×(state p')) ≝146 λglobals,p,p',ge,st,b,args,dest _ra.167 genv globals p → state p' → block → call_args p → call_dest p → 168 IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝ 169 λglobals,p,p',ge,st,b,args,dest. 147 170 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?); 148 171 match fd with 149 172 [ Internal fn ⇒ 150 let st ≝ match dest_ra with 151 [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st 152 | None ⇒ st 153 ] in 154 ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 155 args st ; 156 let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in 157 let l' ≝ joint_if_entry … fn in 158 let st ≝ set_regs p' regs st in 159 return 〈Some label l', E0, st〉 173 return 〈Init … (block_id b) fn args dest, E0, st〉 160 174 | External fn ⇒ 161 175 ! params ← fetch_external_args … p' fn st : IO ???; … … 167 181 let vs ≝ [mk_val ? evres] in 168 182 ! st ← set_result … p' vs st : IO ???; 169 return 〈 None?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉183 return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 170 184 ]. 171 185 172 186 axiom FailedStore: String. 173 187 174 definition push: ∀p. 188 definition push: ∀p.state p → beval → res (state p) ≝ 175 189 λp,st,v. 176 let isp ≝ isp … st in 177 do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v); 178 let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in 179 OK … (set_m … m (set_isp … isp st)). 180 181 definition pop: ∀p. state p → res (state p × beval) ≝ 190 let isp' ≝ isp ? st in 191 do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v); 192 let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in 193 return set_m … m (set_isp … isp'' st). 194 normalize elim (isp p st) // 195 qed. 196 197 definition pop: ∀p. state p → res ((state p ) × beval) ≝ 182 198 λp,st. 183 let isp ≝ isp ? st in 184 let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in 185 let ist ≝ set_isp … isp st in 186 do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp); 187 OK ? 〈st,v〉. 188 189 definition save_ra : ∀p. state p → address → res (state p) ≝ 199 let isp' ≝ isp ? st in 200 let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in 201 let ist ≝ set_isp … isp'' st in 202 do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp''); 203 OK ? 〈ist,v〉. 204 normalize elim (isp p st) // 205 qed. 206 207 definition save_ra : ∀p. state p → cpointer → res (state p) ≝ 190 208 λp,st,l. 191 let 〈addrl,addrh〉 ≝ l in192 do st← push … st addrl;193 push … st addrh.194 195 definition load_ra : ∀p.state p → res ( state p × address) ≝209 let 〈addrl,addrh〉 ≝ address_of_code_pointer l in 210 ! st' ← push … st addrl; 211 push … st' addrh. 212 213 definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝ 196 214 λp,st. 197 do 〈st,addrh〉 ← pop … st; 198 do 〈st,addrl〉 ← pop … st; 199 OK ? 〈st, 〈addrl,addrh〉〉. 200 215 do 〈st',addrh〉 ← pop … st; 216 do 〈st'',addrl〉 ← pop … st'; 217 do pr ← code_pointer_of_address 〈addrh, addrl〉; 218 return 〈st'', pr〉. 219 220 definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow. 221 match flow with 222 [ SProceed _ ⇒ False 223 | SInit _ _ _ _ _ ⇒ False 224 | _ ⇒ True 225 ]. 201 226 202 227 (* parameters that need full params to have type of functions, 203 but are still independent of serialization 204 Paolo: the first element returned by exec extended is None if flow is 205 left to regular sequential one, otherwise a label. 206 The address input is the address of the next statement, to be provided to 207 accomodate extensions that make calls. *) 228 but are still independent of serialization *) 208 229 record more_sem_genv_params (pp : params) : Type[1] ≝ 209 230 { msu_pars :> more_sem_unserialized_params pp 210 231 ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval) 211 ; exec_extended: ∀globals.genv globals pp → ext_instruction pp → 212 state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars)) 213 ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp → 214 state msu_pars → IO io_out io_in (trace × (state msu_pars)) 232 (* change of pc must be left to *_flow execution *) 233 ; exec_extended: ∀globals.genv globals pp → ext_step pp → 234 state msu_pars → 235 IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars)) 236 ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp → 237 state msu_pars → 238 IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars)) 215 239 ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars) 216 240 }. 217 218 241 219 242 (* parameters that are defined by serialization *) 220 243 record more_sem_params (pp : params) : Type[1] ≝ 221 244 { msg_pars :> more_sem_genv_params pp 222 ; succ_pc: succ pp → address → res address 223 ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code) 224 ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals) 245 ; offset_of_point : code_point pp → offset 246 ; point_of_offset : offset → option (code_point pp) 247 ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt 248 ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt) 225 249 }. 250 251 definition pointer_of_point : ∀p.more_sem_params p → 252 cpointer→ code_point p → cpointer ≝ 253 λp,msp,ptr,pt. 254 mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt). 255 [ elim ptr #ptr' #EQ <EQ @pok 256 | %] qed. 257 258 axiom BadOffsetForCodePoint : String. 259 260 definition point_of_pointer : 261 ∀p.more_sem_params p → cpointer → res (code_point p) ≝ 262 λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint) 263 (point_of_offset p msp (poff ptr)). 264 265 lemma point_of_pointer_of_point : 266 ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt. 267 #p #msp #ptr #pt normalize 268 >point_of_offset_of_point % 269 qed. 270 271 lemma pointer_of_point_block : 272 ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr. 273 / by refl/ 274 qed. 275 276 lemma pointer_of_point_uses_block : 277 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt. 278 #p #msp ** #ty1 #bl1 #H1 #o1 #EQ1 279 ** #ty2 #bl2 #H2 #o2 #EQ2 280 #pt #EQ3 destruct normalize // 281 qed. 282 283 lemma pointer_of_point_of_pointer : 284 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt. 285 pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt → 286 pointer_of_point p msp ptr2 pt = ptr1. 287 #p #msp ** #ty1 #bl1 #H1 #o1 #EQ1 288 ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ 289 destruct 290 lapply (offset_of_point_of_offset p msp o1) 291 normalize 292 elim (point_of_offset ???) normalize [* #ABS destruct(ABS)] 293 #pt' #EQ #EQ' destruct % 294 qed. 295 296 297 axiom ProgramCounterOutOfCode : String. 298 axiom PointNotFound : String. 299 axiom LabelNotFound : String. 300 301 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 302 genv globals p → cpointer → res (joint_statement p globals) ≝ 303 λp,msp,globals,ge,ptr. 304 ! pt ← point_of_pointer ? msp ptr ; 305 ! fn ← fetch_function … ge ptr ; 306 opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt). 307 308 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 309 genv globals p → cpointer → label → res cpointer ≝ 310 λp,msp,globals,ge,ptr,lbl. 311 ! fn ← fetch_function … ge ptr ; 312 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 313 (point_of_label … (joint_if_code … fn) lbl) ; 314 return pointer_of_point ? msp ptr pt. 315 316 definition succ_pc : ∀p : params.∀ msp : more_sem_params p. 317 cpointer → succ p → res cpointer ≝ 318 λp,msp,ptr,nxt. 319 ! curr ← point_of_pointer p msp ptr ; 320 return pointer_of_point p msp ptr (point_of_succ p curr nxt). 226 321 227 322 record sem_params : Type[1] ≝ … … 230 325 }. 231 326 232 definition address_of_label: ∀globals. ∀p:sem_params.327 (* definition address_of_label: ∀globals. ∀p:sem_params. 233 328 genv globals p → pointer → label → res address ≝ 234 329 λglobals,p,ge,ptr,l. 235 330 do newptr ← pointer_of_label … p ? ge … ptr l ; 236 OK … (address_of_code_pointer newptr). 331 OK … (address_of_code_pointer newptr). *) 237 332 238 333 definition goto: ∀globals. ∀p:sem_params. 239 genv globals p → label → state p → res (statep) ≝334 genv globals p → label → state_pc p → res (state_pc p) ≝ 240 335 λglobals,p,ge,l,st. 241 ! oldpc ← pointer_of_address (pc … st); 242 ! newpc ← address_of_label … ge oldpc l ; 243 OK (state p) (set_pc … newpc st). 336 ! newpc ← pointer_of_label ? p … ge (pc … st) l ; 337 return set_pc … newpc st. 244 338 245 339 (* … … 248 342 *) 249 343 250 definition next : ∀p:sem_params. succ … p → state p → res (statep) ≝344 definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝ 251 345 λp,l,st. 252 ! l' ← succ_pc … p l (pc … st);253 OK … (set_pc … l' st).346 ! nw ← succ_pc ? p … (pc ? st) l ; 347 return set_pc … nw st. 254 348 255 349 axiom MissingSymbol : String. 256 350 axiom FailedLoad : String. 257 351 axiom BadFunction : String. 258 259 definition eval_call_block: 352 axiom SuccessorNotProvided : String. 353 354 (* the optional point must be given only for calls *) 355 definition eval_step : 260 356 ∀globals.∀p:sem_params. genv globals p → state p → 261 block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝ 262 λglobals,p,ge,st,b,args,dest,ra. 263 ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ; 264 ! new_pc ← match next with 265 [ Some lbl ⇒ 266 let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in 267 address_of_label globals p ge pointer_in_fn lbl 268 | None ⇒ return ra 269 ] ; 270 let st ≝ set_pc … new_pc st in 271 return 〈tr, st〉. 272 % qed. 273 274 definition eval_call_id: 275 ∀globals.∀p:sem_params. genv globals p → state p → 276 ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝ 277 λglobals,p,ge,st,id,args,dest,ra. 278 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???; 279 eval_call_block … ge st b args dest ra. 280 281 282 (* defining because otherwise typechecker stalls *) 283 definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p → 284 ∀i : ident.member i (eq_identifier SymbolTag) globals 285 →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝ 286 λglobals,p,ge,st,ident,prf,ldest,hdest,l. 287 let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in 288 ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ; 289 ! st ← dpl_store … ldest laddr st; 290 ! st ← dph_store … hdest haddr st; 291 ! st ← next … p l st ; 292 return 〈E0, st〉. 293 [ cases addr // 294 | (* TODO: to prove *) 295 elim daemon 296 ] qed. 297 298 (* defining because otherwise typechecker stalls *) 299 definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p → 300 acc_a_reg p → succ p → res (trace × (state p)) ≝ 301 λglobals,p,ge,st,dst,l. 302 ! 〈st,v〉 ← pop p st; 303 ! st ← acca_store p p dst v st; 304 ! st ← next p l st ; 305 return 〈E0, st〉. 306 307 (* defining because otherwise typechecker stalls *) 308 definition eval_sequential : 309 ∀globals.∀p:sem_params. genv globals p → state p → 310 joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝ 311 λglobals,p,ge,st,seq,l. 357 joint_step p globals → 358 IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝ 359 λglobals,p,ge,st,seq. 312 360 match seq with 313 361 [ extension c ⇒ 314 ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ; 315 ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr; 316 ! st ← match next_pc with 317 [ None ⇒ next … p l st 318 | Some lbl ⇒ goto … ge lbl st 319 ] ; 320 return 〈tr, st〉 362 exec_extended … ge c st 321 363 | COST_LABEL cl ⇒ 322 ! st ← next … p l st ; 323 return 〈Echarge cl, st〉 364 return 〈Proceed ??, Echarge cl, st〉 324 365 | COMMENT c ⇒ 325 ! st ← next … p l st ; 326 return 〈E0, st〉 366 return 〈Proceed ??, E0, st〉 327 367 | LOAD dst addrl addrh ⇒ 328 368 ! vaddrh ← dph_arg_retrieve … st addrh ; … … 331 371 ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); 332 372 ! st ← acca_store p … dst v st ; 333 ! st ← next … p l st ; 334 return 〈E0, st〉 373 return 〈Proceed ??, E0, st〉 335 374 | STORE addrl addrh src ⇒ 336 375 ! vaddrh ← dph_arg_retrieve … st addrh; … … 339 378 ! v ← acca_arg_retrieve … st src; 340 379 ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); 341 let st ≝ set_m … m' st in 342 ! st ← next … p l st ; 343 return 〈E0, st〉 380 return 〈Proceed ??, E0, set_m … m' st〉 344 381 | COND src ltrue ⇒ 345 382 ! v ← acca_retrieve … st src; 346 383 ! b ← bool_of_beval v; 347 384 if b then 348 ! st ← goto … p ge ltrue st ; 349 return 〈E0, st〉 385 return 〈Redirect ?? ltrue, E0, st〉 350 386 else 351 ! st ← next … p l st ; 352 return 〈E0, st〉 387 return 〈Proceed ??, E0, st〉 353 388 | ADDRESS ident prf ldest hdest ⇒ 354 eval_address … ge st ident prf ldest hdest l 389 let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in 390 ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ; 391 ! st' ← dpl_store … ldest laddr st; 392 ! st'' ← dph_store … hdest haddr st'; 393 return 〈Proceed ??, E0, st''〉 355 394 | OP1 op dacc_a sacc_a ⇒ 356 395 ! v ← acca_retrieve … st sacc_a; … … 358 397 let v' ≝ BVByte (op1 eval op v) in 359 398 ! st ← acca_store … dacc_a v' st; 360 ! st ← next … l st ; 361 return 〈E0, st〉 399 return 〈Proceed ??, E0, st〉 362 400 | OP2 op dacc_a sacc_a src ⇒ 363 401 ! v1 ← acca_arg_retrieve … st sacc_a; … … 369 407 let v' ≝ BVByte v' in 370 408 let carry ≝ beval_of_bool carry in 371 ! st ← acca_store … dacc_a v' st; 372 let st ≝ set_carry … carry st in 373 ! st ← next … l st ; 374 return 〈E0, st〉 409 ! st' ← acca_store … dacc_a v' st; 410 let st'' ≝ set_carry … carry st' in 411 return 〈Proceed ??, E0, st''〉 375 412 | CLEAR_CARRY ⇒ 376 ! st ← next … l (set_carry … BVfalse st) ;377 return 〈 E0, st〉413 let st' ≝ set_carry … BVfalse st in 414 return 〈Proceed ??, E0, st'〉 378 415 | SET_CARRY ⇒ 379 ! st ← next … l (set_carry … BVtrue st) ;380 return 〈 E0, st〉416 let st' ≝ set_carry … BVtrue st in 417 return 〈Proceed ??, E0, st'〉 381 418 | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ 382 419 ! v1 ← acca_arg_retrieve … st sacc_a_reg; … … 387 424 let v1' ≝ BVByte v1' in 388 425 let v2' ≝ BVByte v2' in 389 ! st ← acca_store … dacc_a_reg v1' st; 390 ! st ← accb_store … dacc_b_reg v2' st; 391 ! st ← next … l st ; 392 return 〈E0, st〉 426 ! st' ← acca_store … dacc_a_reg v1' st; 427 ! st'' ← accb_store … dacc_b_reg v2' st'; 428 return 〈Proceed ??, E0, st''〉 393 429 | POP dst ⇒ 394 eval_pop … ge st dst l 430 ! 〈st',v〉 ← pop p st; 431 ! st'' ← acca_store p p dst v st'; 432 return 〈Proceed ??, E0, st''〉 395 433 | PUSH src ⇒ 396 434 ! v ← acca_arg_retrieve … st src; 397 435 ! st ← push … st v; 398 ! st ← next … l st ; 399 return 〈E0, st〉 436 return 〈Proceed ??, E0, st〉 400 437 | MOVE dst_src ⇒ 401 438 ! st ← pair_reg_move … st dst_src ; 402 ! st ← next … l st ; 403 return 〈E0, st〉 439 return 〈Proceed ??, E0, st〉 404 440 | CALL_ID id args dest ⇒ 405 ! ra ← succ_pc … p l (pc … st) : IO ???;406 eval_call_ id … ge st id args dest ra441 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???; 442 eval_call_block … ge st b args dest 407 443 ]. 444 [ cases addr // 445 | (* TODO: to prove *) 446 elim daemon 447 ] qed. 448 449 definition eval_step_flow : 450 ∀globals.∀p:sem_params.step_flow p globals → 451 succ p → stmt_flow p globals ≝ 452 λglobals,p,cmd,nxt. 453 match cmd with 454 [ Redirect l ⇒ SRedirect … l 455 | Init id fn args dest ⇒ SInit … id fn args dest nxt 456 | Proceed ⇒ SProceed … nxt 457 ]. 408 458 409 459 definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p → 410 state p → IO io_out io_in (trace × (state p)) ≝ 411 λglobals,p,ge,st. 412 ! s ← fetch_statement … ge st : IO ???; 413 match s return λ_.IO io_out io_in (trace × (state p)) with 414 [ GOTO l ⇒ 415 ! st ← goto … ge l st ; 416 return 〈E0, st〉 417 | RETURN ⇒ 460 state p → joint_statement … p globals → 461 IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝ 462 λglobals,p,ge,st,s. 463 match s with 464 [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉 465 | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉 466 | sequential seq l ⇒ 467 ! 〈flow, tr, st〉 ← eval_step … ge st seq ; 468 return 〈eval_step_flow … flow l, tr, st〉 469 | extension_fin c ⇒ 470 ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ; 471 return 〈pi1 … flow, tr, st〉 472 ]. 473 474 definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p → 475 state p → (Σs : joint_statement … p globals.no_seq … s) → 476 IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝ 477 λglobals,p,ge,st,s_sig. 478 match s_sig with 479 [ mk_Sig s s_prf ⇒ 480 match s return λx.no_seq p globals x → ? with 481 [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉 482 | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉 483 | sequential seq l ⇒ Ⓧ 484 | extension_fin c ⇒ λ_.exec_fin_extended … ge c st 485 ] s_prf 486 ]. % qed. 487 488 let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A) 489 (v2 : IO O I B) on v1 : Prop ≝ 490 match v1 with 491 [ Value x ⇒ 492 match v2 with 493 [ Value y ⇒ 494 P x y 495 | _ ⇒ False 496 ] 497 | Wrong _ ⇒ 498 match v2 with 499 [ Wrong _ ⇒ True 500 | _ ⇒ False 501 ] 502 | Interact o1 f1 ⇒ 503 match v2 with 504 [ Interact o2 f2 ⇒ 505 ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?) 506 | _ ⇒ False 507 ] 508 ]. <prf @i qed. 509 510 definition IORel ≝ λO,I. 511 mk_MonadRel (IOMonad O I) (IOMonad O I) 512 (rel_io O I) ???. 513 [// 514 |#X #Y #Z #W #relin #relout #m elim m 515 [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G 516 #f1 #f2 #G' whd %{(refl …)} #i 517 @(IH … (G i) f1 f2 G') 518 | #v * [#o #f * | #v' | #e *] 519 #Pvv' #f #g #H normalize @H @Pvv' 520 | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ % 521 ] 522 | #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] * 523 [1,4,7: #o' #f' [2,3: *] 524 normalize * #prf destruct(prf) normalize #G 525 % [%] normalize #i @IH @G 526 |2,5,8: #v' [1,3: *] 527 @H 528 |*: #e' [1,2: *] // 529 ] 530 ] 531 qed. 532 533 lemma IORel_refl : ∀O,I,X,rel.reflexive X rel → 534 reflexive ? (m_rel ?? (IORel O I) ?? rel). 535 #O #I #X #rel #H #m elim m 536 [ #o #f #IH whd %[%] #i normalize @IH 537 | #v @H 538 | #e % 539 ] 540 qed. 541 542 lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3. 543 (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) → 544 ∀m,n,o. 545 m_rel ?? (IORel O I) … rel1 m n → 546 m_rel ?? (IORel O I) … rel2 n o → 547 m_rel ?? (IORel O I) … rel3 m o. 548 #O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m 549 [ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ] 550 normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) // 551 | #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *] 552 @H 553 | #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] // 554 ] 555 qed. 556 557 lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2. 558 ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n → 559 ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) → 560 m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y). 561 #M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G 562 @(mr_bind … H) @G qed. 563 564 lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y. 565 m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x. 566 #M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq 567 qed. 568 569 lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2. 570 pi1 ?? s1 = s2 → 571 m_rel ?? (IORel ??) ?? 572 (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧ 573 \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y) 574 (eval_statement_no_seq globals p ge st s1) 575 (eval_statement globals p ge st s2). 576 #globals #p #ge #st * * [#s #n | #lbl || #c ]* 577 #s2 #EQ destruct(EQ) 578 whd in match eval_statement; 579 whd in match eval_statement_no_seq; 580 normalize nodelta 581 [1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/] 582 <(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?); 583 @(mr_bind … (IORel ??)) [@eq | @IORel_refl // | 584 #x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/ 585 qed. 586 587 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p → 588 state p → Z → joint_internal_function globals p → call_args p → 589 res (state_pc p) ≝ 590 λglobals,p,ge,st,id,fn,args. 591 ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 592 args st ; 593 let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in 594 let l' ≝ joint_if_entry … fn in 595 let st' ≝ set_regs p regs st in 596 let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in 597 let pc ≝ pointer_of_point ? p … pointer_in_fn l' in 598 return mk_state_pc ? st' pc. % qed. 599 600 definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p → 601 state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝ 602 λglobals,p,ge,st,flow. 603 match flow with 604 [ SRedirect l ⇒ goto … ge l st 605 | SProceed nxt ⇒ next ? nxt st 606 | SInit id fn args dest nxt ⇒ 607 ! ra ← succ_pc ? p … (pc … st) nxt ; 608 let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in 609 do_call ?? ge st' id fn args 610 | STailInit id fn args ⇒ 611 do_call … ge st id fn args 612 | SEnd ⇒ 613 ! 〈st,ra〉 ← fetch_ra … st ; 614 ! st' ← pop_frame … ge st; 615 return mk_state_pc ? st' ra 616 ]. 617 618 definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p → 619 state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) → 620 IO io_out io_in (state_pc p) ≝ 621 λglobals,p,ge,st,id,flow_sig. 622 match flow_sig with 623 [ mk_Sig flow prf ⇒ 624 match flow return λx.flow_no_seq p globals x → ? with 625 [ SRedirect l ⇒ λ_. 626 ! newpc ← pointer_of_label ? p … ge 627 (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ; 628 return mk_state_pc … st newpc 629 | STailInit id fn args ⇒ λ_. 630 do_call … ge st id fn args 631 | SEnd ⇒ λ_. 418 632 ! 〈st,ra〉 ← fetch_ra … st ; 419 ! st ← pop_frame … ge st; 420 return 〈E0,set_pc … ra st〉 421 | sequential seq l ⇒ eval_sequential … ge st seq l 422 | extension_fin c ⇒ exec_fin_extended … ge c st 423 ]. 633 ! st' ← pop_frame … ge st; 634 return mk_state_pc ? st' ra 635 | _ ⇒ Ⓧ 636 ] prf 637 ]. % qed. 638 639 lemma pointer_of_label_eq_with_id : 640 ∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl. 641 block_id (pblock ptr1) = block_id (pblock ptr2) → 642 pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl. 643 #g #p #ge 644 ** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct 645 ** #ty2 * #r2 #id2 #H2 inversion H2 646 [1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct % 647 qed. 648 649 650 lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p. 651 ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2. 652 pi1 … s1 = s2 → block_id (pblock (pc … st)) = id → 653 (eval_stmt_flow_no_seq g p ge st id s1) = 654 (eval_stmt_flow g p ge st s2). 655 #g#p#ge#st#id' 656 **[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]* 657 #s2 #EQ #EQ' destruct(EQ) 658 whd in match eval_stmt_flow_no_seq; normalize nodelta 659 whd in match eval_stmt_flow; normalize nodelta 660 [2,3: %] 661 whd in match goto; normalize nodelta 662 whd in match set_pc; normalize nodelta 663 >pointer_of_label_eq_with_id [% | >EQ' % |] 664 qed. 665 666 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p → 667 state_pc p → IO io_out io_in (trace × (state_pc p)) ≝ 668 λglobals,p,ge,st. 669 ! s ← fetch_statement ? p … ge (pc … st) : IO ???; 670 ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s; 671 let st ≝ set_no_pc … st_npc st in 672 ! st ← eval_stmt_flow … ge st flow; 673 return 〈tr, st〉. 424 674 425 675 definition is_final: ∀globals:list ident. ∀p: sem_params. 426 genv globals p → address → statep → option int ≝676 genv globals p → cpointer → state_pc p → option int ≝ 427 677 λglobals,p,ge,exit,st.res_to_opt ? ( 428 do s ← fetch_statement … ge st;678 do s ← fetch_statement ? p … ge (pc … st); 429 679 match s with 430 680 [ RETURN ⇒ 431 681 do 〈st,ra〉 ← fetch_ra … st; 432 if eq_ addressra exit then682 if eq_pointer ra exit then 433 683 do vals ← read_result … ge st ; 434 684 Word_of_list_beval vals … … 436 686 Error ? [ ] 437 687 | _ ⇒ Error ? [ ]]). 438 688 439 689 record evaluation_parameters : Type[1] ≝ 440 690 { globals: list ident 441 691 ; sparams:> sem_params 442 ; exit: address692 ; exit: cpointer 443 693 ; genv2: genv globals sparams 444 694 }. 445 695 446 696 definition joint_exec: trans_system io_out io_in ≝ 447 mk_trans_system … evaluation_parameters (λG. state G)697 mk_trans_system … evaluation_parameters (λG. state_pc G) 448 698 (λG.is_final (globals G) G (genv2 G) (exit G)) 449 (λG.eval_state ment(globals G) G (genv2 G)).699 (λG.eval_state (globals G) G (genv2 G)). 450 700 451 701 definition make_global : … … 457 707 let b ≝ mk_block Code (-1) in 458 708 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in 459 let addr ≝ address_of_code_pointer ptr in460 709 (λp. mk_evaluation_parameters 461 710 (prog_var_names … p) 462 711 (mk_sem_params … pars) 463 addr712 ptr 464 713 (globalenv Genv … p) 465 714 ). … … 470 719 definition make_initial_state : 471 720 ∀pars: sem_params. 472 ∀p: joint_program … pars. res (state pars) ≝721 ∀p: joint_program … pars. res (state_pc pars) ≝ 473 722 λpars,p. 474 723 let sem_globals ≝ make_global pars p in … … 480 729 let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in 481 730 let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in 482 do sp ← address_of_pointer spp ;483 731 let main ≝ prog_main … p in 484 let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in 485 let trace_state ≝ 486 eval_call_id … pars ge st0 main (call_args_for_main … pars) 487 (call_dest_for_main … pars) (exit sem_globals) in 488 match trace_state with 489 [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *) 490 | Wrong msg ⇒ Error … msg 491 | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) 492 ]. 493 [3: % | cases ispb | cases spb] * #r #off #E >E % 732 let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in 733 (* use exit sem_globals as ra and call_dest_for_main as dest *) 734 let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in 735 let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in 736 ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ; 737 ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ; 738 match main_fd with 739 [ Internal fn ⇒ 740 do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars) 741 | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) 742 ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try // 494 743 qed. 495 744
Note: See TracChangeset
for help on using the changeset viewer.