- Timestamp:
- Mar 30, 2011, 12:34:25 PM (10 years ago)
- Location:
- src
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/CHANGES
r721 r723 10 10 11 11 Formalised missing Assembly.ma file. 12 13 30/03/2011: 14 Split translate_statements into two functions. 15 16 Added a dependent type for the invariant that a LIN function body does not 17 start with a label, and is not empty. -
src/LIN/LIN.ma
r722 r723 1 include "arithmetics/nat.ma". 2 include "ASM/String.ma". 1 include "LIN/JointLTLLIN.ma". 2 3 definition PreLINStatement ≝ JointStatement unit. 3 4 4 include "ASM/I8051.ma".5 include "common/AST.ma".6 7 alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".8 alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".9 10 inductive JointInstruction (globals: list Identifier): Type[0] ≝11 | Joint_Instr_Goto: Identifier → JointInstruction globals12 | Joint_Instr_Comment: String → JointInstruction globals13 | Joint_Instr_CostLabel: Identifier → JointInstruction globals14 | Joint_Instr_Int: Register → Byte → JointInstruction globals15 | Joint_Instr_Pop: JointInstruction globals16 | Joint_Instr_Push: JointInstruction globals17 | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals18 | Joint_Instr_FromAcc: Register → JointInstruction globals19 | Joint_Instr_ToAcc: Register → JointInstruction globals20 | Joint_Instr_OpAccs: OpAccs → JointInstruction globals21 | Joint_Instr_Op1: Op1 → JointInstruction globals22 | Joint_Instr_Op2: Op2 → Register → JointInstruction globals23 | Joint_Instr_ClearCarry: JointInstruction globals24 | Joint_Instr_Load: JointInstruction globals25 | Joint_Instr_Store: JointInstruction globals26 | Joint_Instr_CallId: Identifier → JointInstruction globals27 | Joint_Instr_CondAcc: Identifier → JointInstruction globals.28 29 inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝30 | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals31 | LIN_St_Return: JointStatement A globals.32 33 5 definition LINStatement ≝ 34 6 λglobals. 35 option Identifier × (JointStatement unit globals). 36 37 definition LINInternalFunction ≝ λglobals. list (LINStatement globals). 7 option Identifier × (PreLINStatement globals). 38 8 9 definition WellFormedP ≝ 10 λA, B: Type[0]. 11 λcode: list (option A × B). 12 match code with 13 [ nil ⇒ False 14 | cons hd tl ⇒ 15 match \fst hd with 16 [ Some lbl ⇒ False 17 | None ⇒ True 18 ] 19 ]. 20 39 21 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝ 40 LIN_Fu_Internal: LINInternalFunction globals→ LINFunctionDefinition globals22 LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals 41 23 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals. 42 24 -
src/LIN/LINToASM.ma
r722 r723 32 32 let generated ≝ 33 33 match instr with 34 [ LIN_St_Sequential instr' _ ⇒34 [ Joint_St_Sequential instr' _ ⇒ 35 35 match instr' with 36 36 [ Joint_Instr_Goto lbl ⇒ set_insert ? lbl (set_empty ?) … … 39 39 | _ ⇒ set_empty ? 40 40 ] 41 | LIN_St_Return ⇒ set_empty ?41 | Joint_St_Return ⇒ set_empty ? 42 42 ] in 43 43 match label with … … 59 59 let 〈ignore, fun_def〉 ≝ f in 60 60 match fun_def return λ_. BitVectorTrieSet ? with 61 [ LIN_Fu_Internal stmts ⇒61 [ LIN_Fu_Internal stmts proof ⇒ 62 62 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts 63 63 | LIN_Fu_External _ ⇒ set_empty ? … … 86 86 λglobals_old: list Identifier. 87 87 λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals). 88 λstatement: LINStatement globals_old.89 〈\fst statement, match \sndstatement with90 [ LIN_St_Return ⇒ [ Instruction (RET ?) ]91 | LIN_St_Sequential instr _⇒88 λstatement: PreLINStatement globals_old. 89 match statement with 90 [ Joint_St_Return ⇒ Instruction (RET ?) 91 | Joint_St_Sequential instr _⇒ 92 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 ]93 [ Joint_Instr_Goto lbl ⇒ Jmp lbl 94 | Joint_Instr_Comment comment ⇒ Comment 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 100 | Joint_Instr_OpAccs accs ⇒ 101 101 match accs with 102 [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]103 | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]102 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 103 | Divu ⇒ Instruction (DIV ? ACC_A ACC_B) 104 104 | Modu ⇒ ? 105 105 ] 106 106 | Joint_Instr_Op1 op1 ⇒ 107 107 match op1 with 108 [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]109 | Inc ⇒ [ Instruction (INC ? ACC_A) ]108 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 109 | Inc ⇒ Instruction (INC ? ACC_A) 110 110 ] 111 111 | Joint_Instr_Op2 op2 reg ⇒ … … 117 117 register ]] x) → ? with 118 118 [ ACC_A ⇒ λacc_a: True. 119 [ Instruction (ADD ? ACC_A accumulator_address) ]119 Instruction (ADD ? ACC_A accumulator_address) 120 120 | DIRECT d ⇒ λdirect1: True. 121 [ Instruction (ADD ? ACC_A (DIRECT d)) ]121 Instruction (ADD ? ACC_A (DIRECT d)) 122 122 | REGISTER r ⇒ λregister1: True. 123 [ Instruction (ADD ? ACC_A (REGISTER r)) ]123 Instruction (ADD ? ACC_A (REGISTER r)) 124 124 | _ ⇒ λother: False. ⊥ 125 125 ] (subaddressing_modein … reg') … … 130 130 register ]] x) → ? with 131 131 [ ACC_A ⇒ λacc_a: True. 132 [ Instruction (ADDC ? ACC_A accumulator_address) ]132 Instruction (ADDC ? ACC_A accumulator_address) 133 133 | DIRECT d ⇒ λdirect2: True. 134 [ Instruction (ADDC ? ACC_A (DIRECT d)) ]134 Instruction (ADDC ? ACC_A (DIRECT d)) 135 135 | REGISTER r ⇒ λregister2: True. 136 [ Instruction (ADDC ? ACC_A (REGISTER r)) ]136 Instruction (ADDC ? ACC_A (REGISTER r)) 137 137 | _ ⇒ λother: False. ⊥ 138 138 ] (subaddressing_modein … reg') … … 143 143 register ]] x) → ? with 144 144 [ ACC_A ⇒ λacc_a: True. 145 [ Instruction (SUBB ? ACC_A accumulator_address) ]145 Instruction (SUBB ? ACC_A accumulator_address) 146 146 | DIRECT d ⇒ λdirect3: True. 147 [ Instruction (SUBB ? ACC_A (DIRECT d)) ]147 Instruction (SUBB ? ACC_A (DIRECT d)) 148 148 | REGISTER r ⇒ λregister3: True. 149 [ Instruction (SUBB ? ACC_A (REGISTER r)) ]149 Instruction (SUBB ? ACC_A (REGISTER r)) 150 150 | _ ⇒ λother: False. ⊥ 151 151 ] (subaddressing_modein … reg') … … 156 156 register ]] x) → ? with 157 157 [ ACC_A ⇒ λacc_a: True. 158 [ Instruction (NOP ?) ]158 Instruction (NOP ?) 159 159 | DIRECT d ⇒ λdirect4: True. 160 [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]160 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 161 161 | REGISTER r ⇒ λregister4: True. 162 [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]162 Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 163 163 | _ ⇒ λother: False. ⊥ 164 164 ] (subaddressing_modein … reg') … … 169 169 register ]] x) → ? with 170 170 [ ACC_A ⇒ λacc_a: True. 171 [ Instruction (NOP ?) ]171 Instruction (NOP ?) 172 172 | DIRECT d ⇒ λdirect5: True. 173 [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]173 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) 174 174 | REGISTER r ⇒ λregister5: True. 175 [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]175 Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) 176 176 | _ ⇒ λother: False. ⊥ 177 177 ] (subaddressing_modein … reg') … … 182 182 register ]] x) → ? with 183 183 [ ACC_A ⇒ λacc_a: True. 184 [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]184 Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) 185 185 | DIRECT d ⇒ λdirect6: True. 186 [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]186 Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) 187 187 | REGISTER r ⇒ λregister6: True. 188 [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]188 Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) 189 189 | _ ⇒ λother: False. ⊥ 190 190 ] (subaddressing_modein … reg') … … 196 196 register ]] x) → ? with 197 197 [ REGISTER r ⇒ λregister7: True. 198 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]198 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) 199 199 | ACC_A ⇒ λacc: True. 200 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]200 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) 201 201 | DIRECT d ⇒ λdirect7: True. 202 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]202 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) 203 203 | _ ⇒ λother: False. ⊥ 204 204 ] (subaddressing_modein … reg') … … 209 209 register ]] x) → ? with 210 210 [ REGISTER r ⇒ λregister8: True. 211 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]211 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) 212 212 | ACC_A ⇒ λacc: True. 213 [ Instruction (NOP ?) ]213 Instruction (NOP ?) 214 214 | DIRECT d ⇒ λdirect8: True. 215 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]215 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) 216 216 | _ ⇒ λother: False. ⊥ 217 217 ] (subaddressing_modein … reg') … … 222 222 register ]] x) → ? with 223 223 [ REGISTER r ⇒ λregister9: True. 224 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]224 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) 225 225 | DIRECT d ⇒ λdirect9: True. 226 [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]226 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) 227 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〉)) ]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 233 | Joint_Instr_Address addr proof ⇒ 234 234 let look ≝ association addr globals (prf ? proof) in 235 [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]235 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 236 236 | Joint_Instr_CondAcc lbl ⇒ 237 237 (* dpm: this should be handled in translate_code! *) 238 [ WithLabel (JNZ ? lbl) ]238 WithLabel (JNZ ? lbl) 239 239 ] 240 ] 〉.240 ]. 241 241 try assumption 242 242 try @ I 243 243 cases ImplementedInRuntime 244 244 qed. 245 246 definition build_translated_statement ≝ 247 λglobals. 248 λglobals_old. 249 λprf. 250 λstatement: LINStatement globals_old. 251 〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉. 245 252 246 253 definition translate_code ≝ … … 249 256 λprf. 250 257 λcode: list (LINStatement globals_old). 251 flatten ? (map ? ? (translate_statements globals globals_old prf) code).258 map ? ? (build_translated_statement globals globals_old prf) code. 252 259 260 lemma translate_code_preserves_WellFormedP: 261 ∀globals, globals_old, prf, code. 262 WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code). 263 #G #GO #P #C 264 elim C 265 [ normalize 266 // 267 | #G2 #G02 #IH (* CSC: understand here *) 268 whd in ⊢ (% → %) 269 normalize in ⊢ (% → %) 270 // 271 ] 272 qed. 273 253 274 definition translate_fun_def ≝ 254 λglobals.λglobals_old.λprf. 275 λglobals. 276 λglobals_old. 277 λprf. 255 278 λid_def. 256 279 let 〈id, def〉 ≝ id_def in 257 280 match def with 258 [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals globals_old prf code) 281 [ LIN_Fu_Internal code proof ⇒ 282 match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with 283 [ nil ⇒ λprf2. ⊥ 284 | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl 285 ] (translate_code_preserves_WellFormedP globals globals_old prf code proof) 259 286 | _ ⇒ [ ] 260 287 ]. 288 @ prf2 289 qed. 261 290 262 291 definition translate_functs ≝ … … 270 299 match main with 271 300 [ None ⇒ [ ] 272 | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label]301 | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] 273 302 ] in 274 303 preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)). … … 287 316 (* dpm: plays the role of the string "_exit" in the O'caml source *) 288 317 axiom identifier_prefix: Identifier. 318 319 (* dpm: fresh prefix stuff needs unifying with brian *) 289 320 290 321 (* … … 295 326 let global_addr ≝ globals_addr (LIN_Pr_vars p) in 296 327 〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉. 297 328 *) -
src/LTL/LTL.ma
r722 r723 1 1 include "common/Graphs.ma". 2 include "common/AST.ma".3 4 2 include "utilities/IdentifierTools.ma". 5 6 include "ASM/I8051.ma".7 include "ASM/String.ma".8 3 9 4 include "LIN/LIN.ma". -
src/LTL/LTLToLIN.ma
r722 r723 2 2 include "LIN/LIN.ma". 3 3 4 definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝4 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝ 5 5 λglobals: list Identifier. 6 6 λs: LTLStatement globals. 7 7 match s with 8 [ LIN_St_Return ⇒ LIN_St_Return ? globals9 | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it8 [ Joint_St_Return ⇒ Joint_St_Return ? globals 9 | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it 10 10 ].
Note: See TracChangeset
for help on using the changeset viewer.