Changeset 2233

Timestamp:

Jul 23, 2012, 4:51:51 PM (8 years ago)

Author:

tranquil

Message:

• completed update of ERTL semantics
• some minor changes in joint semantics

Location:

src

Files:

• ERTL/semantics_paolo.ma (modified) (1 diff)
• LIN/joint_LTL_LIN_semantics_paolo.ma (modified) (1 diff)
• RTL/semantics_paolo.ma (modified) (11 diffs)
• joint/semantics_paolo.ma (modified) (13 diffs)

src/ERTL/semantics_paolo.ma

@@ -1 @@
-include "joint/SemanticUtils.ma".
-include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
+include "joint/semanticsUtils_paolo.ma".
+include "ERTL/ERTL_paolo.ma". (* CSC: syntax.ma in RTLabs *)
 include alias "common/Identifiers.ma".
 
+record ertl_psd_env : Type[0] ≝
+  { psd_regs : register_env beval
+  (* this tells what pseudo-registers should have their value corrected by spilled_no *)
+  ; need_spilled_no : identifier_set RegisterTag
+  }.
+
+definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
+definition add_need_spilled_no ≝
+  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
+definition rm_need_spilled_no ≝
+  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
+
+definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
+
 definition ps_reg_store ≝
- λr,v.λlocal_env:(register_env beval) × hw_register_env.
-  do res ← reg_store r v (\fst local_env) ;
-  OK … 〈res, \snd local_env〉.
+ λr,v.λlocal_env : ertl_reg_env.
+  do res ← reg_store r v (psd_regs (\fst local_env)) ;
+  let psd_env ≝ set_psd_regs res (\fst local_env) in
+  OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
 
 definition ps_reg_retrieve ≝
- λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
+ λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
 
 definition hw_reg_store ≝
- λr,v.λlocal_env:(register_env beval) × hw_register_env.
+ λr,v.λlocal_env:ertl_reg_env.
   OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
 
 definition hw_reg_retrieve ≝
- λlocal_env:(register_env beval) × hw_register_env.λreg.
+ λlocal_env:ertl_reg_env.λreg.
   OK … (hwreg_retrieve … (\snd local_env) reg).
 
