Skip to content

Commit

Permalink
Merge pull request #13880 from MathiasVP/type-bounds-preparation
Browse files Browse the repository at this point in the history
C++: Add a type-based `SemReason`.
  • Loading branch information
MathiasVP authored Aug 4, 2023
2 parents 877ee70 + 98e670f commit 3e9d9e7
Show file tree
Hide file tree
Showing 5 changed files with 195 additions and 51 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,24 @@
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import codeql.util.Unit
private import Reason as Reason
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta

module CppLangImplConstant implements LangSig<FloatDelta> {
private module Param implements Reason::ParamSig {
class TypeReasonImpl = Unit;
}

class SemReason = Reason::Make<Param>::SemReason;

class SemNoReason = Reason::Make<Param>::SemNoReason;

class SemCondReason = Reason::Make<Param>::SemCondReason;

class SemTypeReason = Reason::Make<Param>::SemTypeReason;

/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -61,18 +61,23 @@ private newtype TSemReason =
guard = any(ConstantStage::SemCondReason reason).getCond()
or
guard = any(RelativeStage::SemCondReason reason).getCond()
}
} or
TSemTypeReason()

ConstantStage::SemReason constantReason(SemReason reason) {
private ConstantStage::SemReason constantReason(SemReason reason) {
result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
or
result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
or
result instanceof ConstantStage::SemTypeReason and reason instanceof SemTypeReason
}

RelativeStage::SemReason relativeReason(SemReason reason) {
private RelativeStage::SemReason relativeReason(SemReason reason) {
result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
or
result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
or
result instanceof RelativeStage::SemTypeReason and reason instanceof SemTypeReason
}

import Public
Expand Down Expand Up @@ -111,4 +116,12 @@ module Public {

override string toString() { result = this.getCond().toString() }
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* based on type-information.
*/
class SemTypeReason extends SemReason, TSemTypeReason {
override string toString() { result = "TypeReason" }
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,25 @@ private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
private import RangeAnalysisImpl
private import codeql.util.Unit
private import Reason as Reason
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils

module CppLangImplRelative implements LangSig<FloatDelta> {
private module Param implements Reason::ParamSig {
class TypeReasonImpl extends Unit {
TypeReasonImpl() { none() }
}
}

class SemReason = Reason::Make<Param>::SemReason;

class SemNoReason = Reason::Make<Param>::SemNoReason;

class SemCondReason = Reason::Make<Param>::SemCondReason;

class SemTypeReason = Reason::Make<Param>::SemTypeReason;

/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,37 @@ signature module DeltaSig {
}

signature module LangSig<DeltaSig D> {
/** A reason for an inferred bound. */
class SemReason {
/**
* Returns `this` if `reason` is not a `SemTypeReason`. Otherwise,
* this predicate returns `SemTypeReason`.
*
* This predicate ensures that we propagate `SemTypeReason` all the way
* to the top-level of a call to `semBounded` if the inferred bound is
* based on type-information.
*/
bindingset[this, reason]
SemReason combineWith(SemReason reason);
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* without going through a bounding condition.
*/
class SemNoReason extends SemReason;

/** A reason for an inferred bound pointing to a condition. */
class SemCondReason extends SemReason {
SemGuard getCond();
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* based on type-information.
*/
class SemTypeReason extends SemReason;

/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*
Expand Down Expand Up @@ -249,6 +280,14 @@ module RangeStage<
DeltaSig D, BoundSig<D> Bounds, OverflowSig<D> OverflowParam, LangSig<D> LangParam,
UtilSig<D> UtilParam>
{
class SemReason = LangParam::SemReason;

class SemCondReason = LangParam::SemCondReason;

class SemNoReason = LangParam::SemNoReason;

class SemTypeReason = LangParam::SemTypeReason;

private import Bounds
private import LangParam
private import UtilParam
Expand Down Expand Up @@ -509,36 +548,6 @@ module RangeStage<
)
}

private newtype TSemReason =
TSemNoReason() or
TSemCondReason(SemGuard guard) { possibleReason(guard) }

/**
* A reason for an inferred bound. This can either be `CondReason` if the bound
* is due to a specific condition, or `NoReason` if the bound is inferred
* without going through a bounding condition.
*/
abstract class SemReason extends TSemReason {
/** Gets a textual representation of this reason. */
abstract string toString();
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* without going through a bounding condition.
*/
class SemNoReason extends SemReason, TSemNoReason {
override string toString() { result = "NoReason" }
}

/** A reason for an inferred bound pointing to a condition. */
class SemCondReason extends SemReason, TSemCondReason {
/** Gets the condition that is the reason for the bound. */
SemGuard getCond() { this = TSemCondReason(result) }

override string toString() { result = this.getCond().toString() }
}

/**
* Holds if `e + delta` is a valid bound for `v` at `pos`.
* - `upper = true` : `v <= e + delta`
Expand All @@ -551,13 +560,13 @@ module RangeStage<
semSsaUpdateStep(v, e, delta) and
pos.hasReadOfVar(v) and
(upper = true or upper = false) and
reason = TSemNoReason()
reason instanceof SemNoReason
or
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
reason.(SemCondReason).getCond() = guard
)
}

Expand All @@ -570,7 +579,7 @@ module RangeStage<
pos.hasReadOfVar(v) and
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
reason = TSemCondReason(guard)
reason.(SemCondReason).getCond() = guard
)
}

Expand Down Expand Up @@ -700,7 +709,7 @@ module RangeStage<
// upper = true: v <= mid + d1 <= b + d1 + d2 = b + delta
// upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) and
(if r1 instanceof SemNoReason then reason = r2 else reason = r1)
(if r1 instanceof SemNoReason then reason = r2 else reason = r1.combineWith(r2))
)
or
exists(D::Delta d, SemReason r1, SemReason r2 |
Expand All @@ -714,9 +723,9 @@ module RangeStage<
upper = false and delta = D::fromFloat(D::toFloat(d) + 1)
) and
(
reason = r1
reason = r1.combineWith(r2)
or
reason = r2 and not r2 instanceof SemNoReason
reason = r2.combineWith(r1) and not r2 instanceof SemNoReason
)
)
}
Expand Down Expand Up @@ -786,7 +795,7 @@ module RangeStage<
(upper = true or upper = false) and
fromBackEdge0 = false and
origdelta = D::fromFloat(0) and
reason = TSemNoReason()
reason instanceof SemNoReason
|
if semBackEdge(phi, inp, edge)
then
Expand Down Expand Up @@ -1044,13 +1053,13 @@ module RangeStage<
(upper = true or upper = false) and
fromBackEdge = false and
origdelta = delta and
reason = TSemNoReason()
reason instanceof SemNoReason
or
baseBound(e, delta, upper) and
b instanceof SemZeroBound and
fromBackEdge = false and
origdelta = delta and
reason = TSemNoReason()
reason instanceof SemNoReason
or
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
Expand Down Expand Up @@ -1104,9 +1113,9 @@ module RangeStage<
boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
boundedConditionalExpr(cond, b, upper, false, d2, fbe2, od2, r2) and
(
delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1.combineWith(r2)
or
delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2.combineWith(r1)
)
|
upper = true and delta = D::fromFloat(D::toFloat(d1).maximum(D::toFloat(d2)))
Expand All @@ -1132,9 +1141,15 @@ module RangeStage<
delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
b = bLeft and
origdelta = odLeft and
reason = rLeft.combineWith(rRight) and
bRight instanceof SemZeroBound
or
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
b = bRight and
origdelta = odRight and
reason = rRight.combineWith(rLeft) and
bLeft instanceof SemZeroBound
)
or
exists(
Expand All @@ -1150,9 +1165,9 @@ module RangeStage<
(
if D::toFloat(d1).abs() > D::toFloat(d2).abs()
then (
d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1.combineWith(r2)
) else (
d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2.combineWith(r1)
)
)
|
Expand All @@ -1168,11 +1183,14 @@ module RangeStage<
boundedMulOperand(e, upper, true, dLeft, fbeLeft, odLeft, rLeft) and
boundedMulOperand(e, upper, false, dRight, fbeRight, odRight, rRight) and
delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
fromBackEdge = fbeLeft.booleanOr(fbeRight) and
b instanceof SemZeroBound
|
b instanceof SemZeroBound and origdelta = odLeft and reason = rLeft
origdelta = odLeft and
reason = rLeft.combineWith(rRight)
or
b instanceof SemZeroBound and origdelta = odRight and reason = rRight
origdelta = odRight and
reason = rRight.combineWith(rLeft)
)
)
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
/**
* Provides a `Make` parameterized module for constructing a `Reason` type that is used
* when implementing the `LangSig` module.
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic

/** The necessary parameters that must be implemented to instantiate `Make`. */
signature module ParamSig {
class TypeReasonImpl;
}

/**
* The module that constructs a `Reason` type when provided with an implementation
* of `ParamSig`.
*/
module Make<ParamSig Param> {
private import Param

private newtype TSemReason =
TSemNoReason() or
TSemCondReason(SemGuard guard) or
TSemTypeReason(TypeReasonImpl trc)

/**
* A reason for an inferred bound. This can either be `CondReason` if the bound
* is due to a specific condition, or `NoReason` if the bound is inferred
* without going through a bounding condition.
*/
abstract class SemReason extends TSemReason {
/** Gets a textual representation of this reason. */
abstract string toString();

bindingset[this, reason]
abstract SemReason combineWith(SemReason reason);
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* without going through a bounding condition.
*/
class SemNoReason extends SemReason, TSemNoReason {
override string toString() { result = "NoReason" }

override SemReason combineWith(SemReason reason) { result = reason }
}

/** A reason for an inferred bound pointing to a condition. */
class SemCondReason extends SemReason, TSemCondReason {
/** Gets the condition that is the reason for the bound. */
SemGuard getCond() { this = TSemCondReason(result) }

override string toString() { result = this.getCond().toString() }

bindingset[this, reason]
override SemReason combineWith(SemReason reason) {
// Since we end up reporting a `SemReason` for the inferred bound we often pick somewhat
// arbitrarily between two `SemReason`s during the analysis. This isn't an issue for most reasons
// since they're mainly used for constructing alert messages. However, the `SemTypeReason` is
// supposed to be used in query logic to filter out bounds inferred by type-based analysis if
// the query author chooses to do so. So we need to ensure that if _any_ of the bounds that
// contribute to the final bound depends on type information then the `SemReason` we report must
// be a `SemTypeReason`. So when we need to combine this `SemCondReason` with a `SemTypeReason`
// the result should always be a `SemTypeReason`.
if reason instanceof SemTypeReason then result instanceof SemTypeReason else result = this
}
}

/**
* A reason for an inferred bound that indicates that the bound is inferred
* based on type-information.
*/
class SemTypeReason extends SemReason, TSemTypeReason {
TypeReasonImpl impl;

SemTypeReason() { this = TSemTypeReason(impl) }

override string toString() { result = "TypeReason" }

bindingset[this, reason]
override SemReason combineWith(SemReason reason) { result = this and exists(reason) }
}
}

0 comments on commit 3e9d9e7

Please sign in to comment.