Changeset 2705


Ignore:
Timestamp:
Feb 22, 2013, 5:56:31 PM (6 years ago)
Author:
sacerdot
Message:

More progress in ASM towards implementing the new pseudoinstructions.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2704 r2705  
    518518| JZ: A → preinstruction A
    519519| JNZ: A → preinstruction A
    520 | JMP: [[indirect_dptr]] → preinstruction A
    521520| CJNE:
    522521   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
     
    562561| RET: preinstruction A
    563562| RETI: preinstruction A
    564 | NOP: preinstruction A.
     563| NOP: preinstruction A
     564| JMP: [[indirect_dptr]] → preinstruction A.
    565565
    566566definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
     
    978978  | Cost: costlabel → pseudo_instruction
    979979  | Jmp: Identifier → pseudo_instruction
    980   | CondJmp : [[acc_a]] → Identifier → Identifier → pseudo_instruction
    981   | MovSuccessor : [[ registr ; indirect ]] → word_side → Identifier → pseudo_instruction
     980  | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction
     981  | MovSuccessor : [[ acc_a ; direct ; registr ]] → word_side → Identifier → pseudo_instruction
    982982  | Call: Identifier → pseudo_instruction
    983983  | Mov: [[dptr]] → Identifier → pseudo_instruction.
  • src/ASM/AbstractStatus.ma

    r2516 r2705  
    2020  | CJNE _ _ ⇒ cl_jump
    2121  | DJNZ _ _ ⇒ cl_jump
     22  | JMP _ ⇒ cl_call
    2223  | _ ⇒ cl_other
    2324  ].
     
    2930   | ACALL _ ⇒ cl_call
    3031   | LCALL _ ⇒ cl_call
    31    | JMP _ ⇒ cl_call
    3232   | AJMP _ ⇒ cl_other
    3333   | LJMP _ ⇒ cl_other
  • src/ASM/Assembly.ma

    r2651 r2705  
    183183        [ ([[true;false;true;false;false;false;true;true]]) ]
    184184      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     185  | JMP adptr ⇒
     186     [ ([[false;true;true;true;false;false;true;true]]) ]
    185187  | MOV addrs ⇒
    186188     match addrs with
     
    395397          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    396398      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    397   | JMP adptr ⇒
    398      [ ([[false;true;true;true;false;false;true;true]]) ]
    399399  | LCALL addr ⇒
    400400     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     
    509509  | RET ⇒ [ RET ? ]
    510510  | RETI ⇒ [ RETI ? ]
    511   | NOP ⇒ [ RealInstruction (NOP ?) ]
     511  | NOP ⇒ [ NOP ? ]
     512  | JMP arg ⇒ [ RealInstruction (JMP ? arg) ]
    512513  ].
    513514
     
    557558        let address ≝ ADDR16 lookup_address in
    558559        [ LJMP address ]
     560  | Jnz acc tgt1 tgt2 ⇒
     561     
    559562  ].
    560563  %
  • src/ASM/Interpret.ma

    r2504 r2705  
    184184              | _ ⇒ λother: False. ⊥
    185185              ] (subaddressing_modein … addr)
     186        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     187          let s ≝ add_ticks1 s in
     188          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     189          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     190          let jmp_addr ≝ add … big_acc dptr in
     191          let new_pc ≝ add … (program_counter … s) jmp_addr in
     192            set_program_counter … s new_pc
    186193        | NOP ⇒ λinstr_refl.
    187            let s ≝ add_ticks2 s in
     194           let s ≝ add_ticks1 s in
    188195            s
    189196        | DEC addr ⇒ λinstr_refl.
     
    604611              | _ ⇒ λother: False. ⊥
    605612              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
     613        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     614          let s ≝ add_ticks1 s in
     615          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     616          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     617          let jmp_addr ≝ add … big_acc dptr in
     618          let new_pc ≝ add … (program_counter … s) jmp_addr in
     619            set_program_counter … s new_pc
    606620        | NOP ⇒ λinstr_refl.
    607621           let s ≝ add_ticks2 s in
     
    938952    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
    939953    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     954    try (change with (cl_call = cl_other → ?) #absurd destruct(absurd))
    940955    try (@or_introl //)
    941956    try (@or_intror //)
     
    10451060            | _ ⇒ λother: False. ⊥
    10461061            ] (subaddressing_modein … addr2)
    1047       | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
    1048           let s ≝ set_clock ?? s (ticks + clock … s) in
    1049           let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    1050           let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    1051           let jmp_addr ≝ add … big_acc dptr in
    1052           let new_pc ≝ add … (program_counter … s) jmp_addr in
    1053             set_program_counter … s new_pc
    10541062      | LJMP addr ⇒ λinstr_refl.
    10551063          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
     
    10981106        ] (refl … instr). (*10s*)
    10991107  try assumption
    1100   [1,2,3,4,5,6,7,8:
     1108  [1,2,3,4,5,6,7:
    11011109    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    11021110    try //
     
    11101118      /demod by clock_set_program_counter/ /demod nohyps/ %
    11111119    ]
    1112   |9:
     1120  |8:
    11131121    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
    11141122        (λx. λs.
     
    11901198       let s ≝ set_clock … s (\fst ticks + clock … s) in
    11911199        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
     1200    | Jnz acc dst1 dst2 ⇒
     1201       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
     1202        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     1203         set_program_counter … s (address_of_word_labels (\snd cm) dst1)
     1204       else
     1205        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
     1206         set_program_counter … s (address_of_word_labels (\snd cm) dst2)
     1207    | MovSuccessor dst ws lbl ⇒
     1208      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     1209      let addr ≝ address_of_word_labels (\snd cm) lbl in
     1210      let 〈high, low〉 ≝ vsplit ? 8 8 addr in
     1211      let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
     1212       set_arg_8 … s dst v     
    11921213    | Call call ⇒
    11931214      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     
    12091230  in
    12101231    s.
    1211   normalize
    1212   @I
     1232  [2: % | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    12131233qed.
    12141234
  • src/BACKEND_BROKEN_FILES

    r2693 r2705  
    11Directory esaminate: joint, RTLabs, RTL, ERTLptr, LTL, LIN, ASM
    22
    3 joint/linearise.ma:               prova rotta
     3joint/linearise.ma:               prova rotta ci sta lavorando Paolo
    44  joint/lineariseProof.ma
    5   LTL/LTLToLIN.ma
     5  LTL/LTLToLIN.ma                 ma funziona una volta riparato linearise.ma
    66
    77LIN/joint_LTL_LIN_semantics.ma:   parametri
    88  LIN/LIN_semantics.ma
    99  LTL/LTL_semantics.ma
     10
    1011LIN/LINToASM.ma:                  FCOND rotto, deve fare cose diverse ora?
    1112
    1213RTL/RTL_semantics.ma:             parametri
     14
     15ASM/*                             rotto, nuove istruzioni
    1316
    1417ASM/AssemblyProofSplit.ma         working, just veeery slow
  • src/compiler.ma

    r2702 r2705  
    1919include "ERTL/ERTLToERTLptr.ma".
    2020include "ERTLptr/ERTLptrToLTL.ma".
     21include "LTL/LTLToLIN.ma".
    2122(*
    22 include "LTL/LTLToLIN.ma".
    2323include "LIN/LINToASM.ma".
    24 *) include "ASM/ASM.ma". include "LIN/LIN.ma".
    25    axiom ltl_to_lin: ltl_program → lin_program.
     24*) include "ASM/ASM.ma".
    2625   axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2726
Note: See TracChangeset for help on using the changeset viewer.