Changeset 2217 for src

Timestamp:

Jul 19, 2012, 6:13:54 PM (8 years ago)

Author:

tranquil

Message:

• collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
• completed update of RTL, LTL and LIN semantics

Location:

src

Files:

• ERTL/ERTL_paolo.ma (modified) (2 diffs)
• LIN/joint_LTL_LIN_paolo.ma (modified) (2 diffs)
• LIN/joint_LTL_LIN_semantics_paolo.ma (added)
• LIN/semantics_paolo.ma (added)
• LTL/semantics_paolo.ma (added)
• RTL/RTLToERTL_paolo.ma (modified) (4 diffs)
• RTL/RTL_paolo.ma (modified) (4 diffs)
• RTL/semantics_paolo.ma (modified) (8 diffs)
• RTLabs/RTLabsToRTL_paolo.ma (modified) (6 diffs)
• joint/Joint_paolo.ma (modified) (9 diffs)
• joint/TranslateUtils_paolo.ma (modified) (3 diffs)
• joint/semantics_paolo.ma (modified) (11 diffs)

src/ERTL/ERTL_paolo.ma

@@ -25 +25 @@
   | ertl_frame_size: register → ertl_seq.
 
-definition ertl_uns_params ≝ mk_unserialized_params
-  (mk_step_params
+definition ERTL_uns ≝ mk_unserialized_params
     (* acc_a_reg ≝ *) register
     (* acc_b_reg ≝ *) register
@@ -42 +41 @@
     (* ext_call ≝ *) void
     (* ext_tailcall ≝ *) void
-  )
-  (mk_local_params
-    (mk_funct_params
-      (* resultT ≝ *) unit
-      (* paramsT ≝ *) ℕ)
-      (* localsT ≝ *) register).
+    (* paramsT ≝ *) ℕ
+    (* localsT ≝ *) register.
 
-definition ERTL ≝ mk_graph_params ertl_uns_params.
+definition ERTL ≝ mk_graph_params ERTL_uns.
 definition ertl_program ≝ joint_program ERTL.
 

src/LIN/joint_LTL_LIN_paolo.ma

@@ -13 +13 @@
 
 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
-  (mk_step_params
     (* acc_a_reg ≝ *) unit
     (* acc_b_reg ≝ *) unit
@@ -29 +28 @@
     (* ext_call ≝ *) void
     (* ext_tailcall ≝ *) void
-  )
-  (mk_local_params
-    (mk_funct_params
-      (* resultT ≝ *) unit
-      (* paramsT ≝ *) unit)
-      (* localsT ≝ *) void).
+    (* paramsT ≝ *) unit
+    (* localsT ≝ *) void.
 
 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).

src/RTL/RTLToERTL_paolo.ma

@@ -6 +6 @@
 
 include alias "basics/lists/list.ma".
+
+definition ertl_fresh_reg: 
+ ∀globals.freshT ERTL globals register ≝
+  λglobals,def.
+    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
+    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
 
 definition save_hdws :
@@ -101 +107 @@
 definition allocate_regs :
   ∀globals,rs.rs_set rs →
-  state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
+  freshT ERTL globals (list (register×Register)) ≝
   λglobals,rs,saved,def.
    let allocate_regs_internal ≝
     λr: Register.
     λdef_sregs.
-    let 〈def, r'〉 ≝ rtl_ertl_fresh_reg … (\fst def_sregs) in
+    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
     〈def, 〈r', r〉::\snd def_sregs〉 in
   rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
