Changeset 2286 for src/RTL/semantics.ma

Timestamp:

Aug 2, 2012, 3:18:11 PM (8 years ago)

Author:

tranquil

Message:

Big update!

• merge of all _paolo variants
• reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
• split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:

• src/RTL/semantics.ma (modified) (4 diffs)

src/RTL/semantics.ma

@@ -6 +6 @@
 record frame: Type[0] ≝
  { fr_ret_regs: list register
- ; fr_pc: address
- ; fr_sp: pointer
- ; fr_carry: beval
+ ; fr_pc: cpointer
+ ; fr_sp: xpointer
+ ; fr_carry: bebit
  ; fr_regs: register_env beval
  }.
 
-definition rtl_more_sem_params: more_sem_params rtl_params_ :=
- mk_more_sem_params rtl_params_
-  (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*)
-   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
-    reg_store reg_retrieve reg_store reg_retrieve
-     (λlocals,dest_src.
-       do v ← reg_retrieve locals (\snd dest_src) ;
-       reg_store (\fst dest_src) v locals).
-definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
-
-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_state : sem_state_params ≝
+  mk_sem_state_params
+    (list frame)
+    [ ]
+    (register_env beval)
+    (λ_.empty_map …).
+
+definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
+  match a with
+  [ Reg r ⇒ reg_retrieve env r
+  | Imm b ⇒ return b
+  ].
 
 (*CSC: could we use here a dependent type to avoid the Error case? *)
@@ -32 +30 @@
 
 definition rtl_fetch_ra:
- state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
+ RTL_state → res (RTL_state × cpointer) ≝
  λst.
   match st_frms ? st with
@@ -38 +36 @@
   | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
 
-definition rtl_result_regs:
- ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
- λglobals,ge,st.
-  do fn ← graph_fetch_function … globals ge st ;
-  OK … (joint_if_result … fn).
-
-(*CSC: we could use a dependent type here: the list of return values should have
-  the same length of the list of return registers that store the values. This
-  saves the OutOfBounds exception *)
-definition rtl_pop_frame:
- ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
- λglobals,ge,st.
-  do ret_regs ← rtl_result_regs … ge st ;
-  do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
-  match st_frms ? st with
-  [ nil ⇒ Error ? [MSG EmptyStack]
-  | cons hd tl ⇒
-     do st ←
-      mfold_left_i ??
-       (λi.λst.λreg.
-         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
-         greg_store rtl_sem_params reg v st)
-       (OK … st) (fr_ret_regs hd) ;
-     OK …
-      (set_frms rtl_sem_params tl
-        (set_regs rtl_sem_params (fr_regs hd)
-         (set_sp … (fr_sp hd)
-          (set_carry … (fr_carry hd)
-           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
-
-definition rtl_call_function:
- nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
+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 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
@@ -75 +47 @@
    mfold_left2 …
     (λlenv,dest,src.
-      do v ← greg_retrieve … st src ;
+      do v ← rtl_arg_retrieve … (regs ? st) src ;
       OK … (add … lenv dest v))
     (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
   OK …
-   (set_regs rtl_sem_params new_regs
+   (set_regs RTL_state new_regs
     (set_m … mem
-     (set_sp … (mk_pointer b (mk_offset 0)) st))).
-(*cases b * #r #off #E >E %
-qed.*)
-
-definition rtl_save_frame:
- address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
- λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
-  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
-  let st ≝ set_frms rtl_sem_params frame st in
-  rtl_call_function stacksize formal_arg_regs actual_arg_regs 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 : 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_sem_params → res (list val).
-axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
-
-definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
- λglobals.
-  mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
-   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
-   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
-   rtl_fetch_external_args rtl_set_result.
-definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
- λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
-
-definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
- λr1,r2,st.
- do v1 ← greg_retrieve rtl_sem_params st r1 ;
- do v2 ← greg_retrieve rtl_sem_params st r2 ;
- do ptr ← pointer_of_address 〈v1,v2〉 ;
- OK … (pblock ptr).  
+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.
+definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
+
+definition rtl_read_result :
+ ∀globals.genv RTL globals → list register → 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
+  the same length of the list of return registers that store the values. This
+  saves the OutOfBounds exception *)
+definition rtl_pop_frame:
+ ∀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
+  [ nil ⇒ Error ? [MSG EmptyStack]
+  | cons hd tl ⇒
+     do st ←
+      mfold_left_i …
+       (λi.λst.λreg.
+         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
+         rtl_reg_store reg v st)
+       (OK … st) (fr_ret_regs hd) ;
+     OK …
+      (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 … (rtl_params globals) → state rtl_sem_params →
-  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
- λglobals,ge,st,b,args.
-  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b);
+definition eval_tailcall_block:
+ ∀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)×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 fn ⇒
-      let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
-      ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
-      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
-      let l' ≝ joint_if_entry … fn in
-      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
-       return 〈 E0, st〉
-    | External fn ⇒ ?(*
-      ! params ← fetch_external_args … fn st;
-      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
+    [ 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 ← set_result … vs st;
-      let st ≝ set_pc … ra st in
-        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
-     ].
-cases daemon (*CSC: XXX tailcall to external function not implemented yet;
-                    it needs alls other functions on external calls *)
-qed.
-
-definition rtl_exec_extended:
- ∀globals. genv globals (rtl_params globals) →
-  rtl_statement_extension → label → state rtl_sem_params →
-   IO io_out io_in (trace × (state rtl_sem_params)) ≝
- λglobals,ge,stm,l,st.
+      let vs ≝ [mk_val ? evres] in
+      ! st ← rtl_set_result … vs ret st : IO ???;
+      return 〈FEnd2 ??, st〉
+    ].
+
+definition block_of_register_pair: register → register → RTL_state → res block ≝
+ λr1,r2,st.
+ do v1 ← rtl_reg_retrieve st r1 ;
+ do v2 ← rtl_reg_retrieve st r2 ;
+ do ptr ← pointer_of_address 〈v1,v2〉 ;
+ OK … (pblock ptr).  
+
+definition eval_rtl_seq:
+ ∀globals. genv RTL globals →
+  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_st_ext_stack_address dreg1 dreg2  ⇒
+   [ rtl_stack_address dreg1 dreg2  ⇒
       let sp ≝ sp ? st in
       ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
-      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
-      ! st ← greg_store rtl_sem_params dreg2 dph st ;
-      ! st ← next … (rtl_sem_params1 globals) l st ;
-       return 〈E0, st〉
-   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
-      ! b ← block_of_register_pair r1 r2 st : IO ??? ;
-      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
-      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
-       ge st b args dest ra
-   | rtl_st_ext_tailcall_id id args ⇒
+      ! st ← rtl_reg_store dreg1 dpl st ;
+      rtl_reg_store dreg2 dph st
+   ].
+
+definition eval_rtl_call:
+ ∀globals. genv RTL globals →
+  rtl_call → RTL_state →
+   IO io_out io_in ((step_flow RTL ? Call)×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 → 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 ⇒
       ! 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_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
- λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
-
-definition rtl_fullexec ≝
- joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
+definition RTL_semantics ≝
+  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)).