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

    r3034 r3043  
    224224      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    225225      Nat.O))))))))))))))))))), List.Nil)))))
    226 | ASM.MovSuccessor (dst, ws, lbl) ->
    227   let v = ASM.DATA
    228     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    229       Nat.O)))))))))
    230   in
    231   (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
    232            (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
    233            ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty))))))
    234            dst with
    235    | ASM.DIRECT b1 ->
    236      (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
    237        (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1); Types.snd =
    238        v })))))), List.Nil))
    239    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
    240    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
    241    | ASM.REGISTER r ->
    242      (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
    243        (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER r);
    244        Types.snd = v }))))))), List.Nil))
    245    | ASM.ACC_A ->
    246      (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
    247        (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
    248        v }))))))), List.Nil))
    249    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
    250    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
    251    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
    252    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
    253    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
    254    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
    255    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
    256    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
    257    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
    258    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
    259    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
    260    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
    261    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
    262    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
    263226| ASM.Call call ->
    264227  (match jmp_len with
     
    273236         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    274237         Nat.O))))))))))))))))))), List.Nil))
    275 | ASM.Mov (d, trgt) ->
    276   List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inr
    277     { Types.fst = ASM.DPTR; Types.snd = (ASM.DATA16
    278     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    279       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    280       Nat.O)))))))))))))))))) }))))), List.Nil)
     238| ASM.Mov (d, trgt, off) ->
     239  (match d with
     240   | Types.Inl x ->
     241     let address = ASM.DATA16
     242       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     243         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     244         Nat.O)))))))))))))))))
     245     in
     246     List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
     247     (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
     248   | Types.Inr pr ->
     249     let v = ASM.DATA
     250       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     251         (Nat.S Nat.O)))))))))
     252     in
     253     (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
     254              ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
     255              Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
     256              Vector.VEmpty)))))) pr.Types.fst with
     257      | ASM.DIRECT b1 ->
     258        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
     259          (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
     260          Types.snd = v })))))), List.Nil))
     261      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
     262      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
     263      | ASM.REGISTER r ->
     264        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
     265          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
     266          (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
     267      | ASM.ACC_A ->
     268        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
     269          (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
     270          ASM.ACC_A; Types.snd = v }))))))), List.Nil))
     271      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
     272      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
     273      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
     274      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
     275      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
     276      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
     277      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
     278      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
     279      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
     280      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
     281      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
     282      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
     283      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
     284      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
    281285
    282286(** val instruction_size_jmplen :
Note: See TracChangeset for help on using the changeset viewer.