Changeset 2946 for src/RTLabs


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.

Location:
src/RTLabs
Files:
1 edited
1 moved

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.
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r2868 r2946  
    1616include "common/StatusSimulation.ma".
    1717include "joint/Traces.ma".
    18 include "RTLabs/RTLabs_traces.ma".
     18include "RTLabs/RTLabs_abstract.ma".
    1919include "RTL/RTL_semantics.ma".
    2020
     21(* this is in incomplete RTLabs/MeasurableToStructured.ma *)
     22definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
     23λp.
     24  let ge ≝ make_global p in
     25  do m ← init_mem … (λx.[Init_space x]) p;
     26  let main ≝ prog_main ?? p in
     27  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
     28  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
     29  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
     30  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
     31% [ @Ef | % ]
     32qed.
     33
     34(* this should say something like λf,p.∀〈i, Internal f〉 ∈ functs p.f i ≥ stacksize f. *)
     35axiom RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop.
     36
    2137axiom RTLabsToRTL_ok :
    22 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
     38∀stacksizes : ident → option ℕ.
    2339∀p_in : RTLabs_program.
     40RTLabsToRTLstacksizes_ok stacksizes p_in →
    2441let p_out ≝ rtlabs_to_rtl p_in in
    2542∃[1] R.
    2643  status_simulation
    2744    (RTLabs_status (make_global … p_in))
    28     (joint_status RTL_semantics p_out stacksizes) R.
     45    (joint_status RTL_semantics_separate p_out stacksizes) R ∧
     46  ∀init_in.make_ext_initial_state p_in = OK … init_in →
     47  ∃init_out : state_pc RTL_semantics_separate.
     48    make_initial_state
     49     (mk_prog_params RTL_semantics_separate p_out stacksizes) =
     50      OK ? init_out ∧
     51   R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.