Skip to content
Open
4 changes: 0 additions & 4 deletions config/identical-files.json
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,6 @@
"java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll",
"csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll"
],
"Bound Java/C#": [
"java/ql/lib/semmle/code/java/dataflow/Bound.qll",
"csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll"
],
"ModulusAnalysis Java/C#": [
"java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll",
"csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll"
Expand Down
1 change: 1 addition & 0 deletions csharp/ql/lib/qlpack.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ dependencies:
codeql/controlflow: ${workspace}
codeql/dataflow: ${workspace}
codeql/mad: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/ssa: ${workspace}
codeql/threat-models: ${workspace}
codeql/tutorial: ${workspace}
Expand Down
66 changes: 5 additions & 61 deletions csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll
Original file line number Diff line number Diff line change
Expand Up @@ -4,67 +4,11 @@
overlay[local?]
module;

private import csharp as CS
private import internal.rangeanalysis.BoundSpecific
private import internal.rangeanalysis.BoundSpecific as BoundSpecific
private import codeql.rangeanalysis.Bound as SharedBound

private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) {
interestingExprBound(e) and
not exists(SsaVariable v | e = v.getAUse())
}
private module BoundImpl = SharedBound::Bound<CS::Location, BoundSpecific::BoundDefs>;

/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
/** Gets a textual representation of this bound. */
abstract string toString();

/** Gets an expression that equals this bound plus `delta`. */
abstract Expr getExpr(int delta);

/** Gets an expression that equals this bound. */
Expr getExpr() { result = this.getExpr(0) }

/** Gets the location of this bound. */
abstract Location getLocation();
}

/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }

override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }

override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
}

/**
* A bound corresponding to the value of an SSA variable.
*/
class SsaBound extends Bound, TBoundSsa {
/** Gets the SSA variable that equals this bound. */
SsaVariable getSsa() { this = TBoundSsa(result) }

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

override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }

override Location getLocation() { result = this.getSsa().getLocation() }
}

/**
* A bound that corresponds to the value of a specific expression that might be
* interesting, but isn't otherwise represented by the value of an SSA variable.
*/
class ExprBound extends Bound, TBoundExpr {
override string toString() { result = this.getExpr().toString() }

override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }

override Location getLocation() { result = this.getExpr().getLocation() }
}
import BoundImpl
Original file line number Diff line number Diff line change
@@ -1,22 +1,30 @@
/**
* Provides C#-specific definitions for bounds.
*/
overlay[local?]
module;

private import csharp as CS
private import semmle.code.csharp.dataflow.SSA::Ssa as Ssa
private import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils as CU
private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
private import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils as SU
private import codeql.rangeanalysis.Bound as SharedBound

class SsaVariable = SU::SsaVariable;
/** Provides C#-specific definitions for bounds. */
module BoundDefs implements SharedBound::BoundDefinitions<CS::Location> {
class Type = CS::Type;

class Expr = CS::ControlFlowNodes::ExprNode;
class SsaVariable = SU::SsaVariable;

class Location = CS::Location;
class SsaSourceVariable = Ssa::SourceVariable;

class IntegralType = CS::IntegralType;
class Expr = CS::ControlFlowNodes::ExprNode;

class ConstantIntegerExpr = CU::ConstantIntegerExpr;
class IntegralType = CS::IntegralType;

/** Holds if `e` is a bound expression and it is not an SSA variable read. */
predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.getExpr()) }
class ConstantIntegerExpr = CU::ConstantIntegerExpr;

/** Holds if `e` is a bound expression and it is not an SSA variable read. */
predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.getExpr()) }
}
67 changes: 5 additions & 62 deletions java/ql/lib/semmle/code/java/dataflow/Bound.qll
Original file line number Diff line number Diff line change
Expand Up @@ -4,67 +4,10 @@
overlay[local?]
module;

private import internal.rangeanalysis.BoundSpecific
private import java as J
private import internal.rangeanalysis.BoundSpecific as BoundSpecific
private import codeql.rangeanalysis.Bound as SharedBound

private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) {
interestingExprBound(e) and
not exists(SsaVariable v | e = v.getAUse())
}
private module BoundImpl = SharedBound::Bound<J::Location, BoundSpecific::BoundDefs>;

/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
/** Gets a textual representation of this bound. */
abstract string toString();

/** Gets an expression that equals this bound plus `delta`. */
abstract Expr getExpr(int delta);

/** Gets an expression that equals this bound. */
Expr getExpr() { result = this.getExpr(0) }

