 Timestamp:
 Aug 2, 2012, 3:18:11 PM (7 years ago)
 Location:
 src/LIN
 Files:

 4 deleted
 5 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LIN.ma
r1601 r2286 1 1 include "LIN/joint_LTL_LIN.ma". 2 include "basics/lists/list.ma".3 2 4 definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.3 definition LIN ≝ mk_lin_params LTL_LIN. 5 4 6 definition pre_lin_statement ≝ joint_statement lin_params_. 7 definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals). 5 (* aid unification *) 6 unification hint 0 ≔ 7 (**) ⊢ 8 acc_a_reg LIN ≡ unit. 9 unification hint 0 ≔ 10 (**) ⊢ 11 acc_a_arg LIN ≡ unit. 12 unification hint 0 ≔ 13 (**) ⊢ 14 acc_b_reg LIN ≡ unit. 15 unification hint 0 ≔ 16 (**) ⊢ 17 acc_a_arg LIN ≡ unit. 18 unification hint 0 ≔ 19 (**) ⊢ 20 snd_arg LIN ≡ hdw_argument. 21 unification hint 0 ≔ 22 (**) ⊢ 23 ext_seq LIN ≡ ltl_lin_seq. 24 unification hint 0 ≔ 25 (**) ⊢ 26 pair_move LIN ≡ registers_move. 8 27 9 definition lin_params: ∀globals. params globals ≝ 10 λglobals. 11 mk_params globals unit ltl_lin_params1 (list (lin_statement globals)) 12 (λcode. λl. 13 find ?? (λs. let 〈l',x〉 ≝ s in 14 match l' with [ None ⇒ None …  Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code). 15 16 definition lin_function ≝ λglobals. joint_function … (lin_params globals). 17 definition lin_program ≝ joint_program lin_params. 28 definition lin_program ≝ joint_program LIN. 
src/LIN/LINToASM.ma
r1995 r2286 2 2 include "utilities/BitVectorTrieSet.ma". 3 3 include "LIN/LIN.ma". 4 include "ASM/ASM.ma". 5 6 definition register_address: Register → [[ acc_a; direct; registr ]] ≝ 7 λr: Register. 8 match r with 9 [ Register00 ⇒ REGISTER [[ false; false; false ]] 10  Register01 ⇒ REGISTER [[ false; false; true ]] 11  Register02 ⇒ REGISTER [[ false; true; false ]] 12  Register03 ⇒ REGISTER [[ false; true; true ]] 13  Register04 ⇒ REGISTER [[ true; false; false ]] 14  Register05 ⇒ REGISTER [[ true; false; true ]] 15  Register06 ⇒ REGISTER [[ true; true; false ]] 16  Register07 ⇒ REGISTER [[ true; true; true ]] 17  RegisterA ⇒ ACC_A 18  RegisterB ⇒ DIRECT (bitvector_of_nat 8 240) 19  RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82) 20  RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83) 21  _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 22 ]. @I qed. 23 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. 4 47 5 48 let rec association (i: ident) (l: list (ident × nat)) … … 25 68 qed. 26 69 70 definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). 71 27 72 definition statement_labels ≝ 28 73 λg: list ident. … … 33 78 [ sequential instr' _ ⇒ 34 79 match instr' with 35 [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) } 80 [ step_seq instr'' ⇒ 81 match instr'' with 82 [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) } 83  _ ⇒ ∅ 84 ] 36 85  COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) } 86 ] 87  final instr' ⇒ 88 match instr' with 89 [ GOTO lbl ⇒ {(toASM_ident ? lbl)} 37 90  _ ⇒ ∅ 38 91 ] 39  RETURN ⇒ ∅ 40  GOTO lbl ⇒ {(toASM_ident ? lbl)} ] 92 ] 41 93 in 42 94 match label with … … 55 107 λA: Type[0]. 56 108 λglobals: list ident. 57 λf: A × ( lin_functionglobals).109 λf: A × (joint_function LIN globals). 58 110 let 〈ignore, fun_def〉 ≝ f in 59 111 match fun_def return λ_. identifier_set ? with … … 67 119 λglobals: list ident. 68 120 λlabels: identifier_set ?. 69 λfunct: A × ( lin_functionglobals).121 λfunct: A × (joint_function LIN globals). 70 122 labels ∪ (function_labels ? globals funct). 71 123 … … 80 132 definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224). 81 133 134 (* TODO: check and change to free bit *) 135 definition asm_other_bit ≝ BIT_ADDR (zero_byte). 136 82 137 definition translate_statements ≝ 83 138 λglobals: list (ident × nat). 84 139 λglobals_old: list ident. 85 140 λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals). 86 λstatement: pre_lin_statementglobals_old.141 λstatement: joint_statement LIN globals_old. 87 142 match statement with 88 [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) 89  RETURN ⇒ Instruction (RET ?) 143 [ final instr ⇒ 144 match instr with 145 [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) 146  RETURN ⇒ Instruction (RET ?) 147  tailcall abs ⇒ match abs in void with [ ] 148 ] 90 149  sequential instr _ ⇒ 91 150 match instr with 92 [ extension ext ⇒ ⊥ 93  COMMENT comment ⇒ Comment comment 94  COST_LABEL lbl ⇒ Cost lbl 95  POP _ ⇒ Instruction (POP ? accumulator_address) 96  PUSH _ ⇒ Instruction (PUSH ? accumulator_address) 97  CLEAR_CARRY ⇒ Instruction (CLR ? CARRY) 98  CALL_ID f _ _ ⇒ Call (toASM_ident ? f) 99  OPACCS accs _ _ _ _ ⇒ 100 match accs with 101 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 102  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 103 ] 104  OP1 op1 _ _ ⇒ 105 match op1 with 106 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 107  Inc ⇒ Instruction (INC ? ACC_A) 108  Rl ⇒ Instruction (RL ? ACC_A) 109 ] 110  OP2 op2 _ _ reg ⇒ 111 match op2 with 112 [ Add ⇒ 113 let reg' ≝ register_address reg in 114 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 115 direct; 116 registr ]] x) → ? with 117 [ ACC_A ⇒ λacc_a: True. 118 Instruction (ADD ? ACC_A accumulator_address) 119  DIRECT d ⇒ λdirect1: True. 120 Instruction (ADD ? ACC_A (DIRECT d)) 121  REGISTER r ⇒ λregister1: True. 122 Instruction (ADD ? ACC_A (REGISTER r)) 123  _ ⇒ λother: False. ⊥ 124 ] (subaddressing_modein … reg') 125  Addc ⇒ 126 let reg' ≝ register_address reg in 127 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 128 direct; 129 registr ]] x) → ? with 130 [ ACC_A ⇒ λacc_a: True. 131 Instruction (ADDC ? ACC_A accumulator_address) 132  DIRECT d ⇒ λdirect2: True. 133 Instruction (ADDC ? ACC_A (DIRECT d)) 134  REGISTER r ⇒ λregister2: True. 135 Instruction (ADDC ? ACC_A (REGISTER r)) 136  _ ⇒ λother: False. ⊥ 137 ] (subaddressing_modein … reg') 138  Sub ⇒ 139 let reg' ≝ register_address reg in 140 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 141 direct; 142 registr ]] x) → ? with 143 [ ACC_A ⇒ λacc_a: True. 144 Instruction (SUBB ? ACC_A accumulator_address) 145  DIRECT d ⇒ λdirect3: True. 146 Instruction (SUBB ? ACC_A (DIRECT d)) 147  REGISTER r ⇒ λregister3: True. 148 Instruction (SUBB ? ACC_A (REGISTER r)) 149  _ ⇒ λother: False. ⊥ 150 ] (subaddressing_modein … reg') 151  And ⇒ 152 let reg' ≝ register_address reg in 153 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 154 direct; 155 registr ]] x) → ? with 156 [ ACC_A ⇒ λacc_a: True. 157 Instruction (NOP ?) 158  DIRECT d ⇒ λdirect4: True. 159 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 160  REGISTER r ⇒ λregister4: True. 161 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 162  _ ⇒ λother: False. ⊥ 163 ] (subaddressing_modein … reg') 164  Or ⇒ 165 let reg' ≝ register_address reg in 166 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 167 direct; 168 registr ]] x) → ? with 169 [ ACC_A ⇒ λacc_a: True. 170 Instruction (NOP ?) 171  DIRECT d ⇒ λdirect5: True. 172 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 173  REGISTER r ⇒ λregister5: True. 174 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 175  _ ⇒ λother: False. ⊥ 176 ] (subaddressing_modein … reg') 177  Xor ⇒ 178 let reg' ≝ register_address reg in 179 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 180 direct; 181 registr ]] x) → ? with 182 [ ACC_A ⇒ λacc_a: True. 183 Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) 184  DIRECT d ⇒ λdirect6: True. 185 Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) 186  REGISTER r ⇒ λregister6: True. 187 Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) 188  _ ⇒ λother: False. ⊥ 189 ] (subaddressing_modein … reg') 190 ] 191  INT reg byte ⇒ 192 let reg' ≝ register_address reg in 193 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 194 direct; 195 registr ]] x) → ? with 196 [ REGISTER r ⇒ λregister7: True. 197 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) 198  ACC_A ⇒ λacc: True. 199 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) 200  DIRECT d ⇒ λdirect7: True. 201 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) 202  _ ⇒ λother: False. ⊥ 203 ] (subaddressing_modein … reg') 204  MOVE regs ⇒ 205 match regs with 206 [ from_acc reg ⇒ 151 [ step_seq instr' ⇒ 152 match instr' with 153 [ extension_seq ext ⇒ 154 match ext with 155 [ SAVE_CARRY ⇒ 156 Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) 157  RESTORE_CARRY ⇒ 158 Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 159 ] 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 _ _ _ _ ⇒ 168 match accs with 169 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 170  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 171 ] 172  OP1 op1 _ _ ⇒ 173 match op1 with 174 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 175  Inc ⇒ Instruction (INC ? ACC_A) 176  Rl ⇒ Instruction (RL ? ACC_A) 177 ] 178  OP2 op2 _ _ reg ⇒ 179 match op2 with 180 [ Add ⇒ 181 let reg' ≝ arg_address reg in 182 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 183 direct; 184 registr; 185 data ]] x) → ? with 186 [ ACC_A ⇒ λacc_a: True. 187 Instruction (ADD ? ACC_A accumulator_address) 188  DIRECT d ⇒ λdirect1: True. 189 Instruction (ADD ? ACC_A (DIRECT d)) 190  REGISTER r ⇒ λregister1: True. 191 Instruction (ADD ? ACC_A (REGISTER r)) 192  DATA b ⇒ λdata : True. 193 Instruction (ADD ? ACC_A (DATA b)) 194  _ ⇒ Ⓧ 195 ] (subaddressing_modein … reg') 196  Addc ⇒ 197 let reg' ≝ arg_address reg in 198 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 199 direct; 200 registr; 201 data ]] x) → ? with 202 [ ACC_A ⇒ λacc_a: True. 203 Instruction (ADDC ? ACC_A accumulator_address) 204  DIRECT d ⇒ λdirect2: True. 205 Instruction (ADDC ? ACC_A (DIRECT d)) 206  REGISTER r ⇒ λregister2: True. 207 Instruction (ADDC ? ACC_A (REGISTER r)) 208  DATA b ⇒ λdata : True. 209 Instruction (ADDC ? ACC_A (DATA b)) 210  _ ⇒ Ⓧ 211 ] (subaddressing_modein … reg') 212  Sub ⇒ 213 let reg' ≝ arg_address reg in 214 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 215 direct; 216 registr; 217 data ]] x) → ? with 218 [ ACC_A ⇒ λacc_a: True. 219 Instruction (SUBB ? ACC_A accumulator_address) 220  DIRECT d ⇒ λdirect3: True. 221 Instruction (SUBB ? ACC_A (DIRECT d)) 222  REGISTER r ⇒ λregister3: True. 223 Instruction (SUBB ? ACC_A (REGISTER r)) 224  DATA b ⇒ λdata : True. 225 Instruction (SUBB ? ACC_A (DATA b)) 226  _ ⇒ Ⓧ 227 ] (subaddressing_modein … reg') 228  And ⇒ 229 let reg' ≝ arg_address reg in 230 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 231 direct; 232 registr; 233 data ]] x) → ? with 234 [ ACC_A ⇒ λacc_a: True. 235 Instruction (NOP ?) 236  DIRECT d ⇒ λdirect4: True. 237 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 238  REGISTER r ⇒ λregister4: True. 239 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 240  DATA b ⇒ λdata : True. 241 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) 242  _ ⇒ Ⓧ 243 ] (subaddressing_modein … reg') 244  Or ⇒ 245 let reg' ≝ arg_address reg in 246 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 247 direct; 248 registr ; data ]] x) → ? with 249 [ ACC_A ⇒ λacc_a: True. 250 Instruction (NOP ?) 251  DIRECT d ⇒ λdirect5: True. 252 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 253  REGISTER r ⇒ λregister5: True. 254 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 255  DATA b ⇒ λdata : True. 256 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))) 257  _ ⇒ Ⓧ 258 ] (subaddressing_modein … reg') 259  Xor ⇒ 260 let reg' ≝ arg_address reg in 261 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 262 direct; 263 registr ; data ]] x) → ? with 264 [ ACC_A ⇒ λacc_a: True. 265 Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) 266  DIRECT d ⇒ λdirect6: True. 267 Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) 268  REGISTER r ⇒ λregister6: True. 269 Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) 270  DATA b ⇒ λdata : True. 271 Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉)) 272  _ ⇒ Ⓧ 273 ] (subaddressing_modein … reg') 274 ] 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 279 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 280  SET_CARRY ⇒ 281 Instruction (SETB ? CARRY) 282  MOVE regs ⇒ 283 match regs with 284 [ to_acc _ reg ⇒ 285 let reg' ≝ register_address reg in 286 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 287 direct; 288 registr ]] x) → ? with 289 [ REGISTER r ⇒ λregister9: True. 290 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 291  DIRECT d ⇒ λdirect9: True. 292 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 293  ACC_A ⇒ λacc_a: True. 294 Instruction (NOP ?) 295  _ ⇒ λother: False. ⊥ 296 ] (subaddressing_modein … reg') 297  from_acc reg _ ⇒ 207 298 let reg' ≝ register_address reg in 208 299 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; … … 217 308  _ ⇒ λother: False. ⊥ 218 309 ] (subaddressing_modein … reg') 219  to_acc reg ⇒ 220 let reg' ≝ register_address reg in 221 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 222 direct; 223 registr ]] x) → ? with 224 [ REGISTER r ⇒ λregister9: True. 225 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 226  DIRECT d ⇒ λdirect9: True. 227 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 228  ACC_A ⇒ λacc_a: True. 229 Instruction (NOP ?) 230  _ ⇒ λother: False. ⊥ 231 ] (subaddressing_modein … reg')] 232  LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 233  STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 234  ADDRESS addr proof _ _ ⇒ 235 let look ≝ association addr globals (prf ? proof) in 236 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 310  int_to_reg reg bv ⇒ 311 let b ≝ asm_byte_of_beval bv in 312 let reg' ≝ register_address reg in 313 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 314 direct; 315 registr ]] x) → ? with 316 [ REGISTER r ⇒ λregister7: True. 317 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉)))))) 318  ACC_A ⇒ λacc: True. 319 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) 320  DIRECT d ⇒ λdirect7: True. 321 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉))))) 322  _ ⇒ λother: False. ⊥ 323 ] (subaddressing_modein … reg') 324  int_to_acc _ bv ⇒ 325 let b ≝ asm_byte_of_beval bv in 326 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))))) 327 ] 328 ] 237 329  COND _ lbl ⇒ 238 330 (* dpm: this should be handled in translate_code! *) 239 331 Instruction (JNZ ? (toASM_ident ? lbl)) 240  SET_CARRY ⇒241 Instruction (SETB ? CARRY)242 332 ] 243 333 ]. … … 272 362 match def with 273 363 [ Internal int ⇒ 274 let code ≝ joint_if_code … (lin_params globals_old)int in364 let code ≝ joint_if_code LIN globals_old int in 275 365 match translate_code globals globals_old prf code with 276 366 [ nil ⇒ ⊥ … … 293 383 let rec flatten_fun_defs 294 384 (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat) 295 (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function globals_old (lin_params globals_old)))))385 (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old)))) 296 386 on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝ 297 387 match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with 
src/LIN/joint_LTL_LIN.ma
r1378 r2286 2 2 3 3 inductive registers_move: Type[0] ≝ 4  from_acc: Register → registers_move 5  to_acc: Register → registers_move. 4  from_acc: Register → unit → registers_move 5  to_acc: unit → Register → registers_move 6  int_to_reg : Register → beval → registers_move 7  int_to_acc : unit → beval → registers_move. 8 (* the last is redudant, but kept for notation's sake *) 6 9 7 definition ltl_lin_params__: params__ ≝ 8 mk_params__ unit unit unit unit registers_move Register nat unit False. 9 definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit. 10 definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit. 10 inductive ltl_lin_seq : Type[0] ≝ 11  SAVE_CARRY : ltl_lin_seq 12  RESTORE_CARRY : ltl_lin_seq. 13 14 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params 15 (* acc_a_reg ≝ *) unit 16 (* acc_b_reg ≝ *) unit 17 (* acc_a_arg ≝ *) unit 18 (* acc_b_arg ≝ *) unit 19 (* dpl_reg ≝ *) unit 20 (* dph_reg ≝ *) unit 21 (* dpl_arg ≝ *) unit 22 (* dph_arg ≝ *) unit 23 (* snd_arg ≝ *) hdw_argument 24 (* pair_move ≝ *) registers_move 25 (* call_args ≝ *) ℕ 26 (* call_dest ≝ *) unit 27 (* ext_seq ≝ *) ltl_lin_seq 28 (* ext_call ≝ *) void 29 (* ext_tailcall ≝ *) void 30 (* paramsT ≝ *) unit 31 (* localsT ≝ *) void. 32 33 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). 34 interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)). 35 interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)). 36 interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)). 
src/LIN/joint_LTL_LIN_semantics.ma
r1451 r2286 4 4 definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e). 5 5 definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r). 6 definition hw_arg_retrieve ≝ 7 λl,a.match a with 8 [ Reg r ⇒ hw_reg_retrieve l r 9  Imm b ⇒ OK … b 10 ]. 6 11 7 definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) := 8 λsuccT. 9 mk_more_sem_params ? 10 unit it hw_register_env init_hw_register_env 0 it 11 hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA) 12 (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB) 13 (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL) 14 (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH) 15 (λlocals,dest_src. 16 match dest_src with 17 [ from_acc reg ⇒ 18 do v ← hw_reg_retrieve locals RegisterA ; 19 hw_reg_store reg v locals 20  to_acc reg ⇒ 21 do v ← hw_reg_retrieve locals reg ; 22 hw_reg_store RegisterA v locals ]). 12 definition eval_registers_move ≝ λe,m. 13 match m with 14 [ from_acc r _ ⇒ 15 hw_reg_store r (hwreg_retrieve e RegisterA) e 16  to_acc _ r ⇒ 17 hw_reg_store RegisterA (hwreg_retrieve e r) e 18  int_to_reg r v ⇒ 19 hw_reg_store r v e 20  int_to_acc _ v ⇒ 21 hw_reg_store RegisterA v e 22 ]. 23 23 24 definition ltl_lin_sem_params: ∀succT. sem_params ≝ 25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT). 26 27 28 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. 29 definition ltl_lin_pop_frame: 30 ∀succT,codeT,lookup. 31 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → 32 state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝ 33 λ_.λ_.λ_.λ_.λ_.λt.OK … t. 34 definition ltl_lin_save_frame: 35 ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝ 36 λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l. 37 38 (* The following implementation only works for functions that return 32 bits *) 39 definition ltl_lin_result_regs: 40 ∀succT,codeT,lookup. 41 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → 42 state (ltl_lin_sem_params succT) → res (list Register) ≝ 43 λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets. 24 definition LTL_LIN_state : sem_state_params ≝ 25 mk_sem_state_params 26 (* framesT ≝ *) unit 27 (* empty_framesT ≝ *) it 28 (* regsT ≝ *) hw_register_env 29 (* empty_regsT ≝ *) init_hw_register_env. 44 30 45 31 (*CSC: XXXX, for external functions only*) 46 axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT)→ res (list val).47 axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).32 axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val). 33 axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state). 48 34 49 definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT))) 50 ≝ λsuccT,p,globals,ge,abs. ⊥. 51 @abs qed. 35 (* TODO (needs another bit to be added to hdw) *) 36 axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state). 52 37 53 definition ltl_lin_more_sem_params2: 54 ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch. 55 ∀pointer_of_label: ∀globals. genv globals 56 (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) 57 →pointer→label→res (Σp0:pointer.ptype p0=Code). 58 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝ 59 λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals. 60 mk_more_sem_params2 … 61 (mk_more_sem_params1 … (ltl_lin_more_sem_params …) 62 succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …) 63 ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …) 64 (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …). 65 66 definition ltl_lin_fullexec ≝ 67 λsuccT,codeT,lookup,succ,fetch,pointer_of_label. 68 joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)). 38 definition LTL_LIN_semantics ≝ 39 λF.mk_more_sem_unserialized_params LTL_LIN F 40 (* st_pars ≝ *) LTL_LIN_state 41 (* acca_store_ ≝ *) (λ_.hw_reg_store RegisterA) 42 (* acca_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA) 43 (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA) 44 (* accb_store_ ≝ *) (λ_.hw_reg_store RegisterB) 45 (* accb_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB) 46 (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB) 47 (* dpl_store_ ≝ *) (λ_.hw_reg_store RegisterDPL) 48 (* dpl_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL) 49 (* dpl_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL) 50 (* dph_store_ ≝ *) (λ_.hw_reg_store RegisterDPH) 51 (* dph_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH) 52 (* dph_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH) 53 (* snd_arg_retrieve_ ≝ *) hw_arg_retrieve 54 (* pair_reg_move_ ≝ *) eval_registers_move 55 (* fetch_ra ≝ *) (load_ra …) 56 (* allocate_local ≝ *) (λabs.match abs in void with [ ]) 57 (* save_frame ≝ *) (λp.λ_.λst.save_ra … st p) 58 (* setup_call ≝ *) (λ_.λ_.λ_.λst.return st) 59 (* fetch_external_args≝ *) ltl_lin_fetch_external_args 60 (* set_result ≝ *) ltl_lin_set_result 61 (* call_args_for_main ≝ *) 0 62 (* call_dest_for_main ≝ *) it 63 (* read_result ≝ *) (λ_.λ_.λ_. 64 λst.return map … (hwreg_retrieve (regs … st)) RegisterRets) 65 (* eval_ext_seq ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s) 66 (* eval_ext_tailcall ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 67 (* eval_ext_call ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 68 (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st) 69 (* post_op2 ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st). 
src/LIN/semantics.ma
r1601 r2286 2 2 include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) 3 3 4 definition lin_succ_pc: unit → address → res address := 5 λ_.λaddr. addr_add addr 1. 6 7 axiom BadOldPointer: String. 8 (*CSC: XXX factorize the code with graph_fetch_function!!! *) 9 definition lin_fetch_function: 10 ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝ 11 λglobals,ge,old. 12 let b ≝ pblock old in 13 do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b); 14 match def with 15 [ Internal fn ⇒ OK … fn 16  External _ ⇒ Error … [MSG BadOldPointer]]. 17 18 axiom BadLabel: String. 19 definition lin_pointer_of_label: 20 ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝ 21 λglobals,ge,old,l. 22 do fn ← lin_fetch_function … ge old ; 23 do pos ← 24 opt_to_res ? [MSG BadLabel] 25 (position_of ? 26 (λs. let 〈l',x〉 ≝ s in 27 match l' with [ None ⇒ false  Some l'' ⇒ if eq_identifier … l l'' then true else false]) 28 (joint_if_code … (lin_params …) fn)) ; 29 OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). 30 // qed. 31 32 (*CSC: XXX factorize code with graph_fetch_statement?*) 33 axiom BadProgramCounter: String. 34 definition lin_fetch_statement: 35 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝ 36 λglobals,ge,st. 37 do ppc ← pointer_of_address (pc … st) ; 38 do fn ← lin_fetch_function … ge ppc ; 39 let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *) 40 do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ; 41 OK … (\snd found). 42 43 definition lin_fullexec: fullexec io_out io_in ≝ 44 ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label. 4 definition LIN_semantics : sem_params ≝ 5 make_sem_lin_params LIN (LTL_LIN_semantics ?).
Note: See TracChangeset
for help on using the changeset viewer.