Changeset 2078 for src/ASM/Policy.ma
 Timestamp:
 Jun 14, 2012, 11:44:46 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2059 r2078 628 628 629 629 (* 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 *) 630 633 definition jump_expansion': 631 634 ∀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 ≝ 645 639 λprogram. 646 640 let policy ≝ pi1 … (je_fixpoint (\snd program)) in … … 648 642 [ None ⇒ None ? 649 643  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)〉,?» 652 648 ]. 653 649 #ppc normalize nodelta cases daemon
Note: See TracChangeset
for help on using the changeset viewer.