@@ -118 +124 @@
   let end_lbl ≝ joint_if_exit … def in
   state_run … def (
-    ! sral ← rtl_ertl_fresh_reg … ;
-    ! srah ← rtl_ertl_fresh_reg … ;
+    ! sral ← ertl_fresh_reg … ;
+    ! srah ← ertl_fresh_reg … ;
     ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
-    ! prologue' ← bcompile … (rtl_ertl_fresh_reg …) (prologue … params sral srah sregs) ;
+    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
     let epilogue' ≝ epilogue … ret_regs sral srah sregs in
     ! def' ← state_get … ;
@@ -258 +264 @@
       graph' entry' exit' in
   let def'' ≝ b_graph_translate …
-    (rtl_ertl_fresh_reg …)
+    (ertl_fresh_reg …)
     def'
     (translate_step globals)

src/RTL/RTL_paolo.ma

@@ -12 +12 @@
 
 definition RTL_uns ≝ mk_unserialized_params
-  (mk_step_params
     (* acc_a_reg ≝ *) register
     (* acc_b_reg ≝ *) register
@@ -28 +27 @@
     (* ext_call ≝ *) rtl_call
     (* ext_tailcall ≝ *) rtl_tailcall
-  )
-  (mk_local_params
-    (mk_funct_params
-      (* resultT ≝ *) (list register)
-      (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) register).
+    (* paramsT ≝ *) (list register)
+    (* localsT ≝ *) register.
 
 definition RTL ≝ mk_graph_params RTL_uns.
@@ -98 +93 @@
 
 definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
-  (mk_step_params
     (* acc_a_reg ≝ *) register
     (* acc_b_reg ≝ *) register
@@ -114 +108 @@
     (* ext_call ≝ *) rtl_call
     (* ext_tailcall ≝ *) void
-  )
-  (mk_local_params
-    (mk_funct_params
-      (* resultT ≝ *) (list register)
-      (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) register)).
+    (* paramsT ≝ *) (list register)
+    (* localsT ≝ *) register).
 
 definition rtl_ntc_program ≝ joint_program RTL_ntc.

src/RTL/semantics_paolo.ma

@@ -6 +6 @@
 record frame: Type[0] ≝
  { fr_ret_regs: list register
- ; fr_pc: address
- ; fr_sp: pointer
+ ; fr_pc: cpointer
+ ; fr_sp: xpointer
  ; fr_carry: beval
  ; fr_regs: register_env beval
  }.
 
-definition rtl_sem_state_params : sem_state_params ≝
+definition RTL_state : sem_state_params ≝
   mk_sem_state_params
     (list frame)
@@ -19 +19 @@
     (λ_.empty_map …).
 
-definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : rtl_argument.
+definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
   match a with
   [ Reg r ⇒ reg_retrieve env r
-  | Imm b ⇒ return (BVByte b)
+  | Imm b ⇒ return b
   ].
 
@@ -30 +30 @@
 
 definition rtl_fetch_ra:
- state rtl_sem_state_params → res ((state rtl_sem_state_params) × address) ≝
+ state RTL_state → res ((state RTL_state) × cpointer) ≝
  λst.
   match st_frms ? st with
@@ -36 +36 @@
   | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
 
-definition rtl_init_locals :
- list register → register_env beval → register_env beval ≝
- λlocals,env.
-  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
-
+definition rtl_init_local :
+ register → register_env beval → register_env beval ≝
+ λlocal,env.add … env local BVundef.
 
 definition rtl_setup_call:
- nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
+ nat → list register → list psd_argument → state RTL_state → res (state RTL_state) ≝
   λstacksize,formal_arg_regs,actual_arg_regs,st.
   let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
@@ -53 +51 @@
     (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
   OK …
-   (set_regs rtl_sem_state_params new_regs
+   (set_regs RTL_state new_regs
     (set_m … mem
-     (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
+     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
 cases b * #r #off #E >E %
 qed.
 
-definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
+definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state.
   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
-  set_frms rtl_sem_state_params frame st.  
+  OK … (set_frms RTL_state frame st).
 
 (*CSC: XXXX, for external functions only*)
-axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val).
-axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
-
-definition rtl_msu_params :
-  more_sem_unserialized_params rtl_uns_params ≝
- mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
-    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_locals
-    rtl_save_frame
-    rtl_setup_call
-    rtl_fetch_external_args
-    rtl_set_result
-    [ ] [ ] (*dummy*).
-
-(* alias *)
-definition rtl_reg_store : register→beval→state rtl_sem_state_params→
-    res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
-definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
-    acca_retrieve ? rtl_msu_params.
+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).
+
+definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
+definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
 
 definition rtl_read_result :
- ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
- λglobals,ge,st.
-  ! p ← code_pointer_of_address (pc … st) ;
-  ! fn ← fetch_function … ge p ;
-  m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).
+ ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝
+ λglobals,ge,rets,st.
+ m_list_map … (rtl_reg_retrieve st) rets.
 
 (*CSC: we could use a dependent type here: the list of return values should have
@@ -103 +77 @@
   saves the OutOfBounds exception *)
 definition rtl_pop_frame:
- ∀globals. genv globals rtl_params → state rtl_sem_state_params →
-  res (state rtl_sem_state_params) ≝
- λglobals,ge,st.
-  do ret_vals ← rtl_read_result … ge st ;
+ ∀globals. genv RTL globals → list register → state RTL_state →
+  res (state RTL_state) ≝
+ λglobals,ge,ret,st.
+  do ret_vals ← rtl_read_result … ge ret st ;
   match st_frms ? st with
   [ nil ⇒ Error ? [MSG EmptyStack]
@@ -117 +91 @@
        (OK … st) (fr_ret_regs hd) ;
      OK …
-      (set_frms rtl_sem_state_params tl
-        (set_regs rtl_sem_state_params (fr_regs hd)
+      (set_frms RTL_state tl
+        (set_regs RTL_state (fr_regs hd)
          (set_sp … (fr_sp hd)
           (set_carry … (fr_carry hd)
            (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
 
-
 (* This code is quite similar to eval_call_block: can we factorize it out? *)
-definition eval_tail_call_block:
- ∀globals.genv globals rtl_params → state rtl_sem_state_params →
-  block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
- λglobals,ge,st,b,args.
-  ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
-  match next with
-  [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
-    ! 〈st,ra〉 ← fetch_ra … st ;
-    ! st ← rtl_pop_frame … ge st;
-    return 〈tr,st〉
-  | Some lbl ⇒
-    return 〈tr,st〉
-  ].
-
-definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
+definition eval_tailcall_block:
+ ∀globals.genv RTL globals → state 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)) ≝
+ λglobals,ge,st,b,args,ret.
+  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
+    match fd with
+    [ Internal fd ⇒
+      return 〈FTailInit ?? (block_id b) fd args, st〉
+    | External fn ⇒
+      ! params ← rtl_fetch_external_args … fn st : IO ???;
+      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
+      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
+      (* CSC: XXX bug here; I think I should split it into Byte-long
+         components; instead I am making a singleton out of it. To be
+         fixed once we fully implement external functions. *)
+      let vs ≝ [mk_val ? evres] in
+      ! st ← rtl_set_result … vs ret st : IO ???;
+      return 〈FEnd2 ??, st〉
+    ].
+
+definition block_of_register_pair: register → register → state RTL_state → res block ≝
  λr1,r2,st.
  do v1 ← rtl_reg_retrieve st r1 ;
@@ -146 +129 @@
  OK … (pblock ptr).  
 
-definition rtl_exec_extended:
- ∀globals. genv globals rtl_params →
-  rtl_instruction_extension → state rtl_sem_state_params → address →
-   IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
- λglobals,ge,stm,st,next_addr.
+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.
   match stm with
-   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
+   [ rtl_stack_address dreg1 dreg2  ⇒
       let sp ≝ sp ? st in
       ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
       ! st ← rtl_reg_store dreg1 dpl st ;
-      ! st ← rtl_reg_store dreg2 dph st ;
-      return 〈None label,E0, st〉
-   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
-     ! b ← block_of_register_pair r1 r2 st : IO ???;
-     eval_call_block_preamble ? rtl_params rtl_msu_params
-                              ge st b args (Some ? 〈dest,next_addr〉) ].
-
-definition rtl_exec_fin_extended:
- ∀globals. genv globals rtl_params →
-  rtl_statement_extension → state rtl_sem_state_params →
-   IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
-   λglobals,ge,stm,st.
+      rtl_reg_store dreg2 dph st
+   ].
+
+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)) ≝
+ λglobals,ge,stm,st.
+  match stm with
+  [ rtl_call_ptr r1 r2 args dest ⇒
+    ! b ← block_of_register_pair r1 r2 st : IO ???;
+    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
+    match fd with
+    [ Internal fd ⇒
+      return 〈Init ?? (block_id b) fd args dest, st〉
+    | External fn ⇒
+      ! params ← rtl_fetch_external_args … fn st : IO ???;
+      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
+      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
+      (* CSC: XXX bug here; I think I should split it into Byte-long
+         components; instead I am making a singleton out of it. To be
+         fixed once we fully implement external functions. *)
+      let vs ≝ [mk_val ? evres] in
+      ! st ← rtl_set_result … vs dest st : IO ???;
+      return 〈Proceed ???, st〉
+    ]
+  ].
+
+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.
    match stm with
-   [ rtl_st_ext_tailcall_id id args ⇒
+   [ rtl_tailcall_id id args ⇒
       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
-      eval_tail_call_block … ge st b args
-   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
+      eval_tailcall_block … ge st b args ret
+   | rtl_tailcall_ptr r1 r2 args ⇒
       ! b ← block_of_register_pair r1 r2 st : IO ???;
-      eval_tail_call_block … ge st b args
+      eval_tailcall_block … ge st b args ret
    ].
 
-definition rtl_msg_params : more_sem_genv_params rtl_params ≝
-  mk_more_sem_genv_params rtl_params rtl_msu_params
+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
-    rtl_exec_extended
-    rtl_exec_fin_extended
-    rtl_pop_frame.
-
-
-
-definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
-
-definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
+    eval_rtl_seq
+    eval_rtl_tailcall
+    eval_rtl_call.

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -8 +8 @@
 include alias "ASM/BitVector.ma".
 include alias "arithmetics/nat.ma".
+
+definition rtl_fresh_reg: 
+ ∀globals.freshT RTL globals register ≝
+  λglobals,def.
+    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
+    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
+
+definition rtl_fresh_reg_no_local : 
+ ∀globals.freshT RTL globals register ≝
+  λglobals,def.
+    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
+    〈set_runiverse ?? def runiverse, r〉.
+
 definition size_of_sig_type ≝
   λsig.
@@ -48 +61 @@
   λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
 
-definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
-λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.
-
-let rec register_freshes (n: nat) on n :
-  state_monad (universe RegisterTag) (Σl.|l| = n) ≝
-  match n return λx.state_monad ? (Σl.|l| = x) with
-  [ O ⇒ return «[ ],?»
-  | S n' ⇒
-    ! r ← m_fresh ?;
-    ! res ← register_freshes n';
-    return «r::res,?»
-  ].[2: cases res -res #res #EQ <EQ] % qed.
-
 definition initialize_local_env_internal :
-  (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝
-  λlenv_runiverse,r_sig.
-  let 〈runiverse,lenv〉 ≝ lenv_runiverse in
+  ∀globals.
+  ((joint_internal_function RTL globals) × local_env) → (register×typ) →
+  ((joint_internal_function RTL globals) × local_env) ≝
+  λglobals,def_env,r_sig.
+  let 〈def,lenv〉 ≝ def_env in
   let 〈r, sig〉 ≝ r_sig in
   let size ≝ size_of_sig_type sig in
-  let 〈runiverse,rs〉 ≝ register_freshes size runiverse in
-    〈runiverse,add … lenv r rs〉.
-
-definition initialize_local_env :
-  list (register×typ) →
-  state_monad (universe RegisterTag) local_env ≝
-  λregisters,runiverse.
-  foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers.
+  let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in
+    〈def,add … lenv r rs〉.
 
 include alias "common/Identifiers.ma".
@@ -84 +80 @@
   | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
   ].cases prf #A #B assumption qed.
+
+definition initialize_local_env :
+  ∀globals.
+  list (register×typ) →
+  freshT RTL globals local_env ≝
+  λglobals,registers,def.
+  foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers.
+
+lemma initialize_local_env_in : ∀globals,l,def,r.
+  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
+#globals #l #U #r @(list_elim_left … l)
+[ *
+| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
+  whd in match initialize_local_env; normalize nodelta
+  >foldl_step change with (initialize_local_env ???) in match (foldl ?????);
+  [ #H lapply (IH H)
+  | * [2: *] #EQ destruct(EQ)
+  ]  
+  cases (initialize_local_env ???)
+  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
+  elim (repeat_fresh ??????) #U'' #rs
+  [ >mem_set_add @orb_Prop_r assumption
+  | @mem_set_add_id
+  ]
+qed.
+
+example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
+// qed-.
+example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
+// qed-.
+
+definition initialize_locals_params_ret :
+  ∀globals.
+  (* locals *) list (register×typ) →
+  (* params *) list (register×typ) →
+  (* return *) option (register×typ) →
+  freshT RTL globals local_env ≝
+  λglobals,locals,params,ret,def.
+  let 〈def',lenv〉 as EQ ≝
+    initialize_local_env globals
+    ((match ret with
+     [ Some r_sig ⇒ [r_sig]
+     | None ⇒ [ ]
+     ]) @ locals @ params) def in
+  let locals' ≝ map_list_local_env lenv locals ? in
+  let params' ≝ map_list_local_env lenv params ? in
+  let ret' ≝ match ret return λx.ret = x → ? with
+    [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ?
+    | None ⇒ λ_.[ ]
+    ] (refl …) in
+  let def'' ≝
+    mk_joint_internal_function RTL globals
+      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
+      params' locals' (joint_if_stacksize … def')
+      (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in
+   〈def'', lenv〉. @hide_prf
+[ >(proj2_rewrite ????? EQ)
+  @initialize_local_env_in >prf %1 %
+|*: >(proj2_rewrite ????? EQ)
+  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
+  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
+    [ #a #H @Exists_append_r @Exists_append_r @H
+    | generalize in match params;
+    ]
+  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals))
+    [ #a #H @Exists_append_r @Exists_append_l @H
+    | generalize in match locals;
+    ]
+  ]
+  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
+]
+qed.
 
 definition make_addr ≝
@@ -834 +902 @@
 qed.
 
-lemma initialize_local_env_in : ∀l,runiverse,r.
-  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).
-#l #U #r @(list_elim_left … l)
-[ *
-| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
-  whd in match initialize_local_env; normalize nodelta
-  >foldl_step change with (initialize_local_env ??) in match (foldl ?????);
-  [ #H lapply (IH H)
-  | * [2: *] #EQ destruct(EQ)
-  ]  
-  cases (initialize_local_env ??)
-  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
-  elim (register_freshes ??) #U'' #rs
-  [ >mem_set_add @orb_Prop_r assumption
-  | @mem_set_add_id
-  ]
-qed.
-
-definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
-// qed.
-definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
-// qed.
-
-
 (* XXX: we use a "hack" here to circumvent the proof obligations required to
    create res, an empty internal_function record.  we insert into our graph
@@ -865 +909 @@
   λglobals: list ident.
   λdef.
-  let runiverse ≝ f_reggen def in
-  let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env
-    (match f_result def with [ None ⇒ [ ] | Some r_sig ⇒ [r_sig]] @
-     f_params def @ f_locals def) runiverse in
-  let params' ≝ map_list_local_env lenv (f_params def) ? in
-  let locals' ≝ map_list_local_env lenv (f_locals def) ? in
-  let result' ≝
-    match (f_result def) return λx.f_result def = x → ? with
-    [ None ⇒ λ_.[ ]
-    | Some r_typ ⇒ λEQ.
-       find_local_env (\fst r_typ) lenv ?
-    ] (refl …)
-  in
+  let runiverse' ≝ f_reggen def in
   let luniverse' ≝ f_labgen def in
   let stack_size' ≝ f_stacksize def in
@@ -887 +919 @@
   let graph' ≝ add LabelTag ? graph' exit'
     (RETURN …) in
+  let init ≝
+    mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ]
+     [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in
+  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
+    (f_locals def) (f_params def) (f_result def) init in
   let f_trans ≝ λlbl,stmt,def.
     let pr ≝ translate_statement … lenv stmt in
-    b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
-  let res ≝
-    mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
-     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
-    foldi … f_trans (f_graph def) res.  
-    
-[1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
-| >(proj2_rewrite ????? pr_eq)
-  @initialize_local_env_in >EQ normalize nodelta %1 %
-|*: >(proj2_rewrite ????? pr_eq)
-  @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr)))
-  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def)))
-    [ #a #H @Exists_append_r @Exists_append_r @H
-    | generalize in match (f_locals def);
-    ]
-  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def)))
-    [ #a #H @Exists_append_r @Exists_append_l @H
-    | generalize in match (f_params def);
-    ]
-  ]
-  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
-]
+    b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
+  foldi … f_trans (f_graph def) init'.
+@hide_prf
+>graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
 qed.
 

