Changeset 2264 for src/ASM/Assembly.ma
- Timestamp:
- Jul 26, 2012, 12:38:42 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2221 r2264 582 582 583 583 584 (* label_map: identifier ↦ pseudo program counter *)585 definition label_map ≝ identifier_map ASMTag ℕ.586 587 584 (* Labels *) 588 585 definition is_label ≝ … … 617 614 ] 618 615 ] 619 qed.620 621 (* The function that creates the label-to-address map *)622 definition create_label_cost_map0: ∀program:list labelled_instruction.623 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)624 let 〈labels,costs〉 ≝ labels_costs in625 ∀l.occurs_exactly_once ?? l program →626 And (bitvector_of_nat ? (lookup_def ?? labels l 0) =627 address_of_word_labels_code_mem program l)628 (lookup_def ?? labels l 0 < |program|)629 ) ≝630 λprogram.631 \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)632 (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.633 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in634 ppc = |prefix| ∧635 ∀l.occurs_exactly_once ?? l prefix →636 And (bitvector_of_nat ? (lookup_def ?? labels l 0) =637 address_of_word_labels_code_mem prefix l)638 (lookup_def ?? labels l 0 < |program|))639 program640 (λprefix.λx.λtl.λprf.λlabels_costs_ppc.641 let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in642 let 〈label,instr〉 ≝ x in643 let labels ≝644 match label with645 [ None ⇒ labels646 | Some l ⇒ add … labels l ppc647 ] in648 let costs ≝649 match instr with650 [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs651 | _ ⇒ costs ] in652 〈labels,costs,S ppc〉653 ) 〈(empty_map …),(Stub ??),0〉)).654 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2655 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]656 inversion label [#EQ | #l #EQ]657 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta658 >occurs_exactly_once_None in Hocc; @(IH2 lbl)659 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)660 [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj661 [ >address_of_word_labels_code_mem_Some_hit662 [ >IH1 >lookup_def_add_hit %663 | <(eq_identifier_eq … Heq) in Hocc; //664 ]665 | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r666 ]667 | #Hneq #Hocc lapply (IH2 lbl ?)668 [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //669 | #IH3 @conj670 [ <address_of_word_labels_code_mem_Some_miss671 [ >lookup_def_add_miss672 [ @(proj1 ?? IH3)673 | % @neq_identifier_neq @Hneq674 ]675 | @Hocc676 | >eq_identifier_sym @Hneq677 ]678 | >lookup_def_add_miss679 [ @(proj2 ?? IH3)680 | % @neq_identifier_neq @Hneq681 ]682 ]683 ]684 ]685 ]686 | @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %687 #l #abs cases (abs)688 | cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *689 #_ #H @H690 ]691 qed.692 693 (* The function that creates the label-to-address map *)694 definition create_label_cost_map: ∀program:list labelled_instruction.695 label_map × (BitVectorTrie costlabel 16) ≝696 λprogram.697 pi1 … (create_label_cost_map0 program).698 699 theorem create_label_cost_map_ok:700 ∀pseudo_program: pseudo_assembly_program.701 let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in702 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → And703 (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)704 (lookup_def ?? labels id 0 < |\snd pseudo_program|).705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2706 616 qed. 707 617
Note: See TracChangeset
for help on using the changeset viewer.