Ignore:
Timestamp:
Mar 14, 2013, 10:37:39 PM (8 years ago)
Author:
sacerdot
Message:

Extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2827 r2873  
    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_19102 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19102 in
     404let rec eval_rect_Type4 h_mk_Eval x_19271 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19271 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_19104 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19104 in
     413let rec eval_rect_Type5 h_mk_Eval x_19273 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19273 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_19106 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19106 in
     422let rec eval_rect_Type3 h_mk_Eval x_19275 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19275 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_19108 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19108 in
     431let rec eval_rect_Type2 h_mk_Eval x_19277 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19277 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_19110 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19110 in
     440let rec eval_rect_Type1 h_mk_Eval x_19279 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19279 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_19112 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19112 in
     449let rec eval_rect_Type0 h_mk_Eval x_19281 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19281 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    813813    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
    814814let be_op2 carry op a1 a2 =
    815   match a1 with
    816   | ByteValues.BVundef ->
    817     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    818       List.Nil))
    819   | ByteValues.BVnonzero ->
    820     (match a2 with
     815  match op with
     816  | Add ->
     817    (match a1 with
    821818     | ByteValues.BVundef ->
    822819       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    823820         List.Nil))
    824821     | ByteValues.BVnonzero ->
    825        (match op with
    826         | Add ->
    827           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    828             List.Nil))
    829         | Addc ->
    830           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    831             List.Nil))
    832         | Sub ->
    833           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    834             List.Nil))
    835         | And ->
    836           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    837             List.Nil))
    838         | Or ->
    839           Obj.magic
    840             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    841               ByteValues.BVnonzero; Types.snd = carry })
    842         | Xor ->
    843           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    844             List.Nil)))
     822       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     823         List.Nil))
    845824     | ByteValues.BVXor (x, x0, x1) ->
    846        (match op with
    847         | Add ->
    848           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    849             List.Nil))
    850         | Addc ->
    851           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    852             List.Nil))
    853         | Sub ->
    854           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    855             List.Nil))
    856         | And ->
    857           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    858             List.Nil))
    859         | Or ->
    860           Obj.magic
    861             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    862               ByteValues.BVnonzero; Types.snd = carry })
    863         | Xor ->
    864           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    865             List.Nil)))
    866      | ByteValues.BVByte x ->
    867        (match op with
    868         | Add ->
    869           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    870             List.Nil))
    871         | Addc ->
    872           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    873             List.Nil))
    874         | Sub ->
    875           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    876             List.Nil))
    877         | And ->
    878           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    879             List.Nil))
    880         | Or ->
    881           Obj.magic
    882             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    883               ByteValues.BVnonzero; Types.snd = carry })
    884         | Xor ->
    885           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    886             List.Nil)))
     825       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     826         List.Nil))
     827     | ByteValues.BVByte b1 ->
     828       be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
    887829     | ByteValues.BVnull x ->
    888830       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    889831         List.Nil))
    890      | ByteValues.BVptr (x, x0) ->
    891        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    892          List.Nil))
    893      | ByteValues.BVpc (x, x0) ->
    894        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    895          List.Nil)))
    896   | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
    897     (match a2 with
    898      | ByteValues.BVundef ->
    899        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    900          List.Nil))
    901      | ByteValues.BVnonzero ->
    902        (match op with
    903         | Add ->
    904           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    905             List.Nil))
    906         | Addc ->
    907           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    908             List.Nil))
    909         | Sub ->
    910           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    911             List.Nil))
    912         | And ->
    913           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    914             List.Nil))
    915         | Or ->
    916           Obj.magic
    917             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    918               ByteValues.BVnonzero; Types.snd = carry })
    919         | Xor ->
    920           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    921             List.Nil)))
    922      | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
    923        (match op with
    924         | Add ->
    925           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    926             List.Nil))
    927         | Addc ->
    928           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    929             List.Nil))
    930         | Sub ->
    931           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    932             List.Nil))
    933         | And ->
    934           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    935             List.Nil))
    936         | Or ->
    937           (match Bool.orb
    938                    (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
    939                      (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
    940                    (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
    941                      (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
    942            | Bool.True ->
    943              let eq_at = fun p ptr1 ptr2 ->
    944                Bool.andb
    945                  (Pointers.eq_block ptr1.Pointers.pblock
    946                    ptr2.Pointers.pblock)
    947                  (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    948                    (Nat.S (Nat.S Nat.O))))))))
    949                    (byte_at AST.size_pointer
    950                      (Pointers.offv ptr1.Pointers.poff)
    951                      (ByteValues.part_no p))
    952                    (byte_at AST.size_pointer
    953                      (Pointers.offv ptr2.Pointers.poff)
    954                      (ByteValues.part_no p)))
    955              in
    956              (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
    957                       (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
    958               | Bool.True ->
    959                 Obj.magic
    960                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    961                     (ByteValues.BVByte
    962                     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    963                       (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
    964               | Bool.False ->
    965                 Obj.magic
    966                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    967                     ByteValues.BVnonzero; Types.snd = carry }))
    968            | Bool.False ->
    969              Errors.Error (List.Cons ((Errors.MSG
    970                ErrorMessages.UnsupportedOp), List.Nil)))
    971         | Xor ->
    972           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    973             List.Nil)))
    974      | ByteValues.BVByte b2 ->
    975        (match op with
    976         | Add ->
    977           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    978             List.Nil))
    979         | Addc ->
    980           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    981             List.Nil))
    982         | Sub ->
    983           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    984             List.Nil))
    985         | And ->
    986           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    987             List.Nil))
    988         | Or ->
    989           (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    990                    (Nat.S (Nat.S Nat.O))))))))
    991                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    992                      (Nat.S (Nat.S Nat.O))))))))) b2 with
    993            | Bool.True ->
    994              Obj.magic
    995                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = a1;
    996                  Types.snd = carry })
    997            | Bool.False ->
    998              Errors.Error (List.Cons ((Errors.MSG
    999                ErrorMessages.UnsupportedOp), List.Nil)))
    1000         | Xor ->
    1001           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1002             List.Nil)))
    1003      | ByteValues.BVnull x ->
    1004        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1005          List.Nil))
    1006      | ByteValues.BVptr (x, x0) ->
    1007        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1008          List.Nil))
    1009      | ByteValues.BVpc (x, x0) ->
    1010        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1011          List.Nil)))
    1012   | ByteValues.BVByte b1 ->
    1013     (match a2 with
    1014      | ByteValues.BVundef ->
    1015        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1016          List.Nil))
    1017      | ByteValues.BVnonzero ->
    1018        (match op with
    1019         | Add ->
    1020           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1021             List.Nil))
    1022         | Addc ->
    1023           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1024             List.Nil))
    1025         | Sub ->
    1026           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1027             List.Nil))
    1028         | And ->
    1029           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1030             List.Nil))
    1031         | Or ->
    1032           Obj.magic
    1033             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1034               ByteValues.BVnonzero; Types.snd = carry })
    1035         | Xor ->
    1036           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1037             List.Nil)))
    1038      | ByteValues.BVXor (x, x0, x1) ->
    1039        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1040          List.Nil))
    1041      | ByteValues.BVByte b2 ->
    1042        Obj.magic
    1043          (Monad.m_bind0 (Monad.max_def Errors.res0)
    1044            (Obj.magic
    1045              (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
    1046            (fun carry0 ->
    1047            let { Types.fst = result; Types.snd = carry1 } =
    1048              eval0.op3 carry0 op b1 b2
    1049            in
    1050            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1051              (ByteValues.BVByte result); Types.snd = (ByteValues.BBbit
    1052              carry1) }))
    1053      | ByteValues.BVnull x ->
    1054        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1055          List.Nil))
    1056      | ByteValues.BVptr (x, x0) ->
    1057        (match op with
    1058         | Add ->
    1059           be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
    1060         | Addc -> be_add_sub_byte Bool.True carry a2 b1
    1061         | Sub ->
    1062           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1063             List.Nil))
    1064         | And ->
    1065           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1066             List.Nil))
    1067         | Or ->
    1068           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1069             List.Nil))
    1070         | Xor ->
     832     | ByteValues.BVptr (ptr1, p1) ->
     833       (match a2 with
     834        | ByteValues.BVundef ->
     835          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     836            List.Nil))
     837        | ByteValues.BVnonzero ->
     838          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     839            List.Nil))
     840        | ByteValues.BVXor (x, x0, x1) ->
     841          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     842            List.Nil))
     843        | ByteValues.BVByte b2 ->
     844          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
     845        | ByteValues.BVnull x ->
     846          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     847            List.Nil))
     848        | ByteValues.BVptr (x, x0) ->
     849          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     850            List.Nil))
     851        | ByteValues.BVpc (x, x0) ->
    1071852          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1072853            List.Nil)))
     
    1074855       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1075856         List.Nil)))
    1076   | ByteValues.BVnull p1 ->
    1077     (match a2 with
     857  | Addc ->
     858    (match a1 with
    1078859     | ByteValues.BVundef ->
    1079860       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    1085866       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1086867         List.Nil))
    1087      | ByteValues.BVByte x ->
    1088        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1089          List.Nil))
    1090      | ByteValues.BVnull p2 ->
    1091        (match op with
    1092         | Add ->
    1093           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1094             List.Nil))
    1095         | Addc ->
    1096           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1097             List.Nil))
    1098         | Sub ->
    1099           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1100             List.Nil))
    1101         | And ->
    1102           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1103             List.Nil))
    1104         | Or ->
    1105           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1106             List.Nil))
    1107         | Xor ->
    1108           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    1109            | Bool.True ->
    1110              Obj.magic
    1111                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1112                  (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
    1113                  carry })
    1114            | Bool.False ->
    1115              Errors.Error (List.Cons ((Errors.MSG
    1116                ErrorMessages.UnsupportedOp), List.Nil))))
    1117      | ByteValues.BVptr (ptr2, p2) ->
    1118        (match op with
    1119         | Add ->
    1120           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1121             List.Nil))
    1122         | Addc ->
    1123           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1124             List.Nil))
    1125         | Sub ->
    1126           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1127             List.Nil))
    1128         | And ->
    1129           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1130             List.Nil))
    1131         | Or ->
    1132           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1133             List.Nil))
    1134         | Xor ->
    1135           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    1136            | Bool.True ->
    1137              Obj.magic
    1138                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1139                  (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
    1140                  Types.snd = carry })
    1141            | Bool.False ->
    1142              Errors.Error (List.Cons ((Errors.MSG
    1143                ErrorMessages.UnsupportedOp), List.Nil))))
     868     | ByteValues.BVByte b1 -> be_add_sub_byte Bool.True carry a2 b1
     869     | ByteValues.BVnull x ->
     870       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     871         List.Nil))
     872     | ByteValues.BVptr (ptr1, p1) ->
     873       (match a2 with
     874        | ByteValues.BVundef ->
     875          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     876            List.Nil))
     877        | ByteValues.BVnonzero ->
     878          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     879            List.Nil))
     880        | ByteValues.BVXor (x, x0, x1) ->
     881          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     882            List.Nil))
     883        | ByteValues.BVByte b2 -> be_add_sub_byte Bool.True carry a1 b2
     884        | ByteValues.BVnull x ->
     885          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     886            List.Nil))
     887        | ByteValues.BVptr (x, x0) ->
     888          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     889            List.Nil))
     890        | ByteValues.BVpc (x, x0) ->
     891          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     892            List.Nil)))
    1144893     | ByteValues.BVpc (x, x0) ->
    1145894       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1146895         List.Nil)))
    1147   | ByteValues.BVptr (ptr1, p1) ->
    1148     (match a2 with
     896  | Sub ->
     897    (match a1 with
    1149898     | ByteValues.BVundef ->
    1150899       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    1156905       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1157906         List.Nil))
    1158      | ByteValues.BVByte b2 ->
    1159        (match op with
    1160         | Add ->
    1161           be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
    1162         | Addc -> be_add_sub_byte Bool.True carry a1 b2
    1163         | Sub -> be_add_sub_byte Bool.False carry a1 b2
    1164         | And ->
    1165           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1166             List.Nil))
    1167         | Or ->
    1168           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1169             List.Nil))
    1170         | Xor ->
    1171           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1172             List.Nil)))
    1173      | ByteValues.BVnull p2 ->
    1174        (match op with
    1175         | Add ->
    1176           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1177             List.Nil))
    1178         | Addc ->
    1179           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1180             List.Nil))
    1181         | Sub ->
    1182           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1183             List.Nil))
    1184         | And ->
    1185           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1186             List.Nil))
    1187         | Or ->
    1188           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1189             List.Nil))
    1190         | Xor ->
    1191           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    1192            | Bool.True ->
    1193              Obj.magic
    1194                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1195                  (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
    1196                  Types.snd = carry })
    1197            | Bool.False ->
    1198              Errors.Error (List.Cons ((Errors.MSG
    1199                ErrorMessages.UnsupportedOp), List.Nil))))
    1200      | ByteValues.BVptr (ptr2, p2) ->
    1201        (match op with
    1202         | Add ->
    1203           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1204             List.Nil))
    1205         | Addc ->
    1206           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1207             List.Nil))
    1208         | Sub ->
     907     | ByteValues.BVByte b1 -> be_add_sub_byte Bool.False carry a2 b1
     908     | ByteValues.BVnull x ->
     909       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     910         List.Nil))
     911     | ByteValues.BVptr (ptr1, p1) ->
     912       (match a2 with
     913        | ByteValues.BVundef ->
     914          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     915            List.Nil))
     916        | ByteValues.BVnonzero ->
     917          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     918            List.Nil))
     919        | ByteValues.BVXor (x, x0, x1) ->
     920          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     921            List.Nil))
     922        | ByteValues.BVByte b2 -> be_add_sub_byte Bool.False carry a1 b2
     923        | ByteValues.BVnull x ->
     924          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     925            List.Nil))
     926        | ByteValues.BVptr (ptr2, p2) ->
    1209927          (match Pointers.ptype ptr1 with
    1210928           | AST.XData ->
     
    1242960             Errors.Error (List.Cons ((Errors.MSG
    1243961               ErrorMessages.UnsupportedOp), List.Nil)))
    1244         | And ->
    1245           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1246             List.Nil))
    1247         | Or ->
    1248           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1249             List.Nil))
    1250         | Xor ->
     962        | ByteValues.BVpc (x, x0) ->
     963          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     964            List.Nil)))
     965     | ByteValues.BVpc (x, x0) ->
     966       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     967         List.Nil)))
     968  | And ->
     969    Obj.magic
     970      (Monad.m_bind0 (Monad.max_def Errors.res0)
     971        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a1))
     972        (fun b1 ->
     973        Monad.m_bind0 (Monad.max_def Errors.res0)
     974          (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
     975          (fun b2 ->
     976          let res = (eval0.op3 Bool.False And b1 b2).Types.fst in
     977          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     978            (ByteValues.BVByte res); Types.snd = carry })))
     979  | Or ->
     980    (match a1 with
     981     | ByteValues.BVundef ->
     982       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     983         List.Nil))
     984     | ByteValues.BVnonzero ->
     985       (match a2 with
     986        | ByteValues.BVundef ->
     987          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     988            List.Nil))
     989        | ByteValues.BVnonzero ->
     990          Obj.magic
     991            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     992              ByteValues.BVnonzero; Types.snd = carry })
     993        | ByteValues.BVXor (x, x0, x1) ->
     994          Obj.magic
     995            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     996              ByteValues.BVnonzero; Types.snd = carry })
     997        | ByteValues.BVByte x ->
     998          Obj.magic
     999            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1000              ByteValues.BVnonzero; Types.snd = carry })
     1001        | ByteValues.BVnull x ->
     1002          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1003            List.Nil))
     1004        | ByteValues.BVptr (x, x0) ->
     1005          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1006            List.Nil))
     1007        | ByteValues.BVpc (x, x0) ->
     1008          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1009            List.Nil)))
     1010     | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
     1011       (match a2 with
     1012        | ByteValues.BVundef ->
     1013          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1014            List.Nil))
     1015        | ByteValues.BVnonzero ->
     1016          Obj.magic
     1017            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1018              ByteValues.BVnonzero; Types.snd = carry })
     1019        | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
     1020          (match Bool.orb
     1021                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
     1022                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
     1023                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
     1024                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
     1025           | Bool.True ->
     1026             let eq_at = fun p ptr1 ptr2 ->
     1027               Bool.andb
     1028                 (Pointers.eq_block ptr1.Pointers.pblock
     1029                   ptr2.Pointers.pblock)
     1030                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1031                   (Nat.S (Nat.S Nat.O))))))))
     1032                   (byte_at AST.size_pointer
     1033                     (Pointers.offv ptr1.Pointers.poff)
     1034                     (ByteValues.part_no p))
     1035                   (byte_at AST.size_pointer
     1036                     (Pointers.offv ptr2.Pointers.poff)
     1037                     (ByteValues.part_no p)))
     1038             in
     1039             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
     1040                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
     1041              | Bool.True ->
     1042                Obj.magic
     1043                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1044                    (ByteValues.BVByte
     1045                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1046                      (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
     1047              | Bool.False ->
     1048                Obj.magic
     1049                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1050                    ByteValues.BVnonzero; Types.snd = carry }))
     1051           | Bool.False ->
     1052             Errors.Error (List.Cons ((Errors.MSG
     1053               ErrorMessages.UnsupportedOp), List.Nil)))
     1054        | ByteValues.BVByte x ->
     1055          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1056            List.Nil))
     1057        | ByteValues.BVnull x ->
     1058          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1059            List.Nil))
     1060        | ByteValues.BVptr (x, x0) ->
     1061          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1062            List.Nil))
     1063        | ByteValues.BVpc (x, x0) ->
     1064          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1065            List.Nil)))
     1066     | ByteValues.BVByte b1 ->
     1067       (match a2 with
     1068        | ByteValues.BVundef ->
     1069          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1070            List.Nil))
     1071        | ByteValues.BVnonzero ->
     1072          Obj.magic
     1073            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1074              ByteValues.BVnonzero; Types.snd = carry })
     1075        | ByteValues.BVXor (x, x0, x1) ->
     1076          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1077            List.Nil))
     1078        | ByteValues.BVByte b2 ->
     1079          let res = (eval0.op3 Bool.False Or b1 b2).Types.fst in
     1080          Obj.magic
     1081            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1082              (ByteValues.BVByte res); Types.snd = carry })
     1083        | ByteValues.BVnull x ->
     1084          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1085            List.Nil))
     1086        | ByteValues.BVptr (x, x0) ->
     1087          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1088            List.Nil))
     1089        | ByteValues.BVpc (x, x0) ->
     1090          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1091            List.Nil)))
     1092     | ByteValues.BVnull x ->
     1093       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1094         List.Nil))
     1095     | ByteValues.BVptr (x, x0) ->
     1096       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1097         List.Nil))
     1098     | ByteValues.BVpc (x, x0) ->
     1099       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1100         List.Nil)))
     1101  | Xor ->
     1102    (match a1 with
     1103     | ByteValues.BVundef ->
     1104       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1105         List.Nil))
     1106     | ByteValues.BVnonzero ->
     1107       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1108         List.Nil))
     1109     | ByteValues.BVXor (x, x0, x1) ->
     1110       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1111         List.Nil))
     1112     | ByteValues.BVByte b1 ->
     1113       (match a2 with
     1114        | ByteValues.BVundef ->
     1115          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1116            List.Nil))
     1117        | ByteValues.BVnonzero ->
     1118          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1119            List.Nil))
     1120        | ByteValues.BVXor (x, x0, x1) ->
     1121          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1122            List.Nil))
     1123        | ByteValues.BVByte b2 ->
     1124          let res = (eval0.op3 Bool.False Xor b1 b2).Types.fst in
     1125          Obj.magic
     1126            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1127              (ByteValues.BVByte res); Types.snd = carry })
     1128        | ByteValues.BVnull x ->
     1129          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1130            List.Nil))
     1131        | ByteValues.BVptr (x, x0) ->
     1132          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1133            List.Nil))
     1134        | ByteValues.BVpc (x, x0) ->
     1135          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1136            List.Nil)))
     1137     | ByteValues.BVnull p1 ->
     1138       (match a2 with
     1139        | ByteValues.BVundef ->
     1140          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1141            List.Nil))
     1142        | ByteValues.BVnonzero ->
     1143          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1144            List.Nil))
     1145        | ByteValues.BVXor (x, x0, x1) ->
     1146          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1147            List.Nil))
     1148        | ByteValues.BVByte x ->
     1149          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1150            List.Nil))
     1151        | ByteValues.BVnull p2 ->
     1152          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
     1153           | Bool.True ->
     1154             Obj.magic
     1155               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1156                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
     1157                 carry })
     1158           | Bool.False ->
     1159             Errors.Error (List.Cons ((Errors.MSG
     1160               ErrorMessages.UnsupportedOp), List.Nil)))
     1161        | ByteValues.BVptr (ptr2, p2) ->
     1162          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
     1163           | Bool.True ->
     1164             Obj.magic
     1165               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1166                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
     1167                 Types.snd = carry })
     1168           | Bool.False ->
     1169             Errors.Error (List.Cons ((Errors.MSG
     1170               ErrorMessages.UnsupportedOp), List.Nil)))
     1171        | ByteValues.BVpc (x, x0) ->
     1172          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1173            List.Nil)))
     1174     | ByteValues.BVptr (ptr1, p1) ->
     1175       (match a2 with
     1176        | ByteValues.BVundef ->
     1177          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1178            List.Nil))
     1179        | ByteValues.BVnonzero ->
     1180          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1181            List.Nil))
     1182        | ByteValues.BVXor (x, x0, x1) ->
     1183          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1184            List.Nil))
     1185        | ByteValues.BVByte x ->
     1186          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1187            List.Nil))
     1188        | ByteValues.BVnull p2 ->
     1189          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
     1190           | Bool.True ->
     1191             Obj.magic
     1192               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     1193                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
     1194                 Types.snd = carry })
     1195           | Bool.False ->
     1196             Errors.Error (List.Cons ((Errors.MSG
     1197               ErrorMessages.UnsupportedOp), List.Nil)))
     1198        | ByteValues.BVptr (ptr2, p2) ->
    12511199          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    12521200           | Bool.True ->
     
    12571205           | Bool.False ->
    12581206             Errors.Error (List.Cons ((Errors.MSG
    1259                ErrorMessages.UnsupportedOp), List.Nil))))
     1207               ErrorMessages.UnsupportedOp), List.Nil)))
     1208        | ByteValues.BVpc (x, x0) ->
     1209          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     1210            List.Nil)))
    12601211     | ByteValues.BVpc (x, x0) ->
    12611212       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    12621213         List.Nil)))
    1263   | ByteValues.BVpc (x, x0) ->
    1264     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    1265       List.Nil))
    1266 
     1214
Note: See TracChangeset for help on using the changeset viewer.