Skip to content

Commit 017d492

Browse files
aibaarsaibaars
committed
Rust: implement synthesized Locations
1 parent 110d2ea commit 017d492

File tree

4 files changed

+120
-64
lines changed

4 files changed

+120
-64
lines changed

‎rust/ql/lib/codeql/Locations.qll

Lines changed: 3 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -1,68 +1,15 @@
11
/** Provides classes for working with locations. */
22

33
import files.FileSystem
4+
private import codeql.rust.elements.internal.LocationImpl
45

56
/**
67
* A location as given by a file, a start line, a start column,
78
* an end line, and an end column.
89
*
910
* For more information about locations see [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
1011
*/
11-
class Location extends @location_default {
12-
/** Gets the file for this location. */
13-
File getFile() { locations_default(this, result, _, _, _, _) }
14-
15-
/** Gets the 1-based line number (inclusive) where this location starts. */
16-
int getStartLine() { locations_default(this, _, result, _, _, _) }
17-
18-
/** Gets the 1-based column number (inclusive) where this location starts. */
19-
int getStartColumn() { locations_default(this, _, _, result, _, _) }
20-
21-
/** Gets the 1-based line number (inclusive) where this location ends. */
22-
int getEndLine() { locations_default(this, _, _, _, result, _) }
23-
24-
/** Gets the 1-based column number (inclusive) where this location ends. */
25-
int getEndColumn() { locations_default(this, _, _, _, _, result) }
26-
27-
/** Gets the number of lines covered by this location. */
28-
int getNumLines() { result = this.getEndLine() - this.getStartLine() + 1 }
29-
30-
/** Gets a textual representation of this element. */
31-
bindingset[this]
32-
pragma[inline_late]
33-
string toString() {
34-
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
35-
this.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
36-
result = filepath + "@" + startline + ":" + startcolumn + ":" + endline + ":" + endcolumn
37-
)
38-
}
39-
40-
/**
41-
* Holds if this element is at the specified location.
42-
* The location spans column `startcolumn` of line `startline` to
43-
* column `endcolumn` of line `endline` in file `filepath`.
44-
* For more information, see
45-
* [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
46-
*/
47-
predicate hasLocationInfo(
48-
string filepath, int startline, int startcolumn, int endline, int endcolumn
49-
) {
50-
exists(File f |
51-
locations_default(this, f, startline, startcolumn, endline, endcolumn) and
52-
filepath = f.getAbsolutePath()
53-
)
54-
}
55-
56-
/** Holds if this location starts strictly before the specified location. */
57-
pragma[inline]
58-
predicate strictlyBefore(Location other) {
59-
this.getStartLine() < other.getStartLine()
60-
or
61-
this.getStartLine() = other.getStartLine() and this.getStartColumn() < other.getStartColumn()
62-
}
63-
}
12+
final class Location = LocationImpl::Location;
6413

6514
/** An entity representing an empty location. */
66-
class EmptyLocation extends Location {
67-
EmptyLocation() { empty_location(this) }
68-
}
15+
final class EmptyLocation = LocationImpl::EmptyLocation;

‎rust/ql/lib/codeql/rust/Diagnostics.qll

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
/** Provides classes relating to extraction diagnostics. */
22

33
private import codeql.Locations
4+
private import codeql.rust.elements.internal.LocationImpl
45

