Changeset 1060


Ignore:
Timestamp:
Jul 8, 2011, 12:17:14 PM (8 years ago)
Author:
mulligan
Message:

work from this morning and yesterday

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r777 r1060  
    1515inductive OpAccs: Type[0] ≝
    1616  Mul: OpAccs
    17 | Divu: OpAccs
    18 | Modu: OpAccs.
     17| DivuModu: OpAccs.
    1918
    2019inductive Op1: Type[0] ≝
  • src/ASM/Util.ma

    r1059 r1060  
    1212 with precedence 10
    1313for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     14
     15let rec nth_safe
     16  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
     17  (proof: index < | the_list |)
     18    on index ≝
     19  match index return λs. s < | the_list | → elt_type with
     20  [ O ⇒
     21    match the_list return λt. 0 < | t | → elt_type with
     22    [ nil        ⇒ λnil_absurd. ?
     23    | cons hd tl ⇒ λcons_proof. hd
     24    ]
     25  | S index' ⇒
     26    match the_list return λt. S index' < | t | → elt_type with
     27    [ nil ⇒ λnil_absurd. ?
     28    | cons hd tl ⇒
     29      λcons_proof. nth_safe elt_type index' tl ?
     30    ]
     31  ] proof.
     32  [ normalize in nil_absurd;
     33    cases (not_le_Sn_O 0)
     34    #ABSURD
     35    elim (ABSURD nil_absurd)
     36  | normalize in nil_absurd;
     37    cases (not_le_Sn_O (S index'))
     38    #ABSURD
     39    elim (ABSURD nil_absurd)
     40  | normalize in cons_proof
     41    @le_S_S_to_le
     42    assumption
     43  ]
     44qed.
     45
     46definition last_safe ≝
     47  λelt_type: Type[0].
     48  λthe_list: list elt_type.
     49  λproof   : 0 < | the_list |.
     50    nth_safe elt_type (|the_list| - 1) the_list ?.
     51  normalize /2/
     52qed.
    1453
    1554let rec reduce
     
    2867  ].
    2968
     69axiom reduce_strong:
     70  ∀A: Type[0].
     71  ∀left: list A.
     72  ∀right: list A.
     73    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
     74
    3075(*
    3176let rec reduce_strong
     
    3479  [ nil ⇒
    3580    match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    36     [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ?
    37     | cons hd tl ⇒ λnil_cons_asrd_prf. ?
     81    [ nil ⇒ λnil_nil_prf. ?
     82    | cons hd tl ⇒ λnil_cons_absrd_prf. ?
    3883    ]
    3984  | cons hd tl ⇒
    4085    match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    4186    [ nil ⇒ λcons_nil_absrd_prf. ?
    42     | cons hd' tl' ⇒ λcons_cons_prf. ?
     87    | cons hd' tl' ⇒ λcons_cons_prf.
     88      let tail_call ≝ reduce_strong A tl tl' ? in ?
    4389    ]
    4490  ] prf.
    45 *)
    46 
     91  [ 5: normalize in cons_cons_prf;
     92       destruct(cons_cons_prf)
     93       assumption
     94  | 2: normalize in nil_cons_absrd_prf;
     95       destruct(nil_cons_absrd_prf)
     96  | 3: normalize in cons_nil_absrd_prf;
     97       destruct(cons_nil_absrd_prf)
     98  ]
     99qed.
     100*)   
     101 
    47102axiom reduce_length:
    48103  ∀A: Type[0].
  • src/RTL/RTL.ma

    r878 r1060  
    44include "common/Graphs.ma".
    55include "common/CostLabel.ma".
    6 include "ASM/I8051.ma".
    76
    87definition registers ≝ list register.
     
    1514  | rtl_st_int: register → Byte → label → rtl_statement
    1615  | rtl_st_move: register → register → label → rtl_statement
    17   | rtl_st_opaccs: OpAccs → register → register → register → label → rtl_statement
    18   | rtl_st_op1: Op1 → register → register → label → rtl_statement
    19   | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
     16  | rtl_st_opaccs: inter → register → register → register → register → label → rtl_statement
     17  | rtl_st_op1: intermediate_op1 → register → register → label → rtl_statement
     18  | rtl_st_op2: intermediate_op2 → register → register → register → label → rtl_statement
    2019  | rtl_st_clear_carry: label → rtl_statement
    2120  | rtl_st_load: register → register → register → label → rtl_statement
     
    2625  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
    2726  | rtl_st_cond_acc: register → label → label → rtl_statement
     27  | rtl_st_set_carry: label → rtl_statement
     28  | rtl_st_clear_carry: label → rtl_statement
    2829  | rtl_st_return: registers → rtl_statement.
    2930 
     
    4445}.
    4546
    46 
    4747inductive rtl_function_definition: Type[0] ≝
    4848  | rtl_f_internal: rtl_internal_function → rtl_function_definition
  • src/RTLabs/RTLAbstoRTL.ma

    r1059 r1060  
    33include "common/AssocList.ma".
    44include "common/Graphs.ma".
    5 include "common/Maps.ma".
    65(* include "common/IntValue.ma". *)
    76include "common/FrontEndOps.ma".
     
    227226  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
    228227  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
    229   | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
     228  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
    230229  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
    231230  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
     
    238237  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
    239238  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
     239  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
     240  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    240241  | rtl_st_return r ⇒ rtl_st_return r
    241242  ].
     
    299300  λsrcrs: list register.
    300301  λstart_lbl: label.
     302    match reduce_strong register destrs srcrs with
     303    [ dp crl_crr len_proof ⇒
     304      let commonl ≝ \fst (\fst crl_crr) in
     305      let commonr ≝ \fst (\snd crl_crr) in
     306      let restl ≝ \snd (\fst crl_crr) in
     307      let restr ≝ \snd (\snd crl_crr) in
     308      let f_common ≝ translate_move_internal start_lbl in
     309      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
     310      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     311        add_translates [ translate1 ; translate2 ] start_lbl
     312    ].
     313    @len_proof
     314qed.
     315
     316let rec make
     317  (A: Type[0]) (elt: A) (n: nat) on n ≝
     318  match n with
     319  [ O ⇒ [ ]
     320  | S n' ⇒ elt :: make A elt n'
     321  ].
     322 
     323lemma make_length:
     324  ∀A: Type[0].
     325  ∀elt: A.
     326  ∀n: nat.
     327    n = length ? (make A elt n).
     328  #A #ELT #N
     329  elim N
     330  [ normalize %
     331  | #N #IH
     332    normalize <IH %
     333  ]
     334qed.
     335
     336definition translate_cast_unsigned ≝
     337  λdestrs.
     338  λstart_lbl.
     339  λdest_lbl.
     340  λdef.
     341  let 〈def, tmp_zero〉 ≝ fresh_reg def in
     342  let zeros ≝ make ? tmp_zero (length ? destrs) in
     343    add_translates [
     344      adds_graph [
     345        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
     346        ];
     347      translate_move destrs zeros
     348    ] start_lbl dest_lbl def.
     349
     350definition translate_cast_signed ≝
     351  λdestrs.
     352  λsrcr.
     353  λstart_lbl.
     354  λdest_lbl.
     355  λdef.
     356  let 〈def, tmp_128〉 ≝ fresh_reg def in
     357  let 〈def, tmp_255〉 ≝ fresh_reg def in
     358  let 〈def, tmpr〉 ≝ fresh_reg def in
     359  let 〈def, dummy〉 ≝ fresh_reg def in
     360  let insts ≝ [
     361    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
     362    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
     363    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
     364    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
     365    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
     366  ] in
     367  let srcrs ≝ make ? tmpr (length ? destrs) in
     368    add_translates [
     369      adds_graph insts;
     370      translate_move destrs srcrs
     371    ] start_lbl dest_lbl def.
     372
     373definition translate_cast ≝
     374  λsrc_size.
     375  λsrc_sign.
     376  λdest_size.
     377  λdestrs.
     378  λsrcrs.
     379  match | srcrs | return λx. | srcrs | = x → ? with
     380  [ O ⇒ λzero_prf. adds_graph [ ]
     381  | S n' ⇒ λsucc_prf.
     382    if ltb dest_size src_size then
     383      translate_move destrs srcrs
     384    else
     385      match reduce_strong ? destrs srcrs with
     386      [ dp crl len_proof ⇒
     387        let commonl ≝ \fst (\fst crl) in
     388        let commonr ≝ \fst (\snd crl) in
     389        let restl ≝ \snd (\fst crl) in
     390        let restr ≝ \snd (\snd crl) in
     391        let insts_common ≝ translate_move commonl commonr in
     392        let sign_reg ≝ last_safe ? srcrs ? in
     393        let insts_sign ≝
     394          match src_sign with
     395          [ Unsigned ⇒ translate_cast_unsigned restl
     396          | Signed ⇒ translate_cast_signed restl sign_reg
     397          ]
     398        in
     399          add_translates [ insts_common; insts_sign ]
     400      ]
     401  ] (refl ? (|srcrs|)).
     402  >succ_prf //
     403qed.
     404
     405definition translate_negint ≝
     406  λdestrs.
     407  λsrcrs.
     408  λstart_lbl.
     409  λdest_lbl.
     410  λdef.
     411  λprf: | destrs | = | srcrs |. (* assert in caml code *)
     412  let 〈def, tmpr〉 ≝ fresh_reg def in
     413  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     414  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
     415  let insts_init ≝ [
     416    rtl_st_set_carry start_lbl;
     417    rtl_st_int tmpr (zero ?) start_lbl
     418  ] in
     419  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
     420  let insts_add ≝ map … f_add destrs in
     421    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     422
     423definition translate_notbool ≝
     424  λdestrs.
     425  λsrcrs.
     426  λstart_lbl.
     427  λdest_lbl.
     428  λdef.
     429  match destrs with
     430  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     431  | cons destr destrs ⇒
     432    let 〈def, tmpr〉 ≝ fresh_reg def in
     433    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
     434    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
     435    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
     436    let f ≝ λtmp_srcr. [
     437      rtl_st_clear_carry start_lbl;
     438      rtl_st_int tmpr (zero ?) start_lbl;
     439      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
     440      rtl_st_int tmpr (zero ?) start_lbl;
     441      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
     442      rtl_st_op2 Xor destr destr tmpr start_lbl
     443    ] in
     444    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
     445    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
     446      add_translates [
     447        save_srcrs; adds_graph insts; epilogue
     448      ] start_lbl dest_lbl def
     449  ].
     450
     451definition translate_intermediate_op1 ≝
     452  λop1.
     453  λdestrs.
     454  λsrcrs.
     455  λstart_lbl.
     456  λdest_lbl.
     457  λdef.
    301458  λprf: | destrs | = | srcrs |.
    302     let 〈crl, crr〉 ≝ reduce register destrs srcrs in
    303     let 〈commonl, restl〉 ≝ crl in
    304     let 〈commonr, restr〉 ≝ crr in
    305     let f_common ≝ translate_move_internal start_lbl in
    306     let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
    307     let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    308       add_translates [ translate1 ; translate2 ] start_lbl.
    309    
    310 let rec translate_move destrs srcrs start_lbl =
    311   let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
    312   let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
    313   let translates1 = adds_graph (List.map2 f_common common1 common2) in
    314   let translates2 = translate_cst (AST.Cst_int 0) rest1 in
    315   add_translates [translates1 ; translates2] start_lbl
     459  match op1 with
     460  [ intermediate_op1_cast src_size src_sign dest_size ⇒
     461      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
     462  | intermediate_op1_negint ⇒
     463      translate_negint destrs srcrs start_lbl dest_lbl def prf
     464  | intermediate_op1_notbool ⇒
     465      translate_notbool destrs srcrs start_lbl dest_lbl def
     466  | intermediate_op1_notint ⇒
     467    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     468    let l ≝ map2 … f destrs srcrs prf in
     469      adds_graph l start_lbl dest_lbl def
     470  | intermediate_op1_ptrofint ⇒
     471      translate_move destrs srcrs start_lbl dest_lbl def
     472  | intermediate_op1_intofptr ⇒
     473      translate_move destrs srcrs start_lbl dest_lbl def
     474  | intermediate_op1_id ⇒
     475      translate_move destrs srcrs start_lbl dest_lbl def
     476  ].
    316477
    317478definition filter_and_to_list_local_env_internal ≝
  • src/common/AST.ma

    r1059 r1060  
    5656*)
    5757
     58
    5859(* Memory spaces *)
    5960
     
    102103  | I16: intsize
    103104  | I32: intsize.
     105
     106(* unary operations used in the backend intermediate languages, there's also a separate
     107   type for unary operations at the assembly level in ASM/I8051.ma *)
     108inductive intermediate_op1: Type[0] ≝
     109  | intermediate_op1_cast: nat → signedness → nat → intermediate_op1 (**r size in bytes, signedness, to size *)
     110  | intermediate_op1_negint: intermediate_op1           (**r integer opposite *)
     111  | intermediate_op1_notbool: intermediate_op1          (**r boolean negation  *)
     112  | intermediate_op1_notint: intermediate_op1           (**r bitwise complement  *)
     113  | intermediate_op1_id: intermediate_op1               (**r identity *)
     114  | intermediate_op1_ptrofint: intermediate_op1         (**r int to pointer *)
     115  | intermediate_op1_intofptr: intermediate_op1.        (**r pointer to int *)
    104116
    105117(* * Float types come in two sizes: 32 bits (single precision)
Note: See TracChangeset for help on using the changeset viewer.