1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
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
|
