improved bitvectors + examples

drivers/cvc4_bare.drv

@@ -187,25 +187,30 @@ theory bv.BV32
   syntax type t "(_ BitVec 32)"
 
   syntax function zero "#x00000000"
-  syntax function one  "#xFFFFFFFF"
+  syntax function ones "#xFFFFFFFF"
   syntax function bw_and "(bvand %1 %2)"
   syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
 
   syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
   syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
   syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
   syntax function to_uint "(bv2nat %1)"
-  syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0) 
-  	 	  	       (bv2nat %1) 
-			       (-(bv2nat %1) 4294967296) )"
+  syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0)
+  	 	  	       (bv2nat %1)
+			       (- (bv2nat %1) 4294967296))"
   syntax function of_int "((_ int2bv 32) %1)"
-  syntax function nth "(= (bvand (bvlshr %1 ((_ int2bv 32) %2)) #x00000001)
-  	 	      	  #x00000001)"			  
+  syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2)))
+  	 	      	  #b1)"
   syntax predicate eq "(= %1 %2)"
 
   remove prop Nth_zero
-  remove prop Nth_one
+  remove prop Nth_ones
   remove prop Nth_bw_and
+  remove prop Nth_bw_or
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
   remove prop Lsr_nth_low
   remove prop Lsr_nth_high
   remove prop Lsl_nth_low

drivers/ocaml32.drv

@@ -8,7 +8,7 @@ import "ocaml-gen.drv"
 theory bv.BV32
   syntax type      t      "Int32.t"
   syntax constant  zero   "0l"
-  syntax constant  one    "-1l"
+  syntax constant  ones    "-1l"
   syntax function  bw_and "(Int32.logand %1 %2)"
   syntax predicate eq     "(%1 = %2)"
   (* TODO ... *)

drivers/ocaml64.drv

@@ -67,7 +67,7 @@ end
 theory bv.BV63
   syntax type      t      "int"
   syntax constant  zero   "0"
-  syntax constant  one    "-1"
+  syntax constant  ones    "-1"
   syntax function  bw_and "(%1 land %2)"
   syntax predicate eq     "(%1 = %2)"
   (* TODO ... *)

examples/in_progress/hacker.mlw

+
+module Delight
+
+  use import mach.int.Int32
+  use import int.EuclideanDivision
+
+  let f (x y:int32) (ghost k:int) : int32
+    requires { 0 <= k < 1 }
+    requires { to_int y = BV32.to_int (BV32.lsl (BV32.of_int 1) k) }
+    ensures { 0 <= to_int result < to_int y }
+    ensures { to_int result = mod (to_int x) (to_int y) } 
+  = assert { to_int y = 1 };
+    of_bv (BV32.bw_and (to_bv x) (to_bv (y - of_int 1)))
+
+end

examples/logic/bitvectors.why

+
+theory TestBV
+
+  use import int.Int
+  use import bv.BV32
+
+  constant b0000 : t = of_int 0b0000
+  constant b0001 : t = of_int 0b0001
+  constant b0010 : t = of_int 0b0010
+  constant b0011 : t = of_int 0b0011
+  constant b0110 : t = of_int 0b0110
+  constant b0101 : t = of_int 0b0101
+  constant b0111 : t = of_int 0b0111
+  constant b1100 : t = of_int 0b1100
+  constant b11100 : t = of_int 0b11100
+
+  goal g1 : bw_and b0011 b0110 = b0010
+  goal f1 : bw_and b0011 b0110 = b0011
+
+  goal g2 :  bw_or b0011 b0110 = b0111
+  goal f2 :  bw_or b0011 b0110 = b0110
+
+  goal g3 :  bw_xor b0011 b0110 = b0101
+  goal g4 :  bw_not b0011 = (of_int 0xFFFFFFFC)
+
+  goal g3a : lsr b0111 2 = b0001
+  goal g3b : lsr ones 31 = b0001
+  goal g3c : lsr ones 0x100000001 = (of_int 0x7FFFFFFF)
+
+  goal g4a : lsl b0111 2 = b11100
+  goal g4b : lsl b0001 31 = (of_int 0x80000000)
+
+  goal g5a : asr b0111 2 = b0001
+  goal g5b : asr ones 31 = ones
+
+  goal g6a : to_uint b11100 = 28
+  goal g6b : to_uint ones = 0xFFFFFFFF
+
+  goal g7a : to_int b11100 = 28
+  goal g7b : to_int ones = -1
+
+  goal g8a : nth b0110 2 = True
+  goal g8b : nth b0110 3 = False
+
+
+  goal 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)
+
+  goal Nth_bw_or:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
+
+  goal Nth_bw_xor:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
+
+  goal Nth_bw_not:
+    forall v:t, n:int. 0 <= n < size ->
+      nth (bw_not v) n = notb (nth v n)
+
+
+  goal not_not : forall v:t. bw_not (bw_not v) = v
+
+  goal not_and : forall v1 v2:t.
+    bw_not (bw_and v1 v2) = bw_or (bw_not v1) (bw_not v2)
+
+  goal Lsr_nth_low:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s < size -> 
+      nth (lsr b s) n = nth b (n+s)
+
+  goal Lsr_nth_high:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size -> 
+      nth (lsr b s) n = False
+
+  goal Asr_nth_low:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 0 <= n+s < size -> nth (asr b s) n = nth b (n+s)
+
+  goal Asr_nth_high:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size -> nth (asr b s) n = nth b (size-1)
+
+  goal Lsl_nth_high:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 0 <= n-s < size -> nth (lsl b s) n = nth b (n-s)
+
+  goal Lsl_nth_low:
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n-s < 0 -> nth (lsl b s) n = False
+
+
+end

