Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2977 r3001  
    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_185 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_185 in
     404let rec eval_rect_Type4 h_mk_Eval x_3714 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3714 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_187 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_187 in
     413let rec eval_rect_Type5 h_mk_Eval x_3716 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3716 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_189 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_189 in
     422let rec eval_rect_Type3 h_mk_Eval x_3718 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3718 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_191 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_191 in
     431let rec eval_rect_Type2 h_mk_Eval x_3720 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3720 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_193 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_193 in
     440let rec eval_rect_Type1 h_mk_Eval x_3722 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3722 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_195 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_195 in
     449let rec eval_rect_Type0 h_mk_Eval x_3724 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3724 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    702702                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    703703                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
    704                      (Pointers.offv ptr.Pointers.poff)
     704                     (Pointers.offv (Pointers.poff ptr))
    705705                 in
    706706                 let { Types.fst = rslt; Types.snd = carry0 } =
     
    708708                 in
    709709                 let p0 = Nat.O in
    710                  let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
     710                 let ptr' = { Pointers.pblock = (Pointers.pblock ptr);
    711711                   Pointers.poff =
    712712                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    729729              (match Bool.andb
    730730                       (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
    731                          (Pointers.eq_block ptr.Pointers.pblock
    732                            ptr'.Pointers.pblock))
     731                         (Pointers.eq_block (Pointers.pblock ptr)
     732                           (Pointers.pblock ptr')))
    733733                       (ByteValues.eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S
    734734                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S
     
    736736                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    737737                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
    738                          (Pointers.offv ptr.Pointers.poff)
    739                          (Pointers.offv ptr'.Pointers.poff)) with
     738                         (Pointers.offv (Pointers.poff ptr))
     739                         (Pointers.offv (Pointers.poff ptr'))) with
    740740               | Bool.True ->
    741741                 Util.if_then_else_safe
     
    746746                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
    747747                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
    748                        (Pointers.offv ptr.Pointers.poff)
     748                       (Pointers.offv (Pointers.poff ptr))
    749749                   in
    750750                   let o1o1 = Vector.VCons ((Nat.S Nat.O), o1o0.Types.fst,
     
    757757                   in
    758758                   let part1 = Nat.S Nat.O in
    759                    let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
     759                   let ptr'' = { Pointers.pblock = (Pointers.pblock ptr);
    760760                     Pointers.poff =
    761761                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
     
    939939           | AST.XData ->
    940940             (match Bool.andb
    941                       (Pointers.eq_block ptr1.Pointers.pblock
    942                         ptr2.Pointers.pblock)
     941                      (Pointers.eq_block (Pointers.pblock ptr1)
     942                        (Pointers.pblock ptr2))
    943943                      (Nat.eqb (ByteValues.part_no p1)
    944944                        (ByteValues.part_no p2)) with
     
    951951                    let by1 =
    952952                      byte_at AST.size_pointer
    953                         (Pointers.offv ptr1.Pointers.poff)
     953                        (Pointers.offv (Pointers.poff ptr1))
    954954                        (ByteValues.part_no p1)
    955955                    in
    956956                    let by2 =
    957957                      byte_at AST.size_pointer
    958                         (Pointers.offv ptr2.Pointers.poff)
     958                        (Pointers.offv (Pointers.poff ptr2))
    959959                        (ByteValues.part_no p1)
    960960                    in
     
    10371037             let eq_at = fun p ptr1 ptr2 ->
    10381038               Bool.andb
    1039                  (Pointers.eq_block ptr1.Pointers.pblock
    1040                    ptr2.Pointers.pblock)
     1039                 (Pointers.eq_block (Pointers.pblock ptr1)
     1040                   (Pointers.pblock ptr2))
    10411041                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    10421042                   (Nat.S (Nat.S Nat.O))))))))
    10431043                   (byte_at AST.size_pointer
    1044                      (Pointers.offv ptr1.Pointers.poff)
     1044                     (Pointers.offv (Pointers.poff ptr1))
    10451045                     (ByteValues.part_no p))
    10461046                   (byte_at AST.size_pointer
    1047                      (Pointers.offv ptr2.Pointers.poff)
     1047                     (Pointers.offv (Pointers.poff ptr2))
    10481048                     (ByteValues.part_no p)))
    10491049             in
Note: See TracChangeset for help on using the changeset viewer.