src/joint/Joint_paolo.ma

@@ -24 +24 @@
               |       |    /    
           unserialized_params             
-            |            \       
-            |             \      
-            |         local_params
-            |              |    
-    step_params       funct_params
-
-step_params : types needed to define steps (stmts with a default fallthrough)
+
+unserialized_params : things unrelated to serialization (i.e. graph or linear
+                      form)
 stmt_params : adds successor type needed to define statements
 funct_params : types of result register and parameters of function
-local_params : adds types of local registers
 params : adds type of code and related properties *)
 
@@ -75 +70 @@
 definition zero_byte : Byte ≝ bv_zero 8.
 
-record step_params : Type[1] ≝ 
+record unserialized_params : Type[1] ≝ 
  { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
  ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
@@ -95 +90 @@
  ; ext_tailcall : Type[0]
  (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
+ ; paramsT : Type[0]
+ ; localsT: Type[0]
  }.
 
-inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
+inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
   | COMMENT: String → joint_seq p globals
   | COST_LABEL: costlabel → joint_seq p globals
@@ -145 +142 @@
   extension_branch on _s : ext_branch ? to joint_branch ?.*)
 
-inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
+inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
   | step_seq : joint_seq p globals → joint_step p globals
   | COND: acc_a_reg p → label → joint_step p globals.
