Changeset 2951 for extracted/lINToASM.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lINToASM.ml

    r2890 r2951  
    8282
    8383open ASM
     84
     85open Extra_bool
     86
     87open Coqlib
     88
     89open Values
     90
     91open FrontEndVal
     92
     93open GenMem
     94
     95open FrontEndMem
     96
     97open Globalenvs
    8498
    8599open Sets
     
    127141    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    128142    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    129 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_24583 =
     143let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_2395 =
    130144  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
    133146  in
    134147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    140153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    141154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    142 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_24585 =
     155let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_2397 =
    143156  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
    146158  in
    147159  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    153165    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    154166    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    155 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_24587 =
     167let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_2399 =
    156168  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
    159170  in
    160171  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    166177    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    167178    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    168 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24589 =
     179let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_2401 =
    169180  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
    172182  in
    173183  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    179189    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    180190    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    181 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24591 =
     191let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_2403 =
    182192  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
    185194  in
    186195  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    192201    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    193202    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    194 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24593 =
     203let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_2405 =
    195204  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
    198206  in
    199207  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    280288  let globals_addr_internal = fun res_offset x_size ->
    281289    let { Types.fst = res; Types.snd = offset } = res_offset in
    282     let { Types.fst = eta29086; Types.snd = size } = x_size in
    283     let { Types.fst = x; Types.snd = region } = eta29086 in
     290    let { Types.fst = eta24644; Types.snd = data } = x_size in
     291    let { Types.fst = x; Types.snd = region } = eta24644 in
    284292    { Types.fst =
    285293    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    287295        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    288296        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))) }
    290298  in
    291299  let addresses =
    292300    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
    295306  in
    296307  { id_univ = Positive.One; current_funct = Positive.One; ident_map =
     
    309320        (Identifiers.empty_map PreIdentifiers.LabelTag)
    310321    in
    311     let { Types.fst = eta29087; Types.snd = lmap0 } =
     322    let { Types.fst = eta24645; Types.snd = lmap0 } =
    312323      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    313324      | Types.None ->
     
    321332          lmap }
    322333    in
    323     let { Types.fst = id; Types.snd = univ } = eta29087 in
     334    let { Types.fst = id; Types.snd = univ } = eta24645 in
    324335    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    325336    u.ident_map; label_map =
     
    333344  Obj.magic (fun u ->
    334345    let imap = u.ident_map in
    335     let { Types.fst = eta29088; Types.snd = imap0 } =
     346    let { Types.fst = eta24646; Types.snd = imap0 } =
    336347      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    337348      | Types.None ->
     
    345356          imap }
    346357    in
    347     let { Types.fst = id; Types.snd = univ } = eta29088 in
     358    let { Types.fst = id; Types.snd = univ } = eta24646 in
    348359    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    349360    ident_map = imap0; label_map = u.label_map; address_map =
     
    10231034      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
    10241035
     1036(** val store_bytes :
     1037    BitVector.byte List.list -> ASM.labelled_instruction List.list **)
     1038let 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 **)
     1051let 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 **)
     1129let 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 **)
     1143let 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
    10251202(** val get_symboltable :
    10261203    AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
     
    10421219       Monad.m_bind0 (Monad.smax_def State.state_monad)
    10431220         (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 ->
    10461223         Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
    10471224           Monad.m_return0 (Monad.smax_def State.state_monad)
     
    10511228      (Util.foldl add_translation
    10521229        (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 ->
    10541231      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))
    10571233        (fun exit_label ->
    10581234        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 ->
    10621237          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))
    10651239            (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.