Clean up SemanticCFG

This commit is contained in:
Dave Bartolomeo
2022-03-08 17:36:13 -05:00
parent 04fae43734
commit 09a5fded1c
6 changed files with 30 additions and 24 deletions

View File

@@ -4,30 +4,12 @@
private import java
private import SemanticExpr
private import SemanticExprSpecific
private import SemanticCFGSpecific::SemanticCFGConfig as Specific
private newtype TSemBasicBlock = MkSemBasicBlock(BasicBlock block)
class SemBasicBlock extends Specific::BasicBlock {
final predicate bbDominates(SemBasicBlock otherBlock) { Specific::bbDominates(this, otherBlock) }
class SemBasicBlock extends TSemBasicBlock {
BasicBlock block;
final predicate hasDominanceInformation() { Specific::hasDominanceInformation(this) }
SemBasicBlock() { this = MkSemBasicBlock(block) }
final string toString() { result = block.toString() }
final Location getLocation() { result = block.getLocation() }
final predicate bbDominates(SemBasicBlock otherBlock) {
block.bbDominates(getJavaBasicBlock(otherBlock))
}
final SemExpr getAnExpr() { SemanticExprConfig::getExprBasicBlock(result) = this }
}
SemBasicBlock getSemanticBasicBlock(BasicBlock block) { result = MkSemBasicBlock(block) }
BasicBlock getJavaBasicBlock(SemBasicBlock block) { block = getSemanticBasicBlock(result) }
predicate semHasDominanceInformation(SemBasicBlock bb) {
hasDominanceInformation(getJavaBasicBlock(bb))
final SemExpr getAnExpr() { result.getBasicBlock() = this }
}

View File

@@ -0,0 +1,20 @@
private import java as J
private import SemanticCFG
module SemanticCFGConfig {
class BasicBlock instanceof J::BasicBlock {
final string toString() { result = this.(J::BasicBlock).toString() }
final J::Location getLocation() { result = this.(J::BasicBlock).getLocation() }
}
predicate bbDominates(BasicBlock dominator, BasicBlock dominated) {
dominator.(J::BasicBlock).bbDominates(dominated.(J::BasicBlock))
}
predicate hasDominanceInformation(BasicBlock block) { J::hasDominanceInformation(block) }
}
SemBasicBlock getSemanticBasicBlock(J::BasicBlock block) { result = block }
J::BasicBlock getJavaBasicBlock(SemBasicBlock block) { block = getSemanticBasicBlock(result) }

View File

@@ -1,6 +1,7 @@
private import java as J
private import SemanticCFG
private import SemanticExpr
private import SemanticCFGSpecific
private import SemanticSSA
private import SemanticType
private import semmle.code.java.dataflow.SSA as SSA

View File

@@ -6,6 +6,7 @@ private import java
private import semmle.code.java.controlflow.Guards
private import semmle.code.java.controlflow.internal.GuardsLogic
private import SemanticCFG
private import SemanticCFGSpecific
private import SemanticExpr
private import SemanticExprSpecific
private import SemanticSSA

View File

@@ -9,6 +9,7 @@ private import SemanticExpr
private import SemanticType
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
private import SemanticExprSpecific
private import SemanticCFGSpecific
private newtype TSemSsaVariable = MkSemSsaVariable(SSA::SsaVariable var)
@@ -118,6 +119,6 @@ predicate semBackEdge(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionP
// Conservatively assume that every edge is a back edge if we don't have dominance information.
(
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
not semHasDominanceInformation(edge.getOrigBlock())
not edge.getOrigBlock().hasDominanceInformation()
)
}

View File

@@ -2,6 +2,7 @@ import java
import semmle.code.java.dataflow.SignAnalysis
import semmle.code.java.semantic.analysis.SignAnalysisCommon
import semmle.code.java.semantic.SemanticCFG
import semmle.code.java.semantic.SemanticCFGSpecific
import semmle.code.java.semantic.SemanticExpr
import semmle.code.java.semantic.SemanticExprSpecific
import semmle.code.java.semantic.SemanticSSA