mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Java: locations for range analysis
This commit is contained in:
@@ -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
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
@@ -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`).
|
||||
*/
|
||||
@@ -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)
|
||||
}
|
||||
|
||||
@@ -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;
|
||||
|
||||
|
||||
@@ -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]
|
||||
|
||||
@@ -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 {
|
||||
@@ -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);
|
||||
|
||||
@@ -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);
|
||||
@@ -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`).
|
||||
*/
|
||||
@@ -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
|
||||
@@ -409,14 +411,15 @@ 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
|
||||
@@ -424,7 +427,7 @@ module RangeStage<
|
||||
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
|
||||
|
||||
@@ -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
|
||||
|
||||
/**
|
||||
|
||||
Reference in New Issue
Block a user