Changeset 907

Timestamp:

Jun 8, 2011, 6:15:26 PM (9 years ago)

Author:

boender

Message:

• added quadruples to Util
• start of implementation of new jump expansion policy

Location:

src/ASM

Files:

• Assembly.ma (modified) (2 diffs)
• Util.ma (modified) (1 diff)

src/ASM/Assembly.ma

@@ -424 +424 @@
   | long_jump: jump_length.
 
-axiom jump_expansion_policy:
-  ∀program: pseudo_assembly_program.
-  ∀pc: Word.
-   jump_length.
-
+definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
+
+definition find_right_call: Word → Word → nat × (option jump_length) ≝
+ (* medium call: 11 bits, only in "current segment" *)
+ (* can this be done more efficiently with bit vector arithmetic? *)
+ λpc.λaddress.
+  let 〈p1, p2〉 ≝ split ? 5 11 address in
+  let 〈a1, a2〉 ≝ split ? 5 11 pc in
+   if eq_bv ? p1 a1 then (* we're in the same segment *)
+    〈2, Some ? medium_jump〉
+   else
+    〈3, Some ? long_jump〉.
+
+definition distance ≝
+ λx.λy.if gtb x y then x - y else y - x.
+ 
+definition find_right_jump: Word → Word → nat × (option jump_length) ≝
+ (* short jump: 8 bits signed *)
+ (* medium jump: 11 bits, forward only *)
+ λpc.λaddress.
+  let pn ≝ nat_of_bitvector ? pc in
+  let pa ≝ nat_of_bitvector ? address in
+   if ltb (distance pn pa) 512 then
+    〈2, Some ? short_jump〉
+   else
+    find_right_call pc address.
+
+definition find_right_relative_jump: Word → (BitVectorTrie Word 16) →
+ Identifier → nat × (option jump_length) ≝
+ λpc.λlabels.λjmp.
+ match lookup_opt ? ? jmp labels with
+ [ None ⇒ 〈2, Some ? short_jump〉
+ | Some a ⇒ find_right_jump pc a ].
+ 
+definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝
+ λpc.λlabels.λi.
+  match i with
+  [ JC jmp ⇒ find_right_relative_jump pc labels jmp
+  | JNC jmp ⇒ find_right_relative_jump pc labels jmp
+  | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
+  | JZ jmp ⇒ find_right_relative_jump pc labels jmp
+  | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
+  | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
+  | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
+  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
+  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
+  | _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ].
+ 
+definition jump_expansion_policy_internal: pseudo_assembly_program →
+ (BitVectorTrie Word 16) → jump_expansion_policy →
+ ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝
+ λprogram.λlabels.λpolicy.
+   let 〈pc, new_labels, new_policy, changed〉 ≝
+   foldl ? ? (λacc.λi:labelled_instruction.
+    let 〈label, instr〉 ≝ i in
+    let 〈pc,labels,policy,c0〉 ≝ acc in
+    let 〈c1,new_labels〉 ≝ match label with
+     [ None ⇒ 〈c0,labels〉
+     | Some l ⇒
+       match update ? ? pc l labels with
+       [ None ⇒ 〈c0,labels〉
+       | Some x ⇒ 〈true, x〉 ] ] in
+    let 〈pc_delta, jmp_len〉 ≝ match instr with
+     [ Call c ⇒ 
+       match lookup_opt ? ? c new_labels with
+        [ None        ⇒ 〈2, Some ? medium_jump〉
+        | Some c_addr ⇒ find_right_call pc c_addr ]
+     | Jmp j ⇒
+       match lookup_opt ? ? j new_labels with
+        [ None        ⇒ 〈2, Some ? short_jump〉
+        | Some j_addr ⇒ find_right_jump pc j_addr ]
+     | Instruction i ⇒ jep_relative pc new_labels i
+     | Mov _ _ ⇒ (* XXX is this correct? *) 〈2, None …〉
+     | Cost _ ⇒ 〈0, None …〉
+     | Comment _ ⇒ 〈0, None …〉 ] in 
+    let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
+    match jmp_len with
+    [ None   ⇒ 〈new_pc, new_labels, policy, c1〉
+    | Some j ⇒ 
+      match update ? ? pc j policy with
+      [ None ⇒ 〈new_pc, new_labels, policy, c1〉
+      | Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ]
+   ) 〈zero ?, labels, policy, false〉 (\snd program) in
+   〈labels, policy, changed〉.
+
+(* let 〈new_labels, new_policy, ch〉 =
+ jump_expansion_policy_internal program old_labels old_policy in
+ if changed then recurse else stop *)
+ 
 definition expand_relative_jump_internal:
  (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
@@ -563 +647 @@
   λlookup_datalabels.
   λi.
-  let expansion ≝ jump_expansion_policy program pc in
+  let expansion ≝ jump_expansion_policy policy_zero program pc in
     match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     [ None ⇒ None ?

src/ASM/Util.ma

@@ -189 +189 @@
 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
 
+notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
+with precedence 90 for @{ 'quadruple $a $b $c $d}.
+interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
+
+notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
+
 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
  with precedence 10