source: src/ASM/Interpret2.ma @ 2762

Last change on this file since 2762 was 2756, checked in by sacerdot, 7 years ago

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File size: 4.1 KB
Line 
1include "ASM/ASMCosts.ma".
2include "common/Measurable.ma".
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 *)
8axiom 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 *)
11axiom mk_policy: ∀p:pseudo_assembly_program. policy p.
12
13(*CSC: already implemented in AssemblyProof.ma: move elsewhere *)
14axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat.
15
16definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝
17 λp. ticks_of … (mk_policy p).
18
19(*
20definition 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
29axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
30
31definition pseudo_exec: trans_system io_out io_in ≝
32 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.
33
34definition 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
39definition make_global: labelled_object_code → BitVectorTrie costlabel 16 ≝ \snd.
40
41definition 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
50axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
51
52definition exec: trans_system io_out io_in ≝
53 mk_trans_system … is_final execute_1_instruction.
54*)
55
56axiom exec: trans_system io_out io_in.
57
58definition ASM_fullexec: fullexec io_out io_in ≝
59 mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*).
60*)
61
62definition mk_trans_system_of_abstract_status:
63 abstract_status → trans_system io_out io_in
64
65 λS.
66  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
67   (λ_.λstatus.
68     let tr ≝
69      match as_label … status with
70      [ Some cst ⇒ Echarge cst
71      | None ⇒ E0 ] in
72     ! status' ← as_eval … status ;
73     return 〈 tr, status' 〉).
74
75definition 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).
79
80definition mk_preclassified_system_of_abstract_status:
81 abstract_status → preclassified_system
82≝ λS.
83   mk_preclassified_system
84    (mk_fullexec_of_abstract_status S) (λ_.λst. ¬(is_none … (as_label … st)))
85    (λ_.as_classify S)
86    (λ_.λst,prf. as_call_ident S «st,?»).
87 @hide_prf cases (as_classify ??) in prf; normalize // *
88qed.
89
90(*
91definition OC_transition_system: trans_system io_out io_in ≝
92 mk_trans_system ?? OC_global OC_status ?
93  execute_1_instruction.
94
95definition OC_global ≝ BitVectorTrie Byte 16 × costlabel_map.
96
97definition OC_status ≝ λgl:OC_global. Status (\fst gl).
98
99definition 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
108definition OC_transition_system: trans_system io_out io_in ≝
109 mk_trans_system ?? OC_global OC_status ?
110  execute_1_instruction.
111
112definition OC_fullexec: fullexec io_out io_in ≝
113 mk_fullexec ??
114  labelled_object_code*)
115 
116
117definition OC_preclassified_system ≝
118 λc:labelled_object_code.
119  mk_preclassified_system_of_abstract_status (ASM_abstract_status (\fst c) (\fst (\snd c))).
Note: See TracBrowser for help on using the repository browser.