int.mlw 5.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14

(** {1 Arithmetic for programs} *)

(** {2 Integer Division}

It is checked that divisor is not null.

*)

module Int

  use export int.Int
  use export int.ComputerDivision

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15
  let (/) (x: int) (y: int)
16
    requires { "expl:division by zero" y <> 0 }
17
    ensures  { result = div x y }
18 19
  = div x y

20 21 22 23 24
  let (%) (x: int) (y: int)
    requires { "expl:division by zero" y <> 0 }
    ensures  { result = mod x y }
  = mod x y

25 26 27 28
end

(** {2 Machine integers}

29
  Bounded integers, typically n-bit signed and unsigned integers, go
30
  here. We first introduce a generic theory [Bounded_int] of bounded
31
  integers, with minimal and maximal values (resp. [min] and [max]).
32 33
  Then we instantiate it to get 32-bit and 64-bit signed and unsigned integers
  ([Int32], [UInt32], [Int64], and [UInt64]) as well as 31-bit and 63-bit signed
34
  integers ([Int31] and [Int63]) to be used in OCaml programs.
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64

*)

module Bounded_int

  use export int.Int

  type t

  constant min : int
  constant max : int

  function to_int (n:t) : int

  predicate in_bounds (n:int) = min <= n <= max

  axiom to_int_in_bounds: forall n:t. in_bounds (to_int n)

  val of_int (n:int) : t
    requires { "expl:integer overflow" in_bounds n }
    ensures  { to_int result = n }

  val (+) (a:t) (b:t) : t
    requires { "expl:integer overflow" in_bounds (to_int a + to_int b) }
    ensures   { to_int result = to_int a + to_int b }

  val (-) (a:t) (b:t) : t
    requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
    ensures  { to_int result = to_int a - to_int b }

65
  val ( *) (a:t) (b:t) : t
66 67 68 69
    requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
    ensures  { to_int result = to_int a * to_int b }

  val (-_) (a:t) : t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70 71
    requires { "expl:integer overflow" in_bounds (- to_int a) }
    ensures  { to_int result = - to_int a }
72

73
  val eq (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74
    ensures { result <-> to_int a = to_int b }
75 76

  val ne (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
    ensures { result <-> to_int a <> to_int b }
78

79 80 81
  axiom extensionality: forall x y: t. to_int x = to_int y -> x = y

  val (<=) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82
    ensures  { result <-> to_int a <= to_int b }
83 84

  val (<) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
    ensures  { result <-> to_int a < to_int b }
86 87

  val (>=) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88
    ensures  { result <-> to_int a >= to_int b }
89 90

  val (>) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
    ensures  { result <-> to_int a > to_int b }
92 93 94 95 96 97 98 99

  use import int.ComputerDivision

  val (/) (a:t) (b:t) : t
    requires { "expl:division by zero" to_int b <> 0 }
    requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) }
    ensures  { to_int result = div (to_int a) (to_int b) }

100 101 102 103 104
  val (%) (a:t) (b:t) : t
    requires { "expl:division by zero" to_int b <> 0 }
    requires { "expl:integer overflow" in_bounds (mod (to_int a) (to_int b)) }
    ensures  { to_int result = mod (to_int a) (to_int b) }

105 106
end

107 108 109 110 111 112 113 114 115
module Unsigned

  use import int.Int

  constant min_unsigned : int = 0

  clone export Bounded_int with
    constant min = min_unsigned

116 117 118 119
  constant zero_unsigned : t

  axiom zero_unsigned_is_zero : to_int zero_unsigned = 0

120
  val add_with_carry (x y:t) (c:t) : (t,t)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
121
    requires { 0 <= to_int c <= 1 }
122 123 124 125
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
      to_int x + to_int y + to_int c }

Guillaume Melquiond's avatar
Guillaume Melquiond committed
126
  val add3 (x y z:t) : (t,t)
