Changeset 2443 for src/joint/Traces.ma
 Timestamp:
 Nov 8, 2012, 2:27:54 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2442 r2443 7 7 ; exit: cpointer 8 8 ; ev_genv: genv sparams globals 9 ; io_env : state sparams → ∀o:io_out.res (io_in o)9 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) 10 10 }. 11 11 … … 13 13 { prog_spars : sem_params 14 14 ; prog : joint_program prog_spars 15 ; prog_io : state prog_spars → ∀o.res (io_in o)15 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 16 16 }. 17 17 … … 28 28 «ptr, refl …» 29 29 (mk_genv_gen ?? (globalenv_noinit ? p) ?) 30 (prog_io pars).30 (* (prog_io pars) *). 31 31 (* TODO or TOBEFOUND *) 32 32 cases daemon … … 49 49 let dummy_pc ≝ mk_pointer (mk_block Code (1)) (mk_offset (bv_zero …)) in 50 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 51 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) 52 52 let main ≝ prog_main … p in 53 let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in 53 let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in 54 let st0' ≝ set_sp … spp st0 in 54 55 (* 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 in56 ! 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 57 58 ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ; 58 59 ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; … … 63 64 ]. 64 65 [ % 65  cases ispb 66  cases spb 67 ] normalize // 66  cases spb normalize // 67 ] 68 68 qed. 69 69 … … 114 114 qed. 115 115 116 (* 116 117 let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ 117 118 match c with … … 122 123  Wrong e ⇒ Error … e 123 124 ]. 125 *) 124 126 125 127 definition cost_label_of_stmt : … … 145 147 (* as_status ≝ *) (state_pc p) 146 148 (* as_execute ≝ *) 147 (λs1,s2. io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)149 (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2) 148 150 (* as_pc ≝ *) cpointerDeq 149 151 (* as_pc_of ≝ *) (pc …) … … 151 153 (λs. 152 154 match ( 153 ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;155 ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???; 154 156 match stmt with 155 157 [ sequential stp nxt ⇒ 156 ! 〈flow, s'〉 ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;158 ! 〈flow, s'〉 ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ; 157 159 return step_flow_classifier … flow 158 160  final stp ⇒ 159 ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;161 ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ; 160 162 return fin_step_flow_classifier … flow 161 163 ]) with 162 [ OKc ⇒ c163  Error_ ⇒ cl_other164 [ Value c ⇒ c 165  _ ⇒ cl_other 164 166 ]) 165 167 (* as_label_of_pc ≝ *) … … 175 177 succ_pc p p (pc … s1) nxt = return pc … s2) 176 178 (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?) 177 (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed. 179 (* as_call_ident_≝ *) 180 (λst.?). cases daemon (* TODO *) qed.
Note: See TracChangeset
for help on using the changeset viewer.