Skip to content

Commit d66578e

Browse files
jbjjbj
committed
C++: Add IntegerPartial, use in ConstantAnalysis
This adds `IntegerPartial.qll`, which is similar to `IntegerConstant.qll` except that it contains partial functions on integers instead of total functions on optional integers. This speeds up the constant analysis so it takes 6.5s instead of 10.3s on comdb2.
1 parent 06ae0c4 commit d66578e

File tree

6 files changed

+148
-16
lines changed

6 files changed

+148
-16
lines changed

‎cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/constant/ConstantAnalysis.qll‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
private import internal.ConstantAnalysisInternal
2-
import semmle.code.cpp.ir.internal.IntegerConstant
2+
private import semmle.code.cpp.ir.internal.IntegerPartial
33
private import IR
44

55
language[monotonicAggregates]
6-
IntValue getConstantValue(Instruction instr) {
6+
int getConstantValue(Instruction instr) {
77
result = instr.(IntegerConstantInstruction).getValue().toInt() or
8-
exists(BinaryInstruction binInstr, IntValue left, IntValue right |
8+
exists(BinaryInstruction binInstr, int left, int right |
99
binInstr = instr and
1010
left = getConstantValue(binInstr.getLeftOperand()) and
1111
right = getConstantValue(binInstr.getRightOperand()) and
@@ -22,7 +22,7 @@ IntValue getConstantValue(Instruction instr) {
2222
binInstr instanceof CompareGEInstruction and result = compareGE(left, right)
2323
)
2424
) or
25-
exists(UnaryInstruction unaryInstr, IntValue src |
25+
exists(UnaryInstruction unaryInstr, int src |
2626
unaryInstr = instr and
2727
src = getConstantValue(unaryInstr.getOperand()) and
2828
(

‎cpp/ql/src/semmle/code/cpp/ir/implementation/raw/constant/ConstantAnalysis.qll‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
private import internal.ConstantAnalysisInternal
2-
import semmle.code.cpp.ir.internal.IntegerConstant
2+
private import semmle.code.cpp.ir.internal.IntegerPartial
33
private import IR
44

55
language[monotonicAggregates]
6-
IntValue getConstantValue(Instruction instr) {
6+
int getConstantValue(Instruction instr) {
77
result = instr.(IntegerConstantInstruction).getValue().toInt() or
8-
exists(BinaryInstruction binInstr, IntValue left, IntValue right |
8+
exists(BinaryInstruction binInstr, int left, int right |
99
binInstr = instr and
1010
left = getConstantValue(binInstr.getLeftOperand()) and
1111
right = getConstantValue(binInstr.getRightOperand()) and
@@ -22,7 +22,7 @@ IntValue getConstantValue(Instruction instr) {
2222
binInstr instanceof CompareGEInstruction and result = compareGE(left, right)
2323
)
2424
) or
25-
exists(UnaryInstruction unaryInstr, IntValue src |
25+
exists(UnaryInstruction unaryInstr, int src |
2626
unaryInstr = instr and
2727
src = getConstantValue(unaryInstr.getOperand()) and
2828
(

‎cpp/ql/src/semmle/code/cpp/ir/implementation/raw/internal/reachability/ReachableBlock.qll‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11
private import ReachableBlockInternal
2-
private import semmle.code.cpp.ir.internal.IntegerConstant
32
private import IR
43
private import ConstantAnalysis
54

65
predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
76
exists(int conditionValue |
8-
conditionValue = getValue(getConstantValue(instr.(ConditionalBranchInstruction).getCondition())) and
7+
conditionValue = getConstantValue(instr.(ConditionalBranchInstruction).getCondition()) and
98
if conditionValue = 0 then
109
kind instanceof TrueEdge
1110
else

‎cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/constant/ConstantAnalysis.qll‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
private import internal.ConstantAnalysisInternal
2-
import semmle.code.cpp.ir.internal.IntegerConstant
2+
private import semmle.code.cpp.ir.internal.IntegerPartial
33
private import IR
44

55
language[monotonicAggregates]
6-
IntValue getConstantValue(Instruction instr) {
6+
int getConstantValue(Instruction instr) {
77
result = instr.(IntegerConstantInstruction).getValue().toInt() or
8-
exists(BinaryInstruction binInstr, IntValue left, IntValue right |
8+
exists(BinaryInstruction binInstr, int left, int right |
99
binInstr = instr and
1010
left = getConstantValue(binInstr.getLeftOperand()) and
1111
right = getConstantValue(binInstr.getRightOperand()) and
@@ -22,7 +22,7 @@ IntValue getConstantValue(Instruction instr) {
2222
binInstr instanceof CompareGEInstruction and result = compareGE(left, right)
2323
)
2424
) or
25-
exists(UnaryInstruction unaryInstr, IntValue src |
25+
exists(UnaryInstruction unaryInstr, int src |
2626
unaryInstr = instr and
2727
src = getConstantValue(unaryInstr.getOperand()) and
2828
(

‎cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlock.qll‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11
private import ReachableBlockInternal
2-
private import semmle.code.cpp.ir.internal.IntegerConstant
32
private import IR
43
private import ConstantAnalysis
54

65
predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
76
exists(int conditionValue |
8-
conditionValue = getValue(getConstantValue(instr.(ConditionalBranchInstruction).getCondition())) and
7+
conditionValue = getConstantValue(instr.(ConditionalBranchInstruction).getCondition()) and
98
if conditionValue = 0 then
109
kind instanceof TrueEdge
1110
else

‎cpp/ql/src/semmle/code/cpp/ir/internal/IntegerPartial.qll‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
/**
2+
* Provides basic arithmetic operations that have no result if their result
3+
* would overflow a 32-bit two's complement integer.
4+
*/
5+
6+
/**
7+
* Gets the value of the maximum representable integer.
8+
*/
9+
int maxValue() {
10+
result = 2147483647
11+
}
12+
13+
/**
14+
* Gets the value of the minimum representable integer.
15+
*/
16+
int minValue() {
17+
result = -2147483648
18+
}
19+
20+
/**
21+
* Holds if the value `f` is within the range of representable integers.
22+
*/
23+
pragma[inline]
24+
bindingset[f]
25+
private predicate isRepresentable(float f) {
26+
(f >= minValue()) and (f <= maxValue())
27+
}
28+
29+
/**
30+
* Returns `a + b`. If the addition overflows, there is no result.
31+
*/
32+
bindingset[a, b]
33+
int add(int a, int b) {
34+
isRepresentable((float)a + (float)b) and
35+
result = a + b
36+
}
37+
38+
/**
39+
* Returns `a - b`. If the subtraction overflows, there is no result.
40+
*/
41+
bindingset[a, b]
42+
int sub(int a, int b) {
43+
isRepresentable((float)a - (float)b) and
44+
result = a - b
45+
}
46+
47+
/**
48+
* Returns `a * b`. If the multiplication overflows, there is no result. If
49+
* either input is not given, and the other input is non-zero, there is no
50+
* result.
51+
*/
52+
bindingset[a, b]
53+
int mul(int a, int b) {
54+
a = 0 and
55+
result = 0
56+
or
57+
b = 0 and
58+
result = 0
59+
or
60+
isRepresentable((float)a * (float)b) and
61+
result = a * b
62+
}
63+
64+
/**
65+
* Returns `a / b`. If the division overflows, there is no result.
66+
*/
67+
bindingset[a, b]
68+
int div(int a, int b) {
69+
b != 0 and (a != minValue() or b != -1) and
70+
result = a / b
71+
}
72+
73+
/** Returns `a == b`. */
74+
bindingset[a, b]
75+
int compareEQ(int a, int b) {
76+
if a = b then
77+
result = 1
78+
else
79+
result = 0
80+
}
81+
82+
/** Returns `a != b`. */
83+
bindingset[a, b]
84+
int compareNE(int a, int b) {
85+
if a != b then
86+
result = 1
87+
else
88+
result = 0
89+
}
90+
91+
/** Returns `a < b`. */
92+
bindingset[a, b]
93+
int compareLT(int a, int b) {
94+
if a < b then
95+
result = 1
96+
else
97+
result = 0
98+
}
99+
100+
/** Returns `a > b`. */
101+
bindingset[a, b]
102+
int compareGT(int a, int b) {
103+
if a > b then
104+
result = 1
105+
else
106+
result = 0
107+
}
108+
109+
/** Returns `a <= b`. */
110+
bindingset[a, b]
111+
int compareLE(int a, int b) {
112+
if a <= b then
113+
result = 1
114+
else
115+
result = 0
116+
}
117+
118+
/** Returns `a >= b`. */
119+
bindingset[a, b]
120+
int compareGE(int a, int b) {
121+
if a >= b then
122+
result = 1
123+
else
124+
result = 0
125+
}
126+
127+
/**
128+
* Returns `-a`. If the negation would overflow, there is no result.
129+
*/
130+
bindingset[a]
131+
int neg(int a) {
132+
a != minValue() and
133+
result = -a
134+
}

0 commit comments

Comments
 (0)