@@ -170 +167 @@
     ].
 
-definition step_forall_labels : ∀p : step_params.∀globals.
+definition step_forall_labels : ∀p.∀globals.
     (label → Prop) → joint_step p globals → Prop ≝
 λp,g,P,inst. All … P (step_labels … inst).
 
 definition step_classifier :
-  ∀p : step_params.∀globals.
+  ∀p.∀globals.
     joint_step p globals → status_class ≝ λp,g,s.
   match s with
@@ -187 +184 @@
   ].
 
-record funct_params : Type[1] ≝
-  { resultT : Type[0]
-  ; paramsT : Type[0]
-  }.
-  
-record local_params : Type[1] ≝
- { funct_pars :> funct_params
- ; localsT: Type[0]
- }.
-
-record unserialized_params : Type[1] ≝
- { u_inst_pars :> step_params
- ; u_local_pars :> local_params
- }.
-
 record stmt_params : Type[1] ≝
   { uns_pars :> unserialized_params
@@ -208 +190 @@
   }. 
 
-inductive joint_fin_step (p: step_params): Type[0] ≝
+inductive joint_fin_step (p: unserialized_params): Type[0] ≝
   | GOTO: label → joint_fin_step p
   | RETURN: joint_fin_step p
@@ -468 +450 @@
     forall_statements_i … (statement_closed … code) code.
 
