Changeset 2078 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jun 14, 2012, 11:44:46 AM (7 years ago)
Author:
sacerdot
Message:

sigma_policy_specification has been
1) strengthened
2) made nicer to see
3) moved to Assembly.ma
4) used into Policy

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2059 r2078  
    628628
    629629(* The glue between Policy and Assembly. *)
     630(*CSC: modified to really use the specification in Assembly.ma.
     631  I have modified all that follows in vi without testing it in Matita.
     632  Jaap, please repair it *)
    630633definition jump_expansion':
    631634∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    632  option (Σsigma:Word → Word × bool.
    633    ∀ppc: Word. ∀ppc_ok.
    634    let pc ≝ \fst (sigma ppc) in
    635    let labels ≝ \fst (create_label_cost_map (\snd program)) in
    636    let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
    637    let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    638    let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    639      And (nat_of_bitvector … ppc ≤ |\snd program| →
    640        next_pc = add ? pc (bitvector_of_nat …
    641          (instruction_size lookup_labels (λx.\fst (sigma x)) (λx.\snd (sigma x)) ppc instruction)))
    642       (Or (nat_of_bitvector … ppc < |\snd program| →
    643         nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    644        (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))) ≝
     635 option (Σsigma_policy:(Word → Word) × (Word → bool).
     636   let 〈sigma,policy〉≝ sigma_policy in
     637   sigma_policy_specification program sigma policy
     638
    645639 λprogram.
    646640  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     
    648642  [ None ⇒ None ?
    649643  | Some x ⇒ Some ?
    650       «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    651         〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
     644      «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     645          bitvector_of_nat 16 pc),
     646         (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     647          jmpeqb jl long_jump)〉,?»
    652648  ].
    653649 #ppc normalize nodelta cases daemon
Note: See TracChangeset for help on using the changeset viewer.