From cd5509a0f98db63d9b3ad10be3960b35ec1a6f6a Mon Sep 17 00:00:00 2001 From: Rasmus Lerchedahl Petersen Date: Fri, 15 Nov 2024 11:28:38 +0100 Subject: [PATCH] Java: locations for range analysis --- .../code/java/dataflow/RangeAnalysis.qll | 10 ++++---- .../semmle/code/java/dataflow/RangeUtils.qll | 2 +- .../codeql/rangeanalysis/ModulusAnalysis.qll | 4 ++-- .../codeql/rangeanalysis/RangeAnalysis.qll | 23 +++++++++++-------- .../rangeanalysis/internal/RangeUtils.qll | 3 ++- 5 files changed, 23 insertions(+), 19 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index e0055d53f08..774b165e949 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -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 { 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 { +module SignInp implements SignAnalysisSig { private import SignAnalysis private import internal.rangeanalysis.Sign @@ -281,7 +281,7 @@ module SignInp implements SignAnalysisSig { predicate semMayBeNegative(Sem::Expr e) { exprSign(e) = TNeg() } } -module Modulus implements ModulusAnalysisSig { +module Modulus implements ModulusAnalysisSig { 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 { +module JavaLangImpl implements LangSig { /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ @@ -379,7 +379,7 @@ module Bounds implements BoundSig { } } -module Overflow implements OverflowSig { +module Overflow implements OverflowSig { predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr) { positively = [true, false] and exists(expr) } diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll index be7f73fe766..e96d591ced5 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll @@ -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; +private module U = MakeUtils; private predicate backEdge = U::backEdge/3; diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll index f8b4a94079a..88d816b8644 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll @@ -14,9 +14,9 @@ private import codeql.util.Location private import RangeAnalysis module ModulusAnalysis< - LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds> + LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds> { - private import internal.RangeUtils::MakeUtils + private import internal.RangeUtils::MakeUtils bindingset[pos, v] pragma[inline_late] diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index e178c44cafb..d0fc084e6c5 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -65,11 +65,13 @@ private import codeql.util.Location -signature module Semantic { +signature module Semantic { 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 { +signature module SignAnalysisSig Sem> { /** Holds if `e` can be positive and cannot be negative. */ predicate semPositive(Sem::Expr e); @@ -320,7 +322,7 @@ signature module SignAnalysisSig { predicate semMayBeNegative(Sem::Expr e); } -signature module ModulusAnalysisSig { +signature module ModulusAnalysisSig 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 { +signature module LangSig Sem, DeltaSig D> { /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ @@ -372,7 +374,7 @@ signature module LangSig { default predicate includeRelativeBounds() { any() } } -signature module BoundSig { +signature module BoundSig 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 { } } -signature module OverflowSig { +signature module OverflowSig Sem, DeltaSig D> { predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr); } module RangeStage< - LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds, - OverflowSig OverflowParam, LangSig LangParam, SignAnalysisSig SignAnalysis, - ModulusAnalysisSig ModulusAnalysisParam> + LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds, + OverflowSig OverflowParam, LangSig LangParam, + SignAnalysisSig SignAnalysis, + ModulusAnalysisSig 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 + private import internal.RangeUtils::MakeUtils /** * An expression that does conversion, boxing, or unboxing diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll index dc1014a886e..ee6e3a4c958 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll @@ -1,6 +1,7 @@ private import codeql.rangeanalysis.RangeAnalysis +private import codeql.util.Location -module MakeUtils { +module MakeUtils Lang, DeltaSig D> { private import Lang /**