Changeset 3069 for extracted/assembly.ml


Ignore:
Timestamp:
Apr 2, 2013, 2:09:34 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r3065 r3069  
    26442644| ASM.JMP arg -> List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil)
    26452645
     2646(** val is_code : AST.region -> Bool.bool **)
     2647let is_code = function
     2648| AST.XData -> Bool.False
     2649| AST.Code -> Bool.True
     2650
    26462651(** val expand_pseudo_instruction :
    26472652    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    26482653    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    2649     BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list **)
     2654    (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     2655    ASM.instruction List.list **)
    26502656let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function
    26512657| ASM.Instruction instr ->
     
    27142720     List.Cons ((ASM.LCALL address), List.Nil))
    27152721| ASM.Mov (d, trgt, off) ->
    2716   let addr =
    2717     (Arithmetic.add_16_with_carry (lookup_datalabels trgt) off Bool.False).Types.fst
     2722  let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in
     2723  let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in
     2724  let addr1 =
     2725    match is_code r with
     2726    | Bool.True -> sigma addr0
     2727    | Bool.False -> addr0
    27182728  in
    27192729  (match d with
    27202730   | Types.Inl x ->
    2721      let address = ASM.DATA16 addr in
     2731     let address = ASM.DATA16 addr1 in
    27222732     List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
    27232733     (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
     
    27282738          (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    27292739            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2730             (Nat.S (Nat.S Nat.O)))))))) addr).Types.fst
     2740            (Nat.S (Nat.S Nat.O)))))))) addr1).Types.fst
    27312741        | ASM.LOW ->
    27322742          (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    27332743            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2734             (Nat.S (Nat.S Nat.O)))))))) addr).Types.snd)
     2744            (Nat.S (Nat.S Nat.O)))))))) addr1).Types.snd)
    27352745     in
    27362746     (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
     
    27442754      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
    27452755      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
    2746       | ASM.REGISTER r ->
     2756      | ASM.REGISTER r0 ->
    27472757        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
    27482758          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
    2749           (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
     2759          (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil))
    27502760      | ASM.ACC_A ->
    27512761        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
     
    27702780    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    27712781    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    2772     BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
    2773     Vector.vector List.list) Types.prod **)
     2782    (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     2783    (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **)
    27742784let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i =
    27752785  let pseudos =
     
    27832793
    27842794(** val instruction_size :
    2785     (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word)
    2786     -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
    2787     BitVector.word -> ASM.pseudo_instruction -> Nat.nat **)
     2795    (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
     2796    BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
     2797    (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
     2798    -> Nat.nat **)
    27882799let instruction_size lookup_labels lookup_datalabels sigma policy ppc i =
    27892800  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
     
    28082819  in
    28092820  let lookup_datalabels = fun x ->
    2810     Identifiers.lookup_def PreIdentifiers.ASMTag datalabels x
    2811       (sigma (lookup_labels x))
     2821    match Identifiers.lookup PreIdentifiers.ASMTag
     2822            (Status.construct_datalabels preamble) x with
     2823    | Types.None -> { Types.fst = AST.Code; Types.snd = (lookup_labels x) }
     2824    | Types.Some addr -> { Types.fst = AST.XData; Types.snd = addr }
    28122825  in
    28132826  (let { Types.fst = next_pc; Types.snd = revcode } =
Note: See TracChangeset for help on using the changeset viewer.