Index: tracted/Fix.ml
===================================================================
 /extracted/Fix.ml (revision 2737)
+++ (revision )
@@ 1,554 +1,0 @@
(**************************************************************************)
(* *)
(* Fix *)
(* *)
(* Author: François Pottier, INRIA ParisRocquencourt *)
(* Version: 20091201 *)
(* *)
(* The copyright to this code is held by Institut National de Recherche *)
(* en Informatique et en Automatique (INRIA). All rights reserved. This *)
(* file is distributed under the license CeCILLC (see file LICENSE). *)
(* *)
(**************************************************************************)

module MyList = struct
let rec rev_append l1 l2 =
 match l1 with
 [] > l2
  a :: l > rev_append l (a :: l2)

let rev l = rev_append l []

let find_all p =
 let rec find accu = function
  [] > rev accu
  x :: l > if p x then find (x :: accu) l else find accu l in
 find []

let filter = find_all

let rec map f = function
 [] > []
  a::l > let r = f a in r :: map f l

let rec iter f = function
 [] > ()
  a::l > f a; iter f l
end

(*  *)

(* Maps. *)

(* We require imperative maps, that is, maps that can be updated in place.
 An implementation of persistent maps, such as the one offered by ocaml's
 standard library, can easily be turned into an implementation of imperative
 maps, so this is a weak requirement. *)

