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