Changeset 2773 for extracted/backEndOps.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/backEndOps.ml
r2743 r2773 17 17 open Extralib 18 18 19 open Lists 20 21 open Identifiers 22 23 open Integers 24 25 open AST 26 27 open Division 28 29 open Exp 30 31 open Arithmetic 32 19 33 open Setoids 20 34 … … 22 36 23 37 open Option 24 25 open Lists26 27 open Identifiers28 29 open Integers30 31 open AST32 33 open Division34 35 open Exp36 37 open Arithmetic38 38 39 39 open Extranat … … 402 402 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 403 403 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 404 let rec eval_rect_Type4 h_mk_Eval x_1 8831 =405 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8831 in404 let rec eval_rect_Type4 h_mk_Eval x_14141 = 405 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14141 in 406 406 h_mk_Eval opaccs0 op4 op5 407 407 … … 411 411 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 412 412 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 413 let rec eval_rect_Type5 h_mk_Eval x_1 8833 =414 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8833 in413 let rec eval_rect_Type5 h_mk_Eval x_14143 = 414 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14143 in 415 415 h_mk_Eval opaccs0 op4 op5 416 416 … … 420 420 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 421 421 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 422 let rec eval_rect_Type3 h_mk_Eval x_1 8835 =423 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8835 in422 let rec eval_rect_Type3 h_mk_Eval x_14145 = 423 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14145 in 424 424 h_mk_Eval opaccs0 op4 op5 425 425 … … 429 429 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 430 430 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 431 let rec eval_rect_Type2 h_mk_Eval x_1 8837 =432 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8837 in431 let rec eval_rect_Type2 h_mk_Eval x_14147 = 432 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14147 in 433 433 h_mk_Eval opaccs0 op4 op5 434 434 … … 438 438 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 439 439 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 440 let rec eval_rect_Type1 h_mk_Eval x_1 8839 =441 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8839 in440 let rec eval_rect_Type1 h_mk_Eval x_14149 = 441 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14149 in 442 442 h_mk_Eval opaccs0 op4 op5 443 443 … … 447 447 > (BitVector.bit > op2 > BitVector.byte > BitVector.byte > 448 448 (BitVector.byte, BitVector.bit) Types.prod) > 'a1) > eval > 'a1 **) 449 let rec eval_rect_Type0 h_mk_Eval x_1 8841 =450 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 8841 in449 let rec eval_rect_Type0 h_mk_Eval x_14151 = 450 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14151 in 451 451 h_mk_Eval opaccs0 op4 op5 452 452 … … 522 522 opAccs > BitVector.byte > BitVector.byte > (BitVector.byte, 523 523 BitVector.byte) Types.prod **) 524 let opaccs_implementation op 4by1 by2 =524 let opaccs_implementation op by1 by2 = 525 525 let n1 = 526 526 BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 531 531 (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2 532 532 in 533 (match op 4with533 (match op with 534 534  Mul > 535 let prod 0=535 let prod = 536 536 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 537 537 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 542 542 (Nat.S Nat.O))))))))) (Z.z_times n1 n2)) 543 543 in 544 { Types.fst = prod 0.Types.snd; Types.snd = prod0.Types.fst }544 { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst } 545 545  DivuModu > 546 546 (match Z.eqZb n2 Z.OZ with … … 555 555 556 556 (** val op1_implementation : op1 > BitVector.byte > BitVector.byte **) 557 let op1_implementation op 4by =558 match op 4with557 let op1_implementation op by = 558 match op with 559 559  Cmpl > 560 560 BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 572 572 BitVector.bit > op2 > BitVector.byte > BitVector.byte > 573 573 (BitVector.byte, BitVector.bit) Types.prod **) 574 let op2_implementation carry op 4by1 by2 =575 match op 4with574 let op2_implementation carry op by1 by2 = 575 match op with 576 576  Add > 577 let { Types.fst = res 1; Types.snd = flags } =577 let { Types.fst = res; Types.snd = flags } = 578 578 Arithmetic.add_8_with_carry by1 by2 Bool.False 579 579 in 580 { Types.fst = res 1; Types.snd =580 { Types.fst = res; Types.snd = 581 581 (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) } 582 582  Addc > 583 let { Types.fst = res 1; Types.snd = flags } =583 let { Types.fst = res; Types.snd = flags } = 584 584 Arithmetic.add_8_with_carry by1 by2 carry 585 585 in 586 { Types.fst = res 1; Types.snd =586 { Types.fst = res; Types.snd = 587 587 (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) } 588 588  Sub > 589 let { Types.fst = res 1; Types.snd = flags } =589 let { Types.fst = res; Types.snd = flags } = 590 590 Arithmetic.sub_8_with_carry by1 by2 carry 591 591 in 592 { Types.fst = res 1; Types.snd =592 { Types.fst = res; Types.snd = 593 593 (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) } 594 594  And > … … 613 613 opAccs > ByteValues.beval > ByteValues.beval > (ByteValues.beval, 614 614 ByteValues.beval) Types.prod Errors.res **) 615 let be_opaccs op 4a b =615 let be_opaccs op a b = 616 616 Obj.magic 617 617 (Monad.m_bind0 (Monad.max_def Errors.res0) … … 621 621 (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b)) 622 622 (fun b' > 623 let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op 4a' b' in623 let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in 624 624 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 625 625 (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') }))) 626 626 627 627 (** val be_op1 : op1 > ByteValues.beval > ByteValues.beval Errors.res **) 628 let be_op1 op 4a =628 let be_op1 op a = 629 629 Obj.magic 630 630 (Monad.m_bind0 (Monad.max_def Errors.res0) … … 632 632 (fun a' > 633 633 Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte 634 (eval0.op0 op 4a'))))634 (eval0.op0 op a')))) 635 635 636 636 (** val op2_bytes : … … 638 638 BitVector.byte Vector.vector > (BitVector.byte Vector.vector, 639 639 BitVector.bit) Types.prod **) 640 let op2_bytes op 4n carry =640 let op2_bytes op n carry = 641 641 let f = fun n0 b1 b2 pr > 642 642 let { Types.fst = res_tl; Types.snd = carry0 } = pr in 643 643 let { Types.fst = res_hd; Types.snd = carry' } = 644 eval0.op3 carry0 op 4b1 b2644 eval0.op3 carry0 op b1 b2 645 645 in 646 646 { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' } … … 652 652 (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **) 653 653 let be_add_sub_byte is_add carry a1 b2 = 654 let op 4=654 let op = 655 655 match is_add with 656 656  Bool.True > Addc … … 674 674 (fun carry' > 675 675 let { Types.fst = rslt; Types.snd = carry'' } = 676 eval0.op3 carry' op 4b1 b2676 eval0.op3 carry' op b1 b2 677 677 in 678 678 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 703 703 in 704 704 let { Types.fst = rslt; Types.snd = carry0 } = 705 eval0.op3 Bool.False op 4b2 o1o0.Types.snd705 eval0.op3 Bool.False op b2 o1o0.Types.snd 706 706 in 707 707 let p0 = Nat.O in 708 708 let ptr' = { Pointers.pblock = ptr.Pointers.pblock; 709 709 Pointers.poff = 710 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S710 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 711 711 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S 712 712 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst … … 750 750 in 751 751 let { Types.fst = rslt; Types.snd = ignore } = 752 op2_bytes op 4(Nat.S (Nat.S Nat.O)) Bool.False o1o1752 op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1 753 753 (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons 754 754 (Nat.O, by'0, Vector.VEmpty)))) … … 763 763 Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1)); 764 764 Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1, 765 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S765 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 766 766 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S 767 767 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) }) … … 798 798 ('a1 > 'a1 > Bool.bool) > 'a1 Types.option > 'a1 Types.option > 799 799 Bool.bool **) 800 let eq_opt eq 0m n =800 let eq_opt eq m n = 801 801 match m with 802 802  Types.None > … … 807 807 (match n with 808 808  Types.None > Bool.False 809  Types.Some b > eq 0a b)809  Types.Some b > eq a b) 810 810 811 811 (** val be_op2 : 812 812 ByteValues.bebit > op2 > ByteValues.beval > ByteValues.beval > 813 813 (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **) 814 let be_op2 carry op 4a1 a2 =814 let be_op2 carry op a1 a2 = 815 815 match a1 with 816 816  ByteValues.BVundef > … … 823 823 List.Nil)) 824 824  ByteValues.BVnonzero > 825 (match op 4with825 (match op with 826 826  Add > 827 827 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 844 844 List.Nil))) 845 845  ByteValues.BVXor (x, x0, x1) > 846 (match op 4with846 (match op with 847 847  Add > 848 848 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 865 865 List.Nil))) 866 866  ByteValues.BVByte x > 867 (match op 4with867 (match op with 868 868  Add > 869 869 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 894 894 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 895 895 List.Nil))) 896  ByteValues.BVXor (ptr1_opt, ptr1_opt', p 3) >896  ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) > 897 897 (match a2 with 898 898  ByteValues.BVundef > … … 900 900 List.Nil)) 901 901  ByteValues.BVnonzero > 902 (match op 4with902 (match op with 903 903  Add > 904 904 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 920 920 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 921 921 List.Nil))) 922  ByteValues.BVXor (ptr2_opt, ptr2_opt', p 4) >923 (match op 4with922  ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) > 923 (match op with 924 924  Add > 925 925 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 936 936  Or > 937 937 (match Bool.orb 938 (Bool.andb (Nat.eqb (ByteValues.part_no p 3) Nat.O)939 (Nat.eqb (ByteValues.part_no p 4) (Nat.S Nat.O)))940 (Bool.andb (Nat.eqb (ByteValues.part_no p 3) (Nat.S Nat.O))941 (Nat.eqb (ByteValues.part_no p 4) Nat.O)) with938 (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 942  Bool.True > 943 943 let eq_at = fun p ptr1 ptr2 > … … 954 954 (ByteValues.part_no p))) 955 955 in 956 (match Bool.andb (eq_opt (eq_at p 3) ptr1_opt ptr1_opt')957 (eq_opt (eq_at p 4) ptr2_opt ptr2_opt') with956 (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt') 957 (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with 958 958  Bool.True > 959 959 Obj.magic … … 973 973 List.Nil))) 974 974  ByteValues.BVByte b2 > 975 (match op 4with975 (match op with 976 976  Add > 977 977 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1016 1016 List.Nil)) 1017 1017  ByteValues.BVnonzero > 1018 (match op 4with1018 (match op with 1019 1019  Add > 1020 1020 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1046 1046 (fun carry0 > 1047 1047 let { Types.fst = result; Types.snd = carry1 } = 1048 eval0.op3 carry0 op 4b1 b21048 eval0.op3 carry0 op b1 b2 1049 1049 in 1050 1050 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = … … 1055 1055 List.Nil)) 1056 1056  ByteValues.BVptr (x, x0) > 1057 (match op 4with1057 (match op with 1058 1058  Add > 1059 1059 be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1 … … 1074 1074 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 1075 1075 List.Nil))) 1076  ByteValues.BVnull p 3>1076  ByteValues.BVnull p1 > 1077 1077 (match a2 with 1078 1078  ByteValues.BVundef > … … 1088 1088 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 1089 1089 List.Nil)) 1090  ByteValues.BVnull p 4>1091 (match op 4with1090  ByteValues.BVnull p2 > 1091 (match op with 1092 1092  Add > 1093 1093 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1106 1106 List.Nil)) 1107 1107  Xor > 1108 (match Nat.eqb (ByteValues.part_no p 3) (ByteValues.part_no p4) with1108 (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with 1109 1109  Bool.True > 1110 1110 Obj.magic 1111 1111 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 1112 (ByteValues.BVXor (Types.None, Types.None, p 3)); Types.snd =1112 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd = 1113 1113 carry }) 1114 1114  Bool.False > 1115 1115 Errors.Error (List.Cons ((Errors.MSG 1116 1116 ErrorMessages.UnsupportedOp), List.Nil)))) 1117  ByteValues.BVptr (ptr2, p 4) >1118 (match op 4with1117  ByteValues.BVptr (ptr2, p2) > 1118 (match op with 1119 1119  Add > 1120 1120 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1133 1133 List.Nil)) 1134 1134  Xor > 1135 (match Nat.eqb (ByteValues.part_no p 3) (ByteValues.part_no p4) with1135 (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with 1136 1136  Bool.True > 1137 1137 Obj.magic 1138 1138 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 1139 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p 3));1139 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1)); 1140 1140 Types.snd = carry }) 1141 1141  Bool.False > … … 1145 1145 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 1146 1146 List.Nil))) 1147  ByteValues.BVptr (ptr1, p 3) >1147  ByteValues.BVptr (ptr1, p1) > 1148 1148 (match a2 with 1149 1149  ByteValues.BVundef > … … 1157 1157 List.Nil)) 1158 1158  ByteValues.BVByte b2 > 1159 (match op 4with1159 (match op with 1160 1160  Add > 1161 1161 be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2 … … 1171 1171 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), 1172 1172 List.Nil))) 1173  ByteValues.BVnull p 4>1174 (match op 4with1173  ByteValues.BVnull p2 > 1174 (match op with 1175 1175  Add > 1176 1176 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1189 1189 List.Nil)) 1190 1190  Xor > 1191 (match Nat.eqb (ByteValues.part_no p 3) (ByteValues.part_no p4) with1191 (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with 1192 1192  Bool.True > 1193 1193 Obj.magic 1194 1194 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 1195 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p 3));1195 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1)); 1196 1196 Types.snd = carry }) 1197 1197  Bool.False > 1198 1198 Errors.Error (List.Cons ((Errors.MSG 1199 1199 ErrorMessages.UnsupportedOp), List.Nil)))) 1200  ByteValues.BVptr (ptr2, p 4) >1201 (match op 4with1200  ByteValues.BVptr (ptr2, p2) > 1201 (match op with 1202 1202  Add > 1203 1203 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp), … … 1212 1212 (Pointers.eq_block ptr1.Pointers.pblock 1213 1213 ptr2.Pointers.pblock) 1214 (Nat.eqb (ByteValues.part_no p 3)1215 (ByteValues.part_no p 4)) with1214 (Nat.eqb (ByteValues.part_no p1) 1215 (ByteValues.part_no p2)) with 1216 1216  Bool.True > 1217 1217 Obj.magic … … 1223 1223 byte_at AST.size_pointer 1224 1224 (Pointers.offv ptr1.Pointers.poff) 1225 (ByteValues.part_no p 3)1225 (ByteValues.part_no p1) 1226 1226 in 1227 1227 let by2 = 1228 1228 byte_at AST.size_pointer 1229 1229 (Pointers.offv ptr2.Pointers.poff) 1230 (ByteValues.part_no p 3)1230 (ByteValues.part_no p1) 1231 1231 in 1232 1232 let { Types.fst = result; Types.snd = carry1 } = … … 1249 1249 List.Nil)) 1250 1250  Xor > 1251 (match Nat.eqb (ByteValues.part_no p 3) (ByteValues.part_no p4) with1251 (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with 1252 1252  Bool.True > 1253 1253 Obj.magic 1254 1254 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 1255 1255 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2), 1256 p 3)); Types.snd = carry })1256 p1)); Types.snd = carry }) 1257 1257  Bool.False > 1258 1258 Errors.Error (List.Cons ((Errors.MSG
Note: See TracChangeset
for help on using the changeset viewer.