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

    r2783 r2946  
    4040definition RTL ≝ mk_graph_params (mk_uns_params RTL_uns RTL_functs).
    4141definition rtl_program ≝ joint_program RTL.
     42unification hint 0 ≔ ⊢ rtl_program ≡ joint_program RTL.
    4243
    4344interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
     
    9091coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
    9192  on _b : Byte to snd_arg RTL.
     93
     94(* parameters for main need to be passed to the premain *)
     95definition RTL_premain : ∀p : rtl_program.joint_closed_internal_function RTL (prog_var_names ?? p) ≝
     96λp.
     97let l1 : label ≝ an_identifier … one in
     98let l2 : label ≝ an_identifier … (p0 one) in
     99let l3 : label ≝ an_identifier … (p1 one) in
     100let rs : list register ≝
     101  [ an_identifier … one ;
     102    an_identifier … (p0 one) ;
     103    an_identifier … (p1 one) ;
     104    an_identifier … (p0 (p0 one)) ] in
     105let res ≝
     106  mk_joint_internal_function RTL (prog_var_names … p)
     107  (mk_universe … (p0 (p0 one)))
     108  (mk_universe … (p1 (p0 one)))
     109  [ ] rs 0 0 (empty_map …) l1 in
     110(* todo: args for main? *)
     111let res ≝ add_graph … l1
     112  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     113  res in
     114let res ≝ add_graph … l2
     115  (sequential … (CALL RTL ? (inl … (prog_main … p)) (map … (Reg ?) rs) rs) l3)
     116  res in
     117let res ≝ add_graph … l3
     118  (GOTO ? l3)
     119  res in
     120res.
     121%
     122[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     123  %
     124  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     125  |2: %
     126  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     127  ]
     128| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     129| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     130| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct try @I
     131  % try % try % try % try % try % try % try % try %
     132  whd whd in ⊢ (?%%); /2 by double_lt3/
     133| %{l2} %{(init_cost_label … p)} %
     134]
     135qed.
Note: See TracChangeset for help on using the changeset viewer.