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/RTLabs/RTLabsToRTL.ma

    r2931 r2946  
    627627νν |destrs| as tmp_destrs with tmp_destrs_prf in
    628628νdummy in
     629(dummy ← byte_of_nat 0) :::
    629630(* the step calculating all products with least significant byte going in the
    630631   k-th position of the result *)
     
    648649translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
    649650@hide_prf
    650 [ >length_map >tmp_destrs_prf //
    651 | >length_append <plus_n_Sm <plus_n_O //
     651[ >length_append  <plus_n_Sm <plus_n_O //
     652| >length_map >tmp_destrs_prf //
    652653]
    653654qed.
     
    10931094(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
    10941095  because of CompCert heritage *)
    1095 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    1096  λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     1096definition rtlabs_to_rtl: (* initialization cost label *) costlabel →
     1097  RTLabs_program → rtl_program ≝
     1098 λinit_cost, p.
     1099  mk_joint_program …
     1100    (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)))
     1101    init_cost.
Note: See TracChangeset for help on using the changeset viewer.