Changeset 799 for src/RTLabs


Ignore:
Timestamp:
May 13, 2011, 5:35:04 PM (9 years ago)
Author:
mulligan
Message:

more changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r795 r799  
    417417    ] start_lbl start_lbl def.
    418418
     419(*
    419420let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
    420421                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
     
    693694    | Compare_NotEqual ⇒
    694695      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     696    | Compare
    695697    | _ ⇒ None ?
    696698    ]
    697699  | _ ⇒ ?
    698700  ].
    699 
    700     | AST.Op_cmp AST.Cmp_ne, _, _, _
    701     | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
    702       translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    703701
    704702    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
     
    776774
    777775    | _ -> assert false (* wrong number of arguments *)
     776*)
     777
     778definition translate_condcst ≝
     779  λcst.
     780  λstart_lbl: label.
     781  λlbl_true: label.
     782  λlbl_false: label.
     783  λdef.
     784  match cst with
     785  [ cast_int i ⇒
     786    let 〈def, tmpr〉 ≝ fresh_reg def in
     787    adds_graph [
     788      rtl_st_int tmpr i start_lbl;
     789      rtl_st_cond_acc tmpr lbl_true lbl_false
     790    ] start_lbl start_lbl def
     791  | cast_addr_symbol x ⇒
     792    let 〈def, r1〉 ≝ fresh_reg def in
     793    let 〈def, r2〉 ≝ fresh_reg def in
     794    let lbl ≝ fresh_label def in
     795    match lbl with
     796    [ None ⇒ None ?
     797    | Some lbl ⇒
     798      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
     799        translate_condptr r1 r2 lbl lbl_true lbl_false def
     800    ]
     801  | cast_stack_offset off ⇒
     802    let 〈def, r1〉 ≝ fresh_reg def in
     803    let 〈def, r2〉 ≝ fresh_reg def in
     804    let tmp_lbl ≝ fresh_label def in
     805    match tmp_lbl with
     806    [ None ⇒ None ?
     807    | Some tmp_lbl ⇒
     808      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
     809      match def with
     810      [ None ⇒ None ?
     811      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
     812      ]
     813    ]
     814  | cast_float f ⇒ None ? (* error_float *)
     815  ].
     816
     817definition size_of_op1_ret ≝
     818  λop.
     819  match op with
     820  [ op_cast8_unsigned ⇒ Some ? 1
     821  | op_cast8_signed ⇒ Some ? 1
     822  | op_cast16_unsigned ⇒ Some ? 1
     823  | op_cast16_signed ⇒ Some ? 1
     824  | op_neg_int ⇒ Some ? 1
     825  | op_not_int ⇒ Some ? 1
     826  | op_int_of_ptr ⇒ Some ? 1
     827  | op_ptr_of_int ⇒ Some ? 2
     828  | op_id ⇒ None ? (* invalid_argument *)
     829  | _ ⇒ None ? (* error_float *)
     830  ].
     831
     832definition translate_cond1 ≝
     833  λop1.
     834  λsrcrs: list register.
     835  λstart_lbl: label.
     836  λlbl_true: label.
     837  λlbl_false: label.
     838  λdef.
     839  match op1 with
     840  [ op_id ⇒
     841    let srcr ≝ extract_singleton ? srcrs in
     842    match srcr with
     843    [ None ⇒
     844      let srcr12 ≝ extract_pair ? srcrs in
     845      match srcr12 with
     846      [ None ⇒ None ?
     847      | Some srcr12 ⇒
     848        let 〈srcr1, srcr2〉 ≝ srcr12 in
     849          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
     850      ]
     851    | Some srcr ⇒
     852      adds_graph [
     853        rtl_st_cond_acc srcr lbl_true lbl_false
     854      ] start_lbl start_lbl def
     855    ]
     856  | _     ⇒
     857    let size ≝ size_of_op1_ret op1 in
     858    match size with
     859    [ None ⇒ None ?
     860    | Some size ⇒
     861      let 〈def, destrs〉 ≝ fresh_regs def size in
     862      let lbl ≝ fresh_label def in
     863      match lbl with
     864      [ None ⇒ None ?
     865      | Some lbl ⇒
     866        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
     867        match def with
     868        [ None ⇒ None ?
     869        | Some def ⇒
     870          let destr ≝ extract_singleton ? destrs in
     871          match destr with
     872          [ None ⇒
     873            let destr12 ≝ extract_pair ? destrs in
     874            match destr12 with
     875            [ None ⇒ None ?
     876            | Some destr12 ⇒
     877              let 〈destr1, destr2〉 ≝ destr12 in
     878                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
     879            ]
     880          | Some destr ⇒
     881            adds_graph [
     882              rtl_st_cond_acc destr lbl_true lbl_false
     883            ] start_lbl start_lbl def
     884          ]
     885        ]
     886      ]
     887    ]
     888  ].
     889
     890definition size_of_op2_ret ≝
     891  λn: nat.
     892  λop2.
     893  match op2 with
     894  [ op_add ⇒ Some ? 1
     895  | op_sub ⇒ Some ? 1
     896  | op_mul ⇒ Some ? 1
     897  | op_div ⇒ Some ? 1
     898  | op_divu ⇒ Some ? 1
     899  | op_mod ⇒ Some ? 1
     900  | op_modu ⇒ Some ? 1
     901  | op_and ⇒ Some ? 1
     902  | op_or ⇒ Some ? 1
     903  | op_xor ⇒ Some ? 1
     904  | op_shl ⇒ Some ? 1
     905  | op_shr ⇒ Some ? 1
     906  | op_shru ⇒ Some ? 1
     907  | op_cmp _ ⇒ Some ? 1
     908  | op_cmpu _ ⇒ Some ? 1
     909  | op_cmpp _ ⇒ Some ? 1
     910  | op_addp ⇒ Some ? 2
     911  | op_subp ⇒
     912    if eq_nat n 4 then
     913      Some ? 1
     914    else
     915      Some ? 2
     916  | _ ⇒ None ? (* error_float *)
     917  ].
     918
     919definition translate_cond2 ≝
     920  λop2.
     921  λsrcrs1: list register.
     922  λsrcrs2: list register.
     923  λstart_lbl: label.
     924  λlbl_true: label.
     925  λlbl_false: label.
     926  λdef.
     927  match op2 with
     928  [
     929  ]
     930
     931let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
     932  match op2, srcrs1, srcrs2 with
     933
     934    | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
     935      let (def, tmpr) = fresh_reg def in
     936      adds_graph
     937        [RTL.St_clear_carry start_lbl ;
     938         RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
     939         RTL.St_condacc (tmpr, lbl_false, lbl_true)]
     940        start_lbl start_lbl def
     941
     942    | _, _, _ ->
     943      let n = (List.length srcrs1) + (List.length srcrs2) in
     944      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
     945      let lbl = fresh_label def in
     946      let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
     947      translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
Note: See TracChangeset for help on using the changeset viewer.