Changeset 1045 for src/RTLabs


Ignore:
Timestamp:
Jun 29, 2011, 10:47:39 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict in rtlabs

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r799 r1045  
    2727    match fresh LabelTag (rtl_if_luniverse def) with
    2828    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    29     | Error ⇒ None ?
     29    | Error _ ⇒ None ?
    3030    ].
    3131
     
    917917  ].
    918918
     919axiom translate_op2:
     920  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
     921
    919922definition translate_cond2 ≝
    920923  λop2.
     
    926929  λdef.
    927930  match op2 with
     931  [ op_cmp cmp ⇒
     932    match cmp with
     933    [ Compare_Equal ⇒
     934      let srcr1 ≝ extract_singleton ? srcrs1 in
     935      match srcr1 with
     936      [ None ⇒ None ?
     937      | Some srcr1 ⇒
     938        let srcr2 ≝ extract_singleton ? srcrs2 in
     939        match srcr2 with
     940        [ None ⇒ None ?
     941        | Some srcr2 ⇒
     942          let 〈def, tmpr〉 ≝ fresh_reg def in
     943          adds_graph [
     944            rtl_st_clear_carry start_lbl;
     945            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
     946            rtl_st_cond_acc tmpr lbl_false lbl_true
     947          ] start_lbl start_lbl def
     948        ]
     949      ]
     950    | _ ⇒
     951      let n ≝ length ? srcrs1 + length ? srcrs2 in
     952      match size_of_op2_ret n op2 with
     953      [ None ⇒ None ?
     954      | Some size ⇒
     955        let 〈def, destrs〉 ≝ fresh_regs def size in
     956        let lbl ≝ fresh_label def in
     957        match lbl with
     958        [ None ⇒ None ?
     959        | Some lbl ⇒
     960          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
     961          [ None ⇒ None ?
     962          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
     963          ]
     964        ]
     965      ]
     966    ]
     967  | _ ⇒
     968    let n ≝ length ? srcrs1 + length ? srcrs2 in
     969    match size_of_op2_ret n op2 with
     970    [ None ⇒ None ?
     971    | Some size ⇒
     972      let 〈def, destrs〉 ≝ fresh_regs def size in
     973      let lbl ≝ fresh_label def in
     974      match lbl with
     975      [ None ⇒ None ?
     976      | Some lbl ⇒
     977        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
     978        [ None ⇒ None ?
     979        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
     980        ]
     981      ]
     982    ]
     983  ].
     984
     985let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
     986                           (destr2: ?) (start_lbl: label)
     987                           (dest_lbl: label) (def: rtl_internal_function) ≝
     988  let destrs ≝ [ destr1; destr2 ] in
     989  match mode with
     990  [ Aindexed off ⇒
     991    let srcr12 ≝ extract_singleton ? args in
     992    match srcr12 with
     993    [ None ⇒ None ?
     994    | Some srcr12 ⇒
     995      let srcr12 ≝ extract_pair ? srcr12 in
     996      match srcr12 with
     997      [ None ⇒ None ?
     998      | Some srcr12 ⇒
     999        let 〈srcr1, srcr2〉 ≝ srcr12 in
     1000        let 〈def, tmpr〉 ≝ fresh_reg def in
     1001        add_translates [
     1002          adds_graph [
     1003            rtl_st_int tmpr off start_lbl
     1004          ];
     1005          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
     1006        ] start_lbl dest_lbl def
     1007      ]
     1008    ]
     1009  | Aindexed2 ⇒
     1010    let args_pair ≝ extract_pair ? args in
     1011    match args_pair with
     1012    [ None ⇒ None ?
     1013    | Some args_pair ⇒
     1014      let 〈lft, rgt〉 ≝ args_pair in
     1015      let srcr1112 ≝ extract_pair ? lft in
     1016      let srcr2 ≝ extract_singleton ? rgt in
     1017      match srcr1112 with
     1018      [ None ⇒
     1019        let srcr2 ≝ extract_singleton ? rgt in
     1020        let srcr1112 ≝ extract_pair ? lft in
     1021        match srcr2 with
     1022        [ None ⇒ None ?
     1023        | Some srcr2 ⇒
     1024          match srcr1112 with
     1025          [ None ⇒ None ?
     1026          | Some srcr1112 ⇒
     1027            let 〈srcr11, srcr12〉 ≝ srcr1112 in
     1028            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
     1029          ]
     1030        ]
     1031      | Some srcr1112 ⇒
     1032        let 〈srcr11, srcr12〉 ≝ srcr1112 in
     1033        match srcr2 with
     1034        [ None ⇒ None ?
     1035        | Some srcr2 ⇒
     1036          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
     1037        ]
     1038      ]
     1039    ]
     1040  | Aglobal x off ⇒
     1041    let 〈def, tmpr〉 ≝ fresh_reg def in
     1042    add_translates [
     1043      adds_graph [
     1044        rtl_st_int tmpr off start_lbl;
     1045        rtl_st_addr destr1 destr2 x start_lbl
     1046      ];
     1047      translate_op2 op_addp destrs destrs [ tmpr ]
     1048    ] start_lbl dest_lbl def
     1049  | Abased x off ⇒
     1050    let srcrs ≝ extract_singleton ? args in
     1051    match srcrs with
     1052    [ None ⇒ None ?
     1053    | Some srcrs ⇒
     1054      let 〈def, tmpr1〉 ≝ fresh_reg def in
     1055      let 〈def, tmpr2〉 ≝ fresh_reg def in
     1056      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
     1057      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
     1058      let address_unfold ≝
     1059        let 〈def, tmpr〉 ≝ fresh_reg def in
     1060          add_translates [
     1061            adds_graph [
     1062              rtl_st_int tmpr off start_lbl;
     1063              rtl_st_addr tmpr1 tmpr2 x start_lbl
     1064           ];
     1065            translate_op2 op_addp destrs destrs [ tmpr ]
     1066         ]
     1067      in
     1068      add_translates [
     1069        address_unfold;
     1070        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
     1071      ] start_lbl dest_lbl def
     1072    ]
     1073  | Ainstack off ⇒
     1074    let 〈def, tmpr〉 ≝ fresh_reg def in
     1075    add_translates [
     1076      adds_graph [
     1077        rtl_st_int tmpr off start_lbl;
     1078        rtl_st_stack_addr destr1 destr2 start_lbl
     1079      ];
     1080      translate_op2 op_addp destrs destrs [ tmpr ]
     1081    ] start_lbl dest_lbl def
     1082  | _ ⇒ None ? (* wrong number of arguments *)
     1083  ].
     1084
     1085definition translate_load ≝
     1086  λq.
     1087  λmode.
     1088  λargs.
     1089  λdestrs.
     1090  λstart_lbl: label.
     1091  λdest_lbl: label.
     1092  λdef.
     1093  match q with
    9281094  [
    929   ]
    930 
    931 let 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] ->
     1095  ].
     1096
     1097let translate_load q mode args destrs start_lbl dest_lbl def =
     1098  match q, destrs with
     1099
     1100    | Memory.QInt 1, [destr] ->
     1101      let (def, addr1) = fresh_reg def in
     1102      let (def, addr2) = fresh_reg def in
     1103      add_translates
     1104        [addressing_pointer mode args addr1 addr2 ;
     1105         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
     1106        start_lbl dest_lbl def
     1107
     1108    | Memory.QPtr, [destr1 ; destr2] ->
     1109      let (def, addr1) = fresh_reg def in
     1110      let (def, addr2) = fresh_reg def in
     1111      let addr = [addr1 ; addr2] in
    9351112      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
     1113      add_translates
     1114        [addressing_pointer mode args addr1 addr2 ;
     1115         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
     1116                     RTL.St_int (tmpr, 1, start_lbl)] ;
     1117         translate_op2 AST.Op_addp addr addr [tmpr] ;
     1118         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
     1119        start_lbl dest_lbl def
     1120
     1121    | _ -> error "Size error in load."
  • src/RTLabs/syntax.ma

    r888 r1045  
    1010include "common/Graphs.ma".
    1111
    12 (* Statements, including the label of successor(s). *)
     12definition immediate : Type[0] ≝ Byte.
     13
     14(* Addressing modes *)
     15
     16inductive addressing : Type[0] ≝
     17(* dpm: changed from int to Byte *)
     18| Aindexed  : immediate → addressing         (* r1 + offset *)
     19| Aindexed2 : addressing                     (* r1 + r2 *)
     20| Aglobal   : ident → immediate → addressing (* global + offset *)
     21| Abased    : ident → immediate → addressing (* global + offset + r1 *)
     22| Ainstack  : immediate → addressing         (* stack + offset *)
     23.
     24
     25definition addr_mode_args : addressing → nat ≝
     26λa. match a with
     27[ Aindexed _  ⇒ 1
     28| Aindexed2   ⇒ 2
     29| Aglobal _ _ ⇒ 0
     30| Abased _ _  ⇒ 1
     31| Ainstack _  ⇒ 0
     32].
     33
     34definition addr ≝ λm.Vector register (addr_mode_args m).
    1335
    1436inductive statement : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.