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