[1999] | 1 | include "common/Globalenvs.ma". |
---|
[1173] | 2 | include "common/IO.ma". |
---|
[2286] | 3 | (* include "common/SmallstepExec.ma". *) |
---|
[1999] | 4 | include "joint/BEMem.ma". |
---|
[1173] | 5 | include "joint/Joint.ma". |
---|
[1415] | 6 | include "ASM/I8051bis.ma". |
---|
[2473] | 7 | include "common/extraGlobalenvs.ma". |
---|
[1213] | 8 | |
---|
[1173] | 9 | (* CSC: external functions never fail (??) and always return something of the |
---|
| 10 | size of one register, both in the frontend and in the backend. |
---|
| 11 | Is this reasonable??? In OCaml it always return a list, but in the frontend |
---|
| 12 | only the head is kept (or Undef if the list is empty) ??? *) |
---|
| 13 | |
---|
[2286] | 14 | (* Paolo: I'll put in this record the property about genv we need *) |
---|
| 15 | record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ |
---|
| 16 | { ge :> genv_t (fundef (F globals)) |
---|
[2473] | 17 | ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? |
---|
| 18 | ; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ |
---|
[2286] | 19 | }. |
---|
| 20 | |
---|
[2473] | 21 | definition stack_sizes_lift : |
---|
| 22 | ∀pars_in, pars_out : params. |
---|
| 23 | ∀trans : ∀globals.joint_closed_internal_function pars_in globals → |
---|
| 24 | joint_closed_internal_function pars_out globals. |
---|
| 25 | ∀prog_in : program (joint_function pars_in) ℕ. |
---|
| 26 | let prog_out ≝ |
---|
| 27 | transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in |
---|
| 28 | ((Σi.is_internal_function_of_program … prog_out i) → ℕ) → |
---|
| 29 | ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝ |
---|
| 30 | λpars_in,pars_out,prog_in,trans,stack_sizes. |
---|
| 31 | λi.stack_sizes «i, if_propagate … (pi2 … i)». |
---|
| 32 | |
---|
[2422] | 33 | definition genv ≝ λp.genv_gen (joint_closed_internal_function p). |
---|
[2286] | 34 | coercion genv_to_genv_t : |
---|
| 35 | ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝ |
---|
| 36 | λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?. |
---|
| 37 | |
---|
| 38 | record sem_state_params : Type[1] ≝ |
---|
[1233] | 39 | { framesT: Type[0] |
---|
[1408] | 40 | ; empty_framesT: framesT |
---|
[2286] | 41 | ; regsT : Type[0] |
---|
[2443] | 42 | ; empty_regsT: xpointer → regsT (* initial stack pointer *) |
---|
| 43 | ; load_sp : regsT → res xpointer |
---|
| 44 | ; save_sp : regsT → xpointer → regsT |
---|
[1173] | 45 | }. |
---|
| 46 | |
---|
[2443] | 47 | inductive internal_stack : Type[0] ≝ |
---|
| 48 | | empty_is : internal_stack |
---|
| 49 | | one_is : beval → internal_stack |
---|
| 50 | | both_is : beval → beval → internal_stack. |
---|
| 51 | |
---|
| 52 | axiom InternalStackFull : String. |
---|
| 53 | axiom InternalStackEmpty : String. |
---|
| 54 | |
---|
| 55 | definition is_push : internal_stack → beval → res internal_stack ≝ |
---|
| 56 | λis,bv.match is with |
---|
| 57 | [ empty_is ⇒ return one_is bv |
---|
| 58 | | one_is bv' ⇒ return both_is bv' bv |
---|
| 59 | | both_is _ _ ⇒ Error … [MSG … InternalStackFull] |
---|
| 60 | ]. |
---|
| 61 | |
---|
| 62 | definition is_pop : internal_stack → res (beval × internal_stack) ≝ |
---|
| 63 | λis.match is with |
---|
| 64 | [ empty_is ⇒ Error … [MSG … InternalStackEmpty] |
---|
| 65 | | one_is bv' ⇒ return 〈bv', empty_is〉 |
---|
| 66 | | both_is bv bv' ⇒ return 〈bv', one_is bv〉 |
---|
| 67 | ]. |
---|
| 68 | |
---|
[2286] | 69 | record state (semp: sem_state_params): Type[0] ≝ |
---|
| 70 | { st_frms: framesT semp |
---|
[2443] | 71 | ; istack : internal_stack |
---|
[2286] | 72 | ; carry: bebit |
---|
| 73 | ; regs: regsT semp |
---|
[1213] | 74 | ; m: bemem |
---|
[1173] | 75 | }. |
---|
| 76 | |
---|
[2443] | 77 | definition sp ≝ λp,st.load_sp p (regs ? st). |
---|
[1408] | 78 | |
---|
[2286] | 79 | record state_pc (semp : sem_state_params) : Type[0] ≝ |
---|
| 80 | { st_no_pc :> state semp |
---|
[2470] | 81 | ; pc : program_counter |
---|
[2286] | 82 | }. |
---|
[1176] | 83 | |
---|
[2286] | 84 | definition set_m: ∀p. bemem → state p → state p ≝ |
---|
[2443] | 85 | λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m. |
---|
[1289] | 86 | |
---|
[2286] | 87 | definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝ |
---|
[2443] | 88 | λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st). |
---|
[1384] | 89 | |
---|
[2286] | 90 | definition set_sp: ∀p. ? → state p → state p ≝ |
---|
[2443] | 91 | λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in |
---|
| 92 | mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st). |
---|
[1294] | 93 | |
---|
[2286] | 94 | definition set_carry: ∀p. bebit → state p → state p ≝ |
---|
[2443] | 95 | λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st). |
---|
[2286] | 96 | |
---|
[2443] | 97 | definition set_istack: ∀p. internal_stack → state p → state p ≝ |
---|
| 98 | λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st). |
---|
| 99 | |
---|
[2286] | 100 | definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ |
---|
| 101 | λp,pc,st. mk_state_pc … (st_no_pc … st) pc. |
---|
| 102 | |
---|
| 103 | definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝ |
---|
| 104 | λp,s,st. mk_state_pc … s (pc … st). |
---|
| 105 | |
---|
| 106 | definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ |
---|
[2443] | 107 | λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st). |
---|
[2286] | 108 | |
---|
| 109 | axiom BadProgramCounter : String. |
---|
| 110 | |
---|
[2457] | 111 | (* |
---|
[2286] | 112 | inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ |
---|
| 113 | | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *) |
---|
| 114 | | Init : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *) |
---|
| 115 | | Proceed : ∀flows.step_flow p F flows. (* go to implicit successor *) |
---|
| 116 | |
---|
| 117 | inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ |
---|
| 118 | | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls) |
---|
| 119 | | FTailInit : Z → F → call_args p → fin_step_flow p F Call |
---|
| 120 | | FEnd1 : fin_step_flow p F (Labels [ ]) (* end flow *) |
---|
| 121 | | FEnd2 : fin_step_flow p F Call. (* end flow *) |
---|
[2457] | 122 | *) |
---|
[2286] | 123 | |
---|
[2462] | 124 | (* bevals hold a function pointer (BVptr) *) |
---|
[2473] | 125 | definition funct_of_bevals : ∀F,ge. |
---|
| 126 | beval → beval → option (Σi.is_function F ge i) ≝ |
---|
| 127 | λF,ge,dpl,dph. |
---|
[2457] | 128 | ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; |
---|
[2462] | 129 | if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *) |
---|
[2473] | 130 | match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *) |
---|
[2457] | 131 | funct_of_block … (pblock ptr) |
---|
| 132 | else None ?. |
---|
| 133 | |
---|
| 134 | axiom ProgramCounterOutOfCode : String. |
---|
| 135 | axiom PointNotFound : String. |
---|
| 136 | axiom LabelNotFound : String. |
---|
| 137 | axiom MissingSymbol : String. |
---|
| 138 | axiom FailedLoad : String. |
---|
| 139 | axiom BadFunction : String. |
---|
| 140 | axiom SuccessorNotProvided : String. |
---|
| 141 | axiom BadPointer : String. |
---|
| 142 | |
---|
| 143 | (* this can replace graph_fetch function and lin_fetch_function *) |
---|
| 144 | definition fetch_function: |
---|
[2481] | 145 | ∀F. |
---|
| 146 | ∀ge : genv_t (fundef F). |
---|
[2470] | 147 | program_counter → |
---|
[2457] | 148 | res (Σi.is_internal_function … ge i) ≝ |
---|
[2481] | 149 | λpars,ge,p. |
---|
[2457] | 150 | opt_to_res … [MSG BadFunction; MSG BadPointer] |
---|
[2470] | 151 | (int_funct_of_block … ge (pc_block p)). |
---|
[2457] | 152 | |
---|
[2443] | 153 | record sem_unserialized_params |
---|
[2286] | 154 | (uns_pars : unserialized_params) |
---|
| 155 | (F : list ident → Type[0]) : Type[1] ≝ |
---|
[2443] | 156 | { st_pars :> sem_state_params |
---|
[2457] | 157 | |
---|
[2286] | 158 | ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
| 159 | ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval |
---|
| 160 | ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval |
---|
| 161 | ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
| 162 | ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval |
---|
| 163 | ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval |
---|
| 164 | ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
| 165 | ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval |
---|
| 166 | ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval |
---|
| 167 | ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) |
---|
| 168 | ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval |
---|
| 169 | ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval |
---|
| 170 | ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval |
---|
| 171 | ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) |
---|
| 172 | |
---|
[2484] | 173 | ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars |
---|
[2286] | 174 | (* Paolo: save_frame separated from call_setup to factorize tailcall code *) |
---|
[2484] | 175 | ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars) |
---|
[2286] | 176 | (*CSC: setup_call returns a res only because we can call a function with the wrong number and |
---|
[1386] | 177 | type of arguments. To be fixed using a dependent type *) |
---|
[2286] | 178 | ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → |
---|
| 179 | state st_pars → res (state st_pars) |
---|
[2457] | 180 | ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → |
---|
[2286] | 181 | res (list val) |
---|
| 182 | ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) |
---|
| 183 | ; call_args_for_main: call_args uns_pars |
---|
| 184 | ; call_dest_for_main: call_dest uns_pars |
---|
[1385] | 185 | |
---|
[2286] | 186 | (* from now on, parameters that use the type of functions *) |
---|
| 187 | ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) |
---|
[2457] | 188 | ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → |
---|
| 189 | (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars) |
---|
| 190 | ; pop_frame: ∀globals.∀ge : genv_gen F globals. |
---|
[2484] | 191 | (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state_pc st_pars) |
---|
[2286] | 192 | }. |
---|
[1186] | 193 | |
---|
[2484] | 194 | definition allocate_locals : |
---|
| 195 | ∀p,F.∀sup : sem_unserialized_params p F. |
---|
| 196 | list (localsT p) → state sup → state sup ≝ |
---|
| 197 | λp,F,sup,l,st. |
---|
| 198 | let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in |
---|
| 199 | set_regs … r st. |
---|
[1176] | 200 | |
---|
[2286] | 201 | definition helper_def_retrieve : |
---|
| 202 | ∀X : ? → ? → ? → Type[0]. |
---|
[2443] | 203 | (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) → |
---|
| 204 | ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝ |
---|
[2286] | 205 | λX,f,up,F,p,st.f ?? p (regs … st). |
---|
[1233] | 206 | |
---|
[2286] | 207 | definition helper_def_store : |
---|
| 208 | ∀X : ? → ? → ? → Type[0]. |
---|
[2443] | 209 | (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) → |
---|
| 210 | ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝ |
---|
[2286] | 211 | λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st. |
---|
[1386] | 212 | |
---|
[2286] | 213 | definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_. |
---|
| 214 | definition acca_store ≝ helper_def_store ? acca_store_. |
---|
| 215 | definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_. |
---|
| 216 | definition accb_store ≝ helper_def_store ? accb_store_. |
---|
| 217 | definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_. |
---|
| 218 | definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_. |
---|
| 219 | definition dpl_store ≝ helper_def_store ? dpl_store_. |
---|
| 220 | definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_. |
---|
| 221 | definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_. |
---|
| 222 | definition dph_store ≝ helper_def_store ? dph_store_. |
---|
| 223 | definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_. |
---|
| 224 | definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_. |
---|
| 225 | definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. |
---|
| 226 | definition pair_reg_move ≝ |
---|
[2443] | 227 | λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up. |
---|
[2286] | 228 | ! r ← pair_reg_move_ ?? p (regs ? st) pm; |
---|
| 229 | return set_regs ? r st. |
---|
| 230 | |
---|
| 231 | axiom FailedStore: String. |
---|
[1173] | 232 | |
---|
[2286] | 233 | definition push: ∀p.state p → beval → res (state p) ≝ |
---|
| 234 | λp,st,v. |
---|
[2443] | 235 | ! is ← is_push (istack … st) v ; |
---|
| 236 | return set_istack … is st. |
---|
[1430] | 237 | |
---|
[2443] | 238 | definition pop: ∀p. state p → res (beval × (state p)) ≝ |
---|
[2286] | 239 | λp,st. |
---|
[2443] | 240 | ! 〈bv, is〉 ← is_pop (istack … st) ; |
---|
| 241 | return 〈bv, set_istack … is st〉. |
---|
[1173] | 242 | |
---|
[2470] | 243 | definition save_ra : ∀p. state p → program_counter → res (state p) ≝ |
---|
[2286] | 244 | λp,st,l. |
---|
[2462] | 245 | let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in |
---|
[2286] | 246 | ! st' ← push … st addrl; |
---|
| 247 | push … st' addrh. |
---|
[1173] | 248 | |
---|
[2470] | 249 | definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝ |
---|
[2286] | 250 | λp,st. |
---|
[2462] | 251 | ! 〈addrh, st'〉 ← pop … st; |
---|
| 252 | ! 〈addrl, st''〉 ← pop … st'; |
---|
| 253 | ! pr ← pc_of_bevals [addrh; addrl]; |
---|
| 254 | return 〈pr, st''〉. |
---|
[1174] | 255 | |
---|
[2286] | 256 | (* parameters that are defined by serialization *) |
---|
| 257 | record more_sem_params (pp : params) : Type[1] ≝ |
---|
[2443] | 258 | { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp) |
---|
[2470] | 259 | ; offset_of_point : code_point pp → Pos |
---|
| 260 | ; point_of_offset : Pos → code_point pp |
---|
[2286] | 261 | ; point_of_offset_of_point : |
---|
[2470] | 262 | ∀pt.point_of_offset (offset_of_point pt) = pt |
---|
[2286] | 263 | ; offset_of_point_of_offset : |
---|
[2470] | 264 | ∀o.offset_of_point (point_of_offset o) = o |
---|
[2286] | 265 | }. |
---|
[1173] | 266 | |
---|
[2286] | 267 | (* |
---|
| 268 | coercion ms_pars_to_msu_pars nocomposites : |
---|
| 269 | ∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p) |
---|
| 270 | ≝ msu_pars |
---|
| 271 | on _msp : more_sem_params ? to more_sem_unserialized_params ??. |
---|
[1451] | 272 | |
---|
[2286] | 273 | definition ss_pars_of_ms_pars ≝ |
---|
| 274 | λp.λpp : more_sem_params p. |
---|
| 275 | st_pars … (msu_pars … pp). |
---|
| 276 | coercion ms_pars_to_ss_pars nocomposites : |
---|
| 277 | ∀p : params.∀msp : more_sem_params p.sem_state_params ≝ |
---|
| 278 | ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*) |
---|
[1451] | 279 | |
---|
[2470] | 280 | definition pc_of_point : ∀p.more_sem_params p → |
---|
| 281 | program_counter → code_point p → program_counter ≝ |
---|
[2286] | 282 | λp,msp,ptr,pt. |
---|
[2470] | 283 | mk_program_counter (pc_block ptr) (offset_of_point ? msp pt). |
---|
[1173] | 284 | |
---|
[2470] | 285 | definition point_of_pc : |
---|
| 286 | ∀p.more_sem_params p → program_counter → code_point p ≝ |
---|
| 287 | λp,msp,ptr.point_of_offset p msp (pc_offset ptr). |
---|
[1173] | 288 | |
---|
[2286] | 289 | lemma point_of_pointer_of_point : |
---|
[2470] | 290 | ∀p,msp.∀ptr,pt. |
---|
| 291 | point_of_pc ? msp (pc_of_point p msp ptr pt) = pt. |
---|
| 292 | #p #msp #ptr #pt normalize // qed. |
---|
[1173] | 293 | |
---|
[2286] | 294 | lemma pointer_of_point_block : |
---|
[2470] | 295 | ∀p,msp,ptr,pt. |
---|
| 296 | pc_block (pc_of_point p msp ptr pt) = pc_block ptr. |
---|
| 297 | #p #msp #ptr #pt % qed. (* can probably do without *) |
---|
[1173] | 298 | |
---|
[2286] | 299 | lemma pointer_of_point_uses_block : |
---|
[2470] | 300 | ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 → |
---|
| 301 | pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt. |
---|
| 302 | #p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed. |
---|
[1173] | 303 | |
---|
[2286] | 304 | lemma pointer_of_point_of_pointer : |
---|
[2470] | 305 | ∀p,msp.∀ptr1,ptr2. |
---|
| 306 | pc_block ptr1 = pc_block ptr2 → |
---|
| 307 | pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2. |
---|
| 308 | #p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed. |
---|
[1173] | 309 | |
---|
[2286] | 310 | definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. |
---|
[2481] | 311 | ∀ge : genv_t (joint_function p globals). program_counter → |
---|
[2457] | 312 | res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝ |
---|
[2286] | 313 | λp,msp,globals,ge,ptr. |
---|
[2470] | 314 | ! f ← fetch_function … ge ptr ; |
---|
[2457] | 315 | let fn ≝ if_of_function … f in |
---|
[2470] | 316 | let pt ≝ point_of_pc ? msp ptr in |
---|
[2286] | 317 | ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); |
---|
[2457] | 318 | return 〈f, stmt〉. |
---|
| 319 | |
---|
[2470] | 320 | definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. |
---|
[2481] | 321 | genv_t (joint_function p globals) → program_counter → label → res program_counter ≝ |
---|
[2286] | 322 | λp,msp,globals,ge,ptr,lbl. |
---|
[2457] | 323 | ! f ← fetch_function … ge ptr ; |
---|
| 324 | let fn ≝ if_of_function … ge f in |
---|
[2286] | 325 | ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] |
---|
| 326 | (point_of_label … (joint_if_code … fn) lbl) ; |
---|
[2470] | 327 | return pc_of_point p msp ptr pt. |
---|
[1173] | 328 | |
---|
[2286] | 329 | definition succ_pc : ∀p : params.∀ msp : more_sem_params p. |
---|
[2470] | 330 | program_counter → succ p → program_counter ≝ |
---|
[2286] | 331 | λp,msp,ptr,nxt. |
---|
[2470] | 332 | let curr ≝ point_of_pc p msp ptr in |
---|
| 333 | pc_of_point p msp ptr (point_of_succ p curr nxt). |
---|
[1173] | 334 | |
---|
[2286] | 335 | record sem_params : Type[1] ≝ |
---|
| 336 | { spp :> params |
---|
| 337 | ; more_sem_pars :> more_sem_params spp |
---|
| 338 | }. |
---|
[1173] | 339 | |
---|
[2286] | 340 | (* definition msu_pars_of_s_pars : |
---|
| 341 | ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) |
---|
| 342 | ≝ λp : sem_params. |
---|
| 343 | msu_pars … (more_sem_pars p). |
---|
| 344 | coercion s_pars_to_msu_pars nocomposites : |
---|
| 345 | ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝ |
---|
| 346 | msu_pars_of_s_pars |
---|
| 347 | on p : sem_params to more_sem_unserialized_params ??. |
---|
[1173] | 348 | |
---|
[2286] | 349 | definition ss_pars_of_s_pars : |
---|
| 350 | ∀p : sem_params.sem_state_params |
---|
| 351 | ≝ λp : sem_params. |
---|
| 352 | st_pars … (msu_pars … (more_sem_pars p)). |
---|
| 353 | coercion s_pars_to_ss_pars nocomposites : |
---|
| 354 | ∀p : sem_params.sem_state_params ≝ |
---|
| 355 | ss_pars_of_s_pars |
---|
| 356 | on _p : sem_params to sem_state_params. |
---|
[1173] | 357 | |
---|
[2286] | 358 | definition ms_pars_of_s_pars : |
---|
| 359 | ∀p : sem_params.more_sem_params (spp p) |
---|
| 360 | ≝ more_sem_pars. |
---|
| 361 | coercion s_pars_to_ms_pars nocomposites : |
---|
| 362 | ∀p : sem_params.more_sem_params (spp p) ≝ |
---|
| 363 | ms_pars_of_s_pars |
---|
| 364 | on p : sem_params to more_sem_params ?.*) |
---|
[1173] | 365 | |
---|
[2286] | 366 | (* definition address_of_label: ∀globals. ∀p:sem_params. |
---|
| 367 | genv globals p → pointer → label → res address ≝ |
---|
| 368 | λglobals,p,ge,ptr,l. |
---|
| 369 | do newptr ← pointer_of_label … p ? ge … ptr l ; |
---|
| 370 | OK … (address_of_code_pointer newptr). *) |
---|
[1173] | 371 | |
---|
[2481] | 372 | definition goto: ∀p : sem_params.∀globals. |
---|
| 373 | genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝ |
---|
| 374 | λp,globals,ge,l,st,b. |
---|
[2470] | 375 | ! newpc ← pc_of_label ? p … ge b l ; |
---|
[2286] | 376 | return mk_state_pc ? st newpc. |
---|
[1173] | 377 | |
---|
[2286] | 378 | (* |
---|
| 379 | definition empty_state: ∀p. more_sem_params p → state p ≝ |
---|
| 380 | mk_state … (empty_framesT …) |
---|
| 381 | *) |
---|
[1176] | 382 | |
---|
[2484] | 383 | definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝ |
---|
| 384 | λp,l,st. |
---|
| 385 | let newpc ≝ succ_pc ? p … (pc … st) l in |
---|
[2470] | 386 | mk_state_pc … st newpc. |
---|
[2286] | 387 | |
---|
[1173] | 388 | |
---|
[2457] | 389 | definition function_of_call ≝ λp:sem_params.λglobals. |
---|
[2481] | 390 | λge: genv_t (joint_function p globals).λst : state p.λf. |
---|
[2437] | 391 | match f with |
---|
| 392 | [ inl id ⇒ |
---|
[2457] | 393 | opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id) |
---|
[2437] | 394 | | inr addr ⇒ |
---|
| 395 | ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; |
---|
| 396 | ! addr_h ← dph_arg_retrieve … st (\snd addr) ; |
---|
[2457] | 397 | opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h) |
---|
[2437] | 398 | ]. |
---|
| 399 | |
---|
[2457] | 400 | (* Paolo: why external calls do not need args?? *) |
---|
| 401 | definition eval_external_call ≝ |
---|
| 402 | λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st. |
---|
| 403 | ! params ← fetch_external_args … p' fn st args : IO ???; |
---|
| 404 | ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; |
---|
| 405 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
| 406 | (* CSC: XXX bug here; I think I should split it into Byte-long |
---|
| 407 | components; instead I am making a singleton out of it. To be |
---|
| 408 | fixed once we fully implement external functions. *) |
---|
| 409 | let vs ≝ [mk_val ? evres] in |
---|
| 410 | set_result … p' vs dest st. |
---|
| 411 | |
---|
| 412 | definition eval_internal_call_pc ≝ |
---|
[2481] | 413 | λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi. |
---|
[2457] | 414 | let fn ≝ if_of_function … ge i in |
---|
| 415 | let l' ≝ joint_if_entry ?? fn in |
---|
[2473] | 416 | mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l'). |
---|
[2457] | 417 | [ @block_of_funct_ident_is_code |
---|
| 418 | | cases i /2 by internal_function_is_function/ |
---|
| 419 | ] |
---|
| 420 | qed. |
---|
| 421 | |
---|
| 422 | definition eval_internal_call_no_pc ≝ |
---|
| 423 | λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st. |
---|
| 424 | let fn ≝ if_of_function … ge i in |
---|
| 425 | let stack_size ≝ stack_sizes … ge i in |
---|
| 426 | ! st' ← setup_call … stack_size (joint_if_params … fn) args st ; |
---|
[2484] | 427 | return allocate_locals … p (joint_if_locals … fn) st. |
---|
[2457] | 428 | |
---|
[2286] | 429 | definition eval_seq_no_pc : |
---|
[2457] | 430 | ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) → |
---|
[2484] | 431 | state p → joint_seq p globals → |
---|
[2286] | 432 | IO io_out io_in (state p) ≝ |
---|
[2484] | 433 | λp,globals,ge,curr_fn,st,seq. |
---|
[2286] | 434 | match seq return λx.IO ??? with |
---|
| 435 | [ extension_seq c ⇒ |
---|
| 436 | eval_ext_seq … ge c curr_fn st |
---|
| 437 | | LOAD dst addrl addrh ⇒ |
---|
| 438 | ! vaddrh ← dph_arg_retrieve … st addrh ; |
---|
| 439 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
| 440 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
| 441 | ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); |
---|
| 442 | acca_store p … dst v st |
---|
| 443 | | STORE addrl addrh src ⇒ |
---|
| 444 | ! vaddrh ← dph_arg_retrieve … st addrh; |
---|
| 445 | ! vaddrl ← dpl_arg_retrieve … st addrl; |
---|
| 446 | ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉; |
---|
| 447 | ! v ← acca_arg_retrieve … st src; |
---|
| 448 | ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); |
---|
| 449 | return set_m … m' st |
---|
| 450 | | ADDRESS id prf ldest hdest ⇒ |
---|
[2443] | 451 | let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in |
---|
| 452 | let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in |
---|
[2286] | 453 | ! st' ← dpl_store … ldest laddr st; |
---|
| 454 | dph_store … hdest haddr st' |
---|
| 455 | | OP1 op dacc_a sacc_a ⇒ |
---|
| 456 | ! v ← acca_retrieve … st sacc_a; |
---|
| 457 | ! v' ← be_op1 op v ; |
---|
| 458 | acca_store … dacc_a v' st |
---|
| 459 | | OP2 op dacc_a sacc_a src ⇒ |
---|
| 460 | ! v1 ← acca_arg_retrieve … st sacc_a; |
---|
| 461 | ! v2 ← snd_arg_retrieve … st src; |
---|
| 462 | ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ; |
---|
| 463 | ! st' ← acca_store … dacc_a v' st; |
---|
[2457] | 464 | return set_carry … carry st' |
---|
[2286] | 465 | | CLEAR_CARRY ⇒ |
---|
| 466 | return set_carry … (BBbit false) st |
---|
| 467 | | SET_CARRY ⇒ |
---|
| 468 | return set_carry … (BBbit true) st |
---|
| 469 | | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ |
---|
| 470 | ! v1 ← acca_arg_retrieve … st sacc_a_reg; |
---|
| 471 | ! v2 ← accb_arg_retrieve … st sacc_b_reg; |
---|
| 472 | ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ; |
---|
| 473 | ! st' ← acca_store … dacc_a_reg v1' st; |
---|
| 474 | accb_store … dacc_b_reg v2' st' |
---|
| 475 | | POP dst ⇒ |
---|
[2443] | 476 | ! 〈v, st'〉 ← pop p st; |
---|
[2286] | 477 | acca_store … p dst v st' |
---|
| 478 | | PUSH src ⇒ |
---|
| 479 | ! v ← acca_arg_retrieve … st src; |
---|
| 480 | push … st v |
---|
| 481 | | MOVE dst_src ⇒ |
---|
| 482 | pair_reg_move … st dst_src |
---|
[2437] | 483 | | CALL f args dest ⇒ |
---|
[2457] | 484 | ! fn ← function_of_call … ge st f : IO ???; |
---|
| 485 | match description_of_function … fn return λx.description_of_function … fn = x → ? with |
---|
| 486 | [ Internal fd ⇒ λprf. |
---|
[2484] | 487 | eval_internal_call_no_pc … ge «fn, ?» args st (* only pc changes *) |
---|
[2457] | 488 | | External fd ⇒ λ_.eval_external_call … fd args dest st |
---|
| 489 | ] (refl …) |
---|
[2286] | 490 | | _ ⇒ return st |
---|
| 491 | ]. |
---|
[2473] | 492 | [ @hide_prf |
---|
| 493 | @find_symbol_in_globals |
---|
[2286] | 494 | lapply prf |
---|
| 495 | elim globals [*] |
---|
[2491] | 496 | #hd #tl #IH #H elim (orb_Prop_true … H) -H |
---|
| 497 | [@eq_identifier_elim #H * >H %1 % ] |
---|
[2286] | 498 | #G %2 @IH @G |
---|
[2457] | 499 | | @(description_of_internal_function … prf) |
---|
| 500 | ] |
---|
| 501 | qed. |
---|
[1408] | 502 | |
---|
[2457] | 503 | definition eval_seq_pc : |
---|
| 504 | ∀p:sem_params.∀globals.∀ge:genv p globals. |
---|
[2484] | 505 | state_pc p → ? → joint_seq p globals → |
---|
| 506 | res (state_pc p) ≝ |
---|
| 507 | λp,globals,ge,st,nxt,s. |
---|
[2457] | 508 | match s with |
---|
[2437] | 509 | [ CALL f args dest ⇒ |
---|
[2457] | 510 | ! fn ← function_of_call … ge st f; |
---|
| 511 | match ? return λx.description_of_function … fn = x → ? with |
---|
[2484] | 512 | [ Internal _ ⇒ λprf. |
---|
| 513 | let pc ≝ eval_internal_call_pc … ge «fn, ?» in |
---|
| 514 | ! st' ← save_frame … dest st ; |
---|
| 515 | return mk_state_pc … st' pc |
---|
| 516 | | External _ ⇒ λ_.return next p nxt st |
---|
[2457] | 517 | ] (refl …) |
---|
[2484] | 518 | | _ ⇒ return next p nxt st |
---|
[2286] | 519 | ]. |
---|
[2457] | 520 | @(description_of_internal_function … prf) |
---|
| 521 | qed. |
---|
[1999] | 522 | |
---|
[2457] | 523 | definition eval_statement : |
---|
| 524 | ∀p:sem_params.∀globals.∀ge:genv p globals. |
---|
| 525 | (Σi.is_internal_function … ge i) → state_pc p → |
---|
| 526 | ∀s:joint_statement p globals. |
---|
| 527 | IO io_out io_in (state_pc p) ≝ |
---|
[2286] | 528 | λp,g,ge,curr_fn,st,s. |
---|
[2457] | 529 | match s with |
---|
| 530 | [ sequential s next ⇒ |
---|
| 531 | match s return λ_.IO ??? with |
---|
| 532 | [ step_seq s ⇒ |
---|
[2484] | 533 | ! st' ← eval_seq_no_pc … ge curr_fn st s ; |
---|
| 534 | let st'' ≝ mk_state_pc … st' (pc … st) in |
---|
| 535 | eval_seq_pc ?? ge st'' next s |
---|
[2457] | 536 | | COND a l ⇒ |
---|
| 537 | ! v ← acca_retrieve … st a ; |
---|
| 538 | ! b ← bool_of_beval … v ; |
---|
| 539 | ! pc' ← |
---|
| 540 | if b then |
---|
[2470] | 541 | pc_of_label ? p … ge (pc … st) l |
---|
[2457] | 542 | else |
---|
[2470] | 543 | return succ_pc ? p (pc … st) next ; |
---|
[2457] | 544 | return mk_state_pc … st pc' |
---|
| 545 | ] |
---|
| 546 | | final s ⇒ |
---|
| 547 | match s with |
---|
| 548 | [ GOTO l ⇒ |
---|
[2470] | 549 | ! pc' ← pc_of_label ? p ? ge (pc … st) l ; |
---|
[2457] | 550 | return mk_state_pc … st pc' |
---|
[2484] | 551 | | RETURN ⇒ pop_frame … curr_fn st |
---|
[2457] | 552 | | TAILCALL _ f args ⇒ |
---|
| 553 | ! fn ← function_of_call … ge st f : IO ???; |
---|
| 554 | match ? return λx.description_of_function … fn = x → ? with |
---|
| 555 | [ Internal _ ⇒ λprf. |
---|
[2470] | 556 | let pc' ≝ eval_internal_call_pc … ge «fn, ?» in |
---|
[2457] | 557 | return mk_state_pc … st pc' |
---|
| 558 | | External fd ⇒ λ_. |
---|
| 559 | let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in |
---|
| 560 | ! st' ← eval_external_call ??? fd args curr_dest st ; |
---|
[2484] | 561 | pop_frame … curr_fn st' |
---|
[2457] | 562 | ] (refl …) |
---|
| 563 | ] |
---|
[2286] | 564 | ]. |
---|
[2457] | 565 | @(description_of_internal_function … prf) |
---|
| 566 | qed. |
---|
[2286] | 567 | |
---|
[2481] | 568 | definition eval_state : ∀p:sem_params. ∀globals: list ident. |
---|
| 569 | genv p globals → |
---|
[2286] | 570 | state_pc p → IO io_out io_in (state_pc p) ≝ |
---|
[2481] | 571 | λp,globals,ge,st. |
---|
[2286] | 572 | ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???; |
---|
[2457] | 573 | eval_statement … ge fn st s. |
---|
[2286] | 574 | |
---|
| 575 | (* Paolo: what if in an intermediate language main finishes with an external |
---|
| 576 | tailcall? Maybe it should rely on an FEnd flow command issued, but that's |
---|
| 577 | not static... *) |
---|
[2481] | 578 | definition is_final: ∀p: sem_params.∀globals. |
---|
[2470] | 579 | genv p globals → program_counter → state_pc p → option int ≝ |
---|
[2481] | 580 | λp,globals,ge,exit,st.res_to_opt ? ( |
---|
[2457] | 581 | do 〈f,s〉 ← fetch_statement ? p … ge (pc … st); |
---|
| 582 | let fn ≝ if_of_function … f in |
---|
[1214] | 583 | match s with |
---|
[2286] | 584 | [ final s' ⇒ |
---|
| 585 | match s' with |
---|
| 586 | [ RETURN ⇒ |
---|
[2484] | 587 | do st' ← pop_frame … ge f st; |
---|
| 588 | if eq_program_counter (pc … st') exit then |
---|
[2286] | 589 | do vals ← read_result … ge (joint_if_result … fn) st' ; |
---|
[1359] | 590 | Word_of_list_beval vals |
---|
[1214] | 591 | else |
---|
[2286] | 592 | Error ? [ ] |
---|
| 593 | | _ ⇒ Error ? [ ] |
---|
| 594 | ] |
---|
| 595 | | _ ⇒ Error ? [ ] |
---|
| 596 | ]). |
---|
[1173] | 597 | |
---|
[2286] | 598 | (* |
---|
[1233] | 599 | record evaluation_parameters : Type[1] ≝ |
---|
| 600 | { globals: list ident |
---|
[2286] | 601 | ; sparams:> sem_params |
---|
[2470] | 602 | ; exit: program_counter |
---|
[2286] | 603 | ; genv2: genv globals sparams |
---|
[1233] | 604 | }. |
---|
[1173] | 605 | |
---|
[2286] | 606 | (* Paolo: with structured traces, eval need not emit labels. However, this |
---|
| 607 | changes trans_system. For now, just putting a dummy thing for |
---|
| 608 | the transition. *) |
---|
[1233] | 609 | definition joint_exec: trans_system io_out io_in ≝ |
---|
[2286] | 610 | mk_trans_system … evaluation_parameters (λG. state_pc G) |
---|
| 611 | (λG.is_final (globals G) G (genv2 G) (exit G)) |
---|
| 612 | (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉). |
---|
[1233] | 613 | |
---|
| 614 | definition make_global : |
---|
[2286] | 615 | ∀pars: sem_params. |
---|
[1233] | 616 | joint_program pars → evaluation_parameters |
---|
| 617 | ≝ |
---|
[2286] | 618 | λpars. |
---|
[1395] | 619 | (* Invariant: a -1 block is unused in common/Globalenvs *) |
---|
| 620 | let b ≝ mk_block Code (-1) in |
---|
[2286] | 621 | let ptr ≝ mk_pointer Code b ? (mk_offset 0) in |
---|
| 622 | (λp. mk_evaluation_parameters |
---|
| 623 | (prog_var_names … p) |
---|
| 624 | (mk_sem_params … pars) |
---|
| 625 | ptr |
---|
| 626 | (globalenv_noinit … p) |
---|
| 627 | ). |
---|
[1395] | 628 | % qed. |
---|
[1233] | 629 | |
---|
[1408] | 630 | axiom ExternalMain: String. |
---|
[2286] | 631 | |
---|
[1220] | 632 | definition make_initial_state : |
---|
[2286] | 633 | ∀pars: sem_params. |
---|
| 634 | ∀p: joint_program … pars. res (state_pc pars) ≝ |
---|
| 635 | λpars,p. |
---|
| 636 | let sem_globals ≝ make_global pars p in |
---|
[1408] | 637 | let ge ≝ genv2 sem_globals in |
---|
[1999] | 638 | let m ≝ alloc_mem … p in |
---|
[1415] | 639 | let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in |
---|
[1430] | 640 | let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in |
---|
[2286] | 641 | let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in |
---|
| 642 | let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in |
---|
| 643 | let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in |
---|
[1220] | 644 | let main ≝ prog_main … p in |
---|
[2286] | 645 | let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in |
---|
| 646 | (* use exit sem_globals as ra and call_dest_for_main as dest *) |
---|
| 647 | let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in |
---|
| 648 | let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in |
---|
| 649 | ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ; |
---|
| 650 | ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; |
---|
| 651 | match main_fd with |
---|
| 652 | [ Internal fn ⇒ |
---|
| 653 | do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars) |
---|
| 654 | | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) |
---|
| 655 | ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try // |
---|
| 656 | qed. |
---|
[1233] | 657 | |
---|
[1186] | 658 | definition joint_fullexec : |
---|
[2286] | 659 | ∀pars:sem_params.fullexec io_out io_in ≝ |
---|
| 660 | λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars). |
---|
| 661 | *) |
---|