TypeFlow: Simplify interface.

This commit is contained in:
Anders Schack-Mulligen
2024-10-28 15:09:09 +01:00
parent 3939eff260
commit fba4d09e65
4 changed files with 27 additions and 31 deletions

View File

@@ -28,16 +28,11 @@ signature module TypeFlowInput<LocationSig Location> {
}
/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
* necessarily functionally determined by `n2`.
* Holds if data can flow from `n1` to `n2` in one step.
*
* For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
*/
predicate joinStep(TypeFlowNode n1, TypeFlowNode n2);
/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is
* functionally determined by `n2`.
*/
predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2);
predicate step(TypeFlowNode n1, TypeFlowNode n2);
/** Holds if `n` represents a `null` value. */
predicate isNullValue(TypeFlowNode n);

View File

@@ -5,8 +5,20 @@ private import codeql.util.Unit
module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
private import I
/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is
* functionally determined by `n2`.
*/
private predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) { n1 = unique(TypeFlowNode n | step(n, n2)) }
/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
* functionally determined by `n2`.
*/
private predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
/** Holds if `null` is the only value that flows to `n`. */
predicate isNull(TypeFlowNode n) {
private predicate isNull(TypeFlowNode n) {
isNullValue(n)
or
exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))