Changeset 2946 for src/compiler.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/compiler.ma

    r2936 r2946  
    9393
    9494definition back_end :
    95  observe_pass → RTLabs_program →
     95 observe_pass → costlabel → RTLabs_program →
    9696  res (pseudo_assembly_program × stack_cost_model × nat) ≝
    97 λobserve,p.
    98   let p ≝ rtlabs_to_rtl p in
     97λobserve,init_cost,p.
     98  let p ≝ rtlabs_to_rtl init_cost p in
    9999  let st ≝ lookup_stack_cost … p in
    100100  let i ≝ observe rtl_separate_pass 〈p,st〉 in
     
    156156λobserve,p.
    157157  ! 〈init_cost,p',p〉 ← front_end observe p;
    158   ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
     158  ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p;
    159159  ! p ← assembler observe p;
    160160  let k ≝ ASM_cost_map p in
Note: See TracChangeset for help on using the changeset viewer.