| 1 | include "utilities/lists.ma". |
|---|
| 2 | include "common/Globalenvs.ma". |
|---|
| 3 | include "common/IO.ma". |
|---|
| 4 | include "common/SmallstepExec.ma". |
|---|
| 5 | include "joint/Joint.ma". |
|---|
| 6 | include "joint/BEMem.ma". |
|---|
| 7 | |
|---|
| 8 | (* CSC: external functions never fail (??) and always return something of the |
|---|
| 9 | size of one register, both in the frontend and in the backend. |
|---|
| 10 | Is this reasonable??? In OCaml it always return a list, but in the frontend |
|---|
| 11 | only the head is kept (or Undef if the list is empty) ??? *) |
|---|
| 12 | |
|---|
| 13 | definition address ≝ beval × beval. (* CSC: only pointers to XRAM or code memory *) |
|---|
| 14 | |
|---|
| 15 | definition eq_address: address → address → bool ≝ |
|---|
| 16 | λaddr1,addr2. |
|---|
| 17 | eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2). |
|---|
| 18 | |
|---|
| 19 | record more_sem_params (p:params_): Type[1] ≝ |
|---|
| 20 | { framesT: Type[0] |
|---|
| 21 | ; regsT: Type[0] |
|---|
| 22 | |
|---|
| 23 | ; succ_pc: succ p → address → address |
|---|
| 24 | ; pop_frame_: framesT → res framesT |
|---|
| 25 | ; save_frame_: framesT → regsT → framesT |
|---|
| 26 | ; greg_store_: generic_reg p → beval → regsT → res regsT |
|---|
| 27 | ; greg_retrieve_: regsT → generic_reg p → res beval |
|---|
| 28 | ; acca_store_: acc_a_reg p → beval → regsT → res regsT |
|---|
| 29 | ; acca_retrieve_: regsT → acc_a_reg p → res beval |
|---|
| 30 | ; accb_store_: acc_b_reg p → beval → regsT → res regsT |
|---|
| 31 | ; accb_retrieve_: regsT → acc_b_reg p → res beval |
|---|
| 32 | ; dpl_store_: dpl_reg p → beval → regsT → res regsT |
|---|
| 33 | ; dpl_retrieve_: regsT → dpl_reg p → res beval |
|---|
| 34 | ; dph_store_: dph_reg p → beval → regsT → res regsT |
|---|
| 35 | ; dph_retrieve_: regsT → dph_reg p → res beval |
|---|
| 36 | ; pair_reg_move_: regsT → pair_reg p → regsT |
|---|
| 37 | |
|---|
| 38 | ; pointer_of_label: label → Σp:pointer. ptype p = Code |
|---|
| 39 | }. |
|---|
| 40 | |
|---|
| 41 | record sem_params: Type[1] ≝ |
|---|
| 42 | { spp :> params_ |
|---|
| 43 | ; more_sem_pars :> more_sem_params spp |
|---|
| 44 | }. |
|---|
| 45 | |
|---|
| 46 | record state (p: sem_params): Type[0] ≝ |
|---|
| 47 | { st_frms: framesT ? p |
|---|
| 48 | ; pc: address |
|---|
| 49 | ; sp: pointer |
|---|
| 50 | ; carry: beval |
|---|
| 51 | ; regs: regsT ? p |
|---|
| 52 | ; m: bemem |
|---|
| 53 | }. |
|---|
| 54 | |
|---|
| 55 | definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p). |
|---|
| 56 | |
|---|
| 57 | record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝ |
|---|
| 58 | { more_sparams:> more_sem_params p |
|---|
| 59 | |
|---|
| 60 | ; init_locals : localsT p → regsT … more_sparams |
|---|
| 61 | |
|---|
| 62 | ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals) |
|---|
| 63 | ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val) |
|---|
| 64 | ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams)) |
|---|
| 65 | ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val |
|---|
| 66 | |
|---|
| 67 | ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams))) |
|---|
| 68 | }. |
|---|
| 69 | |
|---|
| 70 | record sem_params2 (globals: list ident): Type[1] ≝ |
|---|
| 71 | { p2:> params globals |
|---|
| 72 | ; more_sparams2:> more_sem_params2 globals p2 |
|---|
| 73 | }. |
|---|
| 74 | |
|---|
| 75 | definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2. |
|---|
| 76 | coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params |
|---|
| 77 | ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params. |
|---|
| 78 | (* |
|---|
| 79 | unification hint 0 ≔ globals: (list ident), p: sem_params2 globals; |
|---|
| 80 | S ≟ sem_params_of_sem_params2 globals p |
|---|
| 81 | (* ---------------------------------------- *) ⊢ |
|---|
| 82 | pars_ (spp (mk_sem_params (p2 globals p) |
|---|
| 83 | (more_sparams (p2 globals p) globals |
|---|
| 84 | (more_sparams2 globals p)))) ≡ spp__o__pars_ S. |
|---|
| 85 | *) |
|---|
| 86 | definition address_of_label: sem_params → label → address. |
|---|
| 87 | #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l))) |
|---|
| 88 | cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?) |
|---|
| 89 | [ #res #_ @res |
|---|
| 90 | | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ] |
|---|
| 91 | qed. |
|---|
| 92 | |
|---|
| 93 | definition set_m: ∀p. bemem → state p → state p ≝ |
|---|
| 94 | λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m. |
|---|
| 95 | |
|---|
| 96 | definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝ |
|---|
| 97 | λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st). |
|---|
| 98 | |
|---|
| 99 | definition set_sp: ∀p. pointer → state p → state p ≝ |
|---|
| 100 | λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st). |
|---|
| 101 | |
|---|
| 102 | definition set_carry: ∀p. beval → state p → state p ≝ |
|---|
| 103 | λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st). |
|---|
| 104 | |
|---|
| 105 | definition set_pc: ∀p. address → state p → state p ≝ |
|---|
| 106 | λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st). |
|---|
| 107 | |
|---|
| 108 | definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝ |
|---|
| 109 | λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st). |
|---|
| 110 | |
|---|
| 111 | definition goto: ∀p:sem_params. label → state p → state p ≝ |
|---|
| 112 | λp,l,st. set_pc … (address_of_label p l) st. |
|---|
| 113 | |
|---|
| 114 | definition next: ∀p:sem_params. succ … p → state p → state p ≝ |
|---|
| 115 | λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st. |
|---|
| 116 | |
|---|
| 117 | definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝ |
|---|
| 118 | λp,dst,v,st. |
|---|
| 119 | do regs ← greg_store_ … dst v (regs … st); |
|---|
| 120 | OK ? (set_regs … regs st). |
|---|
| 121 | |
|---|
| 122 | definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝ |
|---|
| 123 | λp,st,dst.greg_retrieve_ … (regs … st) dst. |
|---|
| 124 | |
|---|
| 125 | definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝ |
|---|
| 126 | λp,dst,v,st. |
|---|
| 127 | do regs ← acca_store_ … dst v (regs … st); |
|---|
| 128 | OK ? (set_regs … regs st). |
|---|
| 129 | |
|---|
| 130 | definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝ |
|---|
| 131 | λp,st,dst.acca_retrieve_ … (regs … st) dst. |
|---|
| 132 | |
|---|
| 133 | definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝ |
|---|
| 134 | λp,dst,v,st. |
|---|
| 135 | do regs ← accb_store_ … dst v (regs … st); |
|---|
| 136 | OK ? (set_regs … regs st). |
|---|
| 137 | |
|---|
| 138 | definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝ |
|---|
| 139 | λp,st,dst.accb_retrieve_ … (regs … st) dst. |
|---|
| 140 | |
|---|
| 141 | definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝ |
|---|
| 142 | λp,dst,v,st. |
|---|
| 143 | do regs ← dpl_store_ … dst v (regs … st); |
|---|
| 144 | OK ? (set_regs … regs st). |
|---|
| 145 | |
|---|
| 146 | definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝ |
|---|
| 147 | λp,st,dst.dpl_retrieve_ … (regs … st) dst. |
|---|
| 148 | |
|---|
| 149 | definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝ |
|---|
| 150 | λp,dst,v,st. |
|---|
| 151 | do regs ← dph_store_ … dst v (regs … st); |
|---|
| 152 | OK ? (set_regs … regs st). |
|---|
| 153 | |
|---|
| 154 | definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝ |
|---|
| 155 | λp,st,dst.dph_retrieve_ … (regs … st) dst. |
|---|
| 156 | |
|---|
| 157 | definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝ |
|---|
| 158 | λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st. |
|---|
| 159 | |
|---|
| 160 | definition save_frame: ∀p:sem_params. state p → state p ≝ |
|---|
| 161 | λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st. |
|---|
| 162 | |
|---|
| 163 | (* removes the top frame from the frames list *) |
|---|
| 164 | definition pop_frame: ∀p. state p → res (state p) ≝ |
|---|
| 165 | λp,st. |
|---|
| 166 | do frames ← pop_frame_ … p (st_frms … st); |
|---|
| 167 | OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)). |
|---|
| 168 | |
|---|
| 169 | axiom FailedStore: String. |
|---|
| 170 | |
|---|
| 171 | definition push: ∀p. state p → beval → res (state p) ≝ |
|---|
| 172 | λp,st,v. |
|---|
| 173 | let sp ≝ sp … st in |
|---|
| 174 | do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v); |
|---|
| 175 | let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in |
|---|
| 176 | OK … (set_m … m (set_sp … sp st)). |
|---|
| 177 | |
|---|
| 178 | definition pop: ∀p. state p → res (state p × beval) ≝ |
|---|
| 179 | λp,st. |
|---|
| 180 | let sp ≝ sp ? st in |
|---|
| 181 | let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in |
|---|
| 182 | let st ≝ set_sp … sp st in |
|---|
| 183 | do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp); |
|---|
| 184 | OK ? 〈st,v〉. |
|---|
| 185 | |
|---|
| 186 | definition save_ra : ∀p. state p → succ p → res (state p) ≝ |
|---|
| 187 | λp,st,l. |
|---|
| 188 | let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in |
|---|
| 189 | do st ← push … st addrl; |
|---|
| 190 | push … st addrh. |
|---|
| 191 | |
|---|
| 192 | definition fetch_ra : ∀p.state p → res (state p × address) ≝ |
|---|
| 193 | λp,st. |
|---|
| 194 | do 〈st,addrh〉 ← pop … st; |
|---|
| 195 | do 〈st,addrl〉 ← pop … st; |
|---|
| 196 | OK ? 〈st, 〈addrl,addrh〉〉. |
|---|
| 197 | |
|---|
| 198 | axiom MissingSymbol : String. |
|---|
| 199 | axiom FailedLoad : String. |
|---|
| 200 | axiom BadFunction : String. |
|---|
| 201 | |
|---|
| 202 | definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝ |
|---|
| 203 | λglobals,p,ge,st. |
|---|
| 204 | ! s ← fetch_statement … st; |
|---|
| 205 | match s with |
|---|
| 206 | [ GOTO l ⇒ ret ? 〈E0, goto … l st〉 |
|---|
| 207 | | sequential seq l ⇒ |
|---|
| 208 | match seq with |
|---|
| 209 | [ extension c ⇒ exec_extended … p ge c st |
|---|
| 210 | | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉 |
|---|
| 211 | | COMMENT c ⇒ ret ? 〈E0, next … l st〉 |
|---|
| 212 | | INT dest v ⇒ |
|---|
| 213 | ! st ← greg_store p dest (BVByte v) st; |
|---|
| 214 | ret ? 〈E0, next … l st〉 |
|---|
| 215 | | LOAD dst addrl addrh ⇒ |
|---|
| 216 | ! vaddrh ← dph_retrieve … st addrh; |
|---|
| 217 | ! vaddrl ← dpl_retrieve … st addrl; |
|---|
| 218 | ! vaddr ← pointer_of_bevals [vaddrl;vaddrh]; |
|---|
| 219 | ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); |
|---|
| 220 | ! st ← acca_store p … dst v st; |
|---|
| 221 | ret ? 〈E0, next … l st〉 |
|---|
| 222 | | STORE addrl addrh src ⇒ |
|---|
| 223 | ! vaddrh ← dph_retrieve … st addrh; |
|---|
| 224 | ! vaddrl ← dpl_retrieve … st addrl; |
|---|
| 225 | ! vaddr ← pointer_of_bevals [vaddrl;vaddrh]; |
|---|
| 226 | ! v ← acca_retrieve … st src; |
|---|
| 227 | ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v); |
|---|
| 228 | ret ? 〈E0, next … l (set_m … m' st)〉 |
|---|
| 229 | | COND src ltrue ⇒ |
|---|
| 230 | ! v ← acca_retrieve … st src; |
|---|
| 231 | ! b ← bool_of_beval v; |
|---|
| 232 | ret ? 〈E0, (if b then goto … ltrue else next … l) st〉 |
|---|
| 233 | | ADDRESS ident prf ldest hdest ⇒ |
|---|
| 234 | ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident); |
|---|
| 235 | ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer (block_region addr) addr ? zero_offset); |
|---|
| 236 | ! st ← dpl_store p ldest laddr st; |
|---|
| 237 | ! st ← dph_store p hdest haddr st; |
|---|
| 238 | ret ? 〈E0, next … l st〉 |
|---|
| 239 | | OP1 op dacc_a sacc_a ⇒ |
|---|
| 240 | ! v ← acca_retrieve … st sacc_a; |
|---|
| 241 | ! v ← Byte_of_val v; |
|---|
| 242 | let v' ≝ BVByte (op1 eval op v) in |
|---|
| 243 | ! st ← acca_store p dacc_a v' st; |
|---|
| 244 | ret ? 〈E0, next … l st〉 |
|---|
| 245 | | OP2 op dacc_a sacc_a src ⇒ |
|---|
| 246 | ! v1 ← acca_retrieve … st sacc_a; |
|---|
| 247 | ! v1 ← Byte_of_val v1; |
|---|
| 248 | ! v2 ← greg_retrieve … st src; |
|---|
| 249 | ! v2 ← Byte_of_val v2; |
|---|
| 250 | ! carry ← bool_of_beval (carry … st); |
|---|
| 251 | let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in |
|---|
| 252 | let v' ≝ BVByte v' in |
|---|
| 253 | let carry ≝ beval_of_bool carry in |
|---|
| 254 | ! st ← acca_store p dacc_a v' st; |
|---|
| 255 | ret ? 〈E0, next … l (set_carry … carry st)〉 |
|---|
| 256 | | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉 |
|---|
| 257 | | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉 |
|---|
| 258 | | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ |
|---|
| 259 | ! v1 ← acca_retrieve … st sacc_a_reg; |
|---|
| 260 | ! v1 ← Byte_of_val v1; |
|---|
| 261 | ! v2 ← accb_retrieve … st sacc_b_reg; |
|---|
| 262 | ! v2 ← Byte_of_val v2; |
|---|
| 263 | let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in |
|---|
| 264 | let v1' ≝ BVByte v1' in |
|---|
| 265 | let v2' ≝ BVByte v2' in |
|---|
| 266 | ! st ← acca_store p dacc_a_reg v1' st; |
|---|
| 267 | ! st ← accb_store p dacc_b_reg v2' st; |
|---|
| 268 | ret ? 〈E0, next … l st〉 |
|---|
| 269 | | POP dst ⇒ |
|---|
| 270 | ! 〈st,v〉 ← pop … st; |
|---|
| 271 | ! st ← acca_store p dst v st; |
|---|
| 272 | ret ? 〈E0, next … l st〉 |
|---|
| 273 | | PUSH src ⇒ |
|---|
| 274 | ! v ← acca_retrieve … st src; |
|---|
| 275 | ! st ← push … st v; |
|---|
| 276 | ret ? 〈E0, next … l st〉 |
|---|
| 277 | | MOVE dst_src ⇒ |
|---|
| 278 | ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉 |
|---|
| 279 | (*CSC: XXX bug here dest unused *) |
|---|
| 280 | | CALL_ID id argsno dest ⇒ |
|---|
| 281 | ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); |
|---|
| 282 | ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); |
|---|
| 283 | match fd with |
|---|
| 284 | [ Internal fn ⇒ |
|---|
| 285 | ! st ← save_ra … st l; |
|---|
| 286 | let st ≝ save_frame … st in |
|---|
| 287 | let regs ≝ init_locals … (joint_if_locals … fn) in |
|---|
| 288 | let l' ≝ joint_if_entry … fn in |
|---|
| 289 | ret ? 〈 E0, goto … l' (set_regs p regs st)〉 |
|---|
| 290 | | External fn ⇒ |
|---|
| 291 | ! params ← fetch_external_args … fn st; |
|---|
| 292 | ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); |
|---|
| 293 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
|---|
| 294 | (* CSC: XXX bug here; I think I should split it into Byte-long |
|---|
| 295 | components; instead I am making a singleton out of it *) |
|---|
| 296 | let vs ≝ [mk_val ? evres] in |
|---|
| 297 | ! st ← set_result … vs st; |
|---|
| 298 | ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉 |
|---|
| 299 | ]] |
|---|
| 300 | | RETURN ⇒ |
|---|
| 301 | ! st ← pop_frame … st; |
|---|
| 302 | ! 〈st,pch〉 ← pop … st; |
|---|
| 303 | ! 〈st,pcl〉 ← pop … st; |
|---|
| 304 | ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉]. |
|---|
| 305 | cases addr // |
|---|
| 306 | qed. |
|---|
| 307 | |
|---|
| 308 | definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝ |
|---|
| 309 | λglobals,p,exit,registersno,st. res_to_opt … ( |
|---|
| 310 | do s ← fetch_statement … st; |
|---|
| 311 | match s with |
|---|
| 312 | [ RETURN ⇒ |
|---|
| 313 | do 〈st,l〉 ← fetch_ra … st; |
|---|
| 314 | if eq_address l exit then |
|---|
| 315 | do val ← fetch_result … st registersno; |
|---|
| 316 | match val with |
|---|
| 317 | [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? []) |
|---|
| 318 | | _ ⇒ Error ? []] |
|---|
| 319 | else |
|---|
| 320 | Error ? [] |
|---|
| 321 | | _ ⇒ Error ? []]). |
|---|
| 322 | |
|---|
| 323 | record evaluation_parameters : Type[1] ≝ |
|---|
| 324 | { globals: list ident |
|---|
| 325 | ; sparams2: sem_params2 globals |
|---|
| 326 | ; exit: address |
|---|
| 327 | ; registersno: nat |
|---|
| 328 | ; genv2: genv globals sparams2 |
|---|
| 329 | }. |
|---|
| 330 | |
|---|
| 331 | definition joint_exec: trans_system io_out io_in ≝ |
|---|
| 332 | mk_trans_system … evaluation_parameters (λG. state (sparams2 G)) |
|---|
| 333 | (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G)) |
|---|
| 334 | (λG.eval_statement (globals G) (sparams2 G) (genv2 G)). |
|---|
| 335 | |
|---|
| 336 | definition make_global : |
|---|
| 337 | ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)). |
|---|
| 338 | joint_program pars → evaluation_parameters |
|---|
| 339 | ≝ |
|---|
| 340 | λpars,sparams. |
|---|
| 341 | (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)). |
|---|
| 342 | [1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ] |
|---|
| 343 | qed. |
|---|
| 344 | |
|---|
| 345 | definition make_initial_state : |
|---|
| 346 | ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)). |
|---|
| 347 | ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝ |
|---|
| 348 | λpars,sparams,p. |
|---|
| 349 | let ge ≝ genv2 (make_global pars sparams p) in |
|---|
| 350 | do m ← init_mem Genv … (λx.[Init_space x]) p; |
|---|
| 351 | let main ≝ prog_main … p in |
|---|
| 352 | do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main); |
|---|
| 353 | do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b); |
|---|
| 354 | ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*) |
|---|
| 355 | cases daemon qed. |
|---|
| 356 | (* |
|---|
| 357 | RTL: |
|---|
| 358 | init_prog == init_mem |
|---|
| 359 | init_sp: inizializzare lo stack pointer |
|---|
| 360 | init_isp: inizializzare l'altro stack pointer |
|---|
| 361 | init_renv: inizializzare i registri fisici |
|---|
| 362 | init_main_call: chiamata di funzione |
|---|
| 363 | --- init_fun_call: cambia fra ERTL e LTL |
|---|
| 364 | change_carry: a 0 |
|---|
| 365 | *) |
|---|
| 366 | |
|---|
| 367 | definition joint_fullexec : |
|---|
| 368 | ∀pars:∀globals.params globals. |
|---|
| 369 | ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)). |
|---|
| 370 | fullexec io_out io_in ≝ |
|---|
| 371 | λpars,sparams. |
|---|
| 372 | mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams). |
|---|
