source: src/ASM/PolicyFront.ma @ 3078

Last change on this file since 3078 was 3078, checked in by tranquil, 6 years ago

fixed change of Mov

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