C#: Account for split SSA definitions in guards library

On 03e69e9945, I updated the guards library to account
for control flow graph splitting. However, the logic that relates SSA qualifiers for
the guard and the guarded expression was not updated accordingly.
This commit is contained in:
Tom Hvitved
2018-11-28 19:57:02 +01:00
parent 1a25f0a068
commit 3eb163f656
4 changed files with 10 additions and 17 deletions

View File

@@ -285,7 +285,7 @@ class AccessOrCallExpr extends Expr {
Declaration getTarget() { result = target }
/**
* Gets the (non-trivial) SSA definition corresponding to the longest
* Gets a (non-trivial) SSA definition corresponding to the longest
* qualifier chain of this expression, if any.
*
* This includes the case where this expression is itself an access to an
@@ -299,13 +299,11 @@ class AccessOrCallExpr extends Expr {
* x.Foo().Bar(); // SSA qualifier: SSA definition for `x`
* x; // SSA qualifier: SSA definition for `x`
* ```
*
* An expression can have more than one SSA qualifier in the presence
* of control flow splitting.
*/
Ssa::Definition getSsaQualifier() { result = getSsaQualifier(this) }
/**
* Holds if this expression has an SSA qualifier.
*/
predicate hasSsaQualifier() { exists(this.getSsaQualifier()) }
Ssa::Definition getAnSsaQualifier() { result = getAnSsaQualifier(this) }
}
private Declaration getDeclarationTarget(Expr e) {
@@ -313,11 +311,11 @@ private Declaration getDeclarationTarget(Expr e) {
result = e.(Call).getTarget()
}
private Ssa::Definition getSsaQualifier(Expr e) {
private Ssa::Definition getAnSsaQualifier(Expr e) {
e = getATrackedRead(result)
or
not e = getATrackedRead(_) and
result = getSsaQualifier(e.(QualifiableExpr).getQualifier())
result = getAnSsaQualifier(e.(QualifiableExpr).getQualifier())
}
private AssignableRead getATrackedRead(Ssa::Definition def) {
@@ -688,10 +686,9 @@ module Internal {
predicate isGuardedBy(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, AbstractValue v) {
isGuardedBy1(guarded, g, sub, v) and
sub = g.getAChildExpr*() and
(
not guarded.hasSsaQualifier() and not sub.hasSsaQualifier()
or
guarded.getSsaQualifier() = sub.getSsaQualifier()
forall(Ssa::Definition def |
def = sub.getAnSsaQualifier() |
def = guarded.getAnSsaQualifier()
)
}
}

View File

@@ -81,4 +81,3 @@
| Splitting.cs:119:13:119:13 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:132:25:132:25 | access to parameter b | Splitting.cs:130:21:130:21 | access to parameter b | Splitting.cs:130:21:130:21 | access to parameter b | false |
| Splitting.cs:133:17:133:17 | access to local variable o | Splitting.cs:128:17:128:25 | ... != ... | Splitting.cs:128:17:128:17 | access to local variable o | true |

View File

@@ -192,5 +192,3 @@
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | Splitting.cs:116:22:116:22 | access to parameter o | non-null |
| Splitting.cs:120:16:120:16 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| Splitting.cs:132:25:132:25 | access to parameter b | Splitting.cs:130:21:130:21 | access to parameter b | Splitting.cs:130:21:130:21 | access to parameter b | false |
| Splitting.cs:133:17:133:17 | access to local variable o | Splitting.cs:128:17:128:17 | access to local variable o | Splitting.cs:128:17:128:17 | access to local variable o | non-null |
| Splitting.cs:133:17:133:17 | access to local variable o | Splitting.cs:128:17:128:25 | ... != ... | Splitting.cs:128:17:128:17 | access to local variable o | true |

View File

@@ -53,4 +53,3 @@
| Splitting.cs:117:9:117:9 | access to parameter o |
| Splitting.cs:119:13:119:13 | access to parameter o |
| Splitting.cs:120:16:120:16 | access to parameter o |
| Splitting.cs:133:17:133:17 | access to local variable o |