From 579b57cf6786322114a0f8cf3d926694a434392f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 11 Mar 2022 11:55:22 +0000 Subject: [PATCH] Range analysis: use ranked phi nodes This borrows a technique (and the implementing code) off Modulus analysis. --- .../code/csharp/dataflow/ModulusAnalysis.qll | 7 ---- .../rangeanalysis/ModulusAnalysisSpecific.qll | 33 --------------- .../rangeanalysis/SsaReadPositionCommon.qll | 8 ++++ .../rangeanalysis/SsaReadPositionSpecific.qll | 40 +++++++++++++++++++ .../code/java/dataflow/ModulusAnalysis.qll | 7 ---- .../code/java/dataflow/RangeAnalysis.qll | 25 +++++++++++- .../rangeanalysis/ModulusAnalysisSpecific.qll | 20 ---------- .../rangeanalysis/SsaReadPositionCommon.qll | 8 ++++ .../rangeanalysis/SsaReadPositionSpecific.qll | 26 ++++++++++++ 9 files changed, 105 insertions(+), 69 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll index 2a58cba6209b..b919d143a396 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll @@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) { ) } -/** - * Holds if `rix` is the number of input edges to `phi`. - */ -private predicate maxPhiInputRank(SsaPhiNode phi, int rix) { - rix = max(int r | rankedPhiInput(phi, _, _, r)) -} - /** * Gets the remainder of `val` modulo `mod`. * diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll index 030020ede632..74aee61e6906 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll @@ -43,37 +43,4 @@ module Private { predicate ssaUpdateStep = RU::ssaUpdateStep/3; Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() } - - private class PhiInputEdgeBlock extends BasicBlock { - PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() } - } - - int getId(PhiInputEdgeBlock bb) { - exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) | - t = bb.getFirstNode().getElement() - or - t = bb.(CS::ControlFlow::BasicBlocks::EntryBlock).getCallable() - ) - } - - private string getSplitString(PhiInputEdgeBlock bb) { - result = bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString() - or - not exists(bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()) and - result = "" - } - - /** - * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` - * in an arbitrary 1-based numbering of the input edges to `phi`. - */ - predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) { - edge.phiInput(phi, inp) and - edge = - rank[r](SsaReadPositionPhiInputEdge e | - e.phiInput(phi, _) - | - e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock()) - ) - } } diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll index e450c11b5ab5..08335f6680dd 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll @@ -3,6 +3,7 @@ */ private import SsaReadPositionSpecific +import SsaReadPositionSpecific::Public private newtype TSsaReadPosition = TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or @@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn override string toString() { result = "edge" } } + +/** + * Holds if `rix` is the number of input edges to `phi`. + */ +predicate maxPhiInputRank(SsaPhiNode phi, int rix) { + rix = max(int r | rankedPhiInput(phi, _, _, r)) +} diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll index 7afd9a2a33dd..6b91651691d5 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll @@ -3,6 +3,8 @@ */ private import csharp +private import SsaReadPositionCommon +private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl class SsaVariable = Ssa::Definition; @@ -14,3 +16,41 @@ class BasicBlock = ControlFlow::BasicBlock; BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getARead().getAControlFlowNode().getBasicBlock() } + +private class PhiInputEdgeBlock extends BasicBlock { + PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() } +} + +private int getId(PhiInputEdgeBlock bb) { + exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) | + t = bb.getFirstNode().getElement() + or + t = bb.(ControlFlow::BasicBlocks::EntryBlock).getCallable() + ) +} + +private string getSplitString(PhiInputEdgeBlock bb) { + result = bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString() + or + not exists(bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString()) and + result = "" +} + +/** + * Declarations to be exposed to users of SsaReadPositionCommon. + */ +module Public { + /** + * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` + * in an arbitrary 1-based numbering of the input edges to `phi`. + */ + predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) { + edge.phiInput(phi, inp) and + edge = + rank[r](SsaReadPositionPhiInputEdge e | + e.phiInput(phi, _) + | + e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock()) + ) + } +} diff --git a/java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll index 2a58cba6209b..b919d143a396 100644 --- a/java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll @@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) { ) } -/** - * Holds if `rix` is the number of input edges to `phi`. - */ -private predicate maxPhiInputRank(SsaPhiNode phi, int rix) { - rix = max(int r | rankedPhiInput(phi, _, _, r)) -} - /** * Gets the remainder of `val` modulo `mod`. * diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index de7aca884342..47c3cdd9db63 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -725,6 +725,26 @@ private predicate boundedPhiCandValidForEdge( ) } +/** + * Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge. + * - `upper = true` : `phi <= b + delta` + * - `upper = false` : `phi >= b + delta` + */ +private predicate boundedPhiStep( + SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, + Reason reason, int rix +) { + exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge | + rankedPhiInput(phi, inp, edge, rix) and + boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) and + ( + rix = 1 + or + boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1) + ) + ) +} + /** * Holds if `b + delta` is a valid bound for `phi`. * - `upper = true` : `phi <= b + delta` @@ -734,8 +754,9 @@ private predicate boundedPhi( SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason ) { - forex(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) | - boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) + exists(int r | + boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r) and + maxPhiInputRank(phi, r) ) } diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll index fc17dbfd979b..c5d5bc980094 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll @@ -111,24 +111,4 @@ module Private { predicate ssaUpdateStep = RU::ssaUpdateStep/3; Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() } - - private predicate id(BasicBlock x, BasicBlock y) { x = y } - - private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y) - - private int getId(BasicBlock bb) { idOf(bb, result) } - - /** - * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` - * in an arbitrary 1-based numbering of the input edges to `phi`. - */ - predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) { - edge.phiInput(phi, inp) and - edge = - rank[r](SsaReadPositionPhiInputEdge e | - e.phiInput(phi, _) - | - e order by getId(e.getOrigBlock()) - ) - } } diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll index e450c11b5ab5..08335f6680dd 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll @@ -3,6 +3,7 @@ */ private import SsaReadPositionSpecific +import SsaReadPositionSpecific::Public private newtype TSsaReadPosition = TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or @@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn override string toString() { result = "edge" } } + +/** + * Holds if `rix` is the number of input edges to `phi`. + */ +predicate maxPhiInputRank(SsaPhiNode phi, int rix) { + rix = max(int r | rankedPhiInput(phi, _, _, r)) +} diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll index dcfc3d69e320..410dc6b5cfeb 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll @@ -4,6 +4,7 @@ private import semmle.code.java.dataflow.SSA as Ssa private import semmle.code.java.controlflow.BasicBlocks as BB +private import SsaReadPositionCommon class SsaVariable = Ssa::SsaVariable; @@ -13,3 +14,28 @@ class BasicBlock = BB::BasicBlock; /** Gets a basic block in which SSA variable `v` is read. */ BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getAUse().getBasicBlock() } + +private predicate id(BasicBlock x, BasicBlock y) { x = y } + +private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y) + +private int getId(BasicBlock bb) { idOf(bb, result) } + +/** + * Declarations to be exposed to users of SsaReadPositionCommon + */ +module Public { + /** + * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` + * in an arbitrary 1-based numbering of the input edges to `phi`. + */ + predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) { + edge.phiInput(phi, inp) and + edge = + rank[r](SsaReadPositionPhiInputEdge e | + e.phiInput(phi, _) + | + e order by getId(e.getOrigBlock()) + ) + } +}