Changeset 1285 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Oct 3, 2011, 3:08:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1283 r1285 216 216 ] start_lbl dest_lbl def. 217 217 218 (* 219 definition translate_cast_signed≝220 λglobals .218 definition translate_cast_signed: 219 ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 220 λglobals: list ident. 221 221 λdestrs. 222 222 λsrcr. … … 229 229 let 〈def, dummy〉 ≝ fresh_reg … def in 230 230 let insts ≝ [ 231 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl; 232 rtl_st_op2 And tmpr tmp_128 srcr start_lbl; 233 rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl; 234 rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl; 235 rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl 236 ] in 231 sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)); 232 sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr); 233 sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128); 234 sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255)); 235 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255) 236 ] 237 in 237 238 let srcrs ≝ make … tmpr (length … destrs) in 238 add_translates …[239 adds_graph …insts;240 translate_move destrs srcrs239 add_translates rtl_params1 globals [ 240 adds_graph rtl_params1 globals insts; 241 translate_move globals destrs srcrs 241 242 ] start_lbl dest_lbl def. 242 243 243 244 definition translate_cast ≝ 244 λsrc_size. 245 λsrc_sign. 246 λdest_size. 247 λdestrs. 248 λsrcrs. 245 λglobals: list ident. 246 λsrc_size: nat. 247 λsrc_sign: signedness. 248 λdest_size: nat. 249 λdestrs: list register. 250 λsrcrs: list register. 249 251 match srcrs return λx. srcrs = x → ? with 250 [ O ⇒ λzero_prf. adds_graph [ ]252 [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ] 251 253  S n' ⇒ λsucc_prf. 252 254 if ltb dest_size src_size then 253 translate_move destrs srcrs255 translate_move globals destrs srcrs 254 256 else 255 257 match reduce_strong register register destrs srcrs with … … 259 261 let restl ≝ \snd (\fst crl) in 260 262 let restr ≝ \snd (\snd crl) in 261 let insts_common ≝ translate_move commonl commonr in263 let insts_common ≝ translate_move globals commonl commonr in 262 264 let sign_reg ≝ last_safe ? srcrs ? in 263 265 let insts_sign ≝ 264 266 match src_sign with 265 [ Unsigned ⇒ translate_cast_unsigned restl266  Signed ⇒ translate_cast_signed restl sign_reg267 [ Unsigned ⇒ translate_cast_unsigned globals restl 268  Signed ⇒ translate_cast_signed globals restl sign_reg 267 269 ] 268 270 in 269 add_translates [ insts_common; insts_sign ]271 add_translates rtl_params1 globals [ insts_common; insts_sign ] 270 272 ] 271 273 ] (refl ? (srcrs)). … … 274 276 275 277 definition translate_negint ≝ 276 λdestrs. 277 λsrcrs. 278 λstart_lbl. 279 λdest_lbl. 280 λdef. 281 λprf:  destrs  =  srcrs . (* assert in caml code *) 282 let 〈def, tmpr〉 ≝ fresh_reg def in 283 let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 284 let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in 278 λglobals: list ident. 279 λdestrs: list register. 280 λsrcrs: list register. 281 λstart_lbl: label. 282 λdest_lbl: label. 283 λdef: rtl_internal_function globals. 284 λprf: destrs = srcrs. (* assert in caml code *) 285 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 286 let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in 287 let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in 285 288 let insts_init ≝ [ 286 rtl_st_set_carry start_lbl;287 rtl_st_int tmpr (zero ?) start_lbl289 sequential … (SET_CARRY …); 290 sequential … (INT rtl_params_ globals tmpr (zero ?)) 288 291 ] in 289 let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lblin292 let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in 290 293 let insts_add ≝ map … f_add destrs in 291 adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 292 293 definition translate_notbool ≝ 294 λdestrs. 295 λsrcrs. 296 λstart_lbl. 297 λdest_lbl. 298 λdef. 294 adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 295 296 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 297 λglobals: list ident. 298 λdestrs: list register. 299 λsrcrs: list register. 300 λstart_lbl: label. 301 λdest_lbl: label. 302 λdef: rtl_internal_function globals. 299 303 match destrs with 300 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def304 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def 301 305  cons destr destrs ⇒ 302 let 〈def, tmpr〉 ≝ fresh_reg def in303 let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in304 let save_srcrs ≝ translate_move tmp_srcrs srcrs in305 let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lblin306 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 307 let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in 308 let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in 309 let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in 306 310 let f ≝ λtmp_srcr. [ 307 rtl_st_clear_carry start_lbl;308 rtl_st_int tmpr (zero ?) start_lbl;309 rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;310 rtl_st_int tmpr (zero ?) start_lbl;311 rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;312 rtl_st_op2 Xor destr destr tmpr start_lbl311 sequential … (CLEAR_CARRY rtl_params_ globals); 312 sequential … (INT rtl_params_ globals tmpr (zero ?)); 313 sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr); 314 sequential … (INT rtl_params_ globals tmpr (zero ?)); 315 sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr); 316 sequential … (OP2 rtl_params_ globals Xor destr destr tmpr) 313 317 ] in 314 let insts ≝ init_destr :: (flatten ?(map … f tmp_srcrs)) in315 let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in316 add_translates [317 save_srcrs; adds_graph insts; epilogue318 let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in 319 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 320 add_translates rtl_params1 globals [ 321 save_srcrs; adds_graph rtl_params1 globals insts; epilogue 318 322 ] start_lbl dest_lbl def 319 323 ]. 324 325 (* 320 326 321 327 (* TODO: examine this properly. This is a change from the O'caml code due
Note: See TracChangeset
for help on using the changeset viewer.