Why3 Standard Library index

# Program functions on bitvectors with preconditions

This module provides extra functions with pre-conditions ensuring the absence of overflows.

Those pre-conditions are expressed in term of interpretation into mathematical integers. It is not ideal since conversion to integers is typically poorly supported bit-vectors built-in in SMT solvers. A better solution in the future would be to express those pre-conditions is purely bit-vector logic formulas. An insight on how this could be could can be found in the book Hacker's Delight [Section 2-13, Overflow detection].

Another note for the future: it might be better to introduce two separate modules for signed operation and unsigned operations.

## Generic module, for a parametric size

```module BVCheck_Gen
use int.Int

type t

constant size : int

constant two_power_size : int
constant two_power_size_minus_one : int
constant zeros           : t
constant minus_one : t
constant min_sint : t

function to_uint t   : int
function to_int t   : int
function of_int  int : t

function add  t t : t
function sub  t t : t
function mul  t t : t
function udiv t t : t
function urem t t : t
function sdiv t t : t
function srem t t : t

function lsl    t int : t
function lsl_bv t t   : t
function lsr    t int : t
function lsr_bv t t   : t
function asr    t int : t
function asr_bv t t   : t

predicate ule t t
predicate ult t t
predicate uge t t
predicate ugt t t

predicate sle t t
predicate slt t t
predicate sge t t
predicate sgt t t

```

addition for overflow check

```  val uadd_check (a b:t) : t
requires { [@expl:arithmetic overflow] 0 <= to_uint a + to_uint b < two_power_size }
ensures  { to_uint result = to_uint a + to_uint b }
ensures  { result = add a b }

val sadd_check (a b:t) : t
requires { [@expl:arithmetic overflow]
- two_power_size_minus_one <= to_int a + to_int b < two_power_size_minus_one }
ensures  { to_int result = to_int a + to_int b }
ensures  { result = add a b }

val usub_check (a b:t) : t
requires { [@expl:arithmetic overflow] 0 <= to_uint a - to_uint b < two_power_size }
ensures  { result = sub a b }
ensures  { to_uint result = to_uint a - to_uint b }
```

subtraction with overflow check

```  val ssub_check (a b:t) : t
requires { [@expl:arithmetic overflow]
- two_power_size_minus_one <= to_int a - to_int b < two_power_size_minus_one }
ensures  { result = sub a b }
ensures  { to_int result = to_int a - to_int b }

val umul_check (a b:t) : t
requires { [@expl:arithmetic overflow] 0 <= to_uint a * to_uint b < two_power_size }
ensures  { result = mul a b }
ensures  { to_int result = to_uint a * to_uint b }
```

multiplication with overflow check

```  val smul_check (a b:t) : t
requires { [@expl:arithmetic overflow]
- two_power_size_minus_one <= to_int a * to_int b < two_power_size_minus_one }
ensures  { result = mul a b }
ensures  { to_int result = to_int a * to_int b }

val lsl_check (a b:t) : t
requires { [@expl:out-of-bounds shifting] 0 <= to_uint b < size }
ensures  { result = lsl_bv a b }
ensures  { result = lsl a (to_uint b) }
```

logical shift left requires the second argument to be smaller than bitvector size

```  val lsr_check (a b:t) : t
requires { [@expl:out-of-bounds shifting] 0 <= to_uint b < size }
ensures  { result = lsr_bv a b }
ensures  { result = lsr a (to_uint b) }
```

logical shift right requires the second argument to be smaller than bitvector size

```  val asr_check (a b:t) : t
requires { [@expl:out-of-bounds shifting] 0 <= to_uint b < size }
ensures  { result = asr_bv a b }
ensures  { result = asr a (to_uint b) }
```

arithmetic shift right requires the second argument to be smaller than bitvector size

```  use int.EuclideanDivision as ED

val udiv_check (a b:t) : t
requires { [@expl:division by zero] b <> zeros}
ensures  { to_uint result = ED.div (to_uint a) (to_uint b) }
ensures  { result = udiv a b }
```

unsigned division requires the second argument to be non-zero

```  val urem_check (a b:t) : t
requires { [@expl:remainder by zero] b <> zeros}
ensures  { to_uint result = ED.mod (to_uint a) (to_uint b) }
ensures  { result = urem a b }
```

unsigned remainder requires the second argument to be non-zero

```  use int.ComputerDivision as CD

val sdiv_check (a b:t) : t
requires { [@expl:division by zero] b <> zeros}
requires { [@expl:signed division overflow check] a <> min_sint \/ b <> minus_one}
ensures  { to_int result = CD.div (to_int a) (to_int b) }
ensures  { result = sdiv a b }
```

signed division requires the second argument to be non-zero, but also that either the dividend is not min_int or the divisor is not -1

