Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2873 r2933  
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_19271 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19271 in
     404let rec eval_rect_Type4 h_mk_Eval x_601 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_601 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
     
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_19273 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19273 in
     413let rec eval_rect_Type5 h_mk_Eval x_603 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_603 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
     
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_19275 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19275 in
     422let rec eval_rect_Type3 h_mk_Eval x_605 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_605 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
     
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_19277 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19277 in
     431let rec eval_rect_Type2 h_mk_Eval x_607 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_607 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
     
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_19279 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19279 in
     440let rec eval_rect_Type1 h_mk_Eval x_609 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_609 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
     
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_19281 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19281 in
     449let rec eval_rect_Type0 h_mk_Eval x_611 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_611 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    648648  Vector.fold_right2_i f { Types.fst = Vector.VEmpty; Types.snd = carry } n
    649649
     650(** val op_of_add_or_sub : ByteValues.add_or_sub -> op2 **)
     651let op_of_add_or_sub = function
     652| ByteValues.Do_add -> Addc
     653| ByteValues.Do_sub -> Sub
     654
    650655(** val be_add_sub_byte :
    651     Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
    652     (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
     656    ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
     657    BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
     658    Errors.res **)
    653659let be_add_sub_byte is_add carry a1 b2 =
    654   let op =
    655     match is_add with
    656     | Bool.True -> Addc
    657     | Bool.False -> Sub
    658   in
     660  let op = op_of_add_or_sub is_add in
    659661  (match a1 with
    660662   | ByteValues.BVundef ->
     
    726728            | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
    727729              (match Bool.andb
    728                        (Bool.andb (BitVector.eq_b is_add is_add')
     730                       (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
    729731                         (Pointers.eq_block ptr.Pointers.pblock
    730732                           ptr'.Pointers.pblock))
     
    755757                   in
    756758                   let part1 = Nat.S Nat.O in
    757                    let ptr'0 = { Pointers.pblock = ptr.Pointers.pblock;
     759                   let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
    758760                     Pointers.poff =
    759761                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
     
    761763                       Nat.O)))))))) rslt) }
    762764                   in
    763                    Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1));
    764                    Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1,
     765                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'', part1));
     766                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr', part1,
    765767                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    766768                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
     
    826828         List.Nil))
    827829     | ByteValues.BVByte b1 ->
    828        be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
     830       be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a2 b1
    829831     | ByteValues.BVnull x ->
    830832       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    842844            List.Nil))
    843845        | ByteValues.BVByte b2 ->
    844           be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
     846          be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a1
     847            b2
    845848        | ByteValues.BVnull x ->
    846849          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    866869       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    867870         List.Nil))
    868      | ByteValues.BVByte b1 -> be_add_sub_byte Bool.True carry a2 b1
     871     | ByteValues.BVByte b1 -> be_add_sub_byte ByteValues.Do_add carry a2 b1
    869872     | ByteValues.BVnull x ->
    870873       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    881884          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    882885            List.Nil))
    883         | ByteValues.BVByte b2 -> be_add_sub_byte Bool.True carry a1 b2
     886        | ByteValues.BVByte b2 ->
     887          be_add_sub_byte ByteValues.Do_add carry a1 b2
    884888        | ByteValues.BVnull x ->
    885889          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    905909       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    906910         List.Nil))
    907      | ByteValues.BVByte b1 -> be_add_sub_byte Bool.False carry a2 b1
     911     | ByteValues.BVByte b1 ->
     912       Obj.magic
     913         (Monad.m_bind0 (Monad.max_def Errors.res0)
     914           (Obj.magic
     915             (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
     916           (fun b2 ->
     917           Obj.magic (be_add_sub_byte ByteValues.Do_sub carry a1 b2)))
    908918     | ByteValues.BVnull x ->
    909919       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    920930          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    921931            List.Nil))
    922         | ByteValues.BVByte b2 -> be_add_sub_byte Bool.False carry a1 b2
     932        | ByteValues.BVByte b2 ->
     933          be_add_sub_byte ByteValues.Do_sub carry a1 b2
    923934        | ByteValues.BVnull x ->
    924935          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
Note: See TracChangeset for help on using the changeset viewer.