Changeset 2200
 Timestamp:
 Jul 17, 2012, 6:00:03 PM (7 years ago)
 Location:
 src
 Files:

 1 added
 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorZ.ma
r1516 r2200 3 3 include "ASM/BitVector.ma". 4 4 include "ASM/Arithmetic.ma". 5 include "utilities/binary/division.ma". 5 6 6 7 let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝ … … 124 125 theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n. 125 126 #n #bv normalize 126 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 /127 lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2 by pos_length_lt/ 127 128 qed. 128 129 … … 150 151  #t whd in ⊢ (?%?); // 151 152 ] qed. 153 154 (* TODO *) 155 axiom Z_of_unsigned_bitvector_of_Z : 156 ∀n,z. 157 Z_of_unsigned_bitvector n (bitvector_of_Z n z) = 158 modZ z (Z_two_power_nat n). 159 160 axiom bitvector_of_Z_of_unsigned_bitvector : 161 ∀n,bv. 162 bitvector_of_Z n (Z_of_unsigned_bitvector n bv) = bv. 
src/joint/linearise.ma
r2182 r2200 1 1 include "joint/TranslateUtils_paolo.ma". 2 include "utilities/hide.ma". 2 3 3 4 definition graph_to_lin_statement : … … 15 16 #p#globals * [//] * // 16 17 qed. 17 18 definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.19 definition hide_Prop : Prop → Prop ≝ λP.P.20 21 interpretation "hide proof" 'hide p = (hide_prf ? p).22 interpretation "hide Prop" 'hide p = (hide_Prop p).23 18 24 19 (* discard all elements passing test, return first element failing it *) 
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 
src/joint/semantics_paolo.ma
r2186 r2200 308 308 record more_sem_params (pp : params) : Type[1] ≝ 309 309 { msg_pars :> more_sem_genv_params pp 310 ; offset_of_point : code_point pp → offset 311 ; point_of_offset : offset → option (code_point pp) 312 ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt 313 ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt) 310 ; offset_of_point : code_point pp → option offset (* can overflow *) 311 ; point_of_offset : offset → code_point pp 312 ; point_of_offset_of_point : 313 ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt)) 314 ; offset_of_point_of_offset : 315 ∀o.offset_of_point (point_of_offset o) = Some ? o 314 316 }. 315 317 318 axiom CodePointerOverflow : String. 319 316 320 definition pointer_of_point : ∀p.more_sem_params p → 317 cpointer→ code_point p → cpointer ≝321 cpointer→ code_point p → res cpointer ≝ 318 322 λp,msp,ptr,pt. 319 mk_pointer (pblock ptr) (offset_of_point p msp pt). 323 ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ; 324 return «mk_pointer (pblock ptr) o, ?». 320 325 elim ptr #ptr' #EQ <EQ % qed. 321 326 322 axiom BadOffsetForCodePoint : String.323 324 327 definition point_of_pointer : 325 ∀p.more_sem_params p → cpointer → res (code_point p) ≝ 326 λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint) 327 (point_of_offset p msp (poff ptr)). 328 ∀p.more_sem_params p → cpointer → code_point p ≝ 329 λp,msp,ptr.point_of_offset p msp (poff ptr). 328 330 329 331 lemma point_of_pointer_of_point : 330 ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt. 331 #p #msp #ptr #pt normalize 332 >point_of_offset_of_point % 332 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt. 333 pointer_of_point p msp ptr1 pt = return ptr2 → 334 point_of_pointer p msp ptr2 = pt. 335 #p #msp #ptr1 #ptr2 #pt normalize 336 lapply (point_of_offset_of_point p msp pt) 337 cases (offset_of_point ???) normalize 338 [ * #ABS destruct(ABS) 339  #o #EQ1 #EQ2 destruct % 340 ] 333 341 qed. 334 342 335 343 lemma pointer_of_point_block : 336 ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr. 337 / by refl/ 344 ∀p,msp,ptr1,ptr2,pt. 345 pointer_of_point p msp ptr1 pt = return ptr2 → 346 pblock ptr2 = pblock ptr1. 347 #p #msp #ptr1 #ptr2 #pt normalize 348 cases (offset_of_point ???) normalize 349 [ #ABS destruct(ABS) 350  #o #EQ destruct(EQ) % 351 ] 338 352 qed. 339 353 … … 346 360 347 361 lemma pointer_of_point_of_pointer : 348 ∀p,msp.∀ptr1,ptr2 : cpointer. ∀pt.349 pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →350 pointer_of_point p msp ptr 2 pt = ptr1.362 ∀p,msp.∀ptr1,ptr2 : cpointer. 363 pblock ptr1 = pblock ptr2 → 364 pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2. 351 365 #p #msp ** #b1 #o1 #EQ1 352 366 ** #b2 #o2 #EQ2 353 #pt #EQ3 354 destruct 355 lapply (offset_of_point_of_offset p msp o1) 356 normalize 357 elim (point_of_offset ???) normalize [* #ABS destruct(ABS)] 358 #pt' #EQ #EQ' destruct % 367 #EQ3 destruct 368 normalize >offset_of_point_of_offset normalize % 359 369 qed. 360 361 370 362 371 axiom ProgramCounterOutOfCode : String. … … 367 376 genv globals p → cpointer → res (joint_statement p globals) ≝ 368 377 λp,msp,globals,ge,ptr. 369 ! pt ← point_of_pointer ? msp ptr ;378 let pt ≝ point_of_pointer ? msp ptr in 370 379 ! fn ← fetch_function … ge ptr ; 371 380 opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt). … … 377 386 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 378 387 (point_of_label … (joint_if_code … fn) lbl) ; 379 return (mk_pointer(mk_block Code (block_id (pblock ptr))) 380 (offset_of_point p msp pt) : Σp.?). // qed. 388 pointer_of_point p msp ptr pt. 381 389 382 390 definition succ_pc : ∀p : params.∀ msp : more_sem_params p. 383 391 cpointer → succ p → res cpointer ≝ 384 392 λp,msp,ptr,nxt. 385 ! curr ← point_of_pointer p msp ptr ;386 return pointer_of_point p msp ptr (point_of_succ p curr nxt).393 let curr ≝ point_of_pointer p msp ptr in 394 pointer_of_point p msp ptr (point_of_succ p curr nxt). 387 395 388 396 record sem_params : Type[1] ≝ … … 564 572 let st' ≝ set_regs p regs st in 565 573 let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in 566 let pc ≝ pointer_of_point ? p … pointer_in_fn l' in574 ! pc ← pointer_of_point ? p … pointer_in_fn l' ; 567 575 return mk_state_pc ? st' pc. % qed. 568 576
Note: See TracChangeset
for help on using the changeset viewer.