Changeset 2264 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (7 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2221 r2264  
    582582
    583583 
    584 (* label_map: identifier ↦ pseudo program counter *)
    585 definition label_map ≝ identifier_map ASMTag ℕ.
    586 
    587584(* Labels *)
    588585definition is_label ≝
     
    617614   ]
    618615 ]
    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 in
    625     ∀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 in
    634     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   program
    640   (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
    641    let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
    642    let 〈label,instr〉 ≝ x in
    643    let labels ≝
    644      match label with
    645      [ None   ⇒ labels
    646      | Some l ⇒ add … labels l ppc
    647      ] in
    648    let costs ≝
    649      match instr with
    650      [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
    651      | _ ⇒ costs ] in
    652       〈labels,costs,S ppc〉
    653    ) 〈(empty_map …),(Stub ??),0〉)).
    654 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
    655   -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 nodelta
    658    >occurs_exactly_once_None in Hocc; @(IH2 lbl)
    659  | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
    660    [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj
    661      [ >address_of_word_labels_code_mem_Some_hit
    662        [ >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_r
    666      ]
    667    | #Hneq #Hocc lapply (IH2 lbl ?)
    668      [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //
    669      | #IH3 @conj
    670        [ <address_of_word_labels_code_mem_Some_miss
    671          [ >lookup_def_add_miss
    672            [ @(proj1 ?? IH3)
    673            | % @neq_identifier_neq @Hneq
    674            ] 
    675          | @Hocc
    676          | >eq_identifier_sym @Hneq
    677          ]
    678        | >lookup_def_add_miss
    679          [ @(proj2 ?? IH3)
    680          | % @neq_identifier_neq @Hneq
    681          ]
    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 @H
    690 ]
    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) in
    702     ∀id. occurs_exactly_once ??  id (\snd pseudo_program) → And
    703      (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 ?); @pi2
    706616qed.
    707617
Note: See TracChangeset for help on using the changeset viewer.