-definition ertl_more_sem_params: more_sem_params ertl_params_ :=
- mk_more_sem_params ertl_params_
-  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
-   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
-   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
-    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
-     (λlocals,dest_src.
-       do v ←
-        match \snd dest_src with
-        [ pseudo reg ⇒ ps_reg_retrieve locals reg
-        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
-       match \fst dest_src with
-       [ pseudo reg ⇒ ps_reg_store reg v locals
-       | hardware reg ⇒ hw_reg_store reg v locals]).
-definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
+definition ps_arg_retrieve ≝
+  λlocal_env,a.
+  match a with
+  [ Reg r ⇒ ps_reg_retrieve local_env r
+  | Imm b ⇒ return b
+  ]. 
 
-definition ertl_init_locals :
- list register →
-  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
- λlocals,lenv.
-  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
+definition ERTL_state : sem_state_params ≝
+  mk_sem_state_params
+ (* framesT ≝ *) (list ertl_psd_env)
+ (* empty_framesT ≝ *) [ ]
+ (* regsT ≝ *) ertl_reg_env
+ (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).
 
-(*CSC: could we use here a dependent type to avoid the Error case? *)
-axiom EmptyStack: String.
-definition ertl_pop_frame:
- ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
- λglobals,ge,st.
-  let frms ≝ st_frms ? st in
-  match frms with
-  [ nil ⇒ Error ? [MSG EmptyStack]
-  | cons hd tl ⇒
-     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
+(* we ignore need_spilled_no as we never move framesize based values around in the
+   translation *)
+definition ertl_eval_move ≝ λenv,pr.
+      ! v ←
+        match \snd pr with
+        [ Reg src ⇒
+          match src with
+          [ PSD r ⇒ ps_reg_retrieve env r
+          | HDW r ⇒ hw_reg_retrieve env r
+          ]
+        | Imm bv ⇒ return bv ] ;
+      match \fst pr with
+      [ PSD r ⇒ ps_reg_store r v env
+      | HDW r ⇒ hw_reg_store r v env
+      ].
+
+definition ertl_allocate_local ≝
+  λreg.λlenv : ertl_reg_env.
+  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
 
 definition ertl_save_frame:
- address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
- λl.λ_.λ_.λ_.λ_.λst.
-  do st ← save_ra … st l ;
+ cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
+ λpc.λ_.λst.
+  do st ← save_ra … st pc ;
   OK …
-   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
-    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
-
-definition ertl_result_regs:
- ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
- λglobals,ge,st.
-  do fn ← graph_fetch_function … globals ge st ;
-  OK … (joint_if_result … fn).
+   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
+    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
 
 (*CSC: XXXX, for external functions only*)
-axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
-axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
+axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
+axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
+(* I think there should be a list beval in place of list val here
+  λvals.λ_.λst.
+  (* set all RegisterRets to 0 *)
+  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
+  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
+  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
+  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
+  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
 
-definition framesize:
- ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
-  λglobals,ge,st.
-   do f ← graph_fetch_function … ge st ;
-   OK ? (joint_if_stacksize globals … f).
+definition xdata_pointer_of_address: address → res xpointer ≝
+λp.let 〈v1,v2〉 ≝ p in
+! p ← pointer_of_bevals [v1;v2] ;
+match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
+[ XData ⇒ λE.OK ? (mk_Sig … p E)
+| _ ⇒ λ_.Error … [MSG BadPointer]
+] (refl …).
 
-definition get_hwsp : state ertl_sem_params → address ≝
+definition address_of_xdata_pointer: xpointer → address ≝
+λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
+
+definition get_hwsp : ERTL_state → res xpointer ≝
  λst.
   let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
   let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
-   〈spl,sph〉.
+  xdata_pointer_of_address 〈spl,sph〉.
 
-definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params ≝
+definition set_hwsp : xpointer → ERTL_state → ERTL_state ≝
  λsp,st.
-  let 〈spl,sph〉 ≝ sp in
+  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
   let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
   let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
-  set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
+  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
 
-definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
- λglobals.
-  mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
-    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
-    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
-    ertl_fetch_external_args ertl_set_result.
-definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
- λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).
+definition eval_ertl_seq:
+ ∀globals. genv ERTL globals →
+  ertl_seq → joint_internal_function ERTL globals → ERTL_state →
+   IO io_out io_in ERTL_state ≝
+ λglobals,ge,stm,curr_fn,st.
+ let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
+  match stm with
+   [ ertl_new_frame ⇒
+      ! sp ← get_hwsp st ;
+      let newsp ≝ shift_pointer … sp framesize in
+      return set_hwsp newsp st
+   | ertl_del_frame ⇒
+      ! sp ← get_hwsp st ;
+      let newsp ≝ shift_pointer … sp framesize in
+      return set_hwsp newsp st
+   | ertl_frame_size dst ⇒
+      let env ≝ regs … st in
+      ! env' ← ps_reg_store dst (BVByte framesize) env ;
+      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
+      return set_regs ERTL_state env'' st
+   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  
 
-definition ertl_exec_extended:
- ∀globals. genv globals (ertl_params globals) →
-  ertl_statement_extension → label → state ertl_sem_params →
-   IO io_out io_in (trace × (state ertl_sem_params)) ≝
- λglobals,ge,stm,l,st.
-  match stm with
-   [ ertl_st_ext_new_frame ⇒
-      ! v ← framesize globals … ge st;
-      let sp ≝ get_hwsp st in
-      ! newsp ← addr_sub sp v;
-      let st ≝ set_hwsp newsp st in
-      ! st ← next … (ertl_sem_params1 globals) l st ;
-        return 〈E0,st〉
-   | ertl_st_ext_del_frame ⇒
-      ! v ← framesize … ge st;
-      let sp ≝ get_hwsp st in
-      ! newsp ← addr_add sp v;
-      let st ≝ set_hwsp newsp st in
-      ! st ← next … (ertl_sem_params1 …) l st ;
-        return 〈E0,st〉
-   | ertl_st_ext_frame_size dst ⇒
-      ! v ← framesize … ge st;
-      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
-      ! st ← next … (ertl_sem_params1 …) l st ;
-        return 〈E0, st〉
-   ].
+definition ertl_post_op2 ≝
+  λop,dst,arg1,arg2,st.
+  let local_env ≝ regs ERTL_state st in
+  let f ≝ λarg,st.match arg with
+     [ Reg r ⇒
+       if r ∈ need_spilled_no (\fst local_env) then
+         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
+       else
+         st
+     | _ ⇒ st
+     ] in
+  match op with
+  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
+  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
+  | Sub ⇒ f arg1 st
+  | _ ⇒ st].
+         
 
-definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
- λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).
-
-definition ertl_fullexec: fullexec io_out io_in ≝
- joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
+definition ERTL_semantics ≝
+  make_sem_graph_params ERTL
+  (mk_more_sem_unserialized_params ??
+  (* st_pars            ≝ *) ERTL_state
+  (* acca_store_        ≝ *) ps_reg_store
+  (* acca_retrieve_     ≝ *) ps_reg_retrieve
+  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
+  (* accb_store_        ≝ *) ps_reg_store
+  (* accb_retrieve_     ≝ *) ps_reg_retrieve
+  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
+  (* dpl_store_         ≝ *) ps_reg_store
+  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
+  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
+  (* dph_store_         ≝ *) ps_reg_store
+  (* dph_retrieve_      ≝ *) ps_reg_retrieve
+  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
+  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
+  (* pair_reg_move_     ≝ *) ertl_eval_move
+  (* fetch_ra           ≝ *) (load_ra …)
+  (* allocate_local     ≝ *) ertl_allocate_local
+  (* save_frame         ≝ *) ertl_save_frame
+  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
+  (* fetch_external_args≝ *) ertl_fetch_external_args
+  (* set_result         ≝ *) ertl_set_result
+  (* call_args_for_main ≝ *) 0
+  (* call_dest_for_main ≝ *) it
+  (* read_result        ≝ *) (λ_.λ_.λ_.
+     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
+  (* eval_ext_seq       ≝ *) eval_ertl_seq
+  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
+  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
+  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
+  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).

src/LIN/joint_LTL_LIN_semantics_paolo.ma

@@ -63 +63 @@
   (* read_result        ≝ *) (λ_.λ_.λ_.
   λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
-  (* eval_ext_seq       ≝ *) (λ_.λ_.eval_ltl_lin_seq)
+  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
   (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
-  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st).
+  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
+  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).

src/RTL/semantics_paolo.ma

@@ -30 +30 @@
 
 definition rtl_fetch_ra:
- state RTL_state → res ((state RTL_state) × cpointer) ≝
+ RTL_state → res (RTL_state × cpointer) ≝
  λst.
   match st_frms ? st with
@@ -41 +41 @@
 
 definition rtl_setup_call:
- nat → list register → list psd_argument → state RTL_state → res (state RTL_state) ≝
+ nat → list register → list psd_argument → RTL_state → res RTL_state ≝
   λstacksize,formal_arg_regs,actual_arg_regs,st.
   let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
@@ -57 +57 @@
 qed.
 
-definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state.
+definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
   OK … (set_frms RTL_state frame st).
 
 (*CSC: XXXX, for external functions only*)
-axiom rtl_fetch_external_args: external_function → state RTL_state → res (list val).
-axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state).
+axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
+axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
 
 definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
@@ -69 +69 @@
 
 definition rtl_read_result :
- ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝
+ ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
  λglobals,ge,rets,st.
  m_list_map … (rtl_reg_retrieve st) rets.
@@ -77 +77 @@
   saves the OutOfBounds exception *)
 definition rtl_pop_frame:
