Changeset 1933


Ignore:
Timestamp:
May 10, 2012, 12:00:21 PM (7 years ago)
Author:
boender
Message:
  • slight revamp
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1932 r1933  
    509509  ∀labels:label_map.
    510510  Σpolicy:ppc_pc_map.
    511     And (out_of_program_none (pi1 ?? program) policy)
    512     (jump_in_policy (pi1 ?? program) policy) ≝
     511    And (And (out_of_program_none (pi1 ?? program) policy)
     512    (jump_in_policy (pi1 ?? program) policy))
     513    (policy_isize_sum (pi1 ?? program) labels policy) ≝
    513514  λprogram.λlabels.
    514515  foldl_strong (option Identifier × pseudo_instruction)
    515   (λprefix.Σpolicy:ppc_pc_map.
    516     (And (out_of_program_none prefix policy)
    517     (jump_in_policy prefix policy)))
     516  (λprefix.Σpolicy:ppc_pc_map. 
     517    And (And (out_of_program_none prefix policy)
     518    (jump_in_policy prefix policy))
     519    (policy_isize_sum prefix labels policy))
    518520  program
    519521  (λprefix.λx.λtl.λprf.λp.
     
    540542   ]〉
    541543  ) 〈0, Stub ? ?〉.
    542 [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
     544[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    543545  [ #Hi2
    544546    cases (le_to_or_lt_eq … Hi) -Hi #Hi
     
    558560            ]
    559561          ]
    560           @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     562          @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    561563        |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
    562564          [1,2,3,6,7,24,25: #x #y
     
    573575            ]
    574576          ]
    575           <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     577          <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    576578          >Hi @Hi2
    577579        |9,10,11,12,13,14,15,16,17:
     
    583585            ]
    584586          |1,3,5,7,9,11,13,15,17:
    585             @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     587            @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    586588          ]
    587589        |46,47,48,49,50,51,52,53,54:
     
    593595            ]
    594596          |1,3,5,7,9,11,13,15,17:
    595             @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
     597            @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
    596598          ]
    597599        ]
     
    605607          ]
    606608        ]
    607         [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     609        [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    608610        |2,5,6:
    609           <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     611          <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    610612          >Hi @Hi2
    611613        ]
     
    618620          |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
    619621          ]         
    620         |1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    621         |5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
     622        |1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     623        |5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
    622624        ]
    623625      ]
     
    691693            ]
    692694          ]
    693           @(proj1 ?? (proj2 ?? Hp i (le_S_S_to_le … Hi)) Hj)
    694         | #H @(proj2 ?? (proj2 ?? (pi2 ?? p) i (le_S_S_to_le … Hi)))
     695          @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj)
     696        | #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi)))
    695697          cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    696698          [1: #id cases id
     
    781783        ]
    782784      |2,3,6: #x [3: #id] @conj
    783         [1,3,5: #H @⊥ @H
     785        [1,3,5: #H cases H
    784786        |2,4,6:
    785787          cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p
    786788          normalize nodelta >lookup_insert_hit #H destruct (H)
    787           (* [1,3,5: #_ #H destruct (H)
    788           |2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    789             @le_S_S_to_le @le_plus_n_r
    790           ] *)
    791789        ]
    792790      |4,5: #x @conj
     
    798796    ]
    799797  ]
     798| cases daemon
     799]
    800800| @conj
    801   [ #i #_ #Hi2 / by refl/
    802   | #i #_ @conj
    803     [ >nth_nil #H @⊥ @H
    804     | #H elim H -H #p >lookup_stub #H destruct (H)
    805     ]
     801  [ @conj
     802    [#i #_ #Hi2 / by refl/
     803    | #i #_ @conj
     804      [ >nth_nil #H @⊥ @H
     805      | #H elim H -H #p >lookup_stub #H destruct (H)
     806      ]
     807    ]
     808  | whd in match policy_isize_sum; normalize nodelta
     809    cases daemon
    806810  ]
    807811]
     
    889893      ] in
    890894      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    891       let 〈old_pc, old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉 in
    892       match add_instr with
    893       [ None ⇒
    894         let isize ≝ instruction_size_jmplen short_jump instr in
    895         (* instruction is not a jump: nothing changes *)
    896         〈inc_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈inc_pc, None ?〉 inc_sigma〉〉   
    897       | Some proj_length ⇒
    898         let x ≝ match old_length with
    899         [ None ⇒ (* this should not happen! *) short_jump
    900         | Some y ⇒ y
    901         ] in
    902         let new_length ≝ max_length x proj_length in
    903         let old_size ≝ instruction_size_jmplen x instr in
    904         let isize ≝ instruction_size_jmplen new_length instr in
    905         〈plus inc_added (minus isize old_size), 〈plus inc_pc isize,
    906          bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈inc_pc, Some ? new_length〉 inc_sigma〉〉
    907       ]
     895      let 〈old_pc, ol〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉 in
     896      let old_length ≝ match ol with
     897      [ None   ⇒ short_jump
     898      | Some x ⇒ x
     899      ] in
     900      let old_size ≝ instruction_size_jmplen old_length instr in
     901      let 〈new_length, isize〉 ≝ match add_instr with
     902      [ None    ⇒ 〈None ?, instruction_size_jmplen short_jump instr〉
     903      | Some pl ⇒ 〈Some ? (max_length old_length pl), instruction_size_jmplen (max_length old_length pl) instr〉
     904      ] in
     905      let new_added ≝ match add_instr with
     906      [ None   ⇒ inc_added
     907      | Some x ⇒ plus inc_added (minus isize old_size)
     908      ] in
     909      〈new_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma〉〉
    908910    ) 〈0, 〈0, Stub ??〉〉 in
    909911    if geb (\fst final_policy) 2^16 then
     
    920922  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    921923  ]
    922 | (* XXX complicated proof *) cases daemon 
     924| lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
     925  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉)
     926  #old_pc #old_length normalize nodelta
     927(* XXX complicated proof *) cases daemon 
    923928| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    924929  [ #i #Hi / by refl/
     
    13541359        (jump_in_policy program x))
    13551360        (policy_isize_sum program (create_label_map program) x))
    1356        
    13571361        (\fst x < 2^16)
    13581362    ]) ≝
     
    13691373  ].
    13701374[ normalize nodelta @conj
    1371   [ @conj
    1372     [ @(pi2 ?? (jump_expansion_start program (create_label_map program)))
    1373     | (* XXX *) cases daemon
    1374     ]
     1375  [ @(pi2 ?? (jump_expansion_start program (create_label_map program)))
    13751376  | (* XXX *) cases daemon
    13761377  ]
Note: See TracChangeset for help on using the changeset viewer.