Skip to content

C++: Work around poor codegen for forex in IR-based range analysis #13035

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rdmarsh2 merged 1 commit into from
May 4, 2023
Merged

C++: Work around poor codegen for forex in IR-based range analysis #13035

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 0 additions & 23 deletions cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,13 +120,6 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
)
}

/**
* Holds if `rix` is the number of input edges to `phi`.
*/
private predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}

/**
* Gets the remainder of `val` modulo `mod`.
*
Expand Down Expand Up @@ -322,20 +315,4 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
semExprModulus(rarg, b, val, mod) and isLeft = false
)
}

/**
* 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`.
*/
private predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
}
}
21 changes: 19 additions & 2 deletions ...l/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -877,6 +877,22 @@ module RangeStage<
)
}

pragma[assume_small_delta]
pragma[nomagic]
private predicate boundedPhiRankStep(
SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
D::Delta origdelta, SemReason reason, int rix
) {
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
Utils::rankedPhiInput(phi, inp, edge, rix) and
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
|
if rix = 1
then any()
else boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
)
}

/**
* Holds if `b + delta` is a valid bound for `phi`.
* - `upper = true` : `phi <= b + delta`
Expand All @@ -886,8 +902,9 @@ module RangeStage<
SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
D::Delta origdelta, SemReason reason
) {
forex(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
exists(int r |
Utils::maxPhiInputRank(phi, r) and
boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r)
)
}

Expand Down
23 changes: 23 additions & 0 deletions cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,3 +138,26 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
}
}

/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}

/**
* 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(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
Copy link
Copy Markdown
Contributor

@jbj jbj May 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How unique are these ids? From what I can tell, this call ultimately leads to the database id of block.getFirstInstruction().getAst(). Can it never happen that an AST element produces two different instructions that are both first in a basic block?

Copy link
Copy Markdown
Contributor Author

@MathiasVP MathiasVP May 4, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, the result of e.getOrigBlock().getUniqueId() is the database id of e's IRBlock's getFirstInstruction().getAst(). I can't quite think of an AST element with that property, but I'm sure one can construct something like this (maybe something involving the ternary operator?).

Originally, we were using the display index from the basic block, but this was totally infeasible to compute on real projects. If you have any suggestions for an integer representation whose uniqueness is easier to argue I'm all for it 😄.

This scheme has been used for a while now already in the new range-analysis library (in the modulus-phase) without any observable issues, though.

Copy link
Copy Markdown
Contributor

@jbj jbj May 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It should be easy to check with a consistency query whether two IRBlocks ever get the same id. And even if they do, I suppose it only matters here if those IRBlocks go into the same phi node.

Copy link
Copy Markdown
Contributor Author

@MathiasVP MathiasVP May 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed

)
}