C++: Use StackVariable in def-use libraries

Most of the implementation was already in terms of
`SemanticStackVariable`, so not much should have changed.
This commit is contained in:
Jonas Jensen
2019-11-18 15:37:31 +01:00
parent 95a333d28c
commit e57f98ca64
6 changed files with 15 additions and 17 deletions

View File

@@ -1,5 +1,5 @@
import cpp
private import semmle.code.cpp.controlflow.LocalScopeVariableReachability
private import semmle.code.cpp.controlflow.StackVariableReachability
private import semmle.code.cpp.dataflow.EscapesTree
/**
@@ -108,7 +108,7 @@ library class DefOrUse extends ControlFlowNodeBase {
/*
* Implementation detail: this predicate and its private auxiliary
* predicates are instances of the more general predicates in
* LocalScopeVariableReachability.qll, and should be kept in sync.
* StackVariableReachability.qll, and should be kept in sync.
*
* Unfortunately, caching of abstract predicates does not work well, so the
* predicates are duplicated for now.

View File

@@ -1,24 +1,22 @@
import cpp
import semmle.code.cpp.controlflow.LocalScopeVariableReachability
import semmle.code.cpp.controlflow.StackVariableReachability
// Test that def/use algorithm is an instance of LocalScopeVariableReachability
class MyDefOrUse extends LocalScopeVariableReachability {
// Test that def/use algorithm is an instance of StackVariableReachability
class MyDefOrUse extends StackVariableReachability {
MyDefOrUse() { this = "MyDefUse" }
override predicate isSource(ControlFlowNode node, LocalScopeVariable v) { definition(v, node) }
override predicate isSource(ControlFlowNode node, StackVariable v) { definition(v, node) }
override predicate isSink(ControlFlowNode node, LocalScopeVariable v) { useOfVar(v, node) }
override predicate isSink(ControlFlowNode node, StackVariable v) { useOfVar(v, node) }
override predicate isBarrier(ControlFlowNode node, LocalScopeVariable v) {
definitionBarrier(v, node)
}
override predicate isBarrier(ControlFlowNode node, StackVariable v) { definitionBarrier(v, node) }
}
predicate equivalence() {
forall(LocalScopeVariable v, Expr first, Expr second | definitionUsePair(v, first, second) |
forall(StackVariable v, Expr first, Expr second | definitionUsePair(v, first, second) |
exists(MyDefOrUse x | x.reaches(first, v, second))
) and
forall(LocalScopeVariable v, Expr first, Expr second |
forall(StackVariable v, Expr first, Expr second |
exists(MyDefOrUse x | x.reaches(first, v, second))
|
definitionUsePair(v, first, second)

View File

@@ -1,5 +1,5 @@
import cpp
from LocalScopeVariable v, ControlFlowNode def, Expr e
from StackVariable v, ControlFlowNode def, Expr e
where exprDefinition(v, def, e)
select v, def, e

View File

@@ -1,5 +1,5 @@
import cpp
from LocalScopeVariable v, VariableAccess use
from StackVariable v, VariableAccess use
where useOfVar(v, use)
select v, use

View File

@@ -1,9 +1,9 @@
import cpp
from LocalScopeVariable v, VariableAccess use
from StackVariable v, VariableAccess use
where
useOfVarActual(v, use) and
// Also check that `useOfVarActual` is a subset of `useOfVar`; if not
// the query will not return any results
forall(LocalScopeVariable v0, VariableAccess use0 | useOfVarActual(v0, use0) | useOfVar(v0, use0))
forall(StackVariable v0, VariableAccess use0 | useOfVarActual(v0, use0) | useOfVar(v0, use0))
select v, use

View File

@@ -1,5 +1,5 @@
import cpp
from LocalScopeVariable v, ControlFlowNode def, Expr e
from StackVariable v, ControlFlowNode def, Expr e
where exprDefinition(v, def, e)
select v, def, e