Changeset 1522 for src/LIN


Ignore:
Timestamp:
Nov 21, 2011, 3:49:04 PM (8 years ago)
Author:
mulligan
Message:

changes to preamble and lin to asm pass, resolved conflict in interpret

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1520 r1522  
    288288qed.
    289289
     290include "common/Identifiers.ma".
     291
     292let rec flatten_fun_defs
     293  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
     294    (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function globals_old (lin_params globals_old)))))
     295      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
     296  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
     297  [ cons hd tl ⇒
     298    let fun_def ≝ \snd hd in
     299    let fun_id ≝ \fst hd in
     300    let translated ≝ translate_fun_def globals globals_old prf hd in
     301    let size_translated ≝ | translated | in
     302    let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
     303    let new_hd ≝ translated @ tail_trans in
     304    let new_map ≝ add ? ? tail_map fun_id initial_pc in
     305      〈new_hd, new_map〉
     306  | nil ⇒ 〈[ ], empty_map …〉
     307  ].
     308
    290309definition translate_functs ≝
    291310  λglobals.
     
    296315  λfuncts.
    297316  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    298    preamble @
    299     (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     317  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
     318   〈preamble @ flattened, map〉.
    300319
    301320(*CSC: region silently thrown away here *)
     
    323342  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    324343  let global_addr ≝ globals_addr (prog_vars … p) in
    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)〉.
    327  #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
    328  normalize in match prog_var_names normalize nodelta
     344  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
     345  let 〈translated, funct_map〉 ≝ translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p) in
     346    〈〈funct_map, global_addr'〉, translated〉.
     347 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
     348 normalize in match prog_var_names; normalize nodelta
    329349 elim (prog_vars … p) //
    330  #hd #tl #IH whd in ⊢ (% → %)
    331  whd in match globals_addr normalize nodelta
    332  whd in match (foldl ???? (hd::tl)) normalize nodelta
     350 #hd #tl #IH whd in ⊢ (% → %);
     351 whd in match globals_addr; normalize nodelta
     352 whd in match (foldl ???? (hd::tl)); normalize nodelta
    333353 cases hd * #id #reg #size normalize nodelta
    334354 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
Note: See TracChangeset for help on using the changeset viewer.