Changeset 2946 for src/joint/joint_fullexec.ma

Timestamp:

Mar 24, 2013, 11:29:01 AM (8 years ago)

Author:

tranquil

Message:

main novelties:

• there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
• a premain is added semantically to the global env, so initial cost label and main call and return are observed
• proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:

• src/joint/joint_fullexec.ma (modified) (2 diffs)

src/joint/joint_fullexec.ma

@@ -20 +20 @@
 let p ≝ \fst p_stack in
 let stack_sizes ≝ \snd p_stack in
-let genv ≝ globalenv_noinit ? p in
-let get_pc_lbl ≝ λid,lbl.
-  ! bl ← block_of_funct_id … pars genv id ;
-  pc_of_label … genv bl lbl in
+let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
 mk_joint_global pars
-  (prog_var_names ?? p)
-  (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl).
- (* (prog_io pars) *).
-#s #H
-elim (find_symbol_exists … p s ?)
-[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
-@Exists_append_r
-@(Exists_mp … H) //
-qed.
+  (globals … ev_pars)
+  (ev_genv … ev_pars).
 
 definition joint_exec: sem_params → trans_system io_out io_in ≝
   λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
-   (λenv.is_final G (jglobals … env) env exit_pc)
+   (λenv.joint_final G (jglobals … env) env)
    (λenv.λst.! st' ← eval_state … env st ;
     let charge ≝ match joint_label_of_pc env (pc … st) with
@@ -49 +39 @@
     (make_joint_global G) 
     (λp_stacks.
-      make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
+      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
 
 definition joint_preclassified_system : sem_params →