diff --git a/drivers/ocaml32.drv b/drivers/ocaml32.drv index 8db548be89c6686f8b04d6ad302a8c0a8ef84275..32d0ab920ebdde164118107b97ef0def30d92637 100644 --- a/drivers/ocaml32.drv +++ b/drivers/ocaml32.drv @@ -5,6 +5,15 @@ import "ocaml-gen.drv" +theory bv.BV32 + syntax type t "Int32.t" + syntax constant zero "0l" + syntax constant one "-1l" + syntax function bw_and "(Int32.logand %1 %2)" + syntax predicate eq "(%1 = %2)" + (* TODO ... *) +end + module mach.int.Int32 syntax val of_int "Why3__BigInt.to_int32" syntax converter of_int "%1l" @@ -24,6 +33,9 @@ module mach.int.Int32 syntax val (<) "(<)" syntax val (>=) "(>=)" syntax val (>) "(>)" + + syntax val to_bv "(fun x -> x)" + syntax val of_bv "(fun x -> x)" end module mach.int.UInt32 diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv index 55f54df529d171d09d2bbf9aa86d567701e84699..8b330b58710e02aa3e9d0f064a5cf6691f287b39 100644 --- a/drivers/ocaml64.drv +++ b/drivers/ocaml64.drv @@ -3,6 +3,10 @@ import "ocaml-gen.drv" +(* TODO bv.BV31 ? *) + +(* TODO bv.BV32 -> int or int32 ? *) + module mach.int.Int32 syntax val of_int "Why3__BigInt.to_int" syntax converter of_int "%1" @@ -60,6 +64,15 @@ module mach.int.UInt32 end +theory bv.BV63 + syntax type t "int" + syntax constant zero "0" + syntax constant one "-1" + syntax function bw_and "(%1 land %2)" + syntax predicate eq "(%1 = %2)" + (* TODO ... *) +end + module mach.int.Int63 syntax val of_int "Why3__BigInt.to_int" syntax converter of_int "%1" @@ -79,8 +92,13 @@ module mach.int.Int63 syntax val (<) "(<)" syntax val (>=) "(>=)" syntax val (>) "(>)" + + syntax val to_bv "(fun x -> x)" + syntax val of_bv "(fun x -> x)" end +(* TODO bv.BV64 -> int64 *) + module mach.int.Int64 syntax val of_int "Why3__BigInt.to_int64" syntax converter of_int "%1L" diff --git a/examples/tests/bitvector-test.why b/examples/tests/bitvector-test.why index cc27a0a36f9c4650341c5a5f6164dc064536a8a1..5c4a171a3c59ecabaa6ff507f130b7e1eb705c66 100644 --- a/examples/tests/bitvector-test.why +++ b/examples/tests/bitvector-test.why @@ -1,25 +1,25 @@ theory TestBv32 - use import map.BV32 + use import bv.BV32 lemma Test1: - let b = bw_and bvzero bvone in nth b 1 = False + let b = bw_and zero one in nth b 1 = False lemma Test2: - let b = lsr bvone 16 in nth b 15 = True + let b = lsr one 16 in nth b 15 = True lemma Test3: - let b = lsr bvone 16 in nth b 16 = False + let b = lsr one 16 in nth b 16 = False lemma Test4: - let b = asr bvone 16 in nth b 15 = True + let b = asr one 16 in nth b 15 = True lemma Test5: - let b = asr bvone 16 in nth b 16 = True + let b = asr one 16 in nth b 16 = True lemma Test6: - let b = asr (lsr bvone 1) 16 in nth b 16 = False + let b = asr (lsr one 1) 16 in nth b 16 = False end diff --git a/examples/tests/int32-test.mlw b/examples/tests/int32-test.mlw new file mode 100644 index 0000000000000000000000000000000000000000..5c7662914b365e5bc7ed1bddf9a65690ac8730c7 --- /dev/null +++ b/examples/tests/int32-test.mlw @@ -0,0 +1,11 @@ + +module TestInt32 + + use import mach.int.Int32 + + let mask_111 (x: int32) : int32 + ensures { 0 <= to_int result < 8 } + = + of_bv (BV32.bw_and (to_bv x) (BV32.of_int 7)) + +end diff --git a/modules/mach/int.mlw b/modules/mach/int.mlw index 8e6dae751db2b6d2e75173b5f8242382a4b623d0..4874d8f60c0e2d637cccb2b3ba128138a3322084 100644 --- a/modules/mach/int.mlw +++ b/modules/mach/int.mlw @@ -149,6 +149,13 @@ module Int31 constant min = min_int31, constant max = max_int31 + use bv.BV31 + + val to_bv (x: int31) : BV31.t + ensures { BV31.to_int result = to_int x } + val of_bv (x: BV31.t) : int31 + ensures { to_int result = BV31.to_int x } + end module Int32 @@ -165,6 +172,13 @@ module Int32 constant min = min_int32, constant max = max_int32 + use bv.BV32 + + val to_bv (x: int32) : BV32.t + ensures { BV32.to_int result = to_int x } + val of_bv (x: BV32.t) : int32 + ensures { to_int result = BV32.to_int x } + end module UInt32 @@ -177,6 +191,13 @@ module UInt32 type t = uint32, constant max = max_uint32 + use bv.BV32 + + val to_bv (x: uint32) : BV32.t + ensures { BV32.to_uint result = to_int x } + val of_bv (x: BV32.t) : uint32 + ensures { to_int result = BV32.to_uint x } + end module Int63 @@ -193,6 +214,13 @@ module Int63 constant min = min_int63, constant max = max_int63 + use bv.BV63 + + val to_bv (x: int63) : BV63.t + ensures { BV63.to_int result = to_int x } + val of_bv (x: BV63.t) : int63 + ensures { to_int result = BV63.to_int x } + end module Int64 @@ -209,6 +237,13 @@ module Int64 constant min = min_int64, constant max = max_int64 + use bv.BV64 + + val to_bv (x: int64) : BV64.t + ensures { BV64.to_int result = to_int x } + val of_bv (x: BV64.t) : int64 + ensures { to_int result = BV64.to_int x } + end module UInt64 @@ -223,4 +258,11 @@ module UInt64 type t = uint64, constant max = max_uint64 + use bv.BV64 + + val to_bv (x: uint64) : BV64.t + ensures { BV64.to_uint result = to_int x } + val of_bv (x: BV64.t) : uint64 + ensures { to_int result = BV64.to_uint x } + end diff --git a/theories/bv.why b/theories/bv.why new file mode 100644 index 0000000000000000000000000000000000000000..be57a5928d8737d9cfea83bddd45b17c96f18ea9 --- /dev/null +++ b/theories/bv.why @@ -0,0 +1,104 @@ + +(** {1 Bit vectors} *) + +(** {2 Generic theory (arbitrary length)} *) + +theory BitVector + + use export bool.Bool + use import int.Int + + constant size : int + + axiom size_pos: size > 0 + + type t + + function nth t int: bool + + constant zero : t + axiom Nth_zero: + forall n:int. 0 <= n < size -> nth zero n = False + + constant one : t + axiom Nth_one: + forall n:int. 0 <= n < size -> nth one n = True + + predicate eq (v1 v2 : t) = + forall n:int. 0 <= n < size -> nth v1 n = nth v2 n + + function bw_and (v1 v2 : t) : t + axiom Nth_bw_and: + forall v1 v2:t, n:int. 0 <= n < size -> + nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n) + + (** logical shift right *) + function lsr t int : t + + axiom Lsr_nth_low: + forall b:t,n s:int. 0 <= n+s < size -> nth (lsr b s) n = nth b (n+s) + + axiom Lsr_nth_high: + forall b:t,n s:int. n+s >= size -> nth (lsr b s) n = False + + (** arithmetic shift right *) + function asr t int : t + + axiom Asr_nth_low: + forall b:t,n s:int. 0 <= n+s < size -> nth (asr b s) n = nth b (n+s) + + axiom Asr_nth_high: + forall b:t,n s:int. n+s >= size -> nth (asr b s) n = nth b (size-1) + + (** logical shift left *) + function lsl t int : t + + axiom Lsl_nth_high: + forall b:t,n s:int. 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s) + + axiom Lsl_nth_low: + forall b:t,n s:int. n-s < 0 -> nth (lsl b s) n = False + + function to_int t: int + + (* TODO? axiom - power 2 (size-1) <= to_int b < power 2 (size-1) *) + + function to_uint t: int + + (* TODO? axiom 0 <= to_int b < power 2 size *) + + function of_int int: t + + (* TODO? axioms related to_int/to_unit and of_int *) + +end + +(** {2 31-bits Bitvectors} *) + +theory BV31 + constant size: int = 31 + clone export BitVector with constant size = size, goal size_pos +end + +(** {2 32-bits Bitvectors} *) + +theory BV32 + constant size: int = 32 + clone export BitVector with constant size = size, goal size_pos +end + +(** {2 63-bits Bitvectors} *) + +theory BV63 + constant size: int = 63 + clone export BitVector with constant size = size, goal size_pos +end + +(** {2 64-bits Bitvectors} *) + +theory BV64 + constant size: int = 64 + clone export BitVector with constant size = size, goal size_pos +end + + diff --git a/theories/map.why b/theories/map.why index 960c672b55d80205e7acc9a9e56858c25c79c47b..1420cce9e9c4e7b6db1a887c5a28e5146a94975c 100644 --- a/theories/map.why +++ b/theories/map.why @@ -92,79 +92,6 @@ theory MapSum end -(** {2 Bitvectors (arbitrary length)} - -Seen as maps from int to bool - -*) - -theory BitVector - - use export bool.Bool - use import int.Int - - constant size : int - - type bv - - function nth bv int: bool - - constant bvzero : bv - axiom Nth_zero: - forall n:int. 0 <= n < size -> nth bvzero n = False - - constant bvone : bv - axiom Nth_one: - forall n:int. 0 <= n < size -> nth bvone n = True - - predicate eq (v1 v2 : bv) = - forall n:int. 0 <= n < size -> nth v1 n = nth v2 n - - function bw_and (v1 v2 : bv) : bv - axiom Nth_bw_and: - forall v1 v2:bv, n:int. 0 <= n < size -> - nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n) - - (** logical shift right *) - function lsr bv int : bv - - axiom Lsr_nth_low: - forall b:bv,n s:int. 0 <= n+s < size -> nth (lsr b s) n = nth b (n+s) - - axiom Lsr_nth_high: - forall b:bv,n s:int. n+s >= size -> nth (lsr b s) n = False - - (** arithmetic shift right *) - function asr bv int : bv - - axiom Asr_nth_low: - forall b:bv,n s:int. 0 <= n+s < size -> nth (asr b s) n = nth b (n+s) - - axiom Asr_nth_high: - forall b:bv,n s:int. n+s >= size -> nth (asr b s) n = nth b (size-1) - - (** logical shift left *) - function lsl bv int : bv - - axiom Lsl_nth_high: - forall b:bv,n s:int. 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s) - - axiom Lsl_nth_low: - forall b:bv,n s:int. n-s < 0 -> nth (lsl b s) n = False - -end - -(** {2 32-bits Bitvectors} *) - -theory BV32 - - constant size : int = 32 - - clone export BitVector with constant size = size - -end - - (** {2 Number of occurrences} *) theory Occ