Changeset 2208


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (5 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
Location:
src
Files:
1 added
10 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL_paolo.ma

    r2175 r2208  
    1414  | arg_decision_colour : Register → arg_decision
    1515  | arg_decision_spill : ℕ → arg_decision
    16   | arg_decision_imm : Byte → arg_decision.
     16  | arg_decision_imm : beval → arg_decision.
    1717
    1818coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
     
    3535  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
    3636
     37(* for notation *)
     38definition A ≝ it.
     39
     40coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.
     41
     42(* spill should be byte-based from the start *)
    3743definition set_dp_by_offset :
    38   ∀globals.Byte → list (joint_seq ltl_params globals) ≝
     44  ∀globals.nat → list (joint_seq ltl_params globals) ≝
    3945  λglobals,off.
    40   [ 𝐀 ← off
    41   ; 𝐀 ← 𝐀 .Add. RegisterSPL
    42   ; RegisterDPL ← 𝐀
    43   ; 𝐀 ← 0
    44   ; 𝐀 ← 𝐀 .Addc. RegisterSPH
    45   ; RegisterDPH ← 𝐀
     46  [ A ← byte_of_nat off
     47  ; A ← A .Add. RegisterSPL
     48  ; RegisterDPL ← A
     49  ; A ← zero_byte
     50  ; A ← A .Addc. RegisterSPH
     51  ; RegisterDPH ← A
    4652  ].
    4753
    4854definition get_stack:
    49  ∀globals.Register → Byte → list (joint_seq ltl_params globals) ≝
     55 ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
    5056 λglobals,r,off.
    5157 set_dp_by_offset ? off @
    52  [ LOAD … it it it ] @
    53  if eq_Register r RegisterA then [ ] else [ r ← 𝐀 ].
     58 [ LOAD … A it it ] @
     59 if eq_Register r RegisterA then [ ] else [ r ← A ].
    5460
    5561definition set_stack_not_a :
    56  ∀globals.Byte → Register → list (joint_seq ltl_params globals) ≝
     62 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
    5763 λglobals,off,r.
    5864 set_dp_by_offset ? off @
    59  [ 𝐀 ← r
    60  ; STORE … it it it ].
     65 [ A ← r
     66 ; STORE … it it A ].
    6167
    6268definition set_stack_a :
    63  ∀globals.Byte → list (joint_seq ltl_params globals) ≝
     69 ∀globals.nat → list (joint_seq ltl_params globals) ≝
    6470 λglobals,off.
    65  [ RegisterST1 ← 𝐀 ] @
     71 [ RegisterST1 ← A ] @
    6672 set_stack_not_a ? off RegisterST1.
    6773
    6874definition set_stack :
    69  ∀globals.Byte → Register → list (joint_seq ltl_params globals) ≝
     75 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
    7076 λglobals,off,r.
    7177 if eq_Register r RegisterA then
     
    7581 
    7682definition set_stack_int :
    77   ∀globals.Byte → Byte →  list (joint_seq ltl_params globals) ≝
     83  ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
    7884  λglobals,off,int.
    7985  set_dp_by_offset ? off @
    80   [ 𝐀 ← int
    81   ; STORE … it it it ].
     86  [ A ← int
     87  ; STORE … it it A ].
    8288
    8389definition move :
     
    8995    [ arg_decision_colour srcr ⇒
    9096      if eq_Register dstr srcr then [ ] else
    91       if eq_Register dstr RegisterA then [ 𝐀 ← srcr ] else
    92       if eq_Register srcr RegisterA then [ dstr ← 𝐀 ] else
    93       [ 𝐀 ← srcr ; dstr ← 𝐀]
     97      if eq_Register dstr RegisterA then [ A ← srcr ] else
     98      if eq_Register srcr RegisterA then [ dstr ← A ] else
     99      [ A ← srcr ; dstr ← A]
    94100    | arg_decision_spill srco ⇒
    95101      preserve_carry_bit ? carry_lives_after
    96102        (get_stack ? dstr srco)
    97103    | arg_decision_imm int ⇒
    98       [ 𝐀 ← int ] @
     104      [ A ← int ] @
    99105      if eq_Register dstr RegisterA then [ ] else
    100       [ dstr ← 𝐀 ]
     106      [ dstr ← A ]
    101107    ]
    102108  | decision_spill dsto ⇒
     
    125131  λglobals,stack_sz.
    126132  [ CLEAR_CARRY …
    127   ; 𝐀 ← RegisterSPL
    128   ; 𝐀 ← 𝐀 .Sub. stack_sz
    129   ; RegisterSPL ← 𝐀
    130   ; 𝐀 ← RegisterSPH
    131   ; 𝐀 ← 𝐀 .Sub. 0
    132   ; RegisterSPL ← 𝐀
     133  ; A ← RegisterSPL
     134  ; A ← A .Sub. byte_of_nat stack_sz
     135  ; RegisterSPL ← A
     136  ; A ← RegisterSPH
     137  ; A ← A .Sub. zero_byte
     138  ; RegisterSPL ← A
    133139  ].
    134140
     
    136142  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
    137143  λglobals,stack_sz.
    138   [ 𝐀 ← RegisterSPL
    139   ; 𝐀 ← 𝐀 .Add. stack_sz
    140   ; RegisterSPL ← 𝐀
    141   ; 𝐀 ← RegisterSPH
    142   ; 𝐀 ← 𝐀 .Addc. 0
    143   ; RegisterSPL ← 𝐀
     144  [ A ← RegisterSPL
     145  ; A ← A .Add. byte_of_nat stack_sz
     146  ; RegisterSPL ← A
     147  ; A ← RegisterSPH
     148  ; A ← A .Addc. zero_byte
     149  ; RegisterSPL ← A
    144150  ].
    145151
     
    178184    (move ? false RegisterB arg2 @
    179185     move ? false RegisterA arg1) @
    180     [ 𝐀 ← 𝐀 .op. RegisterB ] @
     186    [ A ← A .op. RegisterB ] @
    181187    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    182188    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
     
    193199    [ arg_decision_colour arg2r ⇒
    194200      move ? (uses_carry op) RegisterA arg1 @
    195       [ 𝐀 ← 𝐀 .op. arg2r ] @
     201      [ A ← A .op. arg2r ] @
    196202      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    197203    | arg_decision_imm arg2i ⇒
    198204      move ? (uses_carry op) RegisterA arg1 @
    199       [ 𝐀 ← 𝐀 .op. arg2i ] @
     205      [ A ← A .op. arg2i ] @
    200206      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    201207    | _ ⇒
     
    204210        [ arg_decision_colour arg1r ⇒
    205211          move ? (uses_carry op) RegisterA arg2 @
    206           [ 𝐀 ← 𝐀 .op. arg1r ] @
     212          [ A ← A .op. arg1r ] @
    207213          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    208214        | arg_decision_imm arg1i ⇒
    209215          move ? (uses_carry op) RegisterA arg2 @
    210           [ 𝐀 ← 𝐀 .op. arg1i ] @
     216          [ A ← A .op. arg1i ] @
    211217          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
    212218        | _ ⇒
     
    275281        move ? false RegisterST0 src @
    276282        move_to_dptr @
    277         [ 𝐀 ← RegisterST0]
     283        [ A ← RegisterST0]
    278284      else move_to_dptr) @
    279      [STORE … it it it]).
     285     [STORE … it it A]).
    280286
    281287definition translate_load : 
     
    285291    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    286292    (move_to_dp ? addr1 addr2 @
    287      [ LOAD … it it it ] @
     293     [ LOAD … A it it ] @
    288294     move ? false dst RegisterA).
    289295
     
    315321    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
    316322    | POP r ⇒
    317       POP … it ::
     323      POP … A ::
    318324      move (lookup r) RegisterA
    319325    | PUSH a ⇒
    320326      move RegisterA (lookup_arg a) @
    321       [ PUSH … it ]
     327      [ PUSH … A ]
    322328    | STORE addr1 addr2 srcr ⇒
    323329      translate_store ? carry_lives_after
     
    349355      let src ≝
    350356        match \snd pair_regs return λ_.arg_decision with
    351         [ REG r ⇒ lookup_move_dst r
    352         | INT b ⇒ arg_decision_imm b
     357        [ Reg r ⇒ lookup_move_dst r
     358        | Imm b ⇒ arg_decision_imm b
    353359        ] in
    354360      move dst src
     
    365371      | ertl_del_frame ⇒ delframe ? stack_sz
    366372      | ertl_frame_size r ⇒
    367         move (lookup r) (arg_decision_imm stack_sz)
     373        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368374      ]
    369375    | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
     
    384390
    385391definition translate_internal: ∀globals: list ident.
    386   ertl_internal_function globals → joint_internal_function globals ltl_params ≝
     392  joint_internal_function globals ertl_params →
     393  joint_internal_function globals ltl_params ≝
    387394  λglobals: list ident.
    388   λint_fun: ertl_internal_function globals.
     395  λint_fun: joint_internal_function globals ertl_params.
    389396  (* initialize graph *)
    390397  let entry ≝ pi1 … (joint_if_entry … int_fun) in
  • src/ERTL/ERTL_paolo.ma

    r2174 r2208  
    66  | HDW: Register → move_dst.
    77
    8 inductive move_src: Type[0] ≝
    9   | INT: Byte → move_src
    10   | REG: move_dst → move_src.
     8definition move_src ≝ argument move_dst.
    119
    12 coercion move_dst_to_src : ∀r : move_dst.move_src ≝ REG on _r : move_dst to move_src.
     10definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
     11coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
    1312
    14 definition rtl_argument_move_src : rtl_argument → move_src ≝
     13definition psd_argument_move_src : psd_argument → move_src ≝
    1514  λarg.match arg with
    16   [ Imm b ⇒ INT b
    17   | Reg r ⇒ REG (PSD r)
     15  [ Imm b ⇒ Imm ? b
     16  | Reg r ⇒ Reg ? (PSD r)
    1817  ].
    19 
    20 coercion rtl_argument_to_move_src : ∀a:rtl_argument.move_src ≝
    21   rtl_argument_move_src on _a : rtl_argument to move_src.
     18coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
     19  psd_argument_move_src on _a : psd_argument to move_src.
    2220
    2321inductive ertl_seq : Type[0] ≝
     
    3028    (* acc_a_reg ≝ *) register
    3129    (* acc_b_reg ≝ *) register
    32     (* acc_a_arg ≝ *) rtl_argument
    33     (* acc_b_arg ≝ *) rtl_argument
     30    (* acc_a_arg ≝ *) psd_argument
     31    (* acc_b_arg ≝ *) psd_argument
    3432    (* dpl_reg   ≝ *) register
    3533    (* dph_reg   ≝ *) register
    36     (* dpl_arg   ≝ *) rtl_argument
    37     (* dph_arg   ≝ *) rtl_argument
    38     (* snd_arg   ≝ *) rtl_argument
     34    (* dpl_arg   ≝ *) psd_argument
     35    (* dph_arg   ≝ *) psd_argument
     36    (* snd_arg   ≝ *) psd_argument
    3937    (* pair_move ≝ *) (move_dst × move_src)
    4038    (* call_args ≝ *) ℕ
     
    5048      (* localsT ≝ *) register).
    5149
    52   definition ertl_params ≝ mk_graph_params ertl_uns_params.
    53   definition ertl_internal_function ≝
    54   λglobals. joint_internal_function globals ertl_params.
     50definition ertl_params ≝ mk_graph_params ertl_uns_params.
    5551definition ertl_program ≝ joint_program ertl_params.
    5652
     
    6965unification hint 0 ≔
    7066(*---------------*) ⊢
    71 acc_a_arg ertl_params ≡ rtl_argument.
     67acc_a_arg ertl_params ≡ psd_argument.
    7268unification hint 0 ≔
    7369(*---------------*) ⊢
    74 acc_b_arg ertl_params ≡ rtl_argument.
     70acc_b_arg ertl_params ≡ psd_argument.
    7571unification hint 0 ≔
    7672(*---------------*) ⊢
     
    8177unification hint 0 ≔
    8278(*---------------*) ⊢
    83 dpl_arg ertl_params ≡ rtl_argument.
     79dpl_arg ertl_params ≡ psd_argument.
    8480unification hint 0 ≔
    8581(*---------------*) ⊢
    86 dph_arg ertl_params ≡ rtl_argument.
     82dph_arg ertl_params ≡ psd_argument.
    8783unification hint 0 ≔
    8884(*---------------*) ⊢
    89 snd_arg ertl_params ≡ rtl_argument.
     85snd_arg ertl_params ≡ psd_argument.
    9086unification hint 0 ≔
    9187(*---------------*) ⊢
     
    105101ext_tailcall ertl_params ≡ void.
    106102
    107 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝ Reg
     103coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝
     104  psd_argument_from_reg
    108105  on _r : register to snd_arg ertl_params.
    109 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝ Imm
     106coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝
     107  psd_argument_from_byte
    110108  on _b : Byte to snd_arg ertl_params.
    111109 
  • src/ERTL/liveness_paolo.ma

    r2182 r2208  
    9292definition ret_regs ≝ set_from_list … RegisterRets.
    9393
    94 definition rl_arg : rtl_argument → register_lattice ≝
     94definition rl_arg : psd_argument → register_lattice ≝
    9595  λarg.match arg with
    9696  [ Imm _ ⇒ rl_bottom
     
    124124        let r2 ≝ \snd pair_reg in
    125125        match r2 with
    126         [ REG p ⇒
     126        [ Reg p ⇒
    127127          match p with
    128128          [ PSD r ⇒ rl_psingleton r
    129129          | HDW r ⇒ rl_hsingleton r
    130130          ]
    131         | INT _ ⇒ rl_bottom
     131        | Imm _ ⇒ rl_bottom
    132132        ]
    133133      | extension_seq ext ⇒
     
    236236definition livebefore ≝
    237237  λglobals: list ident.
    238   λint_fun: ertl_internal_function globals.
     238  λint_fun: joint_internal_function globals ertl_params.
    239239  λlabel.
    240240  λliveafter: valuation register_lattice.
     
    246246definition liveafter ≝
    247247   λglobals: list ident.
    248   λint_fun: ertl_internal_function globals.
     248  λint_fun: joint_internal_function globals ertl_params.
    249249  λlabel.
    250250  λliveafter: valuation register_lattice.
  • src/LIN/joint_LTL_LIN_paolo.ma

    r2174 r2208  
    11include "joint/Joint_paolo.ma".
    2 
    3 definition a_acc ≝ it.
    4 definition b_acc ≝ it.
    52
    63inductive registers_move: Type[0] ≝
    74 | from_acc: Register → unit → registers_move
    85 | to_acc: unit → Register → registers_move
    9  | int_to_reg : Register → Byte → registers_move
    10  | int_to_acc : unit → Byte → registers_move.
    11 
    12 inductive ltl_argument : Type[0] ≝
    13  | Reg : Register → ltl_argument
    14  | Imm : Byte → ltl_argument.
    15 
    16 coercion reg_ltl_argument : ∀r : Register.ltl_argument ≝ Reg on _r : Register to ltl_argument.
    17 coercion int_ltl_argument : ∀b : Byte.ltl_argument ≝ Imm on _b : Byte to ltl_argument.
    18 
    19 notation "𝐀" with precedence 90 for @{a_acc}.
    20 notation "𝐁" with precedence 90 for @{b_acc}.
     6 | int_to_reg : Register → beval → registers_move
     7 | int_to_acc : unit → beval → registers_move.
     8(* the last is redudant, but kept for notation's sake *)
    219
    2210inductive ltl_lin_seq : Type[0] ≝
     
    3422    (* dpl_arg   ≝ *) unit
    3523    (* dph_arg   ≝ *) unit
    36     (* snd_arg   ≝ *) ltl_argument
     24    (* snd_arg   ≝ *) hdw_argument
    3725    (* pair_move ≝ *) registers_move
    3826    (* call_args ≝ *) ℕ
     
    4836      (* localsT ≝ *) void).
    4937
    50 interpretation "from accumulator" 'mov a b = (MOVE ?? (from_acc a b)).
    51 interpretation "to accumulator" 'mov a b = (MOVE ?? (to_acc a b)).
    52 interpretation "int to register" 'mov a b = (MOVE ?? (int_to_reg a b)).
    53 interpretation "int to accumulator" 'mov a b = (MOVE ?? (int_to_acc a b)).
    54 definition nat_to_byte : ℕ → Byte ≝ nat_to_bv 8.
    55 coercion nat_as_byte : ∀n : ℕ.Byte ≝ nat_to_byte on _n : ℕ to Byte.
    56 
     38interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
     39interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
     40interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
     41interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
  • src/LTL/LTL_paolo.ma

    r2174 r2208  
    1818unification hint 0 ≔
    1919(*---------------*) ⊢
    20 snd_arg ltl_params ≡ ltl_argument.
     20snd_arg ltl_params ≡ hdw_argument.
    2121unification hint 0 ≔
    2222(*---------------*) ⊢
     
    2727
    2828definition ltl_program ≝ joint_program ltl_params.
     29
     30coercion byte_to_ltl_argument : ∀b: Byte.snd_arg ltl_params ≝
     31  hdw_argument_from_byte on _b : Byte to snd_arg ltl_params.
     32coercion reg_to_ltl_argument : ∀r: Register.snd_arg ltl_params ≝
     33  hdw_argument_from_reg on _r : Register to snd_arg ltl_params.
  • src/RTL/RTLToERTL_paolo.ma

    r2174 r2208  
    1515
    1616definition restore_hdws :
    17   ∀globals.list (rtl_argument×Register) → list (joint_seq ertl_params globals) ≝
     17  ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
    1818  λglobals.
    1919   let restore_hdws_internal ≝
    20     λdestr_srcr:rtl_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
     20    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
    2121    map ? ? restore_hdws_internal.
    2222
     
    2626  save_hdws … (zip_pottier … params RegisterParams).
    2727
    28 (* Paolo: The following can probably be done way more efficiently with INC DPTR *)
    29 
    3028definition get_param_stack :
    31   ∀globals.register → register → nat → register →
     29  ∀globals.register → register → register →
    3230  list (joint_seq ertl_params globals) ≝
    33   λglobals,addr1,addr2,off,destr.
    34   let int_offset : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in
    35   [ (ertl_frame_size addr1 : joint_seq ??) ;
    36     CLEAR_CARRY … ;
    37     addr1 ← addr1 .Sub. int_offset ; (* are we sure carry bit is unimportant? *)
    38     PSD destr ← HDW RegisterSPL ;
    39     addr1 ← addr1 .Add. destr ;
    40     PSD addr2 ← HDW RegisterSPH ;
    41     addr2 ← addr2 .Addc. 0 ;
    42     LOAD … destr addr1 addr2
     31  λglobals,addr1,addr2,destr.
     32  (* liveness analysis will erase the last useless ops *)
     33  [ LOAD ?? destr addr1 addr2 ;
     34    addr1 ← addr1 .Add. (int_size : Byte) ;
     35    addr2 ← addr2 .Addc. zero_byte
    4336  ].
    4437
     
    4740  bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
    4841  λglobals,params.
    49   νaddr1,addr2 in
    50   flatten … (mapi ?? (get_param_stack globals addr1 addr2) params).
     42  νtmpr,addr1,addr2 in
     43  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     44  [ (ertl_frame_size tmpr : joint_seq ??) ;
     45    CLEAR_CARRY ?? ;
     46    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
     47    PSD addr1 ← HDW RegisterSPL ;
     48    PSD addr2 ← HDW RegisterSPH ;
     49    addr1 ← addr1 .Add. tmpr ;
     50    addr2 ← addr2 .Addc. zero_byte ] @   
     51  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
    5152
    5253definition get_params ≝
     
    6667
    6768definition save_return :
    68   ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝
     69  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
    6970  λglobals,ret_regs.
    7071  match reduce_strong ? ? RegisterSTS ret_regs with
     
    7475    let restl ≝ \snd (\fst crl) in
    7576    (* let restr ≝ \snd (\snd crl) in *)
    76     map2 … (λst.λr : rtl_argument.HDW st ← r) commonl commonr crl_proof @
    77     map … (λst.HDW st ← 0) restl
     77    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
     78    map … (λst.HDW st ← zero_byte) restl
    7879  ].
    7980
     
    9192  list (joint_seq ertl_params globals) ≝
    9293  λglobals,ret_regs,sral,srah,sregs.
    93   save_return … (map … Reg ret_regs) @
    94   restore_hdws … (map … (λpr.〈Reg (\fst pr),\snd pr〉) sregs) @
     94  save_return … (map … (Reg ?) ret_regs) @
     95  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    9596  [ PUSH ertl_params ? srah ;
    9697    PUSH … sral ;
     
    128129
    129130definition set_params_hdw :
    130   ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝
     131  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
    131132  λglobals,params.
    132133  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     
    135136
    136137definition set_param_stack :
    137   ∀globals.register → register → nat → rtl_argument →
     138  ∀globals.register → register → psd_argument →
    138139  list (joint_seq ertl_params globals) ≝
    139   λglobals,addr1,addr2,off,arg.
    140   let int_off : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in
     140  λglobals,addr1,addr2,arg.
     141  [ STORE … addr1 addr2 arg ;
     142    addr1 ← addr1 .Add. (int_size : Byte) ;
     143    addr2 ← addr2 .Addc. zero_byte
     144  ].
     145
     146definition set_params_stack :
     147  ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
     148  λglobals,params.
     149  νaddr1,addr2 in
     150  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
    141151  [ PSD addr1 ← HDW RegisterSPL ;
    142     CLEAR_CARRY … ;
    143     addr1 ← addr1 .Sub. int_off ;
    144152    PSD addr2 ← HDW RegisterSPH ;
    145     addr2 ← addr2 .Sub. 0 ;
    146     STORE … addr1 addr2 arg
    147   ].
    148 
    149 definition set_params_stack :
    150   ∀globals.list rtl_argument → bind_new (localsT ertl_params) ? ≝
    151   λglobals,params.
    152   νaddr1,addr2 in
    153   flatten … (mapi … (set_param_stack globals addr1 addr2) params).
     153    CLEAR_CARRY ?? ;
     154    addr1 ← addr1 .Sub. params_length_byte ;
     155    addr2 ← addr2 .Sub. zero_byte
     156  ] @
     157  flatten … (map … (set_param_stack globals addr1 addr2) params).
    154158
    155159definition set_params ≝
     
    186190    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
    187191    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
    188     | MOVE rs ⇒ PSD (\fst rs) ←
    189         match \snd rs with
    190         [ Reg src ⇒ PSD src
    191         | Imm b ⇒ INT b
    192         ]
     192    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
    193193    | COST_LABEL lbl ⇒
    194194      COST_LABEL … lbl
     
    254254  let def' ≝
    255255    mk_joint_internal_function globals ertl_params
    256       (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
     256      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    257257      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    258258      graph' entry' exit' in
  • src/RTL/RTL_paolo.ma

    r2186 r2208  
    11include "joint/Joint_paolo.ma".
    2 
    3 inductive rtl_argument : Type[0] ≝
    4   | Reg : register → rtl_argument
    5   | Imm : Byte → rtl_argument.
    6  
    7 coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
    8   on _r : register to rtl_argument.
    9 
    10 coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
    11   on _b : Byte to rtl_argument.
    12 
    13 definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
    14  
    15 coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
    16   on _n : nat to rtl_argument.
    172
    183inductive rtl_seq : Type[0] ≝
     
    205 
    216inductive rtl_call : Type[0] ≝
    22   | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
     7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    238
    249inductive rtl_tailcall : Type[0] ≝
    25   | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
    26   | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
     10  | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
     11  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    2712
    2813definition rtl_uns_params ≝ mk_unserialized_params
     
    3015    (* acc_a_reg ≝ *) register
    3116    (* acc_b_reg ≝ *) register
    32     (* acc_a_arg ≝ *) rtl_argument
    33     (* acc_b_arg ≝ *) rtl_argument
     17    (* acc_a_arg ≝ *) psd_argument
     18    (* acc_b_arg ≝ *) psd_argument
    3419    (* dpl_reg   ≝ *) register
    3520    (* dph_reg   ≝ *) register
    36     (* dpl_arg   ≝ *) rtl_argument
    37     (* dph_arg   ≝ *) rtl_argument
    38     (* snd_arg   ≝ *) rtl_argument
    39     (* pair_move ≝ *) (register × rtl_argument)
    40     (* call_args ≝ *) (list rtl_argument)
     21    (* dpl_arg   ≝ *) psd_argument
     22    (* dph_arg   ≝ *) psd_argument
     23    (* snd_arg   ≝ *) psd_argument
     24    (* pair_move ≝ *) (register × psd_argument)
     25    (* call_args ≝ *) (list psd_argument)
    4126    (* call_dest ≝ *) (list register)
    4227    (* ext_seq ≝ *) rtl_seq
     
    5944definition rtl_statement ≝ joint_statement rtl_params.
    6045
    61 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).
     46interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
    6247
    6348(* aid unification *)
     
    7156unification hint 0 ≔
    7257(*---------------*) ⊢
    73 acc_a_arg rtl_params ≡ rtl_argument.
     58acc_a_arg rtl_params ≡ psd_argument.
    7459unification hint 0 ≔
    7560(*---------------*) ⊢
    76 acc_b_arg rtl_params ≡ rtl_argument.
     61acc_b_arg rtl_params ≡ psd_argument.
    7762unification hint 0 ≔
    7863(*---------------*) ⊢
     
    8368unification hint 0 ≔
    8469(*---------------*) ⊢
    85 dpl_arg rtl_params ≡ rtl_argument.
     70dpl_arg rtl_params ≡ psd_argument.
    8671unification hint 0 ≔
    8772(*---------------*) ⊢
    88 dph_arg rtl_params ≡ rtl_argument.
     73dph_arg rtl_params ≡ psd_argument.
    8974unification hint 0 ≔
    9075(*---------------*) ⊢
    91 snd_arg rtl_params ≡ rtl_argument.
     76snd_arg rtl_params ≡ psd_argument.
    9277unification hint 0 ≔
    9378(*---------------*) ⊢
    94 pair_move rtl_params ≡ register × rtl_argument.
     79pair_move rtl_params ≡ register × psd_argument.
    9580unification hint 0 ≔
    9681(*---------------*) ⊢
    97 call_args rtl_params ≡ list rtl_argument.
     82call_args rtl_params ≡ list psd_argument.
    9883unification hint 0 ≔
    9984(*---------------*) ⊢
     
    120105joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    121106
    122 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
     107coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    123108  on _r : register to snd_arg rtl_params.
    124 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
     109coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    125110  on _b : Byte to snd_arg rtl_params.
    126111
     
    132117    (* acc_a_reg ≝ *) register
    133118    (* acc_b_reg ≝ *) register
    134     (* acc_a_arg ≝ *) rtl_argument
    135     (* acc_b_arg ≝ *) rtl_argument
     119    (* acc_a_arg ≝ *) psd_argument
     120    (* acc_b_arg ≝ *) psd_argument
    136121    (* dpl_reg   ≝ *) register
    137122    (* dph_reg   ≝ *) register
    138     (* dpl_arg   ≝ *) rtl_argument
    139     (* dph_arg   ≝ *) rtl_argument
    140     (* snd_arg   ≝ *) rtl_argument
    141     (* pair_move ≝ *) (register × rtl_argument)
    142     (* call_args ≝ *) (list rtl_argument)
     123    (* dpl_arg   ≝ *) psd_argument
     124    (* dph_arg   ≝ *) psd_argument
     125    (* snd_arg   ≝ *) psd_argument
     126    (* pair_move ≝ *) (register × psd_argument)
     127    (* call_args ≝ *) (list psd_argument)
    143128    (* call_dest ≝ *) (list register)
    144129    (* ext_seq ≝ *) rtl_seq
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2162 r2208  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
    10 
    1110definition size_of_sig_type ≝
    1211  λsig.
     
    1615      isize' ÷ (nat_of_bitvector ? int_size)
    1716  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    18   | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
    19   ].
    20   cases not_implemented;
     17  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
     18  ].
     19  cases not_implemented
    2120qed.
    2221
     
    4645qed.
    4746
    48 definition find_local_env_arg
    49   λr,lenv,prf. map … Reg (find_local_env r lenv prf).
     47definition find_local_env_arg : register → local_env → ? → list psd_argument
     48  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
    5049
    5150definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
     
    9796include alias "common/Identifiers.ma".
    9897let rec rtl_args (args : list register) (env : local_env) on args :
    99   All ? (λr.bool_to_Prop (r∈env)) args → list rtl_argument ≝
     98  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
    10099  match args return λx.All ?? x → ? with
    101100  [ nil ⇒ λ_.[ ]
     
    131130  ∀globals. Op2 →
    132131  ∀dests : list register.
    133   ∀srcrs1 : list rtl_argument.
    134   ∀srcrs2 : list rtl_argument.
     132  ∀srcrs1 : list psd_argument.
     133  ∀srcrs2 : list psd_argument.
    135134  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    136135  list (joint_seq rtl_params globals)
     
    149148  ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
    150149
    151 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝
     150let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
    152151match size with
    153152[ O ⇒ [ ]
    154153| S size' ⇒
    155   match nat_to_args size' (k ÷ 8) with
    156   [ mk_Sig res prf ⇒
    157     imm_nat k :: res
    158   ]
    159 ]. normalize // qed.
     154  (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8)
     155]. [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
    160156
    161157definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     
    168164definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
    169165  match cst with
    170   [ Oaddrsymbol r id offset ⇒ member id (eq_identifier ?) globals
     166  [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals
    171167  | _ ⇒ True
    172168  ].
     
    185181  with
    186182  [ Ointconst size sign const ⇒ λcst_prf,prf.
    187       map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs
     183      map2 … (λr.λb : Byte.r ← b) destrs
    188184        (split_into_bytes size const) ?
    189185  | Ofloatconst _ _ ⇒ ?
    190   | Oaddrsymbol r id offset ⇒ λcst_prf,prf.
     186  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    191187    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    192188    [ADDRESS rtl_params globals id ? r1 r2]
     
    206202  ∀globals.
    207203  ∀destrs: list register.
    208   ∀srcrs: list rtl_argument.
     204  ∀srcrs: list psd_argument.
    209205  |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝
    210206  λglobals,destrs,srcrs,length_eq.
     
    229225     *)
    230226  λglobals,destr,srcr.
    231   [destr ← srcr .Or. 127 ;
     227  let byte_127 : Byte ≝ false ::: maximum ? in
     228  [destr ← srcr .Or. byte_127 ;
    232229   destr ← .Rl. destr ;
    233230   destr ← .Inc. destr ;
     
    241238  ν tmp in
    242239  (sign_mask ? tmp srcr @
    243   translate_move ? destrs (make_list ? (Reg tmp) (|destrs|)) (make_list_length …)).
     240  translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) (make_list_length …)).
    244241 
    245242definition translate_fill_with_zero :
     
    282279    let dst_rest   ≝ \snd (\snd t) in
    283280    (* first, move the common part *)
    284     translate_move ? src_common (map … Reg dst_common) ? @@
     281    translate_move ? src_common (map … (Reg ?) dst_common) ? @@
    285282    match src_rest return λ_.bind_new ?? with
    286283    [ nil ⇒ (* upcast *)
     
    314311  match nat_to_args (|destrs|) 1 with
    315312  [ mk_Sig res prf' ⇒
    316     translate_op ? Add destrs (map … Reg destrs) res ??
    317   ].
    318 // qed.
     313    translate_op ? Add destrs (map … (Reg ?) destrs) res ??
     314  ].
     315>length_map // qed.
    319316
    320317definition translate_notbool:
     
    328325    translate_fill_with_zero ? destrs' @@
    329326    match srcrs return λ_.bind_new ?? with
    330     [ nil ⇒ [destr ← 0]
     327    [ nil ⇒ [destr ← zero_byte]
    331328    | cons srcr srcrs' ⇒
    332329      (destr ← srcr) :::
     
    336333      (* many uses of 0, better not use immediates *)
    337334      ν tmp in
    338       [tmp ← 0 ;
     335      [tmp ← zero_byte ;
    339336       destr ← tmp .Sub. tmp ;
    340337       (* now carry bit is set iff destr was non-null *)
     
    363360  | Onotint sz sg ⇒ λeq1,eq2.
    364361    translate_notint globals destrs srcrs ?
    365   | Optrofint sz sg r ⇒ λeq1,eq2.
     362  | Optrofint sz sg ⇒ λeq1,eq2.
    366363    translate_cast globals Unsigned destrs srcrs
    367   | Ointofptr sz sg r ⇒ λeq1,eq2.
     364  | Ointofptr sz sg ⇒ λeq1,eq2.
    368365    translate_cast globals Unsigned destrs srcrs
    369366  | Oid t ⇒ λeq1,eq2.
    370       translate_move globals destrs (map … Reg srcrs) ?
     367      translate_move globals destrs (map … (Reg ?) srcrs) ?
    371368  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
    372369  ] (refl …) (refl …).
    373   [3,4,5,6,7,8,9: cases not_implemented
    374   |*: destruct >prf1 >prf2 //
     370  [3,4,5,6,7,8,9: (* floats *) cases not_implemented
     371  |*: destruct >prf1 >prf2 [3: >length_map ] //
    375372  ]
    376373qed.
     
    401398  (* the temporary destination, with a dummy register at the end *)
    402399  ∀tmp_destrs_dummy : list register.
    403   ∀srcrs1,srcrs2 : list rtl_argument.
     400  ∀srcrs1,srcrs2 : list psd_argument.
    404401  |tmp_destrs_dummy| = S n →
    405402  n = |srcrs1| →
     
    431428         for the bit to be carried. Redundant calculations will be eliminated
    432429         by constant propagation. *)
    433       let args : list rtl_argument ≝
    434         [Reg a;Reg b] @ make_list ? (Imm (zero …)) (n - 1 - k) in
     430      let args : list psd_argument ≝
     431        [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in
    435432      let tmp_destrs_view : list register ≝
    436433        ltl ? tmp_destrs_dummy k in
    437434      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
    438       translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
     435      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
    439436      acc
    440437    ].
     
    452449    [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
    453450  cut (S n = 2 + (n - 1))
    454     [2: #EQ >EQ //]
     451    [2: #EQ >EQ %]
    455452  >plus_minus_commutative
    456453    [2: @(transitive_le … k_prf) //]
    457454  @sym_eq
    458   @plus_to_minus
    459   <plus_n_Sm
    460   //
     455  @plus_to_minus %
    461456] qed.
    462457
     
    464459λglobals : list ident.
    465460λdestrs : list register.
    466 λsrcrs1 : list rtl_argument.
    467 λsrcrs2 : list rtl_argument.
     461λsrcrs1 : list psd_argument.
     462λsrcrs2 : list psd_argument.
    468463λsrcrs1_prf : |destrs| = |srcrs1|.
    469464λsrcrs2_prf : |srcrs1| = |srcrs2|.
     
    494489foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
    495490(* epilogue: saving the result *)
    496 translate_move … destrs (map … Reg tmp_destrs) ?.
     491translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
    497492[ >length_map >tmp_destrs_prf //
    498493| >length_append <plus_n_Sm <plus_n_O //
     
    505500  λdiv_not_mod: bool.
    506501  λdestrs: list register.
    507   λsrcrs1: list rtl_argument.
    508   λsrcrs2: list rtl_argument.
     502  λsrcrs1: list psd_argument.
     503  λsrcrs2: list psd_argument.
    509504  λsrcrs1_prf : |destrs| = |srcrs1|.
    510505  λsrcrs2_prf : |srcrs1| = |srcrs2|.
     
    551546  λglobals: list ident.
    552547  λdestrs: list register.
    553   λsrcrs1: list rtl_argument.
    554   λsrcrs2: list rtl_argument.
     548  λsrcrs1: list psd_argument.
     549  λsrcrs2: list psd_argument.
    555550  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
    556551  [ nil ⇒ λ_.[ ]
     
    558553    translate_fill_with_zero … destrs' @@
    559554    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
    560     [ nil ⇒ λ_.[destr ← 0]
     555    [ nil ⇒ λ_.[destr ← zero_byte]
    561556    | cons srcr1 srcrs1' ⇒
    562557      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
     
    564559      | cons srcr2 srcrs2' ⇒ λEQ.
    565560        νtmpr in
    566         let f : rtl_argument → rtl_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
     561        let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
    567562          λs1,s2,acc.
    568563          tmpr  ← s1 .Xor. s2 ::
     
    571566        let epilogue : list (joint_seq rtl_params globals) ≝
    572567          [ CLEAR_CARRY ?? ;
    573             tmpr ← 0 .Sub. destr ;
     568            tmpr ← zero_byte .Sub. destr ;
    574569            (* now carry bit is 1 iff destrs != 0 *)
    575             destr ← 0 .Addc. 0 ] in
     570            destr ← zero_byte .Addc. zero_byte ] in
    576571         destr ← srcr1 .Xor. srcr2 ::
    577572         foldr2 ??? f epilogue srcrs1' srcrs2' ?
     
    593588  ∀globals.
    594589  ∀destrs: list register.
    595   ∀srcrs1: list rtl_argument.
    596   ∀srcrs2: list rtl_argument.
     590  ∀srcrs1: list psd_argument.
     591  ∀srcrs2: list psd_argument.
    597592  |srcrs1| = |srcrs2| →
    598593  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     
    605600    (* I perform a subtraction, but the only interest is in the carry bit *)
    606601    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @
    607     [ destr ← 0 .Addc. 0 ])
     602    [ destr ← zero_byte .Addc. zero_byte ])
    608603  ].
    609604<make_list_length % qed.
     
    613608let rec shift_signed globals
    614609  (tmp : register)
    615   (srcrs : list rtl_argument) on srcrs :
    616   Σt : (list rtl_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     610  (srcrs : list psd_argument) on srcrs :
     611  Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     612  let byte_128 : Byte ≝ true ::: bv_zero ? in
    617613  match srcrs with
    618614  [ nil ⇒ 〈[ ],[ ]〉
    619615  | cons srcr srcrs' ⇒
    620616    match srcrs' with
    621     [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
     617    [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉
    622618    | _ ⇒
    623619      let re ≝ shift_signed globals tmp srcrs' in
     
    632628  ∀globals.
    633629  ∀destrs: list register.
    634   ∀srcrs1: list rtl_argument.
    635   ∀srcrs2: list rtl_argument.
     630  ∀srcrs1: list psd_argument.
     631  ∀srcrs2: list psd_argument.
    636632  |srcrs1| = |srcrs2| →
    637633  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     
    684680  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
    685681  ∀destrs : list register.
    686   ∀srcrs1,srcrs2 : list rtl_argument.
     682  ∀srcrs1,srcrs2 : list psd_argument.
    687683  |destrs| = size_of_sig_type ty3 →
    688684  |srcrs1| = size_of_sig_type ty1 →
     
    695691  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
    696692    translate_op globals Add destrs srcrs1 srcrs2 ??
    697   | Oaddp sz r ⇒ λprf1,prf2,prf3.
     693  | Oaddp sz ⇒ λprf1,prf2,prf3.
    698694    let is_Oaddp ≝ 0 in
    699695    translate_op globals Add destrs srcrs1 srcrs2 ??
    700696  | Osub sz sg ⇒ λprf1,prf2,prf2.
    701697    translate_op globals Sub destrs srcrs1 srcrs2 ??
    702   | Osubpi sz r ⇒ λprf1,prf2,prf3.
     698  | Osubpi sz ⇒ λprf1,prf2,prf3.
    703699    let is_Osubpi ≝ 0 in
    704700    translate_op globals Sub destrs srcrs1 srcrs2 ??
    705   | Osubpp sz r1 r2 ⇒ λprf1,prf2,prf3.
     701  | Osubpp sz ⇒ λprf1,prf2,prf3.
    706702    let is_Osubpp ≝ 0 in
    707703    translate_op globals Sub destrs srcrs1 srcrs2 ??
     
    722718  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
    723719    translate_cmp true globals c destrs srcrs1 srcrs2 ?
    724   | Ocmpp r sg c ⇒ λprf1,prf2,prf3.
     720  | Ocmpp sg c ⇒ λprf1,prf2,prf3.
    725721    let is_Ocmpp ≝ 0 in
    726722    translate_cmp true globals c destrs srcrs1 srcrs2 ?
    727723  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
    728   ]. // try @not_implemented
     724  ]. try @not_implemented //
    729725  (* pointer arithmetics is broken at the moment *)
    730726  cases daemon
     
    749745definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
    750746  λglobals: list ident.
    751   λaddr : list rtl_argument.
     747  λaddr : list psd_argument.
    752748  λaddr_prf: 2 = |addr|.
    753749  λdestrs: list register.
     
    755751  ν tmp_addr_h in
    756752  let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
    757     LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    758     translate_op Add
     753    LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     754    translate_op ? Add
    759755      [tmp_addr_l ; tmp_addr_h]
    760       [Reg tmp_addr_l ; Reg tmp_addr_h]
    761       [imm_nat 0 ; Imm int_size] ? ? @ acc in
     756      [tmp_addr_l ; tmp_addr_h]
     757      [zero_byte ; (int_size : Byte)] ? ? @ acc in
    762758  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    763759  foldr … f [ ] destrs.
    764 [1: <addr_prf] // qed.
     760[1: <addr_prf
     761] // qed.
    765762 
    766763definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
    767764  λglobals: list ident.
    768   λaddr : list rtl_argument.
     765  λaddr : list psd_argument.
    769766  λaddr_prf: 2 = |addr|.
    770   λsrcrs: list rtl_argument.
     767  λsrcrs: list psd_argument.
    771768  ν tmp_addr_l in
    772769  ν tmp_addr_h in
    773   let f ≝ λsrcr : rtl_argument.λacc : list (joint_seq rtl_params globals).
    774     STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
     770  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals).
     771    STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
    775772    translate_op … Add
    776773      [tmp_addr_l ; tmp_addr_h]
    777       [Reg tmp_addr_l ; Reg tmp_addr_h]
    778       [imm_nat 0 ; Imm int_size] ? ? @ acc in
     774      [tmp_addr_l ; tmp_addr_h]
     775      [zero_byte ; (int_size : Byte)] ? ? @ acc in
    779776  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    780777  foldr … f [ ] srcrs.
  • src/joint/Joint_paolo.ma

    r2186 r2208  
    3939| Labels : list label → possible_flows
    4040| Call : possible_flows.
     41
     42inductive argument (T : Type[0]) : Type[0] ≝
     43| Reg : T → argument T
     44| Imm : beval → argument T.
     45
     46definition psd_argument ≝ argument register.
     47 
     48definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
     49coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
     50  on _r : register to psd_argument.
     51
     52definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
     53coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
     54  on _b : beval to psd_argument.
     55
     56definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     57coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     58  on _b : Byte to psd_argument.
     59
     60definition hdw_argument ≝ argument Register.
     61 
     62definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
     63coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
     64  on _r : Register to hdw_argument.
     65
     66definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
     67coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
     68  on _b : beval to hdw_argument.
     69
     70definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     71coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     72  on _b : Byte to hdw_argument.
     73
     74definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
     75definition zero_byte : Byte ≝ bv_zero 8.
    4176
    4277record step_params : Type[1] ≝
  • src/joint/semanticsUtils_paolo.ma

    r2200 r2208  
    1414(*** Store/retrieve on hardware registers ***)
    1515
    16 definition init_hw_register_env: address → hw_register_env ≝
    17  λaddr.
    18   let 〈dpl,dph〉 ≝ addr in
     16definition init_hw_register_env: xpointer → hw_register_env ≝
     17 λsp.
     18  let 〈dpl,dph〉 ≝
     19    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
     20    [ OK p ⇒ λ_.p
     21    | _ ⇒ λprf.⊥
     22    ] (refl …) in
    1923  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    2024   hwreg_store RegisterDPL dpl env.
     25@hide_prf
     26normalize in prf; destruct(prf)
     27qed.
    2128
    2229(******************************** GRAPHS **************************************)
Note: See TracChangeset for help on using the changeset viewer.