Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Commit 1bc6f88

Browse filesBrowse files
MathiasVPMathiasVP
authored
Merge pull request #14992 from jketema/ir-guards-replacement
C++: replace Guards with IRGuards
2 parents c1cc441 + edf1786 commit 1bc6f88
Copy full SHA for 1bc6f88

File tree

Expand file treeCollapse file tree

6 files changed

+17
-389
lines changed
Filter options
Expand file treeCollapse file tree

6 files changed

+17
-389
lines changed

‎cpp/ql/lib/change-notes/2022-11-21-ir-guards-replacement.md

Copy file name to clipboard
+4Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: minorAnalysis
3+
---
4+
* The `Guards` library has been replaced with the API-compatible `IRGuards` implementation, which has better precision in some cases.

‎cpp/ql/lib/semmle/code/cpp/controlflow/Guards.qll

Copy file name to clipboardExpand all lines: cpp/ql/lib/semmle/code/cpp/controlflow/Guards.qll
+1-365Lines changed: 1 addition & 365 deletions
Original file line numberDiff line numberDiff line change
@@ -7,371 +7,7 @@ import cpp
77
import semmle.code.cpp.controlflow.BasicBlocks
88
import semmle.code.cpp.controlflow.SSA
99
import semmle.code.cpp.controlflow.Dominance
10-
11-
/**
12-
* A Boolean condition that guards one or more basic blocks. This includes
13-
* operands of logical operators but not switch statements.
14-
*/
15-
class GuardCondition extends Expr {
16-
GuardCondition() { is_condition(this) }
17-
18-
/**
19-
* Holds if this condition controls `block`, meaning that `block` is only
20-
* entered if the value of this condition is `testIsTrue`.
21-
*
22-
* Illustration:
23-
*
24-
* ```
25-
* [ (testIsTrue) ]
26-
* [ this ----------------succ ---- controlled ]
27-
* [ | | ]
28-
* [ (testIsFalse) | ------ ... ]
29-
* [ other ]
30-
* ```
31-
*
32-
* The predicate holds if all paths to `controlled` go via the `testIsTrue`
33-
* edge of the control-flow graph. In other words, the `testIsTrue` edge
34-
* must dominate `controlled`. This means that `controlled` must be
35-
* dominated by both `this` and `succ` (the target of the `testIsTrue`
36-
* edge). It also means that any other edge into `succ` must be a back-edge
37-
* from a node which is dominated by `succ`.
38-
*
39-
* The short-circuit boolean operations have slightly surprising behavior
40-
* here: because the operation itself only dominates one branch (due to
41-
* being short-circuited) then it will only control blocks dominated by the
42-
* true (for `&&`) or false (for `||`) branch.
43-
*/
44-
cached
45-
predicate controls(BasicBlock controlled, boolean testIsTrue) {
46-
// This condition must determine the flow of control; that is, this
47-
// node must be a top-level condition.
48-
this.controlsBlock(controlled, testIsTrue)
49-
or
50-
exists(BinaryLogicalOperation binop, GuardCondition lhs, GuardCondition rhs |
51-
this = binop and
52-
lhs = binop.getLeftOperand() and
53-
rhs = binop.getRightOperand() and
54-
lhs.controls(controlled, testIsTrue) and
55-
rhs.controls(controlled, testIsTrue)
56-
)
57-
or
58-
exists(GuardCondition ne, GuardCondition operand |
59-
this = operand and
60-
operand = ne.(NotExpr).getOperand() and
61-
ne.controls(controlled, testIsTrue.booleanNot())
62-
)
63-
}
64-
65-
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
66-
cached
67-
predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
68-
compares_lt(this, left, right, k, isLessThan, testIsTrue)
69-
}
70-
71-
/**
72-
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
73-
* If `isLessThan = false` then this implies `left >= right + k`.
74-
*/
75-
cached
76-
predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
77-
exists(boolean testIsTrue |
78-
compares_lt(this, left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
79-
)
80-
}
81-
82-
/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
83-
cached
84-
predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
85-
compares_eq(this, left, right, k, areEqual, testIsTrue)
86-
}
87-
88-
/**
89-
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
90-
* If `areEqual = false` then this implies `left != right + k`.
91-
*/
92-
cached
93-
predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) {
94-
exists(boolean testIsTrue |
95-
compares_eq(this, left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
96-
)
97-
}
98-
99-
/**
100-
* Holds if this condition controls `block`, meaning that `block` is only
101-
* entered if the value of this condition is `testIsTrue`. This helper
102-
* predicate does not necessarily hold for binary logical operations like
103-
* `&&` and `||`. See the detailed explanation on predicate `controls`.
104-
*/
105-
private predicate controlsBlock(BasicBlock controlled, boolean testIsTrue) {
106-
exists(BasicBlock thisblock | thisblock.contains(this) |
107-
exists(BasicBlock succ |
108-
testIsTrue = true and succ = this.getATrueSuccessor()
109-
or
110-
testIsTrue = false and succ = this.getAFalseSuccessor()
111-
|
112-
bbDominates(succ, controlled) and
113-
forall(BasicBlock pred | pred.getASuccessor() = succ |
114-
pred = thisblock or bbDominates(succ, pred) or not reachable(pred)
115-
)
116-
)
117-
)
118-
}
119-
}
120-
121-
private predicate is_condition(Expr guard) {
122-
guard.isCondition()
123-
or
124-
is_condition(guard.(BinaryLogicalOperation).getAnOperand())
125-
or
126-
exists(NotExpr cond | is_condition(cond) and cond.getOperand() = guard)
127-
}
128-
129-
/*
130-
* Simplification of equality expressions:
131-
* Simplify conditions in the source to the canonical form l op r + k.
132-
*/
133-
134-
/**
135-
* Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`.
136-
*
137-
* Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
138-
*/
139-
private predicate compares_eq(
140-
Expr test, Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue
141-
) {
142-
/* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
143-
exists(boolean eq | simple_comparison_eq(test, left, right, k, eq) |
144-
areEqual = true and testIsTrue = eq
145-
or
146-
areEqual = false and testIsTrue = eq.booleanNot()
147-
)
148-
or
149-
logical_comparison_eq(test, left, right, k, areEqual, testIsTrue)
150-
or
151-
/* a == b + k => b == a - k */
152-
exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, testIsTrue))
153-
or
154-
complex_eq(test, left, right, k, areEqual, testIsTrue)
155-
or
156-
/* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
157-
exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
158-
compares_eq(test.(NotExpr).getOperand(), left, right, k, areEqual, isFalse)
159-
)
160-
}
161-
162-
/**
163-
* If `test => part` and `part => left == right + k` then `test => left == right + k`.
164-
* Similarly for the case where `test` is false.
165-
*/
166-
private predicate logical_comparison_eq(
167-
BinaryLogicalOperation test, Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue
168-
) {
169-
exists(boolean partIsTrue, Expr part | test.impliesValue(part, partIsTrue, testIsTrue) |
170-
compares_eq(part, left, right, k, areEqual, partIsTrue)
171-
)
172-
}
173-
174-
/** Rearrange various simple comparisons into `left == right + k` form. */
175-
private predicate simple_comparison_eq(
176-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean areEqual
177-
) {
178-
left = cmp.getLeftOperand() and
179-
cmp.getOperator() = "==" and
180-
right = cmp.getRightOperand() and
181-
k = 0 and
182-
areEqual = true
183-
or
184-
left = cmp.getLeftOperand() and
185-
cmp.getOperator() = "!=" and
186-
right = cmp.getRightOperand() and
187-
k = 0 and
188-
areEqual = false
189-
}
190-
191-
private predicate complex_eq(
192-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue
193-
) {
194-
sub_eq(cmp, left, right, k, areEqual, testIsTrue)
195-
or
196-
add_eq(cmp, left, right, k, areEqual, testIsTrue)
197-
}
198-
199-
// left - x == right + c => left == right + (c+x)
200-
// left == (right - x) + c => left == right + (c-x)
201-
private predicate sub_eq(
202-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue
203-
) {
204-
exists(SubExpr lhs, int c, int x |
205-
compares_eq(cmp, lhs, right, c, areEqual, testIsTrue) and
206-
left = lhs.getLeftOperand() and
207-
x = int_value(lhs.getRightOperand()) and
208-
k = c + x
209-
)
210-
or
211-
exists(SubExpr rhs, int c, int x |
212-
compares_eq(cmp, left, rhs, c, areEqual, testIsTrue) and
213-
right = rhs.getLeftOperand() and
214-
x = int_value(rhs.getRightOperand()) and
215-
k = c - x
216-
)
217-
}
218-
219-
// left + x == right + c => left == right + (c-x)
220-
// left == (right + x) + c => left == right + (c+x)
221-
private predicate add_eq(
222-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue
223-
) {
224-
exists(AddExpr lhs, int c, int x |
225-
compares_eq(cmp, lhs, right, c, areEqual, testIsTrue) and
226-
(
227-
left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand())
228-
or
229-
left = lhs.getRightOperand() and x = int_value(lhs.getLeftOperand())
230-
) and
231-
k = c - x
232-
)
233-
or
234-
exists(AddExpr rhs, int c, int x |
235-
compares_eq(cmp, left, rhs, c, areEqual, testIsTrue) and
236-
(
237-
right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand())
238-
or
239-
right = rhs.getRightOperand() and x = int_value(rhs.getLeftOperand())
240-
) and
241-
k = c + x
242-
)
243-
}
244-
245-
/*
246-
* Simplification of inequality expressions:
247-
* Simplify conditions in the source to the canonical form l < r + k.
248-
*/
249-
250-
/** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
251-
private predicate compares_lt(
252-
Expr test, Expr left, Expr right, int k, boolean isLt, boolean testIsTrue
253-
) {
254-
/* In the simple case, the test is the comparison, so isLt = testIsTrue */
255-
simple_comparison_lt(test, left, right, k) and isLt = true and testIsTrue = true
256-
or
257-
simple_comparison_lt(test, left, right, k) and isLt = false and testIsTrue = false
258-
or
259-
logical_comparison_lt(test, left, right, k, isLt, testIsTrue)
260-
or
261-
complex_lt(test, left, right, k, isLt, testIsTrue)
262-
or
263-
/* (not (left < right + k)) => (left >= right + k) */
264-
exists(boolean isGe | isLt = isGe.booleanNot() |
265-
compares_ge(test, left, right, k, isGe, testIsTrue)
266-
)
267-
or
268-
/* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
269-
exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
270-
compares_lt(test.(NotExpr).getOperand(), left, right, k, isLt, isFalse)
271-
)
272-
}
273-
274-
/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
275-
private predicate compares_ge(
276-
Expr test, Expr left, Expr right, int k, boolean isGe, boolean testIsTrue
277-
) {
278-
exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, testIsTrue))
279-
}
280-
281-
/**
282-
* If `test => part` and `part => left < right + k` then `test => left < right + k`.
283-
* Similarly for the case where `test` evaluates false.
284-
*/
285-
private predicate logical_comparison_lt(
286-
BinaryLogicalOperation test, Expr left, Expr right, int k, boolean isLt, boolean testIsTrue
287-
) {
288-
exists(boolean partIsTrue, Expr part | test.impliesValue(part, partIsTrue, testIsTrue) |
289-
compares_lt(part, left, right, k, isLt, partIsTrue)
290-
)
291-
}
292-
293-
/** Rearrange various simple comparisons into `left < right + k` form. */
294-
private predicate simple_comparison_lt(ComparisonOperation cmp, Expr left, Expr right, int k) {
295-
left = cmp.getLeftOperand() and
296-
cmp.getOperator() = "<" and
297-
right = cmp.getRightOperand() and
298-
k = 0
299-
or
300-
left = cmp.getLeftOperand() and
301-
cmp.getOperator() = "<=" and
302-
right = cmp.getRightOperand() and
303-
k = 1
304-
or
305-
right = cmp.getLeftOperand() and
306-
cmp.getOperator() = ">" and
307-
left = cmp.getRightOperand() and
308-
k = 0
309-
or
310-
right = cmp.getLeftOperand() and
311-
cmp.getOperator() = ">=" and
312-
left = cmp.getRightOperand() and
313-
k = 1
314-
}
315-
316-
private predicate complex_lt(
317-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean isLt, boolean testIsTrue
318-
) {
319-
sub_lt(cmp, left, right, k, isLt, testIsTrue)
320-
or
321-
add_lt(cmp, left, right, k, isLt, testIsTrue)
322-
}
323-
324-
// left - x < right + c => left < right + (c+x)
325-
// left < (right - x) + c => left < right + (c-x)
326-
private predicate sub_lt(
327-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean isLt, boolean testIsTrue
328-
) {
329-
exists(SubExpr lhs, int c, int x |
330-
compares_lt(cmp, lhs, right, c, isLt, testIsTrue) and
331-
left = lhs.getLeftOperand() and
332-
x = int_value(lhs.getRightOperand()) and
333-
k = c + x
334-
)
335-
or
336-
exists(SubExpr rhs, int c, int x |
337-
compares_lt(cmp, left, rhs, c, isLt, testIsTrue) and
338-
right = rhs.getLeftOperand() and
339-
x = int_value(rhs.getRightOperand()) and
340-
k = c - x
341-
)
342-
}
343-
344-
// left + x < right + c => left < right + (c-x)
345-
// left < (right + x) + c => left < right + (c+x)
346-
private predicate add_lt(
347-
ComparisonOperation cmp, Expr left, Expr right, int k, boolean isLt, boolean testIsTrue
348-
) {
349-
exists(AddExpr lhs, int c, int x |
350-
compares_lt(cmp, lhs, right, c, isLt, testIsTrue) and
351-
(
352-
left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand())
353-
or
354-
left = lhs.getRightOperand() and x = int_value(lhs.getLeftOperand())
355-
) and
356-
k = c - x
357-
)
358-
or
359-
exists(AddExpr rhs, int c, int x |
360-
compares_lt(cmp, left, rhs, c, isLt, testIsTrue) and
361-
(
362-
right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand())
363-
or
364-
right = rhs.getRightOperand() and x = int_value(rhs.getLeftOperand())
365-
) and
366-
k = c + x
367-
)
368-
}
369-
370-
/** The `int` value of integer constant expression. */
371-
private int int_value(Expr e) {
372-
e.getUnderlyingType() instanceof IntegralType and
373-
result = e.getValue().toInt()
374-
}
10+
import IRGuards
37511

37612
/** An `SsaDefinition` with an additional predicate `isLt`. */
37713
class GuardedSsa extends SsaDefinition {

0 commit comments

Comments
0 (0)
Morty Proxy This is a proxified and sanitized view of the page, visit original site.