Why3 Standard Library index

Program functions on bitvectors with preconditions

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

Generic module, for a parametric size

module BVCheck_Gen
  use int.Int

  type t

  constant size : int
  constant size_bv : t

  constant two_power_size : int
  constant two_power_sizem1 : int
  constant zeros           : t
  constant minus_one : 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 neg  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

  constant min_sint : t
  constant max_sint : t
  constant max_uint : t

  predicate u_add_o t t
  predicate s_add_o t t
  predicate u_sub_o t t
  predicate s_sub_o t t
  predicate u_mul_o t t
  predicate s_mul_o t t
  predicate s_neg_o t
  predicate s_div_o t t

  val u_add (a b:t) : t
    requires { [@expl:unsigned addition overflow] not (u_add_o a b) }
    ensures  { to_uint result = to_uint a + to_uint b }
    ensures  { result = add a b }

unsigned addition forbidding overflows

  val s_add (a b:t) : t
    requires { [@expl:signed addition overflow] not (s_add_o a b) }
    ensures  { to_int result = to_int a + to_int b }
    ensures  { result = add a b }

signed addition forbidding overflows

  val u_sub (a b:t) : t
    requires { [@expl:unsigned subtraction overflow] not (u_sub_o a b) }
    ensures  { result = sub a b }
    ensures  { to_uint result = to_uint a - to_uint b }

unsigned subtraction with overflow check

  val s_sub (a b:t) : t
    requires { [@expl:signed subtraction overflow] not (s_sub_o a b) }
    ensures  { result = sub a b }
    ensures  { to_int result = to_int a - to_int b }

signed subtraction with overflow check

  val u_mul (a b:t) : t
    requires { [@expl:unsigned multiplication overflow] not (u_mul_o a b) }
    ensures  { result = mul a b }
    ensures  { to_uint result = to_uint a * to_uint b }

unsigned multiplication with overflow check

  val s_mul (a b:t) : t
    requires { [@expl:signed multiplication overflow] not (s_mul_o a b) }
    ensures  { result = mul a b }
    ensures  { to_int result = to_int a * to_int b }

signed multiplication with overflow check

  val s_neg (a:t) : t
    requires { [@expl:negation overflow] not (s_neg_o a) }
    ensures  { result = neg a }
    ensures  { to_int result = - to_int a }

signed negation with overflow check

remark: there is no such thing as unsigned negation'' 

  use bv.Pow2int

  val u_lsl (a b:t) : t
    requires { [@expl:out-of-bounds shifting] ult b size_bv }
    ensures  { result = lsl_bv a b }
    ensures  { result = lsl a (to_uint b) }

A logical shift left requiring the second argument to be smaller than bitvector size. For this function we do not forbid overflow: bits can be lost'' on the left. This function corresponds to the left shifting [<<] of unsigned ints in C or Java 

  val s_lsl (a b:t) : t
    requires { [@expl:out-of-bounds shifting] ult b size_bv }
    requires { [@expl:out-of-bounds shifting] sle zeros a }
    requires { [@expl:arithmetic overflow]
               (to_int a) * (pow2 (to_int b)) < two_power_sizem1
             }
    ensures  { result = lsl_bv a b }
    ensures  { result = lsl a (to_uint b) }

Alternative logical shift left, still requiring the second argument to be smaller than bitvector size, but also forbidding overflow. This function corresponds to the left shifting [<<] of signed ints in C or Java

  val u_lsr (a b:t) : t
    requires { [@expl:out-of-bounds shifting] ult b size_bv }
    ensures  { result = lsr_bv a b }
    ensures  { result = lsr a (to_uint b) }

Logical shift right, requiring the second argument to be smaller than bitvector size. No overflow can occur anyway. This function corresponds to the (logical) right shifting [>>] of unsigned ints in C or Java.

  val s_asr (a b:t) : t
    requires { [@expl:out-of-bounds shifting] ult b size_bv }
    ensures  { result = asr_bv a b }
    ensures  { result = asr a (to_uint b) }

