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/interpret.ml

    r3064 r3069  
    16311631              | Types.Inr r'' ->
    16321632                let { Types.fst = addr1; Types.snd = addr2 } = r'' in
    1633                 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
     1633                Status.set_arg_16 cm s0
     1634                  (Status.get_arg_16 cm s0
     1635                    (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
     1636                      (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16,
     1637                      Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O),
     1638                      ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr,
     1639                      Vector.VEmpty)))) addr2)) addr1)
    16341640           | Types.Inr r ->
    16351641             let { Types.fst = addr1; Types.snd = addr2 } = r in
     
    19301936       Status.set_program_counter cm s2 new_pc)
    19311937   | ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0)
    1932    | ASM.JMP x ->
    1933      (fun _ ->
    1934        let s0 = add_ticks1 s in
    1935        let dptr =
    1936          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1937            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1938            (Nat.S (Nat.S Nat.O))))))))
    1939            (Status.get_8051_sfr cm s0 Status.SFR_DPH)
    1940            (Status.get_8051_sfr cm s0 Status.SFR_DPL)
    1941        in
    1942        let big_acc =
    1943          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1944            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1945            (Nat.S (Nat.S Nat.O))))))))
    1946            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1947              (Nat.S Nat.O)))))))))
    1948            (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
    1949        in
     1938   | ASM.JMP acc_dptr ->
     1939     (fun _ ->
     1940       let s0 = add_ticks1 s in
    19501941       let jmp_addr =
    1951          Arithmetic.add
    1952            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1953              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1954              (Nat.S Nat.O))))))))) big_acc dptr
     1942         Status.get_arg_16 cm s0
     1943           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
     1944             Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))
     1945             (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O,
     1946             ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr)
    19551947       in
    19561948       Status.set_program_counter cm s0 jmp_addr)) __
     
    35013493              | Types.Inr r'' ->
    35023494                let { Types.fst = addr1; Types.snd = addr2 } = r'' in
    3503                 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
     3495                Status.set_arg_16 cm s0
     3496                  (Status.get_arg_16 cm s0
     3497                    (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
     3498                      (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16,
     3499                      Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O),
     3500                      ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr,
     3501                      Vector.VEmpty)))) addr2)) addr1)
    35043502           | Types.Inr r ->
    35053503             let { Types.fst = addr1; Types.snd = addr2 } = r in
     
    38163814       Status.set_program_counter cm s2 new_pc)) __)) __)
    38173815   | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)
    3818    | ASM.JMP x ->
    3819      (fun _ ->
    3820        let s0 = add_ticks1 s in
    3821        let dptr =
    3822          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3823            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3824            (Nat.S (Nat.S Nat.O))))))))
    3825            (Status.get_8051_sfr cm s0 Status.SFR_DPH)
    3826            (Status.get_8051_sfr cm s0 Status.SFR_DPL)
    3827        in
    3828        let big_acc =
    3829          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3830            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3831            (Nat.S (Nat.S Nat.O))))))))
    3832            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3833              (Nat.S Nat.O)))))))))
    3834            (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
    3835        in
     3816   | ASM.JMP acc_dptr ->
     3817     (fun _ ->
     3818       let s0 = add_ticks1 s in
    38363819       let jmp_addr =
    3837          Arithmetic.add
    3838            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3839              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3840              (Nat.S Nat.O))))))))) big_acc dptr
    3841        in
    3842        let new_pc =
    3843          Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3844            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3845            Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
    3846        in
    3847        Status.set_program_counter cm s0 new_pc)) __
     3820         Status.get_arg_16 cm s0
     3821           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
     3822             Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))
     3823             (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O,
     3824             ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr)
     3825       in
     3826       Status.set_program_counter cm s0 jmp_addr)) __
    38483827
    38493828(** val compute_target_of_unconditional_jump :
Note: See TracChangeset for help on using the changeset viewer.