Changeset 2899 for src/ASM/Interpret2.ma
- Timestamp:
- Mar 19, 2013, 12:33:13 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret2.ma
r2875 r2899 42 42 mk_preclassified_system_of_abstract_status 43 43 labelled_object_code 44 ( ASM_abstract_status cm (costlabels c))44 (OC_abstract_status cm (costlabels c)) 45 45 (λst. return (execute_1 … st)) 46 46 (initialise_status … cm). 47 48 (* Pre-classified system for ASM *) 49 50 include "ASM/Assembly.ma". 51 52 (* Move next function in interpret? *) 53 definition execute_1_pseudo_instruction': 54 ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝ 55 λcm,sigma,policy,status. 56 execute_1_pseudo_instruction cm 57 (ticks_of cm sigma policy) status …. 58 cases daemon (*CSC: we need to prove that we remain inside the program 59 (code closed), which is impossible in case of function pointers. 60 But the type does not allow to fail (yet?) *) 61 qed. 62 63 definition classify_pseudo_instruction: pseudo_instruction → status_class ≝ 64 λinstr. 65 match instr with 66 [ Instruction pre ⇒ ASM_classify00 … pre 67 | Comment _ ⇒ cl_other 68 | Cost _ ⇒ cl_other 69 | Jmp _ ⇒ cl_other 70 | Jnz _ _ _ ⇒ cl_jump 71 | MovSuccessor _ _ _ ⇒ cl_other 72 | Call _ ⇒ cl_call 73 | Mov _ _ ⇒ cl_other ]. 74 75 definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝ 76 λcm,s. 77 classify_pseudo_instruction 78 (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)). 79 cases daemon (*CSC: again*) 80 qed. 81 82 definition ASM_next_instruction_properly_relates_program_counters ≝ 83 λcm. 84 λbefore: PseudoStatus cm. 85 λafter : PseudoStatus cm. 86 let 〈instruction, program_counter_after〉 ≝ 87 fetch_pseudo_instruction (code cm) (program_counter … before) ? 88 in 89 program_counter ?? after = program_counter_after. 90 cases daemon (*CSC: again*) 91 qed. 92 93 definition ASM_as_label_of_pc: 94 ∀prog:pseudo_assembly_program. Word → option costlabel 95 ≝ 96 λprog,pc. 97 match \fst (fetch_pseudo_instruction (code prog) pc ?) with 98 [ Cost label ⇒ Some … label 99 | _ ⇒ None ? ]. 100 cases daemon (*CSC: again*) 101 qed. 102 103 definition ASM_abstract_status: 104 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝ 105 λprog,sigma,policy. 106 mk_abstract_status 107 (PseudoStatus prog) 108 (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2) 109 word_deqset 110 (program_counter …) 111 (ASM_classify …) 112 (ASM_as_label_of_pc prog …) 113 (ASM_next_instruction_properly_relates_program_counters prog) 114 ? (* (λs.False) *) 115 ? 116 ?. 117 #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *) 118 qed. 119 120 definition ASM_preclassified_system: 121 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝ 122 λc,sigma,policy. 123 mk_preclassified_system_of_abstract_status 124 pseudo_assembly_program 125 (ASM_abstract_status c sigma policy) 126 (λst. return (execute_1_pseudo_instruction' … sigma policy st)) 127 (initialise_status … c).
Note: See TracChangeset
for help on using the changeset viewer.