Changeset 2986 for extracted/lINToASM.ml


Ignore:
Timestamp:
Mar 27, 2013, 6:32:11 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • extracted/lINToASM.ml

    r2979 r2986  
    10701070      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
    10711071
    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
     1072type 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 **)
     1078let 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 **)
     1087let 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 **)
     1096let 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 **)
     1105let 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 **)
     1114let 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 **)
     1123let 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 **)
     1130let rec virtual_dptr xxx =
     1131  xxx.virtual_dptr
     1132
     1133(** val actual_dptr : init_mutable -> Z.z **)
     1134let rec actual_dptr xxx =
     1135  xxx.actual_dptr
     1136
     1137(** val built : init_mutable -> ASM.labelled_instruction List.list **)
     1138let 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 **)
     1144let 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 **)
     1150let 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 **)
     1156let 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 **)
     1162let 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 **)
     1168let 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 -> __ **)
     1172let 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 -> __ **)
     1178let 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 **)
     1184let 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))))) }
    10831210
    10841211(** 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 = function
    1088 | AST.Init_int8 n -> store_bytes (List.Cons (n, List.Nil))
     1212    AST.ident List.list -> aSM_universe -> AST.init_data -> init_mutable ->
     1213    init_mutable **)
     1214let do_store_init_data globals u = function
     1215| AST.Init_int8 n -> store_byte n
    10891216| AST.Init_int16 n ->
    10901217  let { Types.fst = by0; Types.snd = by1 } =
    … …  
    10931220      Nat.O)))))))) n
    10941221  in
    1095   store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))
     1222  Relations.compose (store_byte by1) (store_byte by0)
    10961223| AST.Init_int32 n ->
    10971224  let { Types.fst = by0; Types.snd = n0 } =
    … …  
    11131240      Nat.O)))))))) n1
    11141241  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)
    11171245| 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 })
    11331248| AST.Init_null ->
    1134   store_bytes (List.Cons
    1135     ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1136        Nat.O))))))))), (List.Cons
    1137     ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1138        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)
    11391254| AST.Init_addrof (symb, ofs) ->
    11401255  let addr =
    … …  
    11581273      Nat.O)))))))) addr
    11591274  in
    1160   store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))
     1275  Relations.compose (store_byte by1) (store_byte by0)
    11611276
    11621277(** val do_store_init_data_list :
    … …  
    11641279    ASM.labelled_instruction List.list **)
    11651280let 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
    11841288    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)) })
     1289let 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))))))))))
    12431356
    12441357(** val get_symboltable :
    … …  
    12681381     in
    12691382    Monad.m_bind0 (Monad.smax_def State.state_monad)
    1270       (Util.foldl add_translation
    1271         (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 ->
    12731386      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 ->
    12761390        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 ->
    12791393          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
Note: See TracChangeset for help on using the changeset viewer.