Changeset 2286 for src/joint/SemanticUtils.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/SemanticUtils.ma
r2176 r2286 1 1 include "joint/semantics.ma". 2 2 include alias "common/Identifiers.ma". 3 include "utilities/hide.ma". 4 include "ASM/BitVectorTrie.ma". 5 6 record hw_register_env : Type[0] ≝ 7 { reg_env : BitVectorTrie beval 6 8 ; carry_bit : bebit 9 ; other_bit : bebit 10 }. 11 12 definition empty_hw_register_env: hw_register_env ≝ 13 mk_hw_register_env (Stub …) BBundef BBundef. 14 15 include alias "ASM/BitVectorTrie.ma". 16 17 definition hwreg_retrieve: hw_register_env → Register → beval ≝ 18 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef. 19 20 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ 21 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env)) 22 (carry_bit env) (other_bit env). 23 24 definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝ 25 λv,env.mk_hw_register_env (reg_env env) v (other_bit env). 26 27 definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝ 28 λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v. 29 3 30 4 31 (*** Store/retrieve on pseudoregisters ***) 32 include alias "common/Identifiers.ma". 5 33 6 34 axiom BadRegister : String. … … 13 41 (*** Store/retrieve on hardware registers ***) 14 42 15 definition init_hw_register_env: address → hw_register_env ≝ 16 λaddr. 17 let 〈dpl,dph〉 ≝ addr in 43 definition init_hw_register_env: xpointer → hw_register_env ≝ 44 λsp. 45 let 〈dpl,dph〉 ≝ 46 match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with 47 [ OK p ⇒ λ_.p 48  _ ⇒ λprf.⊥ 49 ] (refl …) in 18 50 let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in 19 51 hwreg_store RegisterDPL dpl env. 20 21 (****************************************************************************) 22 23 definition graph_pointer_of_label0: 24 pointer → label → Σp:pointer. ptype p = Code ≝ 25 λoldpc,l. 26 mk_pointer 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 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝ 32 λ_.λ_.λ_.λoldpc,l. 33 OK ? (graph_pointer_of_label0 oldpc l). 34 35 definition graph_label_of_pointer: pointer → res label ≝ 36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one  pos x ⇒ x  neg x ⇒ x ])). 37 38 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. 39 But I can't use it directly because this one uses a concrete definition of 40 pointer_of_label and it is used to istantiate the more_sem_params record 41 where the abstract version is declared as a field. Is there a better way 42 to organize the code? *) 43 definition graph_succ_p: label → address → res address ≝ 44 λl,old. 45 do ptr ← pointer_of_address old ; 46 let newptr ≝ graph_pointer_of_label0 ptr l in 47 address_of_pointer newptr. 48 49 axiom BadProgramCounter: String. 50 51 definition graph_fetch_function: 52 ∀params1,sem_params,globals. 53 genv … (graph_params params1 globals) → 54 state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝ 55 λparams1,sem_params,globals,ge,st. 56 do p ← code_pointer_of_address (pc … st) ; 57 let b ≝ pblock p in 58 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; 59 match def with 60 [ Internal def' ⇒ OK … def' 61  External _ ⇒ Error … [MSG BadProgramCounter]]. 62 63 definition graph_fetch_statement: 64 ∀params1,sem_params,globals. 65 genv … (graph_params params1 globals) → 66 state sem_params → res (joint_statement (graph_params_ params1) globals) ≝ 67 λparams1,sem_params,globals,ge,st. 68 do p ← code_pointer_of_address (pc … st) ; 69 do f ← graph_fetch_function … ge st ; 70 do l ← graph_label_of_pointer p; 71 opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). 52 @hide_prf 53 normalize in prf; destruct(prf) 54 qed. 55 56 (******************************** GRAPHS **************************************) 57 58 definition bitvector_from_pos : 59 ∀n.Pos → BitVector n ≝ 60 λn,p.bitvector_of_Z n (Zpred (pos p)). 61 62 definition pos_from_bitvector : 63 ∀n.BitVector n → Pos ≝ 64 λn,v. 65 match Zsucc (Z_of_unsigned_bitvector n v) 66 return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ? 67 with 68 [ OZ ⇒ λprf.⊥ 69  pos x ⇒ λ_. x 70  neg x ⇒ λprf.⊥ 71 ] (refl …). 72 @hide_prf 73 elim v in prf; 74 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed. 75 76 lemma pos_pos_from_bitvector : 77 ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv). 78 #n #bv elim bv n 79 [ % 80  #n * #bv #IH [ %  @IH ] 81 ] 82 qed. 83 84 lemma bitvector_from_pos_from_bitvector : 85 ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv. 86 #n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector 87 >Zpred_Zsucc // 88 qed. 89 90 lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos. 91 (∀q,r. 92 ppos m = natp_plus (natp_times q (ppos n)) r → 93 natp_lt r n → 94 P (〈q,r〉)) → 95 P (divide m n). 96 #P #m #n #H 97 lapply (refl … (divide m n)) 98 cases (divide ??) in ⊢ (???%→%); 99 #q #r #EQ elim (divide_ok … EQ) EQ @H 100 qed. 101 102 lemma lt_divisor_to_eq_mod : ∀p,q : Pos. 103 p < q → \snd (divide p q) = ppos p. 104 #p #q #H @divide_elim * [2: #quot ] 105 * [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %] 106 @⊥ elim (lt_to_not_le ?? H) #H @H H H 107 [ @(transitive_le … (quot*q)) ] /2 by / 108 qed. 109 110 lemma pos_from_bitvector_from_pos : 111 ∀n,p. 112 p ≤ two_power_nat n → 113 pos_from_bitvector n (bitvector_from_pos n p) = p. 114 #n #p #H 115 cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p) 116 [2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ] 117 >pos_pos_from_bitvector 118 whd in match (bitvector_from_pos ??); 119 >Z_of_unsigned_bitvector_of_Z 120 cases p in H ⊢ %; 121 [ #_ % 122 *: #p' #H 123 whd in match (Zpred ?); 124 whd in match (Z_two_power_nat ?); 125 whd in ⊢ (??(?%)?); 126 >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ] 127 whd 128 <succ_pred_n try assumption % #ABS destruct(ABS) 129 ] 130 qed. 131 132 lemma pos_from_bitvector_max : ∀n,bv. 133 pos_from_bitvector n bv ≤ two_power_nat n. 134 #n #bv 135 change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n) 136 >pos_pos_from_bitvector 137 @Zlt_to_Zle 138 @bv_Z_unsigned_max 139 qed. 140 141 definition graph_offset_of_label : label → option offset ≝ 142 λl.let p ≝ word_of_identifier … l in 143 if leb p (two_power_nat offset_size) then 144 return mk_offset (bitvector_from_pos … p) 145 else 146 None ?. 147 148 definition graph_label_of_offset: offset → label ≝ 149 λo.an_identifier ? (pos_from_bitvector ? (offv o)). 150 151 definition make_sem_graph_params : 152 ∀pars : graph_params. 153 ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars). 154 sem_params ≝ 155 λpars,g_pars. 156 mk_sem_params 157 pars 158 (mk_more_sem_params 159 pars 160 g_pars 161 graph_offset_of_label 162 graph_label_of_offset 163 ?? 164 ). 165 whd in match graph_label_of_offset; 166 whd in match graph_offset_of_label; 167 whd in match word_of_identifier; 168 normalize nodelta * #x 169 @(leb_elim ? (two_power_nat ?)) normalize nodelta 170 [ #_ >bitvector_from_pos_from_bitvector % 171  #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max 172  #H whd >(pos_from_bitvector_from_pos … H) % 173  #_ % 174 ] 175 qed. 176 177 (******************************** LINEAR **************************************) 178 179 definition lin_offset_of_nat : ℕ → option offset ≝ 180 λn. 181 if leb (S n) (2^offset_size) then 182 return mk_offset (bitvector_of_nat ? n) 183 else 184 None ?. 185 186 definition lin_nat_of_offset : offset → ℕ ≝ 187 λo.nat_of_bitvector ? (offv o). 188 189 190 definition make_sem_lin_params : 191 ∀pars : lin_params. 192 ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars). 193 sem_params ≝ 194 λpars,g_pars. 195 mk_sem_params 196 pars 197 (mk_more_sem_params 198 pars 199 g_pars 200 lin_offset_of_nat 201 lin_nat_of_offset 202 ?? 203 ). 204 [ * ] #x 205 whd in match lin_offset_of_nat; 206 whd in match lin_nat_of_offset; 207 normalize nodelta 208 @leb_elim normalize nodelta #H 209 [ >bitvector_of_nat_inverse_nat_of_bitvector % 210  @⊥ cases H #H @H H H // 211  whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) % 212  % 213 ] 214 qed.
Note: See TracChangeset
for help on using the changeset viewer.