Sync Bound between C# and Java

This commit is contained in:
Tamas Vajk
2020-09-24 13:02:10 +02:00
parent 40a7f5aa1f
commit d2d8d009eb
6 changed files with 134 additions and 6 deletions

View File

@@ -2,15 +2,13 @@
* Provides classes for representing abstract bounds for use in, for example, range analysis.
*/
import java
private import SSA
private import RangeUtils
private import internal.rangeanalysis.BoundSpecific
private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) {
e.(FieldRead).getField() instanceof ArrayLengthField and
interestingExprBound(e) and
not exists(SsaVariable v | e = v.getAUse())
}
@@ -75,6 +73,6 @@ class ExprBound extends Bound, TBoundExpr {
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
getExpr().hasLocationInfo(path, sl, sc, el, ec)
getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
}

View File

@@ -0,0 +1,20 @@
/**
* Provides Java-specific definitions for bounds.
*/
private import java as J
private import semmle.code.java.dataflow.SSA as Ssa
private import semmle.code.java.dataflow.RangeUtils as RU
class SsaVariable = Ssa::SsaVariable;
class Expr = J::Expr;
class IntegralType = J::IntegralType;
class ConstantIntegerExpr = RU::ConstantIntegerExpr;
/** Holds if `e` is a bound expression and it is not an SSA variable read. */
predicate interestingExprBound(Expr e) {
e.(J::FieldRead).getField() instanceof J::ArrayLengthField
}