```  val srem_check (a b:t) : t
requires { [@expl:remainder by zero] b <> zeros}
ensures  { to_int result = CD.mod (to_int a) (to_int b) }
ensures  { result = srem a b }
```

unsigned remainder requires the second argument to be non-zero

```  val eq_check (a b:t) : bool
ensures { result <-> a = b }
```

comparison operators have no preconditions

```  val ne_check (a b:t) : bool
ensures { result <-> a <> b }

val ule_check (a b:t) : bool
ensures { result <-> to_uint a <= to_uint b }
ensures { result <-> ule a b }

val ult_check (a b:t) : bool
ensures { result <-> to_uint a < to_uint b }
ensures { result <-> ult a b }

val uge_check (a b:t) : bool
ensures { result <-> to_uint a >= to_uint b }
ensures { result <-> uge a b }

val ugt_check (a b:t) : bool
ensures { result <-> to_uint a > to_uint b }
ensures { result <-> ugt a b }

val sle_check (a b:t) : bool
ensures { result <-> to_int a <= to_int b }
ensures { result <-> sle a b }

val slt_check (a b:t) : bool
ensures { result <-> to_int a < to_int b }
ensures { result <-> slt a b }

val sge_check (a b:t) : bool
ensures { result <-> to_int a >= to_int b }
ensures { result <-> sge a b }

val sgt_check (a b:t) : bool
ensures { result <-> to_int a > to_int b }
ensures { result <-> sgt a b }

end

```

## Modules for specific sizes

obtained by cloning the previous generic module

```module BVCheck8
use export bv.BV8

constant two_power_size_minus_one : int = 0x80
constant minus_one : t = 0xFF
constant min_sint : t = 0x80

clone export BVCheck_Gen with
type t = t,
constant size = size,
function two_power_size = two_power_size,
function two_power_size_minus_one = two_power_size_minus_one,
function zeros = zeros,
function minus_one = minus_one,
function min_sint = min_sint,
function to_uint = t'int,
function to_int = to_int,
function of_int = of_int,
function add = add,
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem,
function sdiv = sdiv,
function srem = srem,
function lsl = lsl,
function lsl_bv = lsl_bv,
function lsr = lsr,
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt,
predicate sle = sle,
predicate slt = slt,
predicate sge = sge,
predicate sgt = sgt
end

module BVCheck16
use export bv.BV16

constant two_power_size_minus_one : int = 0x8000
constant minus_one : t = 0xFFFF
constant min_sint : t = 0x8000

clone export BVCheck_Gen with
type t = t,
constant size = size,
function two_power_size = two_power_size,
function two_power_size_minus_one = two_power_size_minus_one,
function zeros = zeros,
function minus_one = minus_one,
function min_sint = min_sint,
function to_uint = t'int,
function to_int = to_int,
function of_int = of_int,
function add = add,
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem,
function sdiv = sdiv,
function srem = srem,
function lsl = lsl,
function lsl_bv = lsl_bv,
function lsr = lsr,
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt,
predicate sle = sle,
predicate slt = slt,
predicate sge = sge,
predicate sgt = sgt
end

module BVCheck32
use export bv.BV32

constant two_power_size_minus_one : int = 0x8000_0000
constant minus_one : t = 0xFFFF_FFFF
constant min_sint : t = 0x8000_0000

clone export BVCheck_Gen with
type t = t,
constant size = size,
function two_power_size = two_power_size,
function two_power_size_minus_one = two_power_size_minus_one,
function zeros = zeros,
function minus_one = minus_one,
function min_sint = min_sint,
function to_uint = t'int,
function to_int = to_int,
function of_int = of_int,
function add = add,
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem,
function sdiv = sdiv,
function srem = srem,
function lsl = lsl,
function lsl_bv = lsl_bv,
function lsr = lsr,
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt,
predicate sle = sle,
predicate slt = slt,
predicate sge = sge,
predicate sgt = sgt
end

module BVCheck64
use export bv.BV64

constant two_power_size_minus_one : int = 0x8000_0000_0000_0000
constant minus_one : t = 0xFFFF_FFFF_FFFF_FFFF
constant min_sint : t = 0x8000_0000_0000_0000

clone export BVCheck_Gen with
type t = t,
constant size = size,
function two_power_size = two_power_size,
function two_power_size_minus_one = two_power_size_minus_one,
function zeros = zeros,
function minus_one = minus_one,
function min_sint = min_sint,
function to_uint = t'int,
function to_int = to_int,
function of_int = of_int,
function add = add,
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem,
function sdiv = sdiv,
function srem = srem,
function lsl = lsl,
function lsl_bv = lsl_bv,
function lsr = lsr,
function lsr_bv = lsr_bv,
function asr = asr,
function asr_bv = asr_bv,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt,
predicate sle = sle,
predicate slt = slt,
predicate sge = sge,
predicate sgt = sgt
end
```

Generated by why3doc 1.4.0