Changeset 1325 for src/RTLabs/RTLabsToRTL.ma
- Timestamp:
- Oct 7, 2011, 3:45:13 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1315 r1325 153 153 qed. 154 154 155 let rec translate_cst156 (globals: list ident) (cst: constant) (destrs: list register)157 (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)158 on cst: rtl_internal_function globals ≝159 match cst with160 [ Ointconst size const ⇒161 match destrs with162 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def163 | _ ⇒164 let size' ≝ size_intsize size in165 match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with166 [ true ⇒ λgood_case.167 match split_into_bytes size const with168 [ dp bytes bytes_length_proof ⇒169 let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in170 adds_graph rtl_params1 globals mapped start_lbl dest_lbl def171 ]172 | false ⇒ λbad_case. ?173 ] (refl … (eqb size' (|destrs|)))174 ]175 | Ofloatconst float ⇒ ⊥176 | Oaddrsymbol id offset ⇒177 let 〈r1, r2〉 ≝ make_addr … destrs ? in178 add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def179 | Oaddrstack offset ⇒180 let 〈r1, r2〉 ≝ make_addr … destrs ? in181 ?182 (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)183 ].184 [1: >bytes_length_proof185 cut(size' = |destrs|)186 [1: @eqb_implies_eq187 assumption188 |2: #EQ_HYP189 <EQ_HYP %190 ]191 |5: cases not_implemented (* XXX: float, error_float in o'caml *)192 |*: cases daemon193 ].194 qed.195 196 definition translate_move_internal ≝197 λglobals.198 λdestr: register.199 λsrcr: register.200 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).201 202 definition translate_move ≝203 λglobals.204 λdestrs: list register.205 λsrcrs: list register.206 λstart_lbl: label.207 match reduce_strong register register destrs srcrs with208 [ dp crl_crr len_proof ⇒209 let commonl ≝ \fst (\fst crl_crr) in210 let commonr ≝ \fst (\snd crl_crr) in211 let restl ≝ \snd (\fst crl_crr) in212 let restr ≝ \snd (\snd crl_crr) in213 let f_common ≝ translate_move_internal globals in214 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in215 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)216 add_translates … [ translate1 ; translate2 ] start_lbl217 ].218 @len_proof219 qed.220 221 let rec make222 (A: Type[0]) (elt: A) (n: nat) on n ≝223 match n with224 [ O ⇒ [ ]225 | S n' ⇒ elt :: make A elt n'226 ].227 228 lemma make_length:229 ∀A: Type[0].230 ∀elt: A.231 ∀n: nat.232 n = length ? (make A elt n).233 #A #ELT #N234 elim N235 [ normalize %236 | #N #IH237 normalize <IH %238 ]239 qed.240 241 definition translate_cast_unsigned ≝242 λglobals.243 λdestrs.244 λstart_lbl.245 λdest_lbl.246 λdef: joint_internal_function … (rtl_params globals).247 let 〈def, tmp_zero〉 ≝ fresh_reg … def in248 let zeros ≝ make … tmp_zero (length … destrs) in249 add_translates … [250 adds_graph rtl_params1 … [251 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))252 ];253 translate_move globals destrs zeros254 ] start_lbl dest_lbl def.255 256 definition translate_cast_signed:257 ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝258 λglobals: list ident.259 λdestrs.260 λsrcr.261 λstart_lbl.262 λdest_lbl.263 λdef.264 let 〈def, tmp_128〉 ≝ fresh_reg … def in265 let 〈def, tmp_255〉 ≝ fresh_reg … def in266 let 〈def, tmpr〉 ≝ fresh_reg … def in267 let 〈def, dummy〉 ≝ fresh_reg … def in268 let insts ≝ [269 sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));270 sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);271 sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);272 sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));273 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)274 ]275 in276 let srcrs ≝ make … tmpr (length … destrs) in277 add_translates rtl_params1 globals [278 adds_graph rtl_params1 globals insts;279 translate_move globals destrs srcrs280 ] start_lbl dest_lbl def.281 282 definition translate_cast ≝283 λglobals: list ident.284 λsrc_size: nat.285 λsrc_sign: signedness.286 λdest_size: nat.287 λdestrs: list register.288 λsrcrs: list register.289 match |srcrs| return λx. |srcrs| = x → ? with290 [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]291 | S n' ⇒ λsucc_prf.292 if ltb dest_size src_size then293 translate_move globals destrs srcrs294 else295 match reduce_strong register register destrs srcrs with296 [ dp crl len_proof ⇒297 let commonl ≝ \fst (\fst crl) in298 let commonr ≝ \fst (\snd crl) in299 let restl ≝ \snd (\fst crl) in300 let restr ≝ \snd (\snd crl) in301 let insts_common ≝ translate_move globals commonl commonr in302 let sign_reg ≝ last_safe ? srcrs ? in303 let insts_sign ≝304 match src_sign with305 [ Unsigned ⇒ translate_cast_unsigned globals restl306 | Signed ⇒ translate_cast_signed globals restl sign_reg307 ]308 in309 add_translates rtl_params1 globals [ insts_common; insts_sign ]310 ]311 ] (refl ? (|srcrs|)).312 >succ_prf //313 qed.314 315 definition translate_negint ≝316 λglobals: list ident.317 λdestrs: list register.318 λsrcrs: list register.319 λstart_lbl: label.320 λdest_lbl: label.321 λdef: rtl_internal_function globals.322 λprf: |destrs| = |srcrs|. (* assert in caml code *)323 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in324 let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in325 let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in326 let insts_init ≝ [327 sequential … (SET_CARRY …);328 sequential … (INT rtl_params_ globals tmpr (zero ?))329 ] in330 let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in331 let insts_add ≝ map … f_add destrs in332 adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.333 334 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝335 λglobals: list ident.336 λdestrs: list register.337 λsrcrs: list register.338 λstart_lbl: label.339 λdest_lbl: label.340 λdef: rtl_internal_function globals.341 match destrs with342 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def343 | cons destr destrs ⇒344 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in345 let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in346 let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in347 let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in348 let f ≝ λtmp_srcr. [349 sequential … (CLEAR_CARRY rtl_params_ globals);350 sequential … (INT rtl_params_ globals tmpr (zero ?));351 sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);352 sequential … (INT rtl_params_ globals tmpr (zero ?));353 sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);354 sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)355 ] in356 let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in357 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in358 add_translates rtl_params1 globals [359 save_srcrs; adds_graph rtl_params1 globals insts; epilogue360 ] start_lbl dest_lbl def361 ].362 363 (* TODO: examine this properly. This is a change from the O'caml code due364 to us dropping the explicit use of a cast destination size field. We365 instead infer the size of the cast's destination from the context. Is366 this correct?367 *)368 definition translate_op1 ≝369 λglobals: list ident.370 λop1: unary_operation.371 λdestrs: list register.372 λsrcrs: list register.373 λprf: |destrs| = |srcrs|.374 λstart_lbl: label.375 λdest_lbl: label.376 λdef: rtl_internal_function globals.377 match op1 with378 [ Ocastint src_sign src_size ⇒379 let dest_size ≝ |destrs| * 8 in380 let src_size ≝ bitsize_of_intsize src_size in381 translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def382 | Onegint ⇒383 translate_negint globals destrs srcrs start_lbl dest_lbl def prf384 | Onotbool ⇒385 translate_notbool globals destrs srcrs start_lbl dest_lbl def386 | Onotint ⇒387 let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in388 let l ≝ map2 … f destrs srcrs prf in389 adds_graph rtl_params1 globals l start_lbl dest_lbl def390 | Optrofint r ⇒391 translate_move globals destrs srcrs start_lbl dest_lbl def392 | Ointofptr r ⇒393 translate_move globals destrs srcrs start_lbl dest_lbl def394 | Oid ⇒395 translate_move globals destrs srcrs start_lbl dest_lbl def396 | _ ⇒ ? (* float operations implemented in runtime *)397 ].398 cases not_implemented399 qed.400 401 155 definition translate_op: ∀globals. ? → list register → list register → list register → 402 156 label → label → rtl_internal_function globals → rtl_internal_function globals ≝ … … 444 198 |*: cases daemon (* XXX: some of these look like they may be false *) 445 199 ] 200 qed. 201 202 let rec translate_cst 203 (globals: list ident) (cst: constant) (destrs: list register) 204 (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals) 205 on cst: rtl_internal_function globals ≝ 206 match cst with 207 [ Ointconst size const ⇒ 208 match destrs with 209 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def 210 | _ ⇒ 211 let size' ≝ size_intsize size in 212 match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with 213 [ true ⇒ λgood_case. 214 match split_into_bytes size const with 215 [ dp bytes bytes_length_proof ⇒ 216 let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in 217 adds_graph rtl_params1 globals mapped start_lbl dest_lbl def 218 ] 219 | false ⇒ λbad_case. ? 220 ] (refl … (eqb size' (|destrs|))) 221 ] 222 | Ofloatconst float ⇒ ⊥ 223 | Oaddrsymbol id offset ⇒ 224 let 〈r1, r2〉 ≝ make_addr … destrs ? in 225 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in 226 let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in 227 def 228 | Oaddrstack offset ⇒ 229 let 〈r1, r2〉 ≝ make_addr … destrs ? in 230 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_address r1 r2)) dest_lbl) def in 231 let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in 232 def 233 ]. 234 [1: >bytes_length_proof 235 cut(size' = |destrs|) 236 [1: @eqb_implies_eq 237 assumption 238 |2: #EQ_HYP 239 <EQ_HYP % 240 ] 241 |2: cases daemon (* XXX: bad case where destrs is of the wrong length *) 242 |3: cases not_implemented (* XXX: float, error_float in o'caml *) 243 |*: cases daemon (* XXX: various proofs to be filled in *) 244 ]. 245 qed. 246 247 definition translate_move_internal ≝ 248 λglobals. 249 λdestr: register. 250 λsrcr: register. 251 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉). 252 253 definition translate_move ≝ 254 λglobals. 255 λdestrs: list register. 256 λsrcrs: list register. 257 λstart_lbl: label. 258 match reduce_strong register register destrs srcrs with 259 [ dp crl_crr len_proof ⇒ 260 let commonl ≝ \fst (\fst crl_crr) in 261 let commonr ≝ \fst (\snd crl_crr) in 262 let restl ≝ \snd (\fst crl_crr) in 263 let restr ≝ \snd (\snd crl_crr) in 264 let f_common ≝ translate_move_internal globals in 265 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in 266 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 267 add_translates … [ translate1 ; translate2 ] start_lbl 268 ]. 269 @len_proof 270 qed. 271 272 let rec make 273 (A: Type[0]) (elt: A) (n: nat) on n ≝ 274 match n with 275 [ O ⇒ [ ] 276 | S n' ⇒ elt :: make A elt n' 277 ]. 278 279 lemma make_length: 280 ∀A: Type[0]. 281 ∀elt: A. 282 ∀n: nat. 283 n = length ? (make A elt n). 284 #A #ELT #N 285 elim N 286 [ normalize % 287 | #N #IH 288 normalize <IH % 289 ] 290 qed. 291 292 definition translate_cast_unsigned ≝ 293 λglobals. 294 λdestrs. 295 λstart_lbl. 296 λdest_lbl. 297 λdef: joint_internal_function … (rtl_params globals). 298 let 〈def, tmp_zero〉 ≝ fresh_reg … def in 299 let zeros ≝ make … tmp_zero (length … destrs) in 300 add_translates … [ 301 adds_graph rtl_params1 … [ 302 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) 303 ]; 304 translate_move globals destrs zeros 305 ] start_lbl dest_lbl def. 306 307 definition translate_cast_signed: 308 ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 309 λglobals: list ident. 310 λdestrs. 311 λsrcr. 312 λstart_lbl. 313 λdest_lbl. 314 λdef. 315 let 〈def, tmp_128〉 ≝ fresh_reg … def in 316 let 〈def, tmp_255〉 ≝ fresh_reg … def in 317 let 〈def, tmpr〉 ≝ fresh_reg … def in 318 let 〈def, dummy〉 ≝ fresh_reg … def in 319 let insts ≝ [ 320 sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)); 321 sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr); 322 sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128); 323 sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255)); 324 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255) 325 ] 326 in 327 let srcrs ≝ make … tmpr (length … destrs) in 328 add_translates rtl_params1 globals [ 329 adds_graph rtl_params1 globals insts; 330 translate_move globals destrs srcrs 331 ] start_lbl dest_lbl def. 332 333 definition translate_cast ≝ 334 λglobals: list ident. 335 λsrc_size: nat. 336 λsrc_sign: signedness. 337 λdest_size: nat. 338 λdestrs: list register. 339 λsrcrs: list register. 340 match |srcrs| return λx. |srcrs| = x → ? with 341 [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ] 342 | S n' ⇒ λsucc_prf. 343 if ltb dest_size src_size then 344 translate_move globals destrs srcrs 345 else 346 match reduce_strong register register destrs srcrs with 347 [ dp crl len_proof ⇒ 348 let commonl ≝ \fst (\fst crl) in 349 let commonr ≝ \fst (\snd crl) in 350 let restl ≝ \snd (\fst crl) in 351 let restr ≝ \snd (\snd crl) in 352 let insts_common ≝ translate_move globals commonl commonr in 353 let sign_reg ≝ last_safe ? srcrs ? in 354 let insts_sign ≝ 355 match src_sign with 356 [ Unsigned ⇒ translate_cast_unsigned globals restl 357 | Signed ⇒ translate_cast_signed globals restl sign_reg 358 ] 359 in 360 add_translates rtl_params1 globals [ insts_common; insts_sign ] 361 ] 362 ] (refl ? (|srcrs|)). 363 >succ_prf // 364 qed. 365 366 definition translate_negint ≝ 367 λglobals: list ident. 368 λdestrs: list register. 369 λsrcrs: list register. 370 λstart_lbl: label. 371 λdest_lbl: label. 372 λdef: rtl_internal_function globals. 373 λprf: |destrs| = |srcrs|. (* assert in caml code *) 374 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 375 let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in 376 let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in 377 let insts_init ≝ [ 378 sequential … (SET_CARRY …); 379 sequential … (INT rtl_params_ globals tmpr (zero ?)) 380 ] in 381 let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in 382 let insts_add ≝ map … f_add destrs in 383 adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 384 385 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 386 λglobals: list ident. 387 λdestrs: list register. 388 λsrcrs: list register. 389 λstart_lbl: label. 390 λdest_lbl: label. 391 λdef: rtl_internal_function globals. 392 match destrs with 393 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def 394 | cons destr destrs ⇒ 395 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 396 let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in 397 let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in 398 let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in 399 let f ≝ λtmp_srcr. [ 400 sequential … (CLEAR_CARRY rtl_params_ globals); 401 sequential … (INT rtl_params_ globals tmpr (zero ?)); 402 sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr); 403 sequential … (INT rtl_params_ globals tmpr (zero ?)); 404 sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr); 405 sequential … (OP2 rtl_params_ globals Xor destr destr tmpr) 406 ] in 407 let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in 408 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 409 add_translates rtl_params1 globals [ 410 save_srcrs; adds_graph rtl_params1 globals insts; epilogue 411 ] start_lbl dest_lbl def 412 ]. 413 414 (* TODO: examine this properly. This is a change from the O'caml code due 415 to us dropping the explicit use of a cast destination size field. We 416 instead infer the size of the cast's destination from the context. Is 417 this correct? 418 *) 419 definition translate_op1 ≝ 420 λglobals: list ident. 421 λop1: unary_operation. 422 λdestrs: list register. 423 λsrcrs: list register. 424 λprf: |destrs| = |srcrs|. 425 λstart_lbl: label. 426 λdest_lbl: label. 427 λdef: rtl_internal_function globals. 428 match op1 with 429 [ Ocastint src_sign src_size ⇒ 430 let dest_size ≝ |destrs| * 8 in 431 let src_size ≝ bitsize_of_intsize src_size in 432 translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 433 | Onegint ⇒ 434 translate_negint globals destrs srcrs start_lbl dest_lbl def prf 435 | Onotbool ⇒ 436 translate_notbool globals destrs srcrs start_lbl dest_lbl def 437 | Onotint ⇒ 438 let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in 439 let l ≝ map2 … f destrs srcrs prf in 440 adds_graph rtl_params1 globals l start_lbl dest_lbl def 441 | Optrofint r ⇒ 442 translate_move globals destrs srcrs start_lbl dest_lbl def 443 | Ointofptr r ⇒ 444 translate_move globals destrs srcrs start_lbl dest_lbl def 445 | Oid ⇒ 446 translate_move globals destrs srcrs start_lbl dest_lbl def 447 | _ ⇒ ? (* float operations implemented in runtime *) 448 ]. 449 cases not_implemented 446 450 qed. 447 451 … … 512 516 λdummy_lbl: label. 513 517 λi: nat. 514 λi_prf .518 λi_prf: i ≤ |tmp_destrs|. 515 519 λtranslates: list ?. 516 520 λsrcr2i: register. … … 535 539 translates @ tmp_destrs2'. 536 540 537 axiom translate_mul:538 ∀globals: list ident.539 ∀destrs: list register.540 ∀srcrs1: list register.541 ∀srcrs2: list register.542 ∀start_lbl: label.543 ∀dest_lbl: label.544 ∀def: rtl_internal_function globals.545 rtl_internal_function globals.546 547 541 (* 548 542 definition translate_mul ≝ … … 569 563 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 570 564 *) 565 566 axiom translate_mul: 567 ∀globals: list ident. 568 ∀destrs: list register. 569 ∀srcrs1: list register. 570 ∀srcrs2: list register. 571 ∀start_lbl: label. 572 ∀dest_lbl: label. 573 ∀def: rtl_internal_function globals. 574 rtl_internal_function globals. 571 575 572 576 definition translate_divumodu8 ≝
Note: See TracChangeset
for help on using the changeset viewer.