C++: Fix a couple of range analysis issues:

1. The new query is expecting pointer arithmetic operations to generate
range-analysis bounds, but this wasn't true on main.
2. The bounds generated by `boundFlowCond` was incorrectly inferred as
non-strict when comparing a pointers (unlike when comparing values of
integral types). This gave FPs in the new query.

This also fixes a couple of missing results in existing queries that
use the new range-analysis library.
This commit is contained in:
Mathias Vorreiter Pedersen
2022-09-15 15:55:16 +01:00
parent d981f898e4
commit b8a5aa5d85
8 changed files with 43 additions and 30 deletions

View File

@@ -28,6 +28,10 @@ private newtype TBound =
i.(LoadInstruction).getSourceAddress() instanceof FieldAddressInstruction
or
i.getAUse() instanceof ArgumentOperand
or
i instanceof PointerArithmeticInstruction
or
i.getAUse() instanceof AddressOperand
)
}

View File

@@ -178,11 +178,11 @@ class SemRelationalExpr extends SemBinaryExpr {
}
class SemAddExpr extends SemBinaryExpr {
SemAddExpr() { opcode instanceof Opcode::Add }
SemAddExpr() { opcode instanceof Opcode::Add or opcode instanceof Opcode::PointerAdd }
}
class SemSubExpr extends SemBinaryExpr {
SemSubExpr() { opcode instanceof Opcode::Sub }
SemSubExpr() { opcode instanceof Opcode::Sub or opcode instanceof Opcode::PointerSub }
}
class SemMulExpr extends SemBinaryExpr {

View File

@@ -65,10 +65,18 @@ module Opcode {
override string toString() { result = "Add" }
}
class PointerAdd extends Opcode, TPointerAdd {
override string toString() { result = "PointerAdd" }
}
class Sub extends Opcode, TSub {
override string toString() { result = "Sub" }
}
class PointerSub extends Opcode, TPointerSub {
override string toString() { result = "PointerSub" }
}
class Mul extends Opcode, TMul {
override string toString() { result = "Mul" }
}

View File

@@ -223,7 +223,9 @@ private SemGuard boundFlowCond(
else resultIsStrict = testIsTrue.booleanNot()
) and
(
if getTrackedTypeForSsaVariable(v) instanceof SemIntegerType
if
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
getTrackedTypeForSsaVariable(v) instanceof SemAddressType
then
upper = true and strengthen = -1
or