examples/logic/bitvectors/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
+<file name="../bitvectors.why" expanded="true">
+<theory name="TestBV" sum="6c8cf1f3af56cc427b7e569fc12908c2" expanded="true">
+ <goal name="g1">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="f1">
+ <proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
+ </goal>
+ <goal name="g2">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="f2">
+ <proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
+ </goal>
+ <goal name="g3">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g4">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g3a">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g3b">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g3c">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g4a">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g4b">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g5a">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g5b">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g6a">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g6b">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="g7a">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g7b">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g8a">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="g8b">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="Nth_bw_and">
+ <proof prover="1"><result status="valid" time="0.16"/></proof>
+ </goal>
+ <goal name="Nth_bw_or">
+ <proof prover="1"><result status="valid" time="0.16"/></proof>
+ </goal>
+ <goal name="Nth_bw_xor">
+ <proof prover="1"><result status="valid" time="0.17"/></proof>
+ </goal>
+ <goal name="Nth_bw_not">
+ <proof prover="1" edited="bitvectors-TestBV-Nth_bw_not_1.smt2"><result status="valid" time="1.32"/></proof>
+ </goal>
+ <goal name="not_not">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="not_and">
+ <proof prover="1"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="Lsr_nth_low">
+ <proof prover="1" timelimit="98"><result status="valid" time="62.42"/></proof>
+ </goal>
+ <goal name="Lsr_nth_high">
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" timelimit="98"><result status="valid" time="7.81"/></proof>
+ </goal>
+ <goal name="Asr_nth_low">
+ <proof prover="1" timelimit="98"><result status="valid" time="72.85"/></proof>
+ </goal>
+ <goal name="Asr_nth_high">
+ <proof prover="1" timelimit="98"><result status="valid" time="8.10"/></proof>
+ </goal>
+ <goal name="Lsl_nth_high">
+ <proof prover="1" timelimit="98"><result status="valid" time="58.83"/></proof>
+ </goal>
+ <goal name="Lsl_nth_low">
+ <proof prover="1" timelimit="98"><result status="valid" time="7.64"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>

examples/tests/bitvector-test.why

@@ -4,22 +4,22 @@ theory TestBv32
   use import bv.BV32
 
   lemma Test1:
-    let b = bw_and zero one in nth b 1 = False
+    let b = bw_and zero ones in nth b 1 = False
 
   lemma Test2:
-    let b = lsr one 16 in nth b 15 = True
+    let b = lsr ones 16 in nth b 15 = True
 
   lemma Test3:
-    let b = lsr one 16 in nth b 16 = False
+    let b = lsr ones 16 in nth b 16 = False
 
   lemma Test4:
-    let b = asr one 16 in nth b 15 = True
+    let b = asr ones 16 in nth b 15 = True
 
   lemma Test5:
-    let b = asr one 16 in nth b 16 = True
+    let b = asr ones 16 in nth b 16 = True
 
   lemma Test6:
-    let b = asr (lsr one 1) 16 in nth b 16 = False
+    let b = asr (lsr ones 1) 16 in nth b 16 = False
 
 end
 

theories/bv.why

@@ -10,22 +10,27 @@ theory BitVector
 
   constant size : int
 
+  (* useful ? *)
   axiom size_pos: size > 0
 
   type t
 
   function nth t int: bool
+  (** [nth b n] is the n-th bit of x (0 <= n < size). bit 0 is
+      the least significant bit *)
+
+  predicate eq (v1 v2 : t) =
+    forall n:int. 0 <= n < size -> nth v1 n = nth v2 n
+
+  axiom Extensionality: forall x y : t. eq x y -> x = y
 
   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
+  constant ones : t
+  axiom Nth_ones:
+    forall n:int. 0 <= n < size -> nth ones n = True
 
   function bw_and (v1 v2 : t) : t
   axiom Nth_bw_and:
@@ -37,41 +42,58 @@ theory BitVector
     forall v1 v2:t, n:int. 0 <= n < size ->
       nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
 
+  function bw_xor (v1 v2 : t) : t
+  axiom Nth_bw_xor:
+    forall v1 v2:t, n:int. 0 <= n < size ->
+      nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
+
+  function bw_not (v : t) : t
+  axiom Nth_bw_not:
+    forall v:t, n:int. 0 <= n < size ->
+      nth (bw_not v) n = notb (nth v 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)
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 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
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 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)
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 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)
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 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)
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> 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) *)
+    forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n-s < 0 -> nth (lsl b s) n = False
 
+  (** conversion to unsigned integers *)
   function to_uint t: int
 
   (* TODO? axiom 0 <= to_int b < power 2 size *)
 
+  (** conversion to signed integers *)
+  function to_int t: int
+
+  (* TODO? axiom - power 2 (size-1) <= to_int b < power 2 (size-1) *)
+
+  (** conversion from integers. The (infinitary) 2-complement binary
+  representation of the argument is truncated to [size] bits *)
   function of_int int: t
 
   (* TODO? axioms related to_int/to_unit and of_int *)