Merge pull request #567 from hvitved/csharp/guards-splitting

C#: Account for split SSA definitions in guards library
This commit is contained in:
calumgrant
2018-11-30 14:57:57 +00:00
committed by GitHub
5 changed files with 32 additions and 13 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

@@ -82,3 +82,4 @@
| Splitting.cs:117:9:117:9 | access to parameter o | Splitting.cs:116:22:116:30 | ... != ... | Splitting.cs:116:22:116:22 | access to parameter o | true |
| 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 |

View File

@@ -195,3 +195,4 @@
| 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: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 |

View File

@@ -224,3 +224,7 @@
| Splitting.cs:105:22:105:30 | ... != ... | true | Splitting.cs:105:22:105:22 | access to parameter o | non-null |
| Splitting.cs:116:22:116:30 | ... != ... | false | Splitting.cs:116:22:116:22 | access to parameter o | null |
| Splitting.cs:116:22:116:30 | ... != ... | true | Splitting.cs:116:22:116:22 | access to parameter o | non-null |
| Splitting.cs:128:17:128:25 | ... != ... | false | Splitting.cs:128:17:128:17 | access to local variable o | null |
| Splitting.cs:128:17:128:25 | ... != ... | true | Splitting.cs:128:17:128:17 | access to local variable o | non-null |
| Splitting.cs:133:17:133:17 | access to local variable o | non-null | Splitting.cs:132:21:132:29 | call to method M11 | non-null |
| Splitting.cs:133:17:133:17 | access to local variable o | null | Splitting.cs:132:21:132:29 | call to method M11 | null |

View File

@@ -119,4 +119,20 @@ public class Splitting
o.ToString(); // null guarded
return o.ToString(); // null guarded
}
public void M12(int i, bool b)
{
object o = null;
do
{
if (o != null)
{
if (b)
return;
o = M11(b, o);
o.GetHashCode(); // not null guarded
}
}
while (i > 0);
}
}