Changeset 1066 for src/RTLabs


Ignore:
Timestamp:
Jul 13, 2011, 5:12:10 PM (10 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/RTLAbstoRTL.ma

    r1064 r1066  
    204204  λA.
    205205  λlst: list A.
    206   λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)
    207   match lst return λx. length A x = 2 → A × A with
     206  λprf: 2 ≤ length A lst.
     207  match lst return λx. 2 ≤ |x| → A × A with
    208208  [ nil ⇒ λlst_nil_prf. ?
    209209  | cons hd tl ⇒ λprf.
    210     match tl return λx. length A x = 1 → A × A with
     210    match tl return λx. 1 ≤ |x| → A × A with
    211211    [ nil ⇒ λtl_nil_prf. ?
    212212    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    … …  
    214214  ] prf.
    215215  [1: normalize in lst_nil_prf;
    216       destruct(lst_nil_prf);
     216      cases(not_le_Sn_O 1);
     217      #HYP cases(HYP lst_nil_prf)
    217218  |2: normalize in prf;
    218       destruct(prf)
    219       @e0
     219      @le_S_S_to_le
     220      assumption
    220221  |3: normalize in tl_nil_prf;
    221       destruct(tl_nil_prf);
     222      cases(not_le_Sn_O 0)
     223      #HYP cases(HYP tl_nil_prf)
    222224  ]
    223225qed.
    … …  
    253255  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
    254256  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
    255   | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
     257  | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2
    256258  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
    257259  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    … …  
    394396  λdestrs.
    395397  λsrcrs.
    396   match | srcrs | return λx. | srcrs | = x → ? with
     398  match |srcrs| return λx. |srcrs| = x → ? with
    397399  [ O ⇒ λzero_prf. adds_graph [ ]
    398400  | S n' ⇒ λsucc_prf.
    … …  
    466468  ].
    467469
     470(* TODO: examine this properly.  This is a change from the O'caml code due
     471   to us dropping the explicit use of a cast destination size field.  We
     472   instead infer the size of the cast's destination from the context.  Is
     473   this correct?
     474*)
    468475definition translate_op1 ≝
    469   λop1: op1.
     476  λop1: unary_operation.
    470477  λdestrs: list register.
    471478  λsrcrs: list register.
    … …  
    475482  λdef: rtl_internal_function.
    476483  match op1 with
    477   [ op_cast src_size src_sign dest_size ⇒
     484  [ Ocastint src_sign src_size ⇒
     485    let dest_size ≝ |destrs| * 8 in
     486    let src_size ≝ bitsize_of_intsize src_size in
    478487      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    479   | op_neg_int ⇒
     488  | Onegint ⇒
    480489      translate_negint destrs srcrs start_lbl dest_lbl def prf
    481   | op_not_bool ⇒
     490  | Onotbool ⇒
    482491      translate_notbool destrs srcrs start_lbl dest_lbl def
    483   | op_not_int ⇒
     492  | Onotint ⇒
    484493    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
    485494    let l ≝ map2 … f destrs srcrs prf in
    486495      adds_graph l start_lbl dest_lbl def
    487   | op_ptr_of_int ⇒
     496  | Optrofint r ⇒
    488497      translate_move destrs srcrs start_lbl dest_lbl def
    489   | op_int_of_ptr ⇒
     498  | Ointofptr r ⇒
    490499      translate_move destrs srcrs start_lbl dest_lbl def
    491   | op_id ⇒
     500  | Oid ⇒
    492501      translate_move destrs srcrs start_lbl dest_lbl def
    493   ].
     502  | _ ⇒ ? (* float operations implemented in runtime *)
     503  ].
     504  cases not_implemented
     505qed.
    494506 
    495507definition translate_op ≝
    … …  
    498510  λsrcrs1.
    499511  λsrcrs2.
    500   λprf: |srcrs1| = |srcrs2|.
    501512  λstart_lbl.
    502513  λdest_lbl.
    … …  
    533544    ]
    534545  ].
    535 cases not_implemented (* problem here with lengths of lists: possible bug? *)
     546  [1: @third_reduced_proof
     547  |3: @first_reduced_proof
     548  |*: cases daemon (* TODO *)
     549  ]
    536550qed.
    537551
    … …  
    597611  λdestrs: list register.
    598612  λtmp_destrs: list register.
    599   λdestrs_prf: |destrs| = |tmp_destrs|.
    600613  λsrcrs1: list register.
    601614  λdummy_lbl: label.
    … …  
    618631          rtl_st_clear_carry dummy_lbl
    619632        ];
    620         translate_op Addc destrs destrs tmp_destrs destrs_prf
     633        translate_op Addc destrs destrs tmp_destrs
    621634      ]
    622635    ]
    … …  
    822835  λsrcrs1: list register.
    823836  λsrcrs2: list register.
    824   λprf_srcrs: |srcrs1| = |srcrs2|.
    825837  λstart_lbl: label.
    826838  λdest_lbl: label.
    … …  
    889901  λsrcrs1: list register.
    890902  λsrcrs2: list register.
    891   λsrcrs_prf: |srcrs1| = |srcrs2|.
    892903  λsrcrs1_lt_prf: 0 < |srcrs1|.
     904  λsrcrs2_lt_prf: 0 < |srcrs2|.
    893905  λstart_lbl: label.
    894906  λdest_lbl: label.
    … …  
    911923          add_128_to_last tmp_128 tmp_srcrs1 ?;
    912924          add_128_to_last tmp_128 tmp_srcrs2 ?;
    913           translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 ?
     925          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
    914926        ] start_lbl dest_lbl def
    915927    ]
    916928  ].
    917   [2: >srcrs2_prf >srcrs1_prf @srcrs_prf
    918   |3: >srcrs2_prf <srcrs_prf @srcrs1_lt_prf
    919   |1: >srcrs1_prf @srcrs1_lt_prf
     929  [1: >srcrs1_prf @srcrs1_lt_prf
     930  |2: >srcrs2_prf @srcrs2_lt_prf
    920931  ]
    921932qed.
    … …  
    927938  λsrcrs1: list register.
    928939  λsrcrs2: list register.
    929   λsrcrs_prf: |srcrs1| = |srcrs2|.
     940  λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
     941                                   but we need more dep. typ. in modu/divu
     942                                   cases *)
     943  λsrcrs2_prf: lt 0 (|srcrs2|).
    930944  λstart_lbl: label.
    931945  λdest_lbl: label.
    932946  λdef: rtl_internal_function.
    933947  match op2 with
    934   [ op_add ⇒
    935     translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    936   | op_addp ⇒
    937     translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    938   | op_sub ⇒
    939     translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    940   | op_subp ⇒
    941     translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    942   | op_subpp ⇒
    943     translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    944   | op_mul ⇒
    945     translate_op Mul destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    946   | op_divu ⇒ ?
    947   | op_modu ⇒ ?
    948   | op_and ⇒
    949     translate_op And destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    950   | op_or ⇒
    951     translate_op Or destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    952   | op_xor ⇒
    953     translate_op Xor destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
    954   | op_cmp c ⇒
     948  [ Oadd ⇒
     949    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     950  | Oaddp ⇒
     951    translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     952  | Osub ⇒
     953    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     954  | Osubpi ⇒
     955    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     956  | Osubpp sz ⇒
     957    translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     958  | Omul ⇒
     959    translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
     960  | Odivu ⇒
     961    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     962    [ cons hd tl ⇒ λcons_prf.
     963      match tl with
     964      [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     965      | _ ⇒ ? (* not implemented *)
     966      ]
     967    | nil ⇒ λnil_absrd. ?
     968    ] srcrs1_prf
     969  | Omodu ⇒
     970    match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     971    [ cons hd tl ⇒ λcons_prf.
     972      match tl with
     973      [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     974      | _ ⇒ ? (* not implemented *)
     975      ]
     976    | nil ⇒ λnil_absrd. ?
     977    ] srcrs1_prf
     978  | Oand ⇒
     979    translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
     980  | Oor ⇒
     981    translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
     982  | Oxor ⇒
     983    translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
     984  | Ocmp c ⇒
    955985    match c with
    956     [ Compare_Equal ⇒
     986    [ Ceq ⇒
    957987      add_translates [
    958         translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def;
    959         translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     988        translate_ne destrs srcrs1 srcrs2;
     989        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
    960990      ] start_lbl dest_lbl def
    961     | Compare_NotEqual ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    962     | Compare_Less ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def
    963     | Compare_Greater ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def
    964     | Compare_LessEqual ⇒
     991    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     992    | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
     993    | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
     994    | Cle ⇒
    965995      add_translates [
    966         translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def;
    967         translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     996        translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
     997        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
    968998      ] start_lbl dest_lbl def
    969     | Compare_GreaterEqual ⇒
     999    | Cge ⇒
    9701000      add_translates [
    971         translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def;
    972         translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     1001        translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
     1002        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
    9731003      ] start_lbl dest_lbl def
    9741004    ]
     1005  | Ocmpu c ⇒
     1006    match c with
     1007    [ Ceq ⇒
     1008      add_translates [
     1009        translate_ne destrs srcrs1 srcrs2;
     1010        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1011      ] start_lbl dest_lbl def
     1012    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     1013    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     1014    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     1015    | Cle ⇒
     1016      add_translates [
     1017        translate_lt destrs destrs_prf srcrs2 srcrs1;
     1018        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1019      ] start_lbl dest_lbl def
     1020    | Cge ⇒
     1021      add_translates [
     1022        translate_lt destrs destrs_prf srcrs1 srcrs2;
     1023        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1024      ] start_lbl dest_lbl def
     1025    ]
     1026  | Ocmpp c ⇒
     1027    match c with
     1028    [ Ceq ⇒
     1029      add_translates [
     1030        translate_ne destrs srcrs1 srcrs2;
     1031        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1032      ] start_lbl dest_lbl def
     1033    | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     1034    | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     1035    | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     1036    | Cle ⇒
     1037      add_translates [
     1038        translate_lt destrs destrs_prf srcrs2 srcrs1;
     1039        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1040      ] start_lbl dest_lbl def
     1041    | Cge ⇒
     1042      add_translates [
     1043        translate_lt destrs destrs_prf srcrs1 srcrs2;
     1044        translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     1045      ] start_lbl dest_lbl def
     1046    ]
     1047  | _ ⇒ ? (* assert false, implemented in run time or float op *)
     1048  ].
     1049  [ 2,6: normalize in nil_absrd;
     1050         cases(not_le_Sn_O 0)
     1051         #HYP cases(HYP nil_absrd)
     1052  | 3,7,12,17,13,15,18,19,20,21,14,16:
     1053         assumption
     1054  | *:   cases not_implemented (* yes, really *)
     1055  ]
     1056qed.
     1057
     1058definition translate_cond ≝
     1059  λsrcrs: list register.
     1060  λstart_lbl: label.
     1061  λlbl_true: label.
     1062  λlbl_false: label.
     1063  λdef: rtl_internal_function.
     1064  let 〈def, tmpr〉 ≝ fresh_reg def in
     1065  let 〈def, tmp_lbl〉 ≝ fresh_label def in
     1066  let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
     1067  let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
     1068  let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
     1069    add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
     1070
     1071definition translate_load ≝
     1072  λaddr.
     1073  λaddr_prf: 2 ≤ |addr|.
     1074  λdestrs: list register.
     1075  λstart_lbl: label.
     1076  λdest_lbl: label.
     1077  λdef: rtl_internal_function.
     1078  match fresh_regs_strong def (|addr|) with
     1079  [ dp def_save_addr save_addr_prf ⇒
     1080    let def ≝ \fst def_save_addr in
     1081    let save_addr ≝ \snd def_save_addr in
     1082    match fresh_regs_strong def (|addr|) with
     1083    [ dp def_tmp_addr tmp_addr_prf ⇒
     1084      let def ≝ \fst def_tmp_addr in
     1085      let tmp_addr ≝ \snd def_tmp_addr in
     1086      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
     1087      let 〈def, tmpr〉 ≝ fresh_reg def in
     1088      let insts_save_addr ≝ translate_move save_addr addr in
     1089      let f ≝ λtranslates_off. λr.
     1090        let 〈translates, off〉 ≝ translates_off in
     1091        let translates ≝ translates @ [
     1092          adds_graph [
     1093            rtl_st_int tmpr off start_lbl
     1094          ];
     1095          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
     1096          adds_graph [
     1097            rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
     1098          ]
     1099        ]
     1100        in
     1101        let 〈carry, result〉 ≝ half_add ? off int_size in
     1102          〈translates, result〉
     1103      in
     1104      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
     1105        add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
     1106    ]
     1107  ].
     1108  [1: normalize //
     1109  |2: >save_addr_prf normalize
     1110      @(transitive_le 1 2 (|addr|)) //
     1111  |3: >tmp_addr_prf normalize
     1112      @(transitive_le 1 2 (|addr|)) //
     1113  |*: >tmp_addr_prf assumption
     1114  ]
     1115qed.
     1116
     1117definition translate_store ≝
     1118  λaddr.
     1119  λaddr_prf: 2 ≤ |addr|.
     1120  λsrcrs: list register.
     1121  λstart_lbl: label.
     1122  λdest_lbl: label.
     1123  λdef: rtl_internal_function.
     1124  match fresh_regs_strong def (|addr|) with
     1125  [ dp def_tmp_addr tmp_addr_prf ⇒
     1126    let def ≝ \fst def_tmp_addr in
     1127    let tmp_addr ≝ \snd def_tmp_addr in
     1128    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
     1129    let 〈def, tmpr〉 ≝ fresh_reg def in
     1130    let f ≝ λtranslate_off. λsrcr.
     1131      let 〈translates, off〉 ≝ translate_off in
     1132      let translates ≝ translates @ [
     1133        adds_graph [
     1134          rtl_st_int tmpr off start_lbl
     1135        ];
     1136        translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
     1137        adds_graph [
     1138          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
     1139        ]
     1140      ]
     1141      in
     1142        let 〈carry, result〉 ≝ half_add ? off int_size in
     1143          〈translates, result〉
     1144    in
     1145    let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
     1146      add_translates translates start_lbl dest_lbl def
     1147  ].
     1148  [1: normalize //
     1149  |2: >tmp_addr_prf normalize
     1150      @(transitive_le 1 2 (|addr|)) //
     1151  |3: >tmp_addr_prf normalize
     1152      @(transitive_le 1 2 (|addr|)) //
     1153  |*: >tmp_addr_prf assumption
     1154  ]
     1155qed.
     1156
     1157definition translate_stmt ≝
     1158  λlenv.
     1159  λlbl: label.
     1160  λstmt.
     1161  λdef: rtl_internal_function.
     1162  match stmt with
     1163  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
     1164  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
     1165  | St_const destr cst lbl' ⇒
     1166    translate_cst cst (find_local_env destr lenv) lbl lbl' def
     1167  | St_op1 op1 destr srcr lbl' ⇒
     1168    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
     1169  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
     1170    translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
     1171  | St_load ignore addr destr lbl' ⇒
     1172    translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
     1173  | St_store ignore addr srcr lbl' ⇒
     1174    translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
     1175  | St_call_id f args retr lbl' ⇒
     1176    match retr with
     1177    [ Some retr ⇒
     1178      add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
     1179    | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
     1180    ]
     1181  | St_call_ptr f args retr lbl' ⇒
     1182    match retr with
     1183    [ None ⇒
     1184      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
     1185        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
     1186    | Some retr ⇒
     1187      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
     1188        add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
     1189    ]
     1190  | St_tailcall_id f args ⇒
     1191    add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
     1192  | St_tailcall_ptr f args ⇒
     1193    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
     1194      add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
     1195  | St_cond r lbl_true lbl_false ⇒
     1196    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     1197  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
     1198  | St_return r ⇒
     1199    match r with
     1200    [ None ⇒ add_graph lbl (rtl_st_return [ ]) def
     1201    | Some r ⇒ add_graph lbl (rtl_st_return (find_local_env r lenv)) def
     1202    ]
    9751203  | _ ⇒ ?
    9761204  ].
    9771205
    978 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    979   match op2 with
    980 
    981     | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
    982       translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
    983         start_lbl dest_lbl def
    984 
    985     | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
    986       translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
    987         start_lbl dest_lbl def
    988 
    989     | AST.Op_cmp AST.Cmp_eq
    990     | AST.Op_cmpu AST.Cmp_eq
    991     | AST.Op_cmpp AST.Cmp_eq ->
    992       add_translates
    993         [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
    994          translate_op1 AST.Op_notbool destrs destrs]
    995         start_lbl dest_lbl def
    996 
    997     | AST.Op_cmp AST.Cmp_ne
    998     | AST.Op_cmpu AST.Cmp_ne
    999     | AST.Op_cmpp AST.Cmp_ne ->
    1000       translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1001 
    1002     | AST.Op_cmp AST.Cmp_lt ->
    1003       translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1004 
    1005     | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
    1006       translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1007 
    1008     | AST.Op_cmp AST.Cmp_le ->
    1009       add_translates
    1010         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    1011          translate_op1 AST.Op_notbool destrs destrs]
    1012         start_lbl dest_lbl def
    1013 
    1014     | AST.Op_cmpu AST.Cmp_le ->
    1015       add_translates
    1016         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    1017          translate_op1 AST.Op_notbool destrs destrs]
    1018         start_lbl dest_lbl def
    1019 
    1020     | AST.Op_cmpp AST.Cmp_le ->
    1021       add_translates
    1022         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
    1023          translate_op1 AST.Op_notbool destrs destrs]
    1024         start_lbl dest_lbl def
    1025 
    1026     | AST.Op_cmp AST.Cmp_gt ->
    1027       translate_op2 (AST.Op_cmp AST.Cmp_lt)
    1028         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    1029 
    1030     | AST.Op_cmpu AST.Cmp_gt ->
    1031       translate_op2 (AST.Op_cmpu AST.Cmp_lt)
    1032         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    1033 
    1034     | AST.Op_cmpp AST.Cmp_gt ->
    1035       translate_op2 (AST.Op_cmpp AST.Cmp_lt)
    1036         destrs srcrs2 srcrs1 start_lbl dest_lbl def
    1037 
    1038     | AST.Op_cmp AST.Cmp_ge ->
    1039       add_translates
    1040         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    1041          translate_op1 AST.Op_notbool destrs destrs]
    1042         start_lbl dest_lbl def
    1043 
    1044     | AST.Op_cmpu AST.Cmp_ge ->
    1045       add_translates
    1046         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    1047          translate_op1 AST.Op_notbool destrs destrs]
    1048         start_lbl dest_lbl def
    1049 
    1050     | AST.Op_cmpp AST.Cmp_ge ->
    1051       add_translates
    1052         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
    1053          translate_op1 AST.Op_notbool destrs destrs]
    1054         start_lbl dest_lbl def
    1055 
    1056     | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
    1057     | AST.Op_shr | AST.Op_shru ->
    1058       (* Unsupported, should have been replaced by a runtime function. *)
    1059       assert false
    1060 
     1206let translate_stmt lenv lbl stmt def = match stmt with
     1207
     1208  | RTLabs.St_skip lbl' ->
     1209    add_graph lbl (RTL.St_skip lbl') def
     1210
     1211  | RTLabs.St_cost (cost_lbl, lbl') ->
     1212    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
     1213
     1214  | RTLabs.St_cst (destr, cst, lbl') ->
     1215    translate_cst cst (find_local_env destr lenv) lbl lbl' def
     1216
     1217  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
     1218    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
     1219      lbl lbl' def
     1220
     1221  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     1222    translate_op2 op2 (find_local_env destr lenv)
     1223      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
     1224
     1225  | RTLabs.St_load (_, addr, destr, lbl') ->
     1226    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
     1227      lbl lbl' def
     1228
     1229  | RTLabs.St_store (_, addr, srcr, lbl') ->
     1230    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
     1231      lbl lbl' def
     1232
     1233  | RTLabs.St_call_id (f, args, None, _, lbl') ->
     1234    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
     1235
     1236  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
     1237    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
     1238                                   find_local_env retr lenv, lbl')) def
     1239
     1240  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
     1241    let (f1, f2) = find_and_addr f lenv in
     1242    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
     1243
     1244  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
     1245    let (f1, f2) = find_and_addr f lenv in
     1246    add_graph lbl
     1247      (RTL.St_call_ptr
     1248         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
     1249
     1250  | RTLabs.St_tailcall_id (f, args, _) ->
     1251    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
     1252
     1253  | RTLabs.St_tailcall_ptr (f, args, _) ->
     1254    let (f1, f2) = find_and_addr f lenv in
     1255    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
     1256
     1257  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
     1258    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     1259
     1260  | RTLabs.St_jumptable _ ->
     1261    error "Jump tables not supported yet."
     1262
     1263  | RTLabs.St_return None ->
     1264    add_graph lbl (RTL.St_return []) def
     1265
     1266  | RTLabs.St_return (Some r) ->
     1267    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    10611268
    10621269definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.