Changeset 2048 for src/ASM/PolicyFront.ma
 Timestamp:
 Jun 12, 2012, 2:46:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2047 r2048 324 324 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added 325 325 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 326 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 327 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 328 if eq_bv ? upper (zero 8) 326 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 327 if sj_possible 329 328 then short_jump 330 329 else long_jump. … … 336 335 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 337 336 let paddr ≝ lookup_def ? ? labels lbl 0 in 338 let addr ≝ 339 if leb ppc paddr (* forward jump *)337 let addr ≝ bitvector_of_nat ? 338 (if leb ppc paddr (* forward jump *) 340 339 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) 341 340 + added 342 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in 343 let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in 344 let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 345 if eq_bv ? fst_5_addr fst_5_pc 341 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 342 let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in 343 if mj_possible 346 344 then medium_jump 347 345 else long_jump. … … 356 354 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added 357 355 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 358 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 359 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 360 if eq_bv ? upper (zero 8) 356 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 357 if sj_possible 361 358 then short_jump 362 359 else select_call_length labels old_sigma inc_sigma added ppc lbl. … … 644 641 definition policy_equal ≝ 645 642 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 646 (* \fst p1 = \fst p2 ∧ *) 647 (∀n:ℕ.n < program → 648 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in 649 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in 650 \snd pc1 = \snd pc2). 643 (∀n:ℕ.n ≤ program → 644 bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 = 645 bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉). 651 646 652 647 definition nec_plus_ultra ≝ … … 745 740 qed. 746 741 747 (* (Intermediate) policy safety *) 748 definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝ 749 λpc_plus_jmp_length.λaddr.λinstr. 750 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 751 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 752 if flags then 753 eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true 754 else 755 eq_bv 8 upper (zero 8) = true. 756 757 definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝ 758 λpc_plus_jmp_length.λaddr.λinstr. 759 let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in 760 let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in 761 eq_bv 5 fst_5_addr fst_5_pc = true. 762 763 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 764 λprogram.λlabels.λsigma. 742 definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝ 743 λprogram.λlabels.λadded.λold_sigma.λsigma. 765 744 ∀i.i < program → 766 745 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in … … 769 748 ∀dest.is_jump_to instr dest → 770 749 let paddr ≝ lookup_def … labels dest 0 in 771 let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in 750 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *) 751 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added 752 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in 772 753 match j with 773 [ short_jump ⇒ short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_call instr 774  medium_jump ⇒ medium_jump_cond pc_plus_jmp_length addr instr ∧ 775 ¬short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_relative_jump instr 776  long_jump ⇒ ¬short_jump_cond pc_plus_jmp_length addr instr ∧ 777 ¬medium_jump_cond pc_plus_jmp_length addr instr 754 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 755 ¬is_call instr 756  medium_jump ⇒ \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧ 757 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 758 ¬is_relative_jump instr 759  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 760 \fst (medium_jump_cond pc_plus_jmp_length addr) = false 778 761 ]. 779 762
Note: See TracChangeset
for help on using the changeset viewer.