Changeset 2821


Ignore:
Timestamp:
Mar 8, 2013, 11:44:05 AM (7 years ago)
Author:
tranquil
Message:
  • implemented preclassified system for joint (in joint/joint_fullexec.ma)
Location:
src/joint
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2796 r2821  
    88(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    99 }.
    10  
    11 
    1210
    1311record prog_params : Type[1] ≝
     
    162160
    163161definition joint_call_ident : ∀p:evaluation_params.
    164   (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     162  state_pc p → ident ≝
    165163(* this is a definition without a dummy ident :
    166164λp,st.
     
    218216
    219217definition joint_tailcall_ident : ∀p:evaluation_params.
    220   (Σs : state_pc p.joint_classify p s = cl_tailcall) → ident ≝
     218  state_pc p → ident ≝
    221219λp,st.
    222220let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     
    268266  | _ ⇒ None ?
    269267  ].
     268
     269definition joint_label_of_pc ≝
     270  λp : evaluation_params.
     271    (λpc.
     272      match fetch_statement … (ev_genv p) pc with
     273      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
     274      | _ ⇒ None ?
     275      ]).
    270276
    271277definition joint_abstract_status :
     
    281287   (* as_pc_of ≝ *) (pc …)
    282288   (* as_classify ≝ *) (joint_classify p)
    283    (* as_label_of_pc ≝ *)
    284     (λpc.
    285       match fetch_statement … (ev_genv p) pc with
    286       [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    287       | _ ⇒ None ?
    288       ])
     289   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    289290   (* as_after_return ≝ *) (joint_after_ret p)
    290291   (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
    291    (* as_call_ident ≝ *) (joint_call_ident p)
    292    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
     292   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
     293   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
    293294
    294295(* alternative definition with integrated prog_params constructor *)
  • src/joint/joint_semantics.ma

    r2796 r2821  
    641641 | _ ⇒ Error ? [ ]
    642642 ]).
    643 
    644 (*
    645 record evaluation_parameters : Type[1] ≝
    646  { globals: list ident
    647  ; sparams:> sem_params
    648  ; exit: program_counter
    649  ; genv2: genv globals sparams
    650  }.
    651 
    652 (* Paolo: with structured traces, eval need not emit labels. However, this
    653   changes trans_system. For now, just putting a dummy thing for
    654   the transition. *)
    655 definition joint_exec: trans_system io_out io_in ≝
    656   mk_trans_system … evaluation_parameters (λG. state_pc G)
    657    (λG.is_final (globals G) G (genv2 G) (exit G))
    658    (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
    659 
    660 definition make_global :
    661  ∀pars: sem_params.
    662   joint_program pars → evaluation_parameters
    663 
    664  λpars.
    665  (* Invariant: a -1 block is unused in common/Globalenvs *)
    666  let b ≝ mk_block Code (-1) in
    667  let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    668   (λp. mk_evaluation_parameters
    669     (prog_var_names … p)
    670     (mk_sem_params … pars)
    671     ptr
    672     (globalenv_noinit … p)
    673   ).
    674 % qed.
    675 
    676 definition make_initial_state :
    677  ∀pars: sem_params.
    678  ∀p: joint_program … pars. res (state_pc pars) ≝
    679 λpars,p.
    680   let sem_globals ≝ make_global pars p in
    681   let ge ≝ genv2 sem_globals in
    682   let m ≝ alloc_mem … p in
    683   let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    684   let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    685   let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
    686   let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
    687   let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    688   let main ≝ prog_main … p in
    689   let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
    690   (* use exit sem_globals as ra and call_dest_for_main as dest *)
    691   let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
    692   let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
    693   ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    694   ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
    695   match main_fd with
    696   [ Internal fn ⇒
    697     do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
    698   | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    699   ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
    700 qed.
    701 
    702 definition joint_fullexec :
    703  ∀pars:sem_params.fullexec io_out io_in ≝
    704  λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
    705 *)
Note: See TracChangeset for help on using the changeset viewer.