- ∀globals. genv RTL globals → list register → state RTL_state →
-  res (state RTL_state) ≝
- λglobals,ge,ret,st.
+ ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
+  res RTL_state ≝
+ λglobals,ge,curr_fn,st.
+  let ret ≝ joint_if_result … curr_fn in
   do ret_vals ← rtl_read_result … ge ret st ;
   match st_frms ? st with
@@ -99 +100 @@
 (* This code is quite similar to eval_call_block: can we factorize it out? *)
 definition eval_tailcall_block:
- ∀globals.genv RTL globals → state RTL_state →
+ ∀globals.genv RTL globals → RTL_state →
   block → call_args RTL →
   (* this is where the result of the current function should be stored *)
   call_dest RTL →
   IO io_out io_in
-    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝
+    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
  λglobals,ge,st,b,args,ret.
   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
@@ -122 +123 @@
     ].
 
-definition block_of_register_pair: register → register → state RTL_state → res block ≝
+definition block_of_register_pair: register → register → RTL_state → res block ≝
  λr1,r2,st.
  do v1 ← rtl_reg_retrieve st r1 ;
@@ -131 +132 @@
 definition eval_rtl_seq:
  ∀globals. genv RTL globals →
-  rtl_seq → state RTL_state →
-   IO io_out io_in (state RTL_state) ≝
- λglobals,ge,stm,st.
+  rtl_seq → joint_internal_function RTL globals → RTL_state →
+   IO io_out io_in RTL_state ≝
+ λglobals,ge,stm,curr_fn,st.
   match stm with
    [ rtl_stack_address dreg1 dreg2  ⇒
@@ -144 +145 @@
 definition eval_rtl_call:
  ∀globals. genv RTL globals →
-  rtl_call → state RTL_state →
-   IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝
+  rtl_call → RTL_state →
+   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
  λglobals,ge,stm,st.
   match stm with
@@ -169 +170 @@
 definition eval_rtl_tailcall:
  ∀globals. genv RTL globals →
-  rtl_tailcall → call_dest RTL → state RTL_state →
-   IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝
-   λglobals,ge,stm,ret,st.
+  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
+   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
+   λglobals,ge,stm,curr_fn,st.
+   let ret ≝ joint_if_result … curr_fn in
    match stm with
    [ rtl_tailcall_id id args ⇒
@@ -182 +184 @@
 
 definition RTL_semantics ≝
-  mk_more_sem_unserialized_params RTL (joint_internal_function RTL)
-    RTL_state
-    reg_store reg_retrieve rtl_arg_retrieve
-    reg_store reg_retrieve rtl_arg_retrieve
-    reg_store reg_retrieve rtl_arg_retrieve
-    reg_store reg_retrieve rtl_arg_retrieve
-    rtl_arg_retrieve
-    (λenv,p. let 〈dest,src〉 ≝ p in
-      ! v ← rtl_arg_retrieve env src ;
-      reg_store dest v env)
-    rtl_fetch_ra
-    rtl_init_local
-    rtl_save_frame
-    rtl_setup_call
-    rtl_fetch_external_args
-    rtl_set_result
-    [ ] [ ]
-    rtl_read_result
-    eval_rtl_seq
-    eval_rtl_tailcall
-    eval_rtl_call.
+  make_sem_graph_params RTL
+    (mk_more_sem_unserialized_params ??
+      RTL_state
+      reg_store reg_retrieve rtl_arg_retrieve
+      reg_store reg_retrieve rtl_arg_retrieve
+      reg_store reg_retrieve rtl_arg_retrieve
+      reg_store reg_retrieve rtl_arg_retrieve
+      rtl_arg_retrieve
+      (λenv,p. let 〈dest,src〉 ≝ p in
+        ! v ← rtl_arg_retrieve env src ;
+        reg_store dest v env)
+      rtl_fetch_ra
+      rtl_init_local
+      rtl_save_frame
+      rtl_setup_call
+      rtl_fetch_external_args
+      rtl_set_result
+      [ ] [ ]
+      rtl_read_result
+      eval_rtl_seq
+      eval_rtl_tailcall
+      eval_rtl_call
+      rtl_pop_frame
+      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).

src/joint/semantics_paolo.ma

@@ -33 +33 @@
  ; m: bemem
  }.
+
+coercion sem_state_params_to_state nocomposites:
+  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
 
 record state_pc (semp : sem_state_params) : Type[0] ≝
@@ -134 +137 @@
   (* change of pc must be left to *_flow execution *)
   ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
-      state st_pars → IO io_out io_in (state st_pars)
+      F globals → state st_pars → IO io_out io_in (state st_pars)
   ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
-      call_dest uns_pars → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
-  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
-      state st_pars →
+      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
+  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) →
+      ext_call uns_pars → state st_pars →
       IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
