Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_fullexec.ma

    r2821 r2946  
    2020let p ≝ \fst p_stack in
    2121let stack_sizes ≝ \snd p_stack in
    22 let genv ≝ globalenv_noinit ? p in
    23 let get_pc_lbl ≝ λid,lbl.
    24   ! bl ← block_of_funct_id … pars genv id ;
    25   pc_of_label … genv bl lbl in
     22let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
    2623mk_joint_global pars
    27   (prog_var_names ?? p)
    28   (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl).
    29  (* (prog_io pars) *).
    30 #s #H
    31 elim (find_symbol_exists … p s ?)
    32 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
    33 @Exists_append_r
    34 @(Exists_mp … H) //
    35 qed.
     24  (globals … ev_pars)
     25  (ev_genv … ev_pars).
    3626
    3727definition joint_exec: sem_params → trans_system io_out io_in ≝
    3828  λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
    39    (λenv.is_final G (jglobals … env) env exit_pc)
     29   (λenv.joint_final G (jglobals … env) env)
    4030   (λenv.λst.! st' ← eval_state … env st ;
    4131    let charge ≝ match joint_label_of_pc env (pc … st) with
     
    4939    (make_joint_global G)
    5040    (λp_stacks.
    51       make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     41      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    5242
    5343definition joint_preclassified_system : sem_params →
Note: See TracChangeset for help on using the changeset viewer.