Changeset 2316 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (7 years ago)
Author:
boender
Message:
  • committed temporary version: true version has to wait until I recuperate my hard disk
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2268 r2316  
    441441*)
    442442definition expand_relative_jump_internal:
    443  ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
     443 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.∀policy:Word → bool.
    444444 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
    445445 list instruction
    446446 ≝
    447   λlookup_labels.λsigma.λlbl.λppc,i.
     447  λlookup_labels.λsigma.λpolicy.λlbl.λppc,i.
    448448   let lookup_address ≝ sigma (lookup_labels lbl) in
    449449   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    450450   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    451    if sj_possible
     451   if sj_possible ∧ ¬(policy ppc)
    452452   then
    453453     let address ≝ RELATIVE disp in
     
    462462
    463463definition expand_relative_jump:
    464   ∀lookup_labels.∀sigma.
     464  ∀lookup_labels.∀sigma.∀policy.
    465465  Word → (*jump_length →*)
    466466  preinstruction Identifier → list instruction ≝
    467467  λlookup_labels: Identifier → Word.
    468468  λsigma:Word → Word.
     469  λpolicy:Word → bool.
    469470  λppc: Word.
    470471  (*λjmp_len: jump_length.*)
     
    472473  (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
    473474  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)
    483484  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
    484485  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
     
    539540    let address ≝ DATA16 (lookup_datalabels trgt) in
    540541      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    541   | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
     542  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma policy ppc instr
    542543  | Jmp jmp ⇒
    543544    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     
    754755    @(transitive_lt … (assembly1_lt_128 ?))
    755756    @LT)
    756   @pair_elim #x #y #_ cases x normalize nodelta
     757  @pair_elim #x #y #_ cases x cases (policy ppc) normalize nodelta
    757758  try
    758759   (change with (|flatten ? [assembly1 ?]| < ?)
Note: See TracChangeset for help on using the changeset viewer.