Changeset 722


Ignore:
Timestamp:
Mar 29, 2011, 6:32:47 PM (9 years ago)
Author:
mulligan
Message:

Committing changes from today. Several files do not typecheck.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r714 r722  
    185185definition instruction ≝ preinstruction [[relative]].
    186186
    187 inductive labelled_instruction: Type[0] ≝
    188   Instruction: instruction → labelled_instruction
    189 | Cost: Identifier → labelled_instruction
    190 | Jmp: Identifier → labelled_instruction
    191 | Call: Identifier → labelled_instruction
    192 | Mov: [[dptr]] → Identifier → labelled_instruction
    193 | Label: Identifier → labelled_instruction
    194 | WithLabel: jump Identifier → labelled_instruction.
     187inductive pseudo_instruction: Type[0] ≝
     188  Instruction: instruction → pseudo_instruction
     189| Comment: String → pseudo_instruction
     190| Cost: Identifier → pseudo_instruction
     191| Jmp: Identifier → pseudo_instruction
     192| Call: Identifier → pseudo_instruction
     193| Mov: [[dptr]] → Identifier → pseudo_instruction
     194| WithLabel: jump Identifier → pseudo_instruction.
     195
     196definition labelled_instruction ≝ option Identifier × pseudo_instruction.
    195197
    196198definition preamble ≝ list (Identifier × nat).
  • src/LIN/LIN.ma

    r714 r722  
    88alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    99
    10 inductive LINStatement (globals: list Identifier): Type[0] ≝
    11   | LIN_St_Goto: Identifier → LINStatement globals
    12   | LIN_St_Label: Identifier → LINStatement globals
    13   | LIN_St_Comment: String → LINStatement globals
    14   | LIN_St_CostLabel: Identifier → LINStatement globals
    15   | LIN_St_Int: Register → Byte → LINStatement globals
    16   | LIN_St_Pop: LINStatement globals
    17   | LIN_St_Push: LINStatement globals
    18   | LIN_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → LINStatement globals
    19   | LIN_St_FromAcc: Register → LINStatement globals
    20   | LIN_St_ToAcc: Register → LINStatement globals
    21   | LIN_St_OpAccs: OpAccs → LINStatement globals
    22   | LIN_St_Op1: ASMOp1 → LINStatement globals
    23   | LIN_St_Op2: ASMOp2 → Register → LINStatement globals
    24   | LIN_St_ClearCarry: LINStatement globals
    25   | LIN_St_Load: LINStatement globals
    26   | LIN_St_Store: LINStatement globals
    27   | LIN_St_CallId: Identifier → LINStatement globals
    28   | LIN_St_CondAcc: Identifier → LINStatement globals
    29   | LIN_St_Return: LINStatement globals.
     10inductive JointInstruction (globals: list Identifier): Type[0] ≝
     11  | Joint_Instr_Goto: Identifier → JointInstruction globals
     12  | Joint_Instr_Comment: String → JointInstruction globals
     13  | Joint_Instr_CostLabel: Identifier → JointInstruction globals
     14  | Joint_Instr_Int: Register → Byte → JointInstruction globals
     15  | Joint_Instr_Pop: JointInstruction globals
     16  | Joint_Instr_Push: JointInstruction globals
     17  | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
     18  | Joint_Instr_FromAcc: Register → JointInstruction globals
     19  | Joint_Instr_ToAcc: Register → JointInstruction globals
     20  | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
     21  | Joint_Instr_Op1: Op1 → JointInstruction globals
     22  | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
     23  | Joint_Instr_ClearCarry: JointInstruction globals
     24  | Joint_Instr_Load: JointInstruction globals
     25  | Joint_Instr_Store: JointInstruction globals
     26  | Joint_Instr_CallId: Identifier → JointInstruction globals
     27  | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
     28
     29inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
     30  | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals
     31  | LIN_St_Return: JointStatement A globals.
     32 
     33definition LINStatement ≝
     34  λglobals.
     35    option Identifier × (JointStatement unit globals).
    3036 
    3137definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
  • src/LIN/LINToASM.ma

    r699 r722  
    2929  λg: list Identifier.
    3030  λs: LINStatement g.
    31   match s with
    32   [ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
    33   | LIN_St_Label lbl ⇒ set_insert ? lbl (set_empty ?)
    34   | LIN_St_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
    35   | LIN_St_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
    36   | _ ⇒ set_empty ?
     31  let 〈label, instr〉 ≝ s in
     32  let generated ≝
     33    match instr with
     34    [ LIN_St_Sequential instr' _ ⇒
     35        match instr' with
     36        [ Joint_Instr_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
     37        | Joint_Instr_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
     38        | Joint_Instr_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
     39        | _ ⇒ set_empty ?
     40        ]
     41    | LIN_St_Return ⇒ set_empty ?
     42    ] in
     43  match label with
     44  [ None ⇒ generated
     45  | Some lbl ⇒ set_insert ? lbl generated
    3746  ].
    3847
    3948definition function_labels_internal ≝
    4049  λglobals: list Identifier.
    41   λlabels: BitVectorTrieSet 8.
     50  λlabels: BitVectorTrieSet ?.
    4251  λstatement: LINStatement globals.
    4352    set_union ? labels (statement_labels globals statement).
    4453
    4554(* dpm: A = Identifier *)
    46 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8
     55definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ?
    4756  λA: Type[0].
    4857  λglobals: list Identifier.
    4958  λf: A × (LINFunctionDefinition globals).
    5059  let 〈ignore, fun_def〉 ≝ f in
    51   match fun_def return λ_. BitVectorTrieSet 8 with
     60  match fun_def return λ_. BitVectorTrieSet ? with
    5261  [ LIN_Fu_Internal stmts ⇒
    53       foldl ? ? (function_labels_internal globals) (set_empty 8) stmts
     62      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    5463  | LIN_Fu_External _ ⇒ set_empty ?
    5564  ].
    5665 
    57 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8
     66definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ?
    5867  λA: Type[0].
    5968  λglobals: list Identifier.
    60   λlabels: BitVectorTrieSet 8.
     69  λlabels: BitVectorTrieSet ?.
    6170  λfunct: A × (LINFunctionDefinition globals).
    6271    set_union ? labels (function_labels ? globals funct).
     
    6574  λprogram.
    6675    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (LIN_Pr_vars program)))
    67               (set_empty 8) (LIN_Pr_funs program).
     76              (set_empty ?) (LIN_Pr_funs program).
    6877   
    6978definition data_of_int ≝ λbv. DATA bv.
     
    7786  λglobals_old: list Identifier.
    7887  λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
    79   λlin_statement: LINStatement globals_old.
    80   match lin_statement with
    81   [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
    82   | LIN_St_Label lbl ⇒ [ Label lbl ]
    83   | LIN_St_Comment _ ⇒ [ ]
    84   | LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
    85   | LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
    86   | LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
    87   | LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
    88   | LIN_St_Return ⇒ [ Instruction (RET ?) ]
    89   | LIN_St_CallId f ⇒ [ Call f ]
    90   | LIN_St_OpAccs accs ⇒
    91     match accs with
    92     [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
    93     | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
    94     | Modu ⇒ ?
     88  λstatement: LINStatement globals_old.
     89  〈\fst statement, match \snd statement with
     90  [ LIN_St_Return ⇒ [ Instruction (RET ?) ]
     91  | LIN_St_Sequential instr _⇒
     92    match instr with
     93    [ Joint_Instr_Goto lbl ⇒ [ Jmp lbl ]
     94    | Joint_Instr_Comment _ ⇒ [ ]
     95    | Joint_Instr_CostLabel lbl ⇒ [ Cost lbl ]
     96    | Joint_Instr_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
     97    | Joint_Instr_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
     98    | Joint_Instr_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
     99    | Joint_Instr_CallId f ⇒ [ Call f ]
     100    | Joint_Instr_OpAccs accs ⇒
     101      match accs with
     102      [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
     103      | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
     104      | Modu ⇒ ?
     105      ]
     106    | Joint_Instr_Op1 op1 ⇒
     107      match op1 with
     108      [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
     109      | Inc ⇒ [ Instruction (INC ? ACC_A) ]
     110      ]
     111    | Joint_Instr_Op2 op2 reg ⇒
     112      match op2 with
     113      [ Add ⇒
     114        let reg' ≝ register_address reg in
     115        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     116                                                       direct;
     117                                                       register ]] x) → ? with
     118        [ ACC_A ⇒ λacc_a: True.
     119          [ Instruction (ADD ? ACC_A accumulator_address) ]
     120        | DIRECT d ⇒ λdirect1: True.
     121          [ Instruction (ADD ? ACC_A (DIRECT d)) ]
     122        | REGISTER r ⇒ λregister1: True.
     123          [ Instruction (ADD ? ACC_A (REGISTER r)) ]
     124        | _ ⇒ λother: False. ⊥
     125        ] (subaddressing_modein … reg')
     126      | Addc ⇒
     127        let reg' ≝ register_address reg in
     128        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     129                                                       direct;
     130                                                       register ]] x) → ? with
     131        [ ACC_A ⇒ λacc_a: True.
     132          [ Instruction (ADDC ? ACC_A accumulator_address) ]
     133        | DIRECT d ⇒ λdirect2: True.
     134          [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
     135        | REGISTER r ⇒ λregister2: True.
     136          [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
     137        | _ ⇒ λother: False. ⊥
     138        ] (subaddressing_modein … reg')
     139      | Sub ⇒
     140        let reg' ≝ register_address reg in
     141        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     142                                                       direct;
     143                                                       register ]] x) → ? with
     144        [ ACC_A ⇒ λacc_a: True.
     145          [ Instruction (SUBB ? ACC_A accumulator_address) ]
     146        | DIRECT d ⇒ λdirect3: True.
     147          [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
     148        | REGISTER r ⇒ λregister3: True.
     149          [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
     150        | _ ⇒ λother: False. ⊥
     151        ] (subaddressing_modein … reg')
     152      | And ⇒
     153        let reg' ≝ register_address reg in
     154        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     155                                                       direct;
     156                                                       register ]] x) → ? with
     157        [ ACC_A ⇒ λacc_a: True.
     158          [ Instruction (NOP ?) ]
     159        | DIRECT d ⇒ λdirect4: True.
     160          [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     161        | REGISTER r ⇒ λregister4: True.
     162          [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     163        | _ ⇒ λother: False. ⊥
     164        ] (subaddressing_modein … reg')
     165      | Or ⇒
     166        let reg' ≝ register_address reg in
     167        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     168                                                       direct;
     169                                                       register ]] x) → ? with
     170        [ ACC_A ⇒ λacc_a: True.
     171          [ Instruction (NOP ?) ]
     172        | DIRECT d ⇒ λdirect5: True.
     173          [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     174        | REGISTER r ⇒ λregister5: True.
     175          [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     176        | _ ⇒ λother: False. ⊥
     177        ] (subaddressing_modein … reg')
     178      | Xor ⇒
     179        let reg' ≝ register_address reg in
     180        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     181                                                       direct;
     182                                                       register ]] x) → ? with
     183        [ ACC_A ⇒ λacc_a: True.
     184          [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
     185        | DIRECT d ⇒ λdirect6: True.
     186          [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
     187        | REGISTER r ⇒ λregister6: True.
     188          [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
     189        | _ ⇒ λother: False. ⊥
     190        ] (subaddressing_modein … reg')
     191      ]
     192    | Joint_Instr_Int reg byte ⇒
     193      let reg' ≝ register_address reg in
     194        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     195                                                       direct;
     196                                                       register ]] x) → ? with
     197        [ REGISTER r ⇒ λregister7: True.
     198          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
     199        | ACC_A ⇒ λacc: True.
     200          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
     201        | DIRECT d ⇒ λdirect7: True.
     202          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
     203        | _ ⇒ λother: False. ⊥
     204        ] (subaddressing_modein … reg')
     205    | Joint_Instr_FromAcc reg ⇒
     206      let reg' ≝ register_address reg in
     207        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     208                                                       direct;
     209                                                       register ]] x) → ? with
     210        [ REGISTER r ⇒ λregister8: True.
     211          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
     212        | ACC_A ⇒ λacc: True.
     213          [ Instruction (NOP ?) ]
     214        | DIRECT d ⇒ λdirect8: True.
     215          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
     216        | _ ⇒ λother: False. ⊥
     217        ] (subaddressing_modein … reg')
     218    | Joint_Instr_ToAcc reg ⇒
     219      let reg' ≝ register_address reg in
     220        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     221                                                       direct;
     222                                                       register ]] x) → ? with
     223        [ REGISTER r ⇒ λregister9: True.
     224          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
     225        | DIRECT d ⇒ λdirect9: True.
     226          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
     227        | ACC_A ⇒ λacc_a: True.
     228          [ Instruction (NOP ?) ]
     229        | _ ⇒ λother: False. ⊥
     230        ] (subaddressing_modein … reg')
     231    | Joint_Instr_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
     232    | Joint_Instr_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
     233    | Joint_Instr_Address addr proof ⇒
     234      let look ≝ association addr globals (prf ? proof) in
     235        [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
     236    | Joint_Instr_CondAcc lbl ⇒
     237      (* dpm: this should be handled in translate_code! *)
     238      [ WithLabel (JNZ ? lbl) ]
    95239    ]
    96   | LIN_St_Op1 op1 ⇒
    97     match op1 with
    98     [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
    99     | Inc ⇒ [ Instruction (INC ? ACC_A) ]
    100     ]
    101   | LIN_St_Op2 op2 reg ⇒
    102     match op2 with
    103     [ Add ⇒
    104       let reg' ≝ register_address reg in
    105       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    106                                                      direct;
    107                                                      register ]] x) → ? with
    108       [ ACC_A ⇒ λacc_a: True.
    109         [ Instruction (ADD ? ACC_A accumulator_address) ]
    110       | DIRECT d ⇒ λdirect1: True.
    111         [ Instruction (ADD ? ACC_A (DIRECT d)) ]
    112       | REGISTER r ⇒ λregister1: True.
    113         [ Instruction (ADD ? ACC_A (REGISTER r)) ]
    114       | _ ⇒ λother: False. ⊥
    115       ] (subaddressing_modein … reg')
    116     | Addc ⇒
    117       let reg' ≝ register_address reg in
    118       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    119                                                      direct;
    120                                                      register ]] x) → ? with
    121       [ ACC_A ⇒ λacc_a: True.
    122         [ Instruction (ADDC ? ACC_A accumulator_address) ]
    123       | DIRECT d ⇒ λdirect2: True.
    124         [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
    125       | REGISTER r ⇒ λregister2: True.
    126         [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
    127       | _ ⇒ λother: False. ⊥
    128       ] (subaddressing_modein … reg')
    129     | Sub ⇒
    130       let reg' ≝ register_address reg in
    131       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    132                                                      direct;
    133                                                      register ]] x) → ? with
    134       [ ACC_A ⇒ λacc_a: True.
    135         [ Instruction (SUBB ? ACC_A accumulator_address) ]
    136       | DIRECT d ⇒ λdirect3: True.
    137         [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
    138       | REGISTER r ⇒ λregister3: True.
    139         [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
    140       | _ ⇒ λother: False. ⊥
    141       ] (subaddressing_modein … reg')
    142     | And ⇒
    143       let reg' ≝ register_address reg in
    144       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    145                                                      direct;
    146                                                      register ]] x) → ? with
    147       [ ACC_A ⇒ λacc_a: True.
    148         [ Instruction (NOP ?) ]
    149       | DIRECT d ⇒ λdirect4: True.
    150         [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
    151       | REGISTER r ⇒ λregister4: True.
    152         [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
    153       | _ ⇒ λother: False. ⊥
    154       ] (subaddressing_modein … reg')
    155     | Or ⇒
    156       let reg' ≝ register_address reg in
    157       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    158                                                      direct;
    159                                                      register ]] x) → ? with
    160       [ ACC_A ⇒ λacc_a: True.
    161         [ Instruction (NOP ?) ]
    162       | DIRECT d ⇒ λdirect5: True.
    163         [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
    164       | REGISTER r ⇒ λregister5: True.
    165         [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
    166       | _ ⇒ λother: False. ⊥
    167       ] (subaddressing_modein … reg')
    168     | Xor ⇒
    169       let reg' ≝ register_address reg in
    170       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    171                                                      direct;
    172                                                      register ]] x) → ? with
    173       [ ACC_A ⇒ λacc_a: True.
    174         [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
    175       | DIRECT d ⇒ λdirect6: True.
    176         [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
    177       | REGISTER r ⇒ λregister6: True.
    178         [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
    179       | _ ⇒ λother: False. ⊥
    180       ] (subaddressing_modein … reg')
    181     ]
    182   | LIN_St_Int reg byte ⇒
    183     let reg' ≝ register_address reg in
    184       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    185                                                      direct;
    186                                                      register ]] x) → ? with
    187       [ REGISTER r ⇒ λregister7: True.
    188         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
    189       | ACC_A ⇒ λacc: True.
    190         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
    191       | DIRECT d ⇒ λdirect7: True.
    192         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
    193       | _ ⇒ λother: False. ⊥
    194       ] (subaddressing_modein … reg')
    195   | LIN_St_FromAcc reg ⇒
    196     let reg' ≝ register_address reg in
    197       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    198                                                      direct;
    199                                                      register ]] x) → ? with
    200       [ REGISTER r ⇒ λregister8: True.
    201         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
    202       | ACC_A ⇒ λacc: True.
    203         [ Instruction (NOP ?) ]
    204       | DIRECT d ⇒ λdirect8: True.
    205         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
    206       | _ ⇒ λother: False. ⊥
    207       ] (subaddressing_modein … reg')
    208   | LIN_St_ToAcc reg ⇒
    209     let reg' ≝ register_address reg in
    210       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    211                                                      direct;
    212                                                      register ]] x) → ? with
    213       [ REGISTER r ⇒ λregister9: True.
    214         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
    215       | DIRECT d ⇒ λdirect9: True.
    216         [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
    217       | ACC_A ⇒ λacc_a: True.
    218         [ Instruction (NOP ?) ]
    219       | _ ⇒ λother: False. ⊥
    220       ] (subaddressing_modein … reg')
    221   | LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
    222   | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
    223   | LIN_St_Address addr proof ⇒
    224     let look ≝ association addr globals (prf ? proof) in
    225       [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
    226   | LIN_St_CondAcc lbl ⇒
    227     (* dpm: this should be handled in translate_code! *)
    228     [ WithLabel (JNZ ? lbl) ]
    229   ].
     240  ]〉.
    230241  try assumption
    231242  try @ I
  • src/LTL/LTL.ma

    r716 r722  
    77include "ASM/String.ma".
    88
    9 inductive LTLStatement (globals: list Identifier): Type[0] ≝
    10   | LTL_St_Skip: label → LTLStatement globals
    11   | LTL_St_Comment: String → label → LTLStatement globals
    12   | LTL_St_CostLabel: Identifier → label → LTLStatement globals
    13   | LTL_St_Int: Register → Byte → label → LTLStatement globals
    14   | LTL_St_Pop: label → LTLStatement globals
    15   | LTL_St_Push: label → LTLStatement globals
    16   | LTL_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → Identifier → label → LTLStatement globals
    17   | LTL_St_FromAcc: Register → label → LTLStatement globals
    18   | LTL_St_ToAcc: Register → label → LTLStatement globals
    19   | LTL_St_OpAccs: OpAccs → label → LTLStatement globals
    20   | LTL_St_Op1: Op1 → label → LTLStatement globals
    21   | LTL_St_Op2: Op2 → Register → label → LTLStatement globals
    22   | LTL_St_ClearCarry: label → LTLStatement globals
    23   | LTL_St_Load: label → LTLStatement globals
    24   | LTL_St_Store: label → LTLStatement globals
    25   | LTL_St_CallId: Identifier → label → LTLStatement globals
    26   | LTL_St_CondAcc: label → label → LTLStatement globals
    27   | LTL_St_Return: LTLStatement globals.
     9include "LIN/LIN.ma".
     10
     11definition LTLStatement ≝ JointStatement Identifier.
    2812 
    29 definition LTLFunctionGraph ≝ λglobals. graph (LTLStatement globals).
     13definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
    3014 
    3115record LTLInternalFunction (globals: list Identifier): Type[0] ≝
     
    3317  LTL_IF_LUniverse: Universe;
    3418  LTL_IF_StackSize: nat;
    35   LTL_IF_Graph: LTLFunctionGraph globals;
     19  LTL_IF_Graph: LTLStatementGraph globals;
    3620  LTL_IF_Entry: label;
    3721  LTL_IF_Exit: label
  • src/LTL/LTLToLIN.ma

    r716 r722  
    22include "LIN/LIN.ma".
    33
    4 definition label_to_Identifier ≝
    5   λl: label.
    6   let n ≝ nat_of_pos l in
    7     bitvector_of_nat 8 n.
    8 
    9 definition translate_statement ≝
     4definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝
    105  λglobals: list Identifier.
    116  λs: LTLStatement globals.
    127    match s with
    13     [ LTL_St_Skip lbl ⇒ LIN_St_Goto globals (label_to_Identifier lbl)
    14     | LTL_St_Comment comment lbl ⇒ LIN_St_Comment globals comment
    15     | LTL_St_CostLabel cost lbl ⇒ LIN_St_CostLabel globals cost
    16     | LTL_St_Int register val lbl ⇒ LIN_St_Int globals register val
    17     | LTL_St_Pop lbl ⇒ LIN_St_Pop globals
    18     | LTL_St_Push lbl ⇒ LIN_St_Push globals
    19     | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof
    20     | LTL_St_FromAcc register lbl ⇒ LIN_St_FromAcc globals register
    21     | LTL_St_ToAcc register lbl ⇒ LIN_St_ToAcc globals register
    22     | LTL_St_OpAccs opaccs lbl ⇒ LIN_St_OpAccs globals opaccs
    23     | LTL_St_Op1 op1 lbl ⇒ LIN_St_Op1 globals op1
    24     | LTL_St_Op2 op2 register lbl ⇒ LIN_St_Op2 globals op2 register
    25     | LTL_St_ClearCarry lbl ⇒ LIN_St_ClearCarry globals
    26     | LTL_St_Load lbl ⇒ LIN_St_Load globals
    27     | LTL_St_Store lbl ⇒ LIN_St_Store globals
    28     | LTL_St_CallId identifier lbl ⇒ LIN_St_CallId globals identifier
    29     | LTL_St_CondAcc tgt lbl ⇒ LIN_St_CondAcc globals (label_to_Identifier tgt)
    30     | LTL_St_Return ⇒ LIN_St_Return globals
     8    [ LIN_St_Return ⇒ LIN_St_Return ? globals
     9    | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it
    3110    ].
  • src/LTL/LTLToLINI.ma

    r716 r722  
     1include "common/Graphs.ma".
     2include "LTL/LTL.ma".
     3
     4definition fetch: ∀globals. LTLStatementGraph globals → label → option (LTLStatement globals) ≝
     5  λglobals: list Identifier.
     6  λgraph: LTLStatementGraph globals.
     7  λl: label.
     8    graph_lookup ? graph l.
     9   
     10definition generate: ∀globals. LTLStatement globals → list (LTLStatement globals) → list (LTLStatement globals) ≝
     11  λglobals.
     12  λstatement.
     13  λstatements.
     14    statement :: statements.
  • src/common/AST.ma

    r714 r722  
    55include "utilities/Compare.ma".
    66
    7 definition Identifier ≝ Byte.
     7definition Identifier ≝ Word.
    88definition Immediate ≝ nat.
    99
     
    3232| Cast_StackOffset: Immediate → Cast.
    3333
     34(*
    3435inductive Op1: Type[0] ≝
    3536  Op1_Cast8U: Op1
     
    6768| Op2_ShR: Op2
    6869| Op2_ShRU: Op2
    69 (*
    7070| Op2_AddF: Op2
    7171| Op2_SubF: Op2
    7272| Op2_MulF: Op2
    7373| Op2_DivF: Op2
    74 *)
    7574| Op2_Cmp: Compare → Op2
    7675| Op2_CmpU: Compare → Op2
     
    8180| Op2_SubP: Op2
    8281| Op2_CmpP: Compare → Op2.
     82*)
    8383
    8484inductive Data: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.