-(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
-definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
-  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
-
 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
 { joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
@@ -478 +456 @@
      following, right? *)
 (*  joint_if_sig: signature;  -- dropped in front end *)
-  joint_if_result   : resultT p;
+  joint_if_result   : call_dest p;
   joint_if_params   : paramsT p;
   joint_if_locals   : list (localsT p); (* use void where no locals are present *)

src/joint/TranslateUtils_paolo.ma

@@ -1 +1 @@
 include "joint/Joint_paolo.ma".
 include "joint/blocks.ma".
+include "utilities/hide.ma".
 
 (* general type of functions generating fresh things *)
-(* type T is the syntactic type of the generated things *)
-(* (sig for RTLabs registers, unit in others ) *)
-definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
-
-definition rtl_ertl_fresh_reg: 
- ∀inst_pars,funct_pars,globals.
-  freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
-  λinst_pars,var_pars,globals,def.
-    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
-    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
+definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
 
 include alias "basics/lists/list.ma".
-let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
-  freshT globals (rtl_ertl_params inst_pars funct_pars)
-    (Σl : list register. |l| = n) ≝
-  let ret_type ≝ (Σl : list register. |l| = n) in
-  match n  return λx.x = n → freshT … ret_type with
-  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
-  | S n' ⇒ λeq'.
-    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
-    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
-    return (mk_Sig … (reg :: regs') ?)
-  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
-  qed.
+let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
+  on n :
+  freshT pars globals (Σl : list A. |l| = n) ≝
+  match n  return λx.freshT … (Σl.|l| = x) with
+  [ O ⇒ return «[ ], ?»
+  | S n' ⇒
+    ! regs' ← repeat_fresh … fresh n';
+    ! reg ← fresh ;
+    return «reg::regs',?»
+  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
 
 definition fresh_label:
@@ -126 +116 @@
   ∀globals: list ident.
   (* fresh register creation *)
-  freshT globals g_pars (localsT … g_pars) →
+  freshT g_pars globals (localsT … g_pars) →
   ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
        bind_seq_block g_pars globals (joint_fin_step g_pars).
@@ -147 +137 @@
   ∀globals: list ident.
   (* fresh register creation *)
-  freshT globals dst_g_pars (localsT dst_g_pars) →
+  freshT dst_g_pars globals (localsT dst_g_pars) →
   (* initialized function definition with empty graph *)
   joint_internal_function dst_g_pars globals →

src/joint/semantics_paolo.ma

@@ -86 +86 @@
  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
 
-inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
+inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
   | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
   | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
   | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
 
-inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
+inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
   | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
   | FTailInit : Z → F → call_args p → fin_step_flow p F Call
@@ -126 +126 @@
   ; fetch_external_args: external_function → state st_pars →
       res (list val)
-  ; set_result: list val → state st_pars → res (state st_pars)
+  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
   ; call_args_for_main: call_args uns_pars
   ; call_dest_for_main: call_dest uns_pars
 
   (* from now on, parameters that use the type of functions *)
-  ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)
+  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (list beval)
   (* 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)
   ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
-      state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_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 →
       IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
-  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)
+  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars)
   }.
 
