Changeset 1522


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

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1515 r1522  
    204204
    205205definition labelled_instruction ≝ option Identifier × pseudo_instruction.
    206 definition preamble ≝ list ((Identifier × nat) × (String × Word)).
     206definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
    207207definition assembly_program ≝ list instruction.
    208208definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
  • src/ASM/CostsProof.ma

    r1514 r1522  
    1 
    21include "ASM/ASMCosts.ma".
    32include "ASM/WellLabeled.ma".
     
    209208    cases(lt_to_not_zero … proof)
    210209  | #m' #proof
    211     normalize in ⊢ (???%)
     210    normalize in ⊢ (???%);
    212211    cases n
    213212    [ normalize //
     
    256255  ]
    257256qed.
     257
     258include alias "arithmetics/nat.ma".
    258259
    259260lemma plus_minus_rearrangement_1:
     
    277278              >(associative_plus (m' - n) 1 (o - m' - 1))
    278279              <commutative_plus in match (1 + (o - m' - 1));
    279               <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1)
     280              <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1);
    280281              [1: >ind_hyp
    281282                [1: %
     
    338339    clock … (write_at_stack_pointer … s sp) = clock … s.
    339340  #s #sp
    340   change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (
     341  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with (
    341342      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
    342343        ?);
  • src/ASM/Interpret.ma

    r1519 r1522  
    1 include "ASM/Status.ma". 
     1include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
    33
     
    4040   # H2
    4141   normalize
    42    change in H2: (??%?); with (orb ??)
     42   change with (orb ??) in H2: (??%?);
    4343   cases (inclusive_disjunction_true … H2)
    4444   [ # K
     
    8888     [ # K1
    8989       # _
    90        change in K1; with ((andb ? (subvector_with …)) = true)
     90       change with ((andb ? (subvector_with …)) = true) in K1;
    9191       cases (conjunction_true … K1)
    9292       # K3
     
    105105     | # K1
    106106       # K2
    107        (normalize in K2;)
     107       normalize in K2;
    108108       cases K2;
    109109     ]
     
    528528qed.
    529529
    530 definition execute_1_0: Status → instruction × Word × nat → Status ≝
     530include "ASM/JMCoercions.ma".
     531
     532definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
    531533  λs,instr_pc_ticks.
    532534    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
     
    541543        | _ ⇒ λabsd. ⊥
    542544        ] (subaddressing_modein … x)) instr s
     545      | _ ⇒ ?
     546      ] in s.
    543547      | ACALL addr ⇒
    544548          let s ≝ set_clock ? s (ticks + clock ? s) in
  • src/ASM/Status.ma

    r1521 r1522  
    11541154 #id #id' #i #prefix elim prefix
    11551155  [ whd in ⊢ (?% → ?);
    1156     change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?); with (eq_identifier ? id' id);
     1156    change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11571157    @eq_identifier_elim normalize nodelta; /2/
    11581158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11591159    cases he; normalize nodelta
    11601160     [ #H @ (IH H)
    1161      | #x whd in ⊢ (? → ?(??%)); change in match (instruction_matches_identifier ??); with (eq_identifier ? x id)
     1161     | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
    11621162       @eq_identifier_elim #E normalize nodelta
    11631163       [ destruct @eq_identifier_elim normalize nodelta;
     
    11721172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11731173 #id #id' #i #prefix elim prefix
    1174  [ whd in ⊢ (?% → ?); change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?); with (eq_identifier ???)
     1174 [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
    11751175   @eq_identifier_elim #E
    11761176  [ normalize //
     
    11851185       | #H >(does_not_occur_Some)
    11861186         [ #H2 whd in match (does_not_occur ??);
    1187            change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1187           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    11881188           >Heq >eq_identifier_refl normalize nodelta
    11891189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
    1190            change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1190           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    11911191           >eq_identifier_refl
    11921192           normalize nodelta @H2 
     
    11981198       #Hor @orb_elim
    11991199       [ <Heq2 in Hor; #Hor normalize in Hor;
    1200          whd in match (does_not_occur ??); change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1200         whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    12011201         >eq_identifier_false // normalize nodelta
    12021202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    12031203       | normalize nodelta whd in match (occurs_exactly_once ??);
    1204          change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1204         change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    12051205         >eq_identifier_false //
    12061206       ]
  • 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.