Changeset 2200 for src/joint/semanticsUtils_paolo.ma
 Timestamp:
 Jul 17, 2012, 6:00:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils_paolo.ma
r1882 r2200 1 1 include "joint/semantics_paolo.ma". 2 2 include alias "common/Identifiers.ma". 3 include "utilities/hide.ma". 3 4 4 5 (*** Store/retrieve on pseudoregisters ***) … … 21 22 (******************************** GRAPHS **************************************) 22 23 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. 24 definition bitvector_from_pos : 25 ∀n.Pos → BitVector n ≝ 26 λn,p.bitvector_of_Z n (Zpred (pos p)). 28 27 29 definition graph_label_of_pointer: pointer → res label ≝ 30 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one  pos x ⇒ x  neg x ⇒ x ])). 28 definition pos_from_bitvector : 29 ∀n.BitVector n → Pos ≝ 30 λn,v. 31 match Zsucc (Z_of_unsigned_bitvector n v) 32 return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ? 33 with 34 [ OZ ⇒ λprf.⊥ 35  pos x ⇒ λ_. x 36  neg x ⇒ λprf.⊥ 37 ] (refl …). 38 @hide_prf 39 elim v in prf; 40 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed. 31 41 32 definition graph_fetch_statement: 33 ∀pars : graph_params. 34 ∀sem_pars : sem_state_params. 35 ∀globals. 36 genv globals pars → 37 cpointer → 38 res (joint_statement pars globals) ≝ 39 λpars,sem_pars,globals,ge,p. 40 do f ← fetch_function … ge p ; 41 do l ← graph_label_of_pointer p; 42 opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). 42 lemma pos_pos_from_bitvector : 43 ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv). 44 #n #bv elim bv n 45 [ % 46  #n * #bv #IH [ %  @IH ] 47 ] 48 qed. 49 50 lemma bitvector_from_pos_from_bitvector : 51 ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv. 52 #n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector 53 >Zpred_Zsucc // 54 qed. 55 56 lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos. 57 (∀q,r. 58 ppos m = natp_plus (natp_times q (ppos n)) r → 59 natp_lt r n → 60 P (〈q,r〉)) → 61 P (divide m n). 62 #P #m #n #H 63 lapply (refl … (divide m n)) 64 cases (divide ??) in ⊢ (???%→%); 65 #q #r #EQ elim (divide_ok … EQ) EQ @H 66 qed. 67 68 lemma lt_divisor_to_eq_mod : ∀p,q : Pos. 69 p < q → \snd (divide p q) = ppos p. 70 #p #q #H @divide_elim * [2: #quot ] 71 * [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %] 72 @⊥ elim (lt_to_not_le ?? H) #H @H H H 73 [ @(transitive_le … (quot*q)) ] /2 by / 74 qed. 75 76 lemma pos_from_bitvector_from_pos : 77 ∀n,p. 78 p ≤ two_power_nat n → 79 pos_from_bitvector n (bitvector_from_pos n p) = p. 80 #n #p #H 81 cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p) 82 [2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ] 83 >pos_pos_from_bitvector 84 whd in match (bitvector_from_pos ??); 85 >Z_of_unsigned_bitvector_of_Z 86 cases p in H ⊢ %; 87 [ #_ % 88 *: #p' #H 89 whd in match (Zpred ?); 90 whd in match (Z_two_power_nat ?); 91 whd in ⊢ (??(?%)?); 92 >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ] 93 whd 94 <succ_pred_n try assumption % #ABS destruct(ABS) 95 ] 96 qed. 97 98 lemma pos_from_bitvector_max : ∀n,bv. 99 pos_from_bitvector n bv ≤ two_power_nat n. 100 #n #bv 101 change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n) 102 >pos_pos_from_bitvector 103 @Zlt_to_Zle 104 @bv_Z_unsigned_max 105 qed. 106 107 definition graph_offset_of_label : label → option offset ≝ 108 λl.let p ≝ word_of_identifier … l in 109 if leb p (two_power_nat offset_size) then 110 return mk_offset (bitvector_from_pos … p) 111 else 112 None ?. 113 114 definition graph_label_of_offset: offset → label ≝ 115 λo.an_identifier ? (pos_from_bitvector ? (offv o)). 43 116 44 117 definition make_sem_graph_params : … … 52 125 pars 53 126 g_pars 54 graph_ pointer_of_label55 (λ_.λ_.graph_pointer_of_label)56 (graph_fetch_statement ? g_pars)127 graph_offset_of_label 128 graph_label_of_offset 129 ?? 57 130 ). 58 131 whd in match graph_label_of_offset; 132 whd in match graph_offset_of_label; 133 whd in match word_of_identifier; 134 normalize nodelta * #x 135 @(leb_elim ? (two_power_nat ?)) normalize nodelta 136 [ #_ >bitvector_from_pos_from_bitvector % 137  #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max 138  #H whd >(pos_from_bitvector_from_pos … H) % 139  #_ % 140 ] 141 qed. 142 59 143 (******************************** LINEAR **************************************) 60 check mk_pointer61 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.64 144 65 axiom BadLabel: String. 145 definition lin_offset_of_nat : ℕ → option offset ≝ 146 λn. 147 if leb (S n) (2^offset_size) then 148 return mk_offset (bitvector_of_nat ? n) 149 else 150 None ?. 66 151 67 definition lin_pointer_of_label: 68 ∀pars : lin_params. 69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝ 70 λpars,globals,ge,old,l. 71 do fn ← fetch_function … ge old ; 72 do pos ← 73 opt_to_res ? [MSG BadLabel] 74 (position_of ? 75 (λs. let 〈l',x〉 ≝ s in 76 match l' with [ None ⇒ false  Some l'' ⇒ if eq_identifier … l l'' then true else false]) 77 (joint_if_code … pars fn)) ; 78 OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). 79 % qed. 152 definition lin_nat_of_offset : offset → ℕ ≝ 153 λo.nat_of_bitvector ? (offv o). 80 154 81 definition lin_fetch_statement:82 ∀pars : lin_params.83 ∀sem_pars : sem_state_params.84 ∀globals.85 genv globals pars → cpointer → res (joint_statement pars globals) ≝86 λpars,sem_pars,globals,ge,ppc.87 do fn ← fetch_function … ge ppc ;88 let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)89 do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;90 return (\snd found).91 155 92 156 definition make_sem_lin_params : … … 100 164 pars 101 165 g_pars 102 lin_ succ_p103 (lin_pointer_of_label ?)104 (lin_fetch_statement ? g_pars)166 lin_offset_of_nat 167 lin_nat_of_offset 168 ?? 105 169 ). 106 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 170 [ * ] #x 171 whd in match lin_offset_of_nat; 172 whd in match lin_nat_of_offset; 173 normalize nodelta 174 @leb_elim normalize nodelta #H 175 [ >bitvector_of_nat_inverse_nat_of_bitvector % 176  @⊥ cases H #H @H H H // 177  whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) % 178  % 174 179 ] 175 180 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 b179 [ //180  #f #IH #H @bnew_proper181 #x @IH182 ]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 with196 [ nil ⇒ Skip ??197  cons hd tl ⇒198 If step_unbranching … hd then with prf do199 Cons ?? hd (step_list_to_s_block ?? tl)200 else with prf do201 FinStep ?? hd202 ]. [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 → Prop209 ; genv_rel : genv globals p1 → genv globals p2 → Prop210 ; pc_rel : cpointer → cpointer → Prop211 ; st_rel : state p1 → state p2 → Prop212 ; stmt_rel : joint_statement p1 globals → Block213 (* 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 → ? with221 [ 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 H228 lapply (pointer_compat_from_ind … H) H cases b * #z * #H229 %{«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 R238 (safe_address_of_xdata_pointer (sp … st1))239 (safe_address_of_xdata_pointer (sp … st2)) ∧240 isp_rel p1 p2 R241 (safe_address_of_xdata_pointer (isp … st1))242 (safe_address_of_xdata_pointer (isp … st2)) ∧243 sp_rel p1 p2 R244 (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_isp1250 elim st2 st2 #st2 ** #good_pc2 #good_sp2 #good_isp2251 assumption252 qed.253 elim st2254 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
Note: See TracChangeset
for help on using the changeset viewer.