diff --git a/java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll b/java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll index 859a3eedef8..08a29a7dcd8 100644 --- a/java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll +++ b/java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll @@ -337,12 +337,14 @@ module SemanticExprConfig { type = getSemanticType(update.getSourceVariable().getType()) and exists(J::Expr expr | expr = update.getDefiningExpr() | ( - expr instanceof J::Assignment or + expr instanceof J::AssignOp or expr instanceof J::PreIncExpr or expr instanceof J::PreDecExpr ) and sourceExpr = getResultExpr(expr) or + sourceExpr = getResultExpr(expr.(J::AssignExpr).getSource()) + or sourceExpr = getResultExpr(expr.(J::LocalVariableDeclExpr).getInit()) or (expr instanceof J::PostIncExpr or expr instanceof J::PostDecExpr) and diff --git a/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysis.qll b/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysis.qll index ee633ce9ae2..75250a283f3 100644 --- a/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysis.qll +++ b/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysis.qll @@ -6,6 +6,7 @@ private import ModulusAnalysisSpecific::Private private import semmle.code.java.semantic.SemanticBound +private import semmle.code.java.semantic.SemanticCFG private import semmle.code.java.semantic.SemanticExpr private import semmle.code.java.semantic.SemanticGuard private import semmle.code.java.semantic.SemanticSSA @@ -30,9 +31,9 @@ private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, Sem * `ConstantIntegerExpr`s. */ private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) { - exists(AddExpr a | a = add | - larg = a.getLhs() and - rarg = a.getRhs() + exists(SemAddExpr a | a = add | + larg = a.getLeftOperand() and + rarg = a.getRightOperand() ) and not larg instanceof SemConstantIntegerExpr and not rarg instanceof SemConstantIntegerExpr @@ -43,9 +44,9 @@ private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) { * a `ConstantIntegerExpr`. */ private predicate nonConstSubtraction(SemExpr sub, SemExpr larg, SemExpr rarg) { - exists(SubExpr s | s = sub | - larg = s.getLhs() and - rarg = s.getRhs() + exists(SemSubExpr s | s = sub | + larg = s.getLeftOperand() and + rarg = s.getRightOperand() ) and not rarg instanceof SemConstantIntegerExpr } @@ -62,7 +63,7 @@ private SemExpr modExpr(SemExpr arg, int mod) { exists(SemConstantIntegerExpr c | mod = 2.pow([1 .. 30]) and c.getIntValue() = mod - 1 and - result.(BitwiseAndExpr).hasOperands(arg, c) + result.(SemBitAndExpr).hasOperands(arg, c) ) } @@ -107,11 +108,11 @@ private predicate andmaskFactor(int mask, int factor) { /** Holds if `e` is evenly divisible by `factor`. */ private predicate evenlyDivisibleExpr(SemExpr e, int factor) { exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() | - e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2 + e.(SemMulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2 or - e.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0 + e.(SemShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0 or - e.(BitwiseAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f)) + e.(SemBitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f)) ) } @@ -223,49 +224,54 @@ private predicate ssaModulus(SemSsaVariable v, SemSsaReadPosition pos, SemBound */ cached predicate semExprModulus(SemExpr e, SemBound b, int val, int mod) { - e = b.getExpr(val) and mod = 0 - or - evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof SemZeroBound - or - exists(SemSsaVariable v, SemSsaReadPositionBlock bb | - ssaModulus(v, bb, b, val, mod) and - e = v.getAUse() and - bb.getAnExpr() = e - ) - or - exists(SemExpr mid, int val0, int delta | - semExprModulus(mid, b, val0, mod) and - semValueFlowStep(e, mid, delta) and - val = remainder(val0 + delta, mod) - ) - or - exists(SemConditionalExpr cond, int v1, int v2, int m1, int m2 | - cond = e and - condExprBranchModulus(cond, true, b, v1, m1) and - condExprBranchModulus(cond, false, b, v2, m2) and - mod = m1.gcd(m2).gcd(v1 - v2) and - mod != 1 and - val = remainder(v1, mod) - ) - or - exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 | - addModulus(e, true, b1, v1, m1) and - addModulus(e, false, b2, v2, m2) and - mod = m1.gcd(m2) and - mod != 1 and - val = remainder(v1 + v2, mod) - | - b = b1 and b2 instanceof SemZeroBound + not ignoreExprModulus(e) and + ( + e = b.getExpr(val) and mod = 0 or - b = b2 and b1 instanceof SemZeroBound - ) - or - exists(int v1, int v2, int m1, int m2 | - subModulus(e, true, b, v1, m1) and - subModulus(e, false, any(SemZeroBound zb), v2, m2) and - mod = m1.gcd(m2) and - mod != 1 and - val = remainder(v1 - v2, mod) + evenlyDivisibleExpr(e, mod) and + val = 0 and + b instanceof SemZeroBound + or + exists(SemSsaVariable v, SemSsaReadPositionBlock bb | + ssaModulus(v, bb, b, val, mod) and + e = v.getAUse() and + bb.getAnExpr() = e + ) + or + exists(SemExpr mid, int val0, int delta | + semExprModulus(mid, b, val0, mod) and + semValueFlowStep(e, mid, delta) and + val = remainder(val0 + delta, mod) + ) + or + exists(SemConditionalExpr cond, int v1, int v2, int m1, int m2 | + cond = e and + condExprBranchModulus(cond, true, b, v1, m1) and + condExprBranchModulus(cond, false, b, v2, m2) and + mod = m1.gcd(m2).gcd(v1 - v2) and + mod != 1 and + val = remainder(v1, mod) + ) + or + exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 | + addModulus(e, true, b1, v1, m1) and + addModulus(e, false, b2, v2, m2) and + mod = m1.gcd(m2) and + mod != 1 and + val = remainder(v1 + v2, mod) + | + b = b1 and b2 instanceof SemZeroBound + or + b = b2 and b1 instanceof SemZeroBound + ) + or + exists(int v1, int v2, int m1, int m2 | + subModulus(e, true, b, v1, m1) and + subModulus(e, false, any(SemZeroBound zb), v2, m2) and + mod = m1.gcd(m2) and + mod != 1 and + val = remainder(v1 - v2, mod) + ) ) } @@ -290,3 +296,25 @@ private predicate subModulus(SemExpr sub, boolean isLeft, SemBound b, int val, i semExprModulus(rarg, b, val, mod) and isLeft = false ) } + +private predicate id(SemBasicBlock x, SemBasicBlock y) { x = y } + +private predicate idOf(SemBasicBlock x, int y) = equivalenceRelation(id/2)(x, y) + +private int getId(SemBasicBlock bb) { idOf(bb, result) } + +/** + * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` + * in an arbitrary 1-based numbering of the input edges to `phi`. + */ +private predicate rankedPhiInput( + SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r +) { + edge.phiInput(phi, inp) and + edge = + rank[r](SemSsaReadPositionPhiInputEdge e | + e.phiInput(phi, _) + | + e order by getId(e.getOrigBlock()) + ) +} diff --git a/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysisSpecific.qll b/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysisSpecific.qll index c2a157c07a4..2b03e376349 100644 --- a/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysisSpecific.qll +++ b/java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysisSpecific.qll @@ -1,107 +1,11 @@ module Private { private import java as J - private import semmle.code.java.controlflow.BasicBlocks as BB - private import semmle.code.java.semantic.SemanticCFG private import semmle.code.java.semantic.SemanticExpr - private import semmle.code.java.semantic.SemanticSSA - - /** An addition or an assign-add expression. */ - class AddExpr extends SemExpr { - AddExpr() { this instanceof SemAddExpr or this instanceof SemAssignAddExpr } - - /** Gets the LHS operand of this add expression. */ - SemExpr getLhs() { - result = this.(SemAddExpr).getLeftOperand() - or - result = this.(SemAssignAddExpr).getDest() - } - - /** Gets the RHS operand of this add expression. */ - SemExpr getRhs() { - result = this.(SemAddExpr).getRightOperand() - or - result = this.(SemAssignAddExpr).getRhs() - } - } - - /** A subtraction or an assign-sub expression. */ - class SubExpr extends SemExpr { - SubExpr() { this instanceof SemSubExpr or this instanceof SemAssignSubExpr } - - /** Gets the LHS operand of this subtraction expression. */ - SemExpr getLhs() { - result = this.(SemSubExpr).getLeftOperand() - or - result = this.(SemAssignSubExpr).getDest() - } - - /** Gets the RHS operand of this subtraction expression. */ - SemExpr getRhs() { - result = this.(SemSubExpr).getRightOperand() - or - result = this.(SemAssignSubExpr).getRhs() - } - } - - /** A multiplication or an assign-mul expression. */ - class MulExpr extends SemExpr { - MulExpr() { this instanceof SemMulExpr or this instanceof SemAssignMulExpr } - - /** Gets an operand of this multiplication. */ - SemExpr getAnOperand() { - result = this.(SemMulExpr).getAnOperand() or - result = this.(SemAssignMulExpr).getSource() - } - } - - /** A left shift or an assign-lshift expression. */ - class LShiftExpr extends SemExpr { - LShiftExpr() { this instanceof SemLShiftExpr or this instanceof SemAssignLShiftExpr } - - /** Gets the RHS operand of this shift. */ - SemExpr getRhs() { - result = this.(SemLShiftExpr).getRightOperand() or - result = this.(SemAssignLShiftExpr).getRhs() - } - } - - /** A bitwise and or an assign-and expression. */ - class BitwiseAndExpr extends SemExpr { - BitwiseAndExpr() { this instanceof SemAndBitwiseExpr or this instanceof SemAssignAndExpr } - - /** Gets an operand of this bitwise and operation. */ - SemExpr getAnOperand() { - result = this.(SemAndBitwiseExpr).getAnOperand() or - result = this.(SemAssignAndExpr).getSource() - } - - /** Holds if this expression has operands `e1` and `e2`. */ - predicate hasOperands(SemExpr e1, SemExpr e2) { - this.getAnOperand() = e1 and - this.getAnOperand() = e2 and - e1 != e2 - } - } - - private predicate id(BB::BasicBlock x, BB::BasicBlock y) { x = y } - - private predicate idOf(BB::BasicBlock x, int y) = equivalenceRelation(id/2)(x, y) - - private int getId(BB::BasicBlock bb) { idOf(bb, result) } + private import semmle.code.java.semantic.SemanticExprSpecific /** - * Holds if `inp` is an input to `phi` along `edge` and this input has index `r` - * in an arbitrary 1-based numbering of the input edges to `phi`. + * Workaround to preserve the original Java results by ignoring the modulus of + * certain expressions. */ - predicate rankedPhiInput( - SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r - ) { - edge.phiInput(phi, inp) and - edge = - rank[r](SemSsaReadPositionPhiInputEdge e | - e.phiInput(phi, _) - | - e order by getId(getJavaBasicBlock(e.getOrigBlock())) - ) - } + predicate ignoreExprModulus(SemExpr e) { getJavaExpr(e) instanceof J::LocalVariableDeclExpr } } diff --git a/java/ql/test/library-tests/dataflow/modulus-analysis/diff.ql b/java/ql/test/library-tests/dataflow/modulus-analysis/diff.ql index 7622cab009f..81c5d869b3d 100644 --- a/java/ql/test/library-tests/dataflow/modulus-analysis/diff.ql +++ b/java/ql/test/library-tests/dataflow/modulus-analysis/diff.ql @@ -2,16 +2,30 @@ import java import semmle.code.java.semantic.analysis.ModulusAnalysis import semmle.code.java.semantic.SemanticBound import semmle.code.java.semantic.SemanticExpr +import semmle.code.java.semantic.SemanticExprSpecific +import semmle.code.java.semantic.SemanticSSA import semmle.code.java.dataflow.ModulusAnalysis import semmle.code.java.dataflow.Bound +import semmle.code.java.dataflow.SSA +import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon +import semmle.code.java.dataflow.RangeUtils as RU -from Expr e, Bound b, int delta, int mod, string message -where - semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and - not exprModulus(e, b, delta, mod) and - message = "semantic only" - or - not semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and - exprModulus(e, b, delta, mod) and - message = "AST only" -select e, b.toString(), delta, mod +predicate interestingLocation(Location loc) { + // loc.getFile().getBaseName() = "Utf8Test.java" and + // loc.getStartLine() in [164 .. 164] and + any() +} + +query predicate diff_exprModulus(Expr e, string c, Bound b, int delta, int mod, string message) { + interestingLocation(e.getLocation()) and + c = concat(e.getAQlClass(), ", ") and + ( + semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and + not exprModulus(e, b, delta, mod) and + message = "semantic only" + or + not semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and + exprModulus(e, getJavaBound(b), delta, mod) and + message = "AST only" + ) +}