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

    r3001 r3043  
    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_3714 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3714 in
     404let rec eval_rect_Type4 h_mk_Eval x_16364 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16364 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_3716 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3716 in
     413let rec eval_rect_Type5 h_mk_Eval x_16366 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16366 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_3718 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3718 in
     422let rec eval_rect_Type3 h_mk_Eval x_16368 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16368 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_3720 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3720 in
     431let rec eval_rect_Type2 h_mk_Eval x_16370 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16370 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_3722 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3722 in
     440let rec eval_rect_Type1 h_mk_Eval x_16372 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16372 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_3724 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_3724 in
     449let rec eval_rect_Type0 h_mk_Eval x_16374 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16374 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 (Pointers.poff ptr))
     704                     (Pointers.offv ptr.Pointers.poff)
    705705                 in
    706706                 let { Types.fst = rslt; Types.snd = carry0 } =
     
    708708                 in
    709709                 let p0 = Nat.O in
    710                  let ptr' = { Pointers.pblock = (Pointers.pblock ptr);
     710                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
    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 (Pointers.pblock ptr)
    732                            (Pointers.pblock ptr')))
     731                         (Pointers.eq_block ptr.Pointers.pblock
     732                           ptr'.Pointers.pblock))
    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 (Pointers.poff ptr))
    739                          (Pointers.offv (Pointers.poff ptr'))) with
     738                         (Pointers.offv ptr.Pointers.poff)
     739                         (Pointers.offv ptr'.Pointers.poff)) 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 (Pointers.poff ptr))
     748                       (Pointers.offv ptr.Pointers.poff)
    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 = (Pointers.pblock ptr);
     759                   let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
    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 (Pointers.pblock ptr1)
    942                         (Pointers.pblock ptr2))
     941                      (Pointers.eq_block ptr1.Pointers.pblock
     942                        ptr2.Pointers.pblock)
    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 (Pointers.poff ptr1))
     953                        (Pointers.offv ptr1.Pointers.poff)
    954954                        (ByteValues.part_no p1)
    955955                    in
    956956                    let by2 =
    957957                      byte_at AST.size_pointer
    958                         (Pointers.offv (Pointers.poff ptr2))
     958                        (Pointers.offv ptr2.Pointers.poff)
    959959                        (ByteValues.part_no p1)
    960960                    in
     
    10371037             let eq_at = fun p ptr1 ptr2 ->
    10381038               Bool.andb
    1039                  (Pointers.eq_block (Pointers.pblock ptr1)
    1040                    (Pointers.pblock ptr2))
     1039                 (Pointers.eq_block ptr1.Pointers.pblock
     1040                   ptr2.Pointers.pblock)
    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 (Pointers.poff ptr1))
     1044                     (Pointers.offv ptr1.Pointers.poff)
    10451045                     (ByteValues.part_no p))
    10461046                   (byte_at AST.size_pointer
    1047                      (Pointers.offv (Pointers.poff ptr2))
     1047                     (Pointers.offv ptr2.Pointers.poff)
    10481048                     (ByteValues.part_no p)))
    10491049             in
Note: See TracChangeset for help on using the changeset viewer.