Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret.ml

    r2649 r2717  
    2525open Listb
    2626
     27open String
     28
     29open LabelledObjects
     30
    2731open BitVectorTrie
    2832
    29 open String
    30 
    31 open LabelledObjects
     33open Exp
    3234
    3335open Arithmetic
     
    19071909       in
    19081910       Status.set_program_counter cm s2 new_pc)
    1909    | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)) __
     1911   | ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0)
     1912   | ASM.JMP x ->
     1913     (fun _ ->
     1914       let s0 = add_ticks1 s in
     1915       let dptr =
     1916         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1917           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1918           (Nat.S (Nat.S Nat.O))))))))
     1919           (Status.get_8051_sfr cm s0 Status.SFR_DPH)
     1920           (Status.get_8051_sfr cm s0 Status.SFR_DPL)
     1921       in
     1922       let big_acc =
     1923         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1924           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1925           (Nat.S (Nat.S Nat.O))))))))
     1926           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1927             (Nat.S Nat.O)))))))))
     1928           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
     1929       in
     1930       let jmp_addr =
     1931         Arithmetic.add
     1932           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1933             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1934             (Nat.S Nat.O))))))))) big_acc dptr
     1935       in
     1936       let new_pc =
     1937         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1938           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1939           Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
     1940       in
     1941       Status.set_program_counter cm s0 new_pc)) __
    19101942
    19111943(** val execute_1_preinstruction_ok' :
     
    37683800       in
    37693801       Status.set_program_counter cm s2 new_pc)) __)) __)
    3770    | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)) __
     3802   | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)
     3803   | ASM.JMP x ->
     3804     (fun _ ->
     3805       let s0 = add_ticks1 s in
     3806       let dptr =
     3807         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3808           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3809           (Nat.S (Nat.S Nat.O))))))))
     3810           (Status.get_8051_sfr cm s0 Status.SFR_DPH)
     3811           (Status.get_8051_sfr cm s0 Status.SFR_DPL)
     3812       in
     3813       let big_acc =
     3814         Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3815           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3816           (Nat.S (Nat.S Nat.O))))))))
     3817           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3818             (Nat.S Nat.O)))))))))
     3819           (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
     3820       in
     3821       let jmp_addr =
     3822         Arithmetic.add
     3823           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3824             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3825             (Nat.S Nat.O))))))))) big_acc dptr
     3826       in
     3827       let new_pc =
     3828         Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3829           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3830           Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
     3831       in
     3832       Status.set_program_counter cm s0 new_pc)) __
    37713833
    37723834(** val compute_target_of_unconditional_jump :
     
    38683930      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
    38693931      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
    3870 | ASM.JMP x ->
    3871   BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3872     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3873     Nat.O))))))))))))))))
    38743932| ASM.MOVC (x, x0) ->
    38753933  BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    38883946| ASM.LJMP x -> Bool.True
    38893947| ASM.SJMP x -> Bool.True
    3890 | ASM.JMP x -> Bool.False
    38913948| ASM.MOVC (x, x0) -> Bool.False
    38923949| ASM.RealInstruction x -> Bool.False
     
    40704127       in
    40714128       let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in
    4072        Status.set_program_counter cm s1 new_pc)
    4073    | ASM.JMP x ->
    4074      (fun _ ->
    4075        let s1 = Status.set_clock cm s (Nat.plus ticks s.Status.clock) in
    4076        let dptr =
    4077          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4078            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4079            (Nat.S (Nat.S Nat.O))))))))
    4080            (Status.get_8051_sfr cm s1 Status.SFR_DPH)
    4081            (Status.get_8051_sfr cm s1 Status.SFR_DPL)
    4082        in
    4083        let big_acc =
    4084          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4085            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4086            (Nat.S (Nat.S Nat.O))))))))
    4087            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4088              (Nat.S Nat.O)))))))))
    4089            (Status.get_8051_sfr cm s1 Status.SFR_ACC_A)
    4090        in
    4091        let jmp_addr =
    4092          Arithmetic.add
    4093            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4094              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4095              (Nat.S Nat.O))))))))) big_acc dptr
    4096        in
    4097        let new_pc =
    4098          Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4099            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4100            Nat.O)))))))))))))))) s1.Status.program_counter jmp_addr
    4101        in
    41024129       Status.set_program_counter cm s1 new_pc)
    41034130   | ASM.MOVC (addr1, addr2) ->
     
    42234250      Status.set_program_counter cm s1
    42244251        (Fetch.address_of_word_labels cm.Types.snd jmp)
     4252    | ASM.Jnz (acc, dst1, dst2) ->
     4253      (match Bool.notb
     4254               (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4255                 (Nat.S (Nat.S Nat.O))))))))
     4256                 (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
     4257                 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4258                   (Nat.S (Nat.S Nat.O)))))))))) with
     4259       | Bool.True ->
     4260         let s1 =
     4261           Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
     4262         in
     4263         Status.set_program_counter cm s1
     4264           (Fetch.address_of_word_labels cm.Types.snd dst1)
     4265       | Bool.False ->
     4266         let s1 =
     4267           Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
     4268         in
     4269         Status.set_program_counter cm s1
     4270           (Fetch.address_of_word_labels cm.Types.snd dst2))
     4271    | ASM.MovSuccessor (dst, ws, lbl) ->
     4272      let s1 =
     4273        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
     4274      in
     4275      let addr = Fetch.address_of_word_labels cm.Types.snd lbl in
     4276      let { Types.fst = high; Types.snd = low } =
     4277        Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4278          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4279          (Nat.S Nat.O)))))))) addr
     4280      in
     4281      let v =
     4282        match ws with
     4283        | ASM.HIGH -> high
     4284        | ASM.LOW -> low
     4285      in
     4286      Status.set_arg_8 cm s1
     4287        (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
     4288          Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
     4289          (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons
     4290          ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
     4291          Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
     4292          (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
     4293          (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
     4294          ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
     4295          ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
     4296          (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
     4297          ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
     4298          Vector.VEmpty)))))))))))))) dst) v
    42254299    | ASM.Call call ->
    42264300      let s1 =
Note: See TracChangeset for help on using the changeset viewer.