Skip to content
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.

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

Java: locations for range analysis #17998

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
*/

private import Semantic
private import SemanticLocation
private import SemanticExprSpecific::SemanticExprConfig as Specific
private import SemanticType

Expand All @@ -15,7 +16,7 @@ private import SemanticType
class SemExpr instanceof Specific::Expr {
final string toString() { result = super.toString() }

final Specific::Location getLocation() { result = super.getLocation() }
SemLocation getLocation() { result = super.getLocation() }

Opcode getOpcode() { result instanceof Opcode::Unknown }

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation

module FloatDelta implements DeltaSig {
class Delta = float;
Expand All @@ -22,7 +23,7 @@ module FloatDelta implements DeltaSig {
Delta fromFloat(float f) { result = f }
}

module FloatOverflow implements OverflowSig<Sem, FloatDelta> {
module FloatOverflow implements OverflowSig<SemLocation, Sem, FloatDelta> {
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
exists(float lb, float ub, float delta |
typeBounds(expr.getSemType(), lb, ub) and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis

module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
module CppLangImplConstant implements LangSig<SemLocation, Sem, FloatDelta> {
/**
* Ignore the bound on this expression.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ private import SemanticType
private import codeql.rangeanalysis.RangeAnalysis
private import ConstantAnalysis as ConstantAnalysis

module Sem implements Semantic {
module Sem implements Semantic<SemLocation> {
class Expr = SemExpr;

class ConstantIntegerExpr = ConstantAnalysis::SemConstantIntegerExpr;
Expand Down Expand Up @@ -104,7 +104,7 @@ module Sem implements Semantic {
}
}

module SignAnalysis implements SignAnalysisSig<Sem> {
module SignAnalysis implements SignAnalysisSig<SemLocation, Sem> {
private import SignAnalysisCommon as SA
import SA::SignAnalysis<FloatDelta>
}
Expand Down Expand Up @@ -165,7 +165,7 @@ module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
}
}

private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<SemLocation, Sem> {
class ModBound = AllBounds::SemBound;

private import codeql.rangeanalysis.ModulusAnalysis as MA
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,13 @@
*/

private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeAnalysisImpl
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
private import codeql.rangeanalysis.RangeAnalysis

module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
module CppLangImplRelative implements LangSig<SemLocation, Sem, FloatDelta> {
/**
* Ignore the bound on this expression.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,12 @@ private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl
private import SignAnalysisSpecific as Specific
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import ConstantAnalysis
private import Sign

module SignAnalysis<DeltaSig D> {
private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<SemLocation, Sem, D>

/**
* An SSA definition for which the analysis can compute the sign.
Expand Down
10 changes: 5 additions & 5 deletions java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ private import semmle.code.java.Maps
import Bound
private import codeql.rangeanalysis.RangeAnalysis

module Sem implements Semantic {
module Sem implements Semantic<Location> {
private import java as J
private import SSA as SSA
private import RangeUtils as RU
Expand Down Expand Up @@ -264,7 +264,7 @@ module Sem implements Semantic {
predicate conversionCannotOverflow = safeCast/2;
}

module SignInp implements SignAnalysisSig<Sem> {
module SignInp implements SignAnalysisSig<Location, Sem> {
private import SignAnalysis
private import internal.rangeanalysis.Sign

Expand All @@ -281,7 +281,7 @@ module SignInp implements SignAnalysisSig<Sem> {
predicate semMayBeNegative(Sem::Expr e) { exprSign(e) = TNeg() }
}

module Modulus implements ModulusAnalysisSig<Sem> {
module Modulus implements ModulusAnalysisSig<Location, Sem> {
class ModBound = Bound;

private import codeql.rangeanalysis.ModulusAnalysis as Mod
Expand All @@ -307,7 +307,7 @@ module IntDelta implements DeltaSig {
Delta fromFloat(float f) { result = f }
}

module JavaLangImpl implements LangSig<Sem, IntDelta> {
module JavaLangImpl implements LangSig<Location, Sem, IntDelta> {
/**
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
*/
Expand Down Expand Up @@ -379,7 +379,7 @@ module Bounds implements BoundSig<Location, Sem, IntDelta> {
}
}

module Overflow implements OverflowSig<Sem, IntDelta> {
module Overflow implements OverflowSig<Location, Sem, IntDelta> {
predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr) {
positively = [true, false] and exists(expr)
}
Expand Down
2 changes: 1 addition & 1 deletion java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ private import semmle.code.java.Constants
private import semmle.code.java.dataflow.RangeAnalysis
private import codeql.rangeanalysis.internal.RangeUtils

private module U = MakeUtils<Sem, IntDelta>;
private module U = MakeUtils<Location, Sem, IntDelta>;

private predicate backEdge = U::backEdge/3;

Expand Down
4 changes: 2 additions & 2 deletions shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ private import codeql.util.Location
private import RangeAnalysis

module ModulusAnalysis<
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds>
LocationSig Location, Semantic<Location> Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds>
{
private import internal.RangeUtils::MakeUtils<Sem, D>
private import internal.RangeUtils::MakeUtils<Location, Sem, D>

bindingset[pos, v]
pragma[inline_late]
Expand Down
23 changes: 13 additions & 10 deletions shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,13 @@

private import codeql.util.Location

signature module Semantic {
signature module Semantic<LocationSig Location> {
class Expr {
string toString();

BasicBlock getBasicBlock();

Location getLocation();
}

class ConstantIntegerExpr extends Expr {
Expand Down Expand Up @@ -294,7 +296,7 @@ signature module Semantic {
predicate conversionCannotOverflow(Type fromType, Type toType);
}

signature module SignAnalysisSig<Semantic Sem> {
signature module SignAnalysisSig<LocationSig Location, Semantic<Location> Sem> {
/** Holds if `e` can be positive and cannot be negative. */
predicate semPositive(Sem::Expr e);

Expand All @@ -320,7 +322,7 @@ signature module SignAnalysisSig<Semantic Sem> {
predicate semMayBeNegative(Sem::Expr e);
}

signature module ModulusAnalysisSig<Semantic Sem> {
signature module ModulusAnalysisSig<LocationSig Location, Semantic<Location> Sem> {
class ModBound;

predicate exprModulus(Sem::Expr e, ModBound b, int val, int mod);
Expand All @@ -346,7 +348,7 @@ signature module DeltaSig {
Delta fromFloat(float f);
}

signature module LangSig<Semantic Sem, DeltaSig D> {
signature module LangSig<LocationSig Location, Semantic<Location> Sem, DeltaSig D> {
/**
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
*/
Expand All @@ -372,7 +374,7 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
default predicate includeRelativeBounds() { any() }
}

signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
signature module BoundSig<LocationSig Location, Semantic<Location> Sem, DeltaSig D> {
/**
* A bound that the range analysis can infer for a variable. This includes
* constant bounds represented by the abstract value zero, SSA bounds for when
Expand Down Expand Up @@ -409,22 +411,23 @@ signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
}
}

signature module OverflowSig<Semantic Sem, DeltaSig D> {
signature module OverflowSig<LocationSig Location, Semantic<Location> Sem, DeltaSig D> {
predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr);
}

module RangeStage<
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
OverflowSig<Sem, D> OverflowParam, LangSig<Sem, D> LangParam, SignAnalysisSig<Sem> SignAnalysis,
ModulusAnalysisSig<Sem> ModulusAnalysisParam>
LocationSig Location, Semantic<Location> Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
OverflowSig<Location, Sem, D> OverflowParam, LangSig<Location, Sem, D> LangParam,
SignAnalysisSig<Location, Sem> SignAnalysis,
ModulusAnalysisSig<Location, Sem> ModulusAnalysisParam>
{
private import Bounds
private import LangParam
private import D
private import OverflowParam
private import SignAnalysis
private import ModulusAnalysisParam
private import internal.RangeUtils::MakeUtils<Sem, D>
private import internal.RangeUtils::MakeUtils<Location, Sem, D>

/**
* An expression that does conversion, boxing, or unboxing
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
private import codeql.rangeanalysis.RangeAnalysis
private import codeql.util.Location

module MakeUtils<Semantic Lang, DeltaSig D> {
module MakeUtils<LocationSig Location, Semantic<Location> Lang, DeltaSig D> {
private import Lang

/**
Expand Down