C++: fix missing bounds in new range analysis

This commit is contained in:
Robert Marsh
2023-03-10 14:23:08 -05:00
parent b941d54f1f
commit d4e3f7f738
4 changed files with 41 additions and 1 deletions

View File

@@ -5,6 +5,7 @@
private import SemanticExpr
private import SemanticExprSpecific::SemanticExprConfig as Specific
private import SemanticSSA
private import semmle.code.cpp.Location // TODO: SemLocation?
/**
* A valid base for an expression bound.
@@ -14,6 +15,8 @@ private import SemanticSSA
class SemBound instanceof Specific::Bound {
final string toString() { result = super.toString() }
final Location getLocation() {result = super.getLocation() }
final SemExpr getExpr(int delta) { result = Specific::getBoundExpr(this, delta) }
}

View File

@@ -0,0 +1,29 @@
private import RangeAnalysisStage
module IntDelta implements DeltaSig {
class Delta = int;
bindingset[d]
bindingset[result]
float toFloat(Delta d) { result = d }
bindingset[d]
bindingset[result]
int toInt(Delta d) { result = d }
bindingset[n]
bindingset[result]
Delta fromInt(int n) { result = n }
bindingset[f]
Delta fromFloat(float f) {
result =
min(float diff, float res |
diff = (res - f) and res = f.ceil()
or
diff = (f - res) and res = f.floor()
|
res order by diff
)
}
}

View File

@@ -4,6 +4,7 @@ private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
private import RangeUtils
private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
private import semmle.code.cpp.ir.IR as IR
private import semmle.code.cpp.Location // TODO: SemLocation?
private module ConstantBounds implements BoundSig<FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
@@ -15,6 +16,8 @@ private module ConstantBounds implements BoundSig<FloatDelta> {
string toString() { result = super.toString() }
Location getLocation() { result = super.getLocation() }
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
}
@@ -26,9 +29,11 @@ private module ConstantBounds implements BoundSig<FloatDelta> {
}
private module RelativeBounds implements BoundSig<FloatDelta> {
class SemBound instanceof SemanticBound::SemSsaBound {
class SemBound instanceof SemanticBound::SemBound {
string toString() { result = super.toString() }
Location getLocation() { result = super.getLocation() }
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
}

View File

@@ -73,6 +73,7 @@ import experimental.semmle.code.cpp.semantic.SemanticCFG
import experimental.semmle.code.cpp.semantic.SemanticType
import experimental.semmle.code.cpp.semantic.SemanticOpcode
private import ConstantAnalysis
private import semmle.code.cpp.Location
/**
* Holds if `typ` is a small integral type with the given lower and upper bounds.
@@ -228,6 +229,8 @@ signature module UtilSig<DeltaSig DeltaParam> {
signature module BoundSig<DeltaSig D> {
class SemBound {
string toString();
Location getLocation();
SemExpr getExpr(D::Delta delta);
}