Shared SSA: Sync files

This commit is contained in:
Tom Hvitved
2021-11-19 10:19:08 +01:00
parent bc80c9b013
commit 4068cc9c3a
5 changed files with 125 additions and 0 deletions

View File

@@ -634,3 +634,28 @@ class UncertainWriteDefinition extends WriteDefinition {
)
}
}
/** Provides a set of consistency queries. */
module Consistency {
abstract class RelevantDefinition extends Definition {
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(_, def0, bb, i)))
}
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(_, _, bb, i)
}
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _)
}
}

View File

@@ -634,3 +634,28 @@ class UncertainWriteDefinition extends WriteDefinition {
)
}
}
/** Provides a set of consistency queries. */
module Consistency {
abstract class RelevantDefinition extends Definition {
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(_, def0, bb, i)))
}
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(_, _, bb, i)
}
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _)
}
}

View File

@@ -634,3 +634,28 @@ class UncertainWriteDefinition extends WriteDefinition {
)
}
}
/** Provides a set of consistency queries. */
module Consistency {
abstract class RelevantDefinition extends Definition {
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(_, def0, bb, i)))
}
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(_, _, bb, i)
}
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _)
}
}

View File

@@ -634,3 +634,28 @@ class UncertainWriteDefinition extends WriteDefinition {
)
}
}
/** Provides a set of consistency queries. */
module Consistency {
abstract class RelevantDefinition extends Definition {
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(_, def0, bb, i)))
}
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(_, _, bb, i)
}
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _)
}
}

View File

@@ -634,3 +634,28 @@ class UncertainWriteDefinition extends WriteDefinition {
)
}
}
/** Provides a set of consistency queries. */
module Consistency {
abstract class RelevantDefinition extends Definition {
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(_, def0, bb, i)))
}
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(_, _, bb, i)
}
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _)
}
}