Changeset 2946


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (4 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
Files:
5 added
21 edited
3 moved

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2783 r2946  
    6868definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs).
    6969definition ertl_program ≝ joint_program ERTL.
     70unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL.
    7071
    7172interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     
    123124coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
    124125  on _s : ertl_seq to joint_seq ERTL ?.
     126
     127definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝
     128λp.
     129let l1 : label ≝ an_identifier … one in
     130let l2 : label ≝ an_identifier … (p0 one) in
     131let l3 : label ≝ an_identifier … (p1 one) in
     132let res ≝
     133  mk_joint_internal_function ERTL (prog_var_names … p)
     134  (mk_universe … (p0 (p0 one)))
     135  (mk_universe … one)
     136  it 4 0 0 (empty_map …) l1 in
     137(* todo: args for main? *)
     138let res ≝ add_graph … l1
     139  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     140  res in
     141let res ≝ add_graph … l2
     142  (sequential … (CALL ERTL ? (inl … (prog_main … p)) 4 it) l3)
     143  res in
     144let res ≝ add_graph … l3
     145  (GOTO ? l3)
     146  res in
     147res.
     148%
     149[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     150  %
     151  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     152  |2: %
     153  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     154  ]
     155| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     156| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     157| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     158| %{l2} %{(init_cost_label … p)} %
     159]
     160qed.
  • src/ERTL/ERTL_semantics.ma

    r2823 r2946  
    4040 (* empty_framesT ≝ *) [ ]
    4141 (* regsT ≝ *) ertl_reg_env
    42  (* empty_regsT ≝ *) (λsp.〈empty_map …,init_hw_register_env sp〉)
     42 (* empty_regsT ≝ *) (λsp.〈empty_map …, init_hw_register_env sp〉)
    4343 (*load_sp ≝ *) get_hwsp
    4444 (*save_sp ≝ *) set_hwsp.
     
    160160
    161161definition ERTL_semantics ≝
    162   mk_sem_graph_params ERTL ERTL_sem_uns.
     162  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2891 r2946  
    162162definition dummy_state : state ERTL_semantics ≝
    163163mk_state ERTL_semantics
    164    (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
     164   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 0 empty.
    165165
    166166definition sigma_state : ertl_program →
     
    173173  (carry … st)
    174174  (sigma_regs prog f_lbls restr (regs … st))
     175  (stack_usage … st)
    175176  (sigma_mem prog f_lbls (m … st)).
    176177   
     
    667668sigma_state prog f_lbls f_regs restr (set_sp ? ptr st).
    668669#prog #f_lbls #f_regs #restr #ptr #st whd in match set_sp; whd in match sigma_state;
    669 normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???);
     670normalize nodelta @eq_f3 try % whd in match (save_sp ???);
    670671whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
    671672cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
     
    11551156    (added_registers ERTL (prog_var_names … prog) fn (f_regs bl))
    11561157      (mk_state ? (Some ? tl) (istack … st) (carry … st) (〈loc_mem,\snd (regs … st)〉)
    1157       (m … st))) in ⊢ (???????(??%)?); @pop_ra_ok |
     1158      (stack_usage … st) (m … st))) in ⊢ (???????(??%)?); @pop_ra_ok |
    11581159  | * #st1 #pc1 @if_elim normalize nodelta [2: #_ @res_preserve_error1]
    11591160   normalize nodelta @eq_block_elim [2: #_ *] #EQbl1 * @if_elim
     
    16781679              #t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f
    16791680              whd in match set_frms; normalize nodelta >m_return_bind
    1680               cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
    1681                     a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
    1682                       mk_state ERTL_semantics a1 b1 c1 d1 e1 =
    1683                       mk_state ERTL_semantics a2 b2 c2 d2 e2)
     1681              cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2.
     1682                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → f1 = f2 →
     1683                      mk_state ERTL_semantics a1 b1 c1 d1 e1 f1 =
     1684                      mk_state ERTL_semantics a2 b2 c2 d2 e2 f2)
    16841685              [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
    1685                     #H15 //] #APP @APP try %
     1686                    #H15 #H16 #H17 #H18 //] #APP @APP try %
    16861687              [1,3: whd in match sigma_frames_opt; whd in match m_list_map;
    16871688                    normalize nodelta  whd in match (foldr ?????); normalize nodelta
     
    17101711]
    17111712qed.
    1712 
    1713 
  • src/ERTLptr/ERTLptr.ma

    r2783 r2946  
    4747definition ERTLptr ≝ mk_graph_params (mk_uns_params ERTLptr_uns ERTLptr_functs).
    4848definition ertlptr_program ≝ joint_program ERTLptr.
     49unification hint 0 ≔ ⊢ ertlptr_program ≡ joint_program ERTLptr.
    4950 
    5051definition ertlptr_seq_joint ≝ extension_seq ERTLptr.
     
    5253  on _s : ertlptr_seq to joint_seq ERTLptr ?.
    5354 
     55definition ERTLptr_premain : ∀p : ertlptr_program.joint_closed_internal_function ERTLptr (prog_var_names ?? p) ≝
     56λp.
     57let l1 : label ≝ an_identifier … one in
     58let l2 : label ≝ an_identifier … (p0 one) in
     59let l3 : label ≝ an_identifier … (p1 one) in
     60let res ≝
     61  mk_joint_internal_function ERTLptr (prog_var_names … p)
     62  (mk_universe … (p0 (p0 one)))
     63  (mk_universe … one)
     64  it 4 0 0 (empty_map …) l1 in
     65(* todo: args for main? *)
     66let res ≝ add_graph … l1
     67  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     68  res in
     69let res ≝ add_graph … l2
     70  (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 4 it) l3)
     71  res in
     72let res ≝ add_graph … l3
     73  (GOTO ? l3)
     74  res in
     75res.
     76%
     77[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     78  %
     79  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     80  |2: %
     81  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     82  ]
     83| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     84| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     85| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     86| %{l2} %{(init_cost_label … p)} %
     87]
     88qed.
  • src/ERTLptr/ERTLptr_semantics.ma

    r2796 r2946  
    6060 
    6161definition ERTLptr_semantics ≝
    62   mk_sem_graph_params ERTLptr ERTLptr_sem_uns.
     62  mk_sem_graph_params ERTLptr ERTLptr_sem_uns ERTLptr_premain.
  • src/LIN/LIN.ma

    r2286 r2946  
    2727
    2828definition lin_program ≝ joint_program LIN.
     29unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.
     30
     31definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝
     32λp.
     33let l3 : label ≝ an_identifier … (p1 one) in
     34let code ≝
     35  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
     36   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4 it) it〉 ;
     37   〈Some ? l3, GOTO ? l3〉 ] in
     38mk_joint_internal_function LIN (prog_var_names … p)
     39  (mk_universe … (p0 (p0 one)))
     40  (mk_universe … one)
     41  it it 0 0 code 0.
     42%
     43[ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct
     44  % try @I
     45  [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     46  |*: % whd in ⊢ (??%%→?); #EQ destruct
     47  ]
     48| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     49| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     50| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     51| %{it} %{(init_cost_label … p)} %
     52]
     53qed.
  • src/LIN/LINToASM.ma

    r2767 r2946  
    66
    77include "LIN/LIN.ma".
     8
     9
    810
    911(* utilities to provide Identifier's and addresses  *)
     
    2224  let globals_addr_internal ≝
    2325   λres_offset : identifier_map SymbolTag Word × Z.
    24    λx_size: ident × region × nat.
     26   λx_size: ident × region × (list init_data).
    2527    let 〈res, offset〉 ≝ res_offset in
    26     let 〈x, region, size〉 ≝ x_size in
    27       〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
    28   let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
     28    let 〈x, region, data〉 ≝ x_size in
     29      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
     30  let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(globals_stacksize … p)〉 (prog_vars ?? p) in
    2931mk_ASM_universe ? (mk_universe … one)
    3032  (an_identifier … one (* dummy *))
     
    3335@hide_prf
    3436normalize nodelta
    35 cases p -p #vars #functs #main
     37cases p -p * #vars #functs #main #cost_init
    3638#i #H
    37 letin init_val ≝ (〈empty_map ? Word, OZ〉)
     39letin init_val ≝ (〈empty_map ? Word, -(globals_stacksize ??)〉)
    3840cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
    3941[ %2{H} ] -H
     
    354356    ].
    355357
     358definition store_bytes : list Byte → list labelled_instruction ≝
     359λbytes.
     360\fold[(append ?), (nil ?)]_{by ∈ bytes}
     361    [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA by〉))))))〉 ;
     362      〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ;
     363      〈None ?, Instruction (INC ? DPTR)〉 ]. @I qed.
     364
     365definition do_store_init_data :
     366  ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction ≝
     367λglobals,u,nxt_dptr,data.
     368match data with
     369[ Init_int8 n ⇒
     370  store_bytes [ n ]
     371| Init_int16 n ⇒
     372  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in store_bytes [ by0 ; by1 ]
     373| Init_int32 n ⇒
     374  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
     375  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
     376  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
     377  store_bytes [ by0 ; by1 ; by2 ; by3 ]
     378| Init_addrof symb ofs ⇒
     379  let addr : Word ≝
     380    match lookup … (address_map … u) symb with
     381    [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs)
     382    | None ⇒ bv_zero ?
     383    ] in
     384  let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
     385  store_bytes [by0 ; by1] 
     386| Init_space n ⇒
     387  (* if n = 1 it is better to use INC, ow we can set the DPTR with MOV *)
     388  match n with
     389  [ O ⇒ [ ]
     390  | S k ⇒
     391    match k with
     392    [ O ⇒ [ 〈None ?, Instruction (INC ? DPTR)〉 ]
     393    | _ ⇒ [ 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … nxt_dptr)〉))))〉 ]
     394    ]
     395  ]
     396| Init_null ⇒ store_bytes [ bv_zero ? ; bv_zero ? ]
     397]. @I qed.
     398
     399definition do_store_init_data_list :
     400  ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
     401λglobals,u,start_dptr,data.
     402let f ≝ λdata,dptr_acc.
     403  let 〈dptr, acc〉 ≝ dptr_acc in
     404  let nxt_dptr ≝ dptr + size_init_data data in
     405  〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in
     406\snd (foldr ?? f 〈start_dptr, [ ]〉 data).
     407
     408definition translate_initialization : ∀p : lin_program.
     409  state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
     410  λp : lin_program.λu.
     411  let start_sp : Z ≝ -(globals_stacksize … p) in
     412  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
     413  let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
     414  let init_isp ≝
     415    (* initial stack pointer set to 2Fh in order to use addressable bits *)
     416    DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
     417  let isp_direct ≝
     418    (* 81h = 10000001b *)
     419    DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
     420  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
     421  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
     422  〈u, [
     423    〈None ?, Cost (init_cost_label … p)〉 ;
     424    (* initialize the internal stack pointer past the addressable bits *)
     425    〈None ?, Instruction
     426    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
     427      〈isp_direct, init_isp〉)))))〉 ;
     428    (* initialize our stack pointer past the globals *)
     429    〈None ?, Instruction
     430    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
     431      〈reg_spl, DATA spl〉))))))〉 ;
     432    〈None ?, Instruction
     433    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
     434      〈reg_sph, DATA sph〉))))))〉 ] @
     435  do_store_init_data_list ? u start_sp data〉. @I qed.
     436
    356437definition get_symboltable :
    357438  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
     
    373454     ! main ← Identifier_of_ident … (prog_main … p) ;
    374455     ! symboltable ← get_symboltable … ;
     456     ! init ← translate_initialization p ;
    375457     return
    376       (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
    377        ! code_ok ← code_size_opt code ; 
    378        (* atm no data identifier is used in the code, so preamble must be empty *)
    379        return
    380         (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
     458       (let code ≝
     459        init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     460        ! code_ok ← code_size_opt code ; 
     461        (* atm no data identifier is used in the code, so preamble must be empty *)
     462        return
     463          (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
    381464cases daemon
    382465qed.
  • src/LIN/LIN_semantics.ma

    r2783 r2946  
    33
    44definition LIN_semantics : sem_params ≝
    5   mk_sem_lin_params LIN LTL_LIN_semantics.
     5  mk_sem_lin_params LIN LTL_LIN_semantics LIN_premain.
  • src/LTL/LTL.ma

    r2286 r2946  
    2727
    2828definition ltl_program ≝ joint_program LTL.
     29unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL.
    2930
    3031coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝
     
    3233coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝
    3334  hdw_argument_from_reg on _r : Register to snd_arg LTL.
     35
     36definition LTL_premain : ∀p : ltl_program.joint_closed_internal_function LTL (prog_var_names ?? p) ≝
     37λp.
     38let l1 : label ≝ an_identifier … one in
     39let l2 : label ≝ an_identifier … (p0 one) in
     40let l3 : label ≝ an_identifier … (p1 one) in
     41let res ≝
     42  mk_joint_internal_function LTL (prog_var_names … p)
     43  (mk_universe … (p0 (p0 one)))
     44  (mk_universe … one)
     45  it it 0 0 (empty_map …) l1 in
     46(* todo: args for main? *)
     47let res ≝ add_graph … l1
     48  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     49  res in
     50let res ≝ add_graph … l2
     51  (sequential … (CALL LTL ? (inl … (prog_main … p)) 4 it) l3)
     52  res in
     53let res ≝ add_graph … l3
     54  (GOTO ? l3)
     55  res in
     56res.
     57%
     58[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     59  %
     60  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     61  |2: %
     62  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     63  ]
     64| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     65| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     66| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     67| %{l2} %{(init_cost_label … p)} %
     68]
     69qed.
  • src/LTL/LTLToLINAxiom.ma

    r2868 r2946  
    88axiom LTLToLIN_ok :
    99∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    10 ∀p_in : LTL_program.
     10∀p_in : joint_program LTL.
    1111let p_out ≝ ltl_to_lin p_in in
    1212∃[1] R.
     
    1414    (joint_status LTL_semantics p_in stacksizes)
    1515    (joint_status LIN_semantics p_out stacksizes)
    16     R.
     16    R ∧
     17  ∀init_in.make_initial_state
     18    (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in →
     19  ∃init_out.
     20    make_initial_state
     21     (mk_prog_params LIN_semantics p_out stacksizes) =
     22      OK ? init_out ∧
     23   R init_in init_out.
  • src/LTL/LTL_semantics.ma

    r2845 r2946  
    33
    44definition LTL_semantics ≝
    5   mk_sem_graph_params LTL LTL_LIN_semantics.
     5  mk_sem_graph_params LTL LTL_LIN_semantics LTL_premain.
  • 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     
  • 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.
  • 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
  • src/joint/Joint.ma

    r2865 r2946  
    524524(p : params) (globals : list ident) (def : joint_internal_function p globals)
    525525: Prop ≝
    526 { entry_costed :
    527   ∃l,nxt.
    528         stmt_at … (joint_if_code … def) (joint_if_entry … def) =
    529           Some … (sequential … (COST_LABEL … l) nxt)
    530 ; entry_unused :
     526{ entry_unused :
    531527  let entry ≝ joint_if_entry … def in
    532528  let code ≝ joint_if_code … def in
     
    598594definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    599595
    600 definition joint_program ≝
    601  λp:params. program (joint_function p) nat.
     596record joint_program (p : params) : Type[0] ≝
     597{ joint_prog :> program (joint_function p) (list init_data)
     598; init_cost_label : costlabel
     599(* here we can have global invariants (like injectivity of cost labels) *)
     600}.
    602601
    603602(* The cost model for stack consumption *)
     
    613612   [ ] (prog_funct ?? pr).
    614613
     614include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
    615615definition globals_stacksize : ∀p.joint_program p → nat ≝
    616616 λpars,p.
    617  Σ_{entry ∈ prog_vars … p}(\snd entry).
    618 
     617 Σ_{entry ∈ prog_vars … p}(size_init_data_list … (\snd entry)).
     618
  • src/joint/Traces.ma

    r2932 r2946  
    1 include "joint/joint_semantics.ma".
     1include "joint/semanticsUtils.ma".
    22include "common/StructuredTraces.ma".
    33
     
    3939
    4040lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
    41 #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
     41#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
     42
     43lemma lookup_remove_elim : ∀tag,A.∀P : option A → Prop.
     44∀m,i,j.
     45(i = j → P (None ?)) →
     46(i ≠ j → P (lookup tag A m i)) →
     47P (lookup tag A (remove tag A m j) i).
     48#tag #A #P #m #i #j #H1 #H2
     49@(eq_identifier_elim … i j) #H destruct
     50[ >lookup_remove_hit @H1 % | >lookup_remove_miss try @H2 assumption ]
     51qed.
    4252
    4353definition make_global : prog_params → evaluation_params
     
    4656let p ≝ prog pars in
    4757let spars ≝ prog_spars pars in
    48 let genv ≝ globalenv_noinit ? p in
     58let genv ≝ joint_globalenv spars p in
    4959let get_pc_lbl ≝ λid,lbl.
    5060  ! bl ← block_of_funct_id … spars genv id ;
     
    5666 (* (prog_io pars) *).
    5767#s #H
    58 elim (find_symbol_exists … p s ?)
    59 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
     68elim (find_symbol_exists … (λx.x) … p s ?)
     69[ #bl #EQ %
     70  whd in match genv; whd in match find_symbol; whd in match drop_fn; normalize nodelta
     71  @lookup_add_elim #H
     72  [2: @lookup_remove_elim [ #EQ >EQ in H; * #ABS cases (ABS ?) % ]
     73    #_ change with (find_symbol ? (globalenv … (λx.x) p) s = ? → ?) >EQ ]
     74  #ABS destruct(ABS) ]
    6075@Exists_append_r
    6176@(Exists_mp … H) //
     
    6681
    6782definition make_initial_state :
    68  ∀pars: prog_params.res (state_pc pars)
     83 ∀pars: prog_params.state_pc pars
    6984λpars.let p ≝ prog pars in
    7085  let sem_globals : evaluation_params ≝ pars in
    7186  let ge ≝ ev_genv sem_globals in
    72   let m0 ≝ alloc_mem … p in
     87  (* this is going to change shortly: globals will not reside in globalenv anymore *)
     88  let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
    7389  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    7490  let globals_size ≝ globals_stacksize … p in
     
    8197(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8298  let main ≝ prog_main … p in
    83   let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in
    84   (* use exit_pc as ra and call_dest_for_main as dest *)
    85   let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    86   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    87   let st0'' ≝ set_no_pc … st0_no_pc st0' in
    88   ! bl ← block_of_call … ge (inl … main) st0'';
    89   ! 〈i, fn〉 ← fetch_function … ge bl ;
    90   match fn with
    91   [ Internal ifn ⇒
    92     ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
    93     let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    94     return mk_state_pc … st' pc' exit_pc
    95   | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    96   ].
     99  let st ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m globals_size in
     100  mk_state_pc ? (set_sp … spp st) init_pc (null_pc one).
    97101cases m0 in H; #m1 #m2 #m3 #H
    98102whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
     
    197201    match s with
    198202    [ CALL f' args dest ⇒
    199         match
    200           (! bl ← block_of_call … (ev_genv p) f' st;
    201            fetch_internal_function … (ev_genv p) bl) with
    202         [ OK i_f ⇒ \fst i_f
    203         | _ ⇒ dummy
    204         ]
     203      match
     204        (! bl ← block_of_call … (ev_genv p) f' st;
     205         fetch_internal_function … (ev_genv p) bl) with
     206      [ OK i_f ⇒ \fst i_f
    205207      | _ ⇒ dummy
    206208      ]
     209    | _ ⇒ dummy
     210    ]
    207211  | _ ⇒ dummy
    208212  ]
     
    270274      ]).
    271275
     276(* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *)
     277definition exit_pc' : program_counter ≝
     278mk_program_counter «mk_block (-1), refl …» (p1 one).
     279
     280definition joint_final: ∀p: sem_params.∀globals.
     281  genv p globals → state_pc p → option int ≝
     282 λp,globals,ge,st.
     283 if eq_program_counter (pc … st) exit_pc' then
     284   let ret ≝ call_dest_for_main ?? p in
     285   res_to_opt … (! vals ← read_result … ge ret st ;
     286               Word_of_list_beval vals)
     287 else None ?.
     288
    272289definition joint_abstract_status :
    273290 ∀p : prog_params.
     
    284301   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    285302   (* as_after_return ≝ *) (joint_after_ret p)
    286    (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
     303   (* as_result ≝ *) (joint_final p  (globals ?) (ev_genv p))
    287304   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
    288305   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
  • src/joint/TranslateUtils.ma

    r2855 r2946  
    480480@hide_prf
    481481cases def in abs; -def #def #good_def
    482 cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
     482cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct
    483483qed.
    484484
     
    600600  joint_program dst_g_pars ≝
    601601  λsrc,dst,init,p.
    602   transform_program ??? p
    603     (λvarnames.transf_fundef ?? (λdef_in.
    604       b_graph_translate … (init varnames def_in) def_in)).
     602  mk_joint_program ?
     603    (transform_program ??? p
     604      (λvarnames.transf_fundef ?? (λdef_in.
     605        b_graph_translate … (init varnames def_in) def_in)))
     606    (init_cost_label … p).
    605607
    606608definition added_registers :
  • src/joint/joint_fullexec.ma

    r2821 r2946  
    2020let p ≝ \fst p_stack in
    2121let stack_sizes ≝ \snd p_stack in
    22 let genv ≝ globalenv_noinit ? p in
    23 let get_pc_lbl ≝ λid,lbl.
    24   ! bl ← block_of_funct_id … pars genv id ;
    25   pc_of_label … genv bl lbl in
     22let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
    2623mk_joint_global pars
    27   (prog_var_names ?? p)
    28   (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl).
    29  (* (prog_io pars) *).
    30 #s #H
    31 elim (find_symbol_exists … p s ?)
    32 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
    33 @Exists_append_r
    34 @(Exists_mp … H) //
    35 qed.
     24  (globals … ev_pars)
     25  (ev_genv … ev_pars).
    3626
    3727definition joint_exec: sem_params → trans_system io_out io_in ≝
    3828  λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
    39    (λenv.is_final G (jglobals … env) env exit_pc)
     29   (λenv.joint_final G (jglobals … env) env)
    4030   (λenv.λst.! st' ← eval_state … env st ;
    4131    let charge ≝ match joint_label_of_pc env (pc … st) with
     
    4939    (make_joint_global G)
    5040    (λp_stacks.
    51       make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     41      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    5242
    5343definition joint_preclassified_system : sem_params →
  • src/joint/joint_semantics.ma

    r2920 r2946  
    6060 ; regs: regsT semp
    6161 ; m: bemem
     62 ; stack_usage : ℕ
    6263 }.
    6364
     
    6768  { st_no_pc :> state semp
    6869  ; pc : program_counter
    69   (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
     70  (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
    7071  ; last_pop : program_counter
    7172  }.
    7273
    73 (* special program counter that is guaranteed to not correspond to anything *)
    74 definition exit_pc : program_counter ≝
     74definition init_pc : program_counter ≝
    7575  mk_program_counter «mk_block (-1), refl …» one.
    7676
     
    7979
    8080definition set_m: ∀p. bemem → state p → state p ≝
    81  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
     81 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
    8282
    8383definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    84  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
     84 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
    8585
    8686definition set_sp: ∀p. ? → state p → state p ≝
    8787 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    88  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
     88 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
    8989
    9090definition set_carry: ∀p. bebit → state p → state p ≝
    91  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     91 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
    9292
    9393definition set_istack: ∀p. internal_stack → state p → state p ≝
    94  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
     94 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
    9595
    9696definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    100100 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    101101
    102 definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
    103  λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.
     102definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
     103 λp,st,pc. mk_state_pc … st pc pc.
    104104
    105105definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    106  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
     106 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
    107107
    108108(*
     
    268268
    269269(* parameters that are defined by serialization *)
    270 record sem_params : Type[1] ≝
     270record serialized_params : Type[1] ≝
    271271  { spp :> params
    272272  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
     
    277277  ; offset_of_point_of_offset :
    278278    ∀o.offset_of_point (point_of_offset o) = o
     279  }.
     280
     281record sem_params : Type[1] ≝
     282  { spp' :> serialized_params
     283  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
    279284  }.
    280285
     
    513518      set_result … p vs dest st.
    514519
     520definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
     521 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     522  (n + stack_usage … st).
     523
     524definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
     525 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     526  (stack_usage … st - n).
     527
    515528definition eval_internal_call ≝
    516529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
    517530λst : state p.
    518531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    519 setup_call … stack_size (joint_if_params … globals fn) args st.
     532! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     533return increment_stack_usage … stack_size st'.
    520534
    521535definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     
    555569λcurr_id.λcurr_ret : call_dest p.
    556570λst : state p.
    557 ! st' ← pop_frame … ge curr_id curr_ret st ;
    558 ! nxt ← next_of_call_pc … ge (\snd … st') ;
     571! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
     572! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
     573! nxt ← next_of_call_pc … ge call_pc ;
     574let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
    559575return
    560   next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
     576  next ? nxt st'' (* now address pushed on stack are calling ones! *).
    561577
    562578definition eval_tailcall ≝
     
    568584match fd with
    569585[ Internal ifd ⇒
    570   ! st' ← eval_internal_call p globals ge i ifd args st ;
     586  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
     587  let st' ≝ decrement_stack_usage … stack_size st in
     588  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    571589  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    572   return mk_state_pc … st' pc (last_pop … st)
     590  return mk_state_pc … st'' pc (last_pop … st)
    573591| External efd ⇒
    574592  ! st' ← eval_external_call … efd args curr_ret st ;
     
    621639  let st'' ≝ set_no_pc … st' st in
    622640  eval_statement_advance … ge id fn s st''.
    623 
    624 definition is_final: ∀p: sem_params.∀globals.
    625   genv p globals → program_counter → state_pc p → option int ≝
    626  λp,globals,ge,exit,st.res_to_opt ? (
    627   do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
    628   match s with
    629   [ final s' ⇒
    630     match s' with
    631     [ RETURN ⇒
    632       let curr_ret ≝ joint_if_result … fn in
    633       do st' ← pop_frame … ge id curr_ret st;
    634       if eq_program_counter (\snd … st') exit then
    635       do vals ← read_result … ge curr_ret st ;
    636         Word_of_list_beval vals
    637       else
    638         Error ? [ ]
    639    | _ ⇒ Error ? [ ]
    640    ]
    641  | _ ⇒ Error ? [ ]
    642  ]).
  • src/joint/linearise.ma

    r2823 r2946  
    885885   ≝
    886886  λp,pr.transform_program ??? pr
    887     (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
     887    mk_joint_program
     888      (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))
     889      (init_cost_label … pr).
    888890
    889891(*
  • src/joint/semanticsUtils.ma

    r2843 r2946  
    77include "common/extraGlobalenvs.ma".
    88
     9definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
     10
     11definition reg_retrieve : register_env beval → register → res beval ≝
     12 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     13
    914record hw_register_env : Type[0] ≝
    1015  { reg_env : BitVectorTrie beval 6
    1116  ; other_bit : bebit
    1217  }.
    13 
    14 definition empty_hw_register_env: hw_register_env ≝
    15   mk_hw_register_env (Stub …) BBundef.
    1618
    1719include alias "ASM/BitVectorTrie.ma".
     
    4244hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
    4345
     46definition init_hw_register_env: xpointer → hw_register_env ≝
     47 hwreg_store_sp (mk_hw_register_env (Stub …) BBundef).
     48
    4449(*** Store/retrieve on pseudo-registers ***)
    4550include alias "common/Identifiers.ma".
    4651
    47 record reg_sp : Type[0] ≝
    48 { reg_sp_env :> identifier_map RegisterTag beval
    49 ; stackp : xpointer
    50 }.
    51 
    52 definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
    53 
    54 definition reg_retrieve : register_env beval → register → res beval ≝
    55  λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
    56 
    57 definition reg_sp_store ≝ λreg,v,locals.
    58 let locals' ≝ reg_store reg v (reg_sp_env locals) in
    59 mk_reg_sp locals' (stackp locals).
    60 
    6152unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
    62 
    63 definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
    64 
    65 definition reg_sp_init ≝ mk_reg_sp (empty_map …).
    66 (*** Store/retrieve on hardware registers ***)
    67 
    68 definition init_hw_register_env: xpointer → hw_register_env ≝
    69  λsp.hwreg_store_sp empty_hw_register_env sp.
    7053
    7154(******************************** GRAPHS **************************************)
     
    7457{ sgp_pars : uns_params
    7558; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
     59; graph_pre_main_generator :
     60  ∀p : joint_program (mk_graph_params sgp_pars).
     61  joint_closed_internal_function (mk_graph_params sgp_pars) (prog_var_names … p)
    7662}.
    7763
     
    9177  λpars.
    9278  mk_sem_params
    93     (pars : graph_params)
    94     (sgp_sup pars ?)
    95     (word_of_identifier ?)
    96     (an_identifier ?)
    97     ? (refl …).
     79    (mk_serialized_params
     80      (pars : graph_params)
     81      (sgp_sup pars ?)
     82      (word_of_identifier ?)
     83      (an_identifier ?)
     84      ? (refl …))
     85    (graph_pre_main_generator pars).
    9886* #p % qed.
    9987
     
    113101{ slp_pars : uns_params
    114102; slp_sup : ∀F.sem_unserialized_params slp_pars F
     103; lin_pre_main_generator :
     104  ∀p : joint_program (mk_lin_params slp_pars).
     105  joint_closed_internal_function (mk_lin_params slp_pars) (prog_var_names … p)
    115106}.
    116107
     
    129120  λpars.
    130121  mk_sem_params
    131     (pars : lin_params)
    132     (slp_sup pars ?)
    133     succ_pos_of_nat
    134     (λp.pred (nat_of_pos p))
    135     ??.
    136 [ #n >nat_succ_pos %
    137 | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     122    (mk_serialized_params
     123      (pars : lin_params)
     124      (slp_sup pars ?)
     125      succ_pos_of_nat
     126      (λp.pred (nat_of_pos p))
     127      ??)
     128    (lin_pre_main_generator pars).
     129[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     130| #n >nat_succ_pos %
    138131] qed.
    139132
     
    143136  on _pars : sem_lin_params to sem_params.
    144137
     138(* watch out, implementation dependent:
     139   an_identifier SymbolTag one must be unused (used for premain)
     140*)
     141definition pre_main_id : ident ≝ an_identifier … one.
     142
     143lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m.
     144  (p = q → P o) →
     145  (p ≠ q → P (lookup_opt A p m)) →
     146  P (lookup_opt A p (pm_set A q o m)).
     147#A #P #p #q
     148@(eqb_elim p q) #H #o #m #H1 #H2
     149[ >H >lookup_opt_pm_set_hit @H1 @H
     150| >lookup_opt_pm_set_miss [ @H2 ] @H
     151]
     152qed.
     153
     154lemma lookup_add_elim : ∀tag,A.∀P : option A → Prop.∀m,i,j,x.
     155  (i = j → P (Some ? x)) →
     156  (i ≠ j → P (lookup tag A m j)) →
     157  P (lookup tag A (add tag A m i x) j).
     158#tag #A #P * #m * #p * #q #x
     159#H1 #H2 whd in ⊢ (?%); normalize nodelta whd in match insert; normalize nodelta
     160@lookup_opt_pm_set_elim #H destruct
     161[ @H1 % | @H2 % #EQ destruct cases H #H @H % ]
     162qed.
     163
     164(* we just manually overwrite genv_t tables with the pre_main.
     165   the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *)
     166definition joint_globalenv :
     167  ∀pars : sem_params.joint_program pars → genv_t ? ≝
     168  λpars,prog.
     169  let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in
     170  mk_genv_t ?
     171    (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv))
     172    (nextfunction … genv)
     173    (add … (symbols … genv) pre_main_id (mk_block (-1)))
     174    ?.
     175@hide_prf
     176whd in match insert; normalize nodelta #b
     177@lookup_opt_pm_set_elim #H destruct
     178[ #_ %{pre_main_id} @lookup_add_hit ]
     179#G cases (functions_inv … G) #id #EQ %{id}
     180@lookup_add_elim #EQid destruct [2: assumption ]
     181@⊥ whd in match drop_fn in EQ; normalize nodelta in EQ;
     182>lookup_remove_hit in EQ; #ABS destruct
     183qed.
    145184
    146185lemma fetch_statement_eq : ∀p:sem_params.∀g.
     
    346385qed.
    347386
    348 
    349387lemma functions_transf:
    350388 ∀A,B,V,init.∀prog_in : program A V.
     
    403441
    404442lemma fetch_internal_function_transf :
    405  ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V.
    406444 ∀trans : ∀vars.A vars → B vars.
    407445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
    408446 ∀bl.
    409  fetch_internal_function … (globalenv_noinit … prog_out) bl =
    410  ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
     447 fetch_internal_function … (globalenv … init prog_out) bl =
     448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ;
    411449 return 〈i, trans … f〉.
    412 #A #B #prog #trans #bl
     450#A #B #V #init #prog #trans #bl
    413451 whd in match fetch_internal_function; normalize nodelta
    414452>(fetch_function_transf … prog)
     
    452490  λf_regs : block → label → list register.
    453491   let prog_out ≝ b_graph_transform_program src dst data prog_in in
    454    let src_genv ≝ globalenv_noinit ? prog_in in
    455    let dst_genv ≝ globalenv_noinit ? prog_out in
     492   let src_genv ≝ joint_globalenv src prog_in in
     493   let dst_genv ≝ joint_globalenv dst prog_out in
    456494  ∀bl,def_in.
     495  block_id … bl ≠ -1 →
    457496  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
    458497  ∃init_data,def_out.
     
    468507 ∀prog_in : joint_program src.
    469508 let prog_out ≝ b_graph_transform_program … data prog_in in
    470  let src_genv ≝ globalenv_noinit ? prog_in in
    471  let dst_genv ≝ globalenv_noinit ? prog_out in
     509 let src_genv ≝ joint_globalenv src prog_in in
     510 let dst_genv ≝ joint_globalenv dst prog_out in
    472511 ∃init_regs : block → list register.
    473512 ∃f_lbls : block → label → list label.
    474513 ∃f_regs : block → label → list register.
    475514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
     515cases daemon (* TOREDO
    476516#src #dst #data #prog_in
    477517whd in match b_graph_transform_program_props; normalize nodelta
     518whd in match joint_globalenv; normalize nodelta
    478519letin prog_out ≝ (b_graph_transform_program … data prog_in)
    479 letin src_genv ≝ (globalenv_noinit ? prog_in)
    480 letin dst_genv ≝ (globalenv_noinit ? prog_out)
     520letin src_genv ≝ (globalenv … (λx.x) prog_in)
     521letin dst_genv ≝ (globalenv … (λx.x) prog_out)
    481522cut (∀p.lookup_opt ? p (functions ? dst_genv) =
    482523     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
    483524      (lookup_opt ? p (functions ? src_genv)))
    484525[ @functions_transf ]
     526cut (symbols ? dst_genv = symbols ? src_genv)
     527[ @symbols_transf ]
    485528cases dst_genv #functs2 #nextf2 #symbols2 #H2
    486 cases src_genv #functs1 #nextf1 #symbols1 #H1
     529cases src_genv #functs1 #nextf1 #symbols1 #H1 #EQ destruct
    487530lapply H2 lapply H1 lapply functs2
    488531@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
     
    490533#functs2 #H1 #H2 #transf
    491534[ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])}
    492   #bl #def_in #ABS @⊥ lapply ABS -ABS
     535  #bl #def_in #ABS1 #ABS2 @⊥ lapply ABS2 -ABS2 lapply ABS1 -ABS1
    493536  whd in match find_funct_ptr;
     537  whd in match find_symbol;
    494538  normalize nodelta
    495   whd in match (block_region bl);
    496   cases (block_id bl) normalize nodelta
    497   [2,3: #p [2: >functs1_empty ]]
    498   normalize #ABS destruct
     539  cases bl; * normalize nodelta
     540  [2,3: #p ]
     541  [1,3: #_ whd in ⊢ (???%→?); #EQ destruct ]
     542  >lookup_add_hit
     543  #H >lookup_opt_insert_miss
     544  [2: @(swap_neg … H) #EQ >EQ % ]
     545  whd in match drop_fn; normalize nodelta
     546  cases (lookup … symbols1 pre_main_id)
     547  normalize nodelta
     548  [ >functs1_empty | ** [2,3: #p' ] normalize nodelta
     549    [1,3: >functs1_empty
     550    | @lookup_opt_pm_set_elim #H destruct
     551      [2: >functs1_empty ]
     552    ]
     553  ] whd in ⊢ (???%→?); #EQ destruct
    499554]
    500555cases (IH (pm_set … p (None ?) functs2) ???)
    501 [2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
    502   [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
    503   #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
    504 |3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
    505   [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
    506   #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
    507 |4: #b @(eqb_elim b p)
    508   [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
    509   #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
    510   >(lookup_opt_insert_miss ? f b p … NEQ) %
    511 ]
     556[|*: @hide_prf
     557  [ #b #G @(H1 b ?) @(swap_neg … G) -G
     558    whd in match insert; normalize nodelta
     559    @lookup_opt_pm_set_elim
     560    [ #EQ #ABS destruct ]
     561    #NEQ #H @H
     562  | #b #G @(H2 b ?) @(swap_neg … G) -G
     563    @lookup_opt_pm_set_elim
     564    [ #_ #_ % ]
     565    #_ #H @H
     566  | #b @lookup_opt_pm_set_elim
     567    [ #EQ destruct >p_not_in % ]
     568    #NEQ >transf
     569    >(lookup_opt_insert_miss ? f b p … NEQ) %
     570  ]
     571]
     572#init_regs * #f_lbls * #f_regs #props
    512573-IH cases f in H1 transf; -f #f #H1 #transf
    513 #init_regs * #f_lbls * #f_regs #props
    514574[ (* internal *)
    515575  letin upd ≝ (λA : Type[0].λf : block → A.
     
    532592whd in match (block_region (mk_block p'));
    533593cases p' -p' [2,3,5,6: #p' ] normalize nodelta
    534 [1,3,5,6: #ABS normalize in ABS; destruct]
    535 @(eqb_elim p' p) #pp' destruct
    536 [1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
    537   %{loc_data} %
    538   [2: % [ % ]
    539     [ >transf >lookup_opt_insert_hit %
    540     |*: >eq_block_b_b assumption
    541     ]
    542   |]
     594[1,3,5,6: #_ #ABS normalize in ABS; destruct]
     595whd in match find_symbol;
     596whd in match insert; normalize nodelta
     597#bl_prf
     598@lookup_opt_pm_set_elim #pp' destruct
     599[1,3: whd in ⊢ (??%%→?); #EQ destruct(EQ)
     600  [ %{loc_data} %
     601    [2: % [ % ]
     602      [ >lookup_opt_insert_hit %
     603      |*: >eq_block_b_b assumption
     604      ]
     605    |]
    543606|*: >(lookup_opt_insert_miss ???? functs1 … pp')
    544607  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
     
    546609  whd in match find_funct_ptr; normalize nodelta
    547610  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
    548 ]
     611] *)
    549612qed.
    550613
     
    559622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    560623 let prog_out ≝ b_graph_transform_program … data prog_in in
    561  let src_genv ≝ globalenv_noinit ? prog_in in
    562  let dst_genv ≝ globalenv_noinit ? prog_out in
    563  ∀bl,id,def_in.
     624 let src_genv ≝ joint_globalenv src prog_in in
     625 let dst_genv ≝ joint_globalenv dst prog_out in
     626 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
     627 block_id … bl ≠ -1 →
    564628 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
    565629 ∃init_data,def_out.
     
    570634#src #dst #data #prog_in
    571635#init_regs #f_lbls #f_regs #props
    572 #bl #id #def_in
     636#bl #id #def_in #NEQ
    573637#H @('bind_inversion H) * #id' * #def_in' -H
    574638normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
     
    576640#H @('bind_inversion H) -H #def_in' #H
    577641whd in ⊢ (??%%→?); #EQ destruct
    578 cases (props … H)
     642cases (props … NEQ H)
    579643#loc_data * #def_out ** #H1 #H2 #H3
    580644%{loc_data} %{def_out}
     
    582646whd in match fetch_internal_function;
    583647whd in match fetch_function; normalize nodelta
     648cases daemon (* TOREDO
    584649>symbol_for_block_transf >EQ1 >m_return_bind
    585 >H1 %
     650>H1 % *)
    586651qed.
    587652
     
    596661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    597662 let prog_out ≝ b_graph_transform_program … data prog_in in
    598  let src_genv ≝ globalenv_noinit ? prog_in in
    599  let dst_genv ≝ globalenv_noinit ? prog_out in
     663 let src_genv ≝ joint_globalenv src prog_in in
     664 let dst_genv ≝ joint_globalenv dst prog_out in
    600665 ∀pc,id,def_in,s.
     666 block_id … (pc_block … pc) ≠ -1 →
    601667 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    602668 ∃init_data,def_out.
     
    622688#src #dst #data #prog_in
    623689#init_regs #f_lbls #f_regs #props
    624 #pc #id #def_in #s
     690#pc #id #def_in #s #NEQ
    625691#H @('bind_inversion H) * #id' #def_in' -H
    626692#EQfif
     
    628694#H lapply (opt_eq_from_res ???? H) -H
    629695#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    630 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     696cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
    631697#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    632698[ %{H1 H2}
     
    644710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    645711 let prog_out ≝ b_graph_transform_program … data prog_in in
    646  let src_genv ≝ globalenv_noinit ? prog_in in
    647  let dst_genv ≝ globalenv_noinit ? prog_out in
     712 let src_genv ≝ joint_globalenv src prog_in in
     713 let dst_genv ≝ joint_globalenv dst prog_out in
    648714 ∀pc,id,def_in,s.
     715 block_id … (pc_block … pc) ≠ -1 →
    649716 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    650717 ∃init_data,def_out.
     
    679746#src #dst #data #prog_in
    680747#init_regs #f_lbls #f_regs #props
    681 #pc #id #def_in #s
     748#pc #id #def_in #s #NEQ
    682749#H @('bind_inversion H) * #id' #def_in' -H
    683750#EQfif
     
    685752#H lapply (opt_eq_from_res ???? H) -H
    686753#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    687 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     754cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
    688755#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    689756[ %{H1 H2}
Note: See TracChangeset for help on using the changeset viewer.