Changeset 2286 for src/ERTL


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/ERTL
Files:
5 deleted
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1388 r2286  
    11include "joint/Joint.ma".
    22
    3 inductive move_registers: Type[0] ≝
    4   | pseudo: register → move_registers
    5   | hardware: Register → move_registers.
    6                  
    7 inductive ertl_statement_extension: Type[0] ≝
    8   | ertl_st_ext_new_frame: ertl_statement_extension
    9   | ertl_st_ext_del_frame: ertl_statement_extension
    10   | ertl_st_ext_frame_size: register → ertl_statement_extension.
     3inductive move_dst: Type[0] ≝
     4  | PSD: register → move_dst
     5  | HDW: Register → move_dst.
    116
    12 definition ertl_params__: params__ ≝
    13  mk_params__ register register register register (move_registers × move_registers)
    14   register nat unit ertl_statement_extension.
    15 definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
    16 definition ertl_params0: params0 ≝ mk_params0 ertl_params__ (list register) nat.
    17 definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
    18 definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
     7definition move_src ≝ argument move_dst.
    198
    20 definition ertl_statement ≝ joint_statement ertl_params_.
     9definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
     10coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
    2111
    22 definition ertl_internal_function ≝
    23   λglobals.joint_internal_function … (ertl_params globals).
     12definition psd_argument_move_src : psd_argument → move_src ≝
     13  λarg.match arg with
     14  [ Imm b ⇒ Imm ? b
     15  | Reg r ⇒ Reg ? (PSD r)
     16  ].
     17coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
     18  psd_argument_move_src on _a : psd_argument to move_src.
    2419
    25 definition ertl_program ≝ joint_program ertl_params.
     20inductive ertl_seq : Type[0] ≝
     21  | ertl_new_frame: ertl_seq
     22  | ertl_del_frame: ertl_seq
     23  | ertl_frame_size: register → ertl_seq.
     24
     25definition ERTL_uns ≝ mk_unserialized_params
     26    (* acc_a_reg ≝ *) register
     27    (* acc_b_reg ≝ *) register
     28    (* acc_a_arg ≝ *) psd_argument
     29    (* acc_b_arg ≝ *) psd_argument
     30    (* dpl_reg   ≝ *) register
     31    (* dph_reg   ≝ *) register
     32    (* dpl_arg   ≝ *) psd_argument
     33    (* dph_arg   ≝ *) psd_argument
     34    (* snd_arg   ≝ *) psd_argument
     35    (* pair_move ≝ *) (move_dst × move_src)
     36    (* call_args ≝ *) ℕ
     37    (* call_dest ≝ *) unit
     38    (* ext_seq ≝ *) ertl_seq
     39    (* ext_call ≝ *) void
     40    (* ext_tailcall ≝ *) void
     41    (* paramsT ≝ *) ℕ
     42    (* localsT ≝ *) register.
     43
     44definition ERTL ≝ mk_graph_params ERTL_uns.
     45definition ertl_program ≝ joint_program ERTL.
     46
     47interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     48
     49(* aid unification *)
     50unification hint 0 ≔
     51(*---------------*) ⊢
     52pair_move ERTL ≡ move_dst × move_src.
     53unification hint 0 ≔
     54(*---------------*) ⊢
     55acc_a_reg ERTL ≡ register.
     56unification hint 0 ≔
     57(*---------------*) ⊢
     58acc_b_reg ERTL ≡ register.
     59unification hint 0 ≔
     60(*---------------*) ⊢
     61acc_a_arg ERTL ≡ psd_argument.
     62unification hint 0 ≔
     63(*---------------*) ⊢
     64acc_b_arg ERTL ≡ psd_argument.
     65unification hint 0 ≔
     66(*---------------*) ⊢
     67dpl_reg ERTL ≡ register.
     68unification hint 0 ≔
     69(*---------------*) ⊢
     70dph_reg ERTL ≡ register.
     71unification hint 0 ≔
     72(*---------------*) ⊢
     73dpl_arg ERTL ≡ psd_argument.
     74unification hint 0 ≔
     75(*---------------*) ⊢
     76dph_arg ERTL ≡ psd_argument.
     77unification hint 0 ≔
     78(*---------------*) ⊢
     79snd_arg ERTL ≡ psd_argument.
     80unification hint 0 ≔
     81(*---------------*) ⊢
     82call_args ERTL ≡ ℕ.
     83unification hint 0 ≔
     84(*---------------*) ⊢
     85call_dest ERTL ≡ unit.
     86
     87unification hint 0 ≔
     88(*---------------*) ⊢
     89ext_seq ERTL ≡ ertl_seq.
     90unification hint 0 ≔
     91(*---------------*) ⊢
     92ext_call ERTL ≡ void.
     93unification hint 0 ≔
     94(*---------------*) ⊢
     95ext_tailcall ERTL ≡ void.
     96
     97coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
     98  psd_argument_from_reg
     99  on _r : register to snd_arg ERTL.
     100coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
     101  psd_argument_from_byte
     102  on _b : Byte to snd_arg ERTL.
     103 
     104definition ertl_seq_joint ≝ extension_seq ERTL.
     105coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
     106  on _s : ertl_seq to joint_seq ERTL.
  • src/ERTL/ERTLToLTL.ma

    r2103 r2286  
     1
    12include "LTL/LTL.ma".
    23include "ERTL/Interference.ma".
    34include "ASM/Arithmetic.ma".
    4 
    5 definition fresh_label ≝
     5include "joint/TranslateUtils.ma".
     6
     7(* Note: translation is complicated by having to preserve the carry bit and
     8  wanting to do it with as less boilerplate as possible. It could be somewhat
     9  simplified if constant and copy propagation was to be done after this pass:
     10  those optimisations would take care of the boilerplate for us.*)
     11
     12coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision.
     13
     14inductive arg_decision : Type[0] ≝
     15  | arg_decision_colour : Register → arg_decision
     16  | arg_decision_spill : ℕ → arg_decision
     17  | arg_decision_imm : beval → arg_decision.
     18
     19coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
     20
     21(* Paolo: I'm changing the following: before, spilled registers were
     22  assigned stack addresses going from SP + #frame_size - #stack_params
     23  excluded down to SP included. I am turning it upside down, so that
     24  the offset does not need the stack size to be computed *)
     25
     26definition preserve_carry_bit :
     27  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
     28  λglobals,do_it,steps.
     29  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     30
     31(* for notation *)
     32definition A ≝ it.
     33
     34coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.
     35
     36(* spill should be byte-based from the start *)
     37definition set_dp_by_offset :
     38  ∀globals.nat → list (joint_seq LTL globals) ≝
     39  λglobals,off.
     40  [ A ← byte_of_nat off
     41  ; A ← A .Add. RegisterSPL
     42  ; RegisterDPL ← A
     43  ; A ← zero_byte
     44  ; A ← A .Addc. RegisterSPH
     45  ; RegisterDPH ← A
     46  ].
     47
     48definition get_stack:
     49 ∀globals.Register → nat → list (joint_seq LTL globals) ≝
     50 λglobals,r,off.
     51 set_dp_by_offset ? off @
     52 [ LOAD … A it it ] @
     53 if eq_Register r RegisterA then [ ] else [ r ← A ].
     54
     55definition set_stack_not_a :
     56 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
     57 λglobals,off,r.
     58 set_dp_by_offset ? off @
     59 [ A ← r
     60 ; STORE … it it A ].
     61
     62definition set_stack_a :
     63 ∀globals.nat → list (joint_seq LTL globals) ≝
     64 λglobals,off.
     65 [ RegisterST1 ← A ] @
     66 set_stack_not_a ? off RegisterST1.
     67
     68definition set_stack :
     69 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
     70 λglobals,off,r.
     71 if eq_Register r RegisterA then
     72   set_stack_a ? off
     73 else
     74   set_stack_not_a ? off r.
     75 
     76definition set_stack_int :
     77  ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
     78  λglobals,off,int.
     79  set_dp_by_offset ? off @
     80  [ A ← int
     81  ; STORE … it it A ].
     82
     83definition move :
     84  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
     85  λglobals,carry_lives_after,dst,src.
     86  match dst with
     87  [ decision_colour dstr ⇒
     88    match src with
     89    [ arg_decision_colour srcr ⇒
     90      if eq_Register dstr srcr then [ ] else
     91      if eq_Register dstr RegisterA then [ A ← srcr ] else
     92      if eq_Register srcr RegisterA then [ dstr ← A ] else
     93      [ A ← srcr ; dstr ← A]
     94    | arg_decision_spill srco ⇒
     95      preserve_carry_bit ? carry_lives_after
     96        (get_stack ? dstr srco)
     97    | arg_decision_imm int ⇒
     98      [ A ← int ] @
     99      if eq_Register dstr RegisterA then [ ] else
     100      [ dstr ← A ]
     101    ]
     102  | decision_spill dsto ⇒
     103    match src with
     104    [ arg_decision_colour srcr ⇒
     105      preserve_carry_bit ? carry_lives_after
     106        (set_stack ? dsto srcr)
     107    | arg_decision_spill srco ⇒
     108      if eqb srco dsto then [ ] else
     109      preserve_carry_bit ? carry_lives_after
     110        (get_stack ? RegisterA srco @
     111         set_stack ? dsto RegisterA)
     112    | arg_decision_imm int ⇒
     113      preserve_carry_bit ? carry_lives_after
     114        (set_stack_int ? dsto int)
     115    ]
     116  ].
     117
     118definition arg_is_spilled : arg_decision → bool ≝
     119  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
     120definition is_spilled : decision → bool ≝
     121  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].
     122
     123definition newframe :
     124  ∀globals.ℕ → list (joint_seq LTL globals) ≝
     125  λglobals,stack_sz.
     126  [ CLEAR_CARRY …
     127  ; A ← RegisterSPL
     128  ; A ← A .Sub. byte_of_nat stack_sz
     129  ; RegisterSPL ← A
     130  ; A ← RegisterSPH
     131  ; A ← A .Sub. zero_byte
     132  ; RegisterSPL ← A
     133  ].
     134
     135definition delframe :
     136  ∀globals.ℕ → list (joint_seq LTL globals) ≝
     137  λglobals,stack_sz.
     138  [ A ← RegisterSPL
     139  ; A ← A .Add. byte_of_nat stack_sz
     140  ; RegisterSPL ← A
     141  ; A ← RegisterSPH
     142  ; A ← A .Addc. zero_byte
     143  ; RegisterSPL ← A
     144  ].
     145
     146definition commutative : Op2 → bool ≝
     147λop.match op with
     148[ Add ⇒ true
     149| Addc ⇒ true
     150| Or ⇒ true
     151| Xor ⇒ true
     152| And ⇒ true
     153| _ ⇒ false
     154].
     155
     156definition uses_carry : Op2 → bool ≝
     157λop.match op with
     158[ Addc ⇒ true
     159| Sub ⇒ true
     160| _ ⇒ false
     161].
     162
     163definition sets_carry : Op2 → bool ≝
     164λop.match op with
     165[ Add ⇒ true
     166| Addc ⇒ true
     167| Sub ⇒ true
     168| _ ⇒ false
     169].
     170
     171definition translate_op2 :
     172  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     173  λglobals,carry_lives_after,op,dst,arg1,arg2.
     174  (* this won't preserve the carry bit if op does not set it: left to next function *)
     175  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
     176  (preserve_carry_bit ?
     177    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
     178    (move ? false RegisterB arg2 @
     179     move ? false RegisterA arg1) @
     180    [ A ← A .op. RegisterB ] @
     181    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
     182    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
     183
     184definition translate_op2_smart :
     185  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     186  λglobals,carry_lives_after,op,dst,arg1,arg2.
     187  (* if op does not set carry bit (⇒ it does not use it either) then it must be
     188    preserved *)
     189  preserve_carry_bit ?
     190    (¬sets_carry op ∧ carry_lives_after ∧
     191      (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst))
     192    (match arg2 with
     193    [ arg_decision_colour arg2r ⇒
     194      move ? (uses_carry op) RegisterA arg1 @
     195      [ A ← A .op. arg2r ] @
     196      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     197    | arg_decision_imm arg2i ⇒
     198      move ? (uses_carry op) RegisterA arg1 @
     199      [ A ← A .op. arg2i ] @
     200      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     201    | _ ⇒
     202      if commutative op then
     203        match arg1 with
     204        [ arg_decision_colour arg1r ⇒
     205          move ? (uses_carry op) RegisterA arg2 @
     206          [ A ← A .op. arg1r ] @
     207          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     208        | arg_decision_imm arg1i ⇒
     209          move ? (uses_carry op) RegisterA arg2 @
     210          [ A ← A .op. arg1i ] @
     211          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
     212        | _ ⇒
     213          translate_op2 ? carry_lives_after op dst arg1 arg2
     214        ]
     215      else
     216        translate_op2 ? carry_lives_after op dst arg1 arg2
     217    ]).
     218
     219definition dec_to_arg_dec : decision → arg_decision ≝
     220  λd.match d with
     221  [ decision_colour r ⇒ arg_decision_colour r
     222  | decision_spill n ⇒ arg_decision_spill n
     223  ].
     224
     225coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.
     226
     227definition translate_op1 :
     228  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
     229  λglobals,carry_lives_after,op,dst,arg.
     230  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
     231  preserve_carry_bit ? preserve_carry
     232    (move ? false RegisterA arg @
     233     OP1 … op it it ::
     234     move ? false dst RegisterA).
     235
     236definition translate_opaccs :
     237  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     238  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
     239  (* OPACCS always has dead carry bit and sets it to zero *)
     240  move ? false RegisterB arg2 @
     241  move ? false RegisterA arg1 @
     242  OPACCS … op it it it it ::
     243  move ? false dst1 RegisterA @
     244  move ? false dst2 RegisterB @
     245  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
     246    [CLEAR_CARRY ??]
     247  else [ ].
     248
     249(* does not preserve carry bit *)
     250definition move_to_dp :
     251  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     252  λglobals,arg1,arg2.
     253  if ¬arg_is_spilled arg1 then
     254    move ? false RegisterDPH arg2 @
     255    (* does not change dph because arg1 is not spilled *)
     256    move ? false RegisterDPL arg1
     257  else if ¬arg_is_spilled arg2 then
     258    move ? false RegisterDPL arg1 @
     259    (* does not change dpl because arg2 is not spilled *)
     260    move ? false RegisterDPH arg2
     261  else
     262    (* using B as temporary, as moving spilled registers tampers with DPTR *)
     263    move ? false RegisterB arg1 @
     264    move ? false RegisterDPH arg2 @
     265    move ? false RegisterDPL RegisterB.
     266
     267definition translate_store : 
     268  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     269  λglobals,carry_lives_after,addr1,addr2,src.
     270  (* requires src != RegisterA and RegisterB *)
     271  preserve_carry_bit ? (carry_lives_after ∧
     272    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
     273    (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
     274     (if arg_is_spilled src then
     275        move ? false RegisterST0 src @
     276        move_to_dptr @
     277        [ A ← RegisterST0]
     278      else move_to_dptr) @
     279     [STORE … it it A]).
     280
     281definition translate_load : 
     282  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
     283  λglobals,carry_lives_after,dst,addr1,addr2.
     284  preserve_carry_bit ? (carry_lives_after ∧
     285    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
     286    (move_to_dp ? addr1 addr2 @
     287     [ LOAD … A it it ] @
     288     move ? false dst RegisterA).
     289
     290definition translate_address :
     291  ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
     292  list (joint_seq LTL globals) ≝
     293  λglobals,carry_lives_after,id,prf,addr1,addr2.
     294  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
     295    (ADDRESS LTL ? id prf it it ::
     296     move ? false addr1 RegisterDPL @
     297     move ? false addr2 RegisterDPH).
     298
     299definition translate_step:
     300  ∀globals.∀after : valuation register_lattice.
     301  coloured_graph after →
     302  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
     303  λglobals,after,grph,stack_sz,lbl,s.
     304  let lookup ≝ λr.colouring … grph (inl … r) in
     305  let lookup_arg ≝ λa.match a with
     306    [ Reg r ⇒ lookup r
     307    | Imm b ⇒ arg_decision_imm b
     308    ] in
     309  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
     310  let move ≝ move globals carry_lives_after in
     311  match s with
     312  [ step_seq s' ⇒
     313    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
     314    [ COMMENT c ⇒ COMMENT … c
     315    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
     316    | POP r ⇒
     317      POP … A ::
     318      move (lookup r) RegisterA
     319    | PUSH a ⇒
     320      move RegisterA (lookup_arg a) @
     321      [ PUSH … A ]
     322    | STORE addr1 addr2 srcr ⇒
     323      translate_store ? carry_lives_after
     324        (lookup_arg addr1)
     325        (lookup_arg addr2)
     326        (lookup_arg srcr)
     327    | LOAD dstr addr1 addr2 ⇒
     328      translate_load ? carry_lives_after
     329        (lookup dstr)
     330        (lookup_arg addr1)
     331        (lookup_arg addr2)
     332    | CLEAR_CARRY ⇒ CLEAR_CARRY …
     333    | SET_CARRY ⇒ CLEAR_CARRY …
     334    | OP2 op dst arg1 arg2 ⇒
     335      translate_op2_smart ? carry_lives_after op
     336        (lookup dst)
     337        (lookup_arg arg1)
     338        (lookup_arg arg2)
     339    | OP1 op dst arg ⇒
     340      translate_op1 ? carry_lives_after op
     341        (lookup dst)
     342        (lookup arg)
     343    | MOVE pair_regs ⇒
     344      let lookup_move_dst ≝ λx.match x return λ_.decision with
     345        [ PSD r ⇒ lookup r
     346        | HDW r ⇒ r
     347        ] in
     348      let dst ≝ lookup_move_dst (\fst pair_regs) in
     349      let src ≝
     350        match \snd pair_regs return λ_.arg_decision with
     351        [ Reg r ⇒ lookup_move_dst r
     352        | Imm b ⇒ arg_decision_imm b
     353        ] in
     354      move dst src
     355    | ADDRESS lbl prf dpl dph ⇒
     356      translate_address ? carry_lives_after
     357        lbl prf (lookup dpl) (lookup dph)
     358    | OPACCS op dst1 dst2 arg1 arg2 ⇒
     359      translate_opaccs ? carry_lives_after op
     360        (lookup dst1) (lookup dst2)
     361        (lookup_arg arg1) (lookup_arg arg2)
     362    | extension_seq ext ⇒
     363      match ext with
     364      [ ertl_new_frame ⇒ newframe ? stack_sz
     365      | ertl_del_frame ⇒ delframe ? stack_sz
     366      | ertl_frame_size r ⇒
     367        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
     368      ]
     369    | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
     370    | extension_call abs ⇒ match abs in void with [ ]
     371    ]
     372  | COND r ltrue ⇒
     373    〈move RegisterA (lookup r),COND … it ltrue〉
     374  ].
     375
     376definition translate_fin_step:
     377  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
     378  λglobals,lbl,s.
     379  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
     380  [ RETURN ⇒ RETURN ?
     381  | GOTO l ⇒ GOTO ? l
     382  | tailcall abs ⇒ match abs in void with [ ]
     383  ].
     384
     385definition translate_internal: ∀globals: list ident.
     386  joint_internal_function ERTL globals →
     387  joint_internal_function LTL globals ≝
    6388  λglobals: list ident.
    7   λluniv.
    8     fresh LabelTag luniv.
    9 
    10 definition ltl_statement_graph ≝
    11   λglobals.
    12     graph … (ltl_statement globals).
    13 
    14 definition add_graph ≝
    15   λglobals.
    16   λlabel.
    17   λstmt: ltl_statement globals.
    18   λgraph: ltl_statement_graph globals.
    19     add LabelTag ? graph label stmt.
    20 
    21 definition generate ≝
    22   λglobals: list ident.
    23   λluniv.
    24   λgraph: ltl_statement_graph globals.
    25   λstmt: ltl_statement globals.
    26   let 〈l, luniv〉 ≝ fresh_label globals luniv in
    27   let graph ≝ add_graph globals l stmt graph in
    28     〈l, graph, luniv〉.
    29 
    30 definition num_locals ≝
    31   λspilled_no.
    32   λglobals.
    33   λint_fun.
    34     spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    35 
    36 definition stacksize ≝
    37   λspilled_no.
    38   λglobals.
    39   λint_fun.
    40     spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
    41 
    42 definition adjust_off ≝
    43   λspilled_no.
    44   λglobals.
    45   λint_fun.
    46   λoff.
    47   let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    48   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in
    49     sub.
    50 
    51 definition get_stack:
    52  nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
    53   λspilled_no.
    54   λglobals: list ident.
    55   λint_fun.
    56   λgraph: graph (ltl_statement (globals)).
    57   λr.
    58   λoff.
    59   λl.
    60   λoriginal_label.
    61     let off ≝ adjust_off spilled_no globals int_fun off in
    62     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    63     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
    64     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in
    65     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
    66     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
    67     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
    68     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
    69     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    70       〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    71 
    72 definition set_stack:
    73   nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    74     → Register → label → ? ≝
    75   λspilled_no.
    76   λglobals: list ident.
    77   λint_fun.
    78   λgraph: graph (ltl_statement (globals)).
    79   λoff.
    80   λr.
    81   λl.
    82   λoriginal_label.
    83   let off ≝ adjust_off spilled_no globals int_fun off in
    84   let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    85   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
    86   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in
    87   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
    88   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
    89   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
    90   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
    91   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    92     〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    93 
    94 
    95 definition write ≝
    96   λglobals: list ident.
    97   λint_fun: ertl_internal_function globals.
    98   λvaluation.
    99   λcoloured_graph.
    100   λgraph.
    101   λr.
    102   λl.
    103   λoriginal_label: label.
    104   match colouring valuation coloured_graph (inl … r) with
    105   [ decision_spill off ⇒
    106     let luniv ≝ joint_if_luniverse … int_fun in
    107     let 〈graph, luniv〉 ≝ set_stack (spilled_no … coloured_graph) globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
    108       〈RegisterSST, l, graph, luniv〉
    109   | decision_colour hwr ⇒
    110     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    111       〈hwr, l, graph, luniv〉
    112   ].
    113 
    114 definition read ≝
    115   λglobals: list ident.
    116   λint_fun: ertl_internal_function globals.
    117   λvaluation.
    118   λcoloured_graph.
    119   λgraph.
    120   λr.
    121   λstmt.
    122   λoriginal_label: label.
    123   match colouring valuation coloured_graph (inl … r) with
    124   [ decision_colour hwr ⇒
    125     let luniv ≝ joint_if_luniverse … int_fun in
    126       〈add_graph globals original_label (stmt hwr) graph, luniv〉
    127   | decision_spill off ⇒
    128     let temphwr ≝ RegisterSST in
    129     let luniv ≝ joint_if_luniverse … int_fun in
    130     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
    131       get_stack (spilled_no … coloured_graph) globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
    132   ].
    133 
    134 definition move ≝
    135   λspilled_no.
    136   λglobals: list ident.
    137   λint_fun.
    138   λgraph: graph (ltl_statement globals).
    139   λdest: decision.
    140   λsrc: decision.
    141   λl: label.
    142   λoriginal_label: label.
    143   match dest with
    144   [ decision_colour dest_hwr ⇒
    145     match src with
    146     [ decision_colour src_hwr ⇒
    147       let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    148       if eq_Register dest_hwr src_hwr then
    149         〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    150       else
    151         let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
    152           〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
    153     | decision_spill src_off ⇒ get_stack spilled_no globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    154     ]
    155   | decision_spill dest_off ⇒
    156     match src with
    157     [ decision_colour src_hwr ⇒ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    158     | decision_spill src_off ⇒
    159       let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    160       if eq_nat dest_off src_off then
    161         〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    162       else
    163         let temp_hwr ≝ RegisterSST in
    164         let 〈graph, luniv〉 ≝ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
    165           get_stack spilled_no globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    166     ]
    167   ].
    168 
    169 definition newframe ≝
    170   λspilled_no.
    171   λglobals: list ident.
    172   λint_fun: ertl_internal_function globals.
    173   λgraph: ltl_statement_graph globals.
    174   λl: label.
    175   λoriginal_label: label.
    176   if eq_nat (stacksize spilled_no globals int_fun) 0 then
    177     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    178       〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    179   else
    180     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    181     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
    182     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
    183     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
    184     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
    185     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    186     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
    187     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
    188     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) in
    189       〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    190 
    191 definition delframe ≝
    192   λspilled_no.
    193   λglobals.
    194   λint_fun.
    195   λgraph: graph (ltl_statement globals).
    196   λl.
    197   λoriginal_label: label.
    198   if eq_nat (stacksize spilled_no globals int_fun) 0 then
    199     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    200       〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
    201   else
    202     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    203     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
    204     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
    205     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
    206     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    207     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    208       〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) graph, luniv〉.
    209 
    210 definition translate_statement:
    211   ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
    212     coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
    213       label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
    214   λglobals: list ident.
    215   λint_fun.
    216   λvaluation.
    217   λcoloured_graph: coloured_graph valuation.
    218   λgraph: ltl_statement_graph globals.
    219   λstmt: ertl_statement globals.
    220   λoriginal_label: label.
    221   match stmt with
    222   [ sequential seq l ⇒
    223     let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    224     match seq with
    225     [ COMMENT c ⇒
    226       〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
    227     | COST_LABEL cost_lbl ⇒
    228       〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
    229     | POP r ⇒
    230       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    231       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    232       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    233       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
    234         〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
    235     | PUSH r ⇒
    236       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
    237       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    238       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    239       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    240       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    241         〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    242     | COND srcr lbl_true ⇒
    243       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
    244       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    245       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    246       let int_fun' ≝ set_luniverse globals ? int_fun luniv in
    247       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    248         〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    249     | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
    250     | STORE addr1 addr2 srcr ⇒
    251       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
    252       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
    253       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
    254       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
    255       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
    256       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    257       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    258       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    259       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    260       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
    261       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    262       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    263       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    264       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    265       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
    266       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    267       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    268       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    269         〈add_graph globals original_label (GOTO … l) graph, luniv〉
    270     | LOAD destr addr1 addr2 ⇒
    271       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    272       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    273       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    274       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
    275       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
    276       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
    277       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
    278       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
    279       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    280       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    281       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    282       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    283       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
    284       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    285       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    286       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    287       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    288         〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    289     | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
    290     | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
    291     | OP2 op2 destr srcr1 srcr2 ⇒
    292       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    293       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    294       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    295       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
    296       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
    297       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    298       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    299       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    300       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
    301       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    302       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    303       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    304         〈add_graph globals original_label (GOTO … l) graph, luniv〉
    305     | OP1 op1 destr srcr ⇒
    306       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    307       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    308       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    309       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
    310       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
    311       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    312       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    313       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    314       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
    315         〈add_graph globals original_label (GOTO … l) graph, luniv〉
    316     | INT r i ⇒
    317       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    318       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    319       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    320         〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
    321     | MOVE pair_regs ⇒
    322       let regl ≝ \fst pair_regs in
    323       let regr ≝ \snd pair_regs in
    324       match regl with
    325       [ pseudo p1  ⇒
    326         match regr with
    327         [ pseudo p2  ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
    328         | hardware h ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
    329         ]
    330       | hardware h1 ⇒
    331         match regr with
    332         [ pseudo p    ⇒ move (spilled_no … coloured_graph) globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    333         | hardware h2 ⇒
    334           let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
    335             〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
    336         ]
    337       ]
    338     | ADDRESS lbl prf dpl dph ⇒
    339       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    340       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    341       let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
    342       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
    343       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
    344       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
    345       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    346       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    347       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    348       let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
    349       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
    350       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
    351         〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
    352     | extension ext ⇒
    353       match ext with
    354       [ ertl_st_ext_new_frame ⇒ newframe (spilled_no … coloured_graph)globals int_fun graph l original_label
    355       | ertl_st_ext_del_frame ⇒ delframe (spilled_no … coloured_graph) globals int_fun graph l original_label
    356       | ertl_st_ext_frame_size r ⇒
    357         let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    358         let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    359         let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    360           〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize (spilled_no … coloured_graph) … int_fun))) l) graph, luniv〉
    361       ]
    362     | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    363       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    364       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
    365       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
    366       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in
    367       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    368       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    369       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    370       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
    371       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
    372       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    373       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    374       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    375       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
    376         〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
    377     ]
    378   | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    379   | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    380   ].
    381 
    382 definition graph_fold ≝
    383   λglobals.
    384   λb : Type[0].
    385   λf    : label → ertl_statement globals → b → b.
    386   λgraph: graph (ertl_statement globals).
    387   λseed : b.
    388     foldi (ertl_statement globals) b ? f graph seed.
    389 
    390 definition translate_internal: ∀globals: list ident.
    391   ertl_internal_function globals → ltl_internal_function globals ≝
    392   λglobals: list ident.
    393   λint_fun: ertl_internal_function globals.
    394   let graph ≝ (empty_map … : ltl_statement_graph globals) in
    395   let valuation ≝ analyse globals int_fun in
    396   let coloured_graph ≝ build valuation in
    397   let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
    398     let 〈graph, luniv〉 ≝ graph_luniv in
    399       match eliminable globals (valuation label) stmt with
    400       [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
    401       | None           ⇒
    402         translate_statement globals int_fun valuation coloured_graph graph stmt label
    403       ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
    404   in
    405     match joint_if_entry … int_fun with
    406     [ mk_Sig entry_label entry_label_prf ⇒
    407       match joint_if_exit … int_fun with
    408       [ mk_Sig exit_label exit_label_prf ⇒
    409           mk_joint_internal_function globals (ltl_params globals)
    410             luniv (joint_if_runiverse … int_fun)
    411               it it it (joint_if_stacksize … int_fun)
    412                 graph ? ?
    413       ]
    414     ].
    415   [1: %
    416     [1: @entry_label
    417     |2: cases daemon (* XXX *)
    418     ]
    419   |2: %
    420     [1: @exit_label
    421     |2: cases daemon (* XXX *)
    422     ]
    423   ]
    424 qed.
     389  λint_fun: joint_internal_function ERTL globals.
     390  (* initialize graph *)
     391  let entry ≝ pi1 … (joint_if_entry … int_fun) in
     392  let exit ≝ pi1 … (joint_if_exit … int_fun) in
     393  (* colour registers *)
     394  let after ≝ analyse_liveness globals int_fun in
     395  let coloured_graph ≝ build after in
     396  (* compute new stack size *)
     397  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
     398  (* initialize internal function *)
     399  let init ≝ init_graph_if LTL globals
     400    (joint_if_luniverse … int_fun)
     401    (joint_if_runiverse … int_fun)
     402    it it [ ] stack_sz entry exit in
     403  graph_translate …
     404    init
     405    (translate_step … coloured_graph stack_sz)
     406    (translate_fin_step …)
     407    int_fun.
    425408
    426409definition ertl_to_ltl: ertl_program → ltl_program ≝
  • src/ERTL/Interference.ma

    r1730 r2286  
    1 include "ERTL/ERTL.ma".
    21include "ERTL/liveness.ma".
    3 
    4 definition vertex ≝ register ⊎ Register.
    52
    63inductive decision: Type[0] ≝
    74  | decision_spill: nat → decision
    85  | decision_colour: Register → decision.
    9 
    10 definition is_member ≝
    11   λvertex.
    12   λregister_lattice.
    13   let 〈l, r〉 ≝ register_lattice in
    14   match vertex with
    15   [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
    16   | inr v ⇒ set_member ? eq_Register v r
    17   ].
    186
    197(* prop_colouring is the non interferece
     
    2210(* Wilmer: the generation of the destruct principle diverges;
    2311   Ctr-C make the file pass *)
    24 record coloured_graph (v: valuation): Type[1] ≝
     12record coloured_graph (after: valuation register_lattice): Type[1] ≝
    2513{ colouring: vertex → decision
    2614; spilled_no: nat
    2715; prop_colouring: ∀l. ∀v1, v2: vertex.
    28    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
    29 ; prop_colouring2: (*CSC: the exist-guarded premise is just to make the proof more general *)
    30    ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no
    31 (* CSC: useless for the proof and very weak
    32 ; prop_colouring3:
    33    spilled_no = 0 ∨
    34     ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1)
    35 *)
     16  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
     17; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
     18   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
    3619}.
    3720
  • src/ERTL/liveness.ma

    r1995 r2286  
     1
    12include "ASM/Util.ma".
    23include "ERTL/ERTL.ma".
    34include "utilities/adt/set_adt.ma".
    4 
    5 definition statement_successors ≝
    6   λglobals: list ident.
    7   λs: ertl_statement globals.
     5include "utilities/fixpoints.ma".
     6
     7definition register_lattice : property_lattice ≝
     8mk_property_lattice
     9 ((set register) × (set Register))
     10 〈set_empty …, set_empty …〉
     11 (λleft.
     12  λright.
     13  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
     14  set_equal … eq_Register (\snd left) (\snd right))
     15 (λleft.
     16  λright.
     17  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
     18  set_subset … eq_Register (\snd left) (\snd right))
     19 (λ_.false).
     20
     21definition rl_bottom ≝ l_bottom register_lattice.
     22definition rl_psingleton: register → register_lattice ≝
     23  λr.
     24    〈set_singleton … r, set_empty …〉.
     25definition rl_hsingleton: Register → register_lattice ≝
     26  λr.
     27    〈set_empty …, set_singleton … r〉.
     28
     29definition rl_join: register_lattice → register_lattice → register_lattice ≝
     30  λleft.
     31  λright.
     32  let 〈lp, lh〉 ≝ left in
     33  let 〈rp, rh〉 ≝ right in
     34    〈set_union … lp rp, set_union … lh rh〉.
     35
     36definition rl_diff: register_lattice → register_lattice → register_lattice ≝
     37  λleft.
     38  λright.
     39  let 〈lp, lh〉 ≝ left in
     40  let 〈rp, rh〉 ≝ right in
     41    〈set_diff … lp rp, set_diff … lh rh〉.
     42
     43definition defined ≝
     44  λglobals: list ident.
     45  λs: joint_statement ERTL globals.
    846  match s with
    947  [ sequential seq l ⇒
    1048    match seq with
    11     [ COND acc_a_reg lbl_true ⇒
    12         set_insert … lbl_true (set_singleton … l)
    13     | _ ⇒ set_singleton … l ]
    14   | GOTO l ⇒ set_singleton … l
    15   | RETURN ⇒ set_empty ?
    16   ].
    17 
    18 definition register_lattice ≝ (set register) × (set Register).
    19 definition lattice_property ≝ register_lattice.
    20 definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    21 definition lattice_psingleton: register → register_lattice ≝
    22   λr.
    23     〈set_singleton … r, set_empty …〉.
    24 definition lattice_hsingleton: Register → register_lattice ≝
    25   λr.
    26     〈set_empty …, set_singleton … r〉.
    27 
    28 definition lattice_join: register_lattice → register_lattice → register_lattice ≝
    29   λleft.
    30   λright.
    31   let 〈lp, lh〉 ≝ left in
    32   let 〈rp, rh〉 ≝ right in
    33     〈set_union … lp rp, set_union … lh rh〉.
    34 
    35 definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
    36   λleft.
    37   λright.
    38   let 〈lp, lh〉 ≝ left in
    39   let 〈rp, rh〉 ≝ right in
    40     〈set_diff … lp rp, set_diff … lh rh〉.
    41 
    42 definition lattice_equal: register_lattice → register_lattice → bool ≝
    43   λleft.
    44   λright.
    45   let 〈lp, lh〉 ≝ left in
    46   let 〈rp, rh〉 ≝ right in
    47     andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    48 
    49 definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    50 
    51 record lattice_property_sig: Type[1] ≝
    52 {
    53   lp_type      : Type[0];
    54   lp_property  : Type[0];
    55   lp_bottom    : lp_type;
    56   lp_psingleton: register → lp_type;
    57   lp_hsingleton: Register → lp_type;
    58   lp_join      : lp_type → lp_type → lp_type;
    59   lp_diff      : lp_type → lp_type → lp_type;
    60   lp_equal     : lp_type → lp_type → bool;
    61   lp_is_maximal: lp_type → bool
    62 }.
    63 
    64 definition property ≝
    65   mk_lattice_property_sig
    66     ((set register) × (set Register))
    67     lattice_property
    68     lattice_bottom
    69     lattice_psingleton
    70     lattice_hsingleton
    71     lattice_join
    72     lattice_diff
    73     lattice_equal
    74     lattice_is_maximal.
    75 
    76 definition defined ≝
    77   λglobals: list ident.
    78   λs: ertl_statement globals.
     49    [ step_seq s ⇒
     50      match s with
     51      [ OP2 op2 r1 r2 _ ⇒
     52        match op2 with
     53        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
     54        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
     55        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
     56        | _ ⇒ rl_psingleton r1
     57        ]
     58      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
     59      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
     60      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     61        rl_join (rl_join (rl_psingleton dr1)
     62                                    (rl_psingleton dr2))
     63                      (rl_hsingleton RegisterCarry)
     64      | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     65      | POP r ⇒ rl_psingleton r
     66      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     67      | LOAD r _ _ ⇒ rl_psingleton r
     68      | COMMENT c ⇒ rl_bottom
     69      | STORE acc_a dpl dph ⇒ rl_bottom
     70      | COST_LABEL clabel ⇒ rl_bottom
     71      | PUSH r ⇒ rl_bottom
     72      | MOVE pair_reg ⇒
     73        (* first register relevant only *)
     74        match \fst pair_reg with
     75        [ PSD p ⇒ rl_psingleton p
     76        | HDW h ⇒ rl_hsingleton h
     77        ]
     78      | extension_seq ext ⇒
     79        match ext with
     80        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     81        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     82        | ertl_frame_size r ⇒ rl_psingleton r
     83        ]
     84      (* Potentially destroys all caller-save hardware registers. *)
     85      | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     86      | extension_call abs ⇒ match abs in void with [ ]
     87      ]
     88    | COND r lbl_true ⇒ rl_bottom
     89    ]
     90  | final _ ⇒ rl_bottom
     91  ].
     92
     93definition ret_regs ≝ set_from_list … RegisterRets.
     94
     95definition rl_arg : psd_argument → register_lattice ≝
     96  λarg.match arg with
     97  [ Imm _ ⇒ rl_bottom
     98  | Reg r ⇒ rl_psingleton r
     99  ].
     100
     101definition used ≝
     102  λglobals: list ident.
     103  λs: joint_statement ERTL globals.
    79104  match s with
    80105  [ sequential seq l ⇒
    81106    match seq with
    82     [ OP2 op2 r1 r2 _ ⇒
    83       match op2 with
    84       [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
    85       | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
    86       | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry)  (lattice_psingleton r1)
    87       | _ ⇒ lattice_psingleton r1
     107    [ step_seq s ⇒
     108      match s with
     109      [ OP2 op2 acc_a r1 r2 ⇒
     110        rl_join (rl_join (rl_arg r1) (rl_arg r2))
     111          (match op2 with
     112            [ Addc ⇒ rl_hsingleton RegisterCarry
     113            | Sub ⇒ rl_hsingleton RegisterCarry
     114            | _ ⇒ rl_bottom
     115            ])
     116      (* acc_a and acc_b *)
     117      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     118        rl_join (rl_arg sr1) (rl_arg sr2)
     119      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
     120      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
     121      | STORE acc_a dpl dph ⇒
     122        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
     123      | PUSH r ⇒ rl_arg r
     124      | MOVE pair_reg ⇒
     125        let r2 ≝ \snd pair_reg in
     126        match r2 with
     127        [ Reg p ⇒
     128          match p with
     129          [ PSD r ⇒ rl_psingleton r
     130          | HDW r ⇒ rl_hsingleton r
     131          ]
     132        | Imm _ ⇒ rl_bottom
     133        ]
     134      | extension_seq ext ⇒
     135        match ext with
     136        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     137        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     138        | ertl_frame_size r ⇒ rl_bottom
     139        ]
     140      (* Reads the hardware registers that are used to pass parameters. *)
     141      | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     142      | extension_call abs ⇒ match abs in void with [ ]
     143      | _ ⇒ rl_bottom
    88144      ]
    89     | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
    90     | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
    91     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    92        lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
    93     | OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    94     | POP r ⇒ lattice_psingleton r
    95     | INT r _ ⇒ lattice_psingleton r
    96     | ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    97     | LOAD r _ _ ⇒ lattice_psingleton r
    98     (* Potentially destroys all caller-save hardware registers. *)
    99     | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    100     | COMMENT c ⇒ lattice_bottom
    101     | COND r lbl_true ⇒ lattice_bottom
    102     | STORE acc_a dpl dph ⇒ lattice_bottom
    103     | COST_LABEL clabel ⇒ lattice_bottom
    104     | PUSH r ⇒ lattice_bottom
    105     | MOVE pair_reg ⇒
    106       (* first register relevant only *)
    107       let r1 ≝ \fst pair_reg in
    108       match r1 with
    109       [ pseudo p ⇒ lattice_psingleton p
    110       | hardware h ⇒ lattice_hsingleton h
    111       ]
    112     | extension ext ⇒
    113       match ext with
    114       [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    115       | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    116       | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
    117   | RETURN ⇒ lattice_bottom
    118   | GOTO l ⇒ lattice_bottom
    119   ].
    120 
    121 definition ret_regs ≝ set_from_list … RegisterRets.
    122 
    123 definition used ≝
    124   λglobals: list ident.
    125   λs: ertl_statement globals.
     145    | COND r lbl_true ⇒ rl_psingleton r
     146    ]
     147  | final fin ⇒
     148    match fin with
     149    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     150    | GOTO l ⇒ rl_bottom
     151    | tailcall abs ⇒ match abs in void with [ ]
     152    ]
     153  ].
     154
     155definition eliminable ≝
     156  λglobals: list ident.
     157  λl: register_lattice.
     158  λs: joint_statement ERTL globals.
     159  let pliveafter ≝ \fst l in
     160  let hliveafter ≝ \snd l in
    126161  match s with
    127162  [ sequential seq l ⇒
    128163    match seq with
    129     [ OP2 op2 acc_a r1 r2 ⇒
    130       match op2 with
    131       [ Addc ⇒
    132         lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    133       | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     164    [ step_seq s ⇒
     165      match s with
     166      [ OP2 op2 r1 r2 r3 ⇒
     167        if match op2 with
     168          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
     169          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
     170          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
     171          | _ ⇒ false
     172          ] ∨ set_member … (eq_identifier …) r1 pliveafter
     173        then
     174          None ?
     175        else
     176          Some ? l
     177      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     178        if set_member … (eq_identifier …) dr1 pliveafter ∨
     179           set_member … (eq_identifier …) dr2 pliveafter ∨
     180           set_member … eq_Register RegisterCarry hliveafter then
     181          None ?
     182        else
     183          Some ? l
     184      | OP1 op1 r1 r2 ⇒
     185        if set_member … (eq_identifier …) r1 pliveafter then
     186          None ?
     187        else
     188          Some ? l
     189      | ADDRESS _ _ r1 r2 ⇒
     190        if set_member … (eq_identifier …) r1 pliveafter ∨
     191           set_member … (eq_identifier …) r2 pliveafter then
     192          None ?
     193        else
     194          Some ? l
     195      | LOAD acc_a dpl dph ⇒
     196        if set_member ? (eq_identifier …) acc_a pliveafter then
     197          None ?
     198        else
     199          Some ? l
     200      | MOVE pair_reg ⇒
     201        if match \fst pair_reg with
     202          [ PSD p1 ⇒
     203            set_member … (eq_identifier …) p1 pliveafter
     204          | HDW h1 ⇒
     205            set_member … eq_Register h1 hliveafter
     206          ] then
     207            None ?
     208          else
     209            Some ? l
     210      | extension_seq ext ⇒
     211        match ext with
     212        [ ertl_new_frame ⇒ None ?
     213        | ertl_del_frame ⇒ None ?
     214        | ertl_frame_size r ⇒
     215          if set_member ? (eq_identifier RegisterTag) r pliveafter then
     216            None ?
     217          else
     218            Some ? l
     219        ]
     220      | _ ⇒ None ?
    134221      ]
    135     | CLEAR_CARRY ⇒ lattice_bottom
    136     | SET_CARRY ⇒ lattice_bottom
    137     (* acc_a and acc_b *)
    138     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    139        lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
    140     | OP1 op1 r1 r2 ⇒ lattice_psingleton r2
    141     | POP r ⇒ lattice_bottom
    142     | INT r _ ⇒ lattice_bottom
    143     | ADDRESS _ _ r1 r2 ⇒ lattice_bottom
    144     | LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    145     (* Reads the hardware registers that are used to pass parameters. *)
    146     | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    147     | COMMENT c ⇒ lattice_bottom
    148     | COND r lbl_true ⇒ lattice_psingleton r
    149     | STORE acc_a dpl dph ⇒
    150       lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    151     | COST_LABEL clabel ⇒ lattice_bottom
    152     | PUSH r ⇒ lattice_psingleton r
    153     | MOVE pair_reg ⇒
    154       let r2 ≝ \snd pair_reg in
    155       match r2 with
    156       [ pseudo p ⇒ lattice_psingleton p
    157       | hardware h ⇒ lattice_hsingleton h
    158       ]
    159   | extension ext ⇒
    160     match ext with
    161     [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    162     | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    163     | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    164   | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    165   | GOTO l ⇒ lattice_bottom
    166   ].
    167 
    168 definition eliminable ≝
    169   λglobals: list ident.
    170   λl: register_lattice.
    171   λs: ertl_statement globals.
    172   let 〈pliveafter, hliveafter〉 ≝ l in
    173   match s with
    174   [ sequential seq l ⇒
    175     match seq with
    176     [ OP2 op2 r1 r2 r3 ⇒
    177       if set_member … (eq_identifier …) r1 pliveafter ∨
    178          set_member … eq_Register RegisterCarry hliveafter then
    179         None ?
    180       else
    181         Some ? l
    182     | CLEAR_CARRY ⇒ None ?
    183     | SET_CARRY ⇒ None ?
    184     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    185       if set_member … (eq_identifier …) dr1 pliveafter ∨
    186          set_member … (eq_identifier …) dr2 pliveafter ∨
    187          set_member … eq_Register RegisterCarry hliveafter then
    188         None ?
    189       else
    190         Some ? l
    191     | OP1 op1 r1 r2 ⇒
    192       if set_member … (eq_identifier …) r1 pliveafter ∨
    193          set_member … eq_Register RegisterCarry hliveafter then
    194         None ?
    195       else
    196         Some ? l
    197     | POP r ⇒ None ?
    198     | INT r _ ⇒
    199       if set_member … (eq_identifier …) r pliveafter ∨
    200          set_member … eq_Register RegisterCarry hliveafter then
    201         None ?
    202       else
    203         Some ? l
    204     | ADDRESS _ _ r1 r2 ⇒
    205       if set_member … (eq_identifier …) r1 pliveafter ∨
    206          set_member … (eq_identifier …) r2 pliveafter ∨
    207          set_member … eq_Register RegisterCarry hliveafter then
    208         None ?
    209       else
    210         Some ? l
    211     | LOAD acc_a dpl dph ⇒
    212       if set_member ? (eq_identifier …) acc_a pliveafter ∨
    213          set_member … eq_Register RegisterCarry hliveafter then
    214         None ?
    215       else
    216         Some ? l
    217     | CALL_ID _ nparams _ ⇒ None ?
    218     | COMMENT c ⇒ None ?
    219     | COND r lbl_true ⇒ None ?
    220     | STORE acc_a dpl dph ⇒ None ?
    221     | COST_LABEL clabel ⇒ None ?
    222     | PUSH r ⇒ None ?
    223     | MOVE pair_reg ⇒
    224       let r1 ≝ \fst pair_reg in
    225       let r2 ≝ \snd pair_reg in
    226       match r1 with
    227       [ pseudo p1 ⇒
    228         if set_member … (eq_identifier …) p1 pliveafter ∨
    229            set_member … eq_Register RegisterCarry hliveafter then
    230           None ?
    231         else
    232           Some ? l
    233       | hardware h1 ⇒
    234         if set_member … eq_Register h1 hliveafter then
    235           None ?
    236         else
    237           Some ? l]
    238     | extension ext ⇒
    239       match ext with
    240       [ ertl_st_ext_new_frame ⇒ None ?
    241       | ertl_st_ext_del_frame ⇒ None ?
    242       | ertl_st_ext_frame_size r ⇒
    243         if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    244            set_member ? eq_Register RegisterCarry hliveafter then
    245           None ?
    246         else
    247           Some ? l]]
    248   | GOTO l ⇒ None ?
    249   | RETURN ⇒ None ?
    250   ].
    251 
    252 definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
     222    | COND _ _ ⇒ None ?
     223    ]
     224  | _ ⇒ None ?
     225  ].
     226
     227definition statement_semantics: ∀globals: list ident.
     228  joint_statement ERTL globals → register_lattice → register_lattice ≝
    253229  λglobals.
    254230  λstmt.
    255231  λliveafter.
    256232  match eliminable globals liveafter stmt with
    257   [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
     233  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
    258234  | Some l ⇒ liveafter
    259235  ].
    260236
    261 definition valuation ≝ label → register_lattice.
    262 definition rhs ≝ valuation → lattice_property.
    263 definition equations ≝ label → rhs.
    264 
    265237definition livebefore ≝
    266238  λglobals: list ident.
    267   λint_fun: ertl_internal_function globals.
     239  λint_fun: joint_internal_function ERTL globals.
    268240  λlabel.
    269   λliveafter: valuation.
    270   match lookup (joint_if_code … int_fun) label with
    271   [ None      ⇒ ?
     241  λliveafter: valuation register_lattice.
     242  match lookup ?? (joint_if_code … int_fun) label with
     243  [ None      ⇒ rl_bottom
    272244  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    273245  ].
    274   cases not_implemented (* XXX *)
    275 qed.
    276246
    277247definition liveafter ≝
    278   λglobals: list ident.
    279   λint_fun: ertl_internal_function globals.
     248   λglobals: list ident.
     249  λint_fun: joint_internal_function ERTL globals.
    280250  λlabel.
    281   λliveafter: valuation.
    282   match lookup … (joint_if_code … int_fun) label with
    283   [ None      ⇒ ?
    284   | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    285       lattice_join (livebefore globals int_fun successor liveafter) accu)
    286       (statement_successors globals stmt) lattice_bottom
    287   ].
    288   cases not_implemented (* XXX *)
    289 qed.
    290 
    291 record fixpoint: Type[0] ≝
    292 {
    293   (* XXX: this never fails to compute a fixed point as in any program we will
    294           only ever use a finite number of pseudoregisters, therefore no chain
    295           conditions, etc. are necessary for this to terminate with a correct
    296           solution. *)
    297   fix_lfp    :1> equations → valuation;
    298   fix_correct:
    299     ∀globals: list ident.
    300 (*    ∀int_fun.*)
    301     ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
    302       ∀v: label.
    303         lattice_equal (f v (fix_lfp f)) (fix_lfp f v) (*CSC: TOO STRONG: WE ONLY NEED CORRECTNESS NOT COMPLETENESS *)
    304 }.
    305 
    306 axiom the_fixpoint: fixpoint.
    307 
    308 definition analyse ≝
     251  λliveafter: valuation register_lattice.
     252 match lookup ?? (joint_if_code … int_fun) label with
     253  [ None      ⇒ rl_bottom
     254  | Some stmt ⇒
     255    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
     256      (livebefore globals int_fun successor liveafter)
     257  ].
     258
     259definition analyse_liveness ≝
    309260  λglobals.
    310261  λint_fun.
    311     the_fixpoint (liveafter globals int_fun).
     262    the_fixpoint ? (liveafter globals int_fun).
     263
     264definition vertex ≝ register + Register.
     265
     266definition plives : register → register_lattice → bool ≝
     267  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
     268definition hlives : Register → register_lattice → bool ≝
     269  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
     270
     271definition lives : vertex → register_lattice → bool ≝
     272  λvertex.
     273  match vertex with
     274  [ inl v ⇒ plives v
     275  | inr v ⇒ hlives v
     276  ].
  • src/ERTL/semantics.ma

    r2041 r2286  
    33include alias "common/Identifiers.ma".
    44
     5record ertl_psd_env : Type[0] ≝
     6  { psd_regs : register_env beval
     7  (* this tells what pseudo-registers should have their value corrected by spilled_no *)
     8  ; need_spilled_no : identifier_set RegisterTag
     9  }.
     10
     11definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
     12definition add_need_spilled_no ≝
     13  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
     14definition rm_need_spilled_no ≝
     15  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
     16
     17definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
     18
    519definition ps_reg_store ≝
    6  λr,v.λlocal_env:(register_env beval) × hw_register_env.
    7   do res ← reg_store r v (\fst local_env) ;
    8   OK … 〈res, \snd local_env〉.
     20 λr,v.λlocal_env : ertl_reg_env.
     21  do res ← reg_store r v (psd_regs (\fst local_env)) ;
     22  let psd_env ≝ set_psd_regs res (\fst local_env) in
     23  OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
    924
    1025definition ps_reg_retrieve ≝
    11  λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
     26 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
    1227
    1328definition hw_reg_store ≝
    14  λr,v.λlocal_env:(register_env beval) × hw_register_env.
     29 λr,v.λlocal_env:ertl_reg_env.
    1530  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
    1631
    1732definition hw_reg_retrieve ≝
    18  λlocal_env:(register_env beval) × hw_register_env.λreg.
     33 λlocal_env:ertl_reg_env.λreg.
    1934  OK … (hwreg_retrieve … (\snd local_env) reg).
    2035
    21 definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    22  mk_more_sem_params ertl_params_
    23   (list (register_env beval)) [] ((register_env beval) × hw_register_env)
    24    (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
    25    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    26     ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    27      (λlocals,dest_src.
    28        do v ←
    29         match \snd dest_src with
    30         [ pseudo reg ⇒ ps_reg_retrieve locals reg
    31         | hardware reg ⇒ hw_reg_retrieve locals reg] ;
    32        match \fst dest_src with
    33        [ pseudo reg ⇒ ps_reg_store reg v locals
    34        | hardware reg ⇒ hw_reg_store reg v locals]).
    35 definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
     36definition ps_arg_retrieve ≝
     37  λlocal_env,a.
     38  match a with
     39  [ Reg r ⇒ ps_reg_retrieve local_env r
     40  | Imm b ⇒ return b
     41  ].
    3642
    37 definition ertl_init_locals :
    38  list register →
    39   (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
    40  λlocals,lenv.
    41   〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
     43definition ERTL_state : sem_state_params ≝
     44  mk_sem_state_params
     45 (* framesT ≝ *) (list ertl_psd_env)
     46 (* empty_framesT ≝ *) [ ]
     47 (* regsT ≝ *) ertl_reg_env
     48 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).
    4249
    43 (*CSC: could we use here a dependent type to avoid the Error case? *)
    44 axiom EmptyStack: String.
    45 definition ertl_pop_frame:
    46  ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    47  λglobals,ge,st.
    48   let frms ≝ st_frms ? st in
    49   match frms with
    50   [ nil ⇒ Error ? [MSG EmptyStack]
    51   | cons hd tl ⇒
    52      OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
     50(* we ignore need_spilled_no as we never move framesize based values around in the
     51   translation *)
     52definition ertl_eval_move ≝ λenv,pr.
     53      ! v ←
     54        match \snd pr with
     55        [ Reg src ⇒
     56          match src with
     57          [ PSD r ⇒ ps_reg_retrieve env r
     58          | HDW r ⇒ hw_reg_retrieve env r
     59          ]
     60        | Imm bv ⇒ return bv ] ;
     61      match \fst pr with
     62      [ PSD r ⇒ ps_reg_store r v env
     63      | HDW r ⇒ hw_reg_store r v env
     64      ].
     65
     66definition ertl_allocate_local ≝
     67  λreg.λlenv : ertl_reg_env.
     68  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
    5369
    5470definition ertl_save_frame:
    55  address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    56  λl.λ_.λ_.λ_.λ_.λst.
    57   do st ← save_ra … st l ;
     71 cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
     72 λpc.λ_.λst.
     73  do st ← save_ra … st pc ;
    5874  OK …
    59    (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
    60     (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    61 
    62 definition ertl_result_regs:
    63  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
    64  λglobals,ge,st.
    65   do fn ← graph_fetch_function … globals ge st ;
    66   OK … (joint_if_result … fn).
     75   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
     76    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
    6777
    6878(*CSC: XXXX, for external functions only*)
    69 axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
    70 axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
     79axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
     80axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
     81(* I think there should be a list beval in place of list val here
     82  λvals.λ_.λst.
     83  (* set all RegisterRets to 0 *)
     84  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
     85  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
     86  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
     87  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
     88  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    7189
    72 definition framesize:
    73  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
    74   λglobals,ge,st.
    75    do f ← graph_fetch_function … ge st ;
    76    OK ? (joint_if_stacksize globals … f).
     90definition xdata_pointer_of_address: address → res xpointer ≝
     91λp.let 〈v1,v2〉 ≝ p in
     92! p ← pointer_of_bevals [v1;v2] ;
     93match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
     94[ XData ⇒ λE.OK ? (mk_Sig … p E)
     95| _ ⇒ λ_.Error … [MSG BadPointer]
     96] (refl …).
    7797
    78 definition get_hwsp : state ertl_sem_params → address ≝
     98definition address_of_xdata_pointer: xpointer → address ≝
     99λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
     100
     101definition get_hwsp : ERTL_state → res xpointer ≝
    79102 λst.
    80103  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    81104  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    82   〈spl,sph〉.
     105  xdata_pointer_of_address 〈spl,sph〉.
    83106
    84 definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params
     107definition set_hwsp : xpointer → ERTL_state → ERTL_state
    85108 λsp,st.
    86   let 〈spl,sph〉 ≝ sp in
     109  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    87110  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    88111  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    89   set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
     112  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    90113
    91 definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
    92  λglobals.
    93   mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    94     (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    95     ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    96     ertl_fetch_external_args ertl_set_result.
    97 definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
    98  λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).
     114definition eval_ertl_seq:
     115 ∀globals. genv ERTL globals →
     116  ertl_seq → joint_internal_function ERTL globals → ERTL_state →
     117   IO io_out io_in ERTL_state ≝
     118 λglobals,ge,stm,curr_fn,st.
     119 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
     120  match stm with
     121   [ ertl_new_frame ⇒
     122      ! sp ← get_hwsp st ;
     123      let newsp ≝ shift_pointer … sp framesize in
     124      return set_hwsp newsp st
     125   | ertl_del_frame ⇒
     126      ! sp ← get_hwsp st ;
     127      let newsp ≝ shift_pointer … sp framesize in
     128      return set_hwsp newsp st
     129   | ertl_frame_size dst ⇒
     130      let env ≝ regs … st in
     131      ! env' ← ps_reg_store dst (BVByte framesize) env ;
     132      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
     133      return set_regs ERTL_state env'' st
     134   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    99135
    100 definition ertl_exec_extended:
    101  ∀globals. genv globals (ertl_params globals) →
    102   ertl_statement_extension → label → state ertl_sem_params →
    103    IO io_out io_in (trace × (state ertl_sem_params)) ≝
    104  λglobals,ge,stm,l,st.
    105   match stm with
    106    [ ertl_st_ext_new_frame ⇒
    107       ! v ← framesize globals … ge st;
    108       let sp ≝ get_hwsp st in
    109       ! newsp ← addr_sub sp v;
    110       let st ≝ set_hwsp newsp st in
    111       ! st ← next … (ertl_sem_params1 globals) l st ;
    112         return 〈E0,st〉
    113    | ertl_st_ext_del_frame ⇒
    114       ! v ← framesize … ge st;
    115       let sp ≝ get_hwsp st in
    116       ! newsp ← addr_add sp v;
    117       let st ≝ set_hwsp newsp st in
    118       ! st ← next … (ertl_sem_params1 …) l st ;
    119         return 〈E0,st〉
    120    | ertl_st_ext_frame_size dst ⇒
    121       ! v ← framesize … ge st;
    122       ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    123       ! st ← next … (ertl_sem_params1 …) l st ;
    124         return 〈E0, st〉
    125    ].
     136definition ertl_post_op2 ≝
     137  λop,dst,arg1,arg2,st.
     138  let local_env ≝ regs ERTL_state st in
     139  let f ≝ λarg,st.match arg with
     140     [ Reg r ⇒
     141       if r ∈ need_spilled_no (\fst local_env) then
     142         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
     143       else
     144         st
     145     | _ ⇒ st
     146     ] in
     147  match op with
     148  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
     149  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
     150  | Sub ⇒ f arg1 st
     151  | _ ⇒ st].
     152         
    126153
    127 definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    128  λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).
    129 
    130 definition ertl_fullexec: fullexec io_out io_in ≝
    131  joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
     154definition ERTL_semantics ≝
     155  make_sem_graph_params ERTL
     156  (mk_more_sem_unserialized_params ??
     157  (* st_pars            ≝ *) ERTL_state
     158  (* acca_store_        ≝ *) ps_reg_store
     159  (* acca_retrieve_     ≝ *) ps_reg_retrieve
     160  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
     161  (* accb_store_        ≝ *) ps_reg_store
     162  (* accb_retrieve_     ≝ *) ps_reg_retrieve
     163  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
     164  (* dpl_store_         ≝ *) ps_reg_store
     165  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
     166  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
     167  (* dph_store_         ≝ *) ps_reg_store
     168  (* dph_retrieve_      ≝ *) ps_reg_retrieve
     169  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
     170  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
     171  (* pair_reg_move_     ≝ *) ertl_eval_move
     172  (* fetch_ra           ≝ *) (load_ra …)
     173  (* allocate_local     ≝ *) ertl_allocate_local
     174  (* save_frame         ≝ *) ertl_save_frame
     175  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     176  (* fetch_external_args≝ *) ertl_fetch_external_args
     177  (* set_result         ≝ *) ertl_set_result
     178  (* call_args_for_main ≝ *) 0
     179  (* call_dest_for_main ≝ *) it
     180  (* read_result        ≝ *) (λ_.λ_.λ_.
     181     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
     182  (* eval_ext_seq       ≝ *) eval_ertl_seq
     183  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     184  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     185  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     186  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).
Note: See TracChangeset for help on using the changeset viewer.