Changeset 1393 for src/ASM/Assembly.ma

Timestamp:

Oct 17, 2011, 3:50:50 PM (8 years ago)

Author:

boender

Message:

• added invariant for policy trie to assembly
• change (syntax only) to status in order to make it compile
• added lemma + renaming to bitvectortrie

File:

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

src/ASM/Assembly.ma

@@ -414 +414 @@
 
 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
-definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16.
+definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
 
 definition expand_relative_jump_internal:
@@ -545 +545 @@
 
 (* label_trie: identifier ↦ 〈instruction number, address〉 *)
-definition label_trie ≝ BitVectorTrie (nat × Word) 16.
-
-definition add_instruction_size: Word → jump_length → pseudo_instruction → Word ≝
+definition label_trie ≝ BitVectorTrie (nat × nat) 16.
+
+definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
   λpc.λjmp_len.λinstr.
-  let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in
+  let bv_pc ≝ bitvector_of_nat 16 pc in
+  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
   let bv: list (BitVector 8) ≝ match ilist with
     [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
     | Some l ⇒ flatten … (map … assembly1 l)
     ] in 
-  let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
-  new_pc.
-
+  pc + (|bv|).
+  
 definition is_label ≝ 
   λx:labelled_instruction.λl:Identifier. 
@@ -631 +631 @@
  ]
 qed.  
+
+lemma coerc_pair_sigma:
+ ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
+#A #B #P * #a #b #p % [@a | /2/]
+qed.
+coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
+≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). 
      
-definition create_label_trie: list labelled_instruction → jump_expansion_policy → 
-  label_trie ≝
-  λprogram.λpolicy.
+let rec create_label_trie (program: list labelled_instruction)
+  (policy: jump_expansion_policy):
+  (Σlabels:label_trie.
+    ∀i:ℕ.i < |program| →
+    ∀l.occurs_exactly_once l program →
+    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
+    ∃a.lookup_opt … l labels = Some ? 〈i,a〉 
+  ) ≝
   let 〈final_pc, final_labels〉 ≝
     foldl_strong (option Identifier × pseudo_instruction)
-    (λprefix.Σres.
-      let 〈pc,labels〉 ≝ res in
+    (λprefix.ℕ × (Σlabels.
       ∀i:ℕ.i < |prefix| →
-      ∀l.occurs_exactly_once l prefix ->
+      ∀l.occurs_exactly_once l prefix →
       is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
-      ∃a.lookup_opt … l labels = Some ? 〈i,a〉
+      ∃a.lookup_opt … l labels = Some ? 〈i,a〉)
     )
     program
@@ -648 +659 @@
      let 〈pc,labels〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
-     let new_labels ≝ 
-       match label with
-       [ None   ⇒ labels
-       | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
-       ] in
-     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in
-     let new_pc ≝ add_instruction_size pc jmp_len instr in
-     〈new_pc, new_labels〉
-    ) 〈zero ?, Stub ? ?〉 in
+          let new_labels ≝ 
+          match label with
+          [ None   ⇒ labels
+          | Some l ⇒ insert … l 〈|prefix|, pc〉 labels
+          ] in
+          let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
+          〈add_instruction_size pc jmp_len instr, new_labels〉
+    ) 〈0, Stub ? ?〉 in
     final_labels.
-[ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length
-  <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
-  [ #Hi #l cases label
+[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
+  [ #Hi #l normalize nodelta; cases label normalize nodelta
     [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
-      lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr
+      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr  
       % [ @addr | @Haddr ]
     | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
@@ -669 +678 @@
         >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl  
         @⊥ @(absurd … Hocc) 
-      | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?)
-        [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
-        | @Hocc
-        | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]   
+      | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
+        [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ]
+        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
         ]
       ]
@@ -678 +686 @@
     ]
   | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 
-    [ <minus_n_n #Hl normalize in Hl; cases label in Hl;
+    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
       [ normalize nodelta #H @⊥ @H
-      | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]
+      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ]
       ]
     | @le_n
@@ -689 +697 @@
 qed.
 
-definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝
+definition select_reljump_length: label_trie → ℕ → Identifier → jump_length ≝
   λlabels.λpc.λlbl.
   let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
-  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *)
-  then short_jump
-  else long_jump.
-
-definition select_call_length: label_trie → Word → Identifier → jump_length ≝
-  λlabels.λpc.λlbl.
-  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
+  if leb pc addr (* forward jump *)
+  then if leb (addr - pc) 126
+       then short_jump
+       else long_jump
+  else if leb (pc - addr) 129
+       then short_jump
+       else long_jump.
+
+definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝
+  λlabels.λpc_nat.λlbl.
+  let pc ≝ bitvector_of_nat 16 pc_nat in
+  let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) in
   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
@@ -705 +718 @@
   else long_jump.
   
-definition select_jump_length: label_trie → Word → Identifier → jump_length ≝
+definition select_jump_length: label_trie → ℕ → Identifier → jump_length ≝
   λlabels.λpc.λlbl.
   let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
-  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *)
-  then short_jump
-  else
-    let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
-    let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
-    let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
-    if eq_bv ? fst_5_addr fst_5_pc
-    then medium_jump
-    else long_jump.
+  if leb pc addr
+  then if leb (addr - pc) 126
+       then short_jump
+       else select_call_length labels pc lbl
+  else if leb (pc - addr) 129
+       then short_jump
+       else select_call_length labels pc lbl.
  
-definition jump_expansion_step_instruction: label_trie → Word →
+definition jump_expansion_step_instruction: label_trie → ℕ →
   preinstruction Identifier → option jump_length ≝
   λlabels.λpc.λi.
