Changeset 2946 for src/joint/Joint.ma


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.ma

    r2865 r2946  
    524524(p : params) (globals : list ident) (def : joint_internal_function p globals)
    525525: Prop ≝
    526 { entry_costed :
    527   ∃l,nxt.
    528         stmt_at … (joint_if_code … def) (joint_if_entry … def) =
    529           Some … (sequential … (COST_LABEL … l) nxt)
    530 ; entry_unused :
     526{ entry_unused :
    531527  let entry ≝ joint_if_entry … def in
    532528  let code ≝ joint_if_code … def in
     
    598594definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    599595
    600 definition joint_program ≝
    601  λp:params. program (joint_function p) nat.
     596record joint_program (p : params) : Type[0] ≝
     597{ joint_prog :> program (joint_function p) (list init_data)
     598; init_cost_label : costlabel
     599(* here we can have global invariants (like injectivity of cost labels) *)
     600}.
    602601
    603602(* The cost model for stack consumption *)
     
    613612   [ ] (prog_funct ?? pr).
    614613
     614include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
    615615definition globals_stacksize : ∀p.joint_program p → nat ≝
    616616 λpars,p.
    617  Σ_{entry ∈ prog_vars … p}(\snd entry).
    618 
     617 Σ_{entry ∈ prog_vars … p}(size_init_data_list … (\snd entry)).
     618
Note: See TracChangeset for help on using the changeset viewer.