Changeset 1046


Ignore:
Timestamp:
Jun 29, 2011, 12:15:09 PM (8 years ago)
Author:
mulligan
Message:

syntax of rtlabs was wrong: cast not const. more added to rtlabs --> rtl pass

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1045 r1046  
    10921092  λdef.
    10931093  match q with
    1094   [
    1095   ].
    1096 
    1097 let 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
    1112       let (def, tmpr) = fresh_reg def in
    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."
     1094  [ q_int b ⇒
     1095    if eq_bv ? b (bitvector_of_nat ? 1) then
     1096      match extract_singleton ? destrs with
     1097      [ None ⇒ None ? (* error: size error in load *)
     1098      | Some destr ⇒
     1099        let 〈def, addr1〉 ≝ fresh_reg def in
     1100        let 〈def, addr2〉 ≝ fresh_reg def in
     1101          Some ? (add_translates [
     1102            addressing_pointer mode args addr1 addr2;
     1103            adds_graph [
     1104              rtl_st_load destr addr1 addr2 start_lbl
     1105            ]
     1106          ] start_lbl dest_lbl def)
     1107      ]
     1108    else
     1109      None ? (* error: size error in load *)
     1110  | q_ptr ⇒
     1111    match extract_pair ? destrs with
     1112    [ None ⇒ None ? (* error: size error in load *)
     1113    | Some destr12 ⇒
     1114      let 〈destr1, destr2〉 ≝ destr12 in
     1115      let 〈def, addr1〉 ≝ fresh_reg def in
     1116      let 〈def, addr2〉 ≝ fresh_reg def in
     1117      let addr ≝ [ addr1; addr2 ] in
     1118      let 〈def, tmpr〉 ≝ fresh_reg def in
     1119        Some ? (
     1120          add_translates [
     1121            addressing_pointer mode args addr1 addr2;
     1122            adds_graph [
     1123              rtl_st_load destr1 addr1 addr2 start_lbl;
     1124              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
     1125            ];
     1126            translate_op2 op_addp addr addr [ tmpr ];
     1127            adds_graph [
     1128              rtl_st_load destr2 addr1 addr2 start_lbl
     1129            ]
     1130          ] start_lbl dest_lbl def
     1131        )
     1132    ]
     1133  | _ ⇒ None ? (* error: size error in load *)
     1134  ].
     1135 
     1136definition make_addr ≝
     1137  λA: Type[0].
     1138  λlst: list A.
     1139  match lst with
     1140  [ cons hd tl ⇒
     1141    match tl with
     1142    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
     1143    | _ ⇒ None ? (* do not use on these arguments *)
     1144    ]
     1145  | _ ⇒ None ? (* do not use on these arguments *)
     1146  ].
     1147 
     1148definition translate_store_internal ≝
     1149  λaddr.
     1150  λtmp_addr.
     1151  λtmpr.
     1152  λstart_lbl.
     1153  λdest_lbl.
     1154  λtmp_addr1.
     1155  λtmp_addr2.
     1156  λtranslates_off.
     1157  λsrcr.
     1158    let 〈translates, off〉 ≝ translates_off in
     1159    let translates ≝ translates @
     1160      [ adds_graph [
     1161          rtl_st_int tmpr off start_lbl
     1162        ];
     1163        translate_op2 op_addp tmp_addr addr [ tmpr ];
     1164        adds_graph [
     1165          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
     1166        ]
     1167      ]
     1168    in
     1169    let 〈ignore, result〉 ≝ half_add ? off int_size in
     1170      〈translates, result〉.
     1171 
     1172definition translate_store ≝
     1173  λaddr.
     1174  λsrcrs.
     1175  λstart_lbl.
     1176  λdest_lbl.
     1177  λdef.
     1178    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
     1179    match make_addr ? tmp_addr with
     1180    [ None ⇒ None ?
     1181    | Some tmp_addr12 ⇒
     1182      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
     1183      let 〈def, tmpr〉 ≝ fresh_reg def in
     1184      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
     1185      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
     1186        add_translates translates start_lbl dest_lbl def
     1187    ].
     1188
     1189definition translate_stmt ≝
     1190  λlenv.
     1191  λlbl.
     1192  λstmt.
     1193  λdef.
     1194  match stmt with
     1195  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
     1196  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
     1197  | St_cast destr cst lbl' ⇒
     1198      translate_cst cst (find_local_env destr lenv) lbl lbl' def
     1199  | _ ⇒ ?
     1200  ].
     1201
     1202let translate_stmt lenv lbl stmt def = match stmt with
     1203
     1204  | RTLabs.St_skip lbl' ->
     1205    add_graph lbl (RTL.St_skip lbl') def
     1206
     1207  | RTLabs.St_cost (cost_lbl, lbl') ->
     1208    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
     1209
     1210  | RTLabs.St_cst (destr, cst, lbl') ->
     1211    translate_cst cst (find_local_env destr lenv) lbl lbl' def
     1212
     1213  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
     1214    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
     1215      lbl lbl' def
     1216
     1217  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     1218    translate_op2 op2 (find_local_env destr lenv)
     1219      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
     1220
     1221  | RTLabs.St_load (_, addr, destr, lbl') ->
     1222    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
     1223      lbl lbl' def
     1224
     1225  | RTLabs.St_store (_, addr, srcr, lbl') ->
     1226    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
     1227      lbl lbl' def
     1228
     1229  | RTLabs.St_call_id (f, args, None, _, lbl') ->
     1230    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
     1231
     1232  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
     1233    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
     1234                                   find_local_env retr lenv, lbl')) def
     1235
     1236  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
     1237    let (f1, f2) = find_and_addr f lenv in
     1238    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
     1239
     1240  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
     1241    let (f1, f2) = find_and_addr f lenv in
     1242    add_graph lbl
     1243      (RTL.St_call_ptr
     1244         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
     1245
     1246  | RTLabs.St_tailcall_id (f, args, _) ->
     1247    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
     1248
     1249  | RTLabs.St_tailcall_ptr (f, args, _) ->
     1250    let (f1, f2) = find_and_addr f lenv in
     1251    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
     1252
     1253  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
     1254    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     1255
     1256  | RTLabs.St_jumptable _ ->
     1257    error "Jump tables not supported yet."
     1258
     1259  | RTLabs.St_return None ->
     1260    add_graph lbl (RTL.St_return []) def
     1261
     1262  | RTLabs.St_return (Some r) ->
     1263    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
  • src/RTLabs/syntax.ma

    r1045 r1046  
    3737| St_skip : label → statement
    3838| St_cost : costlabel → label → statement
    39 | St_const : register → constant → label → statement
     39| St_const : register → cast → label → statement
    4040| St_op1 : unary_operation → register → register → label → statement
    4141| St_op2 : binary_operation → register → register → register → label → statement
  • src/common/AST.ma

    r1045 r1046  
    4242
    4343definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
     44
     45inductive quantity: Type[0] ≝
     46  | q_int: Byte → quantity
     47  | q_offset: quantity
     48  | q_ptr: quantity.
     49 
     50inductive abstract_size: Type[0] ≝
     51  | size_q: quantity → abstract_size
     52  | size_prod: list abstract_size → abstract_size
     53  | size_sum: list abstract_size → abstract_size
     54  | size_array: nat → abstract_size → abstract_size.
     55
     56inductive cast: Type[0] ≝
     57  | cast_int: Byte → cast                     (* integer constant *)
     58(*  | cast_float: float → cast                (* float constant *) *)
     59  | cast_addrsymbol of identifier → cast      (* address of a global symbol *)
     60  | cast_stack: cast                          (* address of the stack *)
     61  | cast_offset: abstract_offset → cast       (* offset *)
     62  | cast_sizeof: abstract_size → cast.        (* size of a type *)
    4463
    4564(* Memory spaces *)
Note: See TracChangeset for help on using the changeset viewer.