@@ -745 +756 @@
   | short_jump  ⇒ j2
   ].
-      
-definition jump_expansion_step: list labelled_instruction →
-  jump_expansion_policy → jump_expansion_policy ≝ 
-  λprogram.λpolicy.
-  let labels ≝ create_label_trie program policy in
-  let 〈final_n, final_pc, final_policy〉 ≝
+
+definition jmpleq: jump_length → jump_length → Prop ≝
+  λj1.λj2.
+  match j1 with
+  [ short_jump  ⇒ True
+  | medium_jump ⇒
+    match j2 with
+    [ short_jump ⇒ False
+    | _          ⇒ True
+    ]
+  | long_jump   ⇒
+    match j2 with
+    [ long_jump ⇒ True
+    | _         ⇒ False
+    ]
+  ].
+
+definition is_jump' ≝
+  λx:preinstruction Identifier.
+  match x with
+  [ JC _ ⇒ True
+  | JNC _ ⇒ True
+  | JZ _ ⇒ True
+  | JNZ _ ⇒ True
+  | JB _ _ ⇒ True
+  | JNB _ _ ⇒ True
+  | JBC _ _ ⇒ True
+  | CJNE _ _ ⇒ True
+  | DJNZ _ _ ⇒ True
+  | _ ⇒ False
+  ].
+  
+definition is_jump ≝
+  λx:labelled_instruction.
+  let 〈label,instr〉 ≝ x in
+  match instr with
+  [ Instruction i   ⇒ is_jump' i
+  | Call _ ⇒ True
+  | Jmp _ ⇒ True
+  | _ ⇒ False
+  ].
+  
+axiom bitvector_of_nat_ok:
+  ∀x,y,n.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y.
+  
+let rec jump_expansion_step (program: list labelled_instruction)
+  (old_policy: jump_expansion_policy):
+  (Σpolicy.∀i:ℕ.i < |program| →
+    is_jump (nth i ? program 〈None ?, Comment [ ]〉) →
+    ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉 
+  ) ≝ 
+  let labels ≝ create_label_trie program old_policy in
+  let 〈final_pc, final_policy〉 ≝
     foldl_strong (option Identifier × pseudo_instruction)
-    (λprefix.Σres.True)
+    (λprefix.ℕ × Σpolicy.∀i:ℕ.i < |prefix| → 
+      is_jump (nth i ? prefix 〈None ?, Comment [ ]〉) →
+      ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉
+    )
     program
     (λprefix.λx.λtl.λprf.λacc.
-      let 〈n, pc, policy〉 ≝ acc in
+      let 〈pc, policy〉 ≝ acc in
       let 〈label,instr〉 ≝ x in
-      let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in
+      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in
       let add_instr ≝
         match instr with
@@ -766 +827 @@
         ] in
       let 〈new_pc, new_policy〉 ≝
-        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in
+        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in
         match add_instr with
         [ None    ⇒ (* i.e. it's not a jump *)
@@ -772 +833 @@
         | Some ai ⇒
           let new_length ≝ max_length old_length ai in
-          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉 
+          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉 
         ] in
-      〈S n, new_pc, new_policy〉
-    ) 〈0, zero ?, Stub ? ?〉 in
+      〈new_pc, new_policy〉
+    ) 〈0, Stub ? ?〉 in
     final_policy.
- @I
+[ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
+  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
+    lapply (sig2 … policy) #Hacc elim (Hacc i (le_S_S_to_le … Hi) Hj) #henk #ingrid elim ingrid
+    -ingrid #ingrid #Hingrid
+    % [ @henk | % [ @ingrid | normalize nodelta cases instr normalize nodelta
+    [2,3: #x cases (lookup ??? policy ?) #y #z @Hingrid
+    |6: #x #y cases (lookup ??? policy ?) #w #z @Hingrid
+    |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???) 
+      [ @Hingrid
+      | #z normalize nodelta <Hingrid @lookup_opt_insert_miss
+        @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
+        [ @(bitvector_of_nat_ok … H)
+        | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
+        ] ] 
+      ]
+    |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hingrid
+      @lookup_opt_insert_miss @notb_elim >eq_bv_false
+      [1,3: //
+      |2,4: @nmk #H @(absurd (i = (|prefix|)))
+        [1,3: @(bitvector_of_nat_ok … H)
+        |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
+        ] ]
+    ] ] ]
+  | #Hi >nth_append_second >(injective_S … Hi)
+    [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 
+      [2,3: #x #Hj @⊥ @Hj
+      |6: #x #y #Hj @⊥ @Hj
+      |1: #pi cases pi
+        [35,36,37: #Hj @⊥ @Hj
+        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
+        |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
+        |9,10,14,15: #j normalize nodelta #_
+          % [1,3,5,7: @pc
+            |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
+              cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)          
+              #x #y #Hl normalize nodelta
+          % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
+            |2,4,6,8: @lookup_opt_insert_hit
+            ] ]
+        |11,12,13,16,17: #x #j normalize nodelta #_
+          % [1,3,5,7,9: @pc
+            |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
+              cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)          
+              #x #y #Hl normalize nodelta
+          % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
+            |2,4,6,8,10: @lookup_opt_insert_hit
+            ] ]
+        ]
+      |4,5: #j normalize nodelta #_
+        % [1,3: @pc
+          |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
+              #x #y normalize nodelta
+          % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
+            |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
+            |2,4: @lookup_opt_insert_hit
+            ]
+          ]
+      ]
+    | @le_n
+    ]
+  ]
+| #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
+]
 qed.
  
@@ -791 +914 @@
  λprogram.λpc.
   let policy ≝ jump_expansion_internal (\snd program) in
-  let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in
+  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
     j.