Changeset 2764 for src/ASM/Interpret2.ma
- Timestamp:
- Mar 2, 2013, 11:59:37 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret2.ma
r2756 r2764 2 2 include "common/Measurable.ma". 3 3 4 (* 5 (* Transition system on the assembly code *) 6 7 (*CSC: waiting for Jaap's code to compile or to be splitted from Assembly.ma *) 8 axiom policy: pseudo_assembly_program → Type[0]. 9 (*CSC: problem here: mk_policy should be allowed to fail, but mk_fullexec does 10 not allow make_global to fail too *) 11 axiom mk_policy: ∀p:pseudo_assembly_program. policy p. 12 13 (*CSC: already implemented in AssemblyProof.ma: move elsewhere *) 14 axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat. 15 16 definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝ 17 λp. ticks_of … (mk_policy p). 18 19 (* 20 definition execute_1_pseudo_instruction_trace: 21 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝ 22 λticks_of,s. 23 let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in 24 let s ≝ execute_1_pseudo_instruction ticks_of s in 25 match instr with 26 [ Cost cst ⇒ ret … 〈Echarge cst, s〉 27 | _ ⇒ ret ? 〈E0, s〉 ]. 28 29 axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int. 30 31 definition pseudo_exec: trans_system io_out io_in ≝ 32 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace. 33 34 definition pseudo_ASM_fullexec: fullexec io_out io_in ≝ 35 mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)). 36 37 (* Transition system on the object code *) 38 39 definition make_global: labelled_object_code → BitVectorTrie costlabel 16 ≝ \snd. 40 41 definition execute_1_instruction: 42 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝ 43 λcosts,s. 44 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in 45 let 〈instr,pc〉 ≝ instr_pc in 46 match lookup_opt … pc costs with 47 [ None ⇒ ret … 〈E0, s〉 48 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ]. 49 50 axiom is_final: BitVectorTrie costlabel 16 → Status → option int. 51 52 definition exec: trans_system io_out io_in ≝ 53 mk_trans_system … is_final execute_1_instruction. 54 *) 55 56 axiom exec: trans_system io_out io_in. 57 58 definition ASM_fullexec: fullexec io_out io_in ≝ 59 mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*). 60 *) 61 4 (* Move where abstract_status is defined! *) 62 5 definition mk_trans_system_of_abstract_status: 63 abstract_status→ trans_system io_out io_in6 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in 64 7 ≝ 65 λS .8 λS,as_eval. 66 9 mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S) 67 10 (λ_.λstatus. … … 73 16 return 〈 tr, status' 〉). 74 17 75 definition mk_fullexec_of_abstract_status: abstract_status → fullexec io_out io_in 76 ≝ λS. 77 mk_fullexec ?? unit (mk_trans_system_of_abstract_status S) (λ_.it) 78 (λ_.as_init S). 18 definition mk_fullexec_of_abstract_status: 19 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in 20 ≝ λS,as_eval,as_init. 21 mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 22 (λ_.return as_init). 79 23 80 24 definition mk_preclassified_system_of_abstract_status: 81 abstract_status→ preclassified_system82 ≝ λS .25 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system 26 ≝ λS,as_eval,as_init. 83 27 mk_preclassified_system 84 (mk_fullexec_of_abstract_status S) (λ_.λst. ¬(is_none … (as_label … st))) 28 (mk_fullexec_of_abstract_status S as_eval as_init) 29 (λ_.λst. ¬(is_none … (as_label … st))) 85 30 (λ_.as_classify S) 86 31 (λ_.λst,prf. as_call_ident S «st,?»). 87 32 @hide_prf cases (as_classify ??) in prf; normalize // * 88 qed. 33 qed. 89 34 90 (* 91 definition OC_transition_system: trans_system io_out io_in ≝ 92 mk_trans_system ?? OC_global OC_status ? 93 execute_1_instruction. 35 (* End move *) 94 36 95 definition OC_global ≝ BitVectorTrie Byte 16 × costlabel_map. 96 97 definition OC_status ≝ λgl:OC_global. Status (\fst gl). 98 99 definition execute_1_instruction: 100 ∀g:OC_global. OC_status g → IO io_out io_in (trace × OC_status g) ≝ 101 λg. let 〈cm,costs〉 ≝ g in λs. 102 let 〈instr, pc,ticks〉 ≝ fetch cm (program_counter … s) in 103 let s' ≝ execute_1 s in 104 match lookup_opt … pc costs with 105 [ None ⇒ ret … 〈E0, s'〉 106 | Some cst ⇒ ret … 〈Echarge cst, s'〉 ]. 107 108 definition OC_transition_system: trans_system io_out io_in ≝ 109 mk_trans_system ?? OC_global OC_status ? 110 execute_1_instruction. 111 112 definition OC_fullexec: fullexec io_out io_in ≝ 113 mk_fullexec ?? 114 labelled_object_code*) 115 116 117 definition OC_preclassified_system ≝ 37 definition OC_preclassified_system: labelled_object_code → preclassified_system ≝ 118 38 λc:labelled_object_code. 119 mk_preclassified_system_of_abstract_status (ASM_abstract_status (\fst c) (\fst (\snd c))). 39 let cm ≝ load_code_memory (oc c) in 40 mk_preclassified_system_of_abstract_status 41 (ASM_abstract_status cm (costlabels c)) 42 (λst. return (execute_1 … st)) 43 (initialise_status … cm).
Note: See TracChangeset
for help on using the changeset viewer.