more machine arithmetic (still in progress)

.gitignore

@@ -204,6 +204,8 @@ pvsbin/
 /modules/stack/
 /modules/queue/
 /modules/pqueue/
+/modules/mach/array/
+/modules/mach/int/
 
 # jessie3
 /src/jessie/.depend

drivers/ocaml.drv

@@ -61,3 +61,92 @@ module ref.Ref
   syntax val      (:=)     "Pervasives.(:=)"
 end
 
+module mach.int.Int31
+  (* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
+  syntax type     int31     "int"
+  syntax constant min_int31 "(- 0x4000_0000)"
+  syntax constant max_int31    "0x3fff_ffff"
+  syntax val      of_int    "(fun x -> int_of_string (Num.string_of_num x))"
+                            (* FIXME: use a realization instead? *)
+  syntax val      ( + )     "( + )"
+  syntax val      ( - )     "( - )"
+  syntax val      (-_)      "( ~- )"
+  syntax val      ( * )     "( * )"
+  syntax val      ( / )     "( / )"
+  syntax val      (<=)      "(<=)"
+  syntax val      (<)       "(<)"
+  syntax val      (>=)      "(>=)"
+  syntax val      (>)       "(>)"
+end
+
+module mach.int.Int32
+  syntax type     int32     "Int32.t"
+  syntax constant min_int32 "Int32.min_int"
+  syntax constant max_int32 "Int32.max_int"
+  syntax val      of_int    "(fun x -> Int32.of_string (Num.string_of_num x))"
+                            (* FIXME: use a realization instead? *)
+  syntax val      (+)       "Int32.add"
+  syntax val      (-)       "Int32.sub"
+  syntax val      (-_)      "Int32.neg"
+  syntax val      ( * )     "Int32.mul"
+  syntax val      (/)       "Int32.div"
+  syntax val      (<=)      "(<=)"
+  syntax val      (<)       "(<)"
+  syntax val      (>=)      "(>=)"
+  syntax val      (>)       "(>)"
+end
+
+module mach.int.Int63
+  (* only safe on a 64-bit machine *)
+  prelude "let () = assert (Sys.word_size = 64)"
+  syntax type     int63     "int"
+  syntax constant min_int63 "(- 0x4000_0000_0000_0000)"
+  syntax constant max_int63    "0x3fff_ffff_ffff_ffff"
+  syntax val      of_int    "(fun x -> int_of_string (Num.string_of_num x))"
+                            (* FIXME: use a realization instead? *)
+  syntax val      ( + )     "( + )"
+  syntax val      ( - )     "( - )"
+  syntax val      (-_)      "( ~- )"
+  syntax val      ( * )     "( * )"
+  syntax val      ( / )     "( / )"
+  syntax val      (<=)      "(<=)"
+  syntax val      (<)       "(<)"
+  syntax val      (>=)      "(>=)"
+  syntax val      (>)       "(>)"
+end
+
+module mach.int.Int64
+  syntax type     int64     "Int64.t"
+  syntax constant min_int64 "Int64.min_int"
+  syntax constant max_int64 "Int64.max_int"
+  syntax val      of_int    "(fun x -> Int64.of_string (Num.string_of_num x))"
+                            (* FIXME: use a realization instead? *)
+  syntax val      (+)       "Int64.add"
+  syntax val      (-)       "Int64.sub"
+  syntax val      (-_)      "Int64.neg"
+  syntax val      ( * )     "Int64.mul"
+  syntax val      (/)       "Int64.div"
+  syntax val      (<=)      "(<=)"
+  syntax val      (<)       "(<)"
+  syntax val      (>=)      "(>=)"
+  syntax val      (>)       "(>)"
+end
+
+module mach.array.Array31
+  syntax type array  "array"
+  syntax val  make   "Array.make"
+  syntax val  ([])   "Array.get"
+  syntax val  ([]<-) "Array.set"
+  syntax val  length "Array.length"
+  syntax val  append "Array.append"
+  syntax val  sub    "Array.sub"
+  syntax val  copy   "Array.copy"
+  syntax val  fill   "Array.fill"
+  syntax val  blit   "Array.blit"
+  syntax val  self_blit "Array.blit"
+end
+
+(* TODO
+   - OutOfBounds, defensive_get, defensive_set in mach.array.in Array31
+   - mach.array.Array32  -> Bigarray sur 32-bit / Array sur 64-bit ?
+*)

modules/mach/array.mlw

-(** {1 Arrays} *)
+(** {1 Arrays with bounded-size integers}
+
+    Note: We currently duplicate code to get the various modules below
+    but we should eventually be able to implement a single module and
+    then to clone it.  *)
 
 (** {2 Arrays with 32-bit indices} *)
 
@@ -116,3 +120,125 @@ module Array32
       a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
 
 end
+
+(** {2 Arrays with 31-bit indices} *)
+
+module Array31
+
+  use import mach.int.Int31
+  use import map.Map as M
+
+  type array 'a model { length: int31; mutable elts: map int 'a }
+    invariant { 0 <= to_int self.length }
+
+  function get (a: array ~'a) (i: int) : 'a = M.get a.elts i
+
+  function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
+    { a with elts = M.set a.elts i v }
+
+  (** syntactic sugar *)
+  function ([]) (a: array 'a) (i: int) : 'a = get a i
+  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
+
+  val ([]) (a: array ~'a) (i: int31) : 'a
+    requires { 0 <= to_int i < to_int a.length }
+    ensures  { result = a[to_int i] }
+
+  val ([]<-) (a: array ~'a) (i: int31) (v: 'a) : unit writes {a}
+    requires { 0 <= to_int i < to_int a.length }
+    ensures  { a.elts = M.set (old a.elts) (to_int i) v }
+
+  val length (a: array ~'a) : int31 ensures { result = a.length }
+
+  (** unsafe get/set operations with no precondition *)
+  exception OutOfBounds
+
+  let defensive_get (a: array 'a) (i: int31)
+    ensures { 0 <= to_int i < to_int a.length }
+    ensures { result = a[to_int i] }
+    raises  { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
+  = if i < of_int 0 || i >= length a then raise OutOfBounds;
+    a[i]
+
+  let defensive_set (a: array 'a) (i: int31) (v: 'a)
+    ensures { 0 <= to_int i < to_int a.length }
+    ensures { a = (old a)[to_int i <- v] }
+    raises  { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
+  = if i < of_int 0 || i >= length a then raise OutOfBounds;
+    a[i] <- v
+
+  function make (n: int31) (v: ~'a) : array 'a =
+    { length = n; elts = M.const v }
+
+  val make (n: int31) (v: ~'a) : array 'a
+    requires { to_int n >= 0 }
+    ensures  { result = make n v }
+
+  val append (a1: array ~'a) (a2: array 'a) : array 'a
+    ensures { to_int result.length = to_int a1.length + to_int a2.length }
+    ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
+    ensures { forall i:int. 0 <= i < to_int a2.length ->
+              result[to_int a1.length + i] = a2[i] }
+
+  val sub (a: array ~'a) (ofs: int31) (len: int31) : array 'a
+    requires { 0 <= to_int ofs /\ 0 <= to_int len }
+    requires { to_int ofs + to_int len <= to_int a.length }
+    ensures  { result.length = len }
+    ensures  { forall i:int. 0 <= i < to_int len ->
+               result[i] = a[to_int ofs + i] }
+
+  val copy (a: array ~'a) : array 'a
+    ensures  { result.length = a.length }
+    ensures  { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
+
+  let fill (a: array ~'a) (ofs: int31) (len: int31) (v: 'a)
+    requires { 0 <= to_int ofs /\ 0 <= to_int len }
+    requires { to_int ofs + to_int len <= to_int a.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs \/
+        to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
+    ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
+               a[i] = v }
+  = 'Init:
+    for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int31 *)
+      invariant { forall i:int.
+        (0 <= i < to_int ofs \/
+          to_int ofs + to_int len <= i < to_int a.length) ->
+        a[i] = (at a 'Init)[i] }
+      invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
+      let k = of_int k in
+      a[ofs + k] <- v
+    done
+
+  val blit (a1: array ~'a) (ofs1: int31)
+                 (a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2}
+    requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
+    requires { to_int ofs1 + to_int len <= to_int a1.length }
+    requires { 0 <= to_int ofs2 /\
+               to_int ofs2 + to_int len <= to_int a2.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs2 \/
+       to_int ofs2 + to_int len <= i < to_int a2.length) ->
+       a2[i] = (old a2)[i] }
+    ensures  { forall i:int.
+      to_int ofs2 <= i < to_int ofs2 + to_int len ->
+      a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
+
+  val self_blit (a: array ~'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
+    writes {a}
+    requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
+               to_int ofs1 + to_int len <= to_int a.length }
+    requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs2 \/
+       to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
+    ensures  { forall i:int.
+      to_int ofs2 <= i < to_int ofs2 + to_int len ->
+      a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
+
+end
+
+(* TODO
+   - Array63
+   - Array64
+*)

modules/mach/int.mlw

@@ -39,7 +39,12 @@ end
 
 (** {2 Machine integers}
 
-32-bit integers and such go here.
+  Bounded integers, typically n-bit signed and unsigned integers, go
+  here. We first introude a generic theory [Bounded_int]of bounded
+  integers, with minimal and maximal values (resp. [min] and [max]).
+  Then we instantiate it to get 32 and 64 signed and unsigned integers
+  ([Int32], [UInt32], [Int64], and [UInt64]) as well as 31 and 63 signed
+  integers ([Int31] and [Int63]) to be used in OCaml programs.
 
 *)
 
@@ -101,6 +106,22 @@ module Bounded_int
 
 end
 
+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
+
+end
+
 module Int32
 
   use import int.Int
@@ -131,6 +152,22 @@ module UInt32
 
 end
 
+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
+
+end
+
 module Int64
 
   use import int.Int