 Timestamp:
 Jun 12, 2012, 2:46:54 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2047 r2048 14 14  medium_jump: jump_length 15 15  long_jump: jump_length. 16 17 (* Functions that define the conditions under which jumps are possible *) 18 definition short_jump_cond: Word → Word → (*pseudo_instruction →*) 19 bool × (BitVector 8) ≝ 20 λpc_plus_jmp_length.λaddr.(*λinstr.*) 21 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 22 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 23 if get_index' ? 2 0 flags then 24 〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉 25 else 26 〈eq_bv 8 upper (zero 8), zero 8〉. 27 28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*) 29 bool × (BitVector 11) ≝ 30 λpc_plus_jmp_length.λaddr.(*λinstr.*) 31 let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in 32 let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in 33 〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉. 16 34 17 35 definition assembly_preinstruction ≝ … … 430 448 let lookup_address ≝ sigma (lookup_labels lbl) in 431 449 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 432 let 〈 result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length falsein433 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in434 if eq_bv ? upper (zero 8)then435 let address ≝ RELATIVE lowerin450 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 451 if sj_possible 452 then 453 let address ≝ RELATIVE disp in 436 454 [ RealInstruction (i address) ] 437 455 else … … 535 553  Comment comment ⇒ [ ] 536 554  Call call ⇒ 537 let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in538 555 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 556 let lookup_address ≝ sigma (lookup_labels call) in 557 let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in 539 558 let do_a_long ≝ policy ppc in 540 let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 541 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then 542 let address ≝ ADDR11 resta in 559 if mj_possible ∧ ¬ do_a_long then 560 let address ≝ ADDR11 disp in 543 561 [ ACALL address ] 544 562 else 545 let address ≝ ADDR16 (sigma (lookup_labels call))in563 let address ≝ ADDR16 lookup_address in 546 564 [ LCALL address ] 547 565  Mov d trgt ⇒ … … 553 571 let do_a_long ≝ policy ppc in 554 572 let lookup_address ≝ sigma (lookup_labels jmp) in 555 let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in 556 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 557 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then 558 let address ≝ RELATIVE lower in 573 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in 574 if sj_possible ∧ ¬ do_a_long then 575 let address ≝ RELATIVE disp in 559 576 [ SJMP address ] 560 577 else 561 let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in 562 let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 563 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 564 let address ≝ ADDR11 rest_addr in 578 let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in 579 if mj_possible ∧ ¬ do_a_long then 580 let address ≝ ADDR11 disp2 in 565 581 [ AJMP address ] 566 582 else 
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.