Changeset 2048 for src

Timestamp:

Jun 12, 2012, 2:46:54 PM (9 years ago)

Author:

boender

Message:

• factorised jump decisions

Location:

src/ASM

Files:

• Assembly.ma (modified) (4 diffs)
• PolicyFront.ma (modified) (6 diffs)

src/ASM/Assembly.ma

@@ -14 +14 @@
   | medium_jump: jump_length
   | long_jump: jump_length.
+  
+(* Functions that define the conditions under which jumps are possible *)
+definition short_jump_cond: Word → Word → (*pseudo_instruction →*) 
+  bool × (BitVector 8) ≝
+  λpc_plus_jmp_length.λaddr.(*λinstr.*)
+  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
+  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
+    if get_index' ? 2 0 flags then
+      〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉
+    else
+      〈eq_bv 8 upper (zero 8), zero 8〉.
+ 
+definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
+  bool × (BitVector 11) ≝ 
+  λpc_plus_jmp_length.λaddr.(*λinstr.*)
+  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
+  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
+  〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉.
 
 definition assembly_preinstruction ≝
@@ -430 +448 @@
    let lookup_address ≝ sigma (lookup_labels lbl) in
    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
-   let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
-   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
-   if eq_bv ? upper (zero 8) then
-     let address ≝ RELATIVE lower in
+   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
+   if sj_possible
+   then
+     let address ≝ RELATIVE disp in
        [ RealInstruction (i address) ]
    else
@@ -535 +553 @@
   | Comment comment ⇒ [ ]
   | Call call ⇒
-    let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in
     let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
+    let lookup_address ≝ sigma (lookup_labels call) in
+    let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     let do_a_long ≝ policy ppc in
-    let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
-    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
-      let address ≝ ADDR11 resta in
+    if mj_possible ∧ ¬ do_a_long then
+      let address ≝ ADDR11 disp in
         [ ACALL address ]
     else
-      let address ≝ ADDR16 (sigma (lookup_labels call)) in
+      let address ≝ ADDR16 lookup_address in
         [ LCALL address ]
   | Mov d trgt ⇒ 
@@ -553 +571 @@
     let do_a_long ≝ policy ppc in
     let lookup_address ≝ sigma (lookup_labels jmp) in
-    let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in
-    let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
-    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
-      let address ≝ RELATIVE lower in
+    let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
+    if sj_possible ∧ ¬ do_a_long then
+      let address ≝ RELATIVE disp in
         [ SJMP address ]
     else
-      let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in
-      let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
-      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
-        let address ≝ ADDR11 rest_addr in
+      let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
+      if mj_possible ∧ ¬ do_a_long then
+        let address ≝ ADDR11 disp2 in
           [ AJMP address ]
       else    

src/ASM/PolicyFront.ma

@@ -324 +324 @@
   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
-  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
-  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
-  if eq_bv ? upper (zero 8)
+  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
+  if sj_possible
   then short_jump
   else long_jump.
@@ -336 +335 @@
   let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
   let paddr ≝ lookup_def ? ? labels lbl 0 in
-  let addr ≝ 
-    if leb ppc paddr (* forward jump *)
+  let addr ≝ bitvector_of_nat ?
+    (if leb ppc paddr (* forward jump *)
     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
             + added
-    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
-  let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
-  let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
-  if eq_bv ? fst_5_addr fst_5_pc
+    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
+  let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in   
+  if mj_possible
   then medium_jump
   else long_jump.
@@ -356 +354 @@
   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
-  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
-  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
-  if eq_bv ? upper (zero 8)
+  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
+  if sj_possible
   then short_jump
   else select_call_length labels old_sigma inc_sigma added ppc lbl.
@@ -644 +641 @@
 definition policy_equal ≝
   λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
-  (* \fst p1 = \fst p2 ∧ *)
-  (∀n:ℕ.n < |program| →
-    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
-    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
-    \snd pc1 = \snd pc2).
+  (∀n:ℕ.n ≤ |program| →
+    bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 =
+    bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉).
     
 definition nec_plus_ultra ≝
@@ -745 +740 @@
 qed.
 
-(* (Intermediate) policy safety *)
-definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝
-  λpc_plus_jmp_length.λaddr.λinstr.
-  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
-  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
-    if flags then
-      eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true
-    else
-      eq_bv 8 upper (zero 8) = true.
-
-definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝ 
-  λpc_plus_jmp_length.λaddr.λinstr.
-  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
-  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
-  eq_bv 5 fst_5_addr fst_5_pc = true. 
- 
-definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
- λprogram.λlabels.λsigma.
+definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝
+ λprogram.λlabels.λadded.λold_sigma.λsigma.
  ∀i.i < |program| →
  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in
@@ -769 +748 @@
  ∀dest.is_jump_to instr dest → 
    let paddr ≝ lookup_def … labels dest 0 in
-   let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
+   let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
+   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
+   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
    match j with
-   [ short_jump ⇒ short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_call instr
-   | medium_jump ⇒  medium_jump_cond pc_plus_jmp_length addr instr ∧
-       ¬short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_relative_jump instr
-   | long_jump   ⇒ ¬short_jump_cond pc_plus_jmp_length addr instr ∧
-       ¬medium_jump_cond pc_plus_jmp_length addr instr
+   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
+      ¬is_call instr
+   | medium_jump ⇒  \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧
+       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
+       ¬is_relative_jump instr
+   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
+       \fst (medium_jump_cond pc_plus_jmp_length addr) = false
    ].