Changeset 2951 for extracted/lINToASM.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/lINToASM.ml
r2890 r2951 82 82 83 83 open ASM 84 85 open Extra_bool 86 87 open Coqlib 88 89 open Values 90 91 open FrontEndVal 92 93 open GenMem 94 95 open FrontEndMem 96 97 open Globalenvs 84 98 85 99 open Sets … … 127 141 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 128 142 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 129 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_2 4583=143 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_2395 = 130 144 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 131 ident_map0; label_map = label_map0; address_map = address_map0 } = 132 x_24583 145 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2395 133 146 in 134 147 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 140 153 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 141 154 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 142 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_2 4585=155 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_2397 = 143 156 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 144 ident_map0; label_map = label_map0; address_map = address_map0 } = 145 x_24585 157 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2397 146 158 in 147 159 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 153 165 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 154 166 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 155 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_2 4587=167 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_2399 = 156 168 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 157 ident_map0; label_map = label_map0; address_map = address_map0 } = 158 x_24587 169 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2399 159 170 in 160 171 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 166 177 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 167 178 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 168 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24 589=179 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_2401 = 169 180 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 170 ident_map0; label_map = label_map0; address_map = address_map0 } = 171 x_24589 181 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2401 172 182 in 173 183 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 179 189 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 180 190 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 181 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24 591=191 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_2403 = 182 192 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 183 ident_map0; label_map = label_map0; address_map = address_map0 } = 184 x_24591 193 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2403 185 194 in 186 195 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 192 201 Identifiers.identifier_map Identifiers.identifier_map > BitVector.word 193 202 Identifiers.identifier_map > __ > 'a1) > aSM_universe > 'a1 **) 194 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24 593=203 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_2405 = 195 204 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 196 ident_map0; label_map = label_map0; address_map = address_map0 } = 197 x_24593 205 ident_map0; label_map = label_map0; address_map = address_map0 } = x_2405 198 206 in 199 207 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 280 288 let globals_addr_internal = fun res_offset x_size > 281 289 let { Types.fst = res; Types.snd = offset } = res_offset in 282 let { Types.fst = eta2 9086; Types.snd = size} = x_size in283 let { Types.fst = x; Types.snd = region } = eta2 9086in290 let { Types.fst = eta24644; Types.snd = data } = x_size in 291 let { Types.fst = x; Types.snd = region } = eta24644 in 284 292 { Types.fst = 285 293 (Identifiers.add PreIdentifiers.SymbolTag res x … … 287 295 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 288 296 Nat.O)))))))))))))))) offset)); Types.snd = 289 (Z.zplus offset (Z.z_of_nat size)) }297 (Z.zplus offset (Z.z_of_nat (Globalenvs.size_init_data_list data))) } 290 298 in 291 299 let addresses = 292 300 Util.foldl globals_addr_internal { Types.fst = 293 (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd = Z.OZ } 294 p.AST.prog_vars 301 (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd = 302 (Z.zopp 303 (Z.z_of_nat 304 (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))) } 305 p.Joint.joint_prog.AST.prog_vars 295 306 in 296 307 { id_univ = Positive.One; current_funct = Positive.One; ident_map = … … 309 320 (Identifiers.empty_map PreIdentifiers.LabelTag) 310 321 in 311 let { Types.fst = eta2 9087; Types.snd = lmap0 } =322 let { Types.fst = eta24645; Types.snd = lmap0 } = 312 323 match Identifiers.lookup PreIdentifiers.LabelTag lmap l with 313 324  Types.None > … … 321 332 lmap } 322 333 in 323 let { Types.fst = id; Types.snd = univ } = eta2 9087in334 let { Types.fst = id; Types.snd = univ } = eta24645 in 324 335 { Types.fst = { id_univ = univ; current_funct = current; ident_map = 325 336 u.ident_map; label_map = … … 333 344 Obj.magic (fun u > 334 345 let imap = u.ident_map in 335 let { Types.fst = eta2 9088; Types.snd = imap0 } =346 let { Types.fst = eta24646; Types.snd = imap0 } = 336 347 match Identifiers.lookup PreIdentifiers.SymbolTag imap i with 337 348  Types.None > … … 345 356 imap } 346 357 in 347 let { Types.fst = id; Types.snd = univ } = eta2 9088in358 let { Types.fst = id; Types.snd = univ } = eta24646 in 348 359 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 349 360 ident_map = imap0; label_map = u.label_map; address_map = … … 1023 1034 Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) 1024 1035 1036 (** val store_bytes : 1037 BitVector.byte List.list > ASM.labelled_instruction List.list **) 1038 let store_bytes bytes = 1039 List.fold List.append List.Nil (fun by > Bool.True) (fun by > List.Cons 1040 ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV 1041 (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = 1042 ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) }, (List.Cons 1043 ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOVX 1044 (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = 1045 ASM.ACC_A }))) }, (List.Cons ({ Types.fst = Types.None; Types.snd = 1046 (ASM.Instruction (ASM.INC ASM.DPTR)) }, List.Nil)))))) bytes 1047 1048 (** val do_store_init_data : 1049 AST.ident List.list > aSM_universe > Z.z > AST.init_data > 1050 ASM.labelled_instruction List.list **) 1051 let do_store_init_data globals u nxt_dptr = function 1052  AST.Init_int8 n > store_bytes (List.Cons (n, List.Nil)) 1053  AST.Init_int16 n > 1054 let { Types.fst = by0; Types.snd = by1 } = 1055 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1056 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1057 Nat.O)))))))) n 1058 in 1059 store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil)))) 1060  AST.Init_int32 n > 1061 let { Types.fst = by0; Types.snd = n0 } = 1062 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1063 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1064 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1065 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))) 1066 n 1067 in 1068 let { Types.fst = by1; Types.snd = n1 } = 1069 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1070 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1071 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1072 Nat.O)))))))))))))))) n0 1073 in 1074 let { Types.fst = by2; Types.snd = by3 } = 1075 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1076 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1077 Nat.O)))))))) n1 1078 in 1079 store_bytes (List.Cons (by0, (List.Cons (by1, (List.Cons (by2, (List.Cons 1080 (by3, List.Nil)))))))) 1081  AST.Init_space n > 1082 (match n with 1083  Nat.O > List.Nil 1084  Nat.S k > 1085 (match k with 1086  Nat.O > 1087 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1088 (ASM.INC ASM.DPTR)) }, List.Nil) 1089  Nat.S x > 1090 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1091 (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; 1092 Types.snd = (ASM.DATA16 1093 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1094 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1095 (Nat.S (Nat.S Nat.O)))))))))))))))) nxt_dptr)) }))))) }, 1096 List.Nil))) 1097  AST.Init_null > 1098 store_bytes (List.Cons 1099 ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1100 Nat.O))))))))), (List.Cons 1101 ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1102 Nat.O))))))))), List.Nil)))) 1103  AST.Init_addrof (symb, ofs) > 1104 let addr = 1105 match Identifiers.lookup PreIdentifiers.SymbolTag u.address_map symb with 1106  Types.None > 1107 BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1108 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1109 Nat.O)))))))))))))))) 1110  Types.Some x > 1111 BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1112 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1113 Nat.O)))))))))))))))) 1114 (Z.zplus 1115 (BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S 1116 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1117 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) x) (Z.z_of_nat ofs)) 1118 in 1119 let { Types.fst = by1; Types.snd = by0 } = 1120 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1121 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1122 Nat.O)))))))) addr 1123 in 1124 store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil)))) 1125 1126 (** val do_store_init_data_list : 1127 AST.ident List.list > aSM_universe > Z.z > AST.init_data List.list > 1128 ASM.labelled_instruction List.list **) 1129 let do_store_init_data_list globals u start_dptr data = 1130 let f = fun data0 dptr_acc > 1131 let { Types.fst = dptr; Types.snd = acc } = dptr_acc in 1132 let nxt_dptr = 1133 Z.zplus dptr (Z.z_of_nat (Globalenvs.size_init_data data0)) 1134 in 1135 { Types.fst = nxt_dptr; Types.snd = 1136 (List.append (do_store_init_data globals u nxt_dptr data0) acc) } 1137 in 1138 (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd 1139 1140 (** val translate_initialization : 1141 LIN.lin_program > ASM.labelled_instruction List.list 1142 Monad.smax_def__o__monad **) 1143 let translate_initialization p = 1144 Obj.magic (fun u > 1145 let start_sp = 1146 Z.zopp 1147 (Z.z_of_nat 1148 (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)) 1149 in 1150 let { Types.fst = sph; Types.snd = spl } = 1151 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1152 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1153 Nat.O)))))))) 1154 (BitVectorZ.bitvector_of_Z 1155 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1156 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1157 (Nat.S Nat.O))))))))) start_sp) 1158 in 1159 let data = 1160 List.flatten 1161 (List.map (fun x > x.Types.snd) p.Joint.joint_prog.AST.prog_vars) 1162 in 1163 let init_isp = ASM.DATA 1164 (Vector.append (Nat.S (Nat.S Nat.O)) 1165 (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1166 Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O))) 1167 (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S 1168 Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1169 (Nat.O, Bool.False, Vector.VEmpty)))) 1170 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) 1171 in 1172 let isp_direct = ASM.DIRECT 1173 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1174 Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S 1175 (Nat.S (Nat.S Nat.O)))))), Bool.True, 1176 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1177 Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))) 1178 in 1179 let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1180 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1181 (Nat.O, Bool.False, Vector.VEmpty)))))) 1182 in 1183 let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 1184 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons 1185 (Nat.O, Bool.True, Vector.VEmpty)))))) 1186 in 1187 { Types.fst = u; Types.snd = 1188 (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Cost 1189 p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = Types.None; 1190 Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl 1191 (Types.Inr { Types.fst = isp_direct; Types.snd = init_isp })))))) }, 1192 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1193 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr 1194 { Types.fst = reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, 1195 (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction 1196 (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr 1197 { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) }, 1198 List.Nil)))))))) 1199 (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog) u 1200 start_sp data)) }) 1201 1025 1202 (** val get_symboltable : 1026 1203 AST.ident List.list > (ASM.identifier, AST.ident) Types.prod List.list … … 1042 1219 Monad.m_bind0 (Monad.smax_def State.state_monad) 1043 1220 (translate_fun_def 1044 (List.map (fun x > x.Types.fst.Types.fst) p.AST.prog_vars)1045 id_def) (fun code >1221 (List.map (fun x > x.Types.fst.Types.fst) 1222 p.Joint.joint_prog.AST.prog_vars) id_def) (fun code > 1046 1223 Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 > 1047 1224 Monad.m_return0 (Monad.smax_def State.state_monad) … … 1051 1228 (Util.foldl add_translation 1052 1229 (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) 1053 p. AST.prog_funct) (fun code >1230 p.Joint.joint_prog.AST.prog_funct) (fun code > 1054 1231 Monad.m_bind0 (Monad.smax_def State.state_monad) 1055 (aSM_fresh 1056 (List.map (fun x > x.Types.fst.Types.fst) p.AST.prog_vars)) 1232 (aSM_fresh (AST.prog_var_names p.Joint.joint_prog)) 1057 1233 (fun exit_label > 1058 1234 Monad.m_bind0 (Monad.smax_def State.state_monad) 1059 (identifier_of_ident 1060 (List.map (fun x > x.Types.fst.Types.fst) p.AST.prog_vars) 1061 p.AST.prog_main) (fun main > 1235 (identifier_of_ident (AST.prog_var_names p.Joint.joint_prog) 1236 p.Joint.joint_prog.AST.prog_main) (fun main > 1062 1237 Monad.m_bind0 (Monad.smax_def State.state_monad) 1063 (get_symboltable 1064 (List.map (fun x > x.Types.fst.Types.fst) p.AST.prog_vars)) 1238 (get_symboltable (AST.prog_var_names p.Joint.joint_prog)) 1065 1239 (fun symboltable > 1066 Monad.m_return0 (Monad.smax_def State.state_monad) 1067 (let code0 = List.Cons ({ Types.fst = Types.None; Types.snd = 1068 (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some 1069 exit_label); Types.snd = (ASM.Jmp exit_label) }, code))) 1070 in 1071 Monad.m_bind0 (Monad.max_def Option.option) 1072 (Obj.magic (ASM.code_size_opt code0)) (fun _ > 1073 Monad.m_return0 (Monad.max_def Option.option) 1074 { ASM.preamble = List.Nil; ASM.code = code0; 1075 ASM.renamed_symbols = symboltable; ASM.final_label = 1076 exit_label }))))))) 1077 1240 Monad.m_bind0 (Monad.smax_def State.state_monad) 1241 (translate_initialization p) (fun init > 1242 Monad.m_return0 (Monad.smax_def State.state_monad) 1243 (let code0 = 1244 List.append init (List.Cons ({ Types.fst = Types.None; 1245 Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst = 1246 (Types.Some exit_label); Types.snd = (ASM.Jmp 1247 exit_label) }, code)))) 1248 in 1249 Monad.m_bind0 (Monad.max_def Option.option) 1250 (Obj.magic (ASM.code_size_opt code0)) (fun _ > 1251 Monad.m_return0 (Monad.max_def Option.option) 1252 { ASM.preamble = List.Nil; ASM.code = code0; 1253 ASM.renamed_symbols = symboltable; ASM.final_label = 1254 exit_label })))))))) 1255
Note: See TracChangeset
for help on using the changeset viewer.