compilehashtbl

TODO

@@ -5,6 +5,8 @@ MAJOR TODAY
 - rename xextract to xpull;  and xgen to xpush.
 
 
+- Sys.max_array_length 
+
 
 MAJOR NEXT
 

examples/BasicDemos/Makefile

 
 # Possible to define "ML" to be the list of source files to consider
 
+ML := Demo.ml 
+
+
 # Uncomment next line to compile only Test.ml
-#ML := Test.ml 
-# Demo.ml
+ML := Test.ml 
+
 #CFDEBUG := 1
 
-ML := Demo.ml 
 
 include ../Makefile.example

examples/BasicDemos/Test.ml

+let max_array_length = 1000
 
+module type HashedType = sig
+  type t
+  val equal: t -> t -> bool
+  val hash: t -> int
+end
 
+(* A note on array bounds checks. In OCaml, a call [Array.get a i] is always
+   checked, a call [Array.unsafe_get a i] is never checked, and an array access
+   expression [a.(i)] is checked if and only if the compile-time flag [-unsafe]
+   is not passed. In the code that follows, we use the latter form. When
+   processed by CFML, without [-unsafe], this form is translated to
+   [Array.get a i], and we prove that the array index is within bounds. When
+   compiled with OCaml, we pass [-unsafe], so the check is not performed. *)
 
+(* In this code, array indices are always within bounds, even if the client is
+   unverified. This claim is informal, though; at present, we cannot explicitly
+   reason about an unverified client in CFML. *)
 
+module Make (H : HashedType) = struct
 
+  type key = H.t
 
