Changeset 2878 for src/joint

Timestamp:

Mar 15, 2013, 11:32:51 AM (8 years ago)

Author:

tranquil

Message:

backtracked some changes that were not ready for commit

File:

• src/joint/joint_semantics.ma (modified) (6 diffs)

src/joint/joint_semantics.ma

@@ -59 +59 @@
  ; carry: bebit
  ; regs: regsT semp
- ; stack_usage : ℕ
  ; m: bemem
  }.
@@ -80 +79 @@
 
 definition set_m: ∀p. bemem → state p → state p ≝
- λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st)
-  (stack_usage … st) m.
+ λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
 
 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
- λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs
-  (stack_usage … st) (m … st).
+ λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
 
 definition set_sp: ∀p. ? → state p → state p ≝
  λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
- mk_state p (st_frms … st) (istack … st) (carry … st) regs' (stack_usage … st) (m … st).
+ mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
 
 definition set_carry: ∀p. bebit → state p → state p ≝
- λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st)
- (stack_usage … st) (m … st).
+ λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
 
 definition set_istack: ∀p. internal_stack → state p → state p ≝
- λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st)
- (stack_usage … st)  (m … st).
+ λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
 
 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
@@ -109 +104 @@
 
 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
- λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st)
- (stack_usage … st) (m … st).
+ λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
 
 (*
@@ -519 +513 @@
       set_result … p vs dest st.
 
-definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
-λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
-  (stack_usage … st + n) (m … st).
-
-definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
-λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
-  (stack_usage … st - n) (m … st).
-
 definition eval_internal_call ≝
 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
 λst : state p.
 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
-! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
-return increment_stack_usage … stack_size st'.
+setup_call … stack_size (joint_if_params … globals fn) args st.
 
 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
@@ -571 +556 @@
 λst : state p.
 ! st' ← pop_frame … ge curr_id curr_ret st ;
-! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
-let st'' ≝ decrement_stack_usage … stack_size (\fst st') in
 ! nxt ← next_of_call_pc … ge (\snd … st') ;
 return
-  next … nxt (set_last_pop … (\snd … st') 〈st'', \snd st'〉) (* now address pushed on stack are calling ones! *).
+  next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
 
 definition eval_tailcall ≝
@@ -585 +568 @@
 match fd with
 [ Internal ifd ⇒
-  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
-  let st' ≝ decrement_stack_usage … stack_size st in
-  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
+  ! st' ← eval_internal_call p globals ge i ifd args st ;
   let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
-  return mk_state_pc … st'' pc (last_pop … st)
+  return mk_state_pc … st' pc (last_pop … st)
 | External efd ⇒
   ! st' ← eval_external_call … efd args curr_ret st ;