1 | include "joint/semantics.ma". |
---|
2 | include "common/StructuredTraces.ma". |
---|
3 | |
---|
4 | record evaluation_params : Type[1] ≝ |
---|
5 | { globals: list ident |
---|
6 | ; sparams:> sem_params |
---|
7 | ; exit: cpointer |
---|
8 | ; ev_genv: genv sparams globals |
---|
9 | ; io_env : state sparams → ∀o:io_out.res (io_in o) |
---|
10 | }. |
---|
11 | |
---|
12 | record prog_params : Type[1] ≝ |
---|
13 | { prog_spars : sem_params |
---|
14 | ; prog : joint_program prog_spars |
---|
15 | ; prog_io : state prog_spars → ∀o.res (io_in o) |
---|
16 | }. |
---|
17 | |
---|
18 | definition make_global : prog_params → evaluation_params |
---|
19 | ≝ |
---|
20 | λpars. |
---|
21 | (* Invariant: a -1 block is unused in common/Globalenvs *) |
---|
22 | let b ≝ mk_block Code (-1) in |
---|
23 | let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in |
---|
24 | let p ≝ prog pars in |
---|
25 | mk_evaluation_params |
---|
26 | (prog_var_names … p) |
---|
27 | (prog_spars pars) |
---|
28 | «ptr, refl …» |
---|
29 | (mk_genv_gen ?? (globalenv_noinit ? p) ?) |
---|
30 | (prog_io pars). |
---|
31 | (* TODO or TOBEFOUND *) |
---|
32 | cases daemon |
---|
33 | qed. |
---|
34 | |
---|
35 | coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params |
---|
36 | ≝ make_global on _p : prog_params to evaluation_params. |
---|
37 | |
---|
38 | |
---|
39 | axiom ExternalMain : String. |
---|
40 | |
---|
41 | definition make_initial_state : |
---|
42 | ∀pars: prog_params.res (state_pc pars) ≝ |
---|
43 | λpars.let p ≝ prog pars in |
---|
44 | let sem_globals : evaluation_params ≝ pars in |
---|
45 | let ge ≝ ev_genv sem_globals in |
---|
46 | let m ≝ alloc_mem … p in |
---|
47 | let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in |
---|
48 | let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in |
---|
49 | let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in |
---|
50 | let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in |
---|
51 | let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in |
---|
52 | let main ≝ prog_main … p in |
---|
53 | let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in |
---|
54 | (* use exit sem_globals as ra and call_dest_for_main as dest *) |
---|
55 | ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ; |
---|
56 | let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in |
---|
57 | ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ; |
---|
58 | ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; |
---|
59 | match main_fd with |
---|
60 | [ Internal fn ⇒ |
---|
61 | do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars) |
---|
62 | | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) |
---|
63 | ]. |
---|
64 | [ % |
---|
65 | | cases ispb |
---|
66 | | cases spb |
---|
67 | ] normalize // |
---|
68 | qed. |
---|
69 | |
---|
70 | definition step_flow_classifier : |
---|
71 | ∀p : evaluation_params.∀F,flows. |
---|
72 | step_flow p F flows → status_class ≝ |
---|
73 | λp,F,flows,flow.match flow with |
---|
74 | [ Redirect _ _ ⇒ cl_jump |
---|
75 | | Init bl _ _ _ ⇒ |
---|
76 | match symbol_for_block … (ev_genv p) (mk_block Code bl) with |
---|
77 | [ Some f ⇒ cl_call |
---|
78 | | None ⇒ cl_other (* we don't care, as call will fail anyway *) |
---|
79 | ] |
---|
80 | | Proceed flows ⇒ |
---|
81 | match flows with |
---|
82 | [ Labels lbls ⇒ |
---|
83 | match lbls with |
---|
84 | [ nil ⇒ cl_other |
---|
85 | | _ ⇒ cl_jump |
---|
86 | ] |
---|
87 | | _ ⇒ cl_other |
---|
88 | ] |
---|
89 | ]. |
---|
90 | |
---|
91 | definition fin_step_flow_classifier : |
---|
92 | ∀p : evaluation_params.∀F,flows. |
---|
93 | fin_step_flow p F flows → status_class ≝ |
---|
94 | λp,F,flows,flow.match flow with |
---|
95 | [ FRedirect lbls _ ⇒ |
---|
96 | match lbls with |
---|
97 | [ nil ⇒ (* not really possible, we don't care *) cl_other |
---|
98 | | cons _ tl ⇒ |
---|
99 | match tl with |
---|
100 | [ nil ⇒ (* only one label *) cl_other |
---|
101 | | _ ⇒ (* fork *) cl_jump |
---|
102 | ] |
---|
103 | ] |
---|
104 | | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *) |
---|
105 | cl_other |
---|
106 | | _ ⇒ cl_return |
---|
107 | ]. |
---|
108 | |
---|
109 | definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?. |
---|
110 | *#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim |
---|
111 | [ #EQ destruct % #H % |
---|
112 | | * #NEQ % #ABS destruct elim (NEQ ?) % |
---|
113 | ] |
---|
114 | qed. |
---|
115 | |
---|
116 | let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ |
---|
117 | match c with |
---|
118 | [ Value x ⇒ OK … x |
---|
119 | | Interact o f ⇒ |
---|
120 | ! i ← env o ; |
---|
121 | io_evaluate O I X env (f i) |
---|
122 | | Wrong e ⇒ Error … e |
---|
123 | ]. |
---|
124 | |
---|
125 | definition cost_label_of_stmt : |
---|
126 | ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝ |
---|
127 | λp,s.match s with |
---|
128 | [ sequential s _ ⇒ |
---|
129 | match s with |
---|
130 | [ step_seq s ⇒ |
---|
131 | match s with |
---|
132 | [ COST_LABEL lbl ⇒ Some ? lbl |
---|
133 | | _ ⇒ None ? |
---|
134 | ] |
---|
135 | | _ ⇒ None ? |
---|
136 | ] |
---|
137 | | _ ⇒ None ? |
---|
138 | ]. |
---|
139 | |
---|
140 | definition joint_abstract_status : |
---|
141 | ∀p : evaluation_params. |
---|
142 | abstract_status ≝ |
---|
143 | λp. |
---|
144 | mk_abstract_status |
---|
145 | (* as_status ≝ *) (state_pc p) |
---|
146 | (* as_execute ≝ *) |
---|
147 | (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2) |
---|
148 | (* as_pc ≝ *) cpointerDeq |
---|
149 | (* as_pc_of ≝ *) (pc …) |
---|
150 | (* as_classify ≝ *) |
---|
151 | (λs. |
---|
152 | match ( |
---|
153 | ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ; |
---|
154 | match stmt with |
---|
155 | [ sequential stp nxt ⇒ |
---|
156 | ! 〈flow, s'〉 ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ; |
---|
157 | return step_flow_classifier … flow |
---|
158 | | final stp ⇒ |
---|
159 | ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ; |
---|
160 | return fin_step_flow_classifier … flow |
---|
161 | ]) with |
---|
162 | [ OK c ⇒ c |
---|
163 | | Error _ ⇒ cl_other |
---|
164 | ]) |
---|
165 | (* as_label_of_pc ≝ *) |
---|
166 | (λpc. |
---|
167 | match fetch_statement ? p … (ev_genv p) pc with |
---|
168 | [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) |
---|
169 | | _ ⇒ None ? |
---|
170 | ]) |
---|
171 | (* as_after_return ≝ *) |
---|
172 | (λs1,s2. |
---|
173 | (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *) |
---|
174 | ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧ |
---|
175 | succ_pc p p (pc … s1) nxt = return pc … s2) |
---|
176 | (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?) |
---|
177 | (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed. |
---|