+  (* A bucket is is a list of (unboxed) pairs of a key and a value. *)
+
+  type 'a bucket =
+    Empty
+  | Cons of H.t * 'a * 'a bucket
+
+  (* The [data] field holds an array of buckets. The length of this array is
+     always a power of two. Information about the key [k] is stored at index
+     [index h k] in this array. The [population] field records how many
+     bindings (i.e. key-data pairs) are present in the table. The [init] field
+     records the table's initial capacity; it is used only by [reset]. *)
+
+  type 'a table = {
+    mutable data: 'a bucket array;
+    mutable population: int;
+    init: int;
+  }
+
+  type 'a t = 'a table
+
+  (* [power_2_above x n] requires [x] to be a power of two, and ensures that
+     its result [y] is a power of two and satisfies [x <= y]. *)
+
+  (* It does NOT guarantee [n <= y]. In reality, this will be the case unless
+     [max_array_length] is reached. We do not exceed [max_array_length],
+     because we know that this will cause a failure when attempting to
+     allocate the array. Also, this guarantees that the function terminates
+     before an overflow can occur. These aspects are outside of the scope of
+     the formal proof. *)
+
+  let rec power_2_above x n =
+    if x >= n then x
+    else if x * 2 > max_array_length then x
+    else power_2_above (x * 2) n
+
+  let create init =
+    let init = power_2_above 16 init in
+    { data = Array.make init Empty; population = 0; init }
+
+  let clear h =
+    h.population <- 0;
+    Array.fill h.data 0 (Array.length h.data) Empty
+
+  let reset h =
+    h.population <- 0;
+    h.data <- Array.make h.init Empty
+
+  let copy h = {
+    data = Array.copy h.data;
+    population = h.population;
+    init = h.init
+  }
+
+  let population h =
+    h.population
+
+  let length =
+    population
+
+  let index h k =
+    (H.hash k) land (Array.length h.data - 1)
+
+  (* [insert_bucket data mask b] inserts the key-data pairs in [b],
+     back-to-front, into the array [data]. *)
+  (* [mask] must be [Array.length data - 1]. *)
+  (* TEMPORARY measure to see if [mask] is useful *)
+
+  let rec insert_bucket data mask = function
+    | Empty ->
+        ()
+    | Cons (k, x, b) ->
+        insert_bucket data mask b;        (* preserve the original order of elements *)
+        let i = (H.hash k) land mask in   (* inlined [index] *)
+        data.(i) <- Cons (k, x, data.(i))
+
+  let resize h =
+    let odata = h.data in
+    let nsize = Array.length odata * 2 in
+    if nsize < max_array_length then begin
+      let ndata = Array.make nsize Empty in
+      h.data <- ndata;
+      let mask = nsize - 1 in
+      (* We could use [Array.iter] and rely on the OCaml compiler to inline
+         it. The flambda compiler can do it. Still, it seems preferable to
+         use an explicit loop. *)
+      for i = 0 to Array.length odata - 1 do
+        insert_bucket ndata mask odata.(i)
+      done
+    end
+
+  let increment_population h =
+    h.population <- h.population + 1;
+    if h.population > 2 * Array.length h.data then resize h
+
+  let add h k x =
+    let i = index h k in
+    h.data.(i) <- (Cons (k, x, h.data.(i)));
+    increment_population h
+
+  let rec remove_bucket h k = function
+    | Empty ->
+        Empty
+    | Cons (k', i, next) ->
+        if H.equal k' k
+        then begin h.population <- h.population - 1; next end
+        else Cons (k', i, remove_bucket h k next)
+
+  let remove h k =
+    let i = index h k in
+    h.data.(i) <- remove_bucket h k h.data.(i)
+
+  let rec find_rec k = function
+    | Empty ->
+        None
+    | Cons (k', d, rest) ->
+        if H.equal k' k then Some d else find_rec k rest
+
+  let find h k =
+    find_rec k h.data.(index h k)
+
+  let find_all h k =
+    let rec find_in_bucket = function
+    | Empty ->
+        []
+    | Cons(k', d, rest) ->
+        if H.equal k' k
+        then d :: find_in_bucket rest
+        else find_in_bucket rest in
+    find_in_bucket h.data.(index h k)
+
+  let replace h k x =
+    let i = index h k in
+    let b = remove_bucket h k h.data.(i) in
+    h.data.(i) <- Cons (k, x, b);
+    increment_population h
+
+  let mem h k =
+    match find h k with None -> false | Some _ -> true
+
+  let rec iter_bucket f = function
+    | Empty ->
+        ()
+    | Cons(k, x, b) ->
+        f k x;
+        iter_bucket f b
+
+  let iter f h =
+    let data = h.data in
+    for i = 0 to Array.length data - 1 do
+      iter_bucket f data.(i)
+    done
+
+  let fold f h init =
+    let rec do_bucket accu b =
+      match b with
+        Empty ->
+          accu
+      | Cons(k, d, rest) ->
+          do_bucket (f k d accu) rest in
+    Array.fold_left do_bucket init h.data
+
+  type statistics = {
+    num_bindings: int;
+    num_buckets: int;
+    max_bucket_length: int;
+    bucket_histogram: int array
+  }
+
+  let rec bucket_length accu = function
+    | Empty -> accu
+    | Cons(_, _, rest) -> bucket_length (accu + 1) rest
+
+  let stats h =
+    let mbl =
+      Array.fold_left (fun m b -> max m (bucket_length 0 b)) 0 h.data in
+    let histo = Array.make (mbl + 1) 0 in
+    Array.iter
+      (fun b ->
+        let l = bucket_length 0 b in
+        histo.(l) <- histo.(l) + 1)
+      h.data;
+    { num_bindings = h.population;
+      num_buckets = Array.length h.data;
+      max_bucket_length = mbl;
+      bucket_histogram = histo }
+
+end
 
-let x = 3
\ No newline at end of file

generator/renaming.ml

@@ -74,9 +74,13 @@ let coq_keywords =
 let builtin_type_constructors =
   [ "int"; "char"; "unit"; "bool"; "float"; "list"; "string"; "array"; "option" ]
 
+let infix_named_functions =
+   [ "mod"; "land"; "lor"; "lxor"; "lnot"; "lsl"; "lsr"; "asr" ]
+
 let non_rebindable_names =
-    ["mod"; "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">" ]
-  @ ["ignore"; "abs"; "not"; "fst"; "snd"; "pred"; "succ"; "min"; "max";]
+    [ "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">" ]
+  @ infix_named_functions
+  @ [ "ignore"; "abs"; "not"; "fst"; "snd"; "pred"; "succ"; "min"; "max";]
   (* Remark: items from the second list, we could allow rebinding them,
      at the expense of systematically introducing a let-binding when we
      see them; else, we need the normalization to apply to a typed tree. *)
@@ -85,6 +89,7 @@ let reserved_variable_names =
   builtin_type_constructors @ coq_keywords
 
 
+
 (*#########################################################################*)
 (* ** Checking of variables names *)
 
@@ -124,7 +129,8 @@ let check_type_constr_name loc x =
 (* TODO: rename "infix" into something more general *)
 
 (** [infix_name_encode name] encodes an infix function name,
-    e.g. for "+^+" it produces "infix_plus_hat_plus_". *)
+    e.g. for "+^+" it produces "infix_plus_hat_plus_",
+    and for "mod" it produces "infix_mod__" *)
 
 let infix_name_symbols =
   ['!', "emark";
@@ -147,7 +153,7 @@ let infix_name_symbols =
    '~', "tilde" ]
 
 let infix_name_encode name =
-  if name = "mod" then "infix_mod__" else begin
+  if List.mem name infix_named_functions then "infix_" ^ name ^ "__" else begin
      let gen = Buffer.create 20 in
      String.iter (fun c -> 
         let s = 

lib/stdlib/Array.ml

@@ -45,6 +45,16 @@ let blit a1 start1 a2 start2 nb =
     set a2 (start2 + i) (get a1 (start1 + i));
   done
 
+let copy a =
+   let n = length a in
+   if n = 0 then make_empty() else begin
+     let r = make (length a) (get a 0) in
+     for i = 0 to pred n do
+        set r i (get a i);
+     done;
+      r
+   end
+
 let append a1 a2 =
   let n1 = length a1 in
   let n2 = length a2 in
@@ -100,6 +110,7 @@ let fold_left f x a =
   done;
   !r
 
+
 (* TODO: add support for downto in CFML 
 let fold_right f a x =
   let r = ref x in

lib/stdlib/Pervasives.ml

@@ -85,6 +85,19 @@ let abs (x:int)  =
   if x >= 0 then x else -x
 
 
+(************************************************************)
+(** Bit-level Integer *)
+
+external ( land ) : int -> int -> int = "%int_land"
+external ( lor )  : int -> int -> int = "%int_lor"
+external ( lxor ) : int -> int -> int = "%int_lxor"
+external lnot : int -> int = "%int_lnot"
+external ( lsl ) : int -> int -> int = "%int_lsl"
+external ( lsr ) : int -> int -> int = "%int_lsr"
+external ( asr ) : int -> int -> int = "%int_asr"
+
+
+
 (************************************************************)
 (** References *)