-  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars)
+  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → F globals → state st_pars → res (state st_pars)
+  (* do something more in some op2 calculations (e.g. mark a register for correction
+     with spilled_no in ERTL) *)
+  ; post_op2 : ∀globals.genv_t (fundef (F globals)) →
+    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
+    state st_pars → state st_pars
   }.
 
@@ -407 +415 @@
 
 definition eval_seq_no_pc :
- ∀globals.∀p:sem_params. genv p globals → state p →
-  ∀s:joint_seq p globals.
+ ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
+  state p → ∀s:joint_seq p globals.
   IO io_out io_in (state p) ≝
- λglobals,p,ge,st,seq.
+ λp,globals,ge,curr_fn,st,seq.
   match seq return λx.IO ??? with
   [ extension_seq c ⇒
-    eval_ext_seq … ge c st
+    eval_ext_seq … ge c curr_fn st
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -447 +455 @@
       let carry ≝ beval_of_bool carry in
     ! st' ← acca_store … dacc_a v' st;
-    return set_carry … carry st'
+    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
   | CLEAR_CARRY ⇒
     return set_carry … BVfalse st
@@ -484 +492 @@
 
 definition eval_seq_pc :
- ∀globals.∀p:sem_params. genv p globals → state p →
+ ∀p:sem_params.∀globals. genv p globals → state p →
   ∀s:joint_seq p globals.
   IO io_out io_in (step_flow p ? (step_flows … s)) ≝
-  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
+  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
   [ CALL_ID id args dest ⇒
     ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
@@ -499 +507 @@
 
 definition eval_step :
- ∀globals.∀p:sem_params. genv p globals → state p →
+ ∀p:sem_params.∀globals. genv p globals →
+  joint_internal_function p globals → state p →
   ∀s:joint_step p globals.
   IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
-  λglobals,p,ge,st,s.
+  λp,globals,ge,curr_fn,st,s.
   match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
   [ step_seq s ⇒
     ! flow ← eval_seq_pc ?? ge st s ;
-    ! st' ← eval_seq_no_pc ?? ge st s ;
+    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
     return 〈flow,st'〉
   | COND src ltrue ⇒
@@ -518 +527 @@
   %1 % qed.
 
-definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
-  (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
+definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
+  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
   IO io_out io_in (state p) ≝
- λglobals,p,ge,ret,st,s.
+ λp,globals,ge,curr_fn,st,s.
   match s return λx.IO ??? with
     [ tailcall c ⇒
-      !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
+      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
       return st'
     | _ ⇒ return st
@@ -530 +539 @@
 
 definition eval_fin_step_pc :
- ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
+ ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
   ∀s:joint_fin_step p.
   IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
-  λg,p,ge,ret,st,s.
+  λp,g,ge,curr_fn,st,s.
   match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
   [ tailcall c ⇒
-    !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
+    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
     return flow  
   | GOTO l ⇒ return FRedirect … l
@@ -542 +551 @@
   ]. %1 % qed.
 
-definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals →
+definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
   state p → Z → joint_internal_function p globals → call_args p →
   res (state_pc p) ≝
-  λglobals,p,ge,st,id,fn,args.
+  λp,globals,ge,st,id,fn,args.
     ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
               args st ;
@@ -557 +566 @@
 (* The pointer provided is the one to the *next* instruction. *)
 definition eval_step_flow :
- ∀globals.∀p:sem_params.∀flows.genv p globals →
+ ∀p:sem_params.∀globals.∀flows.genv p globals →
  state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
- λglobals,p,flows,ge,st,nxt,cmd.
+ λp,globals,flows,ge,st,nxt,cmd.
  match cmd with
   [ Redirect _ l ⇒
@@ -570 +579 @@
   ].
 
-definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals →
+definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
   state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
-  λglobals,p,lbls,ge,st,curr,cmd.
+  λp,globals,lbls,ge,st,curr,cmd.
   match cmd with
   [ FRedirect _ l ⇒ goto … ge l st curr
@@ -580 +589 @@
     ! 〈st',ra〉 ← fetch_ra … st ;
     ! fn ← fetch_function … ge curr ;
-    ! st'' ← pop_frame … ge (joint_if_result … fn) st';
+    ! st'' ← pop_frame … ge fn st';
     return mk_state_pc ? st'' ra
   ].
@@ -591 +600 @@
  match stmt with
  [ sequential s nxt ⇒
-   ! 〈flow,st'〉 ← eval_step … ge st s ;
+   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
    ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    eval_step_flow … ge st' nxtptr flow
  | final s ⇒
-   let ret ≝ joint_if_result … curr_fn in
-   ! st' ← eval_fin_step_no_pc … ge ret st s ;
-   ! flow ← eval_fin_step_pc … ge ret st s ;
+   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
+   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
    eval_fin_step_flow … ge st' (pc … st) flow
  ].