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

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/byteValues.ml
r2743 r2773 15 15 open Extralib 16 16 17 open Lists 18 19 open Identifiers 20 21 open Integers 22 23 open AST 24 25 open Division 26 27 open Exp 28 29 open Arithmetic 30 17 31 open Setoids 18 32 … … 20 34 21 35 open Option 22 23 open Lists24 25 open Identifiers26 27 open Integers28 29 open AST30 31 open Division32 33 open Exp34 35 open Arithmetic36 36 37 37 open Extranat … … 89 89 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 90 90 'a1 **) 91 let rec program_counter_rect_Type4 h_mk_program_counter x_ 6100=92 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6100in91 let rec program_counter_rect_Type4 h_mk_program_counter x_4404 = 92 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4404 in 93 93 h_mk_program_counter pc_block0 pc_offset0 94 94 … … 96 96 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 97 97 'a1 **) 98 let rec program_counter_rect_Type5 h_mk_program_counter x_ 6102=99 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6102in98 let rec program_counter_rect_Type5 h_mk_program_counter x_4406 = 99 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4406 in 100 100 h_mk_program_counter pc_block0 pc_offset0 101 101 … … 103 103 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 104 104 'a1 **) 105 let rec program_counter_rect_Type3 h_mk_program_counter x_ 6104=106 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6104in105 let rec program_counter_rect_Type3 h_mk_program_counter x_4408 = 106 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4408 in 107 107 h_mk_program_counter pc_block0 pc_offset0 108 108 … … 110 110 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 111 111 'a1 **) 112 let rec program_counter_rect_Type2 h_mk_program_counter x_ 6106=113 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6106in112 let rec program_counter_rect_Type2 h_mk_program_counter x_4410 = 113 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4410 in 114 114 h_mk_program_counter pc_block0 pc_offset0 115 115 … … 117 117 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 118 118 'a1 **) 119 let rec program_counter_rect_Type1 h_mk_program_counter x_ 6108=120 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6108in119 let rec program_counter_rect_Type1 h_mk_program_counter x_4412 = 120 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4412 in 121 121 h_mk_program_counter pc_block0 pc_offset0 122 122 … … 124 124 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 125 125 'a1 **) 126 let rec program_counter_rect_Type0 h_mk_program_counter x_ 6110=127 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6110in126 let rec program_counter_rect_Type0 h_mk_program_counter x_4414 = 127 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4414 in 128 128 h_mk_program_counter pc_block0 pc_offset0 129 129 … … 184 184 Bool.andb 185 185 (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block)) 186 (Positive.eqb 0pc1.pc_offset pc2.pc_offset)186 (Positive.eqb pc1.pc_offset pc2.pc_offset) 187 187 188 188 (** val bitvector_from_pos : … … 202 202 let cpointer_of_pc pc = 203 203 let pc_off = pc.pc_offset in 204 (match Positive.leb 0pc_off (Positive.two_power_nat Pointers.offset_size) with204 (match Positive.leb pc_off (Positive.two_power_nat Pointers.offset_size) with 205 205  Bool.True > 206 206 Obj.magic 207 (Monad.m_return0 (Monad.max_def Option.option 0) { Pointers.pblock =207 (Monad.m_return0 (Monad.max_def Option.option) { Pointers.pblock = 208 208 (Types.pi1 pc.pc_block); Pointers.poff = 209 209 (bitvector_from_pos Pointers.offset_size pc_off) }) … … 215 215 216 216 (** val part_rect_Type4 : (Nat.nat > __ > 'a1) > part > 'a1 **) 217 let rec part_rect_Type4 h_mk_part x_ 6126=218 let part_no = x_ 6126in h_mk_part part_no __217 let rec part_rect_Type4 h_mk_part x_4430 = 218 let part_no = x_4430 in h_mk_part part_no __ 219 219 220 220 (** val part_rect_Type5 : (Nat.nat > __ > 'a1) > part > 'a1 **) 221 let rec part_rect_Type5 h_mk_part x_ 6128=222 let part_no = x_ 6128in h_mk_part part_no __221 let rec part_rect_Type5 h_mk_part x_4432 = 222 let part_no = x_4432 in h_mk_part part_no __ 223 223 224 224 (** val part_rect_Type3 : (Nat.nat > __ > 'a1) > part > 'a1 **) 225 let rec part_rect_Type3 h_mk_part x_ 6130=226 let part_no = x_ 6130in h_mk_part part_no __225 let rec part_rect_Type3 h_mk_part x_4434 = 226 let part_no = x_4434 in h_mk_part part_no __ 227 227 228 228 (** val part_rect_Type2 : (Nat.nat > __ > 'a1) > part > 'a1 **) 229 let rec part_rect_Type2 h_mk_part x_ 6132=230 let part_no = x_ 6132in h_mk_part part_no __229 let rec part_rect_Type2 h_mk_part x_4436 = 230 let part_no = x_4436 in h_mk_part part_no __ 231 231 232 232 (** val part_rect_Type1 : (Nat.nat > __ > 'a1) > part > 'a1 **) 233 let rec part_rect_Type1 h_mk_part x_ 6134=234 let part_no = x_ 6134in h_mk_part part_no __233 let rec part_rect_Type1 h_mk_part x_4438 = 234 let part_no = x_4438 in h_mk_part part_no __ 235 235 236 236 (** val part_rect_Type0 : (Nat.nat > __ > 'a1) > part > 'a1 **) 237 let rec part_rect_Type0 h_mk_part x_ 6136=238 let part_no = x_ 6136in h_mk_part part_no __237 let rec part_rect_Type0 h_mk_part x_4440 = 238 let part_no = x_4440 in h_mk_part part_no __ 239 239 240 240 (** val part_no : part > Nat.nat **) … … 486 486  BVundef > h_BVundef 487 487  BVnonzero > h_BVnonzero 488  BVXor (x_ 6170, x_6169, x_6168) > h_BVXor x_6170 x_6169 x_6168489  BVByte x_ 6171 > h_BVByte x_6171490  BVnull x_ 6172 > h_BVnull x_6172491  BVptr (x_ 6174, x_6173) > h_BVptr x_6174 x_6173492  BVpc (x_ 6176, x_6175) > h_BVpc x_6176 x_6175488  BVXor (x_4474, x_4473, x_4472) > h_BVXor x_4474 x_4473 x_4472 489  BVByte x_4475 > h_BVByte x_4475 490  BVnull x_4476 > h_BVnull x_4476 491  BVptr (x_4478, x_4477) > h_BVptr x_4478 x_4477 492  BVpc (x_4480, x_4479) > h_BVpc x_4480 x_4479 493 493 494 494 (** val beval_rect_Type5 : … … 500 500  BVundef > h_BVundef 501 501  BVnonzero > h_BVnonzero 502  BVXor (x_ 6187, x_6186, x_6185) > h_BVXor x_6187 x_6186 x_6185503  BVByte x_ 6188 > h_BVByte x_6188504  BVnull x_ 6189 > h_BVnull x_6189505  BVptr (x_ 6191, x_6190) > h_BVptr x_6191 x_6190506  BVpc (x_ 6193, x_6192) > h_BVpc x_6193 x_6192502  BVXor (x_4491, x_4490, x_4489) > h_BVXor x_4491 x_4490 x_4489 503  BVByte x_4492 > h_BVByte x_4492 504  BVnull x_4493 > h_BVnull x_4493 505  BVptr (x_4495, x_4494) > h_BVptr x_4495 x_4494 506  BVpc (x_4497, x_4496) > h_BVpc x_4497 x_4496 507 507 508 508 (** val beval_rect_Type3 : … … 514 514  BVundef > h_BVundef 515 515  BVnonzero > h_BVnonzero 516  BVXor (x_ 6204, x_6203, x_6202) > h_BVXor x_6204 x_6203 x_6202517  BVByte x_ 6205 > h_BVByte x_6205518  BVnull x_ 6206 > h_BVnull x_6206519  BVptr (x_ 6208, x_6207) > h_BVptr x_6208 x_6207520  BVpc (x_ 6210, x_6209) > h_BVpc x_6210 x_6209516  BVXor (x_4508, x_4507, x_4506) > h_BVXor x_4508 x_4507 x_4506 517  BVByte x_4509 > h_BVByte x_4509 518  BVnull x_4510 > h_BVnull x_4510 519  BVptr (x_4512, x_4511) > h_BVptr x_4512 x_4511 520  BVpc (x_4514, x_4513) > h_BVpc x_4514 x_4513 521 521 522 522 (** val beval_rect_Type2 : … … 528 528  BVundef > h_BVundef 529 529  BVnonzero > h_BVnonzero 530  BVXor (x_ 6221, x_6220, x_6219) > h_BVXor x_6221 x_6220 x_6219531  BVByte x_ 6222 > h_BVByte x_6222532  BVnull x_ 6223 > h_BVnull x_6223533  BVptr (x_ 6225, x_6224) > h_BVptr x_6225 x_6224534  BVpc (x_ 6227, x_6226) > h_BVpc x_6227 x_6226530  BVXor (x_4525, x_4524, x_4523) > h_BVXor x_4525 x_4524 x_4523 531  BVByte x_4526 > h_BVByte x_4526 532  BVnull x_4527 > h_BVnull x_4527 533  BVptr (x_4529, x_4528) > h_BVptr x_4529 x_4528 534  BVpc (x_4531, x_4530) > h_BVpc x_4531 x_4530 535 535 536 536 (** val beval_rect_Type1 : … … 542 542  BVundef > h_BVundef 543 543  BVnonzero > h_BVnonzero 544  BVXor (x_ 6238, x_6237, x_6236) > h_BVXor x_6238 x_6237 x_6236545  BVByte x_ 6239 > h_BVByte x_6239546  BVnull x_ 6240 > h_BVnull x_6240547  BVptr (x_ 6242, x_6241) > h_BVptr x_6242 x_6241548  BVpc (x_ 6244, x_6243) > h_BVpc x_6244 x_6243544  BVXor (x_4542, x_4541, x_4540) > h_BVXor x_4542 x_4541 x_4540 545  BVByte x_4543 > h_BVByte x_4543 546  BVnull x_4544 > h_BVnull x_4544 547  BVptr (x_4546, x_4545) > h_BVptr x_4546 x_4545 548  BVpc (x_4548, x_4547) > h_BVpc x_4548 x_4547 549 549 550 550 (** val beval_rect_Type0 : … … 556 556  BVundef > h_BVundef 557 557  BVnonzero > h_BVnonzero 558  BVXor (x_ 6255, x_6254, x_6253) > h_BVXor x_6255 x_6254 x_6253559  BVByte x_ 6256 > h_BVByte x_6256560  BVnull x_ 6257 > h_BVnull x_6257561  BVptr (x_ 6259, x_6258) > h_BVptr x_6259 x_6258562  BVpc (x_ 6261, x_6260) > h_BVpc x_6261 x_6260558  BVXor (x_4559, x_4558, x_4557) > h_BVXor x_4559 x_4558 x_4557 559  BVByte x_4560 > h_BVByte x_4560 560  BVnull x_4561 > h_BVnull x_4561 561  BVptr (x_4563, x_4562) > h_BVptr x_4563 x_4562 562  BVpc (x_4565, x_4564) > h_BVpc x_4565 x_4564 563 563 564 564 (** val beval_inv_rect_Type4 : … … 663 663 Errors.Error (List.Cons ((Errors.MSG 664 664 ErrorMessages.CorruptedPointer), List.Nil)) 665  BVptr (ptr1, p 3) >665  BVptr (ptr1, p1) > 666 666 (match bv2 with 667 667  BVundef > … … 680 680 Errors.Error (List.Cons ((Errors.MSG 681 681 ErrorMessages.CorruptedPointer), List.Nil)) 682  BVptr (ptr2, p 4) >682  BVptr (ptr2, p2) > 683 683 (match Bool.andb 684 684 (Bool.andb 685 (Bool.andb (Nat.eqb (part_no p 3) Nat.O)686 (Nat.eqb (part_no p 4) (Nat.S Nat.O)))685 (Bool.andb (Nat.eqb (part_no p1) Nat.O) 686 (Nat.eqb (part_no p2) (Nat.S Nat.O))) 687 687 (Pointers.eq_block ptr1.Pointers.pblock 688 688 ptr2.Pointers.pblock)) … … 741 741 Errors.Error (List.Cons ((Errors.MSG 742 742 ErrorMessages.CorruptedPointer), List.Nil)) 743  BVpc (ptr1, p 3) >743  BVpc (ptr1, p1) > 744 744 (match bv2 with 745 745  BVundef > … … 761 761 Errors.Error (List.Cons ((Errors.MSG 762 762 ErrorMessages.CorruptedPointer), List.Nil)) 763  BVpc (ptr2, p 4) >763  BVpc (ptr2, p2) > 764 764 (match Bool.andb 765 (Bool.andb (Nat.eqb (part_no p 3) Nat.O)766 (Nat.eqb (part_no p 4) (Nat.S Nat.O)))765 (Bool.andb (Nat.eqb (part_no p1) Nat.O) 766 (Nat.eqb (part_no p2) (Nat.S Nat.O))) 767 767 (eq_program_counter ptr1 ptr2) with 768 768  Bool.True > … … 856 856 Obj.magic (Errors.Error (List.Cons ((Errors.MSG 857 857 ErrorMessages.NotAnInt32Val), List.Nil))) 858  List.Cons (hd 0, tl) >858  List.Cons (hd, tl) > 859 859 Monad.m_bind0 (Monad.max_def Errors.res0) 860 (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd 0)) (fun b >860 (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b > 861 861 Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl })) 862 862 in … … 871 871  List.Nil > 872 872 Obj.magic (Errors.OK 873 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S873 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 874 874 (Nat.S (Nat.S Nat.O)))))))) 875 875 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 878 878 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S 879 879 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4 880 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S880 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 881 881 (Nat.S (Nat.S Nat.O)))))))) 882 882 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 883 883 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S 884 884 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3 885 (Vector.append 0(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S885 (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 886 886 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S 887 887 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1)))) … … 899 899 BitVector.bitVector > 'a1) > bebit > 'a1 **) 900 900 let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function 901  BBbit x_ 6380 > h_BBbit x_6380901  BBbit x_4684 > h_BBbit x_4684 902 902  BBundef > h_BBundef 903  BBptrcarry (x_ 6383, x_6382, p, x_6381) >904 h_BBptrcarry x_ 6383 x_6382 p x_6381903  BBptrcarry (x_4687, x_4686, p, x_4685) > 904 h_BBptrcarry x_4687 x_4686 p x_4685 905 905 906 906 (** val bebit_rect_Type5 : … … 908 908 BitVector.bitVector > 'a1) > bebit > 'a1 **) 909 909 let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function 910  BBbit x_ 6388 > h_BBbit x_6388910  BBbit x_4692 > h_BBbit x_4692 911 911  BBundef > h_BBundef 912  BBptrcarry (x_ 6391, x_6390, p, x_6389) >913 h_BBptrcarry x_ 6391 x_6390 p x_6389912  BBptrcarry (x_4695, x_4694, p, x_4693) > 913 h_BBptrcarry x_4695 x_4694 p x_4693 914 914 915 915 (** val bebit_rect_Type3 : … … 917 917 BitVector.bitVector > 'a1) > bebit > 'a1 **) 918 918 let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function 919  BBbit x_ 6396 > h_BBbit x_6396919  BBbit x_4700 > h_BBbit x_4700 920 920  BBundef > h_BBundef 921  BBptrcarry (x_ 6399, x_6398, p, x_6397) >922 h_BBptrcarry x_ 6399 x_6398 p x_6397921  BBptrcarry (x_4703, x_4702, p, x_4701) > 922 h_BBptrcarry x_4703 x_4702 p x_4701 923 923 924 924 (** val bebit_rect_Type2 : … … 926 926 BitVector.bitVector > 'a1) > bebit > 'a1 **) 927 927 let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function 928  BBbit x_ 6404 > h_BBbit x_6404928  BBbit x_4708 > h_BBbit x_4708 929 929  BBundef > h_BBundef 930  BBptrcarry (x_ 6407, x_6406, p, x_6405) >931 h_BBptrcarry x_ 6407 x_6406 p x_6405930  BBptrcarry (x_4711, x_4710, p, x_4709) > 931 h_BBptrcarry x_4711 x_4710 p x_4709 932 932 933 933 (** val bebit_rect_Type1 : … … 935 935 BitVector.bitVector > 'a1) > bebit > 'a1 **) 936 936 let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function 937  BBbit x_ 6412 > h_BBbit x_6412937  BBbit x_4716 > h_BBbit x_4716 938 938  BBundef > h_BBundef 939  BBptrcarry (x_ 6415, x_6414, p, x_6413) >940 h_BBptrcarry x_ 6415 x_6414 p x_6413939  BBptrcarry (x_4719, x_4718, p, x_4717) > 940 h_BBptrcarry x_4719 x_4718 p x_4717 941 941 942 942 (** val bebit_rect_Type0 : … … 944 944 BitVector.bitVector > 'a1) > bebit > 'a1 **) 945 945 let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function 946  BBbit x_ 6420 > h_BBbit x_6420946  BBbit x_4724 > h_BBbit x_4724 947 947  BBundef > h_BBundef 948  BBptrcarry (x_ 6423, x_6422, p, x_6421) >949 h_BBptrcarry x_ 6423 x_6422 p x_6421948  BBptrcarry (x_4727, x_4726, p, x_4725) > 949 h_BBptrcarry x_4727 x_4726 p x_4725 950 950 951 951 (** val bebit_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.