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

Legend:

Unmodified
Added
Removed
  • 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.