Changeset 1046
 Timestamp:
 Jun 29, 2011, 12:15:09 PM (10 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1045 r1046 1092 1092 λdef. 1093 1093 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 1136 definition 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 1148 definition 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 1172 definition 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 1189 definition 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 1202 let 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 37 37  St_skip : label → statement 38 38  St_cost : costlabel → label → statement 39  St_const : register → c onstant → label → statement39  St_const : register → cast → label → statement 40 40  St_op1 : unary_operation → register → register → label → statement 41 41  St_op2 : binary_operation → register → register → register → label → statement 
src/common/AST.ma
r1045 r1046 42 42 43 43 definition Immediate ≝ nat. (* XXX is this the best place to put this? *) 44 45 inductive quantity: Type[0] ≝ 46  q_int: Byte → quantity 47  q_offset: quantity 48  q_ptr: quantity. 49 50 inductive 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 56 inductive 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 *) 44 63 45 64 (* Memory spaces *)
Note: See TracChangeset
for help on using the changeset viewer.