Changeset 1268


Ignore:
Timestamp:
Sep 26, 2011, 2:52:22 PM (8 years ago)
Author:
sacerdot
Message:

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

Location:
src
Files:
1 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1264 r1268  
    11include "ASM/Util.ma".
    22include "utilities/BitVectorTrieSet.ma".
    3 include "utilities/IdentifierTools.ma".
    43include "LIN/LIN.ma".
    54
     
    9493      [ joint_instr_extension ext ⇒ ⊥
    9594      | joint_instr_comment comment ⇒ Comment comment
    96       | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     95      | joint_instr_cost_label lbl ⇒ Cost (word_of_identifier ? lbl)
    9796      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
    9897      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
     
    247246qed.
    248247
     248(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
     249definition ident_of_label: label → ident ≝
     250 λl. an_identifier … (word_of_identifier … l).
     251
    249252definition build_translated_statement ≝
    250253  λglobals.
     
    252255  λprf.
    253256  λstatement: lin_statement globals_old.
    254     〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
     257    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
    255258
    256259definition translate_code ≝
     
    269272    //
    270273  | #G2 #G02 #IH (* CSC: understand here *)
    271     whd in ⊢ (% → %)
    272     normalize in ⊢ (% → %)
    273     //
    274   ]
     274    whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta
     275    cases (\fst G2) normalize // ]
    275276qed.
    276277
    277278definition translate_fun_def ≝
    278   λglobals.
     279  λglobals: list (ident × nat).
    279280  λglobals_old.
    280281  λprf.
    281   λid_def: ? × (fundef … (Σcode:list (lin_statement globals_old).?)).
     282  λid_def.
    282283    let 〈id, def〉 ≝ id_def in
    283284    match def with
    284     [ Internal code_proof ⇒
     285    [ Internal int ⇒
     286      let code_proof ≝ joint_if_code … (lin_params globals_old) int in
    285287      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    286288      [ nil ⇒ λprf2. ⊥
     
    307309  λfuncts.
    308310  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    309    preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     311   preamble @
     312    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
    310313
    311314(*CSC: region silently thrown away here *)
     
    320323  in
    321324    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    322      
     325
    323326(* dpm: plays the role of the string "_exit" in the O'caml source *)
    324 axiom identifier_prefix: Identifier.
     327axiom identifier_prefix: Word.
     328(*CSC: XXXXXXX wrong anyway since labels from different functions can now
     329  clash with each other and with names of functions *)
     330axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
    325331
    326332(* dpm: fresh prefix stuff needs unifying with brian *)
     
    328334  λp.
    329335  let prog_lbls ≝ program_labels … p in
    330   let exit_label ≝ ?(*fresh_prefix … prog_lbls identifier_prefix*) in
     336  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    331337  let global_addr ≝ globals_addr (prog_vars … p) in
    332338  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
    333     〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) ?(*(prog_funct ?? p)*)〉.
    334 [ generalize in match (prog_funct ?? p) #X whd in X:(?(??%)) whd in X:(?(??(?%)))
    335 | #i normalize nodelta whd in match prog_var_names normalize nodelta elim (prog_vars … p)
    336   [ // | #hd #tl #H1 #H2 normalize in ⊢ (???(????%))   
     339    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
     340 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
     341 normalize in match prog_var_names normalize nodelta
     342 elim (prog_vars … p) //
     343 #hd #tl #IH whd in ⊢ (% → %)
     344 whd in match globals_addr normalize nodelta
     345 whd in match (foldl ???? (hd::tl)) normalize nodelta
     346 cases hd * #id #reg #size normalize nodelta
     347 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
     348qed.
  • src/common/AST.ma

    r1225 r1268  
    3838definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
    3939
    40 (* XXX backend is currently using untagged words as identifiers. *)
    41 definition Identifier ≝ Word.
    42 
    4340definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
    4441
     
    675672| Compare_LessEqual: Compare
    676673| Compare_GreaterEqual: Compare.
    677 
    678 (* XXX unused definitions
    679 inductive Cast: Type[0] ≝
    680   Cast_Int: Byte → Cast
    681 | Cast_AddrSymbol: Identifier → Cast
    682 | Cast_StackOffset: Immediate → Cast.
    683 
    684 inductive Data: Type[0] ≝
    685   Data_Reserve: nat → Data
    686 | Data_Int8: Byte → Data
    687 | Data_Int16: Word → Data.
    688 
    689 inductive DataSize: Type[0] ≝
    690   DataSize_Byte: DataSize
    691 | DataSize_HalfWord: DataSize
    692 | DataSize_Word: DataSize.
    693 *)
    694 
    695 definition Trace ≝ list Identifier.
    696674
    697675inductive op1: Type[0] ≝
  • src/common/CostLabel.ma

    r757 r1268  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    9 
    10 (* dpm: fix identifier/costlabel mismatch *)
    11 axiom Identifier_of_costlabel: costlabel → Identifier.
Note: See TracChangeset for help on using the changeset viewer.