Changeset 1515 for src/LIN


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1379 r1515  
    3333    [ sequential instr' _ ⇒
    3434      match instr' with
    35       [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    36       | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | _ ⇒ set_empty ?
     35      [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     36      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
     37      | _ ⇒
    3838      ]
    39     | RETURN ⇒ set_empty ?
    40     | GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
     39    | RETURN ⇒
     40    | GOTO lbl ⇒ {(toASM_ident ? lbl)} ]
    4141  in
    4242  match label with
    4343  [ None ⇒ generated
    44   | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
     44  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
    4545  ].
    4646
    4747definition function_labels_internal ≝
    4848  λglobals: list ident.
    49   λlabels: BitVectorTrieSet ?.
     49  λlabels: identifier_set ?.
    5050  λstatement: lin_statement globals.
    51     set_union ? labels (statement_labels globals statement).
     51    labels ∪ (statement_labels globals statement).
    5252
    5353(* dpm: A = Identifier *)
    54 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
     54definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
    5555  λA: Type[0].
    5656  λglobals: list ident.
    5757  λf: A × (lin_function globals).
    5858  let 〈ignore, fun_def〉 ≝ f in
    59   match fun_def return λ_. BitVectorTrieSet ? with
     59  match fun_def return λ_. identifier_set ? with
    6060  [ Internal stmts ⇒
    61       foldl ? ? (function_labels_internal globals) (set_empty ?) (joint_if_code ?? stmts)
    62   | External _ ⇒ set_empty ?
     61      foldl ? ? (function_labels_internal globals) (joint_if_code ?? stmts)
     62  | External _ ⇒
    6363  ].
    6464 
    65 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
     65definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
    6666  λA: Type[0].
    6767  λglobals: list ident.
    68   λlabels: BitVectorTrieSet ?.
     68  λlabels: identifier_set ?.
    6969  λfunct: A × (lin_function globals).
    70     set_union ? labels (function_labels ? globals funct).
     70    labels ∪ (function_labels ? globals funct).
    7171
    7272(* CSC: here we are silently throwing away the region information *)
     
    7474 λprogram: lin_program.
    7575    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
    76               (set_empty …) (prog_funct … program).
     76              (prog_funct … program).
    7777 
    7878definition data_of_int ≝ λbv. DATA bv.
     
    8686  λstatement: pre_lin_statement globals_old.
    8787  match statement with
    88   [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
     88  [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    8989  | RETURN ⇒ Instruction (RET ?)
    9090  | sequential instr _ ⇒
     
    9292      [ extension ext ⇒ ⊥
    9393      | COMMENT comment ⇒ Comment comment
    94       | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
     94      | COST_LABEL lbl ⇒ Cost (toASM_ident ? lbl)
    9595      | POP _ ⇒ Instruction (POP ? accumulator_address)
    9696      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    9797      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    98       | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
     98      | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    9999      | OPACCS accs _ _ _ _ ⇒
    100100        match accs with
     
    236236      | COND _ lbl ⇒
    237237        (* dpm: this should be handled in translate_code! *)
    238         Instruction (JNZ ? (word_of_identifier ? lbl))
     238        Instruction (JNZ ? (toASM_ident ? lbl))
    239239      | SET_CARRY ⇒
    240240        Instruction (SETB ? CARRY)
     
    246246
    247247(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
    248 definition ident_of_label: label → ident
    249  λl. an_identifier … (word_of_identifier … l).
     248definition ident_of_label: label → Identifier
     249 toASM_ident LabelTag.
    250250
    251251definition build_translated_statement ≝
     
    275275      [ nil ⇒ ⊥
    276276      | cons hd tl ⇒
    277         let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
     277        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
    278278          map ? ? (
    279279            λr.
    280280            match fst ? ? r with
    281             [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
     281            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
    282282            | None ⇒ 〈None ?, \snd r〉
    283283            ]) rest
     
    287287cases daemon (*CSC: XXX will be fixed by an invariant later *)
    288288qed.
    289    
     289
    290290definition translate_functs ≝
    291291  λglobals.
     
    312312
    313313(* dpm: plays the role of the string "_exit" in the O'caml source *)
    314 axiom identifier_prefix: Word.
     314axiom identifier_prefix: Identifier.
    315315(*CSC: XXXXXXX wrong anyway since labels from different functions can now
    316316  clash with each other and with names of functions *)
    317 axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
     317axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
    318318
    319319(* dpm: fresh prefix stuff needs unifying with brian *)
     
    323323  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    324324  let global_addr ≝ globals_addr (prog_vars … p) in
    325   let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
    326     〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
     325  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x,off〉) global_addr in
     326    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p)〉.
    327327 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
    328328 normalize in match prog_var_names normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.