Generalize ConjunctionParent

This commit is contained in:
Tony Torralba
2023-01-10 13:34:44 +01:00
parent 36ca97e4f6
commit ae8c75ac97
3 changed files with 69 additions and 49 deletions

View File

@@ -0,0 +1,45 @@
import ql
signature predicate checkAstNodeSig(AstNode p);
module ConjunctionParent<checkAstNodeSig/1 checkAstNode> {
/**
* Gets the top-most parent of `p` that is not a disjunction.
*/
AstNode getConjunctionParent(AstNode p) {
result =
min(int level, AstNode parent |
parent = getConjunctionParentRec(p) and level = level(parent)
|
parent order by level
)
}
/**
* Gets a (transitive) parent of `p`, where the parent is not a negative edge, and `checkAstNode(p)` holds.
*/
private AstNode getConjunctionParentRec(AstNode p) {
checkAstNode(p) and
result = p
or
result = getConjunctionParentRec(p).getParent() and
not result instanceof Disjunction and
not result instanceof IfFormula and
not result instanceof Implication and
not result instanceof Negation and
not result instanceof Predicate and
not result instanceof FullAggregate and
not result instanceof Forex and
not result instanceof Forall
}
/**
* Gets which level in the AST `p` is at.
* E.g. the top-level is 0, the next level is 1, etc.
*/
private int level(AstNode p) {
p instanceof TopLevel and result = 0
or
result = level(p.getParent()) + 1
}
}

View File

@@ -9,15 +9,14 @@
*/
import ql
import codeql_ql.style.ConjunctionParent
class AggregateOrForQuantifier extends AstNode {
AggregateOrForQuantifier() {
this instanceof FullAggregate or this instanceof Forex or this instanceof Forall
}
}
from VarDecl existsArgument, VarAccess use
where
/**
* Holds if `existsArgument` is the declaration of a variable in an `exists` formula,
* and `use` is both its only use and an argument of a predicate that doesn't restrict
* the corresponding parameter type.
*/
predicate omittableExists(VarDecl existsArgument, VarAccess use) {
existsArgument = any(Exists e).getAnArgument() and
use = unique( | | existsArgument.getAnAccess()) and
exists(Call c, int argPos, Type paramType |
@@ -25,7 +24,16 @@ where
|
existsArgument.getType() = paramType.getASuperType*() and
not paramType instanceof DatabaseType
) and
not use.getParent*() instanceof AggregateOrForQuantifier
)
}
/** Holds if `p` is an exists variable (either declaration or use) that can be omitted. */
predicate omittableExistsNode(AstNode p) { omittableExists(p, _) or omittableExists(_, p) }
from VarDecl existsArgument, VarAccess use
where
omittableExists(existsArgument, use) and
ConjunctionParent<omittableExistsNode/1>::getConjunctionParent(existsArgument) =
ConjunctionParent<omittableExistsNode/1>::getConjunctionParent(use)
select existsArgument, "This exists variable can be omitted by using a don't-care expression $@.",
use, "in this argument"

View File

@@ -9,6 +9,8 @@
*/
import ql
import codeql_ql.style.ConjunctionParent
import codeql.GlobalValueNumbering as GVN
/**
* A variable that is set equal to (assigned) a value one or more times.
@@ -40,8 +42,6 @@ class AssignedVariable extends VarDecl {
}
}
import codeql.GlobalValueNumbering as GVN
/**
* Holds if `assigned1` and `assigned2` assigns the same value to `var`.
* The assignments may be on different branches of a disjunction.
@@ -58,47 +58,14 @@ predicate candidateRedundantAssignment(AssignedVariable var, Expr assigned1, Exp
assigned1 != assigned2
}
/**
* Gets a (transitive) parent of `p`, where the parent is not a disjunction, and `p` is a candidate assignment from `candidateRedundantAssignment`.
*/
AstNode getConjunctionParentRec(AstNode p) {
candidateRedundantAssignment(_, p, _) and
result = p
or
result = getConjunctionParentRec(p).getParent() and
not result instanceof Disjunction and
not result instanceof IfFormula and
not result instanceof Implication and
not result instanceof Negation and
not result instanceof Predicate
}
/**
* Gets which level in the AST `p` is at.
* E.g. the top-level is 0, the next level is 1, etc.
*/
int level(AstNode p) {
p instanceof TopLevel and result = 0
or
result = level(p.getParent()) + 1
}
/**
* Gets the top-most parent of `p` that is not a disjunction.
*/
AstNode getConjunctionParent(AstNode p) {
result =
min(int level, AstNode parent |
parent = getConjunctionParentRec(p) and level = level(parent)
|
parent order by level
)
}
/** Holds if `p` is a candidate node for redundant assignment. */
predicate candidateNode(AstNode p) { candidateRedundantAssignment(_, p, _) }
from AssignedVariable var, Expr assigned1, Expr assigned2
where
candidateRedundantAssignment(var, assigned1, assigned2) and
getConjunctionParent(assigned1) = getConjunctionParent(assigned2) and
ConjunctionParent<candidateNode/1>::getConjunctionParent(assigned1) =
ConjunctionParent<candidateNode/1>::getConjunctionParent(assigned2) and
// de-duplcation:
(
assigned1.getLocation().getStartLine() < assigned2.getLocation().getStartLine()