Skip to content

Commit efa556c

Browse files
committed
Add library for reporting if all instances hold
Add a utility library for determing whether a condition holds for all copies of a statement in a program.
1 parent b5b300d commit efa556c

File tree

1 file changed

+106
-0
lines changed

1 file changed

+106
-0
lines changed
Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
/**
2+
* A module for considering whether a result occurs in all instances (e.g. copies) of the code at a
3+
* given location.
4+
*
5+
* Multiple instances of a statement at the same location can occur for two main reasons:
6+
* 1. Instantiations of a template
7+
* 2. Re-compilation of a file under a different context
8+
* This module helps ensure that a particular condition holds for all copies of a particular logical
9+
* statement. For example, this can be used to determine whether a line of code is dead in all copies
10+
* of a piece of code.
11+
*
12+
* This module is parameterized by a set of _candidate_ statements in the program. For each candidate
13+
* statement, we determine whether all other statements that occur at the same location in the
14+
* program are also part of the same set, ignoring any results generated by macros.
15+
*
16+
* We do so by reporting a new type of result, `LogicalResultStmt`, which represents a logical result
17+
* where all instances of a statement at a given location are considered to be part of the same set.
18+
*/
19+
20+
import cpp
21+
22+
/**
23+
* Holds if the `Stmt` `s` is not within a macro expansion, i.e. generated by a macro, but not the
24+
* outermost `Stmt` generated by the macro.
25+
*/
26+
predicate isNotWithinMacroExpansion(Stmt s) {
27+
not s.isInMacroExpansion()
28+
or
29+
exists(MacroInvocation mi |
30+
mi.getStmt() = s and
31+
not exists(mi.getParentInvocation())
32+
)
33+
}
34+
35+
/** A candidate set of types. */
36+
signature class CandidateStmtSig extends Stmt;
37+
38+
/**
39+
* A module for considering whether a result occurs in all instances (e.g. copies) of the code at a
40+
* given location.
41+
*/
42+
module HoldsForAllInstances<CandidateStmtSig CandidateStmt> {
43+
private predicate hasLocation(
44+
Stmt s, string filepath, int startline, int startcolumn, int endline, int endcolumn
45+
) {
46+
s.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
47+
}
48+
49+
final private class MyStmt = Stmt;
50+
51+
/**
52+
* A `Stmt` that appears at the same location as a candidate statement.
53+
*/
54+
private class RelevantStmt extends MyStmt {
55+
CandidateStmt s;
56+
57+
RelevantStmt() {
58+
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
59+
hasLocation(this, filepath, startline, startcolumn, endline, endcolumn) and
60+
hasLocation(s, filepath, startline, startcolumn, endline, endcolumn)
61+
) and
62+
// Not within a macro expansion, as we cannot match up instances by location in that
63+
// case
64+
isNotWithinMacroExpansion(this) and
65+
// Ignore catch handlers, as they occur at the same location as the catch block
66+
not this instanceof Handler
67+
}
68+
69+
CandidateStmt getCandidateStmt() { result = s }
70+
}
71+
72+
newtype TResultStmts =
73+
TLogicalResultStmt(string filepath, int startline, int startcolumn, int endline, int endcolumn) {
74+
exists(CandidateStmt s |
75+
// Only consider candidates where we can match up the location
76+
isNotWithinMacroExpansion(s) and
77+
hasLocation(s, filepath, startline, startcolumn, endline, endcolumn) and
78+
// All relevant statements that occur at the same location are candidates
79+
forex(RelevantStmt relevantStmt | s = relevantStmt.getCandidateStmt() |
80+
relevantStmt instanceof CandidateStmt
81+
)
82+
)
83+
}
84+
85+
/**
86+
* A logical result statement, representing all instances of a statement that occur at the same
87+
* location.
88+
*/
89+
class LogicalResultStmt extends TLogicalResultStmt {
90+
predicate hasLocationInfo(
91+
string filepath, int startline, int startcolumn, int endline, int endcolumn
92+
) {
93+
this = TLogicalResultStmt(filepath, startline, startcolumn, endline, endcolumn)
94+
}
95+
96+
/** Gets an instance of this logical result statement. */
97+
CandidateStmt getAStmtInstance() {
98+
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
99+
this = TLogicalResultStmt(filepath, startline, startcolumn, endline, endcolumn) and
100+
hasLocation(result, filepath, startline, startcolumn, endline, endcolumn)
101+
)
102+
}
103+
104+
string toString() { result = getAStmtInstance().toString() }
105+
}
106+
}

0 commit comments

Comments
 (0)