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