Index: /extracted/Fix.ml
===================================================================
--- /extracted/Fix.ml (revision 2736)
+++ /extracted/Fix.ml (revision 2736)
@@ -0,0 +1,554 @@
+(**************************************************************************)
+(* *)
+(* Fix *)
+(* *)
+(* Author: François Pottier, INRIA Paris-Rocquencourt *)
+(* 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 CeCILL-C (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] self-contained. *)
+
+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 doubly-linked adjacency lists, one could implement [predecessors]
+ in worst-case linear time with respect to the length of the output list,
+ [set_successors] in worst-case linear time with respect to the length of
+ the input list, and [clear_successors] in worst-case linear time with
+ respect to the number of edges that are removed. We use a simpler
+ implementation, based on singly-linked 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 right-hand 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] re-evaluates the right-hand 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 right-hand 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
+ top-down 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 top-down, 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/Fix.mli
===================================================================
--- /extracted/Fix.mli (revision 2736)
+++ /extracted/Fix.mli (revision 2736)
@@ -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 Paris-Rocquencourt *)
+(* 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 CeCILL-C (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 right-hand side, when supplied with a valuation that gives
+ meaning to its free variables, evaluates to a property. More
+ precisely, a right-hand side is a monotone function of
+ valuations to properties. *)
+ type rhs = valuation -> property
+
+ (* A system of equations is a mapping of variables to right-hand
+ 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 right-hand side produced by this
+ application is, in general, evaluated multiple times). This guarantee can
+ be used to perform costly pre-computation, 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/PROBLEMS
===================================================================
--- /extracted/PROBLEMS (revision 2735)
+++ /extracted/PROBLEMS (revision 2736)
@@ -28,4 +28,7 @@
a) two in compiler.ml (the backend and the compiler itself)
+ - file Fix.ml taken from the untrusted prototype and modified to
+ redefine a few functions from OCaml's List due to module name shadowing
+ - file compute_fixpoints.ml to adapt Fix.ml to the rest
b) set_adt currently implemented by cut&paste from OCaml's set.ml, but
using Pervasives.compare: the equality function taken in input is ignored!
Index: /extracted/compiler.ml
===================================================================
--- /extracted/compiler.ml (revision 2735)
+++ /extracted/compiler.ml (revision 2736)
@@ -271,6 +271,5 @@
(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
-let compute_fixpoint _ =
- failwith "AXIOM TO BE REALIZED"
+let compute_fixpoint = Compute_fixpoints.compute_fixpoint
(** val colour_graph : Interference.coloured_graph_computer **)
Index: /extracted/compute_fixpoints.ml
===================================================================
--- /extracted/compute_fixpoints.ml (revision 2736)
+++ /extracted/compute_fixpoints.ml (revision 2736)
@@ -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/compute_fixpoints.mli
===================================================================
--- /extracted/compute_fixpoints.mli (revision 2736)
+++ /extracted/compute_fixpoints.mli (revision 2736)
@@ -0,0 +1,1 @@
+val compute_fixpoint : Fixpoints.fixpoint_computer