SSA: Make shared library a parameterized module

This commit is contained in:
Tom Hvitved
2022-08-19 15:24:28 +02:00
parent f846c262dc
commit 0d81a6409d
6 changed files with 865 additions and 774 deletions

View File

@@ -1,8 +1,8 @@
import csharp
import semmle.code.csharp.dataflow.internal.SsaImplCommon::Consistency
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency as Consistency
import Ssa
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
@@ -10,6 +10,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
}
}
query predicate nonUniqueDef = Consistency::nonUniqueDef/4;
query predicate readWithoutDef = Consistency::readWithoutDef/3;
query predicate deadDef = Consistency::deadDef/2;
query predicate notDominatedByDef = Consistency::notDominatedByDef/4;
query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
// Local variables in C# must be initialized before every use, so uninitialized
// local variables should not have an SSA definition, as that would imply that

View File

@@ -192,8 +192,7 @@ class BasicBlock extends TBasicBlockStart {
* Gets the basic block that immediately dominates this basic block, if any.
*
* That is, all paths reaching this basic block from some entry point
* basic block must go through the result, which is an immediate basic block
* predecessor of this basic block.
* basic block must go through the result.
*
* Example:
*
@@ -207,8 +206,7 @@ class BasicBlock extends TBasicBlockStart {
*
* The basic block starting on line 2 is an immediate dominator of
* the basic block online 4 (all paths from the entry point of `M`
* to `return s.Length;` must go through the null check, and the null check
* is an immediate predecessor of `return s.Length;`).
* to `return s.Length;` must go through the null check.
*/
BasicBlock getImmediateDominator() { bbIDominates(result, this) }

View File

@@ -3,7 +3,53 @@
*/
import csharp
import SsaImplCommon
private import SsaImplCommon as SsaImplCommon
private import AssignableDefinitions
private module SsaInput implements SsaImplCommon::InputSig {
class BasicBlock = ControlFlow::BasicBlock;
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
class SourceVariable = Ssa::SourceVariable;
/**
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
* variable `v`. The Boolean `certain` indicates whether the write is certain.
*
* This includes implicit writes via calls.
*/
predicate variableWrite(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
variableWriteDirect(bb, i, v, certain)
or
variableWriteQualifier(bb, i, v, certain)
or
updatesNamedFieldOrProp(bb, i, _, v, _) and
certain = false
or
updatesCapturedVariable(bb, i, _, v, _, _) and
certain = false
}
/**
* Holds if the `i`th of basic block `bb` reads source variable `v`.
*
* This includes implicit reads via calls.
*/
predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
variableReadActual(bb, i, v) and
certain = true
or
variableReadPseudo(bb, i, v) and
certain = false
}
}
import SsaImplCommon::Make<SsaInput>
/**
* Holds if the `i`th node of basic block `bb` reads source variable `v`.
@@ -805,24 +851,6 @@ private module CapturedVariableImpl {
}
}
/**
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
* variable `v`. The Boolean `certain` indicates whether the write is certain.
*
* This includes implicit writes via calls.
*/
predicate variableWrite(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
variableWriteDirect(bb, i, v, certain)
or
variableWriteQualifier(bb, i, v, certain)
or
updatesNamedFieldOrProp(bb, i, _, v, _) and
certain = false
or
updatesCapturedVariable(bb, i, _, v, _, _) and
certain = false
}
/**
* Liveness analysis to restrict the size of the SSA representation for
* captured variables.
@@ -1039,19 +1067,6 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
capturedReadIn(bb, i, v, _, _, _)
}
/**
* Holds if the `i`th of basic block `bb` reads source variable `v`.
*
* This includes implicit reads via calls.
*/
predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
variableReadActual(bb, i, v) and
certain = true
or
variableReadPseudo(bb, i, v) and
certain = false
}
cached
private module Cached {
cached
@@ -1151,7 +1166,7 @@ private module Cached {
predicate variableWriteQualifier(
ControlFlow::BasicBlock bb, int i, QualifiedFieldOrPropSourceVariable v, boolean certain
) {
variableWrite(bb, i, v.getQualifier(), certain) and
SsaInput::variableWrite(bb, i, v.getQualifier(), certain) and
// Eliminate corner case where a call definition can overlap with a
// qualifier definition: if method `M` updates field `F`, then a call
// to `M` is both an update of `x.M` and `x.M.M`, so the former call

View File

@@ -1,19 +0,0 @@
/** Provides the C# specific parameters for `SsaImplCommon.qll`. */
private import csharp
private import AssignableDefinitions
private import SsaImpl as SsaImpl
class BasicBlock = ControlFlow::BasicBlock;
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
class SourceVariable = Ssa::SourceVariable;
predicate variableWrite = SsaImpl::variableWrite/4;
predicate variableRead = SsaImpl::variableRead/4;

View File

@@ -1,5 +1,5 @@
import csharp
import semmle.code.csharp.dataflow.internal.SsaImplCommon
import semmle.code.csharp.dataflow.internal.SsaImpl
from Ssa::SourceVariable v, ControlFlow::BasicBlock bb
where phiReadExposedForTesting(bb, v)