Changeset 2316 for src/ASM/Assembly.ma
 Timestamp:
 Sep 3, 2012, 9:03:24 AM (8 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.