module type IMPERATIVE_MAPS = sig
 type key
 type 'data t
 val create: unit > 'data t
 val clear: 'data t > unit
 val add: key > 'data > 'data t > unit
 val find: key > 'data t > 'data
 val iter: (key > 'data > unit) > 'data t > unit
end

(*  *)

(* Properties. *)

(* Properties must form a partial order, equipped with a least element, and
 must satisfy the ascending chain condition: every monotone sequence
 eventually stabilizes. *)

(* [is_maximal] determines whether a property [p] is maximal with respect to
 the partial order. Only a conservative check is required: in any event, it
 is permitted for [is_maximal p] to return [false]. If [is_maximal p]
 returns [true], then [p] must have no upper bound other than itself. In
 particular, if properties form a lattice, then [p] must be the top
 element. This feature, not described in the paper, enables a couple of
 minor optimizations. *)

module type PROPERTY = sig
 type property
 val bottom: property
 val equal: property > property > bool
 val is_maximal: property > bool
end

(*  *)

(* The dynamic dependency graph. *)

(* An edge from [node1] to [node2] means that [node1] depends on [node2], or
 (equivalently) that [node1] observes [node2]. Then, an update of the
 current property at [node2] causes a signal to be sent to [node1]. A node
 can observe itself. *)

(* This module could be placed in a separate file, but is included here in
 order to make [Fix] selfcontained. *)

module Graph : sig

 (* This module provides a data structure for maintaining and modifying
 a directed graph. Each node is allowed to carry a piece of client
 data. There are functions for creating a new node, looking up a
 node's data, looking up a node's predecessors, and setting or
 clearing a node's successors (all at once). *)
 type 'data node

 (* [create data] creates a new node, with no incident edges, with
 client information [data]. Time complexity: constant. *)
 val create: 'data > 'data node

 (* [data node] returns the client information associated with
 the node [node]. Time complexity: constant. *)
 val data: 'data node > 'data

 (* [predecessors node] returns a list of [node]'s predecessors.
 Amortized time complexity: linear in the length of the output
 list. *)
 val predecessors: 'data node > 'data node list

 (* [set_successors src dsts] creates an edge from the node [src] to
 each of the nodes in the list [dsts]. Duplicate elements in the
 list [dsts] are removed, so that no duplicate edges are created. It
 is assumed that [src] initially has no successors. Time complexity:
 linear in the length of the input list. *)
 val set_successors: 'data node > 'data node list > unit

 (* [clear_successors node] removes all of [node]'s outgoing edges.
 Time complexity: linear in the number of edges that are removed. *)
 val clear_successors: 'data node > unit

 (* That's it. *)
end
= struct

 (* Using doublylinked adjacency lists, one could implement [predecessors]
 in worstcase linear time with respect to the length of the output list,
 [set_successors] in worstcase linear time with respect to the length of
 the input list, and [clear_successors] in worstcase linear time with
 respect to the number of edges that are removed. We use a simpler
 implementation, based on singlylinked adjacency lists, with deferred
 removal of edges. It achieves the same complexity bounds, except
 [predecessors] only offers an amortized complexity bound. This is good
 enough for our purposes, and, in practice, is more efficient by a
 constant factor. This simplification was suggested by Arthur
 Charguéraud. *)

 type 'data node = {

 (* The client information associated with this node. *)

 data: 'data;

 (* This node's incoming and outgoing edges. *)

 mutable outgoing: 'data edge list;
 mutable incoming: 'data edge list;

 (* A transient mark, always set to [false], except when checking
 against duplicate elements in a successor list. *)

 mutable marked: bool;

 }

 and 'data edge = {

 (* This edge's nodes. Edges are symmetric: source and destination
 are not distinguished. Thus, an edge appears both in the outgoing
 edge list of its source node and in the incoming edge list of its
 destination node. This allows edges to be easily marked as
 destroyed. *)

 node1: 'data node;
 node2: 'data node;

 (* Edges that are destroyed are marked as such, but are not
 immediately removed from the adjacency lists. *)

 mutable destroyed: bool;

 }

 let create (data : 'data) : 'data node = {
 data = data;
 outgoing = [];
 incoming = [];
 marked = false;
 }

 let data (node : 'data node) : 'data =
 node.data

 (* [follow src edge] returns the node that is connected to [src]
 by [edge]. Time complexity: constant. *)

 let follow src edge =
 if edge.node1 == src then
 edge.node2
 else begin
 assert (edge.node2 == src);
 edge.node1
 end

 (* The [predecessors] function removes edges that have been marked
 destroyed. The cost of removing these has already been paid for,
 so the amortized time complexity of [predecessors] is linear in
 the length of the output list. *)

 let predecessors (node : 'data node) : 'data node list =
 let predecessors = MyList.filter (fun edge > not edge.destroyed) node.incoming in
 node.incoming < predecessors;
 MyList.map (follow node) predecessors

 (* [link src dst] creates a new edge from [src] to [dst], together
 with its reverse edge. Time complexity: constant. *)

 let link (src : 'data node) (dst : 'data node) : unit =
 let edge = {
 node1 = src;
 node2 = dst;
 destroyed = false;
 } in
 src.outgoing < edge :: src.outgoing;
 dst.incoming < edge :: dst.incoming

 let set_successors (src : 'data node) (dsts : 'data node list) : unit =
 assert (src.outgoing = []);
 let rec loop = function
  [] >
 ()
  dst :: dsts >
 if dst.marked then
 loop dsts (* skip duplicate elements *)
 else begin
 dst.marked < true;
 link src dst;
 loop dsts;
 dst.marked < false
 end
 in
 loop dsts

 let clear_successors (node : 'data node) : unit =
 MyList.iter (fun edge >
 assert (not edge.destroyed);
 edge.destroyed < true;
 ) node.outgoing;
 node.outgoing < []

end

(*  *)

(* The code is parametric in an implementation of maps over variables and in
 an implementation of properties. *)

module Make
 (M : IMPERATIVE_MAPS)
 (P : PROPERTY)
= struct

type variable =
 M.key

type property =
 P.property

type valuation =
 variable > property

type rhs =
 valuation > property

type equations =
 variable > rhs

(*  *)

(* Data. *)

(* Each node in the dependency graph carries information about a fixed
 variable [v]. *)

type node =
 data Graph.node

and data = {

 (* This is the result of the application of [rhs] to the variable [v]. It
 must be stored in order to guarantee that this application is performed
 at most once. *)
 rhs: rhs;

 (* This is the current property at [v]. It evolves monotonically with
 time. *)
 mutable property: property;

 (* That's it! *)
}

(* [property node] returns the current property at [node]. *)

let property node =
 (Graph.data node).property

(*  *)

(* Many definitions must be made within the body of the function [lfp].
 For greater syntactic convenience, we place them in a local module. *)

let lfp (eqs : equations) : valuation =
 let module LFP = struct

(*  *)

(* The workset. *)

(* When the algorithm is inactive, the workset is empty. *)

(* Our workset is based on a Queue, but it could just as well be based on a
 Stack. A textual replacement is possible. It could also be based on a
 priority queue, provided a sensible way of assigning priorities could
 be found. *)

module Workset : sig

 (* [insert node] inserts [node] into the workset. [node] must have no
 successors. *)
 val insert: node > unit

 (* [repeat f] repeatedly applies [f] to a node extracted out of the
 workset, until the workset becomes empty. [f] is allowed to use
 [insert]. *)
 val repeat: (node > unit) > unit

 (* That's it! *)
end
= struct

 (* Initialize the workset. *)

 let workset =
 Queue.create()

 let insert node =
 Queue.push node workset

 let repeat f =
 while not (Queue.is_empty workset) do
 f (Queue.pop workset)
 done

end

(*  *)

(* Signals. *)

(* A node in the workset has no successors. (It can have predecessors.) In
 other words, a predecessor (an observer) of some node is never in the
 workset. Furthermore, a node never appears twice in the workset. *)

(* When a variable broadcasts a signal, all of its predecessors (observers)
 receive the signal. Any variable that receives the signal loses all of its
 successors (that is, it ceases to observe anything) and is inserted into
 the workset. This preserves the above invariant. *)

let signal subject =
 MyList.iter (fun observer >
 Graph.clear_successors observer;
 Workset.insert observer
 ) (Graph.predecessors subject)
 (* At this point, [subject] has no predecessors. This plays no role in
 the correctness proof, though. *)

(*  *)

(* Tables. *)

(* The permanent table maps variables that have reached a fixed point
 to properties. It persists forever. *)

let permanent : property M.t =
 M.create()

(* The transient table maps variables that have not yet reached a
 fixed point to nodes. (A node contains not only a property, but
 also a memoized righthand side, and carries edges.) At the
 beginning of a run, it is empty. It fills up during a run. At the
 end of a run, it is copied into the permanent table and cleared. *)

let transient : node M.t =
 M.create()

(* [freeze()] copies the transient table into the permanent table, and
 empties the transient table. This allows all nodes to be reclaimed
 by the garbage collector. *)

let freeze () =
 M.iter (fun v node >
 M.add v (property node) permanent
 ) transient;
 M.clear transient

(*  *)

(* Workset processing. *)


(* [solve node] reevaluates the righthand side at [node]. If this leads to
 a change, then the current property is updated, and [node] emits a signal
 towards its observers. *)

(* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve]
 is invoked by [node_for], [node] is newly created; when [solve] is invoked by
 [Workset.repeat], [node] has just been extracted out of the workset, and a
 node in the workset has no subjects. *)

(* [node] must not be in the workset. *)

(* In short, when [solve node] is invoked, [node] is neither awake nor asleep.
 When [solve node] finishes, [node] is either awake or asleep again. (Chances
 are, it is asleep, unless it is its own observer; then, it is awakened by the
 final call to [signal node].) *)

let rec solve (node : node) : unit =

 (* Retrieve the data record carried by this node. *)
 let data = Graph.data node in

 (* Prepare to compute an updated value at this node. This is done by
 invoking the client's righthand side function. *)

 (* The flag [alive] is used to prevent the client from invoking [request]
 after this interaction phase is over. In theory, this dynamic check seems
 required in order to argue that [request] behaves like a pure function.
 In practice, this check is not very useful: only a bizarre client would
 store a [request] function and invoke it after it has become stale. *)
 let alive = ref true
 and subjects = ref [] in

 (* We supply the client with [request], a function that provides access to
 the current valuation, and dynamically records dependencies. This yields
 a set of dependencies that is correct by construction. *)
 let request (v : variable) : property =
 assert !alive;
 try
 M.find v permanent
 with Not_found >
 let subject = node_for v in
 let p = property subject in
 if not (P.is_maximal p) then
 subjects := subject :: !subjects;
 p
 in

 (* Give control to the client. *)
 let new_property = data.rhs request in

 (* From now on, prevent any invocation of this instance of [request]
 the client. *)
 alive := false;

 (* At this point, [node] has no subjects, as noted above. Thus, the
 precondition of [set_successors] is met. We can install [data.subjects]
 as the new set of subjects for this node. *)

 (* If we have gathered no subjects in the list [data.subjects], then
 this node must have stabilized. If [new_property] is maximal,
 then this node must have stabilized. *)

 (* If this node has stabilized, then it need not observe any more, so the
 call to [set_successors] is skipped. In practice, this seems to be a
 minor optimization. In the particular case where every node stabilizes at
 the very first call to [rhs], this means that no edges are ever
 built. This particular case is unlikely, as it means that we are just
 doing memoization, not a true fixed point computation. *)

 (* One could go further and note that, if this node has stabilized, then it
 could immediately be taken out of the transient table and copied into the
 permanent table. This would have the beneficial effect of allowing the
 detection of further nodes that have stabilized. Furthermore, it would
 enforce the property that no node in the transient table has a maximal
 value, hence the call to [is_maximal] above would become useless. *)

 if not (!subjects = []  P.is_maximal new_property) then
 Graph.set_successors node !subjects;

 (* If the updated value differs from the previous value, record
 the updated value and send a signal to all observers of [node]. *)
 if not (P.equal data.property new_property) then begin
 data.property < new_property;
 signal node
 end
 (* Note that equality of the two values does not imply that this node has
 stabilized forever. *)

(*  *)

(* [node_for v] returns the graph node associated with the variable [v]. It is
 assumed that [v] does not appear in the permanent table. If [v] appears in
 the transient table, the associated node is returned. Otherwise, [v] is a
 newly discovered variable: a new node is created on the fly, and the
 transient table is grown. The new node can either be inserted into the
 workset (it is then awake) or handled immediately via a recursive call to
 [solve] (it is then asleep, unless it observes itself). *)

(* The recursive call to [solve node] can be replaced, if desired, by a call
 to [Workset.insert node]. Using a recursive call to [solve] permits eager
 topdown discovery of new nodes. This can save a constant factor, because
 it allows new nodes to move directly from [bottom] to a good first
 approximation, without sending any signals, since [node] has no observers
 when [solve node] is invoked. In fact, if the dependency graph is acyclic,
 the algorithm discovers nodes topdown, performs computation on the way
 back up, and runs without ever inserting a node into the workset!
 Unfortunately, this causes the stack to grow as deep as the longest path in
 the dependency graph, which can blow up the stack. *)

and node_for (v : variable) : node =
 try
 M.find v transient
 with Not_found >
 let node = Graph.create { rhs = eqs v; property = P.bottom } in
 (* Adding this node to the transient table prior to calling [solve]
 recursively is mandatory, otherwise [solve] might loop, creating
 an infinite number of nodes for the same variable. *)
 M.add v node transient;
 solve node; (* or: Workset.insert node *)
 node

(*  *)

(* Invocations of [get] trigger the fixed point computation. *)

(* The flag [inactive] prevents reentrant calls by the client. *)

let inactive =
 ref true

let get (v : variable) : property =
 try
 M.find v permanent
 with Not_found >
 assert !inactive;
 inactive := false;
 let node = node_for v in
 Workset.repeat solve;
 freeze();
 inactive := true;
 property node

(*  *)

(* Close the local module [LFP]. *)

end
in LFP.get

end
Index: tracted/Fix.mli
===================================================================
 /extracted/Fix.mli (revision 2737)
+++ (revision )
@@ 1,103 +1,0 @@

(** This module provides a generic algorithm to compute the least
 solution of a system of monotonic equations. *)

(**************************************************************************)
(* *)
(* Fix *)
(* *)
(* Author: François Pottier, INRIA ParisRocquencourt *)
(* Version: 20091201 *)
(* *)
(* The copyright to this code is held by Institut National de Recherche *)
(* en Informatique et en Automatique (INRIA). All rights reserved. This *)
(* file is distributed under the license CeCILLC (see file LICENSE). *)
(* *)
(**************************************************************************)

(* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)

(*  *)

(* Maps. *)

(* We require imperative maps, that is, maps that can be updated in place.
 An implementation of persistent maps, such as the one offered by ocaml's
 standard library, can easily be turned into an implementation of imperative
 maps, so this is a weak requirement. *)

module type IMPERATIVE_MAPS = sig
 type key
 type 'data t
 val create: unit > 'data t
 val clear: 'data t > unit
 val add: key > 'data > 'data t > unit
 val find: key > 'data t > 'data
 val iter: (key > 'data > unit) > 'data t > unit
end

(*  *)

(* Properties. *)

(* Properties must form a partial order, equipped with a least element, and
 must satisfy the ascending chain condition: every monotone sequence
 eventually stabilizes. *)

(* [is_maximal] determines whether a property [p] is maximal with respect to
 the partial order. Only a conservative check is required: in any event, it
 is permitted for [is_maximal p] to return [false]. If [is_maximal p]
 returns [true], then [p] must have no upper bound other than itself. In
 particular, if properties form a lattice, then [p] must be the top
 element. This feature, not described in the paper, enables a couple of
 minor optimizations. *)

module type PROPERTY = sig
 type property
 val bottom: property
 val equal: property > property > bool
 val is_maximal: property > bool
end

(*  *)

(* The code is parametric in an implementation of maps over variables and in
 an implementation of properties. *)

module Make
 (M : IMPERATIVE_MAPS)
 (P : PROPERTY)
 : sig
 type variable = M.key
 type property = P.property

 (* A valuation is a mapping of variables to properties. *)
 type valuation = variable > property

 (* A righthand side, when supplied with a valuation that gives
 meaning to its free variables, evaluates to a property. More
 precisely, a righthand side is a monotone function of
 valuations to properties. *)
 type rhs = valuation > property

 (* A system of equations is a mapping of variables to righthand
 sides. *)
 type equations = variable > rhs

 (* [lfp eqs] produces the least solution of the system of monotone
 equations [eqs]. *)

 (* It is guaranteed that, for each variable [v], the application [eqs v] is
 performed at most once (whereas the righthand side produced by this
 application is, in general, evaluated multiple times). This guarantee can
 be used to perform costly precomputation, or memory allocation, when [eqs]
 is applied to its first argument. *)

 (* When [lfp] is applied to a system of equations [eqs], it performs no
 actual computation. It produces a valuation, [get], which represents
 the least solution of the system of equations. The actual fixed point
 computation takes place, on demand, when [get] is applied. *)
 val lfp: equations > valuation
 end

(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
Index: /extracted/build
===================================================================
 /extracted/build (revision 2737)
+++ /extracted/build (revision 2738)
@@ 2,4 +2,4 @@
# Uses a GNU sed extension
ls *.ml  sed e 's/\(.\)\(.*\)\.ml/\U\1\E\2/' > extracted.mlpack
ocamlbuild cflag g extracted.cmo
+for i in `ls *.ml untrusted/*.ml`; do basename $i  sed e 's/\(.\)\(.*\)\.ml/\U\1\E\2/'; done > extracted.mlpack
+ocamlbuild Is untrusted cflag g extracted.cmo
Index: /extracted/compiler.ml
===================================================================
 /extracted/compiler.ml (revision 2737)
+++ /extracted/compiler.ml (revision 2738)
@@ 274,6 +274,5 @@
(** val colour_graph : Interference.coloured_graph_computer **)
let colour_graph _ =
 failwith "AXIOM TO BE REALIZED"
+let colour_graph = Compute_colouring.colour_graph
(** val back_end :
Index: tracted/compute_fixpoints.ml
===================================================================
 /extracted/compute_fixpoints.ml (revision 2737)
+++ (revision )
@@ 1,35 +1,0 @@
module Label_ImperativeMap = struct

 type key = Graphs.label

 type 'data t = 'data Graphs.graph ref

 let create () = ref (Identifiers.empty_map PreIdentifiers.LabelTag)

 let clear t =
 t := Identifiers.empty_map PreIdentifiers.LabelTag

 let add k d t =
 t := Identifiers.add PreIdentifiers.LabelTag !t k d

 let find k t =
 match Identifiers.lookup0 PreIdentifiers.LabelTag !t k with
 Types.Some res > res
  Types.None > raise Not_found

 let iter f t =
 Identifiers.foldi0 PreIdentifiers.LabelTag (fun k v () > f k v) !t ()

end

(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
let compute_fixpoint latt =
 let module L : Fix.PROPERTY with type property = Preamble.__ =
 struct
 type property = Preamble.__
 let bottom = Fixpoints.l_bottom latt
 let equal x y = Fixpoints.l_equal latt x y = Bool.True
 let is_maximal x = Fixpoints.l_is_maximal latt x = Bool.True
 end in
 let module F = Fix.Make (Label_ImperativeMap) (L) in
 F.lfp
Index: tracted/compute_fixpoints.mli
===================================================================
 /extracted/compute_fixpoints.mli (revision 2737)
+++ (revision )
@@ 1,1 +1,0 @@
val compute_fixpoint : Fixpoints.fixpoint_computer
Index: tracted/set_adt.ml
===================================================================
 /extracted/set_adt.ml (revision 2737)
+++ (revision )
@@ 1,202 +1,0 @@
(* Copied from OCaml's set.ml *)

 type 'a set = Empty  Node of 'a set * 'a * 'a set * int

 let height = function
 Empty > 0
  Node(_, _, _, h) > h

 let create l v r =
 let hl = match l with Empty > 0  Node(_,_,_,h) > h in
 let hr = match r with Empty > 0  Node(_,_,_,h) > h in
 Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))

 let bal l v r =
 let hl = match l with Empty > 0  Node(_,_,_,h) > h in
 let hr = match r with Empty > 0  Node(_,_,_,h) > h in
 if hl > hr + 2 then begin
 match l with
 Empty > invalid_arg "Set.bal"
  Node(ll, lv, lr, _) >
 if height ll >= height lr then
 create ll lv (create lr v r)
 else begin
 match lr with
 Empty > invalid_arg "Set.bal"
  Node(lrl, lrv, lrr, _)>
 create (create ll lv lrl) lrv (create lrr v r)
 end
 end else if hr > hl + 2 then begin
 match r with
 Empty > invalid_arg "Set.bal"
  Node(rl, rv, rr, _) >
 if height rr >= height rl then
 create (create l v rl) rv rr
 else begin
 match rl with
 Empty > invalid_arg "Set.bal"
  Node(rll, rlv, rlr, _) >
 create (create l v rll) rlv (create rlr rv rr)
 end
 end else
 Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))

 let rec add x = function
 Empty > Node(Empty, x, Empty, 1)
  Node(l, v, r, _) as t >
 let c = compare x v in
 if c = 0 then t else
 if c < 0 then bal (add x l) v r else bal l v (add x r)

 let rec min_elt = function
 Empty > raise Not_found
  Node(Empty, v, r, _) > v
  Node(l, v, r, _) > min_elt l

 let rec remove_min_elt = function
 Empty > invalid_arg "Set.remove_min_elt"
  Node(Empty, v, r, _) > r
  Node(l, v, r, _) > bal (remove_min_elt l) v r

 let merge t1 t2 =
 match (t1, t2) with
 (Empty, t) > t
  (t, Empty) > t
  (_, _) > bal t1 (min_elt t2) (remove_min_elt t2)

 let rec join l v r =
 match (l, r) with
 (Empty, _) > add v r
  (_, Empty) > add v l
  (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) >
 if lh > rh + 2 then bal ll lv (join lr v r) else
 if rh > lh + 2 then bal (join l v rl) rv rr else
 create l v r

 let rec split x = function
 Empty >
 (Empty, false, Empty)
  Node(l, v, r, _) >
 let c = compare x v in
 if c = 0 then (l, true, r)
 else if c < 0 then
 let (ll, pres, rl) = split x l in (ll, pres, join rl v r)
 else
 let (lr, pres, rr) = split x r in (join l v lr, pres, rr)

 let rec union s1 s2 =
 match (s1, s2) with
 (Empty, t2) > t2
  (t1, Empty) > t1
  (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) >
 if h1 >= h2 then
 if h2 = 1 then add v2 s1 else begin
 let (l2, _, r2) = split v1 s2 in
 join (union l1 l2) v1 (union r1 r2)
 end
 else
 if h1 = 1 then add v1 s2 else begin
 let (l1, _, r1) = split v2 s1 in
 join (union l1 l2) v2 (union r1 r2)
 end

 let concat t1 t2 =
 match (t1, t2) with
 (Empty, t) > t
  (t, Empty) > t
  (_, _) > join t1 (min_elt t2) (remove_min_elt t2)

 let rec mem x = function
 Empty > false
  Node(l, v, r, _) >
 let c = compare x v in
 c = 0  mem x (if c < 0 then l else r)

 let rec for_all p = function
 Empty > true
  Node(l, v, r, _) > p v && for_all p l && for_all p r

 let rec exists p = function
 Empty > false
  Node(l, v, r, _) > p v  exists p l  exists p r

 let rec subset s1 s2 =
 match (s1, s2) with
 Empty, _ >
 true
  _, Empty >
 false
  Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) >
 let c = compare v1 v2 in
 if c = 0 then
 subset l1 l2 && subset r1 r2
 else if c < 0 then
 subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
 else
 subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2

 let rec diff s1 s2 =
 match (s1, s2) with
 (Empty, t2) > Empty
  (t1, Empty) > t1
  (Node(l1, v1, r1, _), t2) >
 match split v1 t2 with
 (l2, false, r2) >
 join (diff l1 l2) v1 (diff r1 r2)
  (l2, true, r2) >
 concat (diff l1 l2) (diff r1 r2)

 type 'a enumeration = End  More of 'a * 'a set * 'a enumeration

 let rec cons_enum s e =
 match s with
 Empty > e
  Node(l, v, r, _) > cons_enum l (More(v, r, e))

 let rec compare_aux e1 e2 =
 match (e1, e2) with
 (End, End) > 0
  (End, _) > 1
  (_, End) > 1
  (More(v1, r1, e1), More(v2, r2, e2)) >
 let c = compare v1 v2 in
 if c <> 0
 then c
 else compare_aux (cons_enum r1 e1) (cons_enum r2 e2)

 let compare s1 s2 =
 compare_aux (cons_enum s1 End) (cons_enum s2 End)

 let equal s1 s2 =
 compare s1 s2 = 0

 let matitabool_of_bool b = if b then Bool.True else Bool.False

(** val set_empty : 'a1 set0 **)
let set_empty = Empty

(** val set_member :
 ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set0 > Bool.bool **)
let set_member _ x s = matitabool_of_bool (mem x s)

(** val set_equal :
 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **)
let set_equal _ s1 s2 = matitabool_of_bool (equal s1 s2)

(** val set_diff : 'a1 set0 > 'a1 set0 > 'a1 set0 **)
let set_diff = diff

(** val set_singleton : 'a1 > 'a1 set0 **)
let set_singleton elt =
 add elt set_empty

(** val set_from_list : 'a1 List.list > 'a1 set0 **)
let set_from_list the_list =
 List.foldr add set_empty the_list

(** val set_subset :
 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **)
let set_subset _ s1 s2 = matitabool_of_bool (subset s1 s2)

(** val set_union : 'a1 set0 > 'a1 set0 > 'a1 set0 **)
let set_union = union
Index: tracted/set_adt.mli
===================================================================
 /extracted/set_adt.mli (revision 2737)
+++ (revision )
@@ 1,19 +1,0 @@
type 'x set

val set_empty : 'a1 set

val set_member : ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set > Bool.bool

val set_equal :
 ('a1 > 'a1 > Bool.bool) > 'a1 set > 'a1 set > Bool.bool

val set_diff : 'a1 set > 'a1 set > 'a1 set

val set_singleton : 'a1 > 'a1 set

val set_from_list : 'a1 List.list > 'a1 set

val set_subset :
 ('a1 > 'a1 > Bool.bool) > 'a1 set > 'a1 set > Bool.bool

val set_union : 'a1 set > 'a1 set > 'a1 set
Index: /extracted/untrusted/Fix.ml
===================================================================
 /extracted/untrusted/Fix.ml (revision 2738)
+++ /extracted/untrusted/Fix.ml (revision 2738)
@@ 0,0 +1,529 @@
+(**************************************************************************)
+(* *)
+(* Fix *)
+(* *)
+(* Author: François Pottier, INRIA ParisRocquencourt *)
+(* Version: 20091201 *)
+(* *)
+(* The copyright to this code is held by Institut National de Recherche *)
+(* en Informatique et en Automatique (INRIA). All rights reserved. This *)
+(* file is distributed under the license CeCILLC (see file LICENSE). *)
+(* *)
+(**************************************************************************)
+
+(*  *)
+
+(* Maps. *)
+
+(* We require imperative maps, that is, maps that can be updated in place.
+ An implementation of persistent maps, such as the one offered by ocaml's
+ standard library, can easily be turned into an implementation of imperative
+ maps, so this is a weak requirement. *)
+
+module type IMPERATIVE_MAPS = sig
+ type key
+ type 'data t
+ val create: unit > 'data t
+ val clear: 'data t > unit
+ val add: key > 'data > 'data t > unit
+ val find: key > 'data t > 'data
+ val iter: (key > 'data > unit) > 'data t > unit
+end
+
+(*  *)
+
+(* Properties. *)
+
+(* Properties must form a partial order, equipped with a least element, and
+ must satisfy the ascending chain condition: every monotone sequence
+ eventually stabilizes. *)
+
+(* [is_maximal] determines whether a property [p] is maximal with respect to
+ the partial order. Only a conservative check is required: in any event, it
+ is permitted for [is_maximal p] to return [false]. If [is_maximal p]
+ returns [true], then [p] must have no upper bound other than itself. In
+ particular, if properties form a lattice, then [p] must be the top
+ element. This feature, not described in the paper, enables a couple of
+ minor optimizations. *)
+
+module type PROPERTY = sig
+ type property
+ val bottom: property
+ val equal: property > property > bool
+ val is_maximal: property > bool
+end
+
+(*  *)
+
+(* The dynamic dependency graph. *)
+
+(* An edge from [node1] to [node2] means that [node1] depends on [node2], or
+ (equivalently) that [node1] observes [node2]. Then, an update of the
+ current property at [node2] causes a signal to be sent to [node1]. A node
+ can observe itself. *)
+
+(* This module could be placed in a separate file, but is included here in
+ order to make [Fix] selfcontained. *)
+
+module Graph : sig
+
+ (* This module provides a data structure for maintaining and modifying
+ a directed graph. Each node is allowed to carry a piece of client
+ data. There are functions for creating a new node, looking up a
+ node's data, looking up a node's predecessors, and setting or
+ clearing a node's successors (all at once). *)
+ type 'data node
+
+ (* [create data] creates a new node, with no incident edges, with
+ client information [data]. Time complexity: constant. *)
+ val create: 'data > 'data node
+
+ (* [data node] returns the client information associated with
+ the node [node]. Time complexity: constant. *)
+ val data: 'data node > 'data
+
+ (* [predecessors node] returns a list of [node]'s predecessors.
+ Amortized time complexity: linear in the length of the output
+ list. *)
+ val predecessors: 'data node > 'data node list
+
+ (* [set_successors src dsts] creates an edge from the node [src] to
+ each of the nodes in the list [dsts]. Duplicate elements in the
+ list [dsts] are removed, so that no duplicate edges are created. It
+ is assumed that [src] initially has no successors. Time complexity:
+ linear in the length of the input list. *)
+ val set_successors: 'data node > 'data node list > unit
+
+ (* [clear_successors node] removes all of [node]'s outgoing edges.
+ Time complexity: linear in the number of edges that are removed. *)
+ val clear_successors: 'data node > unit
+
+ (* That's it. *)
+end
+= struct
+
+ (* Using doublylinked adjacency lists, one could implement [predecessors]
+ in worstcase linear time with respect to the length of the output list,
+ [set_successors] in worstcase linear time with respect to the length of
+ the input list, and [clear_successors] in worstcase linear time with
+ respect to the number of edges that are removed. We use a simpler
+ implementation, based on singlylinked adjacency lists, with deferred
+ removal of edges. It achieves the same complexity bounds, except
+ [predecessors] only offers an amortized complexity bound. This is good
+ enough for our purposes, and, in practice, is more efficient by a
+ constant factor. This simplification was suggested by Arthur
+ Charguéraud. *)
+
+ type 'data node = {
+
+ (* The client information associated with this node. *)
+
+ data: 'data;
+
+ (* This node's incoming and outgoing edges. *)
+
+ mutable outgoing: 'data edge list;
+ mutable incoming: 'data edge list;
+
+ (* A transient mark, always set to [false], except when checking
+ against duplicate elements in a successor list. *)
+
+ mutable marked: bool;
+
+ }
+
+ and 'data edge = {
+
+ (* This edge's nodes. Edges are symmetric: source and destination
+ are not distinguished. Thus, an edge appears both in the outgoing
+ edge list of its source node and in the incoming edge list of its
+ destination node. This allows edges to be easily marked as
+ destroyed. *)
+
+ node1: 'data node;
+ node2: 'data node;
+
+ (* Edges that are destroyed are marked as such, but are not
+ immediately removed from the adjacency lists. *)
+
+ mutable destroyed: bool;
+
+ }
+
+ let create (data : 'data) : 'data node = {
+ data = data;
+ outgoing = [];
+ incoming = [];
+ marked = false;
+ }
+
+ let data (node : 'data node) : 'data =
+ node.data
+
+ (* [follow src edge] returns the node that is connected to [src]
+ by [edge]. Time complexity: constant. *)
+
+ let follow src edge =
+ if edge.node1 == src then
+ edge.node2
+ else begin
+ assert (edge.node2 == src);
+ edge.node1
+ end
+
+ (* The [predecessors] function removes edges that have been marked
+ destroyed. The cost of removing these has already been paid for,
+ so the amortized time complexity of [predecessors] is linear in
+ the length of the output list. *)
+
+ let predecessors (node : 'data node) : 'data node list =
+ let predecessors = OcamlList.filter (fun edge > not edge.destroyed) node.incoming in
+ node.incoming < predecessors;
+ OcamlList.map (follow node) predecessors
+
+ (* [link src dst] creates a new edge from [src] to [dst], together
+ with its reverse edge. Time complexity: constant. *)
+
+ let link (src : 'data node) (dst : 'data node) : unit =
+ let edge = {
+ node1 = src;
+ node2 = dst;
+ destroyed = false;
+ } in
+ src.outgoing < edge :: src.outgoing;
+ dst.incoming < edge :: dst.incoming
+
+ let set_successors (src : 'data node) (dsts : 'data node list) : unit =
+ assert (src.outgoing = []);
+ let rec loop = function
+  [] >
+ ()
+  dst :: dsts >
+ if dst.marked then
+ loop dsts (* skip duplicate elements *)
+ else begin
+ dst.marked < true;
+ link src dst;
+ loop dsts;
+ dst.marked < false
+ end
+ in
+ loop dsts
+
+ let clear_successors (node : 'data node) : unit =
+ OcamlList.iter (fun edge >
+ assert (not edge.destroyed);
+ edge.destroyed < true;
+ ) node.outgoing;
+ node.outgoing < []
+
+end
+
+(*  *)
+
+(* The code is parametric in an implementation of maps over variables and in
+ an implementation of properties. *)
+
+module Make
+ (M : IMPERATIVE_MAPS)
+ (P : PROPERTY)
+= struct
+
+type variable =
+ M.key
+
+type property =
+ P.property
+
+type valuation =
+ variable > property
+
+type rhs =
+ valuation > property
+
+type equations =
+ variable > rhs
+
+(*  *)
+
+(* Data. *)
+
+(* Each node in the dependency graph carries information about a fixed
+ variable [v]. *)
+
+type node =
+ data Graph.node
+
+and data = {
+
+ (* This is the result of the application of [rhs] to the variable [v]. It
+ must be stored in order to guarantee that this application is performed
+ at most once. *)
+ rhs: rhs;
+
+ (* This is the current property at [v]. It evolves monotonically with
+ time. *)
+ mutable property: property;
+
+ (* That's it! *)
+}
+
+(* [property node] returns the current property at [node]. *)
+
+let property node =
+ (Graph.data node).property
+
+(*  *)
+
+(* Many definitions must be made within the body of the function [lfp].
+ For greater syntactic convenience, we place them in a local module. *)
+
+let lfp (eqs : equations) : valuation =
+ let module LFP = struct
+
+(*  *)
+
+(* The workset. *)
+
+(* When the algorithm is inactive, the workset is empty. *)
+
+(* Our workset is based on a Queue, but it could just as well be based on a
+ Stack. A textual replacement is possible. It could also be based on a
+ priority queue, provided a sensible way of assigning priorities could
+ be found. *)
+
+module Workset : sig
+
+ (* [insert node] inserts [node] into the workset. [node] must have no
+ successors. *)
+ val insert: node > unit
+
+ (* [repeat f] repeatedly applies [f] to a node extracted out of the
+ workset, until the workset becomes empty. [f] is allowed to use
+ [insert]. *)
+ val repeat: (node > unit) > unit
+
+ (* That's it! *)
+end
+= struct
+
+ (* Initialize the workset. *)
+
+ let workset =
+ Queue.create()
+
+ let insert node =
+ Queue.push node workset
+
+ let repeat f =
+ while not (Queue.is_empty workset) do
+ f (Queue.pop workset)
+ done
+
+end
+
+(*  *)
+
+(* Signals. *)
+
+(* A node in the workset has no successors. (It can have predecessors.) In
+ other words, a predecessor (an observer) of some node is never in the
+ workset. Furthermore, a node never appears twice in the workset. *)
+
+(* When a variable broadcasts a signal, all of its predecessors (observers)
+ receive the signal. Any variable that receives the signal loses all of its
+ successors (that is, it ceases to observe anything) and is inserted into
+ the workset. This preserves the above invariant. *)
+
+let signal subject =
+ OcamlList.iter (fun observer >
+ Graph.clear_successors observer;
+ Workset.insert observer
+ ) (Graph.predecessors subject)
+ (* At this point, [subject] has no predecessors. This plays no role in
+ the correctness proof, though. *)
+
+(*  *)
+
+(* Tables. *)
+
+(* The permanent table maps variables that have reached a fixed point
+ to properties. It persists forever. *)
+
+let permanent : property M.t =
+ M.create()
+
+(* The transient table maps variables that have not yet reached a
+ fixed point to nodes. (A node contains not only a property, but
+ also a memoized righthand side, and carries edges.) At the
+ beginning of a run, it is empty. It fills up during a run. At the
+ end of a run, it is copied into the permanent table and cleared. *)
+
+let transient : node M.t =
+ M.create()
+
+(* [freeze()] copies the transient table into the permanent table, and
+ empties the transient table. This allows all nodes to be reclaimed
+ by the garbage collector. *)
+
+let freeze () =
+ M.iter (fun v node >
+ M.add v (property node) permanent
+ ) transient;
+ M.clear transient
+
+(*  *)
+
+(* Workset processing. *)
+
+
+(* [solve node] reevaluates the righthand side at [node]. If this leads to
+ a change, then the current property is updated, and [node] emits a signal
+ towards its observers. *)
+
+(* When [solve node] is invoked, [node] has no subjects. Indeed, when [solve]
+ is invoked by [node_for], [node] is newly created; when [solve] is invoked by
+ [Workset.repeat], [node] has just been extracted out of the workset, and a
+ node in the workset has no subjects. *)
+
+(* [node] must not be in the workset. *)
+
+(* In short, when [solve node] is invoked, [node] is neither awake nor asleep.
+ When [solve node] finishes, [node] is either awake or asleep again. (Chances
+ are, it is asleep, unless it is its own observer; then, it is awakened by the
+ final call to [signal node].) *)
+
+let rec solve (node : node) : unit =
+
+ (* Retrieve the data record carried by this node. *)
+ let data = Graph.data node in
+
+ (* Prepare to compute an updated value at this node. This is done by
+ invoking the client's righthand side function. *)
+
+ (* The flag [alive] is used to prevent the client from invoking [request]
+ after this interaction phase is over. In theory, this dynamic check seems
+ required in order to argue that [request] behaves like a pure function.
+ In practice, this check is not very useful: only a bizarre client would
+ store a [request] function and invoke it after it has become stale. *)
+ let alive = ref true
+ and subjects = ref [] in
+
+ (* We supply the client with [request], a function that provides access to
+ the current valuation, and dynamically records dependencies. This yields
+ a set of dependencies that is correct by construction. *)
+ let request (v : variable) : property =
+ assert !alive;
+ try
+ M.find v permanent
+ with Not_found >
+ let subject = node_for v in
+ let p = property subject in
+ if not (P.is_maximal p) then
+ subjects := subject :: !subjects;
+ p
+ in
+
+ (* Give control to the client. *)
+ let new_property = data.rhs request in
+
+ (* From now on, prevent any invocation of this instance of [request]
+ the client. *)
+ alive := false;
+
+ (* At this point, [node] has no subjects, as noted above. Thus, the
+ precondition of [set_successors] is met. We can install [data.subjects]
+ as the new set of subjects for this node. *)
+
+ (* If we have gathered no subjects in the list [data.subjects], then
+ this node must have stabilized. If [new_property] is maximal,
+ then this node must have stabilized. *)
+
+ (* If this node has stabilized, then it need not observe any more, so the
+ call to [set_successors] is skipped. In practice, this seems to be a
+ minor optimization. In the particular case where every node stabilizes at
+ the very first call to [rhs], this means that no edges are ever
+ built. This particular case is unlikely, as it means that we are just
+ doing memoization, not a true fixed point computation. *)
+
+ (* One could go further and note that, if this node has stabilized, then it
+ could immediately be taken out of the transient table and copied into the
+ permanent table. This would have the beneficial effect of allowing the
+ detection of further nodes that have stabilized. Furthermore, it would
+ enforce the property that no node in the transient table has a maximal
+ value, hence the call to [is_maximal] above would become useless. *)
+
+ if not (!subjects = []  P.is_maximal new_property) then
+ Graph.set_successors node !subjects;
+
+ (* If the updated value differs from the previous value, record
+ the updated value and send a signal to all observers of [node]. *)
+ if not (P.equal data.property new_property) then begin
+ data.property < new_property;
+ signal node
+ end
+ (* Note that equality of the two values does not imply that this node has
+ stabilized forever. *)
+
+(*  *)
+
+(* [node_for v] returns the graph node associated with the variable [v]. It is
+ assumed that [v] does not appear in the permanent table. If [v] appears in
+ the transient table, the associated node is returned. Otherwise, [v] is a
+ newly discovered variable: a new node is created on the fly, and the
+ transient table is grown. The new node can either be inserted into the
+ workset (it is then awake) or handled immediately via a recursive call to
+ [solve] (it is then asleep, unless it observes itself). *)
+
+(* The recursive call to [solve node] can be replaced, if desired, by a call
+ to [Workset.insert node]. Using a recursive call to [solve] permits eager
+ topdown discovery of new nodes. This can save a constant factor, because
+ it allows new nodes to move directly from [bottom] to a good first
+ approximation, without sending any signals, since [node] has no observers
+ when [solve node] is invoked. In fact, if the dependency graph is acyclic,
+ the algorithm discovers nodes topdown, performs computation on the way
+ back up, and runs without ever inserting a node into the workset!
+ Unfortunately, this causes the stack to grow as deep as the longest path in
+ the dependency graph, which can blow up the stack. *)
+
+and node_for (v : variable) : node =
+ try
+ M.find v transient
+ with Not_found >
+ let node = Graph.create { rhs = eqs v; property = P.bottom } in
+ (* Adding this node to the transient table prior to calling [solve]
+ recursively is mandatory, otherwise [solve] might loop, creating
+ an infinite number of nodes for the same variable. *)
+ M.add v node transient;
+ solve node; (* or: Workset.insert node *)
+ node
+
+(*  *)
+
+(* Invocations of [get] trigger the fixed point computation. *)
+
+(* The flag [inactive] prevents reentrant calls by the client. *)
+
+let inactive =
+ ref true
+
+let get (v : variable) : property =
+ try
+ M.find v permanent
+ with Not_found >
+ assert !inactive;
+ inactive := false;
+ let node = node_for v in
+ Workset.repeat solve;
+ freeze();
+ inactive := true;
+ property node
+
+(*  *)
+
+(* Close the local module [LFP]. *)
+
+end
+in LFP.get
+
+end
Index: /extracted/untrusted/Fix.mli
===================================================================
 /extracted/untrusted/Fix.mli (revision 2738)
+++ /extracted/untrusted/Fix.mli (revision 2738)
@@ 0,0 +1,103 @@
+
+(** This module provides a generic algorithm to compute the least
+ solution of a system of monotonic equations. *)
+
+(**************************************************************************)
+(* *)
+(* Fix *)
+(* *)
+(* Author: François Pottier, INRIA ParisRocquencourt *)
+(* Version: 20091201 *)
+(* *)
+(* The copyright to this code is held by Institut National de Recherche *)
+(* en Informatique et en Automatique (INRIA). All rights reserved. This *)
+(* file is distributed under the license CeCILLC (see file LICENSE). *)
+(* *)
+(**************************************************************************)
+
+(* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)
+
+(*  *)
+
+(* Maps. *)
+
+(* We require imperative maps, that is, maps that can be updated in place.
+ An implementation of persistent maps, such as the one offered by ocaml's
+ standard library, can easily be turned into an implementation of imperative
+ maps, so this is a weak requirement. *)
+
+module type IMPERATIVE_MAPS = sig
+ type key
+ type 'data t
+ val create: unit > 'data t
+ val clear: 'data t > unit
+ val add: key > 'data > 'data t > unit
+ val find: key > 'data t > 'data
+ val iter: (key > 'data > unit) > 'data t > unit
+end
+
+(*  *)
+
+(* Properties. *)
+
+(* Properties must form a partial order, equipped with a least element, and
+ must satisfy the ascending chain condition: every monotone sequence
+ eventually stabilizes. *)
+
+(* [is_maximal] determines whether a property [p] is maximal with respect to
+ the partial order. Only a conservative check is required: in any event, it
+ is permitted for [is_maximal p] to return [false]. If [is_maximal p]
+ returns [true], then [p] must have no upper bound other than itself. In
+ particular, if properties form a lattice, then [p] must be the top
+ element. This feature, not described in the paper, enables a couple of
+ minor optimizations. *)
+
+module type PROPERTY = sig
+ type property
+ val bottom: property
+ val equal: property > property > bool
+ val is_maximal: property > bool
+end
+
+(*  *)
+
+(* The code is parametric in an implementation of maps over variables and in
+ an implementation of properties. *)
+
+module Make
+ (M : IMPERATIVE_MAPS)
+ (P : PROPERTY)
+ : sig
+ type variable = M.key
+ type property = P.property
+
+ (* A valuation is a mapping of variables to properties. *)
+ type valuation = variable > property
+
+ (* A righthand side, when supplied with a valuation that gives
+ meaning to its free variables, evaluates to a property. More
+ precisely, a righthand side is a monotone function of
+ valuations to properties. *)
+ type rhs = valuation > property
+
+ (* A system of equations is a mapping of variables to righthand
+ sides. *)
+ type equations = variable > rhs
+
+ (* [lfp eqs] produces the least solution of the system of monotone
+ equations [eqs]. *)
+
+ (* It is guaranteed that, for each variable [v], the application [eqs v] is
+ performed at most once (whereas the righthand side produced by this
+ application is, in general, evaluated multiple times). This guarantee can
+ be used to perform costly precomputation, or memory allocation, when [eqs]
+ is applied to its first argument. *)
+
+ (* When [lfp] is applied to a system of equations [eqs], it performs no
+ actual computation. It produces a valuation, [get], which represents
+ the least solution of the system of equations. The actual fixed point
+ computation takes place, on demand, when [get] is applied. *)
+ val lfp: equations > valuation
+ end
+
+(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
Index: /extracted/untrusted/coloring.ml
===================================================================
 /extracted/untrusted/coloring.ml (revision 2738)
+++ /extracted/untrusted/coloring.ml (revision 2738)
@@ 0,0 +1,376 @@
+(* Pasted from Pottier's PP compiler *)
+
+open ERTL
+open Untrusted_interference
+open Printf
+
+(*  *)
+(* Decisions. *)
+
+(* A decision is of the form either [Spill]  the vertex could
+ not be colored and should be spilled into a stack slot  or
+ [Color]  the vertex was assigned a hardware register. *)
+
+type decision =
+  Spill
+  Color of I8051.register
+
+(*
+(* [print_decision] turns a decision into a string. *)
+
+let print_decision = function
+  Spill >
+ "spilled"
+  Color hwr >
+ Printf.sprintf "colored $%s" (I8051.print_register hwr)
+*)
+
+(*  *)
+(* Colorings. *)
+
+(* A coloring is a partial function of graph vertices to decisions.
+ Vertices that are not in the domain of the coloring are waiting for
+ a decision to be made. *)
+
+type coloring =
+ decision Vertex.Map.t
+
+(*  *)
+(* Sets of colors. *)
+
+module ColorSet =
+ HwRegisterSet
+
+(* [add_color coloring r colors] returns the union of the set [colors] with
+ the element [color], if the vertex [r] was assigned color [color], and
+ returns [colors] if [r] was spilled. *)
+
+let add_color coloring r colors =
+ match Vertex.Map.find r coloring with
+  Spill >
+ colors
+  Color color >
+ ColorSet.add color colors
+
+(* These are the colors that we work with. *)
+
+let colors : ColorSet.t =
+ List.foldr
+ (fun reg set > HwRegisterSet.add reg set)
+ HwRegisterSet.empty I8051.registersAllocatable
+
+(* This is the number of available colors. *)
+
+let k : int =
+ ColorSet.cardinal colors
+
+(*  *)
+(* Choices of colors. *)
+
+(* [forbidden_colors graph coloring v] is the set of colors that cannot be
+ assigned to [v] considering [coloring], a coloring of every vertex in
+ [graph] except [v]. *)
+(* This takes into account [v]'s possible interferences with hardware
+ registers, which are viewed as forbidden colors. *)
+
+let forbidden_colors graph coloring v =
+ Vertex.Set.fold (add_color coloring) (ipp graph v) (iph graph v)
+
+(*  *)
+(* Low and high vertices. *)
+
+(* A vertex is low (or insignificant) if its degree is less than [k].
+ It is high (or significant) otherwise. *)
+
+let high graph v =
+ degree graph v >= k
+
+(* [high_neighbors graph v] is the set of all high neighbors of [v]. *)
+
+let high_neighbors graph v =
+ Vertex.Set.filter (high graph) (ipp graph v)
+
+(*  *)
+(* George's conservative coalescing criterion. *)
+
+(* According to this criterion, two vertices [a] and [b] can be
+ coalesced, suppressing [a] and keeping [b], if the following
+ two conditions hold:
+
+ 1. (pseudoregisters) every high neighbor of [a] is a neighbor of [b];
+ 2. (hardware registers) every hardware register that interferes with
+ [a] also interferes with [b].
+
+ This means that, after all low vertices have been removed, any color that
+ is suitable for [b] is also suitable for [a]. *)
+
+let georgepp graph (a, b) =
+ Vertex.Set.subset (high_neighbors graph a) (ipp graph b) &&
+ HwRegisterSet.subset (iph graph a) (iph graph b)
+
+(* According to this criterion, a vertex [a] and a hardware register
+ [c] can be coalesced (that is, [a] can be assigned color [c]) if
+ every high neighbor of [a] interferes with [c]. *)
+
+let georgeph graph (a, c) =
+ Vertex.Set.fold (fun neighbor accu >
+ accu &&
+ HwRegisterSet.mem c (iph graph neighbor)
+ ) (high_neighbors graph a) true
+
+(*  *)
+(* Here is the coloring algorithm. *)
+
+module Color (G : sig
+
+ val graph: graph
+ val uses: Registers.register > int
+ val verbose: bool
+
+end) = struct
+
+ (* The cost function heuristically evaluates how much it might cost
+ to spill vertex [v]. Here, the cost is the ratio of the number of
+ uses of the pseudoregisters represented by [v] by the degree of
+ [v]. One could also take into account the number of nested loops
+ that the uses appear within, but that is not done here. *)
+
+ let cost graph v =
+ let uses =
+ Pset.fold (fun r uses >
+ G.uses r + uses
+ ) (registers graph v) 0
+ in
+ (float_of_int uses) /. (float_of_int (degree graph v))
+
+ (* The algorithm maintains a transformed graph as it runs. It is
+ obtained from the original graph by removing, coalescing, and
+ freezing vertices. *)
+
+ (* Each of the functions that follow returns a coloring of the graph
+ that it is passed. These functions correspond to the various
+ states of the algorithm (simplification, coalescing, freezing,
+ spilling, selection). The function [simplification] is the
+ initial state. *)
+
+ (* [simplification] removes nonmoverelated nodes of low degree. *)
+
+ let rec simplification graph : coloring =
+
+ match lowest_non_move_related graph with
+
+  Some (v, d) when d < k >
+
+ (* We found a nonmoverelated node [v] of low degree. Color
+ the rest of the graph, then color [v]. This is what I call
+ selection. *)
+
+(*
+ if G.verbose then
+ printf "Simplifying low vertex: %s.\n%!" (print_vertex graph v);
+*)
+
+ selection graph v
+
+  _ >
+
+ (* There are no nonmoverelated nodes of low degree.
+ Could not simplify further. Start coalescing. *)
+
+ coalescing graph
+
+ (* [coalescing] looks for a preference edge that can be collapsed.
+ It is called after [simplification], so it is known, at this
+ point, that all nodes of low degree are moverelated. *)
+
+ and coalescing graph : coloring =
+
+ (* Find a preference edge between two vertices that passes
+ George's criterion.
+
+ [pppick] examines all preference edges in the graph, so its use
+ is inefficient. It would be more efficient instead to examine
+ only areas of the graph that have changed recently. More
+ precisely, it is useless to reexamine a preference edge that
+ did not pass George's criterion the last time it was examined
+ and whose neighborhood has not been modified by simplification,
+ coalescing or freezing. Indeed, in that case, and with a
+ sufficiently large definition of ``neighborhood'', this edge is
+ guaranteed to again fail George's criterion. It would be
+ possible to modify the [Interference.graph] data structure so
+ as to keep track of which neighborhoods have been modified and
+ provide a specialized, more efficient version of [pppick]. This
+ is not done here. *)
+
+ match pppick graph (georgepp graph) with
+
+  Some (a, b) >
+
+(*
+ if G.verbose then
+ printf "Coalescing %s with %s.\n%!" (print_vertex graph a) (print_vertex graph b);
+*)
+
+ (* Coalesce [a] with [b] and color the remaining graph. *)
+
+ let coloring = simplification (coalesce graph a b) in
+
+ (* Assign [a] the same color as [b]. *)
+
+ Vertex.Map.add a (Vertex.Map.find b coloring) coloring
+
+  None >
+
+ (* Find a preference edge between a vertex and a hardware
+ register that passes George's criterion. Like [pppick],
+ [phpick] is slow. *)
+
+ match phpick graph (georgeph graph) with
+
+  Some (a, c) >
+
+(*
+ if G.verbose then
+ printf "Coalescing %s with $%s.\n%!" (print_vertex graph a) (I8051.print_register c);
+*)
+
+ (* Coalesce [a] with [c] and color the remaining graph. *)
+
+ let coloring = simplification (coalesceh graph a c) in
+
+ (* Assign [a] the color [c]. *)
+
+ Vertex.Map.add a (Color c) coloring
+
+  None >
+
+ (* Could not coalesce further. Start freezing. *)
+
+ freezing graph
+
+ (* [freezing] begins after [simplification] and [coalescing] are
+ finished, so it is known, at this point, that all nodes of low
+ degree are moverelated and no coalescing is possible. [freezing]
+ looks for a node of low degree (which must be moverelated) and
+ removes the preference edges that it carries. This potentially
+ opens new opportunities for simplification and coalescing. *)
+
+ and freezing graph : coloring =
+
+ match lowest graph with
+
+  Some (v, d) when d < k >
+
+ (* We found a moverelated node [v] of low degree.
+ Freeze it and start over. *)
+
+(*
+ if G.verbose then
+ printf "Freezing low vertex: %s.\n%!" (print_vertex graph v);
+*)
+
+ simplification (freeze graph v)
+
+  _ >
+
+ (* Could not freeze further. Start spilling. *)
+
+ spilling graph
+
+ (* [spilling] begins after [simplification], [coalescing], and
+ [freezing] are finished, so it is known, at this point, that
+ there are no nodes of low degree.
+
+ Thus, we are facing a potential spill. However, we do optimistic
+ coloring: we do not spill a vertex right away, but proceed
+ normally, just as if we were doing simplification. So, we pick a
+ vertex [v], remove it, and check whether a color can be assigned
+ to [v] only after coloring what remains of the graph.
+
+ It is crucial to pick a vertex that has few uses in the code. It
+ would also be good to pick one that has high degree, as this will
+ help color the rest of the graph. Thus, we pick a vertex that has
+ minimum cost, where the cost is obtained as the ratio of the
+ number of uses of the pseudoregisters represented by this vertex
+ in the code by the degree of the vertex. One could also take into
+ account the number of nested loops that the uses appear within,
+ but that is not done here.
+
+ The use of [minimum] is inefficient, because this function
+ examines all vertices in the graph. It would be possible to
+ augment the [Interference.graph] data structure so as to keep
+ track of the cost associated with each vertex and provide
+ efficient access to a minimum cost vertex. This is not done
+ here. *)
+
+ and spilling graph : coloring =
+
+ match minimum (cost graph) graph with
+  Some v >
+
+(*
+ if G.verbose then
+ printf "Spilling high vertex: %s.\n%!" (print_vertex graph v);
+*)
+
+ selection graph v
+
+  None >
+
+ (* The graph is empty. Return an empty coloring. *)
+
+ Vertex.Map.empty
+
+ (* [selection] removes the vertex [v] from the graph, colors the
+ remaining graph, then selects a color for [v].
+
+ If [v] is low, that is, if [v] has degree less than [k], then at
+ least one color must still be available for [v], regardless of
+ how the remaining graph was colored.
+
+ If [v] was a potential spill, then it is not certain that a color
+ is still available. If one is, though, then we are rewarded for
+ being optimistic. If none is, then [v] becomes an actual
+ spill. *)
+
+ and selection graph v : coloring =
+
+ (* Remove [v] from the graph and color what remains. *)
+
+ let coloring = simplification (remove graph v) in
+
+ (* Determine which colors are allowed. *)
+
+ let allowed = ColorSet.diff colors (forbidden_colors graph coloring v) in
+
+ (* Make a decision.
+
+ We pick a color randomly among those that are allowed. One could
+ attempt to use biased coloring, that is, to pick a color that seems
+ desirable (or not undesirable) according to the preference edges
+ found in the initial graph. But that is probably not worth the
+ trouble. *)
+
+ let decision =
+ try
+ Color (ColorSet.choose allowed)
+ with Not_found >
+ Spill
+ in
+
+(*
+ if G.verbose then
+ printf "Decision concerning %s: %s.\n%!" (print_vertex graph v) (print_decision decision);
+*)
+
+ (* Record our decision and return. *)
+
+ Vertex.Map.add v decision coloring
+
+ (* Run the algorithm. *)
+
+ let coloring =
+ simplification G.graph
+
+end
+
Index: /extracted/untrusted/coloring.mli
===================================================================
 /extracted/untrusted/coloring.mli (revision 2738)
+++ /extracted/untrusted/coloring.mli (revision 2738)
@@ 0,0 +1,38 @@
+(* Pasted from Pottier's PP compiler *)
+
+(** This module performs graph coloring. It is used for register
+ allocation. *)
+
+(* A coloring is a partial function of graph vertices to decisions,
+ where a decision is of the form either [Spill]  the vertex could
+ not be colored and should be spilled into a stack slot  or
+ [Color]  the vertex was assigned a hardware register. Vertices
+ that are not in the domain of the coloring are waiting for a
+ decision to be made. *)
+
+type decision =
+  Spill
+  Color of I8051.register
+
+type coloring =
+ decision Untrusted_interference.Vertex.Map.t
+
+(* Here is the coloring algorithm. Out of an interference graph, it
+ produces a coloring. The client should provide information about
+ the number of uses of each pseudoregister; the higher the number,
+ the more undesirable it is to spill that pseudoregister. If the
+ [verbose] flag is set, the algorithm prints information messages to
+ the standard output channel. *)
+
+module Color (G : sig
+
+ val graph: Untrusted_interference.graph
+ val uses: Registers.register > int
+ val verbose: bool
+
+end) : sig
+
+ val coloring: coloring
+
+end
+
Index: /extracted/untrusted/compute_colouring.ml
===================================================================
 /extracted/untrusted/compute_colouring.ml (revision 2738)
+++ /extracted/untrusted/compute_colouring.ml (revision 2738)
@@ 0,0 +1,3 @@
+(* We try first with a stupid colourer: we spill everything *)
+
+let colour_graph graph = assert false
Index: /extracted/untrusted/compute_colouring.mli
===================================================================
 /extracted/untrusted/compute_colouring.mli (revision 2738)
+++ /extracted/untrusted/compute_colouring.mli (revision 2738)
@@ 0,0 +1,1 @@
+val colour_graph : Interference.coloured_graph_computer
Index: /extracted/untrusted/compute_fixpoints.ml
===================================================================
 /extracted/untrusted/compute_fixpoints.ml (revision 2738)
+++ /extracted/untrusted/compute_fixpoints.ml (revision 2738)
@@ 0,0 +1,35 @@
+module Label_ImperativeMap = struct
+
+ type key = Graphs.label
+
+ type 'data t = 'data Graphs.graph ref
+
+ let create () = ref (Identifiers.empty_map PreIdentifiers.LabelTag)
+
+ let clear t =
+ t := Identifiers.empty_map PreIdentifiers.LabelTag
+
+ let add k d t =
+ t := Identifiers.add PreIdentifiers.LabelTag !t k d
+
+ let find k t =
+ match Identifiers.lookup0 PreIdentifiers.LabelTag !t k with
+ Types.Some res > res
+  Types.None > raise Not_found
+
+ let iter f t =
+ Identifiers.foldi0 PreIdentifiers.LabelTag (fun k v () > f k v) !t ()
+
+end
+
+(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
+let compute_fixpoint latt =
+ let module L : Fix.PROPERTY with type property = Preamble.__ =
+ struct
+ type property = Preamble.__
+ let bottom = Fixpoints.l_bottom latt
+ let equal x y = Fixpoints.l_equal latt x y = Bool.True
+ let is_maximal x = Fixpoints.l_is_maximal latt x = Bool.True
+ end in
+ let module F = Fix.Make (Label_ImperativeMap) (L) in
+ F.lfp
Index: /extracted/untrusted/compute_fixpoints.mli
===================================================================
 /extracted/untrusted/compute_fixpoints.mli (revision 2738)
+++ /extracted/untrusted/compute_fixpoints.mli (revision 2738)
@@ 0,0 +1,1 @@
+val compute_fixpoint : Fixpoints.fixpoint_computer
Index: /extracted/untrusted/glue.ml
===================================================================
 /extracted/untrusted/glue.ml (revision 2738)
+++ /extracted/untrusted/glue.ml (revision 2738)
@@ 0,0 +1,11 @@
+let int_of_bitvector v =
+ let rec aux pow v =
+ match v with
+ Vector.VEmpty > 0
+  Vector.VCons (_,hd,tl) >
+ if hd = Bool.True then
+ pow + (aux (pow * 2) tl)
+ else
+ aux (pow * 2) tl
+ in
+ aux 1 (Vector.reverse0 Nat.O v)
Index: /extracted/untrusted/glue.mli
===================================================================
 /extracted/untrusted/glue.mli (revision 2738)
+++ /extracted/untrusted/glue.mli (revision 2738)
@@ 0,0 +1,1 @@
+val int_of_bitvector : BitVector.bitVector > int
Index: /extracted/untrusted/myMap.ml
===================================================================
 /extracted/untrusted/myMap.ml (revision 2738)
+++ /extracted/untrusted/myMap.ml (revision 2738)
@@ 0,0 +1,372 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking described in file ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: myMap.ml,v 1.3 2006/02/17 16:19:52 pottier Exp $ *)
+
+module type OrderedType =
+ sig
+ type t
+ val compare: t > t > int
+ end
+
+module type S =
+ sig
+ type key
+ type +'a t
+ val empty: 'a t
+ val is_empty: 'a t > bool
+ val add: key > 'a > 'a t > 'a t
+ val find: key > 'a t > 'a
+ val remove: key > 'a t > 'a t
+ val mem: key > 'a t > bool
+ val iter: (key > 'a > unit) > 'a t > unit
+ val map: ('a > 'b) > 'a t > 'b t
+ val mapi: (key > 'a > 'b) > 'a t > 'b t
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ val compare: ('a > 'a > int) > 'a t > 'a t > int
+ val equal: ('a > 'a > bool) > 'a t > 'a t > bool
+ type interval = key option * key option
+ val split: interval > 'a t > 'a t
+ val minimum: 'a t > key * 'a
+ val find_remove: key > 'a t > 'a * 'a t
+ val update: key > ('a > 'a) > 'a t > 'a t
+ val restrict: (key > bool) > 'a t > 'a t
+ end
+
+module Make(Ord: OrderedType) = struct
+
+ type key = Ord.t
+
+ type 'a t =
+ Empty
+  Node of 'a t * key * 'a * 'a t * int
+
+ let height = function
+ Empty > 0
+  Node(_,_,_,_,h) > h
+
+ let create l x d r =
+ let hl = height l and hr = height r in
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let bal l x d r =
+ let hl = match l with Empty > 0  Node(_,_,_,_,h) > h in
+ let hr = match r with Empty > 0  Node(_,_,_,_,h) > h in
+ if hl > hr + 2 then begin
+ match l with
+ Empty > invalid_arg "Map.bal"
+  Node(ll, lv, ld, lr, _) >
+ if height ll >= height lr then
+ create ll lv ld (create lr x d r)
+ else begin
+ match lr with
+ Empty > invalid_arg "Map.bal"
+  Node(lrl, lrv, lrd, lrr, _)>
+ create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+ end
+ end else if hr > hl + 2 then begin
+ match r with
+ Empty > invalid_arg "Map.bal"
+  Node(rl, rv, rd, rr, _) >
+ if height rr >= height rl then
+ create (create l x d rl) rv rd rr
+ else begin
+ match rl with
+ Empty > invalid_arg "Map.bal"
+  Node(rll, rlv, rld, rlr, _) >
+ create (create l x d rll) rlv rld (create rlr rv rd rr)
+ end
+ end else
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let empty = Empty
+
+ let is_empty = function Empty > true  _ > false
+
+ let rec add x data = function
+ Empty >
+ Node(Empty, x, data, Empty, 1)
+  Node(l, v, d, r, h) >
+ let c = Ord.compare x v in
+ if c = 0 then
+ Node(l, x, data, r, h)
+ else if c < 0 then
+ bal (add x data l) v d r
+ else
+ bal l v d (add x data r)
+
+ (* Same as create and bal, but no assumptions are made on the
+ relative heights of l and r. *)
+
+ let rec join l v d r =
+ match (l, r) with
+ (Empty, _) > add v d r
+  (_, Empty) > add v d l
+  (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) >
+ if lh > rh + 2 then bal ll lv ld (join lr v d r) else
+ if rh > lh + 2 then bal (join l v d rl) rv rd rr else
+ create l v d r
+
+ let rec find x = function
+ Empty >
+ raise Not_found
+  Node(l, v, d, r, _) >
+ let c = Ord.compare x v in
+ if c = 0 then d
+ else find x (if c < 0 then l else r)
+
+ let rec mem x = function
+ Empty >
+ false
+  Node(l, v, d, r, _) >
+ let c = Ord.compare x v in
+ c = 0  mem x (if c < 0 then l else r)
+
+ let rec min_binding = function
+ Empty > raise Not_found
+  Node(Empty, x, d, r, _) > (x, d)
+  Node(l, x, d, r, _) > min_binding l
+
+ let rec remove_min_binding = function
+ Empty > invalid_arg "Map.remove_min_elt"
+  Node(Empty, x, d, r, _) > r
+  Node(l, x, d, r, _) > bal (remove_min_binding l) x d r
+
+ let merge t1 t2 =
+ match (t1, t2) with
+ (Empty, t) > t
+  (t, Empty) > t
+  (_, _) >
+ let (x, d) = min_binding t2 in
+ bal t1 x d (remove_min_binding t2)
+
+ let rec remove x = function
+ Empty >
+ Empty
+  Node(l, v, d, r, h) >
+ let c = Ord.compare x v in
+ if c = 0 then
+ merge l r
+ else if c < 0 then
+ bal (remove x l) v d r
+ else
+ bal l v d (remove x r)
+
+ let rec iter f = function
+ Empty > ()
+  Node(l, v, d, r, _) >
+ iter f l; f v d; iter f r
+
+ let rec map f = function
+ Empty > Empty
+  Node(l, v, d, r, h) > Node(map f l, v, f d, map f r, h)
+
+ let rec mapi f = function
+ Empty > Empty
+  Node(l, v, d, r, h) > Node(mapi f l, v, f v d, mapi f r, h)
+
+ let rec fold f m accu =
+ match m with
+ Empty > accu
+  Node(l, v, d, r, _) >
+ fold f r (f v d (fold f l accu))
+
+ type 'a enumeration = End  More of key * 'a * 'a t * 'a enumeration
+
+ let rec cons_enum m e =
+ match m with
+ Empty > e
+  Node(l, v, d, r, _) > cons_enum l (More(v, d, r, e))
+
+ let compare cmp m1 m2 =
+ let rec compare_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) > 0
+  (End, _) > 1
+  (_, End) > 1
+  (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) >
+ let c = Ord.compare v1 v2 in
+ if c <> 0 then c else
+ let c = cmp d1 d2 in
+ if c <> 0 then c else
+ compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in compare_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ let equal cmp m1 m2 =
+ let rec equal_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) > true
+  (End, _) > false
+  (_, End) > false
+  (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) >
+ Ord.compare v1 v2 = 0 && cmp d1 d2 &&
+ equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
+ in equal_aux (cons_enum m1 End) (cons_enum m2 End)
+
+ (* Intervals for splitting. An interval consists of a lower bound
+ and an upper bound, each of which can be absent. A key is
+ considered to lie within the interval if it is both greater than
+ (or equal to) the lower bound (if present) and less than (or
+ equal to) the upper bound (if present). *)
+
+ type interval =
+ key option * key option
+
+ (* Splitting. split interval m returns a new map consisting of
+ all bindings in m whose keys are within interval. *)
+
+ let rec split ((lo, hi) as interval) = function
+ Empty >
+ Empty
+  Node(l, v, d, r, _) >
+ let clo = Ord.compare v lo in
+ if clo < 0 then
+ (* v < lo *)
+ split interval r
+ else if clo = 0 then
+ (* v = lo *)
+ add v d (splithi hi r)
+ else
+ (* v > lo *)
+ let chi = Ord.compare v hi in
+ if chi < 0 then
+ (* v < hi *)
+ join (splitlo lo l) v d (splithi hi r)
+ else if chi = 0 then
+ (* v = hi *)
+ add v d (splitlo lo l)
+ else
+ (* v > hi *)
+ split interval l
+
+ and splitlo lo = function
+ Empty >
+ Empty
+  Node(l, v, d, r, _) >
+ let c = Ord.compare v lo in
+ if c < 0 then
+ (* v < lo *)
+ splitlo lo r
+ else if c = 0 then
+ (* v = lo *)
+ add v d r
+ else
+ (* v > lo *)
+ join (splitlo lo l) v d r
+
+ and splithi hi = function
+ Empty >
+ Empty
+  Node(l, v, d, r, _) >
+ let c = Ord.compare v hi in
+ if c < 0 then
+ (* v < hi *)
+ join l v d (splithi hi r)
+ else if c = 0 then
+ (* v = hi *)
+ add v d l
+ else
+ (* v > hi *)
+ splithi hi l
+
+ (* Splitting. This is the public entry point. *)
+
+ let split interval m =
+ match interval with
+  None, None >
+ m
+  Some lo, None >
+ splitlo lo m
+  None, Some hi >
+ splithi hi m
+  Some lo, Some hi >
+ split (lo, hi) m
+
+ (* Finding the minimum key in a map. *)
+
+ let rec minimum key data m =
+ match m with
+  Empty >
+ (key, data)
+  Node (l, k, d, _, _) >
+ minimum k d l
+
+ let minimum = function
+  Empty >
+ raise Not_found
+  Node (l, k, d, _, _) >
+ minimum k d l
+
+ (* Finding an element and removing it in one single traversal. *)
+
+ let find_remove x m =
+ let data = ref None in
+ let rec remove = function
+  Empty >
+ raise Not_found
+  Node(l, v, d, r, h) >
+ let c = Ord.compare x v in
+ if c = 0 then begin
+ data := Some d;
+ merge l r
+ end
+ else if c < 0 then
+ bal (remove l) v d r
+ else
+ bal l v d (remove r)
+ in
+ let m = remove m in
+ match !data with
+  None >
+ assert false
+  Some d >
+ d, m
+
+ (* Updating the data associated with an element in one single traversal. *)
+
+ exception Unmodified
+
+ let rec update x f m =
+ let rec update = function
+  Empty >
+ assert false
+  Node(l, v, d, r, h) >
+ let c = Ord.compare x v in
+ if c = 0 then
+ let d' = f d in
+ if d == d' then
+ raise Unmodified
+ else
+ Node (l, v, d', r, h)
+ else if c < 0 then
+ Node (update l, v, d, r, h)
+ else
+ Node (l, v, d, update r, h)
+ in
+ try
+ update m
+ with Unmodified >
+ m
+
+ (* Restricting the domain of a map. *)
+
+ let restrict p m =
+ fold (fun x d m >
+ if p x then
+ add x d m
+ else
+ m
+ ) m empty
+
+
+end
Index: /extracted/untrusted/myMap.mli
===================================================================
 /extracted/untrusted/myMap.mli (revision 2738)
+++ /extracted/untrusted/myMap.mli (revision 2738)
@@ 0,0 +1,143 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking described in file ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: myMap.mli,v 1.3 2006/02/17 16:19:52 pottier Exp $ *)
+
+(** Association tables over ordered types.
+
+ This module implements applicative association tables, also known as
+ finite maps or dictionaries, given a total ordering function
+ over the keys.
+ All operations over maps are purely applicative (no sideeffects).
+ The implementation uses balanced binary trees, and therefore searching
+ and insertion take time logarithmic in the size of the map.
+*)
+
+module type OrderedType =
+ sig
+ type t
+ (** The type of the map keys. *)
+ val compare : t > t > int
+ (** A total ordering function over the keys.
+ This is a twoargument function [f] such that
+ [f e1 e2] is zero if the keys [e1] and [e2] are equal,
+ [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+ and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+ Example: a suitable ordering function is the generic structural
+ comparison function {!Pervasives.compare}. *)
+ end
+(** Input signature of the functor {!Map.Make}. *)
+
+module type S =
+ sig
+ type key
+ (** The type of the map keys. *)
+
+ type (+'a) t
+ (** The type of maps from type [key] to type ['a]. *)
+
+ val empty: 'a t
+ (** The empty map. *)
+
+ val is_empty: 'a t > bool
+ (** Test whether a map is empty or not. *)
+
+ val add: key > 'a > 'a t > 'a t
+ (** [add x y m] returns a map containing the same bindings as
+ [m], plus a binding of [x] to [y]. If [x] was already bound
+ in [m], its previous binding disappears. *)
+
+ val find: key > 'a t > 'a
+ (** [find x m] returns the current binding of [x] in [m],
+ or raises [Not_found] if no such binding exists. *)
+
+ val remove: key > 'a t > 'a t
+ (** [remove x m] returns a map containing the same bindings as
+ [m], except for [x] which is unbound in the returned map. *)
+
+ val mem: key > 'a t > bool
+ (** [mem x m] returns [true] if [m] contains a binding for [x],
+ and [false] otherwise. *)
+
+ val iter: (key > 'a > unit) > 'a t > unit
+ (** [iter f m] applies [f] to all bindings in map [m].
+ [f] receives the key as first argument, and the associated value
+ as second argument. The bindings are passed to [f] in increasing
+ order with respect to the ordering over the type of the keys.
+ Only current bindings are presented to [f]:
+ bindings hidden by more recent bindings are not passed to [f]. *)
+
+ val map: ('a > 'b) > 'a t > 'b t
+ (** [map f m] returns a map with same domain as [m], where the
+ associated value [a] of all bindings of [m] has been
+ replaced by the result of the application of [f] to [a].
+ The bindings are passed to [f] in increasing order
+ with respect to the ordering over the type of the keys. *)
+
+ val mapi: (key > 'a > 'b) > 'a t > 'b t
+ (** Same as {!Map.S.map}, but the function receives as arguments both the
+ key and the associated value for each binding of the map. *)
+
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
+ where [k1 ... kN] are the keys of all bindings in [m]
+ (in increasing order), and [d1 ... dN] are the associated data. *)
+
+ val compare: ('a > 'a > int) > 'a t > 'a t > int
+ (** Total ordering between maps. The first argument is a total ordering
+ used to compare data associated with equal keys in the two maps. *)
+
+ val equal: ('a > 'a > bool) > 'a t > 'a t > bool
+ (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
+ equal, that is, contain equal keys and associate them with
+ equal data. [cmp] is the equality predicate used to compare
+ the data associated with the keys. *)
+
+ type interval =
+ key option * key option
+ (** A type of key intervals. An interval consists of a lower bound
+ and an upper bound, each of which can be absent. A key is
+ considered to lie within the interval if it is both greater than
+ (or equal to) the lower bound (if present) and less than (or
+ equal to) the upper bound (if present). *)
+
+ val split: interval > 'a t > 'a t
+ (* [split interval m] is a map that consists of all bindings in [m]
+ whose keys lie within [interval]. *)
+
+ val minimum: 'a t > key * 'a
+ (* [minimum m] returns the binding that corresponds to the minimum
+ (smallest) key within the map [m]. If [m] is empty, [Not_found]
+ is raised. *)
+
+ val find_remove: key > 'a t > 'a * 'a t
+ (** [find_remove x m] returns a pair of the current binding of [x]
+ in [m], and a map containing the same bindings as [m], except
+ for [x] which is unbound in the returned map. [Not_found] is
+ raised if no binding for [x] exists. *)
+
+ val update: key > ('a > 'a) > 'a t > 'a t
+ (** If [m] maps [x] to [d], then [update x f m] maps [x] to [f d]
+ and coincides with [m] elsewhere. A binding for [x] in [m]
+ must exist. *)
+
+ val restrict: (key > bool) > 'a t > 'a t
+ (** [restrict p m] is the restriction of the map [m] to only
+ the keys that satisfy predicate [p]. *)
+
+ end
+(** Output signature of the functor {!Map.Make}. *)
+
+module Make (Ord : OrderedType) : S with type key = Ord.t
+(** Functor building an implementation of the map structure
+ given a totally ordered type. *)
Index: /extracted/untrusted/ocamlList.ml
===================================================================
 /extracted/untrusted/ocamlList.ml (revision 2738)
+++ /extracted/untrusted/ocamlList.ml (revision 2738)
@@ 0,0 +1,27 @@
+let rec rev_append l1 l2 =
+ match l1 with
+ [] > l2
+  a :: l > rev_append l (a :: l2)
+
+let rev l = rev_append l []
+
+let find_all p =
+ let rec find accu = function
+  [] > rev accu
+  x :: l > if p x then find (x :: accu) l else find accu l in
+ find []
+
+let filter = find_all
+
+let rec map f = function
+ [] > []
+  a::l > let r = f a in r :: map f l
+
+let rec iter f = function
+ [] > ()
+  a::l > f a; iter f l
+
+let rec fold_right f l accu =
+ match l with
+ [] > accu
+  a::l > f a (fold_right f l accu)
Index: /extracted/untrusted/ocamlString.ml
===================================================================
 /extracted/untrusted/ocamlString.ml (revision 2738)
+++ /extracted/untrusted/ocamlString.ml (revision 2738)
@@ 0,0 +1,5 @@
+(* To recover OCaml's String *)
+
+external length : string > int = "%string_length"
+external get : string > int > char = "%string_safe_get"
+let compare = Pervasives.compare
Index: /extracted/untrusted/pmap.ml
===================================================================
 /extracted/untrusted/pmap.ml (revision 2738)
+++ /extracted/untrusted/pmap.ml (revision 2738)
@@ 0,0 +1,111 @@
+(* Copied from OCaml's Map to make it polymorphic *)
+
+ type ('k,'a) map =
+ Empty
+  Node of ('k,'a) map * 'k * 'a * ('k,'a) map * int
+
+ let empty = Empty
+
+ let height = function
+ Empty > 0
+  Node(_,_,_,_,h) > h
+
+ let rec find x = function
+ Empty >
+ raise Not_found
+  Node(l, v, d, r, _) >
+ let c = compare x v in
+ if c = 0 then d
+ else find x (if c < 0 then l else r)
+
+ let create l x d r =
+ let hl = height l and hr = height r in
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let bal l x d r =
+ let hl = match l with Empty > 0  Node(_,_,_,_,h) > h in
+ let hr = match r with Empty > 0  Node(_,_,_,_,h) > h in
+ if hl > hr + 2 then begin
+ match l with
+ Empty > invalid_arg "Map.bal"
+  Node(ll, lv, ld, lr, _) >
+ if height ll >= height lr then
+ create ll lv ld (create lr x d r)
+ else begin
+ match lr with
+ Empty > invalid_arg "Map.bal"
+  Node(lrl, lrv, lrd, lrr, _)>
+ create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+ end
+ end else if hr > hl + 2 then begin
+ match r with
+ Empty > invalid_arg "Map.bal"
+  Node(rl, rv, rd, rr, _) >
+ if height rr >= height rl then
+ create (create l x d rl) rv rd rr
+ else begin
+ match rl with
+ Empty > invalid_arg "Map.bal"
+  Node(rll, rlv, rld, rlr, _) >
+ create (create l x d rll) rlv rld (create rlr rv rd rr)
+ end
+ end else
+ Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let rec add x data = function
+ Empty >
+ Node(Empty, x, data, Empty, 1)
+  Node(l, v, d, r, h) >
+ let c = compare x v in
+ if c = 0 then
+ Node(l, x, data, r, h)
+ else if c < 0 then
+ bal (add x data l) v d r
+ else
+ bal l v d (add x data r)
+
+ let rec min_binding = function
+ Empty > raise Not_found
+  Node(Empty, x, d, r, _) > (x, d)
+  Node(l, x, d, r, _) > min_binding l
+
+ let rec remove_min_binding = function
+ Empty > invalid_arg "Map.remove_min_elt"
+  Node(Empty, x, d, r, _) > r
+  Node(l, x, d, r, _) > bal (remove_min_binding l) x d r
+
+ let merge t1 t2 =
+ match (t1, t2) with
+ (Empty, t) > t
+  (t, Empty) > t
+  (_, _) >
+ let (x, d) = min_binding t2 in
+ bal t1 x d (remove_min_binding t2)
+
+ let rec remove x = function
+ Empty >
+ Empty
+  Node(l, v, d, r, h) >
+ let c = compare x v in
+ if c = 0 then
+ merge l r
+ else if c < 0 then
+ bal (remove x l) v d r
+ else
+ bal l v d (remove x r)
+
+ let rec fold f m accu =
+ match m with
+ Empty > accu
+  Node(l, v, d, r, _) >
+ fold f r (f v d (fold f l accu))
+
+(* Copied from atom.ml *)
+
+let restrict p m =
+ fold (fun x d m >
+ if p x then
+ add x d m
+ else
+ m
+ ) m empty
Index: /extracted/untrusted/pmap.mli
===================================================================
 /extracted/untrusted/pmap.mli (revision 2738)
+++ /extracted/untrusted/pmap.mli (revision 2738)
@@ 0,0 +1,13 @@
+type ('k,'a) map
+
+val empty: ('k,'a) map
+
+val find: 'k > ('k,'a) map > 'a
+
+val add: 'k > 'a > ('k,'a) map > ('k,'a) map
+
+val remove: 'k > ('k,'a) map > ('k,'a) map
+
+val restrict: ('k > bool) > ('k,'a) map > ('k,'a) map
+
+val fold: ('k > 'a > 'b > 'b) > ('k,'a) map > 'b > 'b
Index: /extracted/untrusted/prioritySet.ml
===================================================================
 /extracted/untrusted/prioritySet.ml (revision 2738)
+++ /extracted/untrusted/prioritySet.ml (revision 2738)
@@ 0,0 +1,146 @@
+(* Pasted from Pottier's PP compiler *)
+
+(* This module offers sets of elements where each element carries an
+ integer priority. All operations execute in logarithmic time with
+ respect to the number of elements in the set. *)
+
+module Make (X : Set.OrderedType)
+= struct
+
+ (* First, define normal sets and maps. *)
+
+ module Set = Set.Make(X)
+
+ module Map = MyMap.Make(X)
+
+ (* Next, define maps of integers to nonempty sets of elements. *)
+
+ module IntMap = struct
+
+ module M = MyMap.Make (struct
+ type t = int
+ let compare = compare
+ end)
+
+ include M
+
+ module H = SetMap.MakeHetero(Set)(M)
+
+ let update = H.update
+
+ end
+
+ (* Now, define priority sets. *)
+
+ type t = {
+
+ (* A mapping of elements to priorities. *)
+
+ priority: int Map.t;
+
+ (* A mapping of priorities to sets of elements. By convention, a
+ priority has no entry in this table if that entry would be an
+ empty set of elements. This allows finding the
+ lowestpriority element in logarithmic time. *)
+
+ level: Set.t IntMap.t
+
+ }
+
+ (* [empty] is the empty set. *)
+
+ let empty =
+ {
+ priority = Map.empty;
+ level = IntMap.empty
+ }
+
+ (* [priority x s] looks up the priority of element [x]. *)
+
+ let priority x s =
+ try
+ Map.find x s.priority
+ with Not_found >
+ assert false
+
+ (* [add x p s] inserts element [x] with priority [p]. *)
+
+ let add x p s =
+ assert (not (Map.mem x s.priority));
+ {
+ priority = Map.add x p s.priority;
+ level = IntMap.update p (Set.add x) s.level
+ }
+
+ (* [remove x s] removes element [x]. *)
+
+ let remove x s =
+ let p, priority =
+ try
+ Map.find_remove x s.priority
+ with Not_found >
+ assert false
+ in
+ let level =
+ IntMap.update p (function xs >
+ assert (Set.mem x xs);
+ Set.remove x xs
+ ) s.level
+ in
+ {
+ priority = priority;
+ level = level
+ }
+
+ (* [change x p s] changes the priority of element [x] to [p]. *)
+
+ let change x p1 s =
+ let p0 = priority x s in
+ if p0 = p1 then
+ s
+ else
+ {
+ priority = Map.add x p1 s.priority; (* overriding previous entry *)
+ level = IntMap.update p1 (Set.add x) (IntMap.update p0 (Set.remove x) s.level)
+ }
+
+ (* [increment x d s] increases the priority of element [x] by [d]. *)
+
+ let increment x d s =
+ change x (priority x s + d) s
+
+ (* [incrementifx x p s] increases the priority of element [x] by [d]
+ if [x] is a member of the priority set. *)
+
+ let incrementifx x d s =
+ if Map.mem x s.priority then
+ increment x d s
+ else
+ s
+
+ (* [lowest s] returns [Some (x, p)], where element [x] has minimum
+ priority [p] among all elements of [s]. It returns [None] if [s]
+ is empty. *)
+
+ let lowest s =
+ try
+ let p, xs = IntMap.minimum s.level in (* can fail if set is empty *)
+ try
+ Some (Set.choose xs, p) (* cannot fail *)
+ with Not_found >
+ assert false
+ with Not_found >
+ None
+
+ (* [fold f s accu] fold over the set [s]. Elements are presented
+ to [f] in increasing order of priority. *)
+
+ let fold f s accu =
+ IntMap.fold (fun p xs accu >
+ Set.fold (fun x accu >
+ f x p accu
+ ) xs accu
+ ) s.level accu
+
+end
+
Index: /extracted/untrusted/prioritySet.mli
===================================================================
 /extracted/untrusted/prioritySet.mli (revision 2738)
+++ /extracted/untrusted/prioritySet.mli (revision 2738)
@@ 0,0 +1,54 @@
+(* Pasted from Pottier's PP compiler *)
+
+(** This module offers sets of elements where each element carries an
+ integer priority. All operations execute in logarithmic time with
+ respect to the number of elements in the set. *)
+
+module Make (X : Set.OrderedType) : sig
+
+ (* This is the type of priority sets. *)
+
+ type t
+
+ (* [empty] is the empty set. *)
+
+ val empty: t
+
+ (* [add x p s] inserts element [x] with priority [p]. *)
+
+ val add: X.t > int > t > t
+
+ (* [remove x s] removes element [x]. *)
+
+ val remove: X.t > t > t
+
+ (* [change x p s] changes the priority of element [x] to [p]. *)
+
+ val change: X.t > int > t > t
+
+ (* [increment x d s] increases the priority of element [x] by [d]. *)
+
+ val increment: X.t > int > t > t
+
+ (* [incrementifx x p s] increases the priority of element [x] by [d]
+ if [x] is a member of the priority set. *)
+
+ val incrementifx: X.t > int > t > t
+
+ (* [priority x s] looks up the priority of element [x]. *)
+
+ val priority: X.t > t > int
+
+ (* [lowest s] returns [Some (x, p)], where element [x] has minimum
+ priority [p] among all elements of [s]. It returns [None] if [s]
+ is empty. *)
+
+ val lowest: t > (X.t * int) option
+
+ (* [fold f s accu] fold over the set [s]. Elements are presented
+ to [f] in increasing order of priority. *)
+
+ val fold: (X.t > int > 'a > 'a) > t > 'a > 'a
+
+end
+
Index: /extracted/untrusted/pset.ml
===================================================================
 /extracted/untrusted/pset.ml (revision 2738)
+++ /extracted/untrusted/pset.ml (revision 2738)
@@ 0,0 +1,197 @@
+(* Copied from OCaml's set.ml *)
+
+ type 'a set = Empty  Node of 'a set * 'a * 'a set * int
+
+ let empty = Empty
+
+ let is_empty = function Empty > true  Node _ > false
+
+ let height = function
+ Empty > 0
+  Node(_, _, _, h) > h
+
+ let create l v r =
+ let hl = match l with Empty > 0  Node(_,_,_,h) > h in
+ let hr = match r with Empty > 0  Node(_,_,_,h) > h in
+ Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let bal l v r =
+ let hl = match l with Empty > 0  Node(_,_,_,h) > h in
+ let hr = match r with Empty > 0  Node(_,_,_,h) > h in
+ if hl > hr + 2 then begin
+ match l with
+ Empty > invalid_arg "Set.bal"
+  Node(ll, lv, lr, _) >
+ if height ll >= height lr then
+ create ll lv (create lr v r)
+ else begin
+ match lr with
+ Empty > invalid_arg "Set.bal"
+  Node(lrl, lrv, lrr, _)>
+ create (create ll lv lrl) lrv (create lrr v r)
+ end
+ end else if hr > hl + 2 then begin
+ match r with
+ Empty > invalid_arg "Set.bal"
+  Node(rl, rv, rr, _) >
+ if height rr >= height rl then
+ create (create l v rl) rv rr
+ else begin
+ match rl with
+ Empty > invalid_arg "Set.bal"
+  Node(rll, rlv, rlr, _) >
+ create (create l v rll) rlv (create rlr rv rr)
+ end
+ end else
+ Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
+
+ let rec add x = function
+ Empty > Node(Empty, x, Empty, 1)
+  Node(l, v, r, _) as t >
+ let c = compare x v in
+ if c = 0 then t else
+ if c < 0 then bal (add x l) v r else bal l v (add x r)
+
+ let singleton elt = add elt Empty
+
+ let rec min_elt = function
+ Empty > raise Not_found
+  Node(Empty, v, r, _) > v
+  Node(l, v, r, _) > min_elt l
+
+ let rec remove_min_elt = function
+ Empty > invalid_arg "Set.remove_min_elt"
+  Node(Empty, v, r, _) > r
+  Node(l, v, r, _) > bal (remove_min_elt l) v r
+
+ let merge t1 t2 =
+ match (t1, t2) with
+ (Empty, t) > t
+  (t, Empty) > t
+  (_, _) > bal t1 (min_elt t2) (remove_min_elt t2)
+
+ let rec remove x = function
+ Empty > Empty
+  Node(l, v, r, _) >
+ let c = compare x v in
+ if c = 0 then merge l r else
+ if c < 0 then bal (remove x l) v r else bal l v (remove x r)
+
+ let rec fold f s accu =
+ match s with
+ Empty > accu
+  Node(l, v, r, _) > fold f r (f v (fold f l accu))
+
+ let rec iter f = function
+ Empty > ()
+  Node(l, v, r, _) > iter f l; f v; iter f r
+
+ let rec cardinal = function
+ Empty > 0
+  Node(l, v, r, _) > cardinal l + 1 + cardinal r
+
+ let rec join l v r =
+ match (l, r) with
+ (Empty, _) > add v r
+  (_, Empty) > add v l
+  (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) >
+ if lh > rh + 2 then bal ll lv (join lr v r) else
+ if rh > lh + 2 then bal (join l v rl) rv rr else
+ create l v r
+
+ let rec split x = function
+ Empty >
+ (Empty, false, Empty)
+  Node(l, v, r, _) >
+ let c = compare x v in
+ if c = 0 then (l, true, r)
+ else if c < 0 then
+ let (ll, pres, rl) = split x l in (ll, pres, join rl v r)
+ else
+ let (lr, pres, rr) = split x r in (join l v lr, pres, rr)
+
+ let rec union s1 s2 =
+ match (s1, s2) with
+ (Empty, t2) > t2
+  (t1, Empty) > t1
+  (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) >
+ if h1 >= h2 then
+ if h2 = 1 then add v2 s1 else begin
+ let (l2, _, r2) = split v1 s2 in
+ join (union l1 l2) v1 (union r1 r2)
+ end
+ else
+ if h1 = 1 then add v1 s2 else begin
+ let (l1, _, r1) = split v2 s1 in
+ join (union l1 l2) v2 (union r1 r2)
+ end
+
+ let concat t1 t2 =
+ match (t1, t2) with
+ (Empty, t) > t
+  (t, Empty) > t
+  (_, _) > join t1 (min_elt t2) (remove_min_elt t2)
+
+ let rec mem x = function
+ Empty > false
+  Node(l, v, r, _) >
+ let c = compare x v in
+ c = 0  mem x (if c < 0 then l else r)
+
+ let rec for_all p = function
+ Empty > true
+  Node(l, v, r, _) > p v && for_all p l && for_all p r
+
+ let rec exists p = function
+ Empty > false
+  Node(l, v, r, _) > p v  exists p l  exists p r
+
+ let rec subset s1 s2 =
+ match (s1, s2) with
+ Empty, _ >
+ true
+  _, Empty >
+ false
+  Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) >
+ let c = compare v1 v2 in
+ if c = 0 then
+ subset l1 l2 && subset r1 r2
+ else if c < 0 then
+ subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
+ else
+ subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
+
+ let rec diff s1 s2 =
+ match (s1, s2) with
+ (Empty, t2) > Empty
+  (t1, Empty) > t1
+  (Node(l1, v1, r1, _), t2) >
+ match split v1 t2 with
+ (l2, false, r2) >
+ join (diff l1 l2) v1 (diff r1 r2)
+  (l2, true, r2) >
+ concat (diff l1 l2) (diff r1 r2)
+
+ type 'a enumeration = End  More of 'a * 'a set * 'a enumeration
+
+ let rec cons_enum s e =
+ match s with
+ Empty > e
+  Node(l, v, r, _) > cons_enum l (More(v, r, e))
+
+ let rec compare_aux e1 e2 =
+ match (e1, e2) with
+ (End, End) > 0
+  (End, _) > 1
+  (_, End) > 1
+  (More(v1, r1, e1), More(v2, r2, e2)) >
+ let c = compare v1 v2 in
+ if c <> 0
+ then c
+ else compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+
+ let compare s1 s2 =
+ compare_aux (cons_enum s1 End) (cons_enum s2 End)
+
+ let equal s1 s2 =
+ compare s1 s2 = 0
Index: /extracted/untrusted/pset.mli
===================================================================
 /extracted/untrusted/pset.mli (revision 2738)
+++ /extracted/untrusted/pset.mli (revision 2738)
@@ 0,0 +1,27 @@
+type 'x set
+
+val empty : 'a1 set
+
+val is_empty: 'a1 set > bool
+
+val mem : 'a1 > 'a1 set > bool
+
+val add : 'a1 > 'a1 set > 'a1 set
+
+val remove: 'a1 > 'a1 set > 'a1 set
+
+val cardinal: 'a1 set > int
+
+val fold: ('a1 > 'a > 'a) > 'a1 set > 'a > 'a
+
+val iter: ('a1 > unit) > 'a1 set > unit
+
+val equal : 'a1 set > 'a1 set > bool
+
+val diff : 'a1 set > 'a1 set > 'a1 set
+
+val singleton : 'a1 > 'a1 set
+
+val subset : 'a1 set > 'a1 set > bool
+
+val union : 'a1 set > 'a1 set > 'a1 set
Index: /extracted/untrusted/setMap.ml
===================================================================
 /extracted/untrusted/setMap.ml (revision 2738)
+++ /extracted/untrusted/setMap.ml (revision 2738)
@@ 0,0 +1,226 @@
+(* Pasted from Pottier's PP compiler *)
+
+(* This signature defines a few operations over maps of keys to
+ nonempty sets of items. Keys and items can have distinct types,
+ hence the name [Heterogeneous].
+
+ These maps can be used to represent directed bipartite graphs whose
+ source vertices are keys and whose target vertices are items. Each
+ key is mapped to the set of its successors. *)
+
+module type Heterogeneous = sig
+
+ (* These are the types of keys, items, and sets of items. *)
+
+ type key
+ type item
+ type itemset
+
+ (* This is the type of maps of keys to sets of items. *)
+
+ type t
+
+ (* [find x m] is the item set associated with key [x] in map [m], if
+ such an association is defined; it is the empty set otherwise. *)
+
+ val find: key > t > itemset
+
+ (* [add x is m] extends [m] with a binding of [x] to the item set
+ [is], if [is] is nonempty. If [is] is empty, it removes [x] from
+ [m]. *)
+
+ val add: key > itemset > t > t
+
+ (* [update x f m] is [add x (f (find x m)) m]. *)
+
+ val update: key > (itemset > itemset) > t > t
+
+ (* [mkedge x i m] extends [m] with a binding of [x] to the union of
+ the set [m x] and the singleton [i], where [m x] is taken to be
+ empty if undefined. In terms of graphs, [mkedge x i m] extends
+ the graph [m] with an edge of [x] to [i]. *)
+
+ val mkedge: key > item > t > t
+
+ (* [rmedge x i m] extends [m] with a binding of [x] to the
+ difference of the set [m x] and the singleton [i], where the
+ binding is considered undefined if that difference is empty. In
+ terms of graphs, [rmedge x i m] removes an edge of [x] to [i]
+ to the graph [m]. *)
+
+ val rmedge: key > item > t > t
+
+ (* [iter] and [fold] iterate over all edges in the graph. *)
+
+ val iter: (key * item > unit) > t > unit
+ val fold: (key * item > 'a > 'a) > t > 'a > 'a
+
+ (* [pick m p] returns an arbitrary edge that satisfies predicate
+ [p], if the graph contains one. *)
+
+ val pick: t > (key * item > bool) > (key * item) option
+
+end
+
+(* This functor offers an implementation of [Heterogeneous] out of
+ standard implementations of sets and maps. *)
+
+module MakeHetero
+ (Set : sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t > bool
+ val add: elt > t > t
+ val remove: elt > t > t
+ val fold: (elt > 'a > 'a) > t > 'a > 'a
+ end)
+ (Map : sig
+ type key
+ type 'a t
+ val add: key > 'a > 'a t > 'a t
+ val find: key > 'a t > 'a
+ val remove: key > 'a t > 'a t
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ end)
+= struct
+
+ type key = Map.key
+ type item = Set.elt
+ type itemset = Set.t
+ type t = Set.t Map.t
+
+ let find x m =
+ try
+ Map.find x m
+ with Not_found >
+ Set.empty
+
+ let add x is m =
+ if Set.is_empty is then
+ Map.remove x m
+ else
+ Map.add x is m
+
+ let update x f m =
+ add x (f (find x m)) m
+
+ let mkedge x i m =
+ update x (Set.add i) m
+
+ let rmedge x i m =
+ update x (Set.remove i) m
+
+ let fold f m accu =
+ Map.fold (fun source targets accu >
+ Set.fold (fun target accu >
+ f (source, target) accu
+ ) targets accu
+ ) m accu
+
+ let iter f m =
+ fold (fun edge () > f edge) m ()
+
+ exception Picked of (key * item)
+
+ let pick m p =
+ try
+ iter (fun edge >
+ if p edge then
+ raise (Picked edge)
+ ) m;
+ None
+ with Picked edge >
+ Some edge
+
+end
+
+(* This signature defines a few common operations over maps of keys
+ to sets of keys  that is, keys and items have the same type,
+ hence the name [Homogeneous].
+
+ These maps can be used to represent general directed graphs. *)
+
+module type Homogeneous = sig
+
+ include Heterogeneous (* [key] and [item] intended to be equal *)
+
+ (* [mkbiedge x1 x2 m] is [mkedge x1 x2 (mkedge x2 x1 m)]. *)
+
+ val mkbiedge: key > key > t > t
+
+ (* [rmbiedge x1 x2 m] is [rmedge x1 x2 (rmedge x2 x1 m)]. *)
+
+ val rmbiedge: key > key > t > t
+
+ (* [reverse m] is the reverse of graph [m]. *)
+
+ val reverse: t > t
+
+ (* [restrict m] is the graph obtained by keeping only the vertices
+ that satisfy predicate [p]. *)
+
+ val restrict: (key > bool) > t > t
+
+end
+
+module MakeHomo
+ (Set : sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t > bool
+ val add: elt > t > t
+ val remove: elt > t > t
+ val fold: (elt > 'a > 'a) > t > 'a > 'a
+ val filter: (elt > bool) > t > t
+ end)
+ (Map : sig
+ type key = Set.elt
+ type 'a t
+ val empty: 'a t
+ val add: key > 'a > 'a t > 'a t
+ val find: key > 'a t > 'a
+ val remove: key > 'a t > 'a t
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ end)
+= struct
+
+ include MakeHetero(Set)(Map)
+
+ let symmetric transform x1 x2 m =
+ transform x1 x2 (transform x2 x1 m)
+
+ let mkbiedge =
+ symmetric mkedge
+
+ let rmbiedge =
+ symmetric rmedge
+
+ let reverse m =
+ Map.fold (fun source targets predecessors >
+ Set.fold (fun target predecessors >
+
+ (* We have a direct edge from [source] to [target]. Thus, we
+ record the existence of a reverse edge from [target] to
+ [source]. *)
+
+ mkedge target source predecessors
+
+ ) targets predecessors
+ ) m Map.empty
+
+ let restrict p m =
+ Map.fold (fun source targets m >
+ if p source then
+ let targets = Set.filter p targets in
+ if Set.is_empty targets then
+ m
+ else
+ Map.add source targets m
+ else
+ m
+ ) m Map.empty
+
+end
+
Index: /extracted/untrusted/setMap.mli
===================================================================
 /extracted/untrusted/setMap.mli (revision 2738)
+++ /extracted/untrusted/setMap.mli (revision 2738)
@@ 0,0 +1,144 @@
+(* Pasted from Pottier's PP compiler *)
+
+(** This signature defines a few operations over maps of keys to
+ nonempty sets of items. Keys and items can have distinct types,
+ hence the name [Heterogeneous].
+
+ These maps can be used to represent directed bipartite graphs whose
+ source vertices are keys and whose target vertices are items. Each
+ key is mapped to the set of its successors. *)
+
+module type Heterogeneous = sig
+
+ (* These are the types of keys, items, and sets of items. *)
+
+ type key
+ type item
+ type itemset
+
+ (* This is the type of maps of keys to sets of items. *)
+
+ type t
+
+ (* [find x m] is the item set associated with key [x] in map [m], if
+ such an association is defined; it is the empty set otherwise. *)
+
+ val find: key > t > itemset
+
+ (* [add x is m] extends [m] with a binding of [x] to the item set
+ [is], if [is] is nonempty. If [is] is empty, it removes [x] from
+ [m]. *)
+
+ val add: key > itemset > t > t
+
+ (* [update x f m] is [add x (f (find x m)) m]. *)
+
+ val update: key > (itemset > itemset) > t > t
+
+ (* [mkedge x i m] extends [m] with a binding of [x] to the union of
+ the set [m x] and the singleton [i], where [m x] is taken to be
+ empty if undefined. In terms of graphs, [mkedge x i m] extends
+ the graph [m] with an edge of [x] to [i]. *)
+
+ val mkedge: key > item > t > t
+
+ (* [rmedge x i m] extends [m] with a binding of [x] to the
+ difference of the set [m x] and the singleton [i], where the
+ binding is considered undefined if that difference is empty. In
+ terms of graphs, [rmedge x i m] removes an edge of [x] to [i]
+ to the graph [m]. *)
+
+ val rmedge: key > item > t > t
+
+ (* [iter] and [fold] iterate over all edges in the graph. *)
+
+ val iter: (key * item > unit) > t > unit
+ val fold: (key * item > 'a > 'a) > t > 'a > 'a
+
+ (* [pick m p] returns an arbitrary edge that satisfies predicate
+ [p], if the graph contains one. *)
+
+ val pick: t > (key * item > bool) > (key * item) option
+
+end
+
+(* This functor offers an implementation of [Heterogeneous] out of
+ standard implementations of sets and maps. *)
+
+module MakeHetero
+ (Set : sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t > bool
+ val add: elt > t > t
+ val remove: elt > t > t
+ val fold: (elt > 'a > 'a) > t > 'a > 'a
+ end)
+ (Map : sig
+ type key
+ type 'a t
+ val add: key > 'a > 'a t > 'a t
+ val find: key > 'a t > 'a
+ val remove: key > 'a t > 'a t
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ end)
+ : Heterogeneous with type key = Map.key
+ and type item = Set.elt
+ and type itemset = Set.t
+ and type t = Set.t Map.t
+
+(* This signature defines a few common operations over maps of keys
+ to sets of keys  that is, keys and items have the same type,
+ hence the name [Homogeneous].
+
+ These maps can be used to represent general directed graphs. *)
+
+module type Homogeneous = sig
+
+ include Heterogeneous (* [key] and [item] intended to be equal *)
+
+ (* [mkbiedge x1 x2 m] is [mkedge x1 x2 (mkedge x2 x1 m)]. *)
+
+ val mkbiedge: key > key > t > t
+
+ (* [rmbiedge x1 x2 m] is [rmedge x1 x2 (rmedge x2 x1 m)]. *)
+
+ val rmbiedge: key > key > t > t
+
+ (* [reverse m] is the reverse of graph [m]. *)
+
+ val reverse: t > t
+
+ (* [restrict m] is the graph obtained by keeping only the vertices
+ that satisfy predicate [p]. *)
+
+ val restrict: (key > bool) > t > t
+
+end
+
+module MakeHomo
+ (Set : sig
+ type elt
+ type t
+ val empty: t
+ val is_empty: t > bool
+ val add: elt > t > t
+ val remove: elt > t > t
+ val fold: (elt > 'a > 'a) > t > 'a > 'a
+ val filter: (elt > bool) > t > t
+ end)
+ (Map : sig
+ type key = Set.elt
+ type 'a t
+ val empty: 'a t
+ val add: key > 'a > 'a t > 'a t
+ val find: key > 'a t > 'a
+ val remove: key > 'a t > 'a t
+ val fold: (key > 'a > 'b > 'b) > 'a t > 'b > 'b
+ end)
+ : Homogeneous with type key = Set.elt
+ and type item = Set.elt
+ and type itemset = Set.t
+ and type t = Set.t Map.t
+
Index: /extracted/untrusted/set_adt.ml
===================================================================
 /extracted/untrusted/set_adt.ml (revision 2738)
+++ /extracted/untrusted/set_adt.ml (revision 2738)
@@ 0,0 +1,31 @@
+type 'x set = 'x Pset.set
+
+let matitabool_of_bool b = if b then Bool.True else Bool.False
+
+(** val set_empty : 'a1 set0 **)
+let set_empty = Pset.empty
+
+(** val set_member :
+ ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set0 > Bool.bool **)
+let set_member _ x s = matitabool_of_bool (Pset.mem x s)
+
+(** val set_equal :
+ ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **)
+let set_equal _ s1 s2 = matitabool_of_bool (Pset.equal s1 s2)
+
+(** val set_diff : 'a1 set0 > 'a1 set0 > 'a1 set0 **)
+let set_diff = Pset.diff
+
+(** val set_singleton : 'a1 > 'a1 set0 **)
+let set_singleton = Pset.singleton
+
+(** val set_from_list : 'a1 List.list > 'a1 set0 **)
+let set_from_list the_list =
+ List.foldr Pset.add set_empty the_list
+
+(** val set_subset :
+ ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **)
+let set_subset _ s1 s2 = matitabool_of_bool (Pset.subset s1 s2)
+
+(** val set_union : 'a1 set0 > 'a1 set0 > 'a1 set0 **)
+let set_union = Pset.union
Index: /extracted/untrusted/set_adt.mli
===================================================================
 /extracted/untrusted/set_adt.mli (revision 2738)
+++ /extracted/untrusted/set_adt.mli (revision 2738)
@@ 0,0 +1,19 @@
+type 'x set
+
+val set_empty : 'a1 set
+
+val set_member : ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set > Bool.bool
+
+val set_equal :
+ ('a1 > 'a1 > Bool.bool) > 'a1 set > 'a1 set > Bool.bool
+
+val set_diff : 'a1 set > 'a1 set > 'a1 set
+
+val set_singleton : 'a1 > 'a1 set
+
+val set_from_list : 'a1 List.list > 'a1 set
+
+val set_subset :
+ ('a1 > 'a1 > Bool.bool) > 'a1 set > 'a1 set > Bool.bool
+
+val set_union : 'a1 set > 'a1 set > 'a1 set
Index: /extracted/untrusted/spill.ml
===================================================================
 /extracted/untrusted/spill.ml (revision 2738)
+++ /extracted/untrusted/spill.ml (revision 2738)
@@ 0,0 +1,159 @@
+(* Pasted from Pottier's PP compiler *)
+
+open Untrusted_interference
+(* open Integer *)
+open Printf
+
+(*  *)
+(* Colorings. *)
+
+(* This module performs graph coloring with an unlimited number of
+ colors and aggressive coalescing. It is used for assigning stack
+ slots to the pseudoregisters that have been spilled by register
+ allocation. *)
+
+(* A coloring is a partial function of graph vertices to stack
+ slots. Vertices that are not in the domain of the coloring are
+ waiting for a decision to be made. *)
+
+type decision =
+ int
+
+type coloring =
+ decision Vertex.Map.t
+
+(*  *)
+(* Here is the coloring algorithm. *)
+
+module Color (G : sig
+
+ val graph: graph
+ val verbose: bool
+
+end) = struct
+
+ module SlotSet =
+ Set.Make(struct type t = int let compare = Pervasives.compare end)
+
+ (* [forbidden_slots graph coloring v] is the set of stack slots that
+ cannot be assigned to [v] considering the (partial) coloring
+ [coloring]. This takes into account [v]'s possible interferences
+ with other spilled vertices. *)
+
+ let add_slot coloring r slots =
+ SlotSet.add (Vertex.Map.find r coloring) slots
+
+ let forbidden_slots graph coloring v =
+ Vertex.Set.fold (add_slot coloring) (ipp graph v) SlotSet.empty
+
+ (* [allocate_slot forbidden] returns a stack slot that is not a
+ member of the set [forbidden]. Unlike hardware registers, stack
+ slots are infinitely many, so it is always possible to allocate a
+ new one. The reference [locals] holds the space that must be
+ reserved on the stack for locals. *)
+
+ let locals =
+ ref 0
+
+ let allocate_slot forbidden =
+ let rec loop slot =
+ if SlotSet.mem slot forbidden then
+ loop (slot + Glue.int_of_bitvector I8051.int_size)
+ else
+ slot
+ in
+ let slot = loop 0 in
+ locals := max (slot + Glue.int_of_bitvector I8051.int_size) !locals;
+ slot
+
+ (* Allocation is in two phases, implemented by [coalescing] and
+ [simplification]. Each of these functions produces a coloring of its
+ graph argument. *)
+
+ (* [simplification] expects a graph that does not contain any preference
+ edges. It picks a vertex [v], removes it, colors the remaining graph,
+ then colors [v] using a color that is still available. Such a color must
+ exist, since there is an unlimited number of colors. *)
+
+ (* Following Appel, [v] is chosen with lowest degree: this will make this
+ vertex easier to color and might (?) help use fewer colors. *)
+
+ let rec simplification graph : coloring =
+
+ match lowest graph with
+  Some (v, _) >
+
+(*
+ if G.verbose then
+ printf "SPILL: Picking vertex: %s.\n" (print_vertex graph v);
+*)
+
+ (* Remove [v] from the graph and color what remains. *)
+
+ let coloring = simplification (Untrusted_interference.remove graph v) in
+
+ (* Choose a color for [v]. *)
+
+ let decision =
+ allocate_slot (forbidden_slots graph coloring v)
+ in
+
+(*
+ if G.verbose then
+ printf "SPILL: Decision concerning %s: offset %d.\n" (print_vertex graph v) decision;
+*)
+
+ (* Record our decision and return. *)
+
+ Vertex.Map.add v decision coloring
+
+  None >
+
+ (* The graph is empty. Return an empty coloring. *)
+
+ Vertex.Map.empty
+
+ (* [coalescing] looks for a preference edge, that is, for two vertices
+ [x] and [y] such that [x] and [y] are moverelated. In that case,
+ [x] and [y] cannot interfere, because the [Interference] module
+ does not allow two vertices to be related by both an interference
+ edge and a preference edge. If [coalescing] finds such an edge, it
+ coalesces [x] and [y] and continues coalescing. Otherwise, it
+ invokes the next phase, [simplification].
+
+ This is aggressive coalescing: we coalesce all preference edges,
+ without fear of creating highdegree nodes. This is good because
+ a move between two pseudoregisters that have been spilled in
+ distinct stack slots is very expensive: one load followed by one
+ store. *)
+
+ let rec coalescing graph : coloring =
+
+ match pppick graph (fun _ > true) with
+  Some (x, y) >
+
+(*
+ if G.verbose then
+ printf "SPILL: Coalescing %s and %s.\n" (print_vertex graph x) (print_vertex graph y);
+*)
+
+ let graph = Untrusted_interference.coalesce graph x y in
+ let coloring = coalescing graph in
+ Vertex.Map.add x (Vertex.Map.find y coloring) coloring
+
+  None >
+
+ simplification graph
+
+ (* Run the algorithm. [coalescing] runs first and calls [simplification]
+ when it is done. *)
+
+ let coloring =
+ coalescing G.graph
+
+ (* Report how much stack space was used. *)
+
+ let locals =
+ !locals
+
+end
Index: /extracted/untrusted/spill.mli
===================================================================
 /extracted/untrusted/spill.mli (revision 2738)
+++ /extracted/untrusted/spill.mli (revision 2738)
@@ 0,0 +1,36 @@
+(* Pasted from Pottier's PP compiler *)
+
+(** This module performs graph coloring with an unlimited number of
+ colors and aggressive coalescing. It is used for assigning stack
+ slots to the pseudoregisters that have been spilled by register
+ allocation. *)
+
+(* A coloring is a partial function of graph vertices to stack
+ slots. Vertices that are not in the domain of the coloring are
+ waiting for a decision to be made. *)
+
+type decision =
+ int
+
+type coloring =
+ decision Untrusted_interference.Vertex.Map.t
+
+(* Here is the coloring algorithm. Out of an interference graph, it
+ produces a coloring and reports how many colors (stack slots) were
+ required. The graph is expected to contain interference and
+ preferences edges between vertices only  no hardware registers
+ are involved. If the [verbose] flag is set, the algorithm prints
+ information messages to the standard output channel. *)
+
+module Color (G : sig
+
+ val graph: Untrusted_interference.graph
+ val verbose: bool
+
+end) : sig
+
+ val coloring: coloring
+ val locals: int
+
+end
+
Index: /extracted/untrusted/untrusted_interference.ml
===================================================================
 /extracted/untrusted/untrusted_interference.ml (revision 2738)
+++ /extracted/untrusted/untrusted_interference.ml (revision 2738)
@@ 0,0 +1,868 @@
+type pseudoregister = Registers.register
+type hwregister = I8051.register
+module HwOrdReg = struct type t = hwregister let compare = compare end
+module HwRegisterSet = Set.Make (HwOrdReg)
+
+(* Pasted from Pottier's PP compiler *)
+
+(* This module implements a data structure for interference graphs.
+ It provides functions that help construct, transform and inspect
+ interference graphs. *)
+
+(*  *)
+
+(* Vertices are represented as integers. We need sets of vertices, maps over
+ vertices, maps of vertices to nonempty sets of vertices, maps of vertices
+ to nonempty sets of hardware registers, and priority sets over vertices. *)
+
+module Vertex = struct
+
+ module V = struct
+ type t = Positive.pos
+ let compare = compare
+ end
+
+ include V
+
+ module Set = Set.Make(V)
+
+ module Map = MyMap.Make(V)
+
+end
+
+module VertexSetMap =
+ SetMap.MakeHomo(Vertex.Set)(Vertex.Map)
+
+module I8051RegisterSetMap =
+ SetMap.MakeHetero(HwRegisterSet)(Vertex.Map)
+
+module PrioritySet =
+ PrioritySet.Make(Vertex)
+
+(*  *)
+
+(* Each vertex maps to a set of pseudoregisters, which initially is a
+ singleton set, but can grow due to coalescing. Conversely, each
+ pseudoregister maps to a single vertex. *)
+
+module RegMap : sig
+
+ type t
+
+ (* [empty] is the empty map. *)
+
+ val empty: t
+
+ (* [forward] maps a vertex to a set of pseudoregisters. *)
+
+ val forward: Vertex.t > t > pseudoregister Pset.set
+
+ (* [backward] maps a pseudoregister to a vertex. *)
+
+ val backward: pseudoregister > t > Vertex.t
+
+ (* [add r v m] adds a relation between pseudoregister [r] and
+ vertex [v], both of which are assumed fresh. *)
+
+ val add: pseudoregister > Vertex.t > t > t
+
+ (* [fold f m accu] folds over all vertices. *)
+
+ val fold: (Vertex.t > pseudoregister Pset.set > 'a > 'a) > t > 'a > 'a
+
+ (* [coalesce x y m] coalesces vertices [x] and [y]. Vertex [x] is
+ removed and the pseudoregisters associated with it become
+ associated with [y] instead. *)
+
+ val coalesce: Vertex.t > Vertex.t > t > t
+
+ (* [remove x m] removes vertex [x]. The pseudoregisters associated
+ with [x] disappear. *)
+
+ val remove: Vertex.t > t > t
+
+ (* [restrict] keeps only those vertices that satisfy predicate [p]. *)
+
+ val restrict: (Vertex.t > bool) > t > t
+
+end = struct
+
+ type t = {
+ forward: pseudoregister Pset.set Vertex.Map.t;
+ backward: (pseudoregister,Vertex.t) Pmap.map
+ }
+
+ let empty = {
+ forward = Vertex.Map.empty;
+ backward = Pmap.empty
+ }
+
+ let forward v m =
+ Vertex.Map.find v m.forward
+
+ let backward r m =
+ try
+ Pmap.find r m.backward
+ with Not_found >
+ assert false (* bad pseudoregister *)
+
+ let add r v m = {
+ forward = Vertex.Map.add v (Pset.singleton r) m.forward;
+ backward = Pmap.add r v m.backward
+ }
+
+ let fold f m accu =
+ Vertex.Map.fold f m.forward accu
+
+ let coalesce x y m =
+ let rx, forward = Vertex.Map.find_remove x m.forward in
+ let forward = Vertex.Map.update y (Pset.union rx) forward in
+ let backward =
+ Pset.fold (fun r backward >
+ Pmap.add r y backward
+ ) rx m.backward
+ in
+ {
+ forward = forward;
+ backward = backward
+ }
+
+ let remove x m =
+ let rx, forward = Vertex.Map.find_remove x m.forward in
+ let backward = Pset.fold Pmap.remove rx m.backward in
+ {
+ forward = forward;
+ backward = backward
+ }
+
+ let restrict p m = {
+ forward = Vertex.Map.restrict p m.forward;
+ backward = Pmap.restrict (fun r > p (backward r m)) m.backward
+ }
+
+end
+
+(*  *)
+
+(* Graphs. *)
+
+type graph = {
+
+ (* A twoway correspondence between vertices and pseudoregisters.
+ This data structure is also used to keep a record of the set of
+ all vertices. *)
+
+ regmap: RegMap.t;
+
+ (* Interference edges between two vertices: ``these two vertices
+ cannot receive the same color''. *)
+
+ ivv: VertexSetMap.t;
+
+ (* Interference edges between a vertex and a hardware register:
+ ``this vertex cannot receive this color''. *)
+
+ ivh: I8051RegisterSetMap.t;
+
+ (* Preference edges between two vertices: ``these two vertices
+ should preferably receive the same color''. *)
+
+ pvv: VertexSetMap.t;
+
+ (* Preference edges between a vertex and a hardware register:
+ ``this vertex should preferably receive this color''. *)
+
+ pvh: I8051RegisterSetMap.t;
+
+ (* The degree of each vertex [v], that is, the number of vertices
+ and hardware registers that [v] interferes with, is recorded at
+ all times. We use a ``priority set'' so as to be able to
+ efficiently find a vertex of minimum degree. *)
+
+ degree: PrioritySet.t;
+
+ (* The degree of each *nonmoverelated* vertex [v]. This
+ information is partially redundant with the [degree] field
+ above. It is nevertheless required in order to be able to
+ efficiently find a *nonmoverelated* vertex of minimum
+ degree. *)
+
+ nmr: PrioritySet.t;
+
+ }
+
+(*  *)
+
+(* Our graphs are made up of two subgraphs: the subgraph formed by the
+ interference edges alone and the one formed by the preference edges
+ alone.
+
+ In order to allow more code sharing, we define functions that allow
+ dealing with a single subgraph at a time. They provide operations
+ such as inspecting the neighbors of a vertex, adding edges,
+ removing edges, coalescing two vertices, removing a vertex, etc.
+
+ We first define functions that deal with a ``generic'' subgraph,
+ then (via inheritance) specialize them to deal with the
+ interference subgraph and the preference subgraph with their
+ specific features. *)
+
+class virtual subgraph = object (self)
+
+ (* These methods provide access to the fields of the [graph] data
+ structure that define the subgraph of interest. All data is
+ stored in the [graph] data structure. The object [self] has no
+ state and holds no data. *)
+
+ method virtual getvv: graph > VertexSetMap.t
+ method virtual setvv: graph > VertexSetMap.t > graph
+ method virtual getvh: graph > I8051RegisterSetMap.t
+ method virtual setvh: graph > I8051RegisterSetMap.t > graph
+
+ (* Accessing the neighbors of a vertex and testing whether edges
+ exist. *)
+
+ method neighborsv graph v =
+ VertexSetMap.find v (self#getvv graph)
+
+ method existsvv graph v1 v2 =
+ Vertex.Set.mem v1 (self#neighborsv graph v2)
+
+ method neighborsh graph v =
+ I8051RegisterSetMap.find v (self#getvh graph)
+
+ method existsvh graph v h =
+ HwRegisterSet.mem h (self#neighborsh graph v)
+
+ (* [degree graph v] is the degree of vertex [v] with respect to the
+ subgraph. *)
+
+ method degree graph v =
+ Vertex.Set.cardinal (self#neighborsv graph v) + HwRegisterSet.cardinal (self#neighborsh graph v)
+
+ (* [hwregs graph] is the set of all hardware registers mentioned in
+ the subgraph. *)
+
+ method hwregs graph =
+ let union _ = HwRegisterSet.union in
+ Vertex.Map.fold union (self#getvh graph) HwRegisterSet.empty
+
+ (* [iter graph fvv fvh] iterates over all edges in the subgraph.
+ Vertextovertex edges are presented only once. *)
+
+ method iter graph fvv fvh =
+ Vertex.Map.iter (fun vertex neighbors >
+ Vertex.Set.iter (fun neighbor >
+ if vertex < neighbor then
+ fvv vertex neighbor
+ ) neighbors
+ ) (self#getvv graph);
+ Vertex.Map.iter (fun vertex neighbors >
+ HwRegisterSet.iter (fun neighbor >
+ fvh vertex neighbor
+ ) neighbors
+ ) (self#getvh graph)
+
+ (* [mkvv graph v1 v2] adds an edge between vertices [v1] and [v2]. *)
+
+ method mkvv graph v1 v2 =
+ if v1 = v2 then
+ graph (* avoid creating selfedge *)
+ else if self#existsvv graph v1 v2 then
+ graph (* avoid readding an existing edge *)
+ else
+ self#mkvvi graph v1 v2
+
+ method mkvvi graph v1 v2 =
+ self#setvv graph (VertexSetMap.mkbiedge v1 v2 (self#getvv graph))
+
+ (* [rmvv graph v1 v2] removes an edge between vertices [v1] and [v2].
+ [rmvvifx] removes an edge if it exists. *)
+
+ method rmvv graph v1 v2 =
+ assert (self#existsvv graph v1 v2);
+ self#setvv graph (VertexSetMap.rmbiedge v1 v2 (self#getvv graph))
+
+ method rmvvifx graph v1 v2 =
+ if self#existsvv graph v1 v2 then
+ self#rmvv graph v1 v2
+ else
+ graph
+
+ (* [mkvh graph v h] adds an edge between vertex [v] and hardware
+ register [h]. *)
+
+ method mkvh graph v h =
+ if self#existsvh graph v h then
+ graph (* avoid readding an existing edge *)
+ else
+ self#mkvhi graph v h
+
+ method mkvhi graph v h =
+ self#setvh graph (I8051RegisterSetMap.update v (HwRegisterSet.add h) (self#getvh graph))
+
+ (* [rmvh v h] removes an edge between vertex [v] and hardware
+ register [h]. [rmvhifx] removes an edge if it exists. *)
+
+ method rmvh graph v h =
+ assert (self#existsvh graph v h);
+ self#setvh graph (I8051RegisterSetMap.update v (HwRegisterSet.remove h) (self#getvh graph))
+
+ method rmvhifx graph v h =
+ if self#existsvh graph v h then
+ self#rmvh graph v h
+ else
+ graph
+
+ (* [coalesce graph x y] turns every neighbor [w] or [h] of [x] into
+ a neighbor of [y] instead. [w] ranges over both vertices and
+ hardware registers. *)
+
+ method coalesce graph x y =
+ let graph =
+ Vertex.Set.fold (fun w graph >
+ self#mkvv (self#rmvv graph x w) y w
+ ) (self#neighborsv graph x) graph
+ in
+ let graph =
+ HwRegisterSet.fold (fun h graph >
+ self#mkvh (self#rmvh graph x h) y h
+ ) (self#neighborsh graph x) graph
+ in
+ graph
+
+ (* [coalesceh graph x h] turns every neighbor [w] of [x] into a
+ neighbor of [h] instead. [w] ranges over both vertices and
+ hardware registers. Edges between two hardware registers are not
+ recorded. *)
+
+ method coalesceh graph x h =
+ let graph =
+ Vertex.Set.fold (fun w graph >
+ self#mkvh (self#rmvv graph x w) w h
+ ) (self#neighborsv graph x) graph
+ in
+ let graph =
+ HwRegisterSet.fold (fun k graph >
+ self#rmvh graph x k
+ ) (self#neighborsh graph x) graph
+ in
+ graph
+
+ (* [remove graph x] removes all edges carried by vertex [x]. *)
+
+ method remove graph x =
+ let graph =
+ Vertex.Set.fold (fun w graph >
+ self#rmvv graph x w
+ ) (self#neighborsv graph x) graph
+ in
+ let graph =
+ HwRegisterSet.fold (fun h graph >
+ self#rmvh graph x h
+ ) (self#neighborsh graph x) graph
+ in
+ graph
+
+end
+
+(*  *)
+
+(* The interference subgraph.
+
+ This is a subgraph with the following specific features: (1) the
+ degree of every vertex is recorded in the [degree] field of the
+ [graph] data structure; (2) the degree of every nonmoverelated
+ vertex is recorded in the [nmr] field of the [graph] data
+ structure; (3) creating an edge in the interference subgraph
+ automatically destroys a corresponding edge in the preference
+ subgraph. *)
+
+class interference (preference : preference Lazy.t) = object (self)
+
+ inherit subgraph as super
+
+ method getvv graph = graph.ivv
+ method setvv graph m = { graph with ivv = m }
+ method getvh graph = graph.ivh
+ method setvh graph m = { graph with ivh = m }
+
+ (* Override the edge creation and destruction methods. *)
+
+ method mkvvi graph v1 v2 =
+ let graph = super#mkvvi graph v1 v2 in
+ let graph = (Lazy.force preference)#rmvvifx graph v1 v2 in (* do not constrain an existing preference edge *)
+ { graph with
+ degree = PrioritySet.increment v1 1 (PrioritySet.increment v2 1 graph.degree);
+ nmr = PrioritySet.incrementifx v1 1 (PrioritySet.incrementifx v2 1 graph.nmr);
+ }
+
+ method rmvv graph v1 v2 =
+ let graph = super#rmvv graph v1 v2 in
+ { graph with
+ degree = PrioritySet.increment v1 (1) (PrioritySet.increment v2 (1) graph.degree);
+ nmr = PrioritySet.incrementifx v1 (1) (PrioritySet.incrementifx v2 (1) graph.nmr);
+ }
+
+ method mkvhi graph v h =
+ let graph = super#mkvhi graph v h in
+ let graph = (Lazy.force preference)#rmvhifx graph v h in (* do not constrain an existing preference edge *)
+ { graph with
+ degree = PrioritySet.increment v 1 graph.degree;
+ nmr = PrioritySet.incrementifx v 1 graph.nmr;
+ }
+
+ method rmvh graph v h =
+ let graph = super#rmvh graph v h in
+ { graph with
+ degree = PrioritySet.increment v (1) graph.degree;
+ nmr = PrioritySet.incrementifx v (1) graph.nmr;
+ }
+
+end
+
+(*  *)
+
+(* The preference subgraph.
+
+ This is a subgraph with the following specific features: (1) an
+ edge in the preference subgraph cannot be created if a
+ corresponding edge exists in the interference subgraph; (2) adding
+ an edge can make a vertex moverelated, which requires taking that
+ vertex out of the [nmr] set; conversely, removing an edge can make
+ a vertex nonmoverelated, which requires adding that vertex to the
+ [nmr] set. *)
+
+and preference (interference : interference Lazy.t) = object (self)
+
+ inherit subgraph as super
+
+ method getvv graph = graph.pvv
+ method setvv graph m = { graph with pvv = m }
+ method getvh graph = graph.pvh
+ method setvh graph m = { graph with pvh = m }
+
+ (* [nmr graph v] tells whether vertex [v] is nonmoverelated. *)
+
+ method nmr graph v =
+ Vertex.Set.is_empty (self#neighborsv graph v) &&
+ HwRegisterSet.is_empty (self#neighborsh graph v)
+
+ (* [mkcheck graph v] moves [v] out of the [nmr] set if [v] is
+ nonmoverelated. *)
+
+ method mkcheck graph v =
+ if self#nmr graph v then
+ { graph with
+ nmr = PrioritySet.remove v graph.nmr }
+ else
+ graph
+
+ (* Override the edge creation methods. *)
+
+ method mkvvi graph v1 v2 =
+ if (Lazy.force interference)#existsvv graph v1 v2 then
+ graph (* avoid creating constrained preference edge *)
+ else
+ let graph = self#mkcheck graph v1 in
+ let graph = self#mkcheck graph v2 in
+ super#mkvvi graph v1 v2
+
+ method mkvhi graph v h =
+ if (Lazy.force interference)#existsvh graph v h then
+ graph (* avoid creating constrained preference edge *)
+ else
+ let graph = self#mkcheck graph v in
+ super#mkvhi graph v h
+
+ (* [rmcheck graph v] moves [v] into the [nmr] set if [v] is
+ nonmoverelated. *)
+
+ method rmcheck graph v =
+ if self#nmr graph v then
+ { graph with
+ nmr = PrioritySet.add v (PrioritySet.priority v graph.degree) graph.nmr
+ }
+ else
+ graph
+
+ (* Override the edge destruction methods. *)
+
+ method rmvv graph v1 v2 =
+ let graph = super#rmvv graph v1 v2 in
+ let graph = self#rmcheck graph v1 in
+ let graph = self#rmcheck graph v2 in
+ graph
+
+ method rmvh graph v h =
+ let graph = super#rmvh graph v h in
+ let graph = self#rmcheck graph v in
+ graph
+
+end
+
+(*  *)
+
+(* Because the interference and preference subgraphs are mutually
+ referential, a recursive definition is required. It is made
+ somewhat inelegant by Objective Caml's insistence on using the
+ [Lazy] mechanism. *)
+
+let rec interference = lazy (new interference preference)
+ and preference = lazy (new preference interference)
+let interference = Lazy.force interference
+let preference = Lazy.force preference
+
+(*  *)
+
+(* Inspecting interference graphs. *)
+
+(* [ipp graph v] is the set of vertices that the vertex [v] interferes
+ with. *)
+
+let ipp graph v =
+ interference#neighborsv graph v
+
+(* [iph graph v] is the set of hardware registers that the vertex [v]
+ interferes with. *)
+
+let iph graph v =
+ interference#neighborsh graph v
+
+(* [ppp graph v] is the set of vertices that should preferably be
+ assigned the same color as the vertex [v]. *)
+
+let ppp graph v =
+ preference#neighborsv graph v
+
+(* [pph graph v] is the set of hardware registers that [v] should
+ preferably be assigned. *)
+
+let pph graph v =
+ preference#neighborsh graph v
+
+(* [degree graph v] is the degree of the vertex [v], that is, the number
+ of vertices and hardware registers that [v] interferes with. *)
+
+let degree graph v =
+ PrioritySet.priority v graph.degree
+
+(* [lowest graph] returns [Some (v, d)], where the vertex [v] has
+ minimum degree [d], or returns [None] if the graph is empty. *)
+
+let lowest graph =
+ PrioritySet.lowest graph.degree
+
+(* [lowest_non_move_related graph] returns [Some (v, d)], where the
+ vertex [v] has minimum degree [d] among the vertices that are not
+ moverelated, or returns [None] if all vertices are moverelated. A
+ vertex is moverelated if it carries a preference edge. *)
+
+let lowest_non_move_related graph =
+ PrioritySet.lowest graph.nmr
+
+(* [fold f graph accu] folds over all vertices. *)
+
+let fold f graph accu =
+ RegMap.fold (fun v _ accu > f v accu) graph.regmap accu
+
+(* [minimum f graph] returns a vertex [v] such that the value of [f x]
+ is minimal. The values returned by [f] are compared using Objective
+ Caml's generic comparison operator [<]. If the graph is empty,
+ [None] is returned. *)
+
+let minimum f graph =
+ match
+ fold (fun w accu >
+ let dw = f w in
+ match accu with
+  None >
+ Some (dw, w)
+  Some (dv, v) >
+ if dw < dv then
+ Some (dw, w)
+ else
+ accu
+ ) graph None
+ with
+  None >
+ None
+  Some (_, v) >
+ Some v
+
+(* [pppick graph p] returns an arbitrary preference edge that
+ satisfies the predicate [p], if the graph contains one. *)
+
+type ppedge =
+ Vertex.t * Vertex.t
+
+let pppick graph p =
+ VertexSetMap.pick graph.pvv p
+
+(* [phpick graph p] returns an arbitrary preference edge that
+ satisfies the predicate [p], if the graph contains one. *)
+
+type phedge =
+ Vertex.t * I8051.register
+
+let phpick graph p =
+ I8051RegisterSetMap.pick graph.pvh p
+
+(*  *)
+
+(* Constructing interference graphs. *)
+
+(* [create regs] creates an interference graph whose vertices are
+ the pseudoregisters [regs] and that does not have any edges. *)
+
+let create regs =
+ let _, regmap, degree =
+ Pset.fold (fun r (v, regmap, degree) >
+ Positive.succ v,
+ RegMap.add r v regmap,
+ PrioritySet.add v 0 degree
+ ) regs (Positive.One, RegMap.empty, PrioritySet.empty)
+ in
+ {
+ regmap = regmap;
+ ivv = Vertex.Map.empty;
+ ivh = Vertex.Map.empty;
+ pvv = Vertex.Map.empty;
+ pvh = Vertex.Map.empty;
+ degree = degree;
+ nmr = degree
+ }
+
+(* [lookup graph r] returns the graph vertex associated with
+ pseudoregister [r]. *)
+
+let lookup graph r =
+ RegMap.backward r graph.regmap
+
+(* Conversely, [registers graph v] returns the set of pseudoregisters
+ associated with vertex [v]. *)
+
+let registers graph v =
+ RegMap.forward v graph.regmap
+
+(* [mkipp graph regs1 regs2] adds interference edges between all pairs
+ of pseudoregisters [r1] and [r2], where [r1] ranges over [regs1],
+ [r2] ranges over [regs2], and [r1] and [r2] are distinct. *)
+
+let mkipp graph regs1 regs2 =
+ Pset.fold (fun r1 graph >
+ let v1 = lookup graph r1 in
+ Pset.fold (fun r2 graph >
+ interference#mkvv graph v1 (lookup graph r2)
+ ) regs2 graph
+ ) regs1 graph
+
+(* [mkiph graph regs hwregs] adds interference edges between all pairs
+ of a pseudoregister [r] and a hardware register [hwr], where [r]
+ ranges over [regs] and [hwr] ranges over [hwregs]. *)
+
+let mkiph graph regs hwregs =
+ Pset.fold (fun r graph >
+ let v = lookup graph r in
+ HwRegisterSet.fold (fun h graph >
+ interference#mkvh graph v h
+ ) hwregs graph
+ ) regs graph
+
+(* [mki graph regs1 regs2] adds interference edges between all pairs
+ of (pseudo or hardware) registers [r1] and [r2], where [r1] ranges
+ over [regs1], [r2] ranges over [regs2], and [r1] and [r2] are
+ distinct. *)
+
+let mki graph (regs1, hwregs1) (regs2, hwregs2) =
+ let graph = mkipp graph regs1 regs2 in
+ let graph = mkiph graph regs1 hwregs2 in
+ let graph = mkiph graph regs2 hwregs1 in
+ graph
+
+(* [mkppp graph r1 r2] adds a preference edge between the
+ pseudoregisters [r1] and [r2]. *)
+
+let mkppp graph r1 r2 =
+ let v1 = lookup graph r1
+ and v2 = lookup graph r2 in
+ let graph = preference#mkvv graph v1 v2 in
+ graph
+
+(* [mkpph graph r h] adds a preference edge between the
+ pseudoregister [r] and the hardware register [h]. *)
+
+let mkpph graph r h =
+ let v = lookup graph r in
+ let graph = preference#mkvh graph v h in
+ graph
+
+(*  *)
+
+(*
+(* Displaying interference graphs. *)
+
+open Printf
+
+let hwregs graph =
+ HwRegisterSet.union (interference#hwregs graph) (preference#hwregs graph)
+
+let print_vertex graph v =
+ Pset.print (registers graph v)
+
+let print f graph =
+
+ fprintf f "graph G {\n";
+(* fprintf f "size=\"6, 3\";\n"; (* in inches *)*)
+ fprintf f "orientation = landscape;\n";
+ fprintf f "rankdir = LR;\n";
+ fprintf f "ratio = compress;\n\n"; (* compress or fill or auto *)
+
+ RegMap.fold (fun vertex regs () >
+ fprintf f "r%d [ label=\"%s\" ] ;\n" vertex (Pset.print regs)
+ ) graph.regmap ();
+
+ HwRegisterSet.iter (fun hwr >
+ let name = I8051.print_register hwr in
+ fprintf f "hwr%s [ label=\"$%s\" ] ;\n" name name
+ ) (hwregs graph);
+
+ interference#iter graph
+ (fun vertex neighbor >
+ fprintf f "r%d  r%d ;\n" vertex neighbor)
+ (fun vertex neighbor >
+ fprintf f "r%d  hwr%s ;\n" vertex (I8051.print_register neighbor));
+
+ preference#iter graph
+ (fun vertex neighbor >
+ fprintf f "r%d  r%d [ style = dashed ] ;\n" vertex neighbor)
+ (fun vertex neighbor >
+ fprintf f "r%d  hwr%s [ style = dashed ] ;\n" vertex (I8051.print_register neighbor));
+
+ fprintf f "\n}\n"
+*)
+
+(*  *)
+
+(* Coalescing. *)
+
+(* [coalesce graph v1 v2] is a new graph where the vertices [v1] and [v2]
+ are coalesced. The new coalesced vertex is known under the name [v2]. *)
+
+let coalesce graph x y =
+
+ assert (x <> y); (* attempt to coalesce one vertex with itself *)
+ assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
+
+ (* Perform coalescing in the two subgraphs. *)
+
+ let graph = interference#coalesce graph x y in
+ let graph = preference#coalesce graph x y in
+
+ (* Remove [x] from all tables. *)
+
+ {
+ graph with
+ regmap = RegMap.coalesce x y graph.regmap;
+ ivh = Vertex.Map.remove x graph.ivh;
+ pvh = Vertex.Map.remove x graph.pvh;
+ degree = PrioritySet.remove x graph.degree;
+ nmr = PrioritySet.remove x graph.nmr;
+ }
+
+(* [coalesceh graph v h] coalesces the vertex [v] with the hardware register
+ [h]. This produces a new graph where [v] no longer exists and all edges
+ leading to [v] are replaced with edges leading to [h]. *)
+
+let coalesceh graph x h =
+
+ assert (not (interference#existsvh graph x h)); (* attempt to coalesce interfering entities *)
+
+ (* Perform coalescing in the two subgraphs. *)
+
+ let graph = interference#coalesceh graph x h in
+ let graph = preference#coalesceh graph x h in
+
+ (* Remove [x] from all tables. *)
+
+ {
+ graph with
+ regmap = RegMap.remove x graph.regmap;
+ ivh = Vertex.Map.remove x graph.ivh;
+ pvh = Vertex.Map.remove x graph.pvh;
+ degree = PrioritySet.remove x graph.degree;
+ nmr = PrioritySet.remove x graph.nmr;
+ }
+
+(*  *)
+
+(* [freeze graph x] is a new graph where all preference edges carried
+ by [x] are removed. *)
+
+let freeze graph x =
+ preference#remove graph x
+
+(*  *)
+
+(* Removal. *)
+
+(* [remove graph v] is a new graph where vertex [v] is removed. *)
+
+let remove graph v =
+
+ (* Remove all edges carried by [v]. *)
+
+ let graph = interference#remove graph v in
+ let graph = preference#remove graph v in
+
+ (* Remove [v] from all tables. *)
+
+ {
+ graph with
+ regmap = RegMap.remove v graph.regmap;
+ degree = PrioritySet.remove v graph.degree;
+ nmr = PrioritySet.remove v graph.nmr;
+ }
+
+(*  *)
+
+(* [mkdeg graph] recomputes degree information from scratch. *)
+
+let mkdeg graph =
+ let degree, nmr =
+ fold (fun v (degree, nmr) >
+ let d = interference#degree graph v in
+ PrioritySet.add v d degree,
+ if preference#nmr graph v then PrioritySet.add v d nmr else nmr
+ ) graph (PrioritySet.empty, PrioritySet.empty)
+ in
+ { graph with
+ degree = degree;
+ nmr = nmr;
+ }
+
+(* [restrict graph p] is a new graph where only those vertices that
+ satisfy predicate [p] are kept. The same effect could be obtained
+ by repeated application of [remove], but [restrict] is likely to be
+ more efficient if many vertices are removed. *)
+
+let restrict graph p =
+ mkdeg {
+ graph with
+ regmap = RegMap.restrict p graph.regmap;
+ ivv = VertexSetMap.restrict p graph.ivv;
+ ivh = Vertex.Map.restrict p graph.ivh;
+ pvv = VertexSetMap.restrict p graph.pvv;
+ pvh = Vertex.Map.restrict p graph.pvh;
+ }
+
+(* [droph graph] is a new graph where all information concerning hardware
+ registers has been dropped. *)
+
+let droph graph =
+ mkdeg {
+ graph with
+ ivh = Vertex.Map.empty;
+ pvh = Vertex.Map.empty;
+ }
+
Index: /extracted/untrusted/untrusted_interference.mli
===================================================================
 /extracted/untrusted/untrusted_interference.mli (revision 2738)
+++ /extracted/untrusted/untrusted_interference.mli (revision 2738)
@@ 0,0 +1,218 @@
+type pseudoregister = Registers.register
+type hwregister = I8051.register
+module HwRegisterSet : Set.S with type elt = hwregister
+
+(* Pasted from Pottier's PP compiler *)
+
+(** This module implements a data structure for interference graphs.
+ It provides functions that help construct, transform and inspect
+ interference graphs. *)
+
+(* Interference graphs record two kinds of edges: interference edges
+ (``these two vertices cannot receive the same color'') and
+ preference edges (``these two vertices should preferably receive
+ the same color''). Furthermore, each kind of edge can relate either
+ two pseudoregisters or one pseudoregister and one hardware
+ register. Thus, an interference graph keeps track of four kinds of
+ relationships.
+
+ This module automatically maintains the invariant that two vertices
+ [x] and [y] cannot be related by both an interference edge and a
+ preference edge. When such a situation appears (for instance,
+ because of coalescing), the preference edge is automatically
+ removed. *)
+
+type graph
+
+(* The vertices of an interference graph initially correspond to
+ pseudoregisters. However, interference graphs support coalescing,
+ which means that a new graph can be constructed by coalescing two
+ vertices in an existing graph. As a result, in general, the vertices
+ of an interference graph correspond to sets of pseudoregisters. *)
+
+(*  *)
+
+(* Operations over vertices: sets of vertices, maps over vertices. *)
+
+module Vertex : sig
+
+ type t
+
+ (* The usual operations on sets, see [Set.S] in Objective Caml's
+ documentation. *)
+
+ module Set : Set.S with type elt = t
+
+ (* The usual operations on maps, see [Map.S] in Objective Caml's
+ documentation. One slight difference is that [find] expects
+ the key to be present in the map  it will fail otherwise. *)
+
+ module Map : MyMap.S with type key = t
+
+end
+
+(*  *)
+
+(* Building interference graphs. *)
+
+(* [create regs] creates an interference graph whose vertices are
+ the pseudoregisters [regs] and that does not have any edges. *)
+
+val create: pseudoregister Pset.set > graph
+
+(* [mki graph regs1 regs2] adds interference edges between all pairs
+ of (pseudo or hardware) registers [r1] and [r2], where [r1] ranges
+ over [regs1], [r2] ranges over [regs2], and [r1] and [r2] are
+ distinct. *)
+
+val mki: graph >
+ pseudoregister Pset.set * HwRegisterSet.t >
+ pseudoregister Pset.set * HwRegisterSet.t >
+ graph
+
+(* [mkiph graph regs hwregs] adds interference edges between all pairs
+ of a pseudoregister [r] and a hardware register [hwr], where [r]
+ ranges over [regs] and [hwr] ranges over [hwregs]. *)
+
+val mkiph: graph > pseudoregister Pset.set > HwRegisterSet.t > graph
+
+(* [mkppp graph r1 r2] adds a preference edge between the
+ pseudoregisters [r1] and [r2]. *)
+
+val mkppp: graph > pseudoregister > pseudoregister > graph
+
+(* [mkpph graph r h] adds a preference edge between the
+ pseudoregister [r] and the hardware register [h]. *)
+
+val mkpph: graph > pseudoregister > hwregister > graph
+
+(*  *)
+
+(* Transforming interference graphs. *)
+
+(* [coalesce graph v1 v2] is a new graph where the vertices [v1] and
+ [v2] are coalesced. [v1] and [v2] must not interfere. The new
+ coalesced vertex is known under the name [v2]. *)
+
+val coalesce: graph > Vertex.t > Vertex.t > graph
+
+(* [coalesceh graph v h] coalesces the vertex [v] with the hardware register
+ [h]. This produces a new graph where [v] no longer exists and all edges
+ leading to [v] are replaced with edges leading to [h]. *)
+
+val coalesceh: graph > Vertex.t > I8051.register > graph
+
+(* [remove graph v] is a new graph where vertex [v] is removed. *)
+
+val remove: graph > Vertex.t > graph
+
+(* [freeze graph x] is a new graph where all preference edges carried
+ by [x] are removed. *)
+
+val freeze: graph > Vertex.t > graph
+
+(* [restrict graph p] is a new graph where only those vertices that
+ satisfy predicate [p] are kept. *)
+
+val restrict: graph > (Vertex.t > bool) > graph
+
+(* [droph graph] is a new graph where all information concerning hardware
+ registers has been dropped. *)
+
+val droph: graph > graph
+
+(*  *)
+
+(* Inspecting interference graphs. *)
+
+(* [lookup graph r] returns the graph vertex associated with
+ pseudoregister [r]. *)
+
+val lookup: graph > pseudoregister > Vertex.t
+
+(* Conversely, [registers graph v] returns the set of pseudoregisters
+ associated with vertex [v]. *)
+
+val registers: graph > Vertex.t > pseudoregister Pset.set
+
+(* [degree graph v] is the degree of the vertex [v], that is, the number
+ of vertices and hardware registers that [v] interferes with. *)
+
+val degree: graph > Vertex.t > int
+
+(* [lowest graph] returns [Some (v, d)], where the vertex [v] has
+ minimum degree [d], or returns [None] if the graph is empty. *)
+
+val lowest: graph > (Vertex.t * int) option
+
+(* [lowest_non_move_related graph] returns [Some (v, d)], where the
+ vertex [v] has minimum degree [d] among the vertices that are not
+ moverelated, or returns [None] if all vertices are moverelated. A
+ vertex is moverelated if it carries a preference edge. *)
+
+val lowest_non_move_related: graph > (Vertex.t * int) option
+
+(* [minimum f graph] returns a vertex [v] such that the value of [f x]
+ is minimal. The values returned by [f] are compared using Objective
+ Caml's generic comparison operator [<]. If the graph is empty,
+ [None] is returned. *)
+
+val minimum: (Vertex.t > 'a) > graph > Vertex.t option
+
+(* [fold f graph accu] folds over all vertices. *)
+
+val fold: (Vertex.t > 'a > 'a) > graph > 'a > 'a
+
+(* [ipp graph v] is the set of vertices that the vertex [v] interferes
+ with. *)
+
+val ipp: graph > Vertex.t > Vertex.Set.t
+
+(* [iph graph v] is the set of hardware registers that the vertex [v]
+ interferes with. *)
+
+val iph: graph > Vertex.t > HwRegisterSet.t
+
+(* [ppp graph v] is the set of vertices that should preferably be
+ assigned the same color as the vertex [v]. *)
+
+val ppp: graph > Vertex.t > Vertex.Set.t
+
+(* [pph graph v] is the set of hardware registers that [v] should
+ preferably be assigned. *)
+
+val pph: graph > Vertex.t > HwRegisterSet.t
+
+(* [pppick graph p] returns an arbitrary preference edge that
+ satisfies the predicate [p], if the graph contains one. *)
+
+type ppedge =
+ Vertex.t * Vertex.t
+
+val pppick: graph > (ppedge > bool) > ppedge option
+
+(* [phpick graph p] returns an arbitrary preference edge that
+ satisfies the predicate [p], if the graph contains one. *)
+
+type phedge =
+ Vertex.t * I8051.register
+
+val phpick: graph > (phedge > bool) > phedge option
+
+(*
+(*  *)
+
+(* Displaying interference graphs. *)
+
+(* [print_vertex graph v] produces a string representation of the
+ vertex [v]. *)
+
+val print_vertex: graph > Vertex.t > string
+
+(* [print f graph] prints a representation of the interference graph
+ [graph] in [dot] format to the output channel [f]. Interference
+ edges are drawn as plain lines; preference edges are drawn as
+ dotted lines. *)
+
+val print: out_channel > graph > unit
+*)