Changeset 2155 for src/RTL

Timestamp:

Jul 6, 2012, 11:25:43 AM (9 years ago)

Author:

tranquil

Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:

• src/RTL/RTL_paolo.ma (modified) (5 diffs)

src/RTL/RTL_paolo.ma

@@ -16 +16 @@
   on _n : nat to rtl_argument.
 
-inductive rtl_step_extension: Type[0] ≝
-  | rtl_st_ext_stack_address: register → register → rtl_step_extension
-  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.
+inductive rtl_seq : Type[0] ≝
+  | rtl_stack_address: register → register → rtl_seq.
+ 
+inductive rtl_call : Type[0] ≝
+  | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
 
-inductive rtl_statement_extension : Type[0] ≝
-  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
-  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
+inductive rtl_tailcall : Type[0] ≝
+  | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
+  | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
 
 definition rtl_uns_params ≝ mk_unserialized_params
@@ -38 +40 @@
     (* call_args ≝ *) (list rtl_argument)
     (* call_dest ≝ *) (list register)
-    (* ext_step ≝ *) rtl_step_extension
-    (* ext_step_labels ≝ *) (λes.[ ])
-    (* ext_fin_stmt ≝ *) rtl_statement_extension
-    (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
+    (* ext_seq ≝ *) rtl_seq
+    (* ext_call ≝ *) rtl_call
+    (* ext_tailcall ≝ *) rtl_tailcall
+  )
   (mk_local_params
     (mk_funct_params
       (* resultT ≝ *) (list register)
       (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) (list register)).
+      (* localsT ≝ *) register).
 
 definition rtl_params ≝ mk_graph_params rtl_uns_params.
@@ -54 +56 @@
 definition rtl_program ≝ joint_program rtl_params.
 definition rtl_step ≝ joint_step rtl_params.
+definition rtl_seq ≝ joint_seq rtl_params.
 definition rtl_statement ≝ joint_statement rtl_params.
-
 
 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
@@ -63 +65 @@
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
+acc_a_reg rtl_params ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
+acc_b_reg rtl_params ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
+acc_a_arg rtl_params ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
+acc_b_arg rtl_params ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
+dpl_reg rtl_params ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
+dph_reg rtl_params ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
+dpl_arg rtl_params ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
+dph_arg rtl_params ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
+snd_arg rtl_params ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
+pair_move rtl_params ≡ register × rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
+call_args rtl_params ≡ list rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
+call_dest rtl_params ≡ list register.
 
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
+ext_seq rtl_params ≡ rtl_seq.
+unification hint 0 ≔
+(*---------------*) ⊢
+ext_call rtl_params ≡ rtl_call.
+unification hint 0 ≔
+(*---------------*) ⊢
+ext_tailcall rtl_params ≡ rtl_tailcall.
 unification hint 0 ≔ globals
 (*---------------*) ⊢
-joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
+joint_step rtl_params globals ≡ rtl_step globals.
 
-unification hint 0 ≔
+unification hint 0 ≔ globals
 (*---------------*) ⊢
-ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
+joint_seq rtl_params globals ≡ rtl_seq globals.
 unification hint 0 ≔ globals
 (*---------------*) ⊢
 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
 
+coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
+  on _r : register to snd_arg rtl_params.
+coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
+  on _b : Byte to snd_arg rtl_params.
+
+
 (************ Same without tail calls ****************)
-
-inductive rtlntc_statement_extension: Type[0] ≝
-  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
-  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
 
 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
@@ -132 +142 @@
     (* call_args ≝ *) (list rtl_argument)
     (* call_dest ≝ *) (list register)
-    (* extend_statements ≝ *) rtlntc_statement_extension
-    (* ext_forall_labels ≝ *) (λes.[ ])
-    void (λes.[ ]))
+    (* ext_seq ≝ *) rtl_seq
+    (* ext_call ≝ *) rtl_call
+    (* ext_tailcall ≝ *) void
+  )
   (mk_local_params
     (mk_funct_params
       (* resultT ≝ *) (list register)
       (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) (list register))).
+      (* localsT ≝ *) register)).
 
 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).