Changeset 2422
- Timestamp:
- Oct 30, 2012, 4:23:09 PM (8 years ago)
- Location:
- src/joint
- Files:
-
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint.ma
r2286 r2422 7 7 include "common/LabelledObjects.ma". 8 8 include "ASM/Util.ma". 9 include "common/StructuredTraces.ma".10 9 11 10 (* Here is the structure of parameter records (downward edges are coercions, … … 169 168 λp,g,P,inst. All … P (step_labels … inst). 170 169 171 definition step_classifier :172 ∀p.∀globals.173 joint_step p globals → status_class ≝ λp,g,s.174 match s with175 [ step_seq s ⇒176 match s with177 [ CALL_ID _ _ _ ⇒ cl_call178 | extension_call _ ⇒ cl_call179 | _ ⇒ cl_other180 ]181 | COND _ _ ⇒ cl_jump182 ].183 184 170 record stmt_params : Type[1] ≝ 185 171 { uns_pars :> unserialized_params … … 207 193 ]. 208 194 209 definition fin_step_classifier :210 ∀p : stmt_params.211 joint_fin_step p → status_class212 ≝ λp,s.213 match s with214 [ GOTO _ ⇒ cl_other215 | _ ⇒ cl_return216 ].217 218 195 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 219 196 | sequential: joint_step p globals → succ p → joint_statement p globals 220 197 | final: joint_fin_step p → joint_statement p globals. 221 222 definition stmt_classifier :223 ∀p : stmt_params.∀globals.224 joint_statement p globals → status_class225 ≝ λp,g,s.226 match s with227 [ sequential stp _ ⇒ step_classifier p g stp228 | final stp ⇒ fin_step_classifier p stp229 ].230 198 231 199 coercion extension_fin_to_fin_step : ∀p : stmt_params. … … 466 434 definition joint_closed_internal_function ≝ 467 435 λp,globals. 468 Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).436 Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def). 469 437 470 438 definition set_joint_code ≝ … … 534 502 (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). 535 503 536 definition joint_function ≝ λp,globals. fundef (joint_ internal_function p globals).504 definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals). 537 505 538 506 definition joint_program ≝ -
src/joint/SemanticUtils.ma
r2286 r2422 151 151 definition make_sem_graph_params : 152 152 ∀pars : graph_params. 153 ∀g_pars : more_sem_unserialized_params pars (joint_ internal_function pars).153 ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars). 154 154 sem_params ≝ 155 155 λpars,g_pars. … … 190 190 definition make_sem_lin_params : 191 191 ∀pars : lin_params. 192 ∀g_pars : more_sem_unserialized_params pars (joint_ internal_function pars).192 ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars). 193 193 sem_params ≝ 194 194 λpars,g_pars. -
src/joint/Traces.ma
r2286 r2422 1 1 include "joint/semantics.ma". 2 include "common/StructuredTraces.ma". 2 3 3 4 record evaluation_params : Type[1] ≝ … … 7 8 ; ev_genv: genv sparams globals 8 9 ; io_env : state sparams → ∀o:io_out.res (io_in o) 9 } . 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 }. 10 17 11 (*record classifier_params : Type[1] ≝ 12 { cl_pars :> evaluation_parameters 13 ; cl_ext_step : ext_step cl_pars → status_class 14 ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class 15 }.*) 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. 16 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 check save_frame 41 42 definition make_initial_state : 43 ∀pars: prog_params.res (state_pc pars) ≝ 44 λpars.let p ≝ prog pars in 45 let sem_globals : evaluation_params ≝ pars in 46 let ge ≝ ev_genv sem_globals in 47 let m ≝ alloc_mem … p in 48 let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in 49 let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in 50 let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in 51 let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in 52 let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in 53 let main ≝ prog_main … p in 54 let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in 55 (* use exit sem_globals as ra and call_dest_for_main as dest *) 56 ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ; 57 let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in 58 ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ; 59 ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; 60 match main_fd with 61 [ Internal fn ⇒ 62 do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars) 63 | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *) 64 ]. 65 [ % 66 | cases ispb 67 | cases spb 68 ] normalize // 69 qed. 70 71 definition step_flow_classifier : 72 ∀p : evaluation_params.∀F,flows. 73 step_flow p F flows → status_class ≝ 74 λp,F,flows,flow.match flow with 75 [ Redirect _ _ ⇒ cl_jump 76 | Init bl _ _ _ ⇒ 77 match symbol_for_block … (ev_genv p) (mk_block Code bl) with 78 [ Some f ⇒ cl_call f 79 | None ⇒ cl_other (* we don't care, as call will fail anyway *) 80 ] 81 | Proceed flows ⇒ 82 match flows with 83 [ Labels lbls ⇒ 84 match lbls with 85 [ nil ⇒ cl_other 86 | _ ⇒ cl_jump 87 ] 88 | _ ⇒ cl_other 89 ] 90 ]. 91 92 definition fin_step_flow_classifier : 93 ∀p : evaluation_params.∀F,flows. 94 fin_step_flow p F flows → status_class ≝ 95 λp,F,flows,flow.match flow with 96 [ FRedirect lbls _ ⇒ 97 match lbls with 98 [ nil ⇒ (* not really possible, we don't care *) cl_other 99 | cons _ tl ⇒ 100 match tl with 101 [ nil ⇒ (* only one label *) cl_other 102 | _ ⇒ (* fork *) cl_jump 103 ] 104 ] 105 | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *) 106 cl_other 107 | _ ⇒ cl_return 108 ]. 17 109 18 110 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?. … … 58 150 (* as_pc_of ≝ *) (pc …) 59 151 (* as_classifier ≝ *) 60 (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧ 61 stmt_classifier … stmt = cl) 152 (λs,cl.∃fn,stmt. 153 fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧ 154 match stmt with 155 [ sequential stp nxt ⇒ 156 ∃flow,s'. 157 io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) = return 〈flow, s'〉 ∧ 158 step_flow_classifier … flow = cl 159 | final stp ⇒ 160 ∃flow.io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) = return flow ∧ 161 fin_step_flow_classifier … flow = cl 162 ]) 62 163 (* as_label_of_pc ≝ *) 63 164 (λpc. -
src/joint/blocks.ma
r2286 r2422 239 239 definition seq_block_step_in_code ≝ 240 240 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst. 241 src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst. 241 ∃hd,tl.l = hd @ [tl] ∧ 242 src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst. 242 243 243 244 definition seq_block_fin_step_in_code ≝ 244 245 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit. 245 src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B). 246 ∃hd,tl.l = hd @ [tl] ∧ 247 src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B). 246 248 247 249 (* generates ambiguity even if it shouldn't -
src/joint/linearise.ma
r2286 r2422 652 652 ∀p : unserialized_params. 653 653 ∀globals. 654 joint_ internal_function (mk_graph_params p) globals →655 joint_ internal_function (mk_lin_params p) globals654 joint_closed_internal_function (mk_graph_params p) globals → 655 joint_closed_internal_function (mk_lin_params p) globals 656 656 (* ∃sigma : identifier_map LabelTag ℕ. 657 657 let g ≝ joint_if_code ?? (pi1 … fin) in … … 669 669 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 670 670 (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ 671 λp,globals,f_ in.672 mk_joint_internal_function (mk_lin_params p) globals671 λp,globals,f_sig.let f_in ≝ pi1 … f_sig in 672 «mk_joint_internal_function (mk_lin_params p) globals 673 673 (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in) 674 674 (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in) 675 675 (joint_if_stacksize ?? f_in) 676 (linearise_code p globals (joint_if_code … f_in) 677 (match daemon in False with [ ]) 678 (joint_if_entry … f_in)) 679 0 0 (* exit is dummy! *). 676 (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in)) 677 0 0 (* exit is dummy! *), ?». 680 678 elim (linearise_code ?????) #c * #code_closed 679 [3: #_ assumption ] 681 680 @hide_prf 682 681 * #sigma * #O_in #sigma_prop … … 688 687 ] 689 688 qed. 689 690 definition linearise : ∀p : unserialized_params. 691 program (joint_function (mk_graph_params p)) ℕ → 692 program (joint_function (mk_lin_params p)) ℕ ≝ 693 λp,pr.transform_program ??? pr 694 (λglobals.transf_fundef ?? (linearise_int_fun p globals)). -
src/joint/semantics.ma
r2286 r2422 17 17 }. 18 18 19 definition genv ≝ λp.genv_gen (joint_ internal_function p).19 definition genv ≝ λp.genv_gen (joint_closed_internal_function p). 20 20 coercion genv_to_genv_t : 21 21 ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝ 22 22 λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?. 23 24 23 definition cpointer ≝ Σp.ptype p = Code. 25 24 definition xpointer ≝ Σp.ptype p = XData. 26 25 unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). 27 26 unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). 27 unification hint 0 ≔ p,g ⊢ 28 joint_closed_internal_function p g ≡ 29 Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)). 28 30 29 31 record sem_state_params : Type[1] ≝ … … 82 84 genv pars globals → 83 85 block → 84 res (joint_ internal_function pars globals) ≝86 res (joint_closed_internal_function pars globals) ≝ 85 87 λpars,globals,ge,b. 86 88 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; … … 95 97 genv pars globals → 96 98 cpointer → 97 res (joint_ internal_function pars globals) ≝99 res (joint_closed_internal_function pars globals) ≝ 98 100 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 99 101 … … 149 151 ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 150 152 F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars)) 153 ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 154 state st_pars → IO io_out io_in ident 151 155 ; eval_ext_call: ∀globals.genv_gen F globals → 152 156 ext_call uns_pars → state st_pars → 153 157 IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars)) 158 ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars → 159 state st_pars → IO io_out io_in ident 154 160 ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars) 155 161 (* do something more in some op2 calculations (e.g. mark a register for correction … … 266 272 (* parameters that are defined by serialization *) 267 273 record more_sem_params (pp : params) : Type[1] ≝ 268 { msu_pars :> more_sem_unserialized_params pp (joint_ internal_function pp)274 { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp) 269 275 ; offset_of_point : code_point pp → option offset (* can overflow *) 270 276 ; point_of_offset : offset → code_point pp … … 347 353 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 348 354 genv p globals → cpointer → 349 res ((joint_ internal_function p globals) × (joint_statement p globals)) ≝355 res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝ 350 356 λp,msp,globals,ge,ptr. 351 357 let pt ≝ point_of_pointer ? msp ptr in … … 427 433 428 434 definition eval_seq_no_pc : 429 ∀p:sem_params.∀globals. genv p globals → joint_ internal_function p globals →435 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → 430 436 state p → ∀s:joint_seq p globals. 431 437 IO io_out io_in (state p) ≝ … … 513 519 definition eval_step : 514 520 ∀p:sem_params.∀globals. genv p globals → 515 joint_ internal_function p globals → state p →521 joint_closed_internal_function p globals → state p → 516 522 ∀s:joint_step p globals. 517 523 IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝ … … 533 539 534 540 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals → 535 (* current function *) joint_ internal_function p globals → state p → ∀s : joint_fin_step p.541 (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p. 536 542 IO io_out io_in (state p) ≝ 537 543 λp,globals,ge,curr_fn,st,s. … … 544 550 545 551 definition eval_fin_step_pc : 546 ∀p:sem_params.∀globals. genv p globals → joint_ internal_function p globals → state p →552 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p → 547 553 ∀s:joint_fin_step p. 548 554 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ … … 557 563 558 564 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals → 559 state p → Z → joint_ internal_function p globals → call_args p →565 state p → Z → joint_closed_internal_function p globals → call_args p → 560 566 res (state_pc p) ≝ 561 567 λp,globals,ge,st,id,fn,args. … … 600 606 definition eval_statement : 601 607 ∀globals.∀p:sem_params.genv p globals → 602 state_pc p → joint_ internal_function p globals → joint_statement p globals →608 state_pc p → joint_closed_internal_function p globals → joint_statement p globals → 603 609 IO io_out io_in (state_pc p) ≝ 604 610 λglobals,p,ge,st,curr_fn,stmt. -
src/joint/semantics_blocks.ma
r2324 r2422 232 232 %* #H @H -H 233 233 lapply tl_other lapply rest_in_code 234 (* BUG? cases tl causes "Ill formed pattern" *) 235 @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?]) 234 cases tl [2: #hd' #tl' ] 236 235 cases rest [2,4: #mid' #rest'] 237 [ 1,4: * ]236 [2,3: * ] 238 237 [2: whd in ⊢ (%→?); #EQ' destruct(EQ') * 239 238 | ** #nxt' * #at_mid #_ #_ * #mid_other #_
Note: See TracChangeset
for help on using the changeset viewer.