Changeset 1280 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Sep 28, 2011, 2:43:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1239 r1280 4 4 include "common/FrontEndOps.ma". 5 5 include "common/Graphs.ma". 6 7 definition add_graph ≝ 8 λl: label. 9 λstmt. 10 λp. 11 let rtl_if_luniverse' ≝ rtl_if_luniverse p in 12 let rtl_if_runiverse' ≝ rtl_if_runiverse p in 13 let rtl_if_result' ≝ rtl_if_result p in 14 let rtl_if_params' ≝ rtl_if_params p in 15 let rtl_if_locals' ≝ rtl_if_locals p in 16 let rtl_if_stacksize' ≝ rtl_if_stacksize p in 17 let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in 18 let rtl_if_entry' ≝ rtl_if_entry p in 19 let rtl_if_exit' ≝ rtl_if_exit p in 20 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' 21 rtl_if_params' rtl_if_params' rtl_if_locals' 22 rtl_if_stacksize' rtl_if_graph' ? ?. 23 [1: cases(rtl_if_entry') 24 #LABEL #HYP % 25 [1: @LABEL 26 2: cases(HYP) 27 generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l); 28 normalize nodelta; 29 /2/ 30 ] 31 2: cases(rtl_if_exit') 32 #LABEL #HYP % 33 [1: @LABEL 34 2: cases(HYP) 35 generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l); 36 normalize nodelta; 37 /2/ 38 ] 39 ] 40 qed. 41 42 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝ 43 λdef. 44 let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in 45 let locals ≝ rtl_if_locals def in 46 let rtl_if_luniverse' ≝ new_univ in 47 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 48 let rtl_if_result' ≝ rtl_if_result def in 49 let rtl_if_params' ≝ rtl_if_params def in 50 let rtl_if_locals' ≝ rtl_if_locals def in 51 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 52 let rtl_if_graph' ≝ rtl_if_graph def in 53 let rtl_if_entry' ≝ rtl_if_entry def in 54 let rtl_if_exit' ≝ rtl_if_exit def in 55 〈mk_rtl_internal_function 56 rtl_if_luniverse' rtl_if_runiverse' rtl_if_result' 57 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 58 rtl_if_entry' rtl_if_exit', lbl〉. 59 60 axiom register_fresh: universe RegisterTag → register. 61 62 definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝ 63 λdef. 64 let r ≝ register_fresh (rtl_if_runiverse def) in 65 let locals ≝ r :: rtl_if_locals def in 66 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 67 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 68 let rtl_if_result' ≝ rtl_if_result def in 69 let rtl_if_params' ≝ rtl_if_params def in 70 let rtl_if_locals' ≝ locals in 71 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 72 let rtl_if_graph' ≝ rtl_if_graph def in 73 let rtl_if_entry' ≝ rtl_if_entry def in 74 let rtl_if_exit' ≝ rtl_if_exit def in 75 〈mk_rtl_internal_function 76 rtl_if_luniverse' rtl_if_runiverse' rtl_if_result' 77 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 78 rtl_if_entry' rtl_if_exit', r〉. 79 80 let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝ 81 match n with 82 [ O ⇒ 〈def, [ ]〉 83  S n ⇒ 84 let 〈def, res〉 ≝ fresh_regs def n in 85 let 〈def, r〉 ≝ fresh_reg def in 86 〈def, r :: res〉 87 ]. 88 89 axiom fresh_regs_length: 90 ∀def: rtl_internal_function. 91 ∀n: nat. 92 (\snd (fresh_regs def n)) = n. 93 94 definition addr_regs ≝ 95 λregs. 96 match regs with 97 [ cons hd tl ⇒ 98 match tl with 99 [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉 100  nil ⇒ None (register × register) 101 ] 102  nil ⇒ None (register × register) (* registers are not an address *) 103 ]. 104 6 include "joint/TranslateUtils.ma". 7 8 (* 105 9 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ 106 10 match n with … … 108 12  S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n') 109 13 ]. 14 *) 110 15 111 16 definition choose_rest ≝ … … 129 34 130 35 definition complete_regs ≝ 36 λglobals. 131 37 λdef. 132 38 λsrcrs1. 133 39 λsrcrs2. 134 let nb_added ≝ abs ((length ? srcrs1)  (length ? srcrs2)) in 135 let 〈def, added_regs〉 ≝ fresh_regs def nb_added in 136 if gtb nb_added 0 then 137 〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉 138 else 139 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 140 141 (* obvious, but proof doesn't look easy! *) 142 axiom complete_regs_length: 143 ∀def. 144 ∀left. 145 ∀right. 146 \fst (\fst (complete_regs def left right)) = \snd (\fst (complete_regs def left right)). 40 if leb (length … srcrs2) (length … srcrs1) then 41 let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in 42 〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉 43 else 44 let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in 45 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 46 47 lemma complete_regs_length: 48 ∀globals,def,left,right. 49 \fst (\fst (complete_regs globals def left right)) = \snd (\fst (complete_regs globals def left right)). 50 #globals #def #left #right 51 whd in match complete_regs normalize nodelta 52 @leb_elim normalize nodelta #H 53 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right))) 54  generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))] 55 cases (fresh_regs ????) #def' #fresh normalize >append_length 56 generalize in match H H; 57 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh) 58 [ /2/  #x #y #z #H generalize in match (not_le_to_lt … H) H #H #E >E >commutative_plus 59 <plus_minus_m_m /2/ ] 60 qed. 147 61 148 62 definition size_of_sig_type ≝ … … 162 76  register_ptr: register → register → register_type. 163 77 164 definition local_env ≝ BitVectorTrie (list register). 165 166 definition mem_local_env ≝ 167 λr: register. 168 match r with 169 [ an_identifier w ⇒ member (list register) 16 w 170 ]. 171 172 definition add_local_env ≝ 173 λr: register. 174 match r with 175 [ an_identifier w ⇒ insert (list register) 16 w 176 ]. 177 178 definition find_local_env ≝ 179 λr: register. 180 λbvt. 181 match r with 182 [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ] 183 ]. 184 78 definition local_env ≝ BitVectorTrie (list register) 16. 79 80 definition mem_local_env : register → local_env → bool ≝ 81 λr. member … (word_of_identifier … r). 82 83 definition add_local_env : register → list register → local_env → local_env ≝ 84 λr. insert … (word_of_identifier … r). 85 86 definition find_local_env : register → local_env → list register ≝ 87 λr: register.λbvt. lookup … (word_of_identifier … r) bvt []. 88 89 (* 185 90 definition initialize_local_env_internal ≝ 186 91 λruniverse. … … 203 108 in 204 109 foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers. 205 110 *) 111 206 112 definition map_list_local_env_internal ≝ 207 λlenv. 208 λres. 209 λr. 210 res @ (find_local_env r lenv). 113 λlenv,res,r. res @ (find_local_env r lenv). 211 114 212 115 definition map_list_local_env ≝ 213 λlenv. 214 λregs. 215 foldl ? ? (map_list_local_env_internal lenv) [ ] regs. 116 λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs. 216 117 217 118 definition make_addr ≝ … … 235 136 3: normalize in tl_nil_prf; 236 137 cases(not_le_Sn_O 0) 237 #HYP cases(HYP tl_nil_prf) 238 ] 138 #HYP cases(HYP tl_nil_prf)] 239 139 qed. 240 140 241 141 definition find_and_addr ≝ 242 λr. 243 λlenv. 244 make_addr ? (find_local_env r lenv). 142 λr,lenv. make_addr ? (find_local_env r lenv). 245 143 246 144 definition rtl_args ≝ 247 λregs_list. 248 λlenv. 249 flatten ? (map ? ? ( 250 λr. find_local_env r lenv) regs_list). 251 252 definition change_label ≝ 253 λlbl. 254 λstmt: rtl_statement. 255 match stmt with 256 [ rtl_st_skip _ ⇒ rtl_st_skip lbl 257  rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl 258  rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl 259  rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl 260  rtl_st_int r i _ ⇒ rtl_st_int r i lbl 261  rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl 262  rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl 263  rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl 264  rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl 265  rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl 266  rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl 267  rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl 268  rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl 269  rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a 270  rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a 271  rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2 272  rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl 273  rtl_st_set_carry l ⇒ rtl_st_set_carry lbl 274  rtl_st_return ⇒ rtl_st_return 275 ]. 276 277 (* Ack! Should generating a fresh label ever fail? This seems to be a sideeffect 278 of implementing everything as a bitvector, which is bounded. If we implemented 279 labels as unbounded nats then this function will never fail. 280 *) 281 (* Fixed with changes to label generation. 282 *) 283 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝ 284 match stmt_list with 285 [ nil ⇒ def 286  cons hd tl ⇒ 287 match tl with 288 [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def 289  cons hd' tl' ⇒ 290 let 〈new_def, tmp_lbl〉 ≝ fresh_label def in 291 let stmt ≝ change_label tmp_lbl hd in 292 let def ≝ add_graph start_lbl stmt new_def in 293 adds_graph tl tmp_lbl dest_lbl new_def 294 ] 295 ]. 296 297 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label) 298 (def: ?) on translate_list ≝ 299 match translate_list with 300 [ nil ⇒ def 301  cons hd tl ⇒ 302 match tl with 303 [ nil ⇒ hd start_lbl dest_lbl def 304  cons hd' tl' ⇒ 305 let 〈new_def, tmp_lbl〉 ≝ fresh_label def in 306 let applied ≝ hd start_lbl tmp_lbl new_def in 307 add_translates tl tmp_lbl dest_lbl applied 308 ] 309 ]. 145 λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list). 310 146 311 147 definition translate_cst_int_internal ≝ 312 λdest_lbl. 313 λr. 314 λi. 315 rtl_st_int r i dest_lbl. 316 148 λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int … r i) dest_lbl. 149 150 (*CSC: XXXXX *) 317 151 axiom translate_cst: 152 ∀globals. 318 153 ∀cst: constant. 319 154 ∀destrs: list register. 320 155 ∀start_lbl: label. 321 156 ∀dest_lbl: label. 322 ∀def: rtl_internal_function .323 rtl_internal_function .157 ∀def: rtl_internal_function globals. 158 rtl_internal_function globals. 324 159 325 160 definition translate_move_internal ≝ 161 λglobals. 326 162 λstart_lbl: label. 327 163 λdestr: register. 328 164 λsrcr: register. 329 rtl_st_move destr srcrstart_lbl.165 joint_st_sequential rtl_params_ globals (joint_instr_move … 〈destr,srcr〉) start_lbl. 330 166 331 167 definition translate_move ≝ 168 λglobals. 332 169 λdestrs: list register. 333 170 λsrcrs: list register. … … 339 176 let restl ≝ \snd (\fst crl_crr) in 340 177 let restr ≝ \snd (\snd crl_crr) in 341 let f_common ≝ translate_move_internal start_lbl in342 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in343 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)344 add_translates [ translate1 ; translate2 ] start_lbl178 let f_common ≝ translate_move_internal globals start_lbl in 179 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in 180 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 181 add_translates … [ translate1 ; translate2 ] start_lbl 345 182 ]. 346 183 @len_proof … … 368 205 369 206 definition translate_cast_unsigned ≝ 207 λglobals. 370 208 λdestrs. 371 209 λstart_lbl. 372 210 λdest_lbl. 373 λdef .374 let 〈def, tmp_zero〉 ≝ fresh_reg def in375 let zeros ≝ make ? tmp_zero (length ?destrs) in376 add_translates [377 adds_graph [378 rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl211 λdef: joint_internal_function … (rtl_params globals). 212 let 〈def, tmp_zero〉 ≝ fresh_reg … def in 213 let zeros ≝ make … tmp_zero (length … destrs) in 214 add_translates … [ 215 adds_graph rtl_params1 … [ 216 joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl 379 217 ]; 380 translate_move destrs zeros218 translate_move globals destrs zeros 381 219 ] start_lbl dest_lbl def. 382 220 383 221 definition translate_cast_signed ≝ 222 λglobals. 384 223 λdestrs. 385 224 λsrcr. … … 387 226 λdest_lbl. 388 227 λdef. 389 let 〈def, tmp_128〉 ≝ fresh_reg def in390 let 〈def, tmp_255〉 ≝ fresh_reg def in391 let 〈def, tmpr〉 ≝ fresh_reg def in392 let 〈def, dummy〉 ≝ fresh_reg def in228 let 〈def, tmp_128〉 ≝ fresh_reg … def in 229 let 〈def, tmp_255〉 ≝ fresh_reg … def in 230 let 〈def, tmpr〉 ≝ fresh_reg … def in 231 let 〈def, dummy〉 ≝ fresh_reg … def in 393 232 let insts ≝ [ 394 233 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl; … … 398 237 rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl 399 238 ] in 400 let srcrs ≝ make ? tmpr (length ?destrs) in401 add_translates [402 adds_graph insts;239 let srcrs ≝ make … tmpr (length … destrs) in 240 add_translates … [ 241 adds_graph … insts; 403 242 translate_move destrs srcrs 404 243 ] start_lbl dest_lbl def.
Note: See TracChangeset
for help on using the changeset viewer.