Changeset 2443 for src/LIN


Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

Location:
src/LIN
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2286 r2443  
    2222    ]. @I qed.
    2323
    24 (* TODO:
    25   this should translate back end immediates (which rely on beval) to ASM
    26   byte immediates. How should it work? surely needs arguments for instantiation
    27   of blocks. If it's too much a fuss, we can go back to byte immediates in the
    28   back end. *)
    29 definition asm_byte_of_beval : beval → Byte ≝
    30   λb.match b with
    31     [ BVByte b ⇒ b
    32     | BVundef ⇒ (* any will do *) zero_byte
    33     | BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]]
    34     | BVnull _ ⇒ zero_byte (* is it correct? *)
    35     | BVptr b p o ⇒ ?
    36     ].
    37   cases daemon qed.
    38 
    39 definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝
    40   λa.match a with
    41   [ Reg r ⇒ register_address r
    42   | Imm bv ⇒ DATA (asm_byte_of_beval bv)
    43   ].
    44   cases a #x [2: normalize //] normalize nodelta
    45   elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
    46 qed.
    47 
    48 let rec association (i: ident) (l: list (ident × nat))
    49                     on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
    50   match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
    51   [ nil ⇒ λabsd. ?
     24let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
     25                    on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
     26  match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
     27  [ nil ⇒ Ⓧ
    5228  | cons hd tl ⇒
    53     λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
    54       (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
    55       [ true ⇒ λeq_prf. \snd hd
    56       | false ⇒ λeq_prf. association i tl ?
    57       ]) (refl ? (eq_identifier ? (\fst hd) i))
    58   ].
    59   [ cases absd
    60   | cases prf
    61     [ > eq_prf
    62       # H
    63       cases H
     29    λprf.
     30    If eq_A a (\fst hd) then \snd hd else with eq_prf do
     31      association … eq_A a tl ?
     32  ].
     33  elim (orb_Prop_true … prf)
     34    [ > eq_prf *
    6435    | # H
    6536      assumption
    6637    ]
     38qed.
     39
     40definition association_ident ≝ association ident nat (eq_identifier ?).
     41definition association_block ≝ association block Word eq_block.
     42
     43definition asm_cst_well_def :
     44  list (block × Word) → beval → bool ≝
     45λglobals,bv.match bv with
     46[ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals)
     47| _ ⇒ true
     48].
     49
     50definition vector_cast :
     51∀A,n,m.A → Vector A n → Vector A m ≝
     52λA,n,m,dflt,v.
     53If leb n m then with prf do
     54  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
     55else with prf do
     56  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
     57lapply prf @(leb_elim n)
     58[2,3: #_ * #abs elim (abs I) ]
     59#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
     60[ assumption ]
     61@(transitive_le … (not_le_to_lt … H)) %2 %1
     62qed.
     63
     64definition asm_byte_of_beval :
     65  ∀globals,bv.asm_cst_well_def globals bv → Byte ≝
     66  λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with
     67    [ BVByte b ⇒ λ_.b
     68    | BVundef ⇒ λ_.(* any will do *) zero_byte
     69    | BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]]
     70    | BVnull _ ⇒ λ_.zero_byte (* is it correct? *)
     71    | BVptr b p o ⇒ λprf.
     72      let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in
     73      let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in
     74      head' … inst
     75    ].
     76
     77definition asm_arg_well_def :
     78  list (block × Word) → hdw_argument → bool ≝
     79λglobals,a.match a with
     80[ Imm bv ⇒ asm_cst_well_def globals bv
     81| _ ⇒ true
     82].
     83
     84definition arg_address : ∀globals,arg.asm_arg_well_def globals arg →
     85  [[ acc_a ; direct ; registr ; data ]] ≝
     86  λglobals,a.
     87  match a
     88  return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]]
     89  with
     90  [ Reg r ⇒ λ_.register_address r
     91  | Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf)
     92  ].
     93  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
     94  | @I
    6795  ]
    6896qed.
    6997
    7098definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
     99
     100definition asm_stmt_well_def :
     101  list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝
     102  λblocks,old_globals,stmt.
     103  match stmt with
     104  [ sequential instr _ ⇒
     105    match instr with
     106    [ step_seq instr' ⇒
     107      match instr' with
     108      [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg
     109      | MOVE regs ⇒
     110        match regs with
     111        [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv
     112        | int_to_acc _ bv ⇒ asm_cst_well_def blocks bv
     113        | _ ⇒ true
     114        ]
     115      | _ ⇒ true
     116      ]
     117    | _ ⇒ true
     118    ]
     119  | _ ⇒ true
     120  ].
    71121 
    72122definition statement_labels ≝
     
    137187definition translate_statements ≝
    138188  λglobals: list (ident × nat).
     189  λblocks: list (block × Word).
    139190  λglobals_old: list ident.
    140   λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
     191  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    141192  λstatement: joint_statement LIN globals_old.
    142   match statement with
    143   [ final instr ⇒
     193  match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with
     194  [ final instr ⇒ λ_.
    144195    match instr with
    145196    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
     
    148199    ]
    149200  | sequential instr _ ⇒
    150       match instr with
     201      match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with
    151202      [ step_seq instr' ⇒
    152         match instr' with
    153         [ extension_seq ext ⇒
     203        match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with
     204        [ extension_seq ext ⇒ λ_.
    154205          match ext with
    155206          [ SAVE_CARRY ⇒
     
    158209            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
    159210          ]
    160         | COMMENT comment ⇒ Comment comment
    161         | COST_LABEL lbl ⇒ Cost lbl
    162         | POP _ ⇒ Instruction (POP ? accumulator_address)
    163         | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    164         | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    165         | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    166         | extension_call abs ⇒ match abs in void with [ ]
    167         | OPACCS accs _ _ _ _ ⇒
     211        | COMMENT comment ⇒ λ_.Comment comment
     212        | COST_LABEL lbl ⇒ λ_.Cost lbl
     213        | POP _ ⇒ λ_.Instruction (POP ? accumulator_address)
     214        | PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address)
     215        | CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY)
     216        | CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f)
     217        | extension_call abs ⇒ λ_.match abs in void with [ ]
     218        | OPACCS accs _ _ _ _ ⇒ λ_.
    168219          match accs with
    169220          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    170221          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    171222          ]
    172         | OP1 op1 _ _ ⇒
     223        | OP1 op1 _ _ ⇒ λ_.
    173224          match op1 with
    174225          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     
    176227          | Rl ⇒ Instruction (RL ? ACC_A)
    177228          ]
    178         | OP2 op2 _ _ reg ⇒
     229        | OP2 op2 _ _ reg ⇒ λprf'.?
     230          | _ ⇒ ?] | _ ⇒ ? ]].[12: whd in prf : (?%);
     231
    179232          match op2 with
    180233          [ Add ⇒
    181             let reg' ≝ arg_address reg in
     234            let reg' ≝ arg_address … prf' in
    182235            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    183236                                                           direct;
     
    195248            ] (subaddressing_modein … reg')
    196249          | Addc ⇒
    197             let reg' ≝ arg_address reg in
     250            let reg' ≝ arg_address … prf' in
    198251            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    199252                                                           direct;
     
    211264            ] (subaddressing_modein … reg')
    212265          | Sub ⇒
    213             let reg' ≝ arg_address reg in
     266            let reg' ≝ arg_address … prf' in
    214267            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    215268                                                           direct;
     
    227280            ] (subaddressing_modein … reg')
    228281          | And ⇒
    229             let reg' ≝ arg_address reg in
     282            let reg' ≝ arg_address … prf' in
    230283            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    231284                                                           direct;
     
    243296            ] (subaddressing_modein … reg')
    244297          | Or ⇒
    245             let reg' ≝ arg_address reg in
     298            let reg' ≝ arg_address … prf' in
    246299            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    247300                                                           direct;
     
    258311            ] (subaddressing_modein … reg')
    259312          | Xor ⇒
    260             let reg' ≝ arg_address reg in
     313            let reg' ≝ arg_address … prf' in
    261314            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    262315                                                           direct;
     
    273326            ] (subaddressing_modein … reg')
    274327          ]
    275         | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    276         | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    277         | ADDRESS addr proof _ _ ⇒
    278           let look ≝ association addr globals (prf ? proof) in
     328        | LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     329        | STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     330        | ADDRESS addr proof _ _ ⇒ λ_.
     331          let look ≝ association_ident addr globals (prf ? proof) in
    279332            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    280         | SET_CARRY ⇒
     333        | SET_CARRY ⇒ λ_.
    281334          Instruction (SETB ? CARRY)
    282335        | MOVE regs ⇒
    283           match regs with
    284           [ to_acc _ reg ⇒
     336          match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with
     337          [ to_acc _ reg ⇒ λ_.
    285338             let reg' ≝ register_address reg in
    286339               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    295348               | _ ⇒ λother: False. ⊥
    296349               ] (subaddressing_modein … reg')
    297           | from_acc reg _ ⇒
     350          | from_acc reg _ ⇒ λ_.
    298351             let reg' ≝ register_address reg in
    299352               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    308361               | _ ⇒ λother: False. ⊥
    309362               ] (subaddressing_modein … reg')
    310           | int_to_reg reg bv ⇒
    311             let b ≝ asm_byte_of_beval bv in
     363          | int_to_reg reg bv ⇒ λprf'.
     364            let b ≝ asm_byte_of_beval … prf' in
    312365            let reg' ≝ register_address reg in
    313366              match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    322375              | _ ⇒ λother: False. ⊥
    323376              ] (subaddressing_modein … reg')
    324           | int_to_acc _ bv ⇒
    325             let b ≝ asm_byte_of_beval bv in
     377          | int_to_acc _ bv ⇒ λprf'.
     378            let b ≝ asm_byte_of_beval … prf' in
    326379            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    327380          ]
    328381        ]
    329       | COND _ lbl ⇒
     382      | COND _ lbl ⇒ λ_.
    330383        (* dpm: this should be handled in translate_code! *)
    331384        Instruction (JNZ ? (toASM_ident ? lbl))
    332385      ]
    333386    ].
    334   try assumption
    335   try @ I
     387  try @I
     388  assumption
    336389qed.
    337390
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2286 r2443  
    2727 (* empty_framesT ≝ *) it
    2828 (* regsT ≝ *) hw_register_env
    29  (* empty_regsT ≝ *) init_hw_register_env.
     29 (* empty_regsT ≝ *) init_hw_register_env
     30 (* load_sp ≝ *) hwreg_retrieve_sp
     31 (* store_sp ≝ *) hwreg_store_sp.
    3032
    3133(*CSC: XXXX, for external functions only*)
     
    3739
    3840definition LTL_LIN_semantics ≝
    39   λF.mk_more_sem_unserialized_params LTL_LIN F
     41  λF.mk_sem_unserialized_params LTL_LIN F
    4042  (* st_pars            ≝ *) LTL_LIN_state
    4143  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
  • src/LIN/semantics.ma

    r2286 r2443  
    33
    44definition LIN_semantics : sem_params ≝
    5   make_sem_lin_params LIN (LTL_LIN_semantics ?).
     5  make_sem_lin_params LIN LTL_LIN_semantics.
Note: See TracChangeset for help on using the changeset viewer.