bit vectors (WIP)

moved from map.why to bv.why + new theories BV31, BV63, and BV64
modules mach.int.Int32 etc. now have to_bv / of_bv routines
ocaml driver identify integers and bit vectors and makes use of
operations such as land

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

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"

examples/tests/bitvector-test.why

 
 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
 

examples/tests/int32-test.mlw

+
+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

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

theories/bv.why

+
+(** {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
+
+

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