Changeset 2986
 Timestamp:
 Mar 27, 2013, 6:32:11 PM (5 years ago)
 Location:
 extracted
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/lINToASM.ml
r2979 r2986 1070 1070 Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) 1071 1071 1072 (** val store_bytes : 1073 BitVector.byte List.list > ASM.labelled_instruction List.list **) 1074 let store_bytes bytes = 1075 List.fold List.append List.Nil (fun by > Bool.True) (fun by > List.Cons 1076 ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV 1077 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = 1078 ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) }, (List.Cons 1079 ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOVX 1080 (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = 1081 ASM.ACC_A }))) }, (List.Cons ({ Types.fst = Types.None; Types.snd = 1082 (ASM.Instruction (ASM.INC ASM.DPTR)) }, List.Nil)))))) bytes 1072 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z; 1073 built : ASM.labelled_instruction List.list } 1074 1075 (** val init_mutable_rect_Type4 : 1076 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1077 > 'a1 **) 1078 let rec init_mutable_rect_Type4 h_mk_init_mutable x_30 = 1079 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1080 built0 } = x_30 1081 in 1082 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1083 1084 (** val init_mutable_rect_Type5 : 1085 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1086 > 'a1 **) 1087 let rec init_mutable_rect_Type5 h_mk_init_mutable x_32 = 1088 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1089 built0 } = x_32 1090 in 1091 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1092 1093 (** val init_mutable_rect_Type3 : 1094 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1095 > 'a1 **) 1096 let rec init_mutable_rect_Type3 h_mk_init_mutable x_34 = 1097 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1098 built0 } = x_34 1099 in 1100 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1101 1102 (** val init_mutable_rect_Type2 : 1103 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1104 > 'a1 **) 1105 let rec init_mutable_rect_Type2 h_mk_init_mutable x_36 = 1106 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1107 built0 } = x_36 1108 in 1109 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1110 1111 (** val init_mutable_rect_Type1 : 1112 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1113 > 'a1 **) 1114 let rec init_mutable_rect_Type1 h_mk_init_mutable x_38 = 1115 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1116 built0 } = x_38 1117 in 1118 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1119 1120 (** val init_mutable_rect_Type0 : 1121 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1122 > 'a1 **) 1123 let rec init_mutable_rect_Type0 h_mk_init_mutable x_40 = 1124 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1125 built0 } = x_40 1126 in 1127 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 1128 1129 (** val virtual_dptr : init_mutable > Z.z **) 1130 let rec virtual_dptr xxx = 1131 xxx.virtual_dptr 1132 1133 (** val actual_dptr : init_mutable > Z.z **) 1134 let rec actual_dptr xxx = 1135 xxx.actual_dptr 1136 1137 (** val built : init_mutable > ASM.labelled_instruction List.list **) 1138 let rec built xxx = 1139 xxx.built 1140 1141 (** val init_mutable_inv_rect_Type4 : 1142 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ 1143 > 'a1) > 'a1 **) 1144 let init_mutable_inv_rect_Type4 hterm h1 = 1145 let hcut = init_mutable_rect_Type4 h1 hterm in hcut __ 1146 1147 (** val init_mutable_inv_rect_Type3 : 1148 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ 1149 > 'a1) > 'a1 **) 1150 let init_mutable_inv_rect_Type3 hterm h1 = 1151 let hcut = init_mutable_rect_Type3 h1 hterm in hcut __ 1152 1153 (** val init_mutable_inv_rect_Type2 : 1154 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ 1155 > 'a1) > 'a1 **) 1156 let init_mutable_inv_rect_Type2 hterm h1 = 1157 let hcut = init_mutable_rect_Type2 h1 hterm in hcut __ 1158 1159 (** val init_mutable_inv_rect_Type1 : 1160 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ 1161 > 'a1) > 'a1 **) 1162 let init_mutable_inv_rect_Type1 hterm h1 = 1163 let hcut = init_mutable_rect_Type1 h1 hterm in hcut __ 1164 1165 (** val init_mutable_inv_rect_Type0 : 1166 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ 1167 > 'a1) > 'a1 **) 1168 let init_mutable_inv_rect_Type0 hterm h1 = 1169 let hcut = init_mutable_rect_Type0 h1 hterm in hcut __ 1170 1171 (** val init_mutable_discr : init_mutable > init_mutable > __ **) 1172 let init_mutable_discr x y = 1173 Logic.eq_rect_Type2 x 1174 (let { virtual_dptr = a0; actual_dptr = a1; built = a2 } = x in 1175 Obj.magic (fun _ dH > dH __ __ __)) y 1176 1177 (** val init_mutable_jmdiscr : init_mutable > init_mutable > __ **) 1178 let init_mutable_jmdiscr x y = 1179 Logic.eq_rect_Type2 x 1180 (let { virtual_dptr = a0; actual_dptr = a1; built = a2 } = x in 1181 Obj.magic (fun _ dH > dH __ __ __)) y 1182 1183 (** val store_byte : BitVector.byte > init_mutable > init_mutable **) 1184 let store_byte by mut = 1185 let { virtual_dptr = virt; actual_dptr = act; built = acc } = mut in 1186 let off = Z.zminus virt act in 1187 let pre = 1188 match Z.eqZb off Z.OZ with 1189  Bool.True > List.Nil 1190  Bool.False > 1191 (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with 1192  Bool.True > 1193 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1194 (ASM.INC ASM.DPTR)) }, List.Nil) 1195  Bool.False > 1196 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1197 (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; 1198 Types.snd = (ASM.DATA16 1199 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1200 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1201 (Nat.S (Nat.S Nat.O)))))))))))))))) virt)) }))))) }, List.Nil)) 1202 in 1203 { virtual_dptr = (Z.zsucc virt); actual_dptr = virt; built = 1204 (List.append pre (List.Cons ({ Types.fst = Types.None; Types.snd = 1205 (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl 1206 (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) }, 1207 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1208 (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = 1209 ASM.ACC_A }))) }, List.Nil))))) } 1083 1210 1084 1211 (** val do_store_init_data : 1085 AST.ident List.list > aSM_universe > Z.z > AST.init_data>1086 ASM.labelled_instruction List.list**)1087 let do_store_init_data globals u nxt_dptr= function1088  AST.Init_int8 n > store_byte s (List.Cons (n, List.Nil))1212 AST.ident List.list > aSM_universe > AST.init_data > init_mutable > 1213 init_mutable **) 1214 let do_store_init_data globals u = function 1215  AST.Init_int8 n > store_byte n 1089 1216  AST.Init_int16 n > 1090 1217 let { Types.fst = by0; Types.snd = by1 } = … … 1093 1220 Nat.O)))))))) n 1094 1221 in 1095 store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))1222 Relations.compose (store_byte by1) (store_byte by0) 1096 1223  AST.Init_int32 n > 1097 1224 let { Types.fst = by0; Types.snd = n0 } = … … 1113 1240 Nat.O)))))))) n1 1114 1241 in 1115 store_bytes (List.Cons (by0, (List.Cons (by1, (List.Cons (by2, (List.Cons 1116 (by3, List.Nil)))))))) 1242 Relations.compose 1243 (Relations.compose (Relations.compose (store_byte by3) (store_byte by2)) 1244 (store_byte by1)) (store_byte by0) 1117 1245  AST.Init_space n > 1118 (match n with 1119  Nat.O > List.Nil 1120  Nat.S k > 1121 (match k with 1122  Nat.O > 1123 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1124 (ASM.INC ASM.DPTR)) }, List.Nil) 1125  Nat.S x > 1126 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1127 (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; 1128 Types.snd = (ASM.DATA16 1129 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1130 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1131 (Nat.S (Nat.S Nat.O)))))))))))))))) nxt_dptr)) }))))) }, 1132 List.Nil))) 1246 (fun mut > { virtual_dptr = (Z.zplus (Z.z_of_nat n) mut.virtual_dptr); 1247 actual_dptr = mut.actual_dptr; built = mut.built }) 1133 1248  AST.Init_null > 1134 store_bytes (List.Cons1135 ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S1136 Nat.O))))))))), (List.Cons1137 ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S1138 Nat.O))))))))), List.Nil))))1249 let z = 1250 BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1251 Nat.O)))))))) 1252 in 1253 Relations.compose (store_byte z) (store_byte z) 1139 1254  AST.Init_addrof (symb, ofs) > 1140 1255 let addr = … … 1158 1273 Nat.O)))))))) addr 1159 1274 in 1160 store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))1275 Relations.compose (store_byte by1) (store_byte by0) 1161 1276 1162 1277 (** val do_store_init_data_list : … … 1164 1279 ASM.labelled_instruction List.list **) 1165 1280 let do_store_init_data_list globals u start_dptr data = 1166 let f = fun data0 dptr_acc > 1167 let { Types.fst = dptr; Types.snd = acc } = dptr_acc in 1168 let nxt_dptr = 1169 Z.zplus dptr (Z.z_of_nat (Globalenvs.size_init_data data0)) 1170 in 1171 { Types.fst = nxt_dptr; Types.snd = 1172 (List.append (do_store_init_data globals u nxt_dptr data0) acc) } 1173 in 1174 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV 1175 (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd = 1176 (ASM.DATA16 1177 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1178 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1179 Nat.O)))))))))))))))) start_dptr)) }))))) }, 1180 (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd) 1181 1182 (** val translate_initialization : 1183 LIN.lin_program > ASM.labelled_instruction List.list 1281 let init = { virtual_dptr = start_dptr; actual_dptr = Z.OZ; built = 1282 List.Nil } 1283 in 1284 (List.foldr (do_store_init_data globals u) init data).built 1285 1286 (** val translate_premain : 1287 LIN.lin_program > ASM.identifier > ASM.labelled_instruction List.list 1184 1288 Monad.smax_def__o__monad **) 1185 let translate_initialization p = 1186 Obj.magic (fun u > 1187 let start_sp = 1188 Z.zopp 1189 (Z.z_of_nat 1190 (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)) 1191 in 1192 let { Types.fst = sph; Types.snd = spl } = 1193 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1194 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1195 Nat.O)))))))) 1196 (BitVectorZ.bitvector_of_Z 1197 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1198 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1199 (Nat.S Nat.O))))))))) start_sp) 1200 in 1201 let data = 1202 List.flatten 1203 (List.map (fun x > x.Types.snd) p.Joint.joint_prog.AST.prog_vars) 1204 in 1205 let init_isp = ASM.DATA 1206 (Vector.append (Nat.S (Nat.S Nat.O)) 1207 (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1208 Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O))) 1209 (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1210 Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1211 (Nat.O, Bool.False, Vector.VEmpty)))) 1212 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) 1213 in 1214 let isp_direct = ASM.DIRECT 1215 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1216 Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S 1217 (Nat.S (Nat.S Nat.O)))))), Bool.True, 1218 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1219 Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))) 1220 in 1221 let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1222 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1223 (Nat.O, Bool.False, Vector.VEmpty)))))) 1224 in 1225 let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1226 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1227 (Nat.O, Bool.True, Vector.VEmpty)))))) 1228 in 1229 { Types.fst = u; Types.snd = 1230 (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Cost 1231 p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = Types.None; 1232 Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl 1233 (Types.Inr { Types.fst = isp_direct; Types.snd = init_isp })))))) }, 1234 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1235 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr 1236 { Types.fst = reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, 1237 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1238 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr 1239 { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) }, 1240 List.Nil)))))))) 1241 (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog) u 1242 start_sp data)) }) 1289 let translate_premain p exit_label = 1290 Monad.m_bind0 (Monad.smax_def State.state_monad) 1291 (identifier_of_ident (AST.prog_var_names p.Joint.joint_prog) 1292 p.Joint.joint_prog.AST.prog_main) (fun main > 1293 Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get 1294 (fun u > 1295 let start_sp = 1296 Z.zopp 1297 (Z.z_of_nat 1298 (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)) 1299 in 1300 let { Types.fst = sph; Types.snd = spl } = 1301 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1302 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1303 (Nat.S Nat.O)))))))) 1304 (BitVectorZ.bitvector_of_Z 1305 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1306 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1307 (Nat.S Nat.O))))))))) start_sp) 1308 in 1309 let data = 1310 List.flatten 1311 (List.map (fun x > x.Types.snd) p.Joint.joint_prog.AST.prog_vars) 1312 in 1313 let init_isp = ASM.DATA 1314 (Vector.append (Nat.S (Nat.S Nat.O)) 1315 (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1316 Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O))) 1317 (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1318 Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1319 (Nat.O, Bool.False, Vector.VEmpty)))) 1320 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) 1321 in 1322 let isp_direct = ASM.DIRECT 1323 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1324 Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S 1325 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, 1326 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1327 Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))) 1328 in 1329 let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1330 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1331 (Nat.O, Bool.False, Vector.VEmpty)))))) 1332 in 1333 let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1334 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1335 (Nat.O, Bool.True, Vector.VEmpty)))))) 1336 in 1337 Monad.m_return0 (Monad.smax_def State.state_monad) 1338 (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = 1339 (ASM.Cost p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = 1340 Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl 1341 (Types.Inl (Types.Inl (Types.Inr { Types.fst = isp_direct; 1342 Types.snd = init_isp })))))) }, (List.Cons ({ Types.fst = 1343 Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl 1344 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_spl; 1345 Types.snd = (ASM.DATA spl) }))))))) }, (List.Cons ({ Types.fst = 1346 Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl 1347 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_sph; 1348 Types.snd = (ASM.DATA sph) }))))))) }, List.Nil)))))))) 1349 (List.append 1350 (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog) 1351 u start_sp data) (List.Cons ({ Types.fst = Types.None; 1352 Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst = 1353 (Types.Some exit_label); Types.snd = (ASM.Cost 1354 u.fresh_cost_label) }, (List.Cons ({ Types.fst = Types.None; 1355 Types.snd = (ASM.Jmp exit_label) }, List.Nil)))))))))) 1243 1356 1244 1357 (** val get_symboltable : … … 1268 1381 in 1269 1382 Monad.m_bind0 (Monad.smax_def State.state_monad) 1270 ( Util.foldl add_translation1271 ( Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)1272 p.Joint.joint_prog.AST.prog_funct) (fun code>1383 (aSM_fresh 1384 (List.map (fun x > x.Types.fst.Types.fst) 1385 p.Joint.joint_prog.AST.prog_vars)) (fun exit_label > 1273 1386 Monad.m_bind0 (Monad.smax_def State.state_monad) 1274 (aSM_fresh (AST.prog_var_names p.Joint.joint_prog)) 1275 (fun exit_label > 1387 (Util.foldl add_translation 1388 (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) 1389 p.Joint.joint_prog.AST.prog_funct) (fun code > 1276 1390 Monad.m_bind0 (Monad.smax_def State.state_monad) 1277 ( identifier_of_ident (AST.prog_var_names p.Joint.joint_prog)1278 p.Joint.joint_prog.AST.prog_main) (fun main>1391 (get_symboltable (AST.prog_var_names p.Joint.joint_prog)) 1392 (fun symboltable > 1279 1393 Monad.m_bind0 (Monad.smax_def State.state_monad) 1280 (get_symboltable (AST.prog_var_names p.Joint.joint_prog)) 1281 (fun symboltable > 1282 Monad.m_bind0 (Monad.smax_def State.state_monad) 1283 (translate_initialization p) (fun init > 1284 Monad.m_bind0 (Monad.smax_def State.state_monad) 1285 State.state_get (fun u > 1286 Monad.m_return0 (Monad.smax_def State.state_monad) 1287 (let code0 = 1288 List.append init (List.Cons ({ Types.fst = Types.None; 1289 Types.snd = (ASM.Call main) }, (List.Cons 1290 ({ Types.fst = (Types.Some exit_label); Types.snd = 1291 (ASM.Cost u.fresh_cost_label) }, (List.Cons 1292 ({ Types.fst = Types.None; Types.snd = (ASM.Jmp 1293 exit_label) }, code)))))) 1294 in 1295 Monad.m_bind0 (Monad.max_def Option.option) 1296 (Obj.magic (ASM.code_size_opt code0)) (fun _ > 1297 Monad.m_return0 (Monad.max_def Option.option) 1298 { ASM.preamble = List.Nil; ASM.code = code0; 1299 ASM.renamed_symbols = symboltable; ASM.final_label = 1300 exit_label }))))))))) 1301 1394 (translate_premain p exit_label) (fun init > 1395 Monad.m_return0 (Monad.smax_def State.state_monad) 1396 (let code0 = List.append init code in 1397 Monad.m_bind0 (Monad.max_def Option.option) 1398 (Obj.magic (ASM.code_size_opt code0)) (fun _ > 1399 Monad.m_return0 (Monad.max_def Option.option) 1400 { ASM.preamble = List.Nil; ASM.code = code0; 1401 ASM.renamed_symbols = symboltable; ASM.final_label = 1402 exit_label }))))))) 1403 
extracted/lINToASM.mli
r2979 r2986 275 275 AST.ident List.list > (AST.ident, Joint.joint_function) Types.prod > __ 276 276 277 val store_bytes : 278 BitVector.byte List.list > ASM.labelled_instruction List.list 277 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z; 278 built : ASM.labelled_instruction List.list } 279 280 val init_mutable_rect_Type4 : 281 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 282 > 'a1 283 284 val init_mutable_rect_Type5 : 285 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 286 > 'a1 287 288 val init_mutable_rect_Type3 : 289 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 290 > 'a1 291 292 val init_mutable_rect_Type2 : 293 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 294 > 'a1 295 296 val init_mutable_rect_Type1 : 297 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 298 > 'a1 299 300 val init_mutable_rect_Type0 : 301 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 302 > 'a1 303 304 val virtual_dptr : init_mutable > Z.z 305 306 val actual_dptr : init_mutable > Z.z 307 308 val built : init_mutable > ASM.labelled_instruction List.list 309 310 val init_mutable_inv_rect_Type4 : 311 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ > 312 'a1) > 'a1 313 314 val init_mutable_inv_rect_Type3 : 315 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ > 316 'a1) > 'a1 317 318 val init_mutable_inv_rect_Type2 : 319 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ > 320 'a1) > 'a1 321 322 val init_mutable_inv_rect_Type1 : 323 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ > 324 'a1) > 'a1 325 326 val init_mutable_inv_rect_Type0 : 327 init_mutable > (Z.z > Z.z > ASM.labelled_instruction List.list > __ > 328 'a1) > 'a1 329 330 val init_mutable_discr : init_mutable > init_mutable > __ 331 332 val init_mutable_jmdiscr : init_mutable > init_mutable > __ 333 334 val store_byte : BitVector.byte > init_mutable > init_mutable 279 335 280 336 val do_store_init_data : 281 AST.ident List.list > aSM_universe > Z.z > AST.init_data>282 ASM.labelled_instruction List.list337 AST.ident List.list > aSM_universe > AST.init_data > init_mutable > 338 init_mutable 283 339 284 340 val do_store_init_data_list : … … 286 342 ASM.labelled_instruction List.list 287 343 288 val translate_ initialization :289 LIN.lin_program > ASM. labelled_instruction List.list344 val translate_premain : 345 LIN.lin_program > ASM.identifier > ASM.labelled_instruction List.list 290 346 Monad.smax_def__o__monad 291 347
Note: See TracChangeset
for help on using the changeset viewer.