Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2920 r2946  
    6060 ; regs: regsT semp
    6161 ; m: bemem
     62 ; stack_usage : ℕ
    6263 }.
    6364
     
    6768  { st_no_pc :> state semp
    6869  ; pc : program_counter
    69   (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
     70  (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
    7071  ; last_pop : program_counter
    7172  }.
    7273
    73 (* special program counter that is guaranteed to not correspond to anything *)
    74 definition exit_pc : program_counter ≝
     74definition init_pc : program_counter ≝
    7575  mk_program_counter «mk_block (-1), refl …» one.
    7676
     
    7979
    8080definition set_m: ∀p. bemem → state p → state p ≝
    81  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
     81 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
    8282
    8383definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    84  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
     84 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
    8585
    8686definition set_sp: ∀p. ? → state p → state p ≝
    8787 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    88  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
     88 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
    8989
    9090definition set_carry: ∀p. bebit → state p → state p ≝
    91  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     91 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
    9292
    9393definition set_istack: ∀p. internal_stack → state p → state p ≝
    94  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
     94 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
    9595
    9696definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    100100 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    101101
    102 definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
    103  λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.
     102definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
     103 λp,st,pc. mk_state_pc … st pc pc.
    104104
    105105definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    106  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
     106 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
    107107
    108108(*
     
    268268
    269269(* parameters that are defined by serialization *)
    270 record sem_params : Type[1] ≝
     270record serialized_params : Type[1] ≝
    271271  { spp :> params
    272272  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
     
    277277  ; offset_of_point_of_offset :
    278278    ∀o.offset_of_point (point_of_offset o) = o
     279  }.
     280
     281record sem_params : Type[1] ≝
     282  { spp' :> serialized_params
     283  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
    279284  }.
    280285
     
    513518      set_result … p vs dest st.
    514519
     520definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
     521 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     522  (n + stack_usage … st).
     523
     524definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
     525 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     526  (stack_usage … st - n).
     527
    515528definition eval_internal_call ≝
    516529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
    517530λst : state p.
    518531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    519 setup_call … stack_size (joint_if_params … globals fn) args st.
     532! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     533return increment_stack_usage … stack_size st'.
    520534
    521535definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     
    555569λcurr_id.λcurr_ret : call_dest p.
    556570λst : state p.
    557 ! st' ← pop_frame … ge curr_id curr_ret st ;
    558 ! nxt ← next_of_call_pc … ge (\snd … st') ;
     571! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
     572! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
     573! nxt ← next_of_call_pc … ge call_pc ;
     574let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
    559575return
    560   next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
     576  next ? nxt st'' (* now address pushed on stack are calling ones! *).
    561577
    562578definition eval_tailcall ≝
     
    568584match fd with
    569585[ Internal ifd ⇒
    570   ! st' ← eval_internal_call p globals ge i ifd args st ;
     586  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
     587  let st' ≝ decrement_stack_usage … stack_size st in
     588  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    571589  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    572   return mk_state_pc … st' pc (last_pop … st)
     590  return mk_state_pc … st'' pc (last_pop … st)
    573591| External efd ⇒
    574592  ! st' ← eval_external_call … efd args curr_ret st ;
     
    621639  let st'' ≝ set_no_pc … st' st in
    622640  eval_statement_advance … ge id fn s st''.
    623 
    624 definition is_final: ∀p: sem_params.∀globals.
    625   genv p globals → program_counter → state_pc p → option int ≝
    626  λp,globals,ge,exit,st.res_to_opt ? (
    627   do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
    628   match s with
    629   [ final s' ⇒
    630     match s' with
    631     [ RETURN ⇒
    632       let curr_ret ≝ joint_if_result … fn in
    633       do st' ← pop_frame … ge id curr_ret st;
    634       if eq_program_counter (\snd … st') exit then
    635       do vals ← read_result … ge curr_ret st ;
    636         Word_of_list_beval vals
    637       else
    638         Error ? [ ]
    639    | _ ⇒ Error ? [ ]
    640    ]
    641  | _ ⇒ Error ? [ ]
    642  ]).
Note: See TracChangeset for help on using the changeset viewer.