Changeset 2537


Ignore:
Timestamp:
Dec 6, 2012, 1:24:29 PM (7 years ago)
Author:
tranquil
Message:

rolled back changes on calls in joint. Now the save_frame parameter
has a switch that tells whether the call is an ident one or a pointer one.
The idea is that in the latter case, from LTL onwards, the caller address is not saved (as it is done by explicit instructions

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN.ma

    r2490 r2537  
    1010inductive ltl_lin_seq : Type[0] ≝
    1111| SAVE_CARRY : ltl_lin_seq
    12 | RESTORE_CARRY : ltl_lin_seq.
     12| RESTORE_CARRY : ltl_lin_seq
     13| LOW_ADDRESS : Register → label → ltl_lin_seq
     14| HIGH_ADDRESS : Register → label → ltl_lin_seq.
     15
     16definition ltl_lin_seq_labels ≝ λs.match s with
     17[ LOW_ADDRESS _ lbl ⇒ [ lbl ]
     18| HIGH_ADDRESS _ lbl ⇒ [ lbl ]
     19| _ ⇒ [ ]
     20].
    1321
    1422definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
     
    2634    (* call_dest ≝ *) unit
    2735    (* ext_seq ≝ *) ltl_lin_seq
     36    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
    2837    (* has_tailcalls ≝ *) false
    2938    (* paramsT ≝ *) unit
  • src/joint/Joint.ma

    r2532 r2537  
    8080 ; snd_arg : Type[0]  (* second argument of binary op *)
    8181 ; pair_move: Type[0] (* argument of move instructions *)
    82  ; call_spec: Type[0] (* type of call (ident/pointer) *)
    8382 ; call_args: Type[0] (* arguments of function calls *)
    8483 ; call_dest: Type[0] (* possible destination of function computation *)
     
    108107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    109108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    110   | CALL: call_spec p → call_args p → call_dest p → joint_seq p globals
     109  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_seq p globals
    111110  | extension_seq : ext_seq p → joint_seq p globals.
    112111
     
    170169  | RETURN: joint_fin_step p
    171170  | TAILCALL :
    172     has_tailcalls p → call_spec p
     171    has_tailcalls p → (ident + (dpl_arg p × (dph_arg p)))
    173172    call_args p → joint_fin_step p.
    174173
  • src/joint/semantics.ma

    r2532 r2537  
    165165  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    166166  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    167   ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars)
     167  ; save_frame: bool (* ident or ptr *) → call_dest uns_pars → state_pc st_pars → res (state st_pars)
    168168   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    169169     type of arguments. To be fixed using a dependent type *)
     
    177177
    178178  (* from now on, parameters that use the type of functions *)
    179   ; block_of_call : ∀globals.genv_t (fundef (F globals)) → call_spec uns_pars →
    180       state st_pars →  res (Σbl.block_region bl = Code)
    181179  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars →
    182180      state st_pars → res (list beval)
     
    369367 let newpc ≝ succ_pc … (pc … st) l in
    370368 mk_state_pc … st newpc.
    371 
    372 definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
    373 λbl.match block_region bl
    374   return λx.block_region bl = x → option (Σb.block_region b = Code) with
    375   [ Code ⇒ λprf.Some ? «bl, prf»
    376   | XData ⇒ λ_.None ?
    377   ] (refl …).
    378 
    379 (* to be used in implementations *)
    380 definition block_of_call_id ≝  λF.λsp:sem_state_params.
    381   λge: genv_t F.λid.λst:state sp.
    382   opt_to_res … [MSG BadFunction; CTX … id] (
    383     ! bl ← find_symbol … ge id;
    384     code_block_of_block bl).
    385  
    386 definition block_of_call_id_ptr ≝ λp,F.λsp : sem_unserialized_params p F.
    387   λglobals.λge: genv_t (F globals).λf.λst : state sp.
    388   match f with
    389   [ inl id ⇒ block_of_call_id … ge id st
    390   | inr addr ⇒
    391     ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    392     ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    393     ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
    394     if eq_bv … (bv_zero …) (offv (poff ptr)) then
    395       opt_to_res … [MSG BadFunction; MSG BadPointer]
    396         (code_block_of_block (pblock … ptr))
    397     else
    398       Error … [MSG BadFunction; MSG BadPointer]
    399   ].
    400 
    401 (* Paolo: why external calls do not need args?? *)
    402 definition eval_external_call ≝
    403 λp : sem_params.λfn,args,dest,st.
    404       ! params ← fetch_external_args … p fn st args : IO ???;
    405       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    406       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    407       (* CSC: XXX bug here; I think I should split it into Byte-long
    408          components; instead I am making a singleton out of it. To be
    409          fixed once we fully implement external functions. *)
    410       let vs ≝ [mk_val ? evres] in
    411       set_result … p vs dest st.
    412 
    413 axiom MissingStackSize : String.
    414 
    415 definition eval_internal_call_no_pc ≝
    416 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
    417 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    418 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    419 return allocate_locals … p (joint_if_locals … fn) st.
    420369
    421370axiom NoSuccessor : String.
     
    495444qed.
    496445
     446definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
     447λbl.match block_region bl
     448  return λx.block_region bl = x → option (Σb.block_region b = Code) with
     449  [ Code ⇒ λprf.Some ? «bl, prf»
     450  | XData ⇒ λ_.None ?
     451  ] (refl …).
     452
     453(* to be used in implementations *)
     454definition block_of_call_id ≝  λF.λsp:sem_state_params.
     455  λge: genv_t F.λid.λst:state sp.
     456  opt_to_res … [MSG BadFunction; CTX … id] (
     457    ! bl ← find_symbol … ge id;
     458    code_block_of_block bl).
     459 
     460definition block_of_call ≝ λp : sem_params.
     461  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
     462  ! bl ← match f with
     463    [ inl id ⇒
     464      opt_to_res … [MSG BadFunction; CTX … id]
     465        (find_symbol … ge id)
     466    | inr addr ⇒
     467      ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     468      ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     469      ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
     470      if eq_bv … (bv_zero …) (offv (poff ptr)) then
     471        return pblock ptr
     472      else
     473        Error … [MSG BadFunction; MSG BadPointer]
     474    ] ;
     475  opt_to_res … [MSG BadFunction; MSG BadPointer]
     476    (code_block_of_block bl).
     477
     478definition eval_external_call ≝
     479λp : sem_params.λfn,args,dest,st.
     480      ! params ← fetch_external_args … p fn st args : IO ???;
     481      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     482      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     483      (* CSC: XXX bug here; I think I should split it into Byte-long
     484         components; instead I am making a singleton out of it. To be
     485         fixed once we fully implement external functions. *)
     486      let vs ≝ [mk_val ? evres] in
     487      set_result … p vs dest st.
     488
     489axiom MissingStackSize : String.
     490
     491definition eval_internal_call ≝
     492λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
     493! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
     494! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     495return allocate_locals … p (joint_if_locals … fn) st.
     496
     497definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     498
    497499definition eval_seq_call ≝
    498500λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
     
    502504match fd with
    503505[ Internal ifd ⇒
    504   ! st' ← save_frame … dest st ;
    505   ! st'' ← eval_internal_call_no_pc p globals ge i ifd args st' ;
     506  ! st' ← save_frame … (is_inl … f) dest st ;
     507  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    506508  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    507509  return mk_state_pc … st'' pc
     
    552554match fd with
    553555[ Internal ifd ⇒
    554   ! st' ← eval_internal_call_no_pc p globals ge i ifd args st ;
     556  ! st' ← eval_internal_call p globals ge i ifd args st ;
    555557  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    556558  return mk_state_pc … st' pc
Note: See TracChangeset for help on using the changeset viewer.