Changeset 2462
 Timestamp:
 Nov 14, 2012, 10:31:55 AM (8 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/common/BackEndOps.ma
r2435 r2462 136 136 the arguments (columns marked by 1st argument, rows by 2nd). Further 137 137 checks for definedness are done for pointer parts taking into account 138 blocks, parts and the carry value. TODO update table 138 blocks, parts and the carry value. 139 Neither BVundef nor BVpc allow any operations 139 140 arg2\arg1  BVByte  BVptr (D)  BVptr (C)  BVnull  BVXor  BVnonzero  140 141 +++++++ 
src/common/ByteValues.ma
r2443 r2462 5 5 include "common/Pointers.ma". 6 6 include "utilities/hide.ma". 7 8 definition cpointer ≝ Σp.ptype p = Code. 9 definition xpointer ≝ Σp.ptype p = XData. 10 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). 11 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). 7 12 8 13 record part (*r: region*): Type[0] ≝ … … 37 42  BVByte: Byte → beval 38 43  BVnull: (*∀r:region.*) part → beval 39  BVptr: pointer → part → beval. 44  BVptr: pointer → part → beval 45  BVpc: cpointer → part → beval. (* only used in back end, needed to separate 46 program counters that go in the stack from 47 function pointers, as they are linked with 48 different relations in some passes *) 40 49 41 50 definition eq_bv_suffix : ∀n,m,p. … … 80 89 ]. 81 90 91 definition pc_of_bevals: list beval → res cpointer ≝ 92 λl. 93 match l with 94 [ nil ⇒ Error … [MSG CorruptedPointer] 95  cons bv1 tl ⇒ 96 match tl with 97 [ nil ⇒ Error … [MSG CorruptedPointer] 98  cons bv2 tl' ⇒ 99 match tl' with 100 [ cons _ _ ⇒ Error … [MSG CorruptedPointer] 101  nil ⇒ 102 match bv1 with 103 [ BVpc ptr1 p1 ⇒ 104 match bv2 with 105 [ BVpc ptr2 p2 ⇒ 106 if eqb p1 0 ∧ eqb p2 1 ∧ eq_pointer ptr1 ptr2 then 107 return ptr2 108 else Error … [MSG CorruptedPointer] 109  _ ⇒ Error … [MSG CorruptedPointer] 110 ] 111  _ ⇒ Error … [MSG CorruptedPointer] 112 ] 113 ] 114 ] 115 ]. 116 82 117 definition bevals_of_pointer ≝ 83 118 λp:pointer. 84 119 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer). 120 121 definition bevals_of_pc ≝ 122 λp:cpointer. 123 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer). 85 124 86 125 lemma pointer_of_bevals_bevals_of_pointer: … … 92 131 change with (eq_bv ???) in match (eq_bv_suffix ?????); 93 132 >eq_bv_refl % 133 qed. 134 135 lemma pc_of_bevals_bevals_of_pc: 136 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p. 137 #ptr 138 whd in match (bevals_of_pc ?); 139 whd in ⊢ (??%?); 140 >reflexive_eq_pointer 141 % 94 142 qed. 95 143 … … 114 162  _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*) 115 163 116 definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝ 117 λp. list_to_pair ? (bevals_of_pointer p) (refl …). 118 (* 119 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒ 120 match pty return λpty. ? → pty = Code → ? with 121 [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ? 122  _ ⇒ λpok'.λabs. ⊥] pok] ?. 123 [@(pi2 … p) 7: // 8: %] destruct (abs)*) 124 125 axiom NotACodePointer: String. 164 definition beval_pair_of_pc: cpointer → beval × beval ≝ 165 λp. list_to_pair ? (bevals_of_pc p) (refl …). 166 167 (* axiom NotACodePointer: String. 126 168 definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝ 127 169 λp. … … 130 172 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with 131 173 [ Code ⇒ λE.OK ? (mk_Sig … p E) 132  _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). 174  _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *) 133 175 134 176 axiom ValueNotABoolean: String. … … 142 184 series of XORs has been 143 185 completed *) 186  BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *) 144 187  BVByte b ⇒ OK … (eq_bv … (zero …) b) 145 188  BVnull _ ⇒ OK … false 
src/joint/Joint.ma
r2457 r2462 410 410 λp,globals. 411 411 Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def). 412 413 unification hint 0 ≔ p,g ⊢ 414 joint_closed_internal_function p g ≡ 415 Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)). 412 416 413 417 definition set_joint_code ≝ 
src/joint/semantics.ma
r2457 r2462 73 73 ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝ 74 74 λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?. 75 definition cpointer ≝ Σp.ptype p = Code.76 definition xpointer ≝ Σp.ptype p = XData.77 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).78 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).79 unification hint 0 ≔ p,g ⊢80 joint_closed_internal_function p g ≡81 Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).82 75 83 76 record sem_state_params : Type[1] ≝ … … 239 232 qed. 240 233 234 (* bevals hold a function pointer (BVptr) *) 241 235 definition funct_of_bevals : ∀F,globals,ge. 242 236 beval → beval → option (Σi.is_function F globals ge i) ≝ 243 237 λF,globals,ge,dpl,dph. 244 238 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 245 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ 239 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *) 246 240 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 247 241 funct_of_block … (pblock ptr) … … 370 364 definition save_ra : ∀p. state p → cpointer → res (state p) ≝ 371 365 λp,st,l. 372 let 〈addrl,addrh〉 ≝ beval_pair_of_p ointerl in366 let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in 373 367 ! st' ← push … st addrl; 374 368 push … st' addrh. … … 376 370 definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝ 377 371 λp,st. 378 do 〈addrh, st'〉 ← pop … st; 379 do 〈addrl, st''〉 ← pop … st'; 380 do pr ← pointer_of_address 〈addrh, addrl〉; 381 match ptype pr return λx.ptype pr = x → res (cpointer × ?) with 382 [ Code ⇒ λprf.return 〈«pr,prf», st''〉 383  _ ⇒ λ_.Error … [MSG BadPointer] 384 ] (refl …). 372 ! 〈addrh, st'〉 ← pop … st; 373 ! 〈addrl, st''〉 ← pop … st'; 374 ! pr ← pc_of_bevals [addrh; addrl]; 375 return 〈pr, st''〉. 385 376 386 377 (* parameters that are defined by serialization *)
Note: See TracChangeset
for help on using the changeset viewer.