/** Gets the location of this bound. */
abstract Location getLocation();
}

/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }

override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }

override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
}

/**
* A bound corresponding to the value of an SSA variable.
*/
class SsaBound extends Bound, TBoundSsa {
/** Gets the SSA variable that equals this bound. */
SsaVariable getSsa() { this = TBoundSsa(result) }

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

override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }

override Location getLocation() { result = this.getSsa().getLocation() }
}

/**
* A bound that corresponds to the value of a specific expression that might be
* interesting, but isn't otherwise represented by the value of an SSA variable.
*/
class ExprBound extends Bound, TBoundExpr {
override string toString() { result = this.getExpr().toString() }

override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }

override Location getLocation() { result = this.getExpr().getLocation() }
}
import BoundImpl
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,26 @@ module;
private import java as J
private import semmle.code.java.dataflow.SSA as Ssa
private import semmle.code.java.dataflow.RangeUtils as RU
private import codeql.rangeanalysis.Bound as SharedBound

class SsaVariable extends Ssa::SsaDefinition {
/** Gets a use of this variable. */
Expr getAUse() { result = super.getARead() }
}
module BoundDefs implements SharedBound::BoundDefinitions<J::Location> {
class SsaVariable extends Ssa::SsaDefinition {
/** Gets a use of this variable. */
Expr getAUse() { result = super.getARead() }
}

class SsaSourceVariable = Ssa::SourceVariable;

class Expr = J::Expr;
class Type = J::Type;

class Location = J::Location;
class Expr = J::Expr;

class IntegralType = J::IntegralType;
class IntegralType = J::IntegralType;

class ConstantIntegerExpr = RU::ConstantIntegerExpr;
class ConstantIntegerExpr = RU::ConstantIntegerExpr;

/** Holds if `e` is a bound expression and it is not an SSA variable read. */
predicate interestingExprBound(Expr e) {
e.(J::FieldRead).getField() instanceof J::ArrayLengthField
/** Holds if `e` is a bound expression and it is not an SSA variable read. */
predicate interestingExprBound(Expr e) {
e.(J::FieldRead).getField() instanceof J::ArrayLengthField
}
}
3 changes: 3 additions & 0 deletions shared/rangeanalysis/change-notes/released/1.0.52.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
## 1.0.52

No user-facing changes.
111 changes: 111 additions & 0 deletions shared/rangeanalysis/codeql/rangeanalysis/Bound.qll
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
/**
* Provides classes for representing abstract bounds for use in, for example, range analysis.
*/
overlay[local?]
module;

private import codeql.util.Location

signature module BoundDefinitions<LocationSig Location> {
class Type;

class IntegralType extends Type;

class ConstantIntegerExpr extends Expr {
int getIntValue();
}

class SsaSourceVariable {
Type getType();
}

class SsaVariable {
SsaSourceVariable getSourceVariable();

string toString();

Location getLocation();

Expr getAUse();
}

class Expr {
string toString();

Location getLocation();
}

predicate interestingExprBound(Expr e);
}

/**
* Provides classes for representing abstract bounds for use in, for example, range analysis.
* This is a generic implementation of bounds that relies on language specific modules to provide language-specific definitions of expressions, SSA variables, etc.
*/
overlay[local?]
module Bound<LocationSig Location, BoundDefinitions<Location> Defs> {
private import Defs

private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) {
interestingExprBound(e) and
not exists(SsaVariable v | e = v.getAUse())
}

/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
/** Gets a textual representation of this bound. */
abstract string toString();

/** Gets an expression that equals this bound plus `delta`. */
abstract Expr getExpr(int delta);

/** Gets an expression that equals this bound. */
Expr getExpr() { result = this.getExpr(0) }

/** Gets the location of this bound. */
abstract Location getLocation();
}

/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }

override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }

override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
}

/**
* A bound corresponding to the value of an SSA variable.
*/
class SsaBound extends Bound, TBoundSsa {
/** Gets the SSA variable that equals this bound. */
SsaVariable getSsa() { this = TBoundSsa(result) }

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

override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }

override Location getLocation() { result = this.getSsa().getLocation() }
}

/**
* A bound that corresponds to the value of a specific expression that might be
* interesting, but isn't otherwise represented by the value of an SSA variable.
*/
class ExprBound extends Bound, TBoundExpr {
override string toString() { result = this.getExpr().toString() }

override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }

override Location getLocation() { result = this.getExpr().getLocation() }
}
}
Loading