Changeset 2316 for src/ASM/Assembly.ma
- Timestamp:
- Sep 3, 2012, 9:03:24 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2268 r2316 441 441 *) 442 442 definition expand_relative_jump_internal: 443 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word. 443 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.∀policy:Word → bool. 444 444 Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 445 445 list instruction 446 446 ≝ 447 λlookup_labels.λsigma.λ lbl.λppc,i.447 λlookup_labels.λsigma.λpolicy.λlbl.λppc,i. 448 448 let lookup_address ≝ sigma (lookup_labels lbl) in 449 449 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 450 450 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 451 if sj_possible 451 if sj_possible ∧ ¬(policy ppc) 452 452 then 453 453 let address ≝ RELATIVE disp in … … 462 462 463 463 definition expand_relative_jump: 464 ∀lookup_labels.∀sigma. 464 ∀lookup_labels.∀sigma.∀policy. 465 465 Word → (*jump_length →*) 466 466 preinstruction Identifier → list instruction ≝ 467 467 λlookup_labels: Identifier → Word. 468 468 λsigma:Word → Word. 469 λpolicy:Word → bool. 469 470 λppc: Word. 470 471 (*λjmp_len: jump_length.*) … … 472 473 (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*) 473 474 match i with 474 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)475 | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)476 | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)477 | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)478 | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)479 | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)480 | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)481 | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)482 | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)475 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JC ?) 476 | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNC ?) 477 | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JB ? baddr) 478 | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JZ ?) 479 | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNZ ?) 480 | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JBC ? baddr) 481 | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNB ? baddr) 482 | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (CJNE ? addr) 483 | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (DJNZ ? addr) 483 484 | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] 484 485 | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] … … 539 540 let address ≝ DATA16 (lookup_datalabels trgt) in 540 541 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 541 | Instruction instr ⇒ expand_relative_jump lookup_labels sigma p pc instr542 | Instruction instr ⇒ expand_relative_jump lookup_labels sigma policy ppc instr 542 543 | Jmp jmp ⇒ 543 544 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in … … 754 755 @(transitive_lt … (assembly1_lt_128 ?)) 755 756 @LT) 756 @pair_elim #x #y #_ cases x normalize nodelta757 @pair_elim #x #y #_ cases x cases (policy ppc) normalize nodelta 757 758 try 758 759 (change with (|flatten ? [assembly1 ?]| < ?)
Note: See TracChangeset
for help on using the changeset viewer.