mirror of
https://github.com/github/codeql.git
synced 2026-02-02 16:23:02 +01:00
New SemanticExpr implementation
Cleans up SignAnalysis to reduce need for language-specific enhancements
This commit is contained in:
Dave Bartolomeo
@@ -374,3 +374,11 @@ predicate strictlyNegative(Expr e) {
|
||||
not exprSign(e) = TPos() and
|
||||
not exprSign(e) = TZero()
|
||||
}
|
||||
|
||||
/**
|
||||
* Expose some predicates for testing purposes without making them implicitly public to any module
|
||||
* that imports this file.
|
||||
*/
|
||||
module SignAnalysisCommonTest {
|
||||
predicate testSsaDefSign = ssaDefSign/1;
|
||||
}
|
||||
|
||||
@@ -4,6 +4,7 @@
|
||||
|
||||
private import java
|
||||
private import SemanticExpr
|
||||
private import SemanticExprSpecific
|
||||
|
||||
private newtype TSemBasicBlock = MkSemBasicBlock(BasicBlock block)
|
||||
|
||||
@@ -14,6 +15,8 @@ class SemBasicBlock extends TSemBasicBlock {
|
||||
|
||||
final string toString() { result = block.toString() }
|
||||
|
||||
final Location getLocation() { result = block.getLocation() }
|
||||
|
||||
final predicate bbDominates(SemBasicBlock otherBlock) {
|
||||
block.bbDominates(getJavaBasicBlock(otherBlock))
|
||||
}
|
||||
|
||||
@@ -4,39 +4,226 @@
|
||||
|
||||
private import java
|
||||
private import SemanticCFG
|
||||
private import SemanticSSA
|
||||
private import SemanticType
|
||||
private import SemanticExprSpecific::SemanticExprConfig as Specific
|
||||
|
||||
private newtype TExpr = MkExpr(Expr expr) { any() }
|
||||
private newtype TOpcode =
|
||||
TCopyValue() or
|
||||
TLoad() or
|
||||
TStore() or
|
||||
TAdd() or
|
||||
TSub() or
|
||||
TMul() or
|
||||
TDiv() or
|
||||
TRem() or
|
||||
TNegate() or
|
||||
TShiftLeft() or
|
||||
TShiftRight() or
|
||||
TShiftRightUnsigned() or // TODO: Based on type
|
||||
TBitAnd() or
|
||||
TBitOr() or
|
||||
TBitXor() or
|
||||
TBitComplement() or
|
||||
TLogicalNot() or
|
||||
TCompareEQ() or
|
||||
TCompareNE() or
|
||||
TCompareLT() or
|
||||
TCompareGT() or
|
||||
TCompareLE() or
|
||||
TCompareGE() or
|
||||
TPointerAdd() or
|
||||
TPointerSub() or
|
||||
TPointerDiff() or
|
||||
TConvert() or
|
||||
TConstant() or
|
||||
TStringConstant() or
|
||||
TAddOne() or // TODO: Combine with `TAdd`
|
||||
TSubOne() or // TODO: Combine with `TSub`
|
||||
TPostInc() or // TODO: Reconnect result to merge with `TPreInc`
|
||||
TPostDec() or // TODO: Reconnect result to merge with `TPreDec`
|
||||
TConditional() or // TODO: Represent as flow
|
||||
TCall() or
|
||||
TUnknown()
|
||||
|
||||
class SemExpr extends MkExpr {
|
||||
Expr expr;
|
||||
|
||||
SemExpr() { this = MkExpr(expr) }
|
||||
|
||||
final string toString() { result = expr.toString() }
|
||||
|
||||
final Location getLocation() { result = expr.getLocation() }
|
||||
|
||||
final SemType getSemType() { result = getSemanticType(expr.getType()) }
|
||||
|
||||
final SemBasicBlock getBasicBlock() { result = getSemanticBasicBlock(expr.getBasicBlock()) }
|
||||
class Opcode extends TOpcode {
|
||||
string toString() { result = "???" }
|
||||
}
|
||||
|
||||
class SemLiteralExpr extends SemExpr {
|
||||
override Literal expr;
|
||||
module Opcode {
|
||||
class CopyValue extends Opcode, TCopyValue {
|
||||
override string toString() { result = "CopyValue" }
|
||||
}
|
||||
|
||||
class Load extends Opcode, TLoad {
|
||||
override string toString() { result = "Load" }
|
||||
}
|
||||
|
||||
class Store extends Opcode, TStore {
|
||||
override string toString() { result = "Store" }
|
||||
}
|
||||
|
||||
class Add extends Opcode, TAdd {
|
||||
override string toString() { result = "Add" }
|
||||
}
|
||||
|
||||
class Sub extends Opcode, TSub {
|
||||
override string toString() { result = "Sub" }
|
||||
}
|
||||
|
||||
class Mul extends Opcode, TMul {
|
||||
override string toString() { result = "Mul" }
|
||||
}
|
||||
|
||||
class Div extends Opcode, TDiv {
|
||||
override string toString() { result = "Div" }
|
||||
}
|
||||
|
||||
class Rem extends Opcode, TRem {
|
||||
override string toString() { result = "Rem" }
|
||||
}
|
||||
|
||||
class Negate extends Opcode, TNegate {
|
||||
override string toString() { result = "Negate" }
|
||||
}
|
||||
|
||||
class ShiftLeft extends Opcode, TShiftLeft {
|
||||
override string toString() { result = "ShiftLeft" }
|
||||
}
|
||||
|
||||
class ShiftRight extends Opcode, TShiftRight {
|
||||
override string toString() { result = "ShiftRight" }
|
||||
}
|
||||
|
||||
class ShiftRightUnsigned extends Opcode, TShiftRightUnsigned {
|
||||
override string toString() { result = "ShiftRightUnsigned" }
|
||||
}
|
||||
|
||||
class BitAnd extends Opcode, TBitAnd {
|
||||
override string toString() { result = "BitAnd" }
|
||||
}
|
||||
|
||||
class BitOr extends Opcode, TBitOr {
|
||||
override string toString() { result = "BitOr" }
|
||||
}
|
||||
|
||||
class BitXor extends Opcode, TBitXor {
|
||||
override string toString() { result = "BitXor" }
|
||||
}
|
||||
|
||||
class BitComplement extends Opcode, TBitComplement {
|
||||
override string toString() { result = "BitComplement" }
|
||||
}
|
||||
|
||||
class LogicalNot extends Opcode, TLogicalNot {
|
||||
override string toString() { result = "LogicalNot" }
|
||||
}
|
||||
|
||||
class CompareEQ extends Opcode, TCompareEQ {
|
||||
override string toString() { result = "CompareEQ" }
|
||||
}
|
||||
|
||||
class CompareNE extends Opcode, TCompareNE {
|
||||
override string toString() { result = "CompareNE" }
|
||||
}
|
||||
|
||||
class CompareLT extends Opcode, TCompareLT {
|
||||
override string toString() { result = "CompareLT" }
|
||||
}
|
||||
|
||||
class CompareLE extends Opcode, TCompareLE {
|
||||
override string toString() { result = "CompareLE" }
|
||||
}
|
||||
|
||||
class CompareGT extends Opcode, TCompareGT {
|
||||
override string toString() { result = "CompareGT" }
|
||||
}
|
||||
|
||||
class CompareGE extends Opcode, TCompareGE {
|
||||
override string toString() { result = "CompareGE" }
|
||||
}
|
||||
|
||||
class Convert extends Opcode, TConvert {
|
||||
override string toString() { result = "Convert" }
|
||||
}
|
||||
|
||||
class AddOne extends Opcode, TAddOne {
|
||||
override string toString() { result = "AddOne" }
|
||||
}
|
||||
|
||||
class SubOne extends Opcode, TSubOne {
|
||||
override string toString() { result = "SubOne" }
|
||||
}
|
||||
|
||||
class PostInc extends Opcode, TPostInc {
|
||||
override string toString() { result = "PostInc" }
|
||||
}
|
||||
|
||||
class PostDec extends Opcode, TPostDec {
|
||||
override string toString() { result = "PostDec" }
|
||||
}
|
||||
|
||||
class Conditional extends Opcode, TConditional {
|
||||
override string toString() { result = "Conditional" }
|
||||
}
|
||||
|
||||
class Constant extends Opcode, TConstant {
|
||||
override string toString() { result = "Constant" }
|
||||
}
|
||||
|
||||
class StringConstant extends Opcode, TStringConstant {
|
||||
override string toString() { result = "StringConstant" }
|
||||
}
|
||||
|
||||
class Unknown extends Opcode, TUnknown {
|
||||
override string toString() { result = "Unknown" }
|
||||
}
|
||||
}
|
||||
|
||||
class SemExpr instanceof Specific::Expr {
|
||||
final string toString() { result = Specific::exprToString(this) }
|
||||
|
||||
final Location getLocation() { result = Specific::getExprLocation(this) }
|
||||
|
||||
Opcode getOpcode() { result instanceof Opcode::Unknown }
|
||||
|
||||
SemType getSemType() { result = Specific::getUnknownExprType(this) }
|
||||
|
||||
final SemBasicBlock getBasicBlock() { result = Specific::getExprBasicBlock(this) }
|
||||
}
|
||||
|
||||
abstract private class SemKnownExpr extends SemExpr {
|
||||
Opcode opcode;
|
||||
SemType type;
|
||||
|
||||
final override Opcode getOpcode() { result = opcode }
|
||||
|
||||
final override SemType getSemType() { result = type }
|
||||
}
|
||||
|
||||
class SemLiteralExpr extends SemKnownExpr {
|
||||
SemLiteralExpr() {
|
||||
Specific::integerLiteral(this, type, _) and opcode instanceof Opcode::Constant
|
||||
or
|
||||
Specific::largeIntegerLiteral(this, type, _) and opcode instanceof Opcode::Constant
|
||||
or
|
||||
Specific::booleanLiteral(this, type, _) and opcode instanceof Opcode::Constant
|
||||
or
|
||||
Specific::floatingPointLiteral(this, type, _) and opcode instanceof Opcode::Constant
|
||||
or
|
||||
Specific::nullLiteral(this, type) and opcode instanceof Opcode::Constant
|
||||
or
|
||||
Specific::stringLiteral(this, type, _) and opcode instanceof Opcode::StringConstant
|
||||
}
|
||||
}
|
||||
|
||||
class SemNumericLiteralExpr extends SemLiteralExpr {
|
||||
SemNumericLiteralExpr() {
|
||||
expr instanceof IntegerLiteral
|
||||
Specific::integerLiteral(this, _, _)
|
||||
or
|
||||
expr instanceof LongLiteral
|
||||
Specific::largeIntegerLiteral(this, _, _)
|
||||
or
|
||||
expr instanceof CharacterLiteral
|
||||
or
|
||||
expr instanceof FloatingPointLiteral
|
||||
or
|
||||
expr instanceof DoubleLiteral
|
||||
Specific::floatingPointLiteral(this, _, _)
|
||||
}
|
||||
|
||||
float getApproximateFloatValue() { none() }
|
||||
@@ -44,246 +231,172 @@ class SemNumericLiteralExpr extends SemLiteralExpr {
|
||||
|
||||
class SemIntegerLiteralExpr extends SemNumericLiteralExpr {
|
||||
SemIntegerLiteralExpr() {
|
||||
expr instanceof IntegerLiteral
|
||||
Specific::integerLiteral(this, _, _)
|
||||
or
|
||||
expr instanceof LongLiteral
|
||||
or
|
||||
expr instanceof CharacterLiteral
|
||||
Specific::largeIntegerLiteral(this, _, _)
|
||||
}
|
||||
|
||||
final int getIntValue() {
|
||||
result = expr.(IntegerLiteral).getIntValue()
|
||||
or
|
||||
result = expr.(CharacterLiteral).getCodePointValue()
|
||||
// To avoid changing analysis results, we don't report an exact `int` value for a `LongLiteral`,
|
||||
// even if it fits in a 32-bit `int`.
|
||||
}
|
||||
final int getIntValue() { Specific::integerLiteral(this, _, result) }
|
||||
|
||||
final override float getApproximateFloatValue() {
|
||||
result = getIntValue()
|
||||
or
|
||||
not exists(getIntValue()) and result = expr.(LongLiteral).getValue().toFloat()
|
||||
Specific::largeIntegerLiteral(this, _, result)
|
||||
}
|
||||
}
|
||||
|
||||
class SemFloatingPointLiteralExpr extends SemNumericLiteralExpr {
|
||||
SemFloatingPointLiteralExpr() {
|
||||
expr instanceof FloatingPointLiteral
|
||||
or
|
||||
expr instanceof DoubleLiteral
|
||||
}
|
||||
float value;
|
||||
|
||||
final override float getApproximateFloatValue() { result = getFloatValue() }
|
||||
SemFloatingPointLiteralExpr() { Specific::floatingPointLiteral(this, _, value) }
|
||||
|
||||
final float getFloatValue() {
|
||||
result = expr.(FloatingPointLiteral).getFloatValue()
|
||||
or
|
||||
result = expr.(DoubleLiteral).getDoubleValue()
|
||||
}
|
||||
final override float getApproximateFloatValue() { result = value }
|
||||
|
||||
final float getFloatValue() { result = value }
|
||||
}
|
||||
|
||||
class SemBinaryExpr extends SemExpr {
|
||||
override BinaryExpr expr;
|
||||
class SemBinaryExpr extends SemKnownExpr {
|
||||
SemExpr leftOperand;
|
||||
SemExpr rightOperand;
|
||||
|
||||
final SemExpr getLeftOperand() { getJavaExpr(result) = expr.getLeftOperand() }
|
||||
SemBinaryExpr() { Specific::binaryExpr(this, opcode, type, leftOperand, rightOperand) }
|
||||
|
||||
final SemExpr getRightOperand() { getJavaExpr(result) = expr.getRightOperand() }
|
||||
final SemExpr getLeftOperand() { result = leftOperand }
|
||||
|
||||
final SemExpr getRightOperand() { result = rightOperand }
|
||||
|
||||
final predicate hasOperands(SemExpr a, SemExpr b) {
|
||||
expr.hasOperands(getJavaExpr(a), getJavaExpr(b))
|
||||
a = getLeftOperand() and b = getRightOperand()
|
||||
or
|
||||
a = getRightOperand() and b = getLeftOperand()
|
||||
}
|
||||
|
||||
final SemExpr getAnOperand() { getJavaExpr(result) = expr.getAnOperand() }
|
||||
final SemExpr getAnOperand() { result = getLeftOperand() or result = getRightOperand() }
|
||||
}
|
||||
|
||||
class SemComparisonExpr extends SemBinaryExpr {
|
||||
override ComparisonExpr expr;
|
||||
class SemRelationalExpr extends SemBinaryExpr {
|
||||
SemRelationalExpr() {
|
||||
opcode instanceof Opcode::CompareLT
|
||||
or
|
||||
opcode instanceof Opcode::CompareLE
|
||||
or
|
||||
opcode instanceof Opcode::CompareGT
|
||||
or
|
||||
opcode instanceof Opcode::CompareGE
|
||||
}
|
||||
|
||||
final SemExpr getLesserOperand() { getJavaExpr(result) = expr.getLesserOperand() }
|
||||
final SemExpr getLesserOperand() {
|
||||
if opcode instanceof Opcode::CompareLT or opcode instanceof Opcode::CompareLE
|
||||
then result = getLeftOperand()
|
||||
else result = getRightOperand()
|
||||
}
|
||||
|
||||
final SemExpr getGreaterOperand() { getJavaExpr(result) = expr.getGreaterOperand() }
|
||||
final SemExpr getGreaterOperand() {
|
||||
if opcode instanceof Opcode::CompareGT or opcode instanceof Opcode::CompareGE
|
||||
then result = getLeftOperand()
|
||||
else result = getRightOperand()
|
||||
}
|
||||
|
||||
final predicate isStrict() { expr.isStrict() }
|
||||
final predicate isStrict() {
|
||||
opcode instanceof Opcode::CompareLT or opcode instanceof Opcode::CompareGT
|
||||
}
|
||||
}
|
||||
|
||||
class SemAddExpr extends SemBinaryExpr {
|
||||
override AddExpr expr;
|
||||
SemAddExpr() { opcode instanceof Opcode::Add }
|
||||
}
|
||||
|
||||
class SemSubExpr extends SemBinaryExpr {
|
||||
override SubExpr expr;
|
||||
SemSubExpr() { opcode instanceof Opcode::Sub }
|
||||
}
|
||||
|
||||
class SemMulExpr extends SemBinaryExpr {
|
||||
override MulExpr expr;
|
||||
SemMulExpr() { opcode instanceof Opcode::Mul }
|
||||
}
|
||||
|
||||
class SemDivExpr extends SemBinaryExpr {
|
||||
override DivExpr expr;
|
||||
SemDivExpr() { opcode instanceof Opcode::Div }
|
||||
}
|
||||
|
||||
class SemRemExpr extends SemBinaryExpr {
|
||||
override RemExpr expr;
|
||||
SemRemExpr() { opcode instanceof Opcode::Rem }
|
||||
}
|
||||
|
||||
class SemLShiftExpr extends SemBinaryExpr {
|
||||
override LShiftExpr expr;
|
||||
class SemShiftLeftExpr extends SemBinaryExpr {
|
||||
SemShiftLeftExpr() { opcode instanceof Opcode::ShiftLeft }
|
||||
}
|
||||
|
||||
class SemRShiftExpr extends SemBinaryExpr {
|
||||
override RShiftExpr expr;
|
||||
class SemShiftRightExpr extends SemBinaryExpr {
|
||||
SemShiftRightExpr() { opcode instanceof Opcode::ShiftRight }
|
||||
}
|
||||
|
||||
class SemURShiftExpr extends SemBinaryExpr {
|
||||
override URShiftExpr expr;
|
||||
class SemBitAndExpr extends SemBinaryExpr {
|
||||
SemBitAndExpr() { opcode instanceof Opcode::BitAnd }
|
||||
}
|
||||
|
||||
class SemAndBitwiseExpr extends SemBinaryExpr {
|
||||
override AndBitwiseExpr expr;
|
||||
class SemBitOrExpr extends SemBinaryExpr {
|
||||
SemBitOrExpr() { opcode instanceof Opcode::BitOr }
|
||||
}
|
||||
|
||||
class SemOrBitwiseExpr extends SemBinaryExpr {
|
||||
override OrBitwiseExpr expr;
|
||||
class SemBitXorExpr extends SemBinaryExpr {
|
||||
SemBitXorExpr() { opcode instanceof Opcode::BitXor }
|
||||
}
|
||||
|
||||
class SemCastExpr extends SemExpr {
|
||||
override CastExpr expr;
|
||||
class SemUnaryExpr extends SemKnownExpr {
|
||||
SemExpr operand;
|
||||
|
||||
final SemExpr getExpr() { getJavaExpr(result) = expr.getExpr() }
|
||||
SemUnaryExpr() { Specific::unaryExpr(this, opcode, type, operand) }
|
||||
|
||||
final SemExpr getOperand() { result = operand }
|
||||
}
|
||||
|
||||
class SemUnaryExpr extends SemExpr {
|
||||
override UnaryExpr expr;
|
||||
|
||||
final SemExpr getExpr() { getJavaExpr(result) = expr.getExpr() }
|
||||
class SemConvertExpr extends SemUnaryExpr {
|
||||
SemConvertExpr() { opcode instanceof Opcode::Convert }
|
||||
}
|
||||
|
||||
class SemIncrementExpr extends SemUnaryExpr {
|
||||
SemIncrementExpr() {
|
||||
expr instanceof PreIncExpr
|
||||
class SemCopyValueExpr extends SemUnaryExpr {
|
||||
SemCopyValueExpr() { opcode instanceof Opcode::CopyValue }
|
||||
}
|
||||
|
||||
class SemNegateExpr extends SemUnaryExpr {
|
||||
SemNegateExpr() { opcode instanceof Opcode::Negate }
|
||||
}
|
||||
|
||||
class SemBitComplementExpr extends SemUnaryExpr {
|
||||
SemBitComplementExpr() { opcode instanceof Opcode::BitComplement }
|
||||
}
|
||||
|
||||
class SemLogicalNotExpr extends SemUnaryExpr {
|
||||
SemLogicalNotExpr() { opcode instanceof Opcode::LogicalNot }
|
||||
}
|
||||
|
||||
class SemAddOneExpr extends SemUnaryExpr {
|
||||
SemAddOneExpr() { opcode instanceof Opcode::AddOne }
|
||||
}
|
||||
|
||||
class SemSubOneExpr extends SemUnaryExpr {
|
||||
SemSubOneExpr() { opcode instanceof Opcode::SubOne }
|
||||
}
|
||||
|
||||
class SemLoadExpr extends SemKnownExpr {
|
||||
SemLoadExpr() { opcode instanceof Opcode::Load and Specific::loadExpr(this, type) }
|
||||
|
||||
final SemSsaVariable getDef() { result = Specific::getLoadDef(this) }
|
||||
}
|
||||
|
||||
class SemConditionalExpr extends SemKnownExpr {
|
||||
SemExpr condition;
|
||||
SemExpr trueResult;
|
||||
SemExpr falseResult;
|
||||
|
||||
SemConditionalExpr() {
|
||||
opcode instanceof Opcode::Conditional and
|
||||
Specific::conditionalExpr(this, type, condition, trueResult, falseResult)
|
||||
}
|
||||
|
||||
final SemExpr getBranchExpr(boolean branch) {
|
||||
branch = true and result = trueResult
|
||||
or
|
||||
expr instanceof PostIncExpr
|
||||
branch = false and result = falseResult
|
||||
}
|
||||
}
|
||||
|
||||
class SemDecrementExpr extends SemUnaryExpr {
|
||||
SemDecrementExpr() {
|
||||
expr instanceof PreDecExpr
|
||||
or
|
||||
expr instanceof PostDecExpr
|
||||
}
|
||||
}
|
||||
|
||||
class SemPreIncExpr extends SemIncrementExpr {
|
||||
override PreIncExpr expr;
|
||||
}
|
||||
|
||||
class SemPreDecExpr extends SemDecrementExpr {
|
||||
override PreDecExpr expr;
|
||||
}
|
||||
|
||||
class SemPostIncExpr extends SemIncrementExpr {
|
||||
override PostIncExpr expr;
|
||||
}
|
||||
|
||||
class SemPostDecExpr extends SemDecrementExpr {
|
||||
override PostDecExpr expr;
|
||||
}
|
||||
|
||||
class SemMinusExpr extends SemUnaryExpr {
|
||||
override MinusExpr expr;
|
||||
}
|
||||
|
||||
class SemBitNotExpr extends SemUnaryExpr {
|
||||
override BitNotExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignment extends SemExpr {
|
||||
override Assignment expr;
|
||||
|
||||
final SemExpr getDest() { getJavaExpr(result) = expr.getDest() }
|
||||
|
||||
final SemExpr getRhs() { getJavaExpr(result) = expr.getRhs() }
|
||||
}
|
||||
|
||||
class SemAssignExpr extends SemAssignment {
|
||||
override AssignExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignOp extends SemAssignment {
|
||||
override AssignOp expr;
|
||||
|
||||
final SemExpr getSource() { getJavaExpr(result) = expr.getSource() }
|
||||
}
|
||||
|
||||
class SemAssignAddExpr extends SemAssignOp {
|
||||
override AssignAddExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignOrExpr extends SemAssignOp {
|
||||
override AssignOrExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignSubExpr extends SemAssignOp {
|
||||
override AssignSubExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignMulExpr extends SemAssignOp {
|
||||
override AssignMulExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignDivExpr extends SemAssignOp {
|
||||
override AssignDivExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignRemExpr extends SemAssignOp {
|
||||
override AssignRemExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignLShiftExpr extends SemAssignOp {
|
||||
override AssignLShiftExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignRShiftExpr extends SemAssignOp {
|
||||
override AssignRShiftExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignURShiftExpr extends SemAssignOp {
|
||||
override AssignURShiftExpr expr;
|
||||
}
|
||||
|
||||
class SemAssignAndExpr extends SemAssignOp {
|
||||
override AssignAndExpr expr;
|
||||
}
|
||||
|
||||
class SemVariableAssign extends SemExpr {
|
||||
override VariableAssign expr;
|
||||
|
||||
final SemExpr getSource() { getJavaExpr(result) = expr.getSource() }
|
||||
}
|
||||
|
||||
class SemVarAccess extends SemExpr {
|
||||
override VarAccess expr;
|
||||
}
|
||||
|
||||
class SemVariableUpdate extends SemExpr {
|
||||
override VariableUpdate expr;
|
||||
}
|
||||
|
||||
class SemPlusExpr extends SemUnaryExpr {
|
||||
override PlusExpr expr;
|
||||
}
|
||||
|
||||
class SemConditionalExpr extends SemExpr {
|
||||
override ConditionalExpr expr;
|
||||
|
||||
final SemExpr getBranchExpr(boolean branch) { getJavaExpr(result) = expr.getBranchExpr(branch) }
|
||||
}
|
||||
|
||||
class SemNullLiteral extends SemExpr {
|
||||
override NullLiteral expr;
|
||||
}
|
||||
|
||||
Expr getJavaExpr(SemExpr e) { e = MkExpr(result) }
|
||||
|
||||
SemExpr getSemanticExpr(Expr e) { e = getJavaExpr(result) }
|
||||
|
||||
286
java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll
Normal file
286
java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll
Normal file
@@ -0,0 +1,286 @@
|
||||
private import java as J
|
||||
private import SemanticCFG
|
||||
private import SemanticExpr
|
||||
private import SemanticSSA
|
||||
private import SemanticType
|
||||
private import semmle.code.java.dataflow.SSA as SSA
|
||||
|
||||
private module Impl {
|
||||
newtype TExpr =
|
||||
TPrimaryExpr(J::Expr e) or
|
||||
TPostUpdateExpr(J::UnaryAssignExpr e) {
|
||||
e instanceof J::PostIncExpr or e instanceof J::PostDecExpr
|
||||
}
|
||||
|
||||
TExpr getResultExpr(J::Expr e) { result = TPrimaryExpr(e) }
|
||||
}
|
||||
|
||||
module SemanticExprConfig {
|
||||
private import Impl
|
||||
|
||||
class Expr extends TExpr {
|
||||
string toString() { none() }
|
||||
|
||||
J::Location getLocation() { none() }
|
||||
}
|
||||
|
||||
private class PrimaryExpr extends Expr, TPrimaryExpr {
|
||||
J::Expr e;
|
||||
|
||||
PrimaryExpr() { this = TPrimaryExpr(e) }
|
||||
|
||||
override string toString() { result = e.toString() }
|
||||
|
||||
override J::Location getLocation() { result = e.getLocation() }
|
||||
|
||||
J::Expr getExpr() { result = e }
|
||||
}
|
||||
|
||||
private class PostUpdateExpr extends Expr, TPostUpdateExpr {
|
||||
J::UnaryAssignExpr e;
|
||||
|
||||
PostUpdateExpr() { this = TPostUpdateExpr(e) }
|
||||
|
||||
override string toString() { result = "post-update for " + e.toString() }
|
||||
|
||||
override J::Location getLocation() { result = e.getLocation() }
|
||||
|
||||
J::UnaryAssignExpr getExpr() { result = e }
|
||||
}
|
||||
|
||||
string exprToString(Expr e) { result = e.toString() }
|
||||
|
||||
J::Location getExprLocation(Expr e) { result = e.getLocation() }
|
||||
|
||||
SemBasicBlock getExprBasicBlock(Expr e) { result.getAnExpr() = e }
|
||||
|
||||
predicate integerLiteral(Expr expr, SemIntegerType type, int value) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
(
|
||||
value = javaExpr.(J::IntegerLiteral).getIntValue()
|
||||
or
|
||||
value = javaExpr.(J::CharacterLiteral).getCodePointValue()
|
||||
)
|
||||
// For compatibility reasons, we don't provide exact values for `LongLiteral`s, even if the value
|
||||
// would fit in an `int`.
|
||||
)
|
||||
}
|
||||
|
||||
predicate largeIntegerLiteral(Expr expr, SemIntegerType type, float approximateFloatValue) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
approximateFloatValue = javaExpr.(J::LongLiteral).getValue().toFloat()
|
||||
)
|
||||
}
|
||||
|
||||
predicate floatingPointLiteral(Expr expr, SemFloatingPointType type, float value) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
(
|
||||
value = javaExpr.(J::FloatingPointLiteral).getFloatValue()
|
||||
or
|
||||
value = javaExpr.(J::DoubleLiteral).getDoubleValue()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
predicate booleanLiteral(Expr expr, SemBooleanType type, boolean value) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
value = javaExpr.(J::BooleanLiteral).getBooleanValue()
|
||||
)
|
||||
}
|
||||
|
||||
predicate nullLiteral(Expr expr, SemAddressType type) {
|
||||
type = getSemanticType(expr.(PrimaryExpr).getExpr().(J::NullLiteral).getType())
|
||||
}
|
||||
|
||||
predicate stringLiteral(Expr expr, SemType type, string value) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
value = javaExpr.(J::StringLiteral).getValue()
|
||||
)
|
||||
}
|
||||
|
||||
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
|
||||
exists(J::Expr javaExpr | javaExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
(
|
||||
exists(J::BinaryExpr binary | binary = javaExpr |
|
||||
leftOperand = getResultExpr(binary.getLeftOperand()) and
|
||||
rightOperand = getResultExpr(binary.getRightOperand()) and
|
||||
(
|
||||
binary instanceof J::AddExpr and opcode instanceof Opcode::Add
|
||||
or
|
||||
binary instanceof J::SubExpr and opcode instanceof Opcode::Sub
|
||||
or
|
||||
binary instanceof J::MulExpr and opcode instanceof Opcode::Mul
|
||||
or
|
||||
binary instanceof J::DivExpr and opcode instanceof Opcode::Div
|
||||
or
|
||||
binary instanceof J::RemExpr and opcode instanceof Opcode::Rem
|
||||
or
|
||||
binary instanceof J::AndBitwiseExpr and opcode instanceof Opcode::BitAnd
|
||||
or
|
||||
binary instanceof J::OrBitwiseExpr and opcode instanceof Opcode::BitOr
|
||||
or
|
||||
binary instanceof J::XorBitwiseExpr and opcode instanceof Opcode::BitXor
|
||||
or
|
||||
binary instanceof J::LShiftExpr and opcode instanceof Opcode::ShiftLeft
|
||||
or
|
||||
binary instanceof J::RShiftExpr and opcode instanceof Opcode::ShiftRight
|
||||
or
|
||||
binary instanceof J::URShiftExpr and opcode instanceof Opcode::ShiftRightUnsigned
|
||||
or
|
||||
binary instanceof J::EQExpr and opcode instanceof Opcode::CompareEQ
|
||||
or
|
||||
binary instanceof J::NEExpr and opcode instanceof Opcode::CompareNE
|
||||
or
|
||||
binary instanceof J::LTExpr and opcode instanceof Opcode::CompareLT
|
||||
or
|
||||
binary instanceof J::LEExpr and opcode instanceof Opcode::CompareLE
|
||||
or
|
||||
binary instanceof J::GTExpr and opcode instanceof Opcode::CompareGT
|
||||
or
|
||||
binary instanceof J::GEExpr and opcode instanceof Opcode::CompareGE
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(J::AssignOp assignOp | assignOp = javaExpr |
|
||||
leftOperand = getResultExpr(assignOp.getDest()) and
|
||||
rightOperand = getResultExpr(assignOp.getRhs()) and
|
||||
(
|
||||
assignOp instanceof J::AssignAddExpr and opcode instanceof Opcode::Add
|
||||
or
|
||||
assignOp instanceof J::AssignSubExpr and opcode instanceof Opcode::Sub
|
||||
or
|
||||
assignOp instanceof J::AssignMulExpr and opcode instanceof Opcode::Mul
|
||||
or
|
||||
assignOp instanceof J::AssignDivExpr and opcode instanceof Opcode::Div
|
||||
or
|
||||
assignOp instanceof J::AssignRemExpr and opcode instanceof Opcode::Rem
|
||||
or
|
||||
assignOp instanceof J::AssignAndExpr and opcode instanceof Opcode::BitAnd
|
||||
or
|
||||
assignOp instanceof J::AssignOrExpr and opcode instanceof Opcode::BitOr
|
||||
or
|
||||
assignOp instanceof J::AssignXorExpr and opcode instanceof Opcode::BitXor
|
||||
or
|
||||
assignOp instanceof J::AssignLShiftExpr and opcode instanceof Opcode::ShiftLeft
|
||||
or
|
||||
assignOp instanceof J::AssignRShiftExpr and opcode instanceof Opcode::ShiftRight
|
||||
or
|
||||
// TODO: Add new opcode or add an implicit conversion
|
||||
assignOp instanceof J::AssignURShiftExpr and opcode instanceof Opcode::ShiftRightUnsigned
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
|
||||
exists(J::Expr javaExpr | expr = TPrimaryExpr(javaExpr) |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
(
|
||||
exists(J::UnaryExpr unary | unary = javaExpr |
|
||||
operand = getResultExpr(unary.getExpr()) and
|
||||
(
|
||||
unary instanceof J::MinusExpr and opcode instanceof Opcode::Negate
|
||||
or
|
||||
unary instanceof J::PlusExpr and opcode instanceof Opcode::CopyValue
|
||||
or
|
||||
unary instanceof J::BitNotExpr and opcode instanceof Opcode::BitComplement
|
||||
or
|
||||
unary instanceof J::LogNotExpr and opcode instanceof Opcode::LogicalNot
|
||||
or
|
||||
unary instanceof J::PreIncExpr and opcode instanceof Opcode::AddOne
|
||||
or
|
||||
unary instanceof J::PreDecExpr and opcode instanceof Opcode::SubOne
|
||||
or
|
||||
// Post-increment/decrement returns the original value. The actual increment/decrement part
|
||||
// is a separate `Expr`.
|
||||
unary instanceof J::PostIncExpr and opcode instanceof Opcode::CopyValue
|
||||
or
|
||||
unary instanceof J::PostDecExpr and opcode instanceof Opcode::CopyValue
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(J::CastExpr cast | cast = javaExpr |
|
||||
// TODO: Boolean? Null? Boxing?
|
||||
type instanceof SemNumericType and
|
||||
getSemanticType(cast.getExpr().getType()) instanceof SemNumericType and
|
||||
opcode instanceof Opcode::Convert and
|
||||
operand = getResultExpr(cast.getExpr())
|
||||
)
|
||||
or
|
||||
exists(J::AssignExpr assign | assign = javaExpr |
|
||||
opcode instanceof Opcode::CopyValue and
|
||||
operand = getResultExpr(assign.getSource())
|
||||
)
|
||||
or
|
||||
exists(J::LocalVariableDeclExpr decl | decl = javaExpr |
|
||||
opcode instanceof Opcode::CopyValue and
|
||||
operand = getResultExpr(decl.getInit())
|
||||
)
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(J::UnaryAssignExpr javaExpr | javaExpr = expr.(PostUpdateExpr).getExpr() |
|
||||
type = getSemanticType(javaExpr.getType()) and
|
||||
operand = getResultExpr(javaExpr.getExpr()) and
|
||||
(
|
||||
javaExpr instanceof J::PostIncExpr and opcode instanceof Opcode::AddOne
|
||||
or
|
||||
javaExpr instanceof J::PostDecExpr and opcode instanceof Opcode::SubOne
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
predicate loadExpr(Expr expr, SemType type) {
|
||||
type = getSemanticType(expr.(PrimaryExpr).getExpr().(J::RValue).getType())
|
||||
}
|
||||
|
||||
SemSsaVariable getLoadDef(Expr expr) {
|
||||
exists(SSA::SsaVariable var | expr.(PrimaryExpr).getExpr() = var.getAUse() |
|
||||
result = getSemanticSsaVariable(var)
|
||||
)
|
||||
}
|
||||
|
||||
predicate conditionalExpr(
|
||||
Expr expr, SemType type, Expr condition, Expr trueResult, Expr falseResult
|
||||
) {
|
||||
exists(J::ConditionalExpr condExpr | condExpr = expr.(PrimaryExpr).getExpr() |
|
||||
type = getSemanticType(condExpr.getType()) and
|
||||
condition = getResultExpr(condExpr.getCondition()) and
|
||||
trueResult = getResultExpr(condExpr.getTrueExpr()) and
|
||||
falseResult = getResultExpr(condExpr.getFalseExpr())
|
||||
)
|
||||
}
|
||||
|
||||
SemType getUnknownExprType(Expr expr) {
|
||||
result = getSemanticType(expr.(PrimaryExpr).getExpr().getType())
|
||||
}
|
||||
}
|
||||
|
||||
private import Impl
|
||||
|
||||
SemExpr getSemanticExpr(J::Expr javaExpr) { result = TPrimaryExpr(javaExpr) }
|
||||
|
||||
J::Expr getJavaExpr(SemExpr e) { e = getSemanticExpr(result) }
|
||||
|
||||
SemExpr getUpdateExpr(SSA::SsaExplicitUpdate update) {
|
||||
exists(J::Expr expr | expr = update.getDefiningExpr() |
|
||||
(
|
||||
expr instanceof J::Assignment or
|
||||
expr instanceof J::PreIncExpr or
|
||||
expr instanceof J::PreDecExpr
|
||||
) and
|
||||
result = getResultExpr(expr)
|
||||
or
|
||||
result = getResultExpr(expr.(J::LocalVariableDeclExpr).getInit())
|
||||
or
|
||||
(expr instanceof J::PostIncExpr or expr instanceof J::PostDecExpr) and
|
||||
result = TPostUpdateExpr(expr)
|
||||
)
|
||||
}
|
||||
@@ -7,6 +7,7 @@ private import semmle.code.java.controlflow.Guards
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
||||
private import SemanticCFG
|
||||
private import SemanticExpr
|
||||
private import SemanticExprSpecific
|
||||
private import SemanticSSA
|
||||
|
||||
class LanguageGuard = Guard;
|
||||
@@ -68,7 +69,7 @@ predicate semGuardControlsSsaRead(SemGuard guard, SemSsaReadPosition controlled,
|
||||
)
|
||||
}
|
||||
|
||||
SemGuard semGetComparisonGuard(SemComparisonExpr e) { result = getSemanticGuard(getJavaExpr(e)) }
|
||||
SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = getSemanticGuard(getJavaExpr(e)) }
|
||||
|
||||
SemGuard getSemanticGuard(LanguageGuard guard) { result = MkSemGuard(guard) }
|
||||
|
||||
|
||||
@@ -8,6 +8,7 @@ private import SemanticCFG
|
||||
private import SemanticExpr
|
||||
private import SemanticType
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||
private import SemanticExprSpecific
|
||||
|
||||
private newtype TSemSsaVariable = MkSemSsaVariable(SSA::SsaVariable var)
|
||||
|
||||
@@ -30,7 +31,9 @@ class SemSsaVariable extends TSemSsaVariable {
|
||||
class SemSsaExplicitUpdate extends SemSsaVariable {
|
||||
override SSA::SsaExplicitUpdate var;
|
||||
|
||||
final SemExpr getDefiningExpr() { result = getSemanticExpr(var.getDefiningExpr()) }
|
||||
final SemExpr getSourceExpr() { result = getUpdateExpr(var) }
|
||||
|
||||
deprecated final SemExpr getDefiningExpr() { result = getSemanticExpr(var.getDefiningExpr()) }
|
||||
}
|
||||
|
||||
class SemSsaPhiNode extends SemSsaVariable {
|
||||
@@ -72,6 +75,8 @@ class SemSsaReadPosition extends TSemSsaReadPosition {
|
||||
|
||||
final string toString() { result = pos.toString() }
|
||||
|
||||
Location getLocation() { none() }
|
||||
|
||||
final predicate hasReadOfVar(SemSsaVariable var) { pos.hasReadOfVar(getJavaSsaVariable(var)) }
|
||||
}
|
||||
|
||||
@@ -82,6 +87,8 @@ class SemSsaReadPositionPhiInputEdge extends SemSsaReadPosition {
|
||||
pos.phiInput(getJavaSsaVariable(phi), getJavaSsaVariable(inp))
|
||||
}
|
||||
|
||||
override Location getLocation() { result = getPhiBlock().getLocation() }
|
||||
|
||||
SemBasicBlock getOrigBlock() { result = getSemanticBasicBlock(pos.getOrigBlock()) }
|
||||
|
||||
SemBasicBlock getPhiBlock() { result = getSemanticBasicBlock(pos.getPhiBlock()) }
|
||||
@@ -90,6 +97,8 @@ class SemSsaReadPositionPhiInputEdge extends SemSsaReadPosition {
|
||||
class SemSsaReadPositionBlock extends SemSsaReadPosition {
|
||||
override SsaReadPositionBlock pos;
|
||||
|
||||
override Location getLocation() { result = getBlock().getLocation() }
|
||||
|
||||
SemBasicBlock getBlock() { result = getSemanticBasicBlock(pos.getBlock()) }
|
||||
|
||||
SemExpr getAnExpr() { result = getBlock().getAnExpr() }
|
||||
|
||||
@@ -15,7 +15,7 @@ private predicate constantIntegerExpr(SemExpr e, int val) {
|
||||
// Copy of another constant
|
||||
exists(SemSsaExplicitUpdate v, SemExpr src |
|
||||
e = v.getAUse() and
|
||||
src = v.getDefiningExpr().(SemVariableAssign).getSource() and
|
||||
src = v.getSourceExpr() and
|
||||
constantIntegerExpr(src, val)
|
||||
)
|
||||
or
|
||||
|
||||
@@ -1,5 +1,6 @@
|
||||
private import java
|
||||
private import semmle.code.java.semantic.SemanticExpr
|
||||
private import semmle.code.java.semantic.SemanticExprSpecific
|
||||
private import ArrayLengthFlow
|
||||
|
||||
/**
|
||||
|
||||
@@ -5,11 +5,62 @@ private import semmle.code.java.Collections
|
||||
private import semmle.code.java.Maps
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||
private import semmle.code.java.security.RandomDataSource
|
||||
private import semmle.code.java.semantic.SemanticExprSpecific
|
||||
private import semmle.code.java.semantic.SemanticExpr
|
||||
private import semmle.code.java.semantic.SemanticSSA
|
||||
private import semmle.code.java.semantic.SemanticType
|
||||
private import ArrayLengthFlow
|
||||
|
||||
/**
|
||||
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
|
||||
*
|
||||
* This predicate is to keep the results identical to the original Java implementation. It should be
|
||||
* removed once we hae the new implementation matching the old results exactly.
|
||||
*/
|
||||
predicate ignoreSsaReadCopy(SemExpr e) {
|
||||
getJavaExpr(e) instanceof LocalVariableDeclExpr
|
||||
or
|
||||
getJavaExpr(e) instanceof PlusExpr
|
||||
or
|
||||
getJavaExpr(e) instanceof PostIncExpr
|
||||
or
|
||||
getJavaExpr(e) instanceof PostDecExpr
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
|
||||
*
|
||||
* This predicate is to keep the results identical to the original Java implementation. It should be
|
||||
* removed once we hae the new implementation matching the old results exactly.
|
||||
*/
|
||||
predicate ignoreSsaReadArithmeticExpr(SemExpr e) { getJavaExpr(e) instanceof AssignOp }
|
||||
|
||||
/**
|
||||
* Holds if the specified variable should be excluded from the result of `ssaRead()`.
|
||||
*
|
||||
* This predicate is to keep the results identical to the original Java implementation. It should be
|
||||
* removed once we hae the new implementation matching the old results exactly.
|
||||
*/
|
||||
predicate ignoreSsaReadAssignment(SemSsaVariable v) {
|
||||
getJavaSsaVariable(v).(SsaExplicitUpdate).getDefiningExpr() instanceof LocalVariableDeclExpr
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds additional results to `ssaRead()` that are specific to Java.
|
||||
*
|
||||
* This predicate handles propagation of offsets for post-increment and post-decrement expressions
|
||||
* in exactly the same way as the old Java implementation. Once the new implementation matches the
|
||||
* old one, we should remove this predicate and propagate deltas for all similar patterns, whether
|
||||
* or not they come from a post-increment/decrement expression.
|
||||
*/
|
||||
SemExpr specificSsaRead(SemSsaVariable v, int delta) {
|
||||
exists(SsaExplicitUpdate ssaVar | ssaVar = getJavaSsaVariable(v) |
|
||||
result = getSemanticExpr(ssaVar.getDefiningExpr().(PostIncExpr)) and delta = 1
|
||||
or
|
||||
result = getSemanticExpr(ssaVar.getDefiningExpr().(PostDecExpr)) and delta = -1
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
|
||||
*/
|
||||
@@ -79,23 +130,6 @@ predicate additionalValueFlowStep(SemExpr dest, SemExpr src, int delta) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the specified cast expression is known to not overflow or underflow.
|
||||
*/
|
||||
predicate isSafeCast(SemCastExpr cast) {
|
||||
exists(CastExpr javaCast, Type fromType, Type toType |
|
||||
getSemanticExpr(javaCast) = cast and
|
||||
fromType = javaCast.getExpr().getType() and
|
||||
toType = javaCast.getType()
|
||||
|
|
||||
conversionCannotOverflow(getSemanticType(fromType.(BoxedType).getPrimitiveType()),
|
||||
getSemanticType(toType))
|
||||
or
|
||||
conversionCannotOverflow(getSemanticType(fromType),
|
||||
getSemanticType(toType.(BoxedType).getPrimitiveType()))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the type that range analysis should use to track the result of the specified expression,
|
||||
* if a type other than the original type of the expression is to be used.
|
||||
|
||||
@@ -14,31 +14,32 @@ private import ConstantAnalysis
|
||||
* Gets an expression that equals `v - d`.
|
||||
*/
|
||||
SemExpr semSsaRead(SemSsaVariable v, int delta) {
|
||||
// There are various language-specific extension points that can be removed once we no longer
|
||||
// expect to match the original Java implementation's results exactly.
|
||||
result = v.getAUse() and delta = 0
|
||||
or
|
||||
exists(int d1, SemConstantIntegerExpr c |
|
||||
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
|
||||
delta = d1 - c.getIntValue()
|
||||
delta = d1 - c.getIntValue() and
|
||||
not Specific::ignoreSsaReadArithmeticExpr(result)
|
||||
)
|
||||
or
|
||||
exists(SemSubExpr sub, int d1, SemConstantIntegerExpr c |
|
||||
result = sub and
|
||||
sub.getLeftOperand() = semSsaRead(v, d1) and
|
||||
sub.getRightOperand() = c and
|
||||
delta = d1 + c.getIntValue()
|
||||
delta = d1 + c.getIntValue() and
|
||||
not Specific::ignoreSsaReadArithmeticExpr(result)
|
||||
)
|
||||
or
|
||||
v.(SemSsaExplicitUpdate).getDefiningExpr().(SemPreIncExpr) = result and delta = 0
|
||||
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
|
||||
delta = 0 and
|
||||
not Specific::ignoreSsaReadAssignment(v)
|
||||
or
|
||||
v.(SemSsaExplicitUpdate).getDefiningExpr().(SemPreDecExpr) = result and delta = 0
|
||||
result = Specific::specificSsaRead(v, delta)
|
||||
or
|
||||
v.(SemSsaExplicitUpdate).getDefiningExpr().(SemPostIncExpr) = result and delta = 1 // x++ === ++x - 1
|
||||
or
|
||||
v.(SemSsaExplicitUpdate).getDefiningExpr().(SemPostDecExpr) = result and delta = -1 // x-- === --x + 1
|
||||
or
|
||||
v.(SemSsaExplicitUpdate).getDefiningExpr().(SemAssignment) = result and delta = 0
|
||||
or
|
||||
result.(SemAssignExpr).getRhs() = semSsaRead(v, delta)
|
||||
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) and
|
||||
not Specific::ignoreSsaReadCopy(result)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -64,46 +65,36 @@ SemGuard semEqFlowCond(SemSsaVariable v, SemExpr e, int delta, boolean isEq, boo
|
||||
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
|
||||
*/
|
||||
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, int delta) {
|
||||
v.getDefiningExpr().(SemVariableAssign).getSource() = e and delta = 0
|
||||
or
|
||||
v.getDefiningExpr().(SemPostIncExpr).getExpr() = e and delta = 1
|
||||
or
|
||||
v.getDefiningExpr().(SemPreIncExpr).getExpr() = e and delta = 1
|
||||
or
|
||||
v.getDefiningExpr().(SemPostDecExpr).getExpr() = e and delta = -1
|
||||
or
|
||||
v.getDefiningExpr().(SemPreDecExpr).getExpr() = e and delta = -1
|
||||
or
|
||||
v.getDefiningExpr().(SemAssignOp) = e and delta = 0
|
||||
exists(SemExpr defExpr | defExpr = v.getDefiningExpr() |
|
||||
defExpr.(SemCopyValueExpr).getOperand() = e and delta = 0
|
||||
or
|
||||
defExpr.(SemAddOneExpr).getOperand() = e and delta = 1
|
||||
or
|
||||
defExpr.(SemSubOneExpr).getOperand() = e and delta = -1
|
||||
or
|
||||
e = defExpr and
|
||||
not (
|
||||
defExpr instanceof SemCopyValueExpr or
|
||||
defExpr instanceof SemAddOneExpr or
|
||||
defExpr instanceof SemSubOneExpr
|
||||
) and
|
||||
delta = 0
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e1 + delta` equals `e2`.
|
||||
*/
|
||||
predicate semValueFlowStep(SemExpr e2, SemExpr e1, int delta) {
|
||||
e2.(SemAssignExpr).getRhs() = e1 and delta = 0
|
||||
e2.(SemCopyValueExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(SemPlusExpr).getExpr() = e1 and delta = 0
|
||||
e2.(SemAddOneExpr).getOperand() = e1 and delta = 1
|
||||
or
|
||||
e2.(SemPostIncExpr).getExpr() = e1 and delta = 0
|
||||
or
|
||||
e2.(SemPostDecExpr).getExpr() = e1 and delta = 0
|
||||
or
|
||||
e2.(SemPreIncExpr).getExpr() = e1 and delta = 1
|
||||
or
|
||||
e2.(SemPreDecExpr).getExpr() = e1 and delta = -1
|
||||
e2.(SemSubOneExpr).getOperand() = e1 and delta = -1
|
||||
or
|
||||
Specific::additionalValueFlowStep(e2, e1, delta)
|
||||
or
|
||||
exists(SemExpr x |
|
||||
e2.(SemAddExpr).hasOperands(e1, x)
|
||||
or
|
||||
exists(SemAssignAddExpr add | add = e2 |
|
||||
add.getDest() = e1 and add.getRhs() = x
|
||||
or
|
||||
add.getDest() = x and add.getRhs() = e1
|
||||
)
|
||||
|
|
||||
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
|
||||
x.(SemConstantIntegerExpr).getIntValue() = delta
|
||||
)
|
||||
or
|
||||
@@ -113,12 +104,6 @@ predicate semValueFlowStep(SemExpr e2, SemExpr e1, int delta) {
|
||||
sub.getLeftOperand() = e1 and
|
||||
sub.getRightOperand() = x
|
||||
)
|
||||
or
|
||||
exists(SemAssignSubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getDest() = e1 and
|
||||
sub.getRhs() = x
|
||||
)
|
||||
|
|
||||
x.(SemConstantIntegerExpr).getIntValue() = -delta
|
||||
)
|
||||
|
||||
@@ -1,3 +1,5 @@
|
||||
private import semmle.code.java.semantic.SemanticExpr
|
||||
|
||||
newtype TSign =
|
||||
TNeg() or
|
||||
TZero() or
|
||||
@@ -243,38 +245,38 @@ class Sign extends TSign {
|
||||
}
|
||||
|
||||
/** Perform `op` on this sign. */
|
||||
Sign applyUnaryOp(TUnarySignOperation op) {
|
||||
op = TIncOp() and result = inc()
|
||||
Sign applyUnaryOp(Opcode op) {
|
||||
op instanceof Opcode::AddOne and result = inc()
|
||||
or
|
||||
op = TDecOp() and result = dec()
|
||||
op instanceof Opcode::SubOne and result = dec()
|
||||
or
|
||||
op = TNegOp() and result = neg()
|
||||
op instanceof Opcode::Negate and result = neg()
|
||||
or
|
||||
op = TBitNotOp() and result = bitnot()
|
||||
op instanceof Opcode::BitComplement and result = bitnot()
|
||||
}
|
||||
|
||||
/** Perform `op` on this sign and sign `s`. */
|
||||
Sign applyBinaryOp(Sign s, TBinarySignOperation op) {
|
||||
op = TAddOp() and result = add(s)
|
||||
Sign applyBinaryOp(Sign s, Opcode op) {
|
||||
op instanceof Opcode::Add and result = add(s)
|
||||
or
|
||||
op = TSubOp() and result = sub(s)
|
||||
op instanceof Opcode::Sub and result = sub(s)
|
||||
or
|
||||
op = TMulOp() and result = mul(s)
|
||||
op instanceof Opcode::Mul and result = mul(s)
|
||||
or
|
||||
op = TDivOp() and result = div(s)
|
||||
op instanceof Opcode::Div and result = div(s)
|
||||
or
|
||||
op = TRemOp() and result = rem(s)
|
||||
op instanceof Opcode::Rem and result = rem(s)
|
||||
or
|
||||
op = TBitAndOp() and result = bitand(s)
|
||||
op instanceof Opcode::BitAnd and result = bitand(s)
|
||||
or
|
||||
op = TBitOrOp() and result = bitor(s)
|
||||
op instanceof Opcode::BitOr and result = bitor(s)
|
||||
or
|
||||
op = TBitXorOp() and result = bitxor(s)
|
||||
op instanceof Opcode::BitXor and result = bitxor(s)
|
||||
or
|
||||
op = TLShiftOp() and result = lshift(s)
|
||||
op instanceof Opcode::ShiftLeft and result = lshift(s)
|
||||
or
|
||||
op = TRShiftOp() and result = rshift(s)
|
||||
op instanceof Opcode::ShiftRight and result = rshift(s)
|
||||
or
|
||||
op = TURShiftOp() and result = urshift(s)
|
||||
op instanceof Opcode::ShiftRightUnsigned and result = urshift(s)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -45,9 +45,9 @@ private predicate unknownSign(SemExpr e) {
|
||||
(
|
||||
exists(SemIntegerLiteralExpr lit | lit = e and not exists(lit.getIntValue()))
|
||||
or
|
||||
exists(SemCastExpr cast, SemType fromtyp |
|
||||
exists(SemConvertExpr cast, SemType fromtyp |
|
||||
cast = e and
|
||||
fromtyp = getTrackedType(cast.getExpr()) and
|
||||
fromtyp = getTrackedType(cast.getOperand()) and
|
||||
not fromtyp instanceof SemNumericType
|
||||
)
|
||||
or
|
||||
@@ -62,7 +62,7 @@ private predicate unknownSign(SemExpr e) {
|
||||
private predicate lowerBound(
|
||||
SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
|
||||
) {
|
||||
exists(boolean testIsTrue, SemComparisonExpr comp |
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
not unknownSign(lowerbound)
|
||||
@@ -86,7 +86,7 @@ private predicate lowerBound(
|
||||
private predicate upperBound(
|
||||
SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
|
||||
) {
|
||||
exists(boolean testIsTrue, SemComparisonExpr comp |
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
not unknownSign(upperbound)
|
||||
@@ -191,7 +191,7 @@ private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
|
||||
*/
|
||||
pragma[noinline]
|
||||
private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
result = ssaDefSign(v) and
|
||||
result = semSsaDefSign(v) and
|
||||
pos.hasReadOfVar(v) and
|
||||
hasGuard(v, pos, result)
|
||||
}
|
||||
@@ -202,7 +202,7 @@ private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
*/
|
||||
pragma[noinline]
|
||||
private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
result = ssaDefSign(v) and
|
||||
result = semSsaDefSign(v) and
|
||||
pos.hasReadOfVar(v) and
|
||||
not hasGuard(v, pos, result)
|
||||
}
|
||||
@@ -224,7 +224,7 @@ private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
}
|
||||
|
||||
/** Gets a possible sign for `v` at `pos`. */
|
||||
private Sign ssaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
result = unguardedSsaSign(v, pos)
|
||||
or
|
||||
result = guardedSsaSign(v, pos) and
|
||||
@@ -233,62 +233,62 @@ private Sign ssaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
|
||||
/** Gets a possible sign for `v`. */
|
||||
pragma[nomagic]
|
||||
private Sign ssaDefSign(SemSsaVariable v) {
|
||||
result = explicitSsaDefSign(v)
|
||||
private Sign semSsaDefSign(SemSsaVariable v) {
|
||||
result = semExplicitSsaDefSign(v)
|
||||
or
|
||||
result = implicitSsaDefSign(v)
|
||||
or
|
||||
exists(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
|
||||
v = phi and
|
||||
edge.phiInput(phi, inp) and
|
||||
result = ssaSign(inp, edge)
|
||||
result = semSsaSign(inp, edge)
|
||||
)
|
||||
}
|
||||
|
||||
Sign semSsaPhiSign(SemSsaPhiNode phi) {
|
||||
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
|
||||
edge.phiInput(phi, inp) and
|
||||
result = semSsaSign(inp, edge)
|
||||
)
|
||||
}
|
||||
|
||||
/** Returns the sign of explicit SSA definition `v`. */
|
||||
private Sign explicitSsaDefSign(SemSsaVariable v) {
|
||||
exists(SemVariableUpdate def | def = getExplicitSsaAssignment(v) |
|
||||
result = semExprSign(getExprFromSsaAssignment(def))
|
||||
or
|
||||
semAnySign(result) and explicitSsaDefWithAnySign(def)
|
||||
or
|
||||
result = semExprSign(def.(SemIncrementExpr).getExpr()).inc()
|
||||
or
|
||||
result = semExprSign(def.(SemDecrementExpr).getExpr()).dec()
|
||||
)
|
||||
Sign semExplicitSsaDefSign(SemSsaVariable v) {
|
||||
semAnySign(result) and explicitSsaDefWithAnySign(v)
|
||||
or
|
||||
result = semExprSign(v.(SemSsaExplicitUpdate).getSourceExpr())
|
||||
}
|
||||
|
||||
/** Gets a possible sign for `e`. */
|
||||
cached
|
||||
Sign semExprSign(SemExpr e) {
|
||||
Sign semExprSign(SemExpr e) { result = semExprSign(e, _) }
|
||||
|
||||
Sign semExprSign(SemExpr e, string branch) {
|
||||
not ignoreExprSign(e) and
|
||||
exists(Sign s |
|
||||
// We know exactly what the sign is. This handles constants, collection sizes, etc.
|
||||
s = certainExprSign(e)
|
||||
s = certainExprSign(e) and branch = "certain"
|
||||
or
|
||||
not exists(certainExprSign(e)) and
|
||||
(
|
||||
// We'll never know what the sign is.
|
||||
semAnySign(s) and unknownSign(e)
|
||||
semAnySign(s) and unknownSign(e) and branch = "unknown"
|
||||
or
|
||||
// Propagate via SSA
|
||||
exists(SemSsaVariable v | v.getAUse() = e |
|
||||
// Propagate the sign from the def of `v`, incorporating any inference from guards.
|
||||
s = ssaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = e))
|
||||
s = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = e)) and branch = "use"
|
||||
or
|
||||
// No block for this read. Just use the sign of the def.
|
||||
// REVIEW: How can this happen?
|
||||
not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = e) and
|
||||
s = ssaDefSign(v)
|
||||
s = semSsaDefSign(v) and
|
||||
branch = "def only"
|
||||
)
|
||||
or
|
||||
// A variable access without an SSA definition. Let the language give us any constraints it
|
||||
// can.
|
||||
exists(SemVarAccess access | access = e |
|
||||
not exists(SemSsaVariable v | v.getAUse() = access) and
|
||||
s = getVarAccessSign(access)
|
||||
)
|
||||
s = languageExprSign(e) and branch = "language" // Let the language try
|
||||
or
|
||||
s = specificSubExprSign(e)
|
||||
s = specificSubExprSign(e) and branch = "specific"
|
||||
)
|
||||
|
|
||||
if getTrackedType(e) instanceof SemUnsignedIntegerType and s = TNeg()
|
||||
@@ -307,12 +307,12 @@ private Sign specificSubExprSign(SemExpr e) {
|
||||
div.getRightOperand().(SemFloatingPointLiteralExpr).getFloatValue() = 0
|
||||
)
|
||||
or
|
||||
exists(UnaryOperation unary | unary = e |
|
||||
result = semExprSign(unary.getOperand()).applyUnaryOp(unary.getOp())
|
||||
exists(SemUnaryExpr unary | unary = e |
|
||||
result = semExprSign(unary.getOperand()).applyUnaryOp(unary.getOpcode())
|
||||
)
|
||||
or
|
||||
exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) |
|
||||
result = s1.applyBinaryOp(s2, e.(BinaryOperation).getOp())
|
||||
result = s1.applyBinaryOp(s2, e.(SemBinaryExpr).getOpcode())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -322,9 +322,9 @@ private predicate binaryOpSigns(SemExpr e, Sign lhs, Sign rhs) {
|
||||
rhs = binaryOpRhsSign(e)
|
||||
}
|
||||
|
||||
private Sign binaryOpLhsSign(BinaryOperation e) { result = semExprSign(e.getLeftOperand()) }
|
||||
private Sign binaryOpLhsSign(SemBinaryExpr e) { result = semExprSign(e.getLeftOperand()) }
|
||||
|
||||
private Sign binaryOpRhsSign(BinaryOperation e) { result = semExprSign(e.getRightOperand()) }
|
||||
private Sign binaryOpRhsSign(SemBinaryExpr e) { result = semExprSign(e.getRightOperand()) }
|
||||
|
||||
/**
|
||||
* Dummy predicate that holds for any sign. This is added to improve readability
|
||||
@@ -357,3 +357,7 @@ predicate semStrictlyNegative(SemExpr e) {
|
||||
not semExprSign(e) = TPos() and
|
||||
not semExprSign(e) = TZero()
|
||||
}
|
||||
|
||||
module SemSignAnalysisCommonTest {
|
||||
predicate testSemSsaDefSign = semSsaDefSign/1;
|
||||
}
|
||||
|
||||
@@ -8,113 +8,6 @@ module Private {
|
||||
private import semmle.code.java.semantic.SemanticGuard
|
||||
private import semmle.code.java.semantic.SemanticSSA
|
||||
import Impl
|
||||
|
||||
/** Class to represent unary operation. */
|
||||
class UnaryOperation extends SemUnaryExpr {
|
||||
UnaryOperation() {
|
||||
expr instanceof J::PreIncExpr or
|
||||
expr instanceof J::PreDecExpr or
|
||||
expr instanceof J::MinusExpr or
|
||||
expr instanceof J::BitNotExpr
|
||||
}
|
||||
|
||||
/** Returns the operand of this expression. */
|
||||
SemExpr getOperand() { result = getExpr() }
|
||||
|
||||
/** Returns the operation representing this expression. */
|
||||
TUnarySignOperation getOp() {
|
||||
this instanceof SemPreIncExpr and result = TIncOp()
|
||||
or
|
||||
this instanceof SemPreDecExpr and result = TDecOp()
|
||||
or
|
||||
this instanceof SemMinusExpr and result = TNegOp()
|
||||
or
|
||||
this instanceof SemBitNotExpr and result = TBitNotOp()
|
||||
}
|
||||
}
|
||||
|
||||
/** Class to represent binary operation. */
|
||||
class BinaryOperation extends SemExpr {
|
||||
BinaryOperation() {
|
||||
expr instanceof J::AddExpr or
|
||||
expr instanceof J::AssignAddExpr or
|
||||
expr instanceof J::SubExpr or
|
||||
expr instanceof J::AssignSubExpr or
|
||||
expr instanceof J::MulExpr or
|
||||
expr instanceof J::AssignMulExpr or
|
||||
expr instanceof J::DivExpr or
|
||||
expr instanceof J::AssignDivExpr or
|
||||
expr instanceof J::RemExpr or
|
||||
expr instanceof J::AssignRemExpr or
|
||||
expr instanceof J::AndBitwiseExpr or
|
||||
expr instanceof J::AssignAndExpr or
|
||||
expr instanceof J::OrBitwiseExpr or
|
||||
expr instanceof J::AssignOrExpr or
|
||||
expr instanceof J::XorBitwiseExpr or
|
||||
expr instanceof J::AssignXorExpr or
|
||||
expr instanceof J::LShiftExpr or
|
||||
expr instanceof J::AssignLShiftExpr or
|
||||
expr instanceof J::RShiftExpr or
|
||||
expr instanceof J::AssignRShiftExpr or
|
||||
expr instanceof J::URShiftExpr or
|
||||
expr instanceof J::AssignURShiftExpr
|
||||
}
|
||||
|
||||
/** Returns the operation representing this expression. */
|
||||
TBinarySignOperation getOp() {
|
||||
expr instanceof J::AddExpr and result = TAddOp()
|
||||
or
|
||||
expr instanceof J::AssignAddExpr and result = TAddOp()
|
||||
or
|
||||
expr instanceof J::SubExpr and result = TSubOp()
|
||||
or
|
||||
expr instanceof J::AssignSubExpr and result = TSubOp()
|
||||
or
|
||||
expr instanceof J::MulExpr and result = TMulOp()
|
||||
or
|
||||
expr instanceof J::AssignMulExpr and result = TMulOp()
|
||||
or
|
||||
expr instanceof J::DivExpr and result = TDivOp()
|
||||
or
|
||||
expr instanceof J::AssignDivExpr and result = TDivOp()
|
||||
or
|
||||
expr instanceof J::RemExpr and result = TRemOp()
|
||||
or
|
||||
expr instanceof J::AssignRemExpr and result = TRemOp()
|
||||
or
|
||||
expr instanceof J::AndBitwiseExpr and result = TBitAndOp()
|
||||
or
|
||||
expr instanceof J::AssignAndExpr and result = TBitAndOp()
|
||||
or
|
||||
expr instanceof J::OrBitwiseExpr and result = TBitOrOp()
|
||||
or
|
||||
expr instanceof J::AssignOrExpr and result = TBitOrOp()
|
||||
or
|
||||
expr instanceof J::XorBitwiseExpr and result = TBitXorOp()
|
||||
or
|
||||
expr instanceof J::AssignXorExpr and result = TBitXorOp()
|
||||
or
|
||||
expr instanceof J::LShiftExpr and result = TLShiftOp()
|
||||
or
|
||||
expr instanceof J::AssignLShiftExpr and result = TLShiftOp()
|
||||
or
|
||||
expr instanceof J::RShiftExpr and result = TRShiftOp()
|
||||
or
|
||||
expr instanceof J::AssignRShiftExpr and result = TRShiftOp()
|
||||
or
|
||||
expr instanceof J::URShiftExpr and result = TURShiftOp()
|
||||
or
|
||||
expr instanceof J::AssignURShiftExpr and result = TURShiftOp()
|
||||
}
|
||||
|
||||
SemExpr getLeftOperand() {
|
||||
result = this.(SemBinaryExpr).getLeftOperand() or result = this.(SemAssignOp).getDest()
|
||||
}
|
||||
|
||||
SemExpr getRightOperand() {
|
||||
result = this.(SemBinaryExpr).getRightOperand() or result = this.(SemAssignOp).getRhs()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private module Impl {
|
||||
@@ -128,6 +21,7 @@ private module Impl {
|
||||
private import Sign
|
||||
private import SignAnalysisCommon
|
||||
private import semmle.code.java.semantic.SemanticExpr
|
||||
private import semmle.code.java.semantic.SemanticExprSpecific
|
||||
private import semmle.code.java.semantic.SemanticGuard
|
||||
private import semmle.code.java.semantic.SemanticSSA
|
||||
|
||||
@@ -145,6 +39,19 @@ private module Impl {
|
||||
)
|
||||
}
|
||||
|
||||
Sign languageExprSign(SemExpr e) {
|
||||
exists(VarAccess access | access = getJavaExpr(e) |
|
||||
not exists(SsaVariable v | v.getAUse() = access) and
|
||||
(
|
||||
result = fieldSign(getField(access.(FieldAccess)))
|
||||
or
|
||||
semAnySign(result) and not access instanceof FieldAccess
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
predicate ignoreExprSign(SemExpr e) { getJavaExpr(e) instanceof LocalVariableDeclExpr }
|
||||
|
||||
/**
|
||||
* Holds if `e` has type `NumericOrCharType`, but the sign of `e` is unknown.
|
||||
*/
|
||||
@@ -157,24 +64,19 @@ private module Impl {
|
||||
expr instanceof MethodAccess and expr.getType() instanceof NumericOrCharType
|
||||
or
|
||||
expr instanceof ClassInstanceExpr and expr.getType() instanceof NumericOrCharType
|
||||
or
|
||||
exists(CastExpr cast | cast = expr |
|
||||
// TODO: Stop tracking the result if the _result_ is not numeric.
|
||||
not cast.getExpr().getType() instanceof NumericOrCharType
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/** Returns the underlying variable update of the explicit SSA variable `v`. */
|
||||
SemVariableUpdate getExplicitSsaAssignment(SemSsaVariable v) {
|
||||
result = v.(SemSsaExplicitUpdate).getDefiningExpr()
|
||||
}
|
||||
|
||||
/** Returns the assignment of the variable update `def`. */
|
||||
SemExpr getExprFromSsaAssignment(SemVariableUpdate def) {
|
||||
result = def.(SemVariableAssign).getSource()
|
||||
or
|
||||
exists(SemAssignOp a | a = def and result = a)
|
||||
}
|
||||
|
||||
/** Holds if `def` can have any sign. */
|
||||
predicate explicitSsaDefWithAnySign(SemVariableUpdate def) {
|
||||
exists(EnhancedForStmt for | def = getSemanticExpr(for.getVariable()))
|
||||
predicate explicitSsaDefWithAnySign(SemSsaExplicitUpdate def) {
|
||||
exists(EnhancedForStmt for |
|
||||
getJavaSsaVariable(def).(SsaExplicitUpdate).getDefiningExpr() = for.getVariable()
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the variable underlying the implicit SSA variable `v`. */
|
||||
@@ -214,7 +116,7 @@ private module Impl {
|
||||
/** Returned an expression that is assigned to `f`. */
|
||||
private SemExpr getAssignedValueToField(Field f) {
|
||||
result = getSemanticExpr(f.getAnAssignedValue()) or
|
||||
result = any(SemAssignOp a | a.getDest() = getSemanticExpr(f.getAnAccess()))
|
||||
result = getSemanticExpr(any(AssignOp a | a.getDest() = f.getAnAccess()))
|
||||
}
|
||||
|
||||
/** Holds if `f` can have any sign. */
|
||||
@@ -252,17 +154,15 @@ private module Impl {
|
||||
|
||||
/** Returns a sub expression of `e` for expression types where the sign depends on the child. */
|
||||
SemExpr getASubExprWithSameSign(SemExpr e) {
|
||||
result = e.(SemAssignExpr).getRhs() or
|
||||
result = e.(SemPlusExpr).getExpr() or
|
||||
result = e.(SemPostIncExpr).getExpr() or
|
||||
result = e.(SemPostDecExpr).getExpr() or
|
||||
result = e.(SemCopyValueExpr).getOperand() or
|
||||
result = getSemanticExpr(getJavaExpr(e).(ChooseExpr).getAResultExpr()) or
|
||||
result = e.(SemCastExpr).getExpr()
|
||||
result = e.(SemConvertExpr).getOperand() or
|
||||
result = getSemanticExpr(getJavaExpr(e).(CastExpr).getExpr()) // REVIEW: Should only apply to trackable operations
|
||||
}
|
||||
|
||||
private Field getField(FieldAccess fa) { result = fa.getField() }
|
||||
|
||||
Sign getVarAccessSign(SemVarAccess access) {
|
||||
Sign getLoadSign(SemLoadExpr access) {
|
||||
result = fieldSign(getField(getJavaExpr(access).(FieldAccess)))
|
||||
or
|
||||
semAnySign(result) and not getJavaExpr(access) instanceof FieldAccess
|
||||
|
||||
@@ -0,0 +1,2 @@
|
||||
diff_exprSign
|
||||
diff_ssaDefSign
|
||||
|
||||
@@ -1,18 +1,34 @@
|
||||
import java
|
||||
import semmle.code.java.dataflow.SignAnalysis
|
||||
import semmle.code.java.semantic.analysis.SignAnalysisCommon
|
||||
import semmle.code.java.semantic.SemanticCFG
|
||||
import semmle.code.java.semantic.SemanticExpr
|
||||
import semmle.code.java.semantic.SemanticExprSpecific
|
||||
import semmle.code.java.semantic.SemanticSSA
|
||||
import semmle.code.java.semantic.SemanticType
|
||||
import semmle.code.java.dataflow.SSA
|
||||
import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||
import SignAnalysisCommonTest
|
||||
import SemSignAnalysisCommonTest
|
||||
|
||||
string getSemanticSign(Expr e) {
|
||||
result = concat(string s | s = semExprSign(getSemanticExpr(e)).toString() | s, "")
|
||||
predicate interestingLocation(Location loc) {
|
||||
// loc.getFile().getBaseName() = "UnsignedLongs.java" and
|
||||
// loc.getStartLine() in [470 .. 477] and
|
||||
any()
|
||||
}
|
||||
|
||||
string getASTSign(Expr e) { result = concat(string s | s = exprSign(e).toString() | s, "") }
|
||||
query predicate diff_exprSign(SemExpr e, string astSign, string semSign) {
|
||||
getJavaExpr(e).getEnclosingCallable().fromSource() and
|
||||
interestingLocation(e.getLocation()) and
|
||||
semSign = concat(semExprSign(e).toString(), "") and
|
||||
astSign = concat(exprSign(getJavaExpr(e)).toString(), "") and
|
||||
astSign != semSign
|
||||
}
|
||||
|
||||
from Expr e, string semSign, string astSign
|
||||
where
|
||||
e.getEnclosingCallable().fromSource() and
|
||||
semSign = getSemanticSign(e) and
|
||||
astSign = getASTSign(e) and
|
||||
semSign != astSign
|
||||
select e, "AST sign was '" + astSign + "', but semantic sign was '" + semSign + "'."
|
||||
query predicate diff_ssaDefSign(SemSsaVariable v, string astSign, string semSign) {
|
||||
getJavaBasicBlock(v.getBasicBlock()).getEnclosingCallable().fromSource() and
|
||||
interestingLocation(v.getBasicBlock().getLocation()) and
|
||||
semSign = concat(testSemSsaDefSign(v).toString(), "") and
|
||||
astSign = concat(testSsaDefSign(getJavaSsaVariable(v)).toString(), "") and
|
||||
astSign != semSign
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user