public class ReachChecker extends DataFlow<ReachChecker.DataFlowItem>
| Modifier and Type | Class and Description |
|---|---|
protected static class |
ReachChecker.DataFlowItem |
DataFlow.BoolItem<FlowItem extends DataFlow.Item>, DataFlow.ConditionNavigator<FlowItem extends DataFlow.Item>, DataFlow.FlowGraphSource<FlowItem extends DataFlow.Item>, DataFlow.Frame<FlowItem extends DataFlow.Item>, DataFlow.ItemdataflowOnEntry, detectBackEdges, flowCounter, flowgraphStack, forward, postorderingerror, job, nf, tsbypass, bypassParent| Constructor and Description |
|---|
ReachChecker(Job job,
TypeSystem ts,
NodeFactory nf) |
| Modifier and Type | Method and Description |
|---|---|
void |
check(FlowGraph<ReachChecker.DataFlowItem> graph,
Term n,
boolean entry,
ReachChecker.DataFlowItem inItem,
java.util.Map<FlowGraph.EdgeKey,ReachChecker.DataFlowItem> outItems)
Check that the term n satisfies whatever properties this
dataflow is checking for.
|
protected Node |
checkReachability(Term n) |
ReachChecker.DataFlowItem |
confluence(java.util.List<ReachChecker.DataFlowItem> inItems,
FlowGraph.Peer<ReachChecker.DataFlowItem> peer,
FlowGraph<ReachChecker.DataFlowItem> graph)
The confluence operator for many flows.
|
ReachChecker.DataFlowItem |
confluence(java.util.List<ReachChecker.DataFlowItem> inItems,
java.util.List<FlowGraph.EdgeKey> itemKeys,
FlowGraph.Peer<ReachChecker.DataFlowItem> peer,
FlowGraph<ReachChecker.DataFlowItem> graph)
The confluence operator for many flows.
|
protected CFGBuilder<ReachChecker.DataFlowItem> |
createCFGBuilder(TypeSystem ts,
FlowGraph<ReachChecker.DataFlowItem> g)
Construct a CFGBuilder.
|
ReachChecker.DataFlowItem |
createInitialItem(FlowGraph<ReachChecker.DataFlowItem> graph,
Term node,
boolean entry)
Create an initial Item for the term node.
|
java.util.Map<FlowGraph.EdgeKey,ReachChecker.DataFlowItem> |
flow(ReachChecker.DataFlowItem in,
FlowGraph<ReachChecker.DataFlowItem> graph,
FlowGraph.Peer<ReachChecker.DataFlowItem> peer)
Produce new
Items as appropriate for the
Peer and the input Items. |
Node |
leaveCall(Node old,
Node n,
NodeVisitor v)
Overridden superclass method, to pop from the stack of
FlowGraphs if necessary. |
void |
post(FlowGraph<ReachChecker.DataFlowItem> graph,
Term root)
Check all of the Peers in the graph, after the dataflow analysis has
been performed.
|
check, constructItemsFromCondition, createFrame, createInitialItem, currentFlowGraph, dataflow, dataflow, dataflow, dumpFlowGraph, enterCall, filterItems, filterItemsExceptionSubclass, filterItemsNonError, filterItemsNonException, findSCCs, flow, flow, flow, flow, flowBooleanConditions, flowToBooleanFlow, hasTrueFalseBranches, initGraph, initGraph, itemsToMap, itemToMap, lang, leave, safeConfluence, safeConfluence, safeConfluencebegin, catchErrors, enter, enterCall, enterError, errorQueue, hasErrors, job, leaveCall, leaveCall, nodeFactory, typeSystembypass, bypass, bypassChildren, override, visitChildrencopy, enter, finish, finish, leave, override, toString, visitEdge, visitEdgeNoOverridepublic ReachChecker(Job job, TypeSystem ts, NodeFactory nf)
protected CFGBuilder<ReachChecker.DataFlowItem> createCFGBuilder(TypeSystem ts, FlowGraph<ReachChecker.DataFlowItem> g)
DataFlowcreateCFGBuilder in class DataFlow<ReachChecker.DataFlowItem>ts - The type systemg - The flow graph to that the CFGBuilder will construct.public ReachChecker.DataFlowItem createInitialItem(FlowGraph<ReachChecker.DataFlowItem> graph, Term node, boolean entry)
DataFlowcreateInitialItem in class DataFlow<ReachChecker.DataFlowItem>public java.util.Map<FlowGraph.EdgeKey,ReachChecker.DataFlowItem> flow(ReachChecker.DataFlowItem in, FlowGraph<ReachChecker.DataFlowItem> graph, FlowGraph.Peer<ReachChecker.DataFlowItem> peer)
DataFlowItems as appropriate for the
Peer and the input Items.flow in class DataFlow<ReachChecker.DataFlowItem>graph - the FlowGraph which the dataflow is operating onpeer - the Peer which this method must calculate the flow for.public ReachChecker.DataFlowItem confluence(java.util.List<ReachChecker.DataFlowItem> inItems, FlowGraph.Peer<ReachChecker.DataFlowItem> peer, FlowGraph<ReachChecker.DataFlowItem> graph)
DataFlowconfluence in class DataFlow<ReachChecker.DataFlowItem>inItems - List of Items that flow into node.
this method will only be called if the list has at least 2
elements.peer - Peer for which the items are
flowing into.public ReachChecker.DataFlowItem confluence(java.util.List<ReachChecker.DataFlowItem> inItems, java.util.List<FlowGraph.EdgeKey> itemKeys, FlowGraph.Peer<ReachChecker.DataFlowItem> peer, FlowGraph<ReachChecker.DataFlowItem> graph)
DataFlowconfluence in class DataFlow<ReachChecker.DataFlowItem>inItems - List of Items that flow into node.
This method will only be called if the list has at least 2
elements.itemKeys - List of FlowGraph.ExceptionEdgeKeys for
the edges that the corresponding Items in
items flowed from.peer - Peer for which the items are
flowing into.public Node leaveCall(Node old, Node n, NodeVisitor v) throws SemanticException
DataFlowFlowGraphs if necessary.leaveCall in class DataFlow<ReachChecker.DataFlowItem>SemanticExceptionprotected Node checkReachability(Term n) throws SemanticException
SemanticExceptionpublic void post(FlowGraph<ReachChecker.DataFlowItem> graph, Term root) throws SemanticException
DataFlowpost in class DataFlow<ReachChecker.DataFlowItem>SemanticExceptionpublic void check(FlowGraph<ReachChecker.DataFlowItem> graph, Term n, boolean entry, ReachChecker.DataFlowItem inItem, java.util.Map<FlowGraph.EdgeKey,ReachChecker.DataFlowItem> outItems) throws SemanticException
DataFlowcheck in class DataFlow<ReachChecker.DataFlowItem>SemanticException - if the properties this dataflow
analysis is checking for is not satisfied.