The so-called "arithmetic" shift right, requirings the second argument to be smaller than bitvector size. This function corresponds to the arithmetic right shifting [>>>] of signed ints in Java, that does not exist in C.

  val s_asr_strict (a b:t) : t
    requires { [@expl:out-of-bounds shifting] ult b size_bv }
    requires { [@expl:out-of-bounds shifting] sge a zeros }
    ensures  { result = asr_bv a b }
    ensures  { result = asr a (to_uint b) }

The shift right function for signed int, requirings the second argument to be smaller than bitvector size, and that the first argument in non-negative. This function corresponds to the right shifting [>>] of signed ints in C.

  use int.EuclideanDivision as ED

  val u_div (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 u_rem (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 s_div (a b:t) : t
    requires { [@expl:division by zero] b <> zeros }
    requires { [@expl:signed division overflow check] not (s_div_o a b) }
    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 s_rem (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 }

signed remainder requires the second argument to be non-zero

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

comparison operators have no preconditions

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

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

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

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

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

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

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

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

  val s_gt (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

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

  use bv.BV16 as BV16
  use bv.BVConverter_8_16 as C

  clone bv.BV_overflow_defs with
    type t = t,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    predicate uge = uge,
    type tBig = BV16.t,
    function sto_big = C.stoBig,
    function uto_big = C.toBig,
    predicate ule = BV16.ule,
    predicate sle = BV16.sle,
    function add = BV16.add,
    function sub = BV16.sub,
    function mul = BV16.mul

end

module BVCheck16
  use export bv.BV16

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

  use bv.BV32 as BV32
  use bv.BVConverter_16_32 as C

  clone bv.BV_overflow_defs with
    type t = t,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    predicate uge = uge,
    type tBig = BV32.t,
    function sto_big = C.stoBig,
    function uto_big = C.toBig,
    predicate ule = BV32.ule,
    predicate sle = BV32.sle,
    function add = BV32.add,
    function sub = BV32.sub,
    function mul = BV32.mul

end

module BVCheck32
  use export bv.BV32

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

  use bv.BV64 as BV64
  use bv.BVConverter_32_64 as C

  clone bv.BV_overflow_defs with
    type t = t,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    predicate uge = uge,
    type tBig = BV64.t,
    function sto_big = C.stoBig,
    function uto_big = C.toBig,
    predicate ule = BV64.ule,
    predicate sle = BV64.sle,
    function add = BV64.add,
    function sub = BV64.sub,
    function mul = BV64.mul

end

module BVCheck64
  use export bv.BV64

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

  use bv.BV128 as BV128
  use bv.BVConverter_64_128 as C

  clone bv.BV_overflow_defs with
    type t = t,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    predicate uge = uge,
    type tBig = BV128.t,
    function sto_big = C.stoBig,
    function uto_big = C.toBig,
    predicate ule = BV128.ule,
    predicate sle = BV128.sle,
    function add = BV128.add,
    function sub = BV128.sub,
    function mul = BV128.mul

end

(* not ready

module BVCheck128
  use export bv.BV128

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

end


module BVCheck256
  use export bv.BV256

  clone export BVCheck_Gen with
    type t = t,
    constant size = size,
    constant size_bv = size_bv,
    function two_power_size = two_power_size,
    function two_power_sizem1 = two_power_sizem1,
    function zeros = zeros,
    function minus_one = minus_one,
    function min_sint = min_sint,
    function max_sint = max_sint,
    function max_uint = max_uint,
    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 neg = neg,
    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,
    predicate u_add_o = u_add_o,
    predicate s_add_o = s_add_o,
    predicate u_sub_o = u_sub_o,
    predicate s_sub_o = s_sub_o,
    predicate u_mul_o = u_mul_o,
    predicate s_mul_o = s_mul_o,
    predicate s_neg_o = s_neg_o,
    predicate s_div_o = s_div_o

end

*)

Generated by why3doc 1.9.0+git