1 files changed, 151 insertions, 0 deletions
diff --git a/cil/src/ext/dataflow.mli b/cil/src/ext/dataflow.mli
new file mode 100755
index 0000000..e72c5db
--- /dev/null
+++ b/cil/src/ext/dataflow.mli
@@ -0,0 +1,151 @@
+(** A framework for data flow analysis for CIL code.  Before using 
+    this framework, you must initialize the Control-flow Graph for your
+    program, e.g using {!Cfg.computeFileCFG} *)
+
+type 't action = 
+    Default (** The default action *)
+  | Done of 't (** Do not do the default action. Use this result *)
+  | Post of ('t -> 't) (** The default action, followed by the given 
+                        * transformer *)
+
+type 't stmtaction = 
+    SDefault   (** The default action *)
+  | SDone      (** Do not visit this statement or its successors *)
+  | SUse of 't (** Visit the instructions and successors of this statement
+                  as usual, but use the specified state instead of the 
+                  one that was passed to doStmt *)
+
+(* For if statements *)
+type 't guardaction = 
+    GDefault      (** The default state *) 
+  | GUse of 't    (** Use this data for the branch *)
+  | GUnreachable  (** The branch will never be taken. *)
+
+
+(******************************************************************
+ **********
+ **********         FORWARDS 
+ **********
+ ********************************************************************)
+
+module type ForwardsTransfer = sig
+  val name: string (** For debugging purposes, the name of the analysis *)
+
+  val debug: bool ref (** Whether to turn on debugging *)
+
+  type t  (** The type of the data we compute for each block start. May be 
+           * imperative.  *)
+
+  val copy: t -> t
+  (** Make a deep copy of the data *)
+
+
+  val stmtStartData: t Inthash.t
+  (** For each statement id, the data at the start. Not found in the hash 
+   * table means nothing is known about the state at this point. At the end 
+   * of the analysis this means that the block is not reachable. *)
+
+  val pretty: unit -> t -> Pretty.doc 
+  (** Pretty-print the state *)
+
+  val computeFirstPredecessor: Cil.stmt -> t -> t
+  (** Give the first value for a predecessors, compute the value to be set 
+   * for the block *)
+
+  val combinePredecessors: Cil.stmt -> old:t -> t -> t option
+  (** Take some old data for the start of a statement, and some new data for 
+   * the same point. Return None if the combination is identical to the old 
+   * data. Otherwise, compute the combination, and return it. *)
+
+  val doInstr: Cil.instr -> t -> t action
+  (** The (forwards) transfer function for an instruction. The 
+   * {!Cil.currentLoc} is set before calling this. The default action is to 
+   * continue with the state unchanged. *)
+
+  val doStmt: Cil.stmt -> t -> t stmtaction
+  (** The (forwards) transfer function for a statement. The {!Cil.currentLoc} 
+   * is set before calling this. The default action is to do the instructions
+   * in this statement, if applicable, and continue with the successors. *)
+
+  val doGuard: Cil.exp -> t -> t guardaction
+  (** Generate the successor to an If statement assuming the given expression
+    * is nonzero.  Analyses that don't need guard information can return 
+    * GDefault; this is equivalent to returning GUse of the input.
+    * A return value of GUnreachable indicates that this half of the branch
+    * will not be taken and should not be explored.  This will be called
+    * twice per If, once for "then" and once for "else".  
+    *)
+
+  val filterStmt: Cil.stmt -> bool
+  (** Whether to put this statement in the worklist. This is called when a 
+   * block would normally be put in the worklist. *)
+  
+end
+
+module ForwardsDataFlow (T : ForwardsTransfer) : sig
+  val compute: Cil.stmt list -> unit
+  (** Fill in the T.stmtStartData, given a number of initial statements to 
+   * start from. All of the initial statements must have some entry in 
+   * T.stmtStartData (i.e., the initial data should not be bottom) *)
+end
+
+(******************************************************************
+ **********
+ **********         BACKWARDS 
+ **********
+ ********************************************************************)
+module type BackwardsTransfer = sig
+  val name: string (** For debugging purposes, the name of the analysis *)
+
+  val debug: bool ref (** Whether to turn on debugging *)
+
+  type t  (** The type of the data we compute for each block start. In many 
+           * presentations of backwards data flow analysis we maintain the 
+           * data at the block end. This is not easy to do with JVML because 
+           * a block has many exceptional ends. So we maintain the data for 
+           * the statement start. *)
+
+  val pretty: unit -> t -> Pretty.doc (** Pretty-print the state *)
+
+  val stmtStartData: t Inthash.t
+  (** For each block id, the data at the start. This data structure must be 
+   * initialized with the initial data for each block *)
+
+  val combineStmtStartData: Cil.stmt -> old:t -> t -> t option
+  (** When the analysis reaches the start of a block, combine the old data 
+   * with the one we have just computed. Return None if the combination is 
+   * the same as the old data, otherwise return the combination. In the 
+   * latter case, the predecessors of the statement are put on the working 
+   * list. *)
+
+
+  val combineSuccessors: t -> t -> t
+  (** Take the data from two successors and combine it *)
+
+
+  val doStmt: Cil.stmt -> t action
+  (** The (backwards) transfer function for a branch. The {!Cil.currentLoc} is 
+   * set before calling this. If it returns None, then we have some default 
+   * handling. Otherwise, the returned data is the data before the branch 
+   * (not considering the exception handlers) *)
+
+  val doInstr: Cil.instr -> t -> t action
+  (** The (backwards) transfer function for an instruction. The 
+   * {!Cil.currentLoc} is set before calling this. If it returns None, then we 
+   * have some default handling. Otherwise, the returned data is the data 
+   * before the branch (not considering the exception handlers) *)
+
+  val filterStmt: Cil.stmt -> Cil.stmt -> bool
+  (** Whether to put this predecessor block in the worklist. We give the 
+   * predecessor and the block whose predecessor we are (and whose data has 
+   * changed)  *)
+  
+end
+
+module BackwardsDataFlow (T : BackwardsTransfer) : sig
+  val compute: Cil.stmt list -> unit
+  (** Fill in the T.stmtStartData, given a number of initial statements to 
+   * start from (the sinks for the backwards data flow). All of the statements
+   * (not just the initial ones!) must have some entry in T.stmtStartData 
+   * (i.e., the initial data should not be bottom) *)
+end