hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-17 01:03:14 +01:00
Code Issues Packages Projects Releases Wiki Activity

UniversalFlow: More renaming.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2024-10-28 16:31:23 +01:00
parent 7d98d391b7
commit 1d3bad1358
2 changed files with 29 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files

52
shared/typeflow/codeql/typeflow/UniversalFlow.qll
View File

@@ -60,7 +60,7 @@ signature module UniversalFlowInput<LocationSig Location> {
default predicate isExcludedFromNullAnalysis(FlowNode n) { none() }
}
module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
module Make<LocationSig Location, UniversalFlowInput<Location> I> {
private import I
/**
@@ -170,48 +170,48 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
int lastRank(Node n) { result = max(int r | edgeRank(r, _, n)) }
}
private signature module TypePropagation {
class Typ;
private signature module PropPropagation {
class Prop;
predicate candType(FlowNode n, Typ t);
predicate candProp(FlowNode n, Prop t);
bindingset[t]
predicate supportsType(FlowNode n, Typ t);
predicate supportsProp(FlowNode n, Prop t);
}
/** Implements recursion through `forall` by way of edge ranking. */
private module ForAll<NodeSig Node, RankedEdge<Node> E, TypePropagation T> {
private module ForAll<NodeSig Node, RankedEdge<Node> E, PropPropagation T> {
/**
* Holds if `t` is a bound that holds on one of the incoming edges to `n` and
* thus is a candidate bound for `n`.
* Holds if `t` is a property that holds on one of the incoming edges to `n` and
* thus is a candidate property for `n`.
*/
pragma[nomagic]
private predicate candJoinType(Node n, T::Typ t) {
private predicate candJoinProp(Node n, T::Prop t) {
exists(FlowNode mid |
T::candType(mid, t) and
T::candProp(mid, t) and
E::edgeRank(_, mid, n)
)
}
/**
* Holds if `t` is a candidate bound for `n` that is also valid for data coming
* Holds if `t` is a candidate property for `n` that is also valid for data coming
* through the edges into `n` ranked from `1` to `r`.
*/
private predicate flowJoin(int r, Node n, T::Typ t) {
private predicate flowJoin(int r, Node n, T::Prop t) {
(
r = 1 and candJoinType(n, t)
r = 1 and candJoinProp(n, t)
or
flowJoin(r - 1, n, t) and E::edgeRank(r, _, n)
) and
forall(FlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
forall(FlowNode mid | E::edgeRank(r, mid, n) | T::supportsProp(mid, t))
}
/**
* Holds if `t` is a candidate bound for `n` that is also valid for data
* coming through all the incoming edges, and therefore is a valid bound for
* Holds if `t` is a candidate property for `n` that is also valid for data
* coming through all the incoming edges, and therefore is a valid property for
* `n`.
*/
predicate flowJoin(Node n, T::Typ t) { flowJoin(E::lastRank(n), n, t) }
predicate flowJoin(Node n, T::Prop t) { flowJoin(E::lastRank(n), n, t) }
}
private module JoinStep implements Edge {
@@ -237,12 +237,12 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
}
module FlowNullary<NullaryPropertySig P> {
private module Propagation implements TypePropagation {
class Typ = Unit;
private module Propagation implements PropPropagation {
class Prop = Unit;
predicate candType(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
predicate candProp(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
predicate supportsType = candType/2;
predicate supportsProp = candProp/2;
}
predicate hasProperty(FlowNode n) {
@@ -278,14 +278,14 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
}
module Flow<PropertySig P> {
private module Propagation implements TypePropagation {
class Typ = P::Prop;
private module Propagation implements PropPropagation {
class Prop = P::Prop;
predicate candType = hasProperty/2;
predicate candProp = hasProperty/2;
bindingset[t]
predicate supportsType(FlowNode n, Typ t) {
exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
predicate supportsProp(FlowNode n, Prop t) {
exists(Prop t0 | hasProperty(n, t0) and P::propImplies(t0, t))
}
}

6
shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
View File

@@ -1,12 +1,12 @@
private import codeql.typeflow.TypeFlow
private import codeql.typeflow.UniversalFlow
private import codeql.typeflow.UniversalFlow as UniversalFlow
private import codeql.util.Location
private import codeql.util.Unit
module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
private import I
private module UfInput implements UniversalFlowInput<Location> {
private module UfInput implements UniversalFlow::UniversalFlowInput<Location> {
class FlowNode = TypeFlowNode;
predicate step = I::step/2;
@@ -16,7 +16,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
predicate isExcludedFromNullAnalysis = I::isExcludedFromNullAnalysis/1;
}
private module UnivFlow = UfMake<Location, UfInput>;
private module UnivFlow = UniversalFlow::Make<Location, UfInput>;
private module ExactTypeProperty implements UnivFlow::PropertySig {
class Prop = Type;