Changeset 2946 for src/RTL


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/RTL
Files:
2 added
2 edited
1 moved

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.
  • src/RTL/RTLToERTLAxiom.ma

    r2868 r2946  
    1111∃[1] R.
    1212  status_simulation
    13     (joint_status RTL_semantics p_in stacksizes)
     13    (joint_status RTL_semantics_unique p_in stacksizes)
    1414    (joint_status ERTL_semantics p_out stacksizes)
    15     R.
     15    R ∧
     16  ∀init_in.make_initial_state
     17    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
     18  ∃init_out.
     19    make_initial_state
     20     (mk_prog_params ERTL_semantics p_out stacksizes) =
     21      OK ? init_out ∧
     22   R init_in init_out.
  • src/RTL/RTL_semantics.ma

    r2935 r2946  
    247247      rtl_fetch_external_args
    248248      rtl_set_result
    249       [ ] [ ]
     249      [ ]
     250      [an_identifier … one ; an_identifier … (p0 one) ;
     251       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    250252      (λ_.λ_.rtl_read_result) 
    251253      (λ_.λ_.eval_rtl_seq)
    252       (λ_.λ_.λ_.rtl_pop_frame_separate)).
     254      (λ_.λ_.λ_.rtl_pop_frame_separate))
     255    RTL_premain.
    253256
    254257definition RTL_semantics_separate_overflow ≝
     
    268271      rtl_fetch_external_args
    269272      rtl_set_result
    270       [ ] [ ]
     273      [ ]
     274      [an_identifier … one ; an_identifier … (p0 one) ;
     275       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    271276      (λ_.λ_.rtl_read_result) 
    272277      (λ_.λ_.eval_rtl_seq)
    273       (λ_.λ_.λ_.rtl_pop_frame_separate)).
     278      (λ_.λ_.λ_.rtl_pop_frame_separate))
     279    RTL_premain.
    274280
    275281definition RTL_semantics_unique ≝
     
    289295      rtl_fetch_external_args
    290296      rtl_set_result
    291       [ ] [ ]
     297      [ ]
     298      [an_identifier … one ; an_identifier … (p0 one) ;
     299       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
    292300      (λ_.λ_.rtl_read_result) 
    293301      (λ_.λ_.eval_rtl_seq)
    294       (λ_.λ_.λ_.rtl_pop_frame_unique)).
     302      (λ_.λ_.λ_.rtl_pop_frame_unique))
     303    RTL_premain.
     304     
Note: See TracChangeset for help on using the changeset viewer.