MARCHE Claude's avatar
MARCHE Claude committed
127 128
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
129
      to_int x + to_int y + to_int z }
MARCHE Claude's avatar
MARCHE Claude committed
130

Guillaume Melquiond's avatar
Guillaume Melquiond committed
131
  val mul_double (x y:t) : (t,t)
MARCHE Claude's avatar
MARCHE Claude committed
132 133
    returns { (r,d) ->
      to_int r + (max+1) * to_int d =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
134
      to_int x * to_int y }
MARCHE Claude's avatar
MARCHE Claude committed
135

136 137
end

138 139 140 141 142 143 144 145 146 147 148 149 150 151
module Int31

  use import int.Int

  type int31

  constant min_int31 : int = - 0x40000000
  constant max_int31 : int =   0x3fffffff

  clone export Bounded_int with
    type t = int31,
    constant min = min_int31,
    constant max = max_int31

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152 153 154 155 156 157 158
  use bv.BV31

  val to_bv (x: int31) : BV31.t
    ensures { BV31.to_int result = to_int x }
  val of_bv (x: BV31.t) : int31
    ensures { to_int result = BV31.to_int x }

159 160
end

161 162 163 164 165 166 167 168 169 170 171 172 173 174
module Int32

  use import int.Int

  type int32

  constant min_int32 : int = - 0x80000000
  constant max_int32 : int =   0x7fffffff

  clone export Bounded_int with
    type t = int32,
    constant min = min_int32,
    constant max = max_int32

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175 176 177 178 179 180 181
  use bv.BV32

  val to_bv (x: int32) : BV32.t
    ensures { BV32.to_int result = to_int x }
  val of_bv (x: BV32.t) : int32
    ensures { to_int result = BV32.to_int x }

182 183 184 185 186 187 188 189
end

module UInt32

  type uint32

  constant max_uint32 : int = 0xffffffff

190
  clone export Unsigned with
191 192 193
    type t = uint32,
    constant max = max_uint32

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194 195 196 197 198 199 200
  use bv.BV32

  val to_bv (x: uint32) : BV32.t
    ensures { BV32.to_uint result = to_int x }
  val of_bv (x: BV32.t) : uint32
    ensures { to_int result = BV32.to_uint x }

201 202
end

203 204 205 206 207 208 209 210 211 212 213 214 215 216
module Int63

  use import int.Int

  type int63

  constant min_int63 : int = - 0x4000000000000000
  constant max_int63 : int =   0x3fffffffffffffff

  clone export Bounded_int with
    type t = int63,
    constant min = min_int63,
    constant max = max_int63

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217 218 219 220 221 222 223
  use bv.BV63

  val to_bv (x: int63) : BV63.t
    ensures { BV63.to_int result = to_int x }
  val of_bv (x: BV63.t) : int63
    ensures { to_int result = BV63.to_int x }

224 225
end

226 227 228 229 230 231 232 233 234 235 236 237 238 239
module Int64

  use import int.Int

  type int64

  constant min_int64 : int = - 0x8000000000000000
  constant max_int64 : int =   0x7fffffffffffffff

  clone export Bounded_int with
    type t = int64,
    constant min = min_int64,
    constant max = max_int64

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240 241 242 243 244 245 246
  use bv.BV64

  val to_bv (x: int64) : BV64.t
    ensures { BV64.to_int result = to_int x }
  val of_bv (x: BV64.t) : int64
    ensures { to_int result = BV64.to_int x }

247 248 249 250 251 252 253 254 255 256
end

module UInt64

  use import int.Int

  type uint64

  constant max_uint64 : int =  0xffffffffffffffff

257
  clone export Unsigned with
258 259 260
    type t = uint64,
    constant max = max_uint64

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261 262 263 264 265 266 267
  use bv.BV64

  val to_bv (x: uint64) : BV64.t
    ensures { BV64.to_uint result = to_int x }
  val of_bv (x: BV64.t) : uint64
    ensures { to_int result = BV64.to_uint x }

268
end