@@ -206 +206 @@
          fixed once we fully implement external functions. *)
       let vs ≝ [mk_val ? evres] in
-      ! st ← set_result … p' vs st : IO ???;
+      ! st ← set_result … p' vs dest st : IO ???;
       return 〈Proceed ???, st〉
       ].
@@ -326 +326 @@
 
 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv p globals → cpointer → res (joint_statement p globals) ≝
+  genv p globals → cpointer →
+  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
   λp,msp,globals,ge,ptr.
   let pt ≝ point_of_pointer ? msp ptr in
   ! fn ← fetch_function … ge ptr ;
-  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
+  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
+  return 〈fn, stmt〉.
   
 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
@@ -517 +519 @@
 
 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
-  state p → ∀s : joint_fin_step p.
+  (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
   IO io_out io_in (state p) ≝
- λglobals,p,ge,st,s.
+ λglobals,p,ge,ret,st,s.
   match s return λx.IO ??? with
     [ tailcall c ⇒
-      !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
+      !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
       return st'
     | _ ⇒ return st
@@ -528 +530 @@
 
 definition eval_fin_step_pc :
- ∀globals.∀p:sem_params. genv p globals → state p →
+ ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
   ∀s:joint_fin_step p.
   IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
-  λg,p,ge,st,s.
+  λg,p,ge,ret,st,s.
   match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
   [ tailcall c ⇒
-    !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
+    !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
     return flow  
   | GOTO l ⇒ return FRedirect … l
@@ -577 +579 @@
   | _ ⇒
     ! 〈st',ra〉 ← fetch_ra … st ;
-    ! st'' ← pop_frame … ge st;
+    ! fn ← fetch_function … ge curr ;
+    ! st'' ← pop_frame … ge (joint_if_result … fn) st';
     return mk_state_pc ? st'' ra
   ].
@@ -583 +586 @@
 definition eval_statement :
  ∀globals.∀p:sem_params.genv p globals →
-  state_pc p → joint_statement p globals →
+  state_pc p → joint_internal_function p globals → joint_statement p globals →
     IO io_out io_in (state_pc p) ≝
- λglobals,p,ge,st,stmt.
+ λglobals,p,ge,st,curr_fn,stmt.
  match stmt with
  [ sequential s nxt ⇒
@@ -592 +595 @@
    eval_step_flow … ge st' nxtptr flow
  | final s ⇒
-   ! st' ← eval_fin_step_no_pc … ge st s ;
-   ! flow ← eval_fin_step_pc … ge st 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 ;
    eval_fin_step_flow … ge st' (pc … st) flow
  ].
@@ -600 +604 @@
   state_pc p → IO io_out io_in (state_pc p) ≝
   λglobals,p,ge,st.
-  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
-  eval_statement … ge st s.
+  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
+  eval_statement … ge st fn s.
 
 (* Paolo: what if in an intermediate language main finishes with an external
@@ -609 +613 @@
   genv p globals → cpointer → state_pc p → option int ≝
  λglobals,p,ge,exit,st.res_to_opt ? (
-  do s ← fetch_statement ? p … ge (pc … st);
+  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
   match s with
   [ final s' ⇒
     match s' with
     [ RETURN ⇒ 
-      do 〈st,ra〉 ← fetch_ra … st; 
+      do 〈st',ra〉 ← fetch_ra … st;
       if eq_pointer ra exit then 
-       do vals ← read_result … ge st ;
+       do vals ← read_result … ge (joint_if_result … fn) st' ;
        Word_of_list_beval vals
       else