|
18 | 18 |
|
19 | 19 | import cpp |
20 | 20 | import semmle.code.cpp.controlflow.SSA |
| 21 | +import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis |
| 22 | +import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils |
21 | 23 |
|
22 | 24 | /** |
23 | 25 | * Holds if `e` is either: |
@@ -64,6 +66,110 @@ int getEffectiveMulOperands(MulExpr me) { |
64 | 66 | ) |
65 | 67 | } |
66 | 68 |
|
| 69 | +/** |
| 70 | + * As SimpleRangeAnalysis does not support reasoning about multiplication |
| 71 | + * we create a tiny abstract interpreter for handling multiplication, which |
| 72 | + * we invoke only after weeding out of all of trivial cases that we do |
| 73 | + * not care about. By default, the maximum and minimum values are computed |
| 74 | + * using SimpleRangeAnalysis. |
| 75 | + */ |
| 76 | +class AnalyzableExpr extends Expr { |
| 77 | + float maxValue() { result = upperBound(this.getFullyConverted()) } |
| 78 | + |
| 79 | + float minValue() { result = lowerBound(this.getFullyConverted()) } |
| 80 | +} |
| 81 | + |
| 82 | +class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr { |
| 83 | + override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() } |
| 84 | + |
| 85 | + override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() } |
| 86 | +} |
| 87 | + |
| 88 | +class MulAnalyzableExpr extends AnalyzableExpr, MulExpr { |
| 89 | + override float maxValue() { |
| 90 | + exists(float x1, float y1, float x2, float y2 | |
| 91 | + x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and |
| 92 | + x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and |
| 93 | + y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and |
| 94 | + y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and |
| 95 | + result = (x1 * y1).maximum(x1 * y2).maximum(x2 * y1).maximum(x2 * y2) |
| 96 | + ) |
| 97 | + } |
| 98 | + |
| 99 | + override float minValue() { |
| 100 | + exists(float x1, float x2, float y1, float y2 | |
| 101 | + x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and |
| 102 | + x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and |
| 103 | + y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and |
| 104 | + y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and |
| 105 | + result = (x1 * y1).minimum(x1 * y2).minimum(x2 * y1).minimum(x2 * y2) |
| 106 | + ) |
| 107 | + } |
| 108 | +} |
| 109 | + |
| 110 | +class AddAnalyzableExpr extends AnalyzableExpr, AddExpr { |
| 111 | + override float maxValue() { |
| 112 | + result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() + |
| 113 | + this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() |
| 114 | + } |
| 115 | + |
| 116 | + override float minValue() { |
| 117 | + result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() + |
| 118 | + this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() |
| 119 | + } |
| 120 | +} |
| 121 | + |
| 122 | +class SubAnalyzableExpr extends AnalyzableExpr, SubExpr { |
| 123 | + override float maxValue() { |
| 124 | + result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() - |
| 125 | + this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() |
| 126 | + } |
| 127 | + |
| 128 | + override float minValue() { |
| 129 | + result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() - |
| 130 | + this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() |
| 131 | + } |
| 132 | +} |
| 133 | + |
| 134 | +class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess { |
| 135 | + VarAnalyzableExpr() { this.getTarget() instanceof StackVariable } |
| 136 | + |
| 137 | + override float maxValue() { |
| 138 | + exists(SsaDefinition def, Variable v | |
| 139 | + def.getAUse(v) = this and |
| 140 | + // if there is a defining expression, use that for |
| 141 | + // computing the maximum value. Otherwise, assign the |
| 142 | + // variable the largest possible value it can hold |
| 143 | + if exists(def.getDefiningValue(v)) |
| 144 | + then result = def.getDefiningValue(v).(AnalyzableExpr).maxValue() |
| 145 | + else result = upperBound(this) |
| 146 | + ) |
| 147 | + } |
| 148 | + |
| 149 | + override float minValue() { |
| 150 | + exists(SsaDefinition def, Variable v | |
| 151 | + def.getAUse(v) = this and |
| 152 | + if exists(def.getDefiningValue(v)) |
| 153 | + then result = def.getDefiningValue(v).(AnalyzableExpr).minValue() |
| 154 | + else result = lowerBound(this) |
| 155 | + ) |
| 156 | + } |
| 157 | +} |
| 158 | + |
| 159 | +/** |
| 160 | + * Holds if `t` is not an instance of `IntegralType`, |
| 161 | + * or if `me` cannot be proven to not overflow |
| 162 | + */ |
| 163 | +predicate overflows(MulExpr me, Type t) { |
| 164 | + t instanceof IntegralType |
| 165 | + implies |
| 166 | + ( |
| 167 | + me.(MulAnalyzableExpr).maxValue() > exprMaxVal(me) |
| 168 | + or |
| 169 | + me.(MulAnalyzableExpr).minValue() < exprMinVal(me) |
| 170 | + ) |
| 171 | +} |
| 172 | + |
67 | 173 | from MulExpr me, Type t1, Type t2 |
68 | 174 | where |
69 | 175 | t1 = me.getType().getUnderlyingType() and |
@@ -101,7 +207,11 @@ where |
101 | 207 | e = other.(BinaryOperation).getAnOperand*() |
102 | 208 | ) and |
103 | 209 | e.(Literal).getType().getSize() = t2.getSize() |
104 | | - ) |
| 210 | + ) and |
| 211 | + // only report if we cannot prove that the result of the |
| 212 | + // multiplication will be less (resp. greater) than the |
| 213 | + // maximum (resp. minimum) number we can compute. |
| 214 | + overflows(me, t1) |
105 | 215 | select me, |
106 | 216 | "Multiplication result may overflow '" + me.getType().toString() + "' before it is converted to '" |
107 | 217 | + me.getFullyConverted().getType().toString() + "'." |
0 commit comments