Changeset 722 for src/LIN/LINToASM.ma
 Timestamp:
 Mar 29, 2011, 6:32:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LINToASM.ma
r699 r722 29 29 λg: list Identifier. 30 30 λ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 37 46 ]. 38 47 39 48 definition function_labels_internal ≝ 40 49 λglobals: list Identifier. 41 λlabels: BitVectorTrieSet 8.50 λlabels: BitVectorTrieSet ?. 42 51 λstatement: LINStatement globals. 43 52 set_union ? labels (statement_labels globals statement). 44 53 45 54 (* dpm: A = Identifier *) 46 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8≝55 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝ 47 56 λA: Type[0]. 48 57 λglobals: list Identifier. 49 58 λf: A × (LINFunctionDefinition globals). 50 59 let 〈ignore, fun_def〉 ≝ f in 51 match fun_def return λ_. BitVectorTrieSet 8with60 match fun_def return λ_. BitVectorTrieSet ? with 52 61 [ LIN_Fu_Internal stmts ⇒ 53 foldl ? ? (function_labels_internal globals) (set_empty 8) stmts62 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts 54 63  LIN_Fu_External _ ⇒ set_empty ? 55 64 ]. 56 65 57 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8≝66 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝ 58 67 λA: Type[0]. 59 68 λglobals: list Identifier. 60 λlabels: BitVectorTrieSet 8.69 λlabels: BitVectorTrieSet ?. 61 70 λfunct: A × (LINFunctionDefinition globals). 62 71 set_union ? labels (function_labels ? globals funct). … … 65 74 λprogram. 66 75 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). 68 77 69 78 definition data_of_int ≝ λbv. DATA bv. … … 77 86 λglobals_old: list Identifier. 78 87 λ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) ] 95 239 ] 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 ]〉. 230 241 try assumption 231 242 try @ I
Note: See TracChangeset
for help on using the changeset viewer.