[3103] | 1 | |
---|
[2034] | 2 | include "utilities/extralib.ma". |
---|
[3103] | 3 | |
---|
[2034] | 4 | include "ASM/Assembly.ma". |
---|
| 5 | |
---|
| 6 | (* Internal types *) |
---|
| 7 | |
---|
| 8 | (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) |
---|
| 9 | definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16). |
---|
| 10 | |
---|
| 11 | (* The different properties that we want/need to prove at some point *) |
---|
| 12 | (* During our iteration, everything not yet seen is None, and vice versa *) |
---|
[2101] | 13 | definition out_of_program_none ≝ |
---|
| 14 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
| 15 | ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?). |
---|
[2034] | 16 | |
---|
[2101] | 17 | definition not_jump_default ≝ |
---|
| 18 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
[2034] | 19 | ∀i:ℕ.i < |prefix| → |
---|
[2652] | 20 | ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment EmptyString〉)) → |
---|
[2101] | 21 | \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. |
---|
| 22 | |
---|
[2034] | 23 | (* Between two policies, jumps cannot decrease *) |
---|
| 24 | definition jmpeqb: jump_length → jump_length → bool ≝ |
---|
| 25 | λj1.λj2. |
---|
| 26 | match j1 with |
---|
| 27 | [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ] |
---|
[2101] | 28 | | absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true | _ ⇒ false ] |
---|
[2034] | 29 | | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ] |
---|
| 30 | ]. |
---|
| 31 | |
---|
| 32 | lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2. |
---|
| 33 | #j1 #j2 cases j1 cases j2 |
---|
| 34 | [1,5,9: / by /] |
---|
| 35 | #H cases H |
---|
| 36 | qed. |
---|
| 37 | |
---|
| 38 | definition jmple: jump_length → jump_length → Prop ≝ |
---|
| 39 | λj1.λj2. |
---|
| 40 | match j1 with |
---|
| 41 | [ short_jump ⇒ |
---|
| 42 | match j2 with |
---|
| 43 | [ short_jump ⇒ False |
---|
| 44 | | _ ⇒ True |
---|
| 45 | ] |
---|
[2101] | 46 | | absolute_jump ⇒ |
---|
[2034] | 47 | match j2 with |
---|
| 48 | [ long_jump ⇒ True |
---|
| 49 | | _ ⇒ False |
---|
| 50 | ] |
---|
| 51 | | long_jump ⇒ False |
---|
| 52 | ]. |
---|
| 53 | |
---|
| 54 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
| 55 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
| 56 | |
---|
[2101] | 57 | definition jump_increase ≝ |
---|
| 58 | λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. |
---|
| 59 | ∀i.i ≤ |prefix| → |
---|
| 60 | let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in |
---|
| 61 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in |
---|
[2211] | 62 | jmpleq oj j. |
---|
[2059] | 63 | |
---|
[2034] | 64 | (* this is the instruction size as determined by the jump length given *) |
---|
| 65 | definition expand_relative_jump_internal_unsafe: |
---|
| 66 | jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ |
---|
| 67 | λjmp_len:jump_length.λi. |
---|
| 68 | match jmp_len with |
---|
| 69 | [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] |
---|
[2101] | 70 | | absolute_jump ⇒ [ ] (* this should not happen *) |
---|
[2034] | 71 | | long_jump ⇒ |
---|
| 72 | [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); |
---|
| 73 | SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) |
---|
| 74 | LJMP (ADDR16 (zero 16)) |
---|
| 75 | ] |
---|
| 76 | ]. |
---|
| 77 | @I |
---|
| 78 | qed. |
---|
| 79 | |
---|
[2235] | 80 | definition strip_target: |
---|
| 81 | preinstruction Identifier → |
---|
| 82 | ([[relative]] → preinstruction [[relative]]) ⊎ instruction ≝ |
---|
| 83 | λi. |
---|
| 84 | match i with |
---|
| 85 | [ JC _ ⇒ inl … (JC ?) |
---|
| 86 | | JNC _ ⇒ inl … (JNC ?) |
---|
| 87 | | JB baddr _ ⇒ inl … (JB ? baddr) |
---|
| 88 | | JZ _ ⇒ inl … (JZ ?) |
---|
| 89 | | JNZ _ ⇒ inl … (JNZ ?) |
---|
| 90 | | JBC baddr _ ⇒ inl … (JBC ? baddr) |
---|
| 91 | | JNB baddr _ ⇒ inl … (JNB ? baddr) |
---|
| 92 | | CJNE addr _ ⇒ inl … (CJNE ? addr) |
---|
| 93 | | DJNZ addr _ ⇒ inl … (DJNZ ? addr) |
---|
| 94 | | ADD arg1 arg2 ⇒ inr … (ADD ? arg1 arg2) |
---|
| 95 | | ADDC arg1 arg2 ⇒ inr … (ADDC ? arg1 arg2) |
---|
| 96 | | SUBB arg1 arg2 ⇒ inr … (SUBB ? arg1 arg2) |
---|
| 97 | | INC arg ⇒ inr … (INC ? arg) |
---|
| 98 | | DEC arg ⇒ inr … (DEC ? arg) |
---|
| 99 | | MUL arg1 arg2 ⇒ inr … (MUL ? arg1 arg2) |
---|
| 100 | | DIV arg1 arg2 ⇒ inr … (DIV ? arg1 arg2) |
---|
| 101 | | DA arg ⇒ inr … (DA ? arg) |
---|
| 102 | | ANL arg ⇒ inr … (ANL ? arg) |
---|
| 103 | | ORL arg ⇒ inr … (ORL ? arg) |
---|
| 104 | | XRL arg ⇒ inr … (XRL ? arg) |
---|
| 105 | | CLR arg ⇒ inr … (CLR ? arg) |
---|
| 106 | | CPL arg ⇒ inr … (CPL ? arg) |
---|
| 107 | | RL arg ⇒ inr … (RL ? arg) |
---|
| 108 | | RR arg ⇒ inr … (RR ? arg) |
---|
| 109 | | RLC arg ⇒ inr … (RLC ? arg) |
---|
| 110 | | RRC arg ⇒ inr … (RRC ? arg) |
---|
| 111 | | SWAP arg ⇒ inr … (SWAP ? arg) |
---|
| 112 | | MOV arg ⇒ inr … (MOV ? arg) |
---|
| 113 | | MOVX arg ⇒ inr … (MOVX ? arg) |
---|
| 114 | | SETB arg ⇒ inr … (SETB ? arg) |
---|
| 115 | | PUSH arg ⇒ inr … (PUSH ? arg) |
---|
| 116 | | POP arg ⇒ inr … (POP ? arg) |
---|
| 117 | | XCH arg1 arg2 ⇒ inr … (XCH ? arg1 arg2) |
---|
| 118 | | XCHD arg1 arg2 ⇒ inr … (XCHD ? arg1 arg2) |
---|
| 119 | | RET ⇒ inr … (RET ?) |
---|
| 120 | | RETI ⇒ inr … (RETI ?) |
---|
[2713] | 121 | | NOP ⇒ inr … (NOP ?) |
---|
| 122 | | JMP dst ⇒ inr … (RealInstruction (JMP ? dst)) |
---|
[2235] | 123 | ]. |
---|
| 124 | |
---|
[2034] | 125 | definition expand_relative_jump_unsafe: |
---|
| 126 | jump_length → preinstruction Identifier → list instruction ≝ |
---|
| 127 | λjmp_len:jump_length.λi. |
---|
[2235] | 128 | match strip_target i with |
---|
| 129 | [ inl jmp ⇒ expand_relative_jump_internal_unsafe jmp_len jmp |
---|
| 130 | | inr instr ⇒ [ instr ] ]. |
---|
[2034] | 131 | |
---|
[2235] | 132 | definition expand_pseudo_instruction_unsafe: |
---|
| 133 | jump_length → pseudo_instruction → list instruction ≝ |
---|
[2034] | 134 | λjmp_len. |
---|
| 135 | λi. |
---|
[2235] | 136 | match i with |
---|
[3034] | 137 | [ Cost cost ⇒ [ NOP … ] |
---|
[2034] | 138 | | Comment comment ⇒ [ ] |
---|
| 139 | | Call call ⇒ |
---|
| 140 | match jmp_len with |
---|
| 141 | [ short_jump ⇒ [ ] (* this should not happen *) |
---|
[2101] | 142 | | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] |
---|
[2034] | 143 | | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] |
---|
| 144 | ] |
---|
[3039] | 145 | | Mov d trgt off ⇒ |
---|
| 146 | match d with |
---|
| 147 | [ inl _ ⇒ |
---|
| 148 | let address ≝ DATA16 (bv_zero 16) in |
---|
| 149 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] |
---|
| 150 | | inr pr ⇒ |
---|
| 151 | let v ≝ DATA (bv_zero 8) in |
---|
| 152 | match \fst pr return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with |
---|
| 153 | [ ACC_A ⇒ λ_. |
---|
| 154 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, v〉))))))] |
---|
| 155 | | DIRECT b1 ⇒ λ_. |
---|
| 156 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))] |
---|
| 157 | | REGISTER r ⇒ λ_. |
---|
| 158 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))] |
---|
| 159 | | _ ⇒ Ⓧ ] (subaddressing_modein …)] |
---|
[2034] | 160 | | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr |
---|
[2713] | 161 | | Jnz acc dst1 dst2 ⇒ |
---|
| 162 | [ RealInstruction (JNZ … (RELATIVE (bitvector_of_nat ? 3))); |
---|
| 163 | LJMP (ADDR16 (zero ?)); |
---|
| 164 | LJMP (ADDR16 (zero ?)) ] |
---|
[2034] | 165 | | Jmp jmp ⇒ |
---|
| 166 | match jmp_len with |
---|
| 167 | [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] |
---|
[2101] | 168 | | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] |
---|
[2034] | 169 | | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] |
---|
| 170 | ] |
---|
[2235] | 171 | ]. |
---|
| 172 | % |
---|
| 173 | qed. |
---|
| 174 | |
---|
| 175 | definition instruction_size_jmplen: |
---|
| 176 | jump_length → pseudo_instruction → ℕ ≝ |
---|
| 177 | λjmp_len. |
---|
| 178 | λi. |
---|
| 179 | let mapped ≝ map ? ? assembly1 (expand_pseudo_instruction_unsafe jmp_len i) in |
---|
[2034] | 180 | let flattened ≝ flatten ? mapped in |
---|
| 181 | let pc_len ≝ length ? flattened in |
---|
| 182 | pc_len. |
---|
| 183 | |
---|
[2101] | 184 | definition sigma_compact_unsafe ≝ |
---|
| 185 | λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
| 186 | ∀n.n < |prefix| → |
---|
[2034] | 187 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
| 188 | [ None ⇒ False |
---|
| 189 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
| 190 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
| 191 | [ None ⇒ False |
---|
| 192 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
[2652] | 193 | pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment EmptyString〉)) |
---|
[2034] | 194 | ] |
---|
| 195 | ]. |
---|
[2273] | 196 | |
---|
[2101] | 197 | (* new safety condition: sigma corresponds to program and resulting program is compact *) |
---|
| 198 | definition sigma_compact ≝ |
---|
| 199 | λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
[2318] | 200 | ∀datalabels.∀n.n < |program| → |
---|
[2034] | 201 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
| 202 | [ None ⇒ False |
---|
| 203 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
| 204 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
| 205 | [ None ⇒ False |
---|
| 206 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
| 207 | pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
[2318] | 208 | datalabels |
---|
[2034] | 209 | (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
| 210 | (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
[2652] | 211 | (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment EmptyString〉)) |
---|
[2034] | 212 | ] |
---|
| 213 | ]. |
---|
[2101] | 214 | |
---|
| 215 | (* jumps are of the proper size *) |
---|
| 216 | definition sigma_safe ≝ |
---|
[2316] | 217 | λprefix:list labelled_instruction.λlabels:label_map. |
---|
[2101] | 218 | λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. |
---|
| 219 | ∀i.i < |prefix| → |
---|
[2653] | 220 | let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in |
---|
[2101] | 221 | ∀dest.is_jump_to instr dest → |
---|
[2316] | 222 | let paddr ≝ lookup_def … labels dest 0 in |
---|
| 223 | let 〈j,src,dest〉 ≝ |
---|
| 224 | if leb paddr i then (* backward jump *) |
---|
| 225 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in |
---|
| 226 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in |
---|
| 227 | let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in |
---|
| 228 | 〈j,pc_plus_jmp_length,addr〉 |
---|
| 229 | else |
---|
| 230 | let 〈pc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉 in |
---|
| 231 | let 〈npc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in |
---|
| 232 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉)) in |
---|
| 233 | let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)) in |
---|
| 234 | 〈j,pc_plus_jmp_length,addr〉 in |
---|
[2101] | 235 | match j with |
---|
[2316] | 236 | [ short_jump ⇒ \fst (short_jump_cond src dest) = true |
---|
| 237 | | absolute_jump ⇒ \fst (absolute_jump_cond src dest) = true (*∧ |
---|
| 238 | \fst (short_jump_cond src dest) = false*) |
---|
| 239 | | long_jump ⇒ True (* do not talk about long jump *) |
---|
[2101] | 240 | ]. |
---|
[2316] | 241 | |
---|
| 242 | definition sigma_jumps ≝ |
---|
| 243 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
| 244 | ∀i.i < |prefix| → |
---|
[2652] | 245 | let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in |
---|
[2316] | 246 | (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump → |
---|
| 247 | bool_to_Prop (¬is_call instr)) ∧ |
---|
| 248 | (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = absolute_jump → |
---|
| 249 | bool_to_Prop (¬is_relative_jump instr)). |
---|
[2034] | 250 | |
---|
| 251 | (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) |
---|
| 252 | definition max_length: jump_length → jump_length → jump_length ≝ |
---|
| 253 | λj1.λj2. |
---|
| 254 | match j1 with |
---|
| 255 | [ long_jump ⇒ long_jump |
---|
[2101] | 256 | | absolute_jump ⇒ |
---|
[2034] | 257 | match j2 with |
---|
[2101] | 258 | [ absolute_jump ⇒ absolute_jump |
---|
[2034] | 259 | | _ ⇒ long_jump |
---|
| 260 | ] |
---|
| 261 | | short_jump ⇒ |
---|
| 262 | match j2 with |
---|
| 263 | [ short_jump ⇒ short_jump |
---|
| 264 | | _ ⇒ long_jump |
---|
| 265 | ] |
---|
| 266 | ]. |
---|
| 267 | |
---|
| 268 | lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)). |
---|
| 269 | #x #y cases x cases y /3 by inl, inr, nmk, I/ |
---|
| 270 | qed. |
---|
| 271 | |
---|
| 272 | lemma jmpleq_max_length: ∀ol,nl. |
---|
| 273 | jmpleq ol (max_length ol nl). |
---|
| 274 | #ol #nl cases ol cases nl |
---|
| 275 | /2 by or_introl, or_intror, I/ |
---|
| 276 | qed. |
---|
| 277 | |
---|
| 278 | lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b). |
---|
| 279 | #a #b cases a cases b /2/ |
---|
| 280 | %2 @nmk #H destruct (H) |
---|
| 281 | qed. |
---|
| 282 | |
---|
| 283 | (* The function that creates the label-to-address map *) |
---|
| 284 | definition create_label_map: ∀program:list labelled_instruction. |
---|
| 285 | (Σlabels:label_map. |
---|
| 286 | ∀l.occurs_exactly_once ?? l program → |
---|
[2264] | 287 | (*And (bitvector_of_nat ? (lookup_def ?? labels l 0) = |
---|
| 288 | address_of_word_labels program l) |
---|
| 289 | ( *)lookup_def ?? labels l 0 < |program|(*)*) |
---|
[2034] | 290 | ) ≝ |
---|
| 291 | λprogram. |
---|
| 292 | \fst (create_label_cost_map program). |
---|
[2264] | 293 | #l #Hl cases (create_label_cost_map_ok program) #_ #X @(X … Hl) |
---|
[2034] | 294 | qed. |
---|
| 295 | |
---|
| 296 | (* General note on jump length selection: the jump displacement is added/replaced |
---|
| 297 | * AFTER the fetch (and attendant PC increase), but we calculate before the |
---|
[2316] | 298 | * fetch, which means that we are [jump_length] bytes off and have to compensate. *) |
---|
| 299 | definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → |
---|
| 300 | Identifier → ℕ → jump_length ≝ |
---|
| 301 | λlabels.λold_sigma.λinc_sigma.λppc.λlbl.λins_len. |
---|
| 302 | let paddr ≝ lookup_def ?? labels lbl 0 in |
---|
| 303 | let 〈src,dest〉 ≝ |
---|
| 304 | if leb paddr ppc then (* backward jump *) |
---|
| 305 | let pc ≝ \fst inc_sigma in |
---|
| 306 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
| 307 | 〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉 |
---|
| 308 | else |
---|
| 309 | let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 310 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 311 | 〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉 in |
---|
| 312 | let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in |
---|
[2048] | 313 | if sj_possible |
---|
[2034] | 314 | then short_jump |
---|
| 315 | else long_jump. |
---|
| 316 | |
---|
[2316] | 317 | definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → |
---|
[2034] | 318 | Identifier → jump_length ≝ |
---|
[2316] | 319 | λlabels.λold_sigma.λinc_sigma.λppc.λlbl. |
---|
| 320 | let paddr ≝ lookup_def ?? labels lbl 0 in |
---|
| 321 | let 〈src,dest〉 ≝ |
---|
| 322 | if leb paddr ppc then (* backward jump *) |
---|
| 323 | let pc ≝ \fst inc_sigma in |
---|
| 324 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
| 325 | 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 |
---|
| 326 | else |
---|
| 327 | let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 328 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 329 | 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in |
---|
| 330 | let 〈aj_possible, disp〉 ≝ absolute_jump_cond src dest in |
---|
[2101] | 331 | if aj_possible |
---|
| 332 | then absolute_jump |
---|
[2034] | 333 | else long_jump. |
---|
| 334 | |
---|
[2316] | 335 | definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → |
---|
[2034] | 336 | Identifier → jump_length ≝ |
---|
[2316] | 337 | λlabels.λold_sigma.λinc_sigma.λppc.λlbl. |
---|
| 338 | let paddr ≝ lookup_def ?? labels lbl 0 in |
---|
| 339 | let 〈src,dest〉 ≝ |
---|
| 340 | if leb paddr ppc then (* backward jump *) |
---|
| 341 | let pc ≝ \fst inc_sigma in |
---|
| 342 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
| 343 | 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 |
---|
| 344 | else |
---|
| 345 | let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 346 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in |
---|
| 347 | 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in |
---|
| 348 | let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in |
---|
[2048] | 349 | if sj_possible |
---|
[2034] | 350 | then short_jump |
---|
[2316] | 351 | else select_call_length labels old_sigma inc_sigma ppc lbl. |
---|
[2225] | 352 | |
---|
| 353 | definition destination_of: preinstruction Identifier → option Identifier ≝ |
---|
| 354 | λi. |
---|
| 355 | match i with |
---|
| 356 | [ JC j ⇒ Some ? j |
---|
| 357 | | JNC j ⇒ Some ? j |
---|
| 358 | | JZ j ⇒ Some ? j |
---|
| 359 | | JNZ j ⇒ Some ? j |
---|
| 360 | | JB _ j ⇒ Some ? j |
---|
| 361 | | JBC _ j ⇒ Some ? j |
---|
| 362 | | JNB _ j ⇒ Some ? j |
---|
| 363 | | CJNE _ j ⇒ Some ? j |
---|
| 364 | | DJNZ _ j ⇒ Some ? j |
---|
| 365 | | _ ⇒ None ? |
---|
| 366 | ]. |
---|
| 367 | |
---|
[2316] | 368 | definition length_of: preinstruction Identifier → ℕ ≝ |
---|
| 369 | λi. |
---|
| 370 | match i with |
---|
| 371 | [ JC j ⇒ 2 |
---|
| 372 | | JNC j ⇒ 2 |
---|
| 373 | | JZ j ⇒ 2 |
---|
| 374 | | JNZ j ⇒ 2 |
---|
| 375 | | JB _ j ⇒ 3 |
---|
| 376 | | JBC _ j ⇒ 3 |
---|
| 377 | | JNB _ j ⇒ 3 |
---|
| 378 | | CJNE _ j ⇒ 3 |
---|
| 379 | | DJNZ x j ⇒ match x with [ REGISTER _ ⇒ 2 | _ ⇒ 3 ] |
---|
| 380 | | _ ⇒ 0 |
---|
| 381 | ]. |
---|
| 382 | |
---|
[2034] | 383 | definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → |
---|
[2316] | 384 | ℕ → preinstruction Identifier → option jump_length ≝ |
---|
| 385 | λlabels.λold_sigma.λinc_sigma.λppc.λi. |
---|
| 386 | let ins_len ≝ length_of i in |
---|
[2225] | 387 | match destination_of i with |
---|
[2316] | 388 | [ Some j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma ppc j ins_len) |
---|
[2225] | 389 | | None ⇒ None ? |
---|
[2034] | 390 | ]. |
---|
| 391 | |
---|
| 392 | (* The first step of the jump expansion: everything to short. *) |
---|
| 393 | definition jump_expansion_start: |
---|
[2141] | 394 | ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
[2034] | 395 | ∀labels:label_map. |
---|
| 396 | Σpolicy:option ppc_pc_map. |
---|
| 397 | match policy with |
---|
| 398 | [ None ⇒ True |
---|
[2152] | 399 | | Some p ⇒ And (And (And (And (And |
---|
| 400 | (not_jump_default (pi1 ?? program) p) |
---|
[2034] | 401 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) |
---|
[2101] | 402 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
[2141] | 403 | (sigma_compact_unsafe program labels p)) |
---|
[2034] | 404 | (∀i.i ≤ |program| → ∃pc. |
---|
| 405 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) |
---|
[2211] | 406 | (\fst p ≤ 2^16) |
---|
[2034] | 407 | ] ≝ |
---|
| 408 | λprogram.λlabels. |
---|
[3098] | 409 | let 〈ignore,final_policy〉 ≝ foldl_strong (option Identifier × pseudo_instruction) |
---|
| 410 | (λprefix.Σacc_policy:Word × ppc_pc_map. |
---|
| 411 | let 〈acc,policy〉 ≝ acc_policy in |
---|
| 412 | And (acc = bitvector_of_nat … (|prefix|)) |
---|
| 413 | (And (And (And (And |
---|
[2152] | 414 | (not_jump_default prefix policy) |
---|
[2034] | 415 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
[2101] | 416 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) |
---|
[2141] | 417 | (sigma_compact_unsafe prefix labels policy)) |
---|
[2034] | 418 | (∀i.i ≤ |prefix| → ∃pc. |
---|
[3098] | 419 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))) |
---|
[2034] | 420 | program |
---|
[3098] | 421 | (λprefix.λx.λtl.λprf.λacc_pol. |
---|
| 422 | let 〈acc,p〉 ≝ pi1 ?? acc_pol in |
---|
| 423 | let 〈pc,sigma〉 ≝ p in |
---|
[2034] | 424 | let 〈label,instr〉 ≝ x in |
---|
| 425 | let isize ≝ instruction_size_jmplen short_jump instr in |
---|
[3098] | 426 | let Sacc ≝ increment … acc in |
---|
| 427 | 〈Sacc,〈pc + isize, bvt_insert … Sacc 〈pc+isize,short_jump〉 sigma〉〉 |
---|
| 428 | ) 〈zero ?,〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉〉 in |
---|
| 429 | if gtb (\fst final_policy) 2^16 then |
---|
[2034] | 430 | None ? |
---|
| 431 | else |
---|
[3098] | 432 | Some ? final_policy. |
---|
[2034] | 433 | [ / by I/ |
---|
[3098] | 434 | | cases (foldl_strong ?(λprefix.Σx.?)???) in p; #pi1 #IS #EQp1 >EQp1 in IS; * |
---|
| 435 | #_ #X % try assumption @not_lt_to_le @ltb_false_to_not_lt @p1 |
---|
| 436 | | cases p in p1; -p #pc #sigma #p1 lapply (pi2 ?? acc_pol) >p1 -acc_pol |
---|
| 437 | normalize nodelta * #EQacc #Hp cases x in prf; #lbl #ins #prf normalize nodelta |
---|
| 438 | % [ >EQacc >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat |
---|
| 439 | >length_append >commutative_plus % |
---|
| 440 | | @conj [ @conj [ @conj [ @conj |
---|
| 441 | [ (* not_jump_default *) #i >append_length <commutative_plus #Hi |
---|
[2034] | 442 | normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 443 | [ >lookup_insert_miss |
---|
[2141] | 444 | [ (* USE[pass]: not_jump_default *) |
---|
[2152] | 445 | lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) |
---|
[2034] | 446 | >nth_append_first |
---|
| 447 | [ #H #H2 @H @H2 |
---|
| 448 | | @Hi |
---|
| 449 | ] |
---|
[3098] | 450 | | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 451 | @bitvector_of_nat_abs |
---|
[2141] | 452 | [ @(transitive_lt ??? Hi) @le_S_to_le] |
---|
| 453 | [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length |
---|
| 454 | <plus_n_Sm @le_S_S @le_plus_n_r |
---|
[2034] | 455 | | @lt_to_not_eq @le_S @Hi |
---|
| 456 | ] |
---|
| 457 | ] |
---|
| 458 | | >Hi >lookup_insert_miss |
---|
[2141] | 459 | [ #_ (* USE: everything is short *) |
---|
| 460 | elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl |
---|
[2034] | 461 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl |
---|
[3098] | 462 | | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 463 | @bitvector_of_nat_abs |
---|
[2141] | 464 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r |
---|
| 465 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S |
---|
[2034] | 466 | @le_plus_n_r |
---|
| 467 | | @lt_to_not_eq @le_n |
---|
| 468 | ] |
---|
| 469 | ] |
---|
| 470 | ] |
---|
[2141] | 471 | | (* 0 ↦ 0 *) |
---|
| 472 | >lookup_insert_miss |
---|
| 473 | [ (* USE[pass]: 0 ↦ 0 *) |
---|
[2152] | 474 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) |
---|
[3098] | 475 | | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 476 | @bitvector_of_nat_abs |
---|
[2316] | 477 | [ @ltb_true_to_lt / by refl/ |
---|
[2141] | 478 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm |
---|
| 479 | @le_S_S @le_plus_n_r |
---|
[2316] | 480 | | @lt_to_not_eq @ltb_true_to_lt / by refl/ |
---|
[2141] | 481 | ] |
---|
| 482 | ] |
---|
| 483 | ] |
---|
| 484 | | (* fst p = pc *) |
---|
[3098] | 485 | >append_length >(commutative_plus (|prefix|)) |
---|
| 486 | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 487 | >lookup_insert_hit @refl |
---|
| 488 | |
---|
[2141] | 489 | ] |
---|
[2034] | 490 | | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
| 491 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
| 492 | [ >lookup_opt_insert_miss |
---|
| 493 | [ >lookup_opt_insert_miss |
---|
[2141] | 494 | [ (* USE[pass]: policy_compact_unsafe *) |
---|
| 495 | lapply (proj2 ?? (proj1 ?? Hp) i Hi) |
---|
[2034] | 496 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) |
---|
| 497 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); |
---|
| 498 | [ #_ normalize nodelta / by / |
---|
| 499 | | #x cases x -x #pci #ji #EQi |
---|
| 500 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma)) |
---|
| 501 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %); |
---|
| 502 | [ #_ normalize nodelta / by / |
---|
| 503 | | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first |
---|
| 504 | [ / by / |
---|
| 505 | | @Hi |
---|
| 506 | ] |
---|
| 507 | ] |
---|
| 508 | ] |
---|
| 509 | ] |
---|
| 510 | ] |
---|
| 511 | [2: lapply (le_S_to_le … Hi) -Hi #Hi] |
---|
[3098] | 512 | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
[2034] | 513 | @bitvector_of_nat_abs |
---|
[2141] | 514 | [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus |
---|
[2034] | 515 | @le_plus_a @Hi |
---|
[2141] | 516 | |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
[2034] | 517 | @le_S_S @le_plus_n_r |
---|
| 518 | |3,6: @lt_to_not_eq @le_S_S @Hi |
---|
| 519 | ] |
---|
| 520 | | >lookup_opt_insert_miss |
---|
[3098] | 521 | [ >Hi |
---|
| 522 | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 523 | >lookup_opt_insert_hit normalize nodelta |
---|
[2141] | 524 | (* USE: everything is short, fst p = pc *) |
---|
| 525 | elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl |
---|
| 526 | lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl |
---|
| 527 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second |
---|
| 528 | [ <minus_n_n whd in match (nth ????); >EQ @refl |
---|
[2034] | 529 | | @le_n |
---|
| 530 | ] |
---|
[3098] | 531 | | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 532 | @bitvector_of_nat_abs |
---|
[2141] | 533 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus |
---|
[2034] | 534 | @le_plus_a @le_n |
---|
[2141] | 535 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
[2034] | 536 | @le_S_S @le_plus_n_r |
---|
| 537 | | @lt_to_not_eq @le_S_S >Hi @le_n |
---|
| 538 | ] |
---|
| 539 | ] |
---|
| 540 | ] |
---|
| 541 | ] |
---|
[2141] | 542 | | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
[2034] | 543 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
| 544 | [ >lookup_opt_insert_miss |
---|
[2141] | 545 | [ (* USE[pass]: everything is short *) |
---|
| 546 | @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) |
---|
[3098] | 547 | | |
---|
| 548 | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 549 | @bitvector_of_nat_abs |
---|
[2141] | 550 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S |
---|
| 551 | >commutative_plus @le_plus_a @le_S_S_to_le @Hi |
---|
| 552 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm |
---|
| 553 | @le_S_S @le_S_S @le_plus_n_r |
---|
[2034] | 554 | | @lt_to_not_eq @Hi |
---|
| 555 | ] |
---|
| 556 | ] |
---|
[3098] | 557 | | >Hi |
---|
| 558 | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat |
---|
| 559 | >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump ins)) |
---|
[2034] | 560 | @refl |
---|
| 561 | ] |
---|
[3098] | 562 | ]] |
---|
| 563 | | normalize nodelta % % [ @conj [ @conj [ @conj |
---|
[2034] | 564 | [ #i cases i |
---|
| 565 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 566 | | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 567 | ] |
---|
[2152] | 568 | ] ] |
---|
[2141] | 569 | >lookup_insert_hit @refl |
---|
[2034] | 570 | | #i cases i |
---|
| 571 | [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n |
---|
| 572 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 573 | ] |
---|
| 574 | ] |
---|
| 575 | | #i cases i |
---|
| 576 | [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl |
---|
| 577 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
| 578 | ] |
---|
| 579 | ] |
---|
| 580 | ] |
---|
| 581 | qed. |
---|
| 582 | |
---|
[2059] | 583 | (* NOTE: we only compare the first elements here because otherwise the |
---|
| 584 | * added = 0 → policy_equal property of jump_expansion_step doesn't hold: |
---|
| 585 | * if we have not added anything to the pc, we only know the PC hasn't changed, |
---|
| 586 | * there might still have been a short/medium jump change *) |
---|
[2101] | 587 | definition sigma_pc_equal ≝ |
---|
[2034] | 588 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
[2101] | 589 | (∀n.n ≤ |program| → |
---|
[2059] | 590 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
| 591 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
| 592 | |
---|
[2101] | 593 | definition sigma_jump_equal ≝ |
---|
[2059] | 594 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
[2101] | 595 | (∀n.n < |program| → |
---|
[2059] | 596 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
| 597 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
[2034] | 598 | |
---|
| 599 | definition nec_plus_ultra ≝ |
---|
| 600 | λprogram:list labelled_instruction.λp:ppc_pc_map. |
---|
[2652] | 601 | ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) → |
---|
[2034] | 602 | \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). |
---|
| 603 | |
---|
| 604 | (*include alias "common/Identifiers.ma".*) |
---|
| 605 | include alias "ASM/BitVector.ma". |
---|
| 606 | include alias "basics/lists/list.ma". |
---|
| 607 | include alias "arithmetics/nat.ma". |
---|
| 608 | include alias "basics/logic.ma". |
---|
| 609 | |
---|
[2141] | 610 | lemma jump_length_equal_max: ∀a,b,i. |
---|
[2034] | 611 | is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → |
---|
| 612 | (max_length a b) = a. |
---|
| 613 | #a #b #i cases i |
---|
| 614 | [1: #pi cases pi |
---|
[2225] | 615 | try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H |
---|
| 616 | cases a in EQ; cases b #EQ try % |
---|
| 617 | try (normalize in EQ; destruct(EQ) @False) |
---|
| 618 | try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False) |
---|
| 619 | lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w |
---|
| 620 | try (#EQ normalize in EQ; destruct(EQ) @False) |
---|
| 621 | @(subaddressing_mode_elim … a1) #w |
---|
| 622 | #EQ normalize in EQ; destruct(EQ) |
---|
[2713] | 623 | |2,3,8: #x [3: #y] #H cases H |
---|
[3039] | 624 | |4,6: #id #_ cases a cases b #H try % normalize in H; destruct(H) |
---|
| 625 | |5,7: #x #y #z #H normalize in H; cases H |
---|
[2225] | 626 | ] |
---|
[2034] | 627 | qed. |
---|
| 628 | |
---|
[2141] | 629 | lemma jump_length_le_max: ∀a,b,i.is_jump i → |
---|
[2034] | 630 | instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. |
---|
| 631 | #a #b #i cases i |
---|
[2713] | 632 | [2,3,8: #x [3: #y] #H cases H |
---|
[3039] | 633 | |4,6: #id #_ cases a cases b @leb_true_to_le / by refl/ |
---|
[2034] | 634 | |1: #pi cases pi |
---|
[2225] | 635 | try (#x #y #H) try (#x #H) try (#H) cases H |
---|
| 636 | -H cases a cases b @leb_true_to_le try % |
---|
| 637 | try (@(subaddressing_mode_elim … x) #w % @False) |
---|
| 638 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % |
---|
| 639 | @(subaddressing_mode_elim … a1) #w % |
---|
[3039] | 640 | |5,7: #x #y #z #H cases H |
---|
[2034] | 641 | ] |
---|
| 642 | qed. |
---|
| 643 | |
---|
[2141] | 644 | lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l). |
---|
[2213] | 645 | ∀old_sigma.∀sigma. |
---|
[2141] | 646 | sigma_pc_equal program old_sigma sigma → |
---|
[2316] | 647 | sigma_jump_equal program old_sigma sigma → |
---|
| 648 | sigma_jumps program old_sigma → |
---|
| 649 | sigma_safe program (create_label_map program) old_sigma sigma → |
---|
[2213] | 650 | sigma_compact_unsafe program (create_label_map program) sigma → |
---|
| 651 | sigma_compact program (create_label_map program) sigma. |
---|
[2316] | 652 | #program cases program -program #program #Hprogram #old_sigma #sigma |
---|
[2318] | 653 | #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #dlbl #i #Hi |
---|
[2316] | 654 | lapply (Hcp_unsafe i Hi) -Hcp_unsafe lapply (Hsafe i Hi) -Hsafe |
---|
[2235] | 655 | inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) |
---|
[3103] | 656 | |
---|
[2141] | 657 | [ / by / |
---|
[2316] | 658 | | #x cases x -x #pc #jl #EQ |
---|
| 659 | inversion (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) |
---|
[2141] | 660 | [ / by / |
---|
[2316] | 661 | | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hsafe #Hcp_unsafe |
---|
[2235] | 662 | (*CSC: make a lemma here; to shorten the proof, reimplement the |
---|
| 663 | safe case so that it also does a pattern matching on the jump_length |
---|
| 664 | type *) |
---|
[2316] | 665 | cut (instruction_size_jmplen jl |
---|
[2652] | 666 | (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) = |
---|
[2141] | 667 | instruction_size … (bitvector_of_nat ? i) |
---|
[2652] | 668 | (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) |
---|
[2316] | 669 | [6: #H <H @Hcp_unsafe |
---|
| 670 | |5: whd in match (instruction_size_jmplen ??); |
---|
| 671 | whd in match (instruction_size …); |
---|
[2141] | 672 | whd in match (assembly_1_pseudoinstruction …); |
---|
| 673 | whd in match (expand_pseudo_instruction …); |
---|
[2652] | 674 | normalize nodelta inversion (nth i ? program 〈None ?,Comment EmptyString〉) in Hsafe; |
---|
[2141] | 675 | #lbl #instr cases instr |
---|
[2316] | 676 | [1: #pi normalize nodelta cases pi |
---|
| 677 | try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe) |
---|
| 678 | try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id |
---|
[3039] | 679 | |2,3,5: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ % |
---|
[3078] | 680 | |7: * |
---|
| 681 | [ #x @(subaddressing_mode_elim … x) |
---|
| 682 | | * #x @(subaddressing_mode_elim … x) [2,3: #y] * |
---|
| 683 | ] normalize nodelta #lbl #off #_ #_ |
---|
| 684 | @pair_elim * #addr normalize nodelta #_ % |
---|
| 685 | ] |
---|
[2316] | 686 | #id lapply (Hpc_equal i (le_S_to_le … Hi)) |
---|
| 687 | lapply (Hpc_equal (S i) Hi) |
---|
| 688 | lapply (Hjump_equal i Hi) |
---|
| 689 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #jeq #OSeq #Oeq #Hnth_eq #Hsafe |
---|
| 690 | lapply (Hsafe id (refl ? id)) -Hsafe normalize nodelta |
---|
| 691 | whd in match expand_relative_jump; |
---|
| 692 | whd in match expand_relative_jump_internal; normalize nodelta |
---|
[2141] | 693 | >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O |
---|
[2316] | 694 | >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) in OSeq; #OSeq >Hcp_unsafe |
---|
| 695 | inversion (leb (lookup_def … (create_label_map program) id 0) i) #Hli |
---|
| 696 | normalize nodelta |
---|
| 697 | [1,3,5,7,9,11,13,15,17,19,21: (* JC JNC JB JNB JBC JZ JNZ CJNE DJNZ Jmp Call *) |
---|
| 698 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
| 699 | cases jl in jeq; normalize nodelta #jeq |
---|
| 700 | [2,5,8,11,14,17,20,23,26: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs |
---|
| 701 | cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute reljmps *) |
---|
| 702 | |31: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs |
---|
| 703 | cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *) |
---|
| 704 | |28: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold; |
---|
| 705 | #sj_poss #disp #Hold normalize nodelta >Hold normalize nodelta % |
---|
| 706 | |1,4,7,10,13,16,19,22,25: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold; |
---|
| 707 | #sj_poss #disp #Hold normalize nodelta >Hold |
---|
| 708 | try % try (@(subaddressing_mode_elim … x) #w %) |
---|
| 709 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % |
---|
| 710 | @(subaddressing_mode_elim … a1) #w % |
---|
| 711 | |3,6,9,12,15,18,21,24,27: >Hnth_eq #_ whd in match (jmpeqb ??); |
---|
| 712 | cases (short_jump_cond ??); #sj_poss #disp normalize nodelta |
---|
| 713 | cases sj_poss normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %) |
---|
| 714 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % |
---|
| 715 | @(subaddressing_mode_elim … a1) #w % |
---|
| 716 | |29,32: >Hnth_eq #Hold cases (absolute_jump_cond ??) in Hold; |
---|
| 717 | #aj_poss #disp #Hold >Hold normalize nodelta |
---|
| 718 | cases (short_jump_cond ??); |
---|
| 719 | [1,2: #sj_poss #disp2 normalize nodelta cases sj_poss % |
---|
| 720 | |3,4: @(zero 16) |
---|
[2221] | 721 | ] |
---|
[2316] | 722 | |30,33: >Hnth_eq #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??); |
---|
| 723 | #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??); |
---|
| 724 | [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss % |
---|
| 725 | |3,4: @(zero 16) (* where does this come from? *) |
---|
[2141] | 726 | ] |
---|
| 727 | ] |
---|
[2316] | 728 | |*: cases (lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) in Oeq jeq; |
---|
| 729 | #opc #ojl #Oeq #jeq normalize nodelta |
---|
| 730 | cases (lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉) in OSeq; |
---|
| 731 | #oSpc #oSjl #OSeq normalize nodelta >jeq |
---|
| 732 | >OSeq >Hcp_unsafe -Hcp_unsafe >Hnth_eq lapply (Hpc_equal (lookup_def … (create_label_map program) id 0) ?) |
---|
| 733 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 734 | @(le_S_to_le … (pi2 ?? (create_label_map program) id ?)) |
---|
| 735 | cut (i < 2^16) |
---|
| 736 | [1,3,5,7,9,11,13,15,17,19,21: |
---|
| 737 | @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] #Hi2 |
---|
| 738 | @(proj2 ?? ((proj2 ?? Hprogram) id (bitvector_of_nat ? i) ???)) |
---|
| 739 | [1,5,9,13,17,21,25,29,33,37,41: |
---|
| 740 | whd in match fetch_pseudo_instruction; normalize nodelta |
---|
[2652] | 741 | >(nth_safe_nth … 〈None ?, Comment EmptyString〉) >nat_of_bitvector_bitvector_of_nat_inverse |
---|
[2316] | 742 | [1: >Hnth_eq in ⊢ (??%?); |
---|
| 743 | |3: >Hnth_eq in ⊢ (??%?); |
---|
| 744 | |5: >Hnth_eq in ⊢ (??%?); |
---|
| 745 | |7: >Hnth_eq in ⊢ (??%?); |
---|
| 746 | |9: >Hnth_eq in ⊢ (??%?); |
---|
| 747 | |11: >Hnth_eq in ⊢ (??%?); |
---|
| 748 | |13: >Hnth_eq in ⊢ (??%?); |
---|
| 749 | |15: >Hnth_eq in ⊢ (??%?); |
---|
| 750 | |17: >Hnth_eq in ⊢ (??%?); |
---|
| 751 | |19: >Hnth_eq in ⊢ (??%?); |
---|
| 752 | |21: >Hnth_eq in ⊢ (??%?); ] |
---|
| 753 | [1,2,3,4,5,6,7,8,9,10,11: % |
---|
| 754 | |*: assumption] |
---|
| 755 | |3,7,11,15,19,23,27,31,35,39,43: |
---|
| 756 | >nat_of_bitvector_bitvector_of_nat_inverse assumption |
---|
| 757 | |4,8,12,16,20,24,28,32,36,40,44: % |
---|
| 758 | ] |
---|
| 759 | |*: #Hpc lapply (Hjumps i Hi) >Hnth_eq >(Hjump_equal i Hi) |
---|
| 760 | >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
| 761 | cases jl normalize nodelta |
---|
| 762 | [31: #abs cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *) |
---|
| 763 | |2,5,8,11,14,17,20,23,26: #abs cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute RJs *) |
---|
| 764 | |1,4,7,10,13,16,19,22,25,28: |
---|
| 765 | >Hpc cases (short_jump_cond ??); #sj_poss #disp #_ #H normalize nodelta |
---|
| 766 | >H normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %) |
---|
| 767 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % |
---|
| 768 | @(subaddressing_mode_elim … a1) #w % |
---|
| 769 | |3,6,9,12,15,18,21,24,27: >Hpc #_ #_ cases (short_jump_cond ??); |
---|
| 770 | #sj_poss #disp normalize nodelta normalize nodelta |
---|
| 771 | whd in match (jmpeqb ??); cases sj_poss |
---|
| 772 | try % try (@(subaddressing_mode_elim … x) #w %) |
---|
| 773 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % |
---|
| 774 | @(subaddressing_mode_elim … a1) #w % |
---|
| 775 | |29,32: >Hpc #_ #Hold cases (absolute_jump_cond ??) in Hold; |
---|
| 776 | #aj_poss #disp #Hold >Hold normalize nodelta cases (short_jump_cond ??) |
---|
| 777 | [1,2: #sj_poss #disp2 cases sj_poss normalize nodelta % |
---|
| 778 | |3,4: @(zero 16) |
---|
[2221] | 779 | ] |
---|
[2316] | 780 | |30,33: >Hnth_eq #_ #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??); |
---|
| 781 | #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??); |
---|
| 782 | [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss % |
---|
| 783 | |3,4: @(zero 16) |
---|
| 784 | ] |
---|
[2221] | 785 | ] |
---|
[2213] | 786 | ] |
---|
[2316] | 787 | ] |
---|
| 788 | ] |
---|
| 789 | ] |
---|
| 790 | ] |
---|
[3103] | 791 | |
---|
[2152] | 792 | qed. |
---|
| 793 | |
---|
| 794 | lemma instruction_size_irrelevant: ∀i. |
---|
| 795 | ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i. |
---|
| 796 | #i cases i |
---|
[3039] | 797 | [2,3: #x [3: #y] #Hj #j1 #j2 % |
---|
| 798 | |5,7: #x #y #z #_ #j1 #j2 % |
---|
| 799 | |4,6: #x #Hi cases Hi |
---|
[2225] | 800 | |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2) |
---|
| 801 | try % cases Hj ] |
---|
[2713] | 802 | qed. |
---|