Changeset 2316 for src/ASM/Assembly.ma

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:

• src/ASM/Assembly.ma (modified) (5 diffs)

src/ASM/Assembly.ma

@@ -441 +441 @@
 *)
 definition expand_relative_jump_internal:
- ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
+ ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.∀policy:Word → bool.
  Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
  list instruction
  ≝
-  λlookup_labels.λsigma.λlbl.λppc,i.
+  λlookup_labels.λsigma.λpolicy.λlbl.λppc,i.
    let lookup_address ≝ sigma (lookup_labels lbl) in
    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
-   if sj_possible
+   if sj_possible ∧ ¬(policy ppc)
    then
      let address ≝ RELATIVE disp in
@@ -462 +462 @@
 
 definition expand_relative_jump: 
-  ∀lookup_labels.∀sigma.
+  ∀lookup_labels.∀sigma.∀policy.
   Word → (*jump_length →*)
   preinstruction Identifier → list instruction ≝
   λlookup_labels: Identifier → Word.
   λsigma:Word → Word.
+  λpolicy:Word → bool.
   λppc: Word.
   (*λjmp_len: jump_length.*)
@@ -472 +473 @@
   (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
   match i with
-  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)
-  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)
-  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)
-  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)
-  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)
-  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)
-  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)
-  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)
-  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)
+  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JC ?)
+  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNC ?)
+  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JB ? baddr)
+  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JZ ?)
+  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNZ ?)
+  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JBC ? baddr)
+  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNB ? baddr)
+  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (CJNE ? addr)
+  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (DJNZ ? addr)
   | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
   | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
@@ -539 +540 @@
     let address ≝ DATA16 (lookup_datalabels trgt) in
       [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
-  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
+  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma policy ppc instr
   | Jmp jmp ⇒
     let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
@@ -754 +755 @@
     @(transitive_lt … (assembly1_lt_128 ?))
     @LT)
-  @pair_elim #x #y #_ cases x normalize nodelta
+  @pair_elim #x #y #_ cases x cases (policy ppc) normalize nodelta
   try
    (change with (|flatten ? [assembly1 ?]| < ?)