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, or using bitvectors of size 128.

Generic module, for a parametric size

module BVCheck_Gen
  use int.Int

  type t

  constant size : int
  constant size_bv : t

  (* Overflow checks are performed using bitvectors of size 128. Thus
     this module cannot be cloned with a [size] > 64. *)
  axiom not_greater_than_64 : size <= 64

  constant two_power_size : int
  constant two_power_size_minus_one : 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 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

  use bv.BV128 as BV128

  function sto_bv128 t : BV128.t
  function uto_bv128 t : BV128.t

  constant min_sint : t
  constant max_sint : t
  constant max_uint : t
  constant min_sint_as_bv128 : BV128.t = sto_bv128 min_sint
  constant max_sint_as_bv128 : BV128.t = sto_bv128 max_sint
  constant max_uint_as_bv128 : BV128.t = uto_bv128 max_uint

  val u_add (a b:t) : t
    requires { [@expl:arithmetic overflow]
                  to_uint a + to_uint b < two_power_size
               \/ BV128.ule (BV128.add (uto_bv128 a) (uto_bv128 b)) max_uint_as_bv128 }
    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:arithmetic overflow]
      - two_power_size_minus_one <= to_int a + to_int b < two_power_size_minus_one
      \/ let r = BV128.add (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    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:arithmetic overflow] to_uint a >= to_uint b \/ uge 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:arithmetic overflow]
      - two_power_size_minus_one <= to_int a - to_int b < two_power_size_minus_one
      \/ let r = BV128.sub (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    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:arithmetic overflow]
                  to_uint a * to_uint b < two_power_size
               \/ BV128.ule (BV128.mul (uto_bv128 a) (uto_bv128 b)) max_uint_as_bv128 }
    ensures  { result = mul a b }
    ensures  { to_int result = to_uint a * to_uint b }

unsigned multiplication with overflow check

  val s_mul (a b:t) : t
    requires { [@expl:arithmetic overflow]
      - two_power_size_minus_one <= to_int a * to_int b < two_power_size_minus_one
      \/ let r = BV128.mul (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    ensures  { result = mul a b }
    ensures  { to_int result = to_int a * to_int b }

signed multiplication with overflow check

  use bv.Pow2int

  val u_lsl (a b:t) : t
    requires { [@expl:out-of-bounds shifting]
                ult b size_bv \/ to_uint b < size }
    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 \/ to_uint b < size }
    requires { [@expl:out-of-bounds shifting]
                sle zeros a \/ to_int a >= 0 }
    requires { [@expl:arithmetic overflow]
      (to_int a) * (pow2 (to_int b)) < two_power_size_minus_one
      \/ let r = BV128.lsl_bv (sto_bv128 a) (sto_bv128 b) in
         (BV128.sle min_sint_as_bv128 r /\ BV128.sle r max_sint_as_bv128) }
    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 \/ to_uint b < size }
    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 \/ to_uint b < size }
    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 \/ to_uint b < size }
    requires { [@expl:out-of-bounds shifting]
                sge a zeros \/ to_int a >= 0 }
    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 \/ to_uint b <> 0 }
    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  \/ to_uint b <> 0 }
    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  \/ to_int b <> 0 }
    requires { [@expl:signed division overflow check] (a <> min_sint \/ b <> minus_one)
                \/ (to_int a <> to_int min_sint \/ to_int b <> -1)}
    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 \/ to_int b <> 0 }
    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

  constant minus_one : t = 0xFF
  constant min_sint : t = 0x80
  constant max_sint : t = 0x7F
  constant max_uint : t = 0xFF

  use bv.BVConverter_8_128

  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_size_minus_one = two_power_size_minus_one,
    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 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,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end

module BVCheck16
  use export bv.BV16

  constant minus_one : t = 0xFFFF
  constant min_sint : t = 0x8000
  constant max_sint : t = 0x7FFF
  constant max_uint : t = 0xFFFF

  use bv.BVConverter_16_128

  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_size_minus_one = two_power_size_minus_one,
    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 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,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end

module BVCheck32
  use export bv.BV32

  constant minus_one : t = 0xFFFF_FFFF
  constant min_sint : t = 0x8000_0000
  constant max_sint : t = 0x7FFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF

  use bv.BVConverter_32_128

  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_size_minus_one = two_power_size_minus_one,
    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 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,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end

module BVCheck64
  use export bv.BV64

  constant minus_one : t = 0xFFFF_FFFF_FFFF_FFFF
  constant min_sint : t = 0x8000_0000_0000_0000
  constant max_sint : t = 0x7FFF_FFFF_FFFF_FFFF
  constant max_uint : t = 0xFFFF_FFFF_FFFF_FFFF

  use bv.BVConverter_64_128

  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_size_minus_one = two_power_size_minus_one,
    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 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,
    function sto_bv128 = stoBig,
    function uto_bv128 = toBig
end