Changeset 793


Ignore:
Timestamp:
May 12, 2011, 5:33:22 PM (9 years ago)
Author:
mulligan
Message:

Work from today on rtlabs -> rtl pass.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r789 r793  
    55
    66definition add_graph ≝
    7   λlbl: label.
     7  λl: label.
    88  λstmt.
    9   λdef.
    10   let f_labgen' ≝ f_labgen def in
    11   let f_reggen' ≝ f_reggen def in
    12   let f_sig' ≝ f_sig def in
    13   let f_result' ≝ f_result def in
    14   let f_params' ≝ f_params def in
    15   let f_locals' ≝ f_locals def in
    16   let f_ptrs' ≝ f_ptrs def in
    17   let f_stacksize' ≝ f_stacksize def in
    18   let f_graph' ≝ add ? ? (f_graph def) lbl stmt in
    19   let f_entry' ≝ f_entry def in
    20   let f_exit' ≝ f_exit def in
    21     mk_internal_function
    22       f_labgen' f_reggen' f_sig' f_result'
    23       f_params' f_locals' f_ptrs' f_stacksize'
    24       f_graph' f_entry' f_exit'.
     9  λp.
     10  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
     11  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
     12  let rtl_if_sig' ≝ rtl_if_sig p in
     13  let rtl_if_result' ≝ rtl_if_result p in
     14  let rtl_if_params' ≝ rtl_if_params p in
     15  let rtl_if_locals' ≝ rtl_if_locals p in
     16  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
     17  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
     18  let rtl_if_entry' ≝ rtl_if_entry p in
     19  let rtl_if_exit' ≝ rtl_if_exit p in
     20    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
     21                             rtl_if_params' rtl_if_params' rtl_if_locals'
     22                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
     23                             rtl_if_exit'.
    2524     
    2625definition fresh_label ≝
    2726  λdef.
    28     match fresh LabelTag (f_labgen def) with
     27    match fresh LabelTag (rtl_if_luniverse def) with
    2928    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    3029    | Error ⇒ None ?
    3130    ].
    3231
    33 axiom fresh_reg: internal_function → internal_function × register.
    34 
    35 let rec fresh_regs (def: internal_function) (n: nat) on n ≝
     32axiom fresh_reg: rtl_internal_function → rtl_internal_function × register.
     33
     34let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
    3635  match n with
    3736  [ O   ⇒ 〈def, [ ]〉
     
    137136definition change_label ≝
    138137  λlbl.
    139   λstmt.
     138  λstmt: rtl_statement.
    140139  match stmt with
    141140  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
     
    160159  ].
    161160
    162 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) def
     161let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function)
    163162  match stmt_list with
    164   [ nil ⇒ def
     163  [ nil ⇒ Some ? def
    165164  | cons hd tl ⇒
    166165    match tl with
    167     [ nil ⇒ add_graph start_lbl (change_lbl dest_lbl stmt) def
    168     | cons hd' tl' ⇒ ?
    169     ]
    170   ].
    171 
    172 let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
    173   | [] -> def
    174   | [stmt] ->
    175     add_graph start_lbl (change_label dest_lbl stmt) def
    176   | stmt :: stmt_list ->
    177     let tmp_lbl = fresh_label def in
    178     let stmt = change_label tmp_lbl stmt in
    179     let def = add_graph start_lbl stmt def in
    180     adds_graph stmt_list tmp_lbl dest_lbl def
     166    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
     167    | cons hd' tl' ⇒
     168      let tmp_lbl ≝ fresh_label def in
     169      match tmp_lbl with
     170      [ None ⇒ None ?
     171      | Some tmp_lbl ⇒
     172        let stmt ≝ change_label tmp_lbl hd in
     173        let def ≝ add_graph start_lbl stmt def in
     174          adds_graph tl tmp_lbl dest_lbl def
     175      ]
     176    ]
     177  ].
     178 
     179let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
     180                       (def: ?) on translate_list ≝
     181  match translate_list with
     182  [ nil ⇒ Some ? def
     183  | cons hd tl ⇒
     184    match tl with
     185    [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
     186    | cons hd' tl' ⇒
     187      let tmp_lbl ≝ fresh_label def in
     188      match tmp_lbl with
     189      [ None ⇒ None ?
     190      | Some tmp_lbl ⇒
     191        let def ≝ hd start_lbl tmp_lbl def in
     192          add_translates tl tmp_lbl dest_lbl def
     193      ]
     194    ]
     195  ].
     196 
     197
     198(* dpm: horrendous, use dependent types.
     199  length destr = length srcrs *)
     200let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
     201                       (dest_lbl: label) (def: ?) ≝
     202  match destrs with
     203  [ nil ⇒
     204    match srcrs with
     205    [ nil        ⇒ Some ? def
     206    | cons hd tl ⇒ None ?
     207    ]
     208  | cons hd tl ⇒
     209    match srcrs with
     210    [ nil        ⇒ None ?
     211    | cons hd' tl' ⇒
     212      match tl with
     213      [ nil            ⇒
     214        match tl' with
     215        (* one element lists *)
     216        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
     217        | cons hd'' tl'' ⇒ None ?
     218        ]
     219      | cons hd'' tl'' ⇒
     220        match tl' with
     221        [ nil ⇒ None ?
     222        (* multielement lists *)
     223        | cons hd''' tl''' ⇒
     224          let tmp_lbl ≝ fresh_label def in
     225          match tmp_lbl with
     226          [ None ⇒ None ?
     227          | Some tmp_lbl ⇒
     228            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
     229              translate_move tl tl' tmp_lbl dest_lbl def
     230          ]
     231        ]
     232      ]
     233    ]
     234  ].
     235
     236definition translate_cst ≝
     237  λcst.
     238  λdestrs.
     239  λstart_lbl.
     240  λdest_lbl.
     241  λdef.
     242  match cst with
     243  [ cast_int i ⇒
     244    match destrs with
     245    [ nil ⇒ None ?
     246    | cons hd tl ⇒
     247      match tl with
     248      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
     249      | cons hd' tl' ⇒ None ?
     250      ]
     251    ]
     252  | cast_addr_symbol id ⇒
     253    match destrs with
     254    [ nil ⇒ None ?
     255    | cons hd tl ⇒
     256      match tl with
     257      [ nil ⇒ None ?
     258      | cons hd' tl' ⇒
     259        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
     260      ]
     261    ]
     262  | cast_stack_offset off ⇒
     263    match destrs with
     264    [ nil ⇒ None ?
     265    | cons hd tl ⇒
     266      match tl with
     267      [ nil ⇒ None ?
     268      | cons hd' tl' ⇒
     269        let 〈def, tmpr〉 ≝ fresh_reg def in
     270        adds_graph [
     271          rtl_st_stack_addr hd hd' start_lbl;
     272          rtl_st_int tmpr off start_lbl;
     273          rtl_st_op2 Add hd hd tmpr start_lbl;
     274          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
     275          rtl_st_op2 Addc hd' hd' tmpr start_lbl
     276        ] start_lbl dest_lbl def
     277      ]
     278    ]
     279  | cast_float f ⇒ None ?
     280  ].
     281
     282definition extract_singleton ≝
     283  λA: Type[0].
     284  λl: list A.
     285  match l with
     286  [ nil ⇒ None ?
     287  | cons hd tl ⇒
     288    match tl with
     289    [ nil ⇒ Some ? hd
     290    | cons hd tl ⇒ None ?
     291    ]
     292  ].
     293
     294definition extract_pair ≝
     295  λA: Type[0].
     296  λl: list A.
     297  match l with
     298  [ nil ⇒ None ?
     299  | cons hd tl ⇒
     300    match tl with
     301    [ nil ⇒ None ?
     302    | cons hd' tl' ⇒
     303      match tl' with
     304      [ nil ⇒ Some ? 〈hd, hd'〉
     305      | cons hd'' tl'' ⇒ None ?
     306      ]
     307    ]
     308  ].
     309
     310definition translate_op1 ≝
     311  λop1.
     312  λdestrs.
     313  λsrcrs.
     314  λstart_lbl.
     315  λdest_lbl.
     316  λdef.
     317  match op1 with
     318  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
     319  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
     320  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
     321  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
     322  | op_neg_int ⇒
     323    let dstr ≝ extract_singleton ? destrs in
     324    let srcr ≝ extract_singleton ? srcrs in
     325    match dstr with
     326    [ None ⇒ None ?
     327    | Some dstr ⇒
     328      match srcr with
     329      [ None ⇒ None ?
     330      | Some srcr ⇒
     331        adds_graph [
     332          rtl_st_op1 Cmpl dstr srcr start_lbl;
     333          rtl_st_op1 Inc dstr dstr start_lbl
     334        ] start_lbl dest_lbl def
     335      ]
     336    ]
     337  | op_not_int ⇒
     338    let dstr ≝ extract_singleton ? destrs in
     339    let srcr ≝ extract_singleton ? srcrs in
     340    match dstr with
     341    [ None ⇒ None ?
     342    | Some dstr ⇒
     343      match srcr with
     344      [ None ⇒ None ?
     345      | Some srcr ⇒
     346        adds_graph [
     347          rtl_st_op1 Cmpl dstr srcr start_lbl
     348        ] start_lbl dest_lbl def
     349      ]
     350    ]
     351  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
     352  | op_ptr_of_int ⇒
     353    let destr12 ≝ extract_pair ? destrs in
     354    let srcr ≝ extract_singleton ? srcrs in
     355    match destr12 with
     356    [ None ⇒ None ?
     357    | Some destr12 ⇒
     358      let 〈destr1, destr2〉 ≝ destr12 in
     359      match srcr with
     360      [ None ⇒ None ?
     361      | Some srcr ⇒
     362        adds_graph [
     363          rtl_st_move destr1 srcr dest_lbl;
     364          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
     365        ] start_lbl dest_lbl def
     366      ]
     367    ]
     368  | op_int_of_ptr ⇒
     369    let destr ≝ extract_singleton ? destrs in
     370    match destr with
     371    [ None ⇒ None ?
     372    | Some destr ⇒
     373      match srcrs with
     374      [ nil ⇒ None ?
     375      | cons srcr tl ⇒
     376        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
     377      ]
     378    ]
     379  | op_not_bool ⇒
     380    let destr ≝ extract_singleton ? destrs in
     381    let srcrs ≝ extract_singleton ? srcrs in
     382    match destr with
     383    [ None ⇒ None ?
     384    | Some destr ⇒
     385      match srcrs with
     386      [ None ⇒ None ?
     387      | Some srcr ⇒
     388        let 〈def, tmpr〉 ≝ fresh_reg def in
     389        adds_graph [
     390          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
     391          rtl_st_clear_carry start_lbl;
     392          rtl_st_op2 Sub destr tmpr srcr start_lbl;
     393          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
     394          rtl_st_op2 Addc destr destr destr start_lbl;
     395          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
     396          rtl_st_op2 Xor destr destr tmpr start_lbl
     397        ] start_lbl dest_lbl def
     398      ]
     399    ]
     400  | _ ⇒ None ? (* error float *)
     401  ].
     402
     403definition translate_condptr ≝
     404  λr1.
     405  λr2.
     406  λstart_lbl: label.
     407  λlbl_true: label.
     408  λlbl_false: label.
     409  λdef.
     410  let 〈def, tmpr〉 ≝ fresh_reg def in
     411    adds_graph [
     412      rtl_st_op2 Or tmpr r1 r2 start_lbl;
     413      rtl_st_cond_acc tmpr lbl_true lbl_false
     414    ] start_lbl start_lbl def.
     415
     416let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
     417                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
     418  match op2 with
     419  [ op_add ⇒
     420    let destr ≝ extract_singleton ? destrs in
     421    let srcr1 ≝ extract_singleton ? srcrs1 in
     422    let srcr2 ≝ extract_singleton ? srcrs2 in
     423    match destr with
     424    [ None ⇒ None ?
     425    | Some destr ⇒
     426      match srcr1 with
     427      [ None ⇒ None ?
     428      | Some srcr1 ⇒
     429        match srcr2 with
     430        [ None ⇒ None ?
     431        | Some srcr2 ⇒
     432          adds_graph [
     433            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
     434          ] start_lbl dest_lbl def
     435        ]
     436      ]
     437    ]
     438  | op_sub ⇒
     439    let destr ≝ extract_singleton ? destrs in
     440    let srcr1 ≝ extract_singleton ? srcrs1 in
     441    let srcr2 ≝ extract_singleton ? srcrs2 in
     442    match destr with
     443    [ None ⇒ None ?
     444    | Some destr ⇒
     445      match srcr1 with
     446      [ None ⇒ None ?
     447      | Some srcr1 ⇒
     448        match srcr2 with
     449        [ None ⇒ None ?
     450        | Some srcr2 ⇒
     451          adds_graph [
     452            rtl_st_clear_carry start_lbl;
     453            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
     454          ] start_lbl dest_lbl def
     455        ]
     456      ]
     457    ]
     458  | op_mul ⇒
     459    let destr ≝ extract_singleton ? destrs in
     460    let srcr1 ≝ extract_singleton ? srcrs1 in
     461    let srcr2 ≝ extract_singleton ? srcrs2 in
     462    match destr with
     463    [ None ⇒ None ?
     464    | Some destr ⇒
     465      match srcr1 with
     466      [ None ⇒ None ?
     467      | Some srcr1 ⇒
     468        match srcr2 with
     469        [ None ⇒ None ?
     470        | Some srcr2 ⇒
     471          adds_graph [
     472            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
     473          ] start_lbl dest_lbl def
     474        ]
     475      ]
     476    ]
     477  | op_div ⇒ None ? (* signed div not supported *)
     478  | op_divu ⇒
     479    let destr ≝ extract_singleton ? destrs in
     480    let srcr1 ≝ extract_singleton ? srcrs1 in
     481    let srcr2 ≝ extract_singleton ? srcrs2 in
     482    match destr with
     483    [ None ⇒ None ?
     484    | Some destr ⇒
     485      match srcr1 with
     486      [ None ⇒ None ?
     487      | Some srcr1 ⇒
     488        match srcr2 with
     489        [ None ⇒ None ?
     490        | Some srcr2 ⇒
     491          adds_graph [
     492            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
     493          ] start_lbl dest_lbl def
     494        ]
     495      ]
     496    ]
     497  | op_modu ⇒
     498    let destr ≝ extract_singleton ? destrs in
     499    let srcr1 ≝ extract_singleton ? srcrs1 in
     500    let srcr2 ≝ extract_singleton ? srcrs2 in
     501    match destr with
     502    [ None ⇒ None ?
     503    | Some destr ⇒
     504      match srcr1 with
     505      [ None ⇒ None ?
     506      | Some srcr1 ⇒
     507        match srcr2 with
     508        [ None ⇒ None ?
     509        | Some srcr2 ⇒
     510          adds_graph [
     511            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
     512          ] start_lbl dest_lbl def
     513        ]
     514      ]
     515    ]
     516  | op_mod ⇒ None ? (* signed mod not supported *)
     517  | op_and ⇒
     518    let destr ≝ extract_singleton ? destrs in
     519    let srcr1 ≝ extract_singleton ? srcrs1 in
     520    let srcr2 ≝ extract_singleton ? srcrs2 in
     521    match destr with
     522    [ None ⇒ None ?
     523    | Some destr ⇒
     524      match srcr1 with
     525      [ None ⇒ None ?
     526      | Some srcr1 ⇒
     527        match srcr2 with
     528        [ None ⇒ None ?
     529        | Some srcr2 ⇒
     530          adds_graph [
     531            rtl_st_op2 And destr srcr1 srcr2 start_lbl
     532          ] start_lbl dest_lbl def
     533        ]
     534      ]
     535    ]
     536  | op_or ⇒
     537    let destr ≝ extract_singleton ? destrs in
     538    let srcr1 ≝ extract_singleton ? srcrs1 in
     539    let srcr2 ≝ extract_singleton ? srcrs2 in
     540    match destr with
     541    [ None ⇒ None ?
     542    | Some destr ⇒
     543      match srcr1 with
     544      [ None ⇒ None ?
     545      | Some srcr1 ⇒
     546        match srcr2 with
     547        [ None ⇒ None ?
     548        | Some srcr2 ⇒
     549          adds_graph [
     550            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
     551          ] start_lbl dest_lbl def
     552        ]
     553      ]
     554    ]
     555  | op_xor ⇒
     556    let destr ≝ extract_singleton ? destrs in
     557    let srcr1 ≝ extract_singleton ? srcrs1 in
     558    let srcr2 ≝ extract_singleton ? srcrs2 in
     559    match destr with
     560    [ None ⇒ None ?
     561    | Some destr ⇒
     562      match srcr1 with
     563      [ None ⇒ None ?
     564      | Some srcr1 ⇒
     565        match srcr2 with
     566        [ None ⇒ None ?
     567        | Some srcr2 ⇒
     568          adds_graph [
     569            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
     570          ] start_lbl dest_lbl def
     571        ]
     572      ]
     573    ]
     574  | op_shru ⇒ None ? (* shifts not supported *)
     575  | op_shr ⇒ None ?
     576  | op_shl ⇒ None ?
     577  | op_addf ⇒ None ? (* floats not supported *)
     578  | op_subf ⇒ None ?
     579  | op_mulf ⇒ None ?
     580  | op_divf ⇒ None ?
     581  | op_cmpf _ ⇒ None ?
     582  | op_addp ⇒ ?
     583  | _ ⇒ ?
     584  ].
     585
     586    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
     587    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
     588      let (def, tmpr1) = fresh_reg def in
     589      let (def, tmpr2) = fresh_reg def in
     590      adds_graph
     591        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
     592         RTL.St_int (tmpr2, 0, start_lbl) ;
     593         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
     594         RTL.St_move (destr1, tmpr1, start_lbl)]
     595        start_lbl dest_lbl def
     596
     597    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
     598      let (def, tmpr1) = fresh_reg def in
     599      let (def, tmpr2) = fresh_reg def in
     600      adds_graph
     601        [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
     602         RTL.St_int (tmpr2, 1, start_lbl) ;
     603         RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
     604         RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
     605        start_lbl dest_lbl def
     606
     607    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
     608      adds_graph
     609        [RTL.St_clear_carry start_lbl ;
     610         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
     611         RTL.St_int (destr2, 0, start_lbl) ;
     612         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
     613        start_lbl dest_lbl def
     614
     615    | AST.Op_cmp AST.Cmp_eq, _, _, _
     616    | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
     617      add_translates
     618        [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
     619         translate_op1 AST.Op_notbool destrs destrs]
     620        start_lbl dest_lbl def
     621
     622    | AST.Op_cmp AST.Cmp_ne, _, _, _
     623    | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
     624      translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     625
     626    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
     627      let (def, tmpr) = fresh_reg def in
     628      adds_graph
     629        [RTL.St_clear_carry start_lbl ;
     630         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
     631         RTL.St_int (destr, 0, start_lbl) ;
     632         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
     633        start_lbl dest_lbl def
     634
     635    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
     636      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
     637        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     638
     639    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
     640      add_translates
     641        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
     642         translate_op1 AST.Op_notbool destrs destrs]
     643        start_lbl dest_lbl def
     644
     645    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
     646      add_translates
     647        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     648         translate_op1 AST.Op_notbool destrs destrs]
     649        start_lbl dest_lbl def
     650
     651    | AST.Op_cmp cmp, _, _, _ ->
     652      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
     653      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
     654      add_translates
     655        [translate_cst (AST.Cst_int 128) tmprs1 ;
     656         translate_cst (AST.Cst_int 128) tmprs2 ;
     657         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
     658         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
     659         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2]
     660        start_lbl dest_lbl def
     661
     662    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
     663      let (def, tmpr) = fresh_reg def in
     664      add_translates
     665        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
     666         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
     667         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
     668         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
     669         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
     670        start_lbl dest_lbl def
     671
     672    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
     673      let (def, tmpr1) = fresh_reg def in
     674      let (def, tmpr2) = fresh_reg def in
     675      add_translates
     676        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
     677         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
     678         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
     679         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
     680         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
     681        start_lbl dest_lbl def
     682
     683    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
     684      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
     685        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     686
     687    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
     688      add_translates
     689        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
     690         translate_op1 AST.Op_notbool destrs destrs]
     691        start_lbl dest_lbl def
     692
     693    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
     694      add_translates
     695        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     696         translate_op1 AST.Op_notbool destrs destrs]
     697        start_lbl dest_lbl def
     698
     699    | _ -> assert false (* wrong number of arguments *)
  • src/common/AST.ma

    r764 r793  
    540540
    541541definition Trace ≝ list Identifier.
     542
     543(* dpm: how are floats represented? *)
     544inductive cast: Type[0] ≝
     545  | cast_int: Byte → cast                    (* integer constant *)
     546  | cast_float: Byte → cast                  (* float constant *)
     547  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
     548  | cast_stack_offset: Byte → cast.
     549
     550inductive op1: Type[0] ≝
     551  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
     552  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
     553  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
     554  | op_cast16_signed: op1    (**r 16-bit sign extension *)
     555  | op_neg_int: op1          (**r integer opposite *)
     556  | op_not_bool: op1         (**r boolean negation  *)
     557  | op_not_int: op1          (**r bitwise complement  *)
     558  | op_negf: op1             (**r float opposite *)
     559  | op_absf: op1             (**r float absolute value *)
     560  | op_single_of_float: op1  (**r float truncation *)
     561  | op_int_of_float: op1     (**r signed integer to float *)
     562  | op_intu_of_float: op1    (**r unsigned integer to float *)
     563  | op_float_of_int: op1     (**r float to signed integer *)
     564  | op_float_of_intu: op1    (**r float to unsigned integer *)
     565  | op_id: op1               (**r identity *)
     566  | op_ptr_of_int: op1       (**r int to pointer *)
     567  | op_int_of_ptr: op1.      (**r pointer to int *)
     568
     569inductive op2: Type[0] ≝
     570  | op_add: op2         (**r integer addition *)
     571  | op_sub: op2         (**r integer subtraction *)
     572  | op_mul: op2         (**r integer multiplication *)
     573  | op_div: op2         (**r integer signed division *)
     574  | op_divu: op2        (**r integer unsigned division *)
     575  | op_mod: op2         (**r integer signed modulus *)
     576  | op_modu: op2        (**r integer unsigned modulus *)
     577  | op_and: op2         (**r bitwise ``and'' *)
     578  | op_or: op2          (**r bitwise ``or'' *)
     579  | op_xor: op2         (**r bitwise ``xor'' *)
     580  | op_shl: op2         (**r left shift *)
     581  | op_shr: op2         (**r right signed shift *)
     582  | op_shru: op2        (**r right unsigned shift *)
     583  | op_addf: op2        (**r float addition *)
     584  | op_subf: op2        (**r float subtraction *)
     585  | op_mulf: op2        (**r float multiplication *)
     586  | op_divf: op2        (**r float division *)
     587  | op_cmp: Compare → op2   (**r integer signed comparison *)
     588  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
     589  | op_cmpf: Compare → op2  (**r float comparison *)
     590  | op_addp: op2        (**r addition for a pointer and an integer *)
     591  | op_subp: op2        (**r substraction for a pointer and a integer *)
     592  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset for help on using the changeset viewer.