56
/** A diagnostic emitted during extraction, such as a parse error */
67
class Diagnostic extends @diagnostic {
@@ -10,7 +11,12 @@ class Diagnostic extends @diagnostic {
1011
string fullMessage;
1112
Location location;
1213

13-
Diagnostic() { diagnostics(this, severity, tag, message, fullMessage, location) }
14+
Diagnostic() {
15+
exists(@location_default loc |
16+
diagnostics(this, severity, tag, message, fullMessage, loc) and
17+
location = LocationImpl::TLocationDefault(loc)
18+
)
19+
}
1420

1521
/**
1622
* Gets the numerical severity level associated with this diagnostic.

‎rust/ql/lib/codeql/rust/elements/internal/LocatableImpl.qll

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
*/
66

77
import codeql.Locations
8+
private import codeql.rust.elements.internal.LocationImpl
89
private import codeql.rust.elements.internal.generated.Locatable
910
private import codeql.rust.elements.internal.generated.Synth
1011
private import codeql.rust.elements.internal.generated.Raw
@@ -17,9 +18,21 @@ module Impl {
1718
class Locatable extends Generated::Locatable {
1819
pragma[nomagic]
1920
final Location getLocation() {
20-
exists(Raw::Locatable raw |
21-
raw = Synth::convertLocatableToRaw(this) and
22-
locatable_locations(raw, result)
21+
exists(@location_default location |
22+
result = LocationImpl::TLocationDefault(location) and
23+
locatable_locations(Synth::convertLocatableToRaw(this), location)
24+
)
25+
or
26+
not locatable_locations(Synth::convertLocatableToRaw(this), _) and
27+
exists(File file, int beginLine, int beginColumn, int endLine, int endColumn |
28+
this.hasLocationInfo(file.getAbsolutePath(), beginLine, beginColumn, endLine, endColumn)
29+
|
30+
result = LocationImpl::TLocationSynth(file, beginLine, beginColumn, endLine, endColumn)
31+
or
32+
exists(@location_default location |
33+
result = LocationImpl::TLocationDefault(location) and
34+
locations_default(location, file, beginLine, beginColumn, endLine, endColumn)
35+
)
2336
)
2437
}
2538

@@ -34,10 +47,6 @@ module Impl {
3447
string filepath, int startline, int startcolumn, int endline, int endcolumn
3548
) {
3649
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
37-
or
38-
not exists(this.getLocation()) and
39-
pragma[only_bind_out](any(EmptyLocation e))
40-
.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
4150
}
4251

4352
/**

‎rust/ql/lib/codeql/rust/elements/internal/LocationImpl.qll

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
private import codeql.files.FileSystem
2+
3+
module LocationImpl {
4+
newtype TLocation =
5+
TLocationDefault(@location_default location) or
6+
TLocationSynth(File file, int beginLine, int beginColumn, int endLine, int endColumn) {
7+
not locations_default(_, file, beginLine, beginColumn, endLine, endColumn) and none()
8+
}
9+
10+
/**
11+
* A location as given by a file, a start line, a start column,
12+
* an end line, and an end column.
13+
*
14+
* For more information about locations see [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
15+
*/
16+
abstract class Location extends TLocation {
17+
/** Gets the file for this location. */
18+
File getFile() { this.hasLocationInfo(result.getAbsolutePath(), _, _, _, _) }
19+
20+
/** Gets the 1-based line number (inclusive) where this location starts. */
21+
int getStartLine() { this.hasLocationInfo(_, result, _, _, _) }
22+
23+
/** Gets the 1-based column number (inclusive) where this location starts. */
24+
int getStartColumn() { this.hasLocationInfo(_, _, result, _, _) }
25+
26+
/** Gets the 1-based line number (inclusive) where this location ends. */
27+
int getEndLine() { this.hasLocationInfo(_, _, _, result, _) }
28+
29+
/** Gets the 1-based column number (inclusive) where this location ends. */
30+
int getEndColumn() { this.hasLocationInfo(_, _, _, _, result) }
31+
32+
/** Gets the number of lines covered by this location. */
33+
int getNumLines() { result = this.getEndLine() - this.getStartLine() + 1 }
34+
35+
/** Gets a textual representation of this element. */
36+
bindingset[this]
37+
pragma[inline_late]
38+
string toString() {
39+
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
40+
this.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
41+
result = filepath + "@" + startline + ":" + startcolumn + ":" + endline + ":" + endcolumn
42+
)
43+
}
44+
45+
/**
46+
* Holds if this element is at the specified location.
47+
* The location spans column `startcolumn` of line `startline` to
48+
* column `endcolumn` of line `endline` in file `filepath`.
49+
* For more information, see
50+
* [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
51+
*/
52+
abstract predicate hasLocationInfo(
53+
string filepath, int startline, int startcolumn, int endline, int endcolumn
54+
);
55+
56+
/** Holds if this location starts strictly before the specified location. */
57+
pragma[inline]
58+
predicate strictlyBefore(Location other) {
59+
this.getStartLine() < other.getStartLine()
60+
or
61+
this.getStartLine() = other.getStartLine() and this.getStartColumn() < other.getStartColumn()
62+
}
63+
}
64+
65+
private class LocationDefault extends Location, TLocationDefault {
66+
@location_default self;
67+
68+
LocationDefault() { this = TLocationDefault(self) }
69+
70+
override predicate hasLocationInfo(
71+
string filepath, int startline, int startcolumn, int endline, int endcolumn
72+
) {
73+
exists(File f |
74+
locations_default(self, f, startline, startcolumn, endline, endcolumn) and
75+
filepath = f.getAbsolutePath()
76+
)
77+
}
78+
}
79+
80+
/** An entity representing an empty location. */
81+
class EmptyLocation extends LocationDefault {
82+
EmptyLocation() { empty_location(self) }
83+
}
84+
85+
private class LocationSynth extends Location, TLocationSynth {
86+
override predicate hasLocationInfo(
87+
string filepath, int startline, int startcolumn, int endline, int endcolumn
88+
) {
89+
this =
90+
TLocationSynth(any(File f | f.getAbsolutePath() = filepath), startline, startcolumn,
91+
endline, endcolumn)
92+
}
93+
}
94+
}

0 commit comments

Comments
 (0)