Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret.ml

    r2909 r3043  
    42524252(** val execute_1_pseudo_instruction0 :
    42534253    (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
    4254     Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
     4254    (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word)
     4255    -> Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
    42554256    Status.pseudoStatus **)
    4256 let execute_1_pseudo_instruction0 ticks cm s instr pc =
     4257let execute_1_pseudo_instruction0 ticks cm addr_of_label addr_of_symbol s instr pc =
    42574258  let s0 = Status.set_program_counter cm s pc in
    42584259  let s1 =
     
    42684269        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    42694270      in
    4270       Status.set_program_counter cm s1
    4271         (Fetch.address_of_word_labels cm.ASM.code jmp)
     4271      Status.set_program_counter cm s1 (addr_of_label jmp)
    42724272    | ASM.Jnz (acc, dst1, dst2) ->
    42734273      (match Bool.notb
     
    42814281           Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    42824282         in
    4283          Status.set_program_counter cm s1
    4284            (Fetch.address_of_word_labels cm.ASM.code dst1)
     4283         Status.set_program_counter cm s1 (addr_of_label dst1)
    42854284       | Bool.False ->
    42864285         let s1 =
    42874286           Status.set_clock cm s0 (Nat.plus ticks.Types.snd s0.Status.clock)
    42884287         in
    4289          Status.set_program_counter cm s1
    4290            (Fetch.address_of_word_labels cm.ASM.code dst2))
    4291     | ASM.MovSuccessor (dst, ws, lbl) ->
    4292       let s1 =
    4293         Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    4294       in
    4295       let addr = Fetch.address_of_word_labels cm.ASM.code lbl in
    4296       let { Types.fst = high; Types.snd = low } =
    4297         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4298           Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4299           (Nat.S Nat.O)))))))) addr
    4300       in
    4301       let v =
    4302         match ws with
    4303         | ASM.HIGH -> high
    4304         | ASM.LOW -> low
    4305       in
    4306       Status.set_arg_8 cm s1
    4307         (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
    4308           Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
    4309           (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons
    4310           ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
    4311           Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    4312           (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
    4313           (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
    4314           ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
    4315           ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
    4316           (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
    4317           ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
    4318           Vector.VEmpty)))))))))))))) dst) v
     4288         Status.set_program_counter cm s1 (addr_of_label dst2))
    43194289    | ASM.Call call ->
    43204290      let s1 =
    43214291        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    43224292      in
    4323       let a = Fetch.address_of_word_labels cm.ASM.code call in
     4293      let a = addr_of_label call in
    43244294      let new_sp =
    43254295        Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    43444314      let s5 = Status.write_at_stack_pointer cm s4 pc_bu in
    43454315      Status.set_program_counter cm s5 a
    4346     | ASM.Mov (dptr, ident) ->
     4316    | ASM.Mov (dst, ident, off) ->
    43474317      let s1 =
    43484318        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    43494319      in
    4350       let the_preamble = cm.ASM.preamble in
    4351       let data_labels = Status.construct_datalabels the_preamble in
    4352       Status.set_arg_16 cm s1
    4353         (Status.get_arg_16 cm s1 (ASM.DATA16
    4354           (Identifiers.lookup_def PreIdentifiers.ASMTag data_labels ident
    4355             (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4356               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4357               Nat.O)))))))))))))))))))) dptr
     4320      let v = addr_of_symbol ident in
     4321      (match dst with
     4322       | Types.Inl dptr -> Status.set_arg_16 cm s1 v dptr
     4323       | Types.Inr pr ->
     4324         let v' =
     4325           match pr.Types.snd with
     4326           | ASM.HIGH ->
     4327             (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4328               (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4329               (Nat.S (Nat.S Nat.O)))))))) v).Types.fst
     4330           | ASM.LOW ->
     4331             (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4332               (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4333               (Nat.S (Nat.S Nat.O)))))))) v).Types.snd
     4334         in
     4335         Status.set_arg_8 cm s1
     4336           (ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S
     4337             Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
     4338             (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons
     4339             ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
     4340             Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
     4341             (Nat.S (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S
     4342             (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect,
     4343             (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
     4344             ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
     4345             ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_b,
     4346             (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons
     4347             (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty))))))))))))))
     4348             pr.Types.fst) v')
    43584349  in
    43594350  s1
     
    43614352(** val execute_1_pseudo_instruction :
    43624353    ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat,
    4363     Nat.nat) Types.prod) -> Status.pseudoStatus -> Status.pseudoStatus **)
    4364 let execute_1_pseudo_instruction cm ticks_of s =
     4354    Nat.nat) Types.prod) -> (ASM.identifier -> BitVector.word) ->
     4355    (ASM.identifier -> BitVector.word) -> Status.pseudoStatus ->
     4356    Status.pseudoStatus **)
     4357let execute_1_pseudo_instruction cm ticks_of addr_of_label addr_of_symbol s =
    43654358  let { Types.fst = instr; Types.snd = pc } =
    43664359    ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter
    43674360  in
    43684361  let ticks = ticks_of s.Status.program_counter __ in
    4369   execute_1_pseudo_instruction0 ticks cm s instr pc
     4362  execute_1_pseudo_instruction0 ticks cm addr_of_label addr_of_symbol s instr
     4363    pc
    43704364
    43714365(** val execute :
Note: See TracChangeset for help on using the changeset viewer.