Skip to content

Commit

Permalink
Merge branch 'main' into yousif-memory-region-analysis
Browse files Browse the repository at this point in the history
  • Loading branch information
@yousifpatti
yousifpatti committed Nov 7, 2023
2 parents f8dc3e6 + ccb7669 commit de5b348
Show file tree
Hide file tree
Showing 383 changed files with 13,335 additions and 10,328 deletions.
6 changes: 2 additions & 4 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,15 @@
gen/
out/
target/
boogie_out.txt
boogie_out.bpl
metals.sbt
password.txt
*.iml
*.out
samples/const_prop_tests/
src/main/antlr4/.antlr
*.bpl
*.dot
result.txt
*.il
*.txt
examplesold/
src/test/scala/dump/
src/test/analysis/dump/
6 changes: 3 additions & 3 deletions build.sbt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,8 @@ updateExpected := {
if (resultPath.exists()) {
val result = IO.read(resultPath)
val verified = result.strip().equals("Boogie program verifier finished with 0 errors")
if (verified == shouldVerify && outPath.exists()) {
if (!expectedPath.exists() || !compareFiles(outPath, expectedPath)) {
if (verified == shouldVerify) {
if (outPath.exists() && !(expectedPath.exists() && filesContentEqual(outPath, expectedPath))) {
IO.copyFile(outPath, expectedPath)
}
}
Expand All @@ -59,7 +59,7 @@ updateExpected := {
}
}

def compareFiles(path1: File, path2: File): Boolean = {
def filesContentEqual(path1: File, path2: File): Boolean = {
val source1 = Source.fromFile(path1)
val source2 = Source.fromFile(path2)
val lines1 = source1.getLines
Expand Down
35 changes: 20 additions & 15 deletions src/main/scala/Main.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import util.RunUtils
import scala.collection.mutable.{ArrayBuffer, Set}
import scala.collection.{immutable, mutable}
import scala.language.postfixOps
import scala.sys.process._
import scala.sys.process.*
import util.*
import mainargs.{main, arg, ParserForClass, Flag}

Expand All @@ -23,17 +23,23 @@ object Main {
@arg(name = "spec", short = 's', doc = "BASIL specification file.")
specFileName: Option[String],
@arg(name = "output", short = 'o', doc = "Boogie output destination file.")
outFileName: String = "boogie_out.bpl",
outFileName: String = "basil-out",
@arg(name = "boogie-use-lambda-stores", doc = "Use lambda representation of store operations.")
lambdaStores: Flag,
@arg(name = "verbose", short = 'v', doc = "Show extra debugging logs.")
verbose: Flag,
@arg(name = "analyse", doc = "Run static analysis pass.")
analyse: Flag,
@arg(name = "interpret", doc = "Run BASIL IL interpreter.")
interpret: Flag,
@arg(name = "dump-il", doc = "Dump the Intermediate Language to text.")
dumpIL: Flag,
dumpIL: Option[String],
@arg(name = "help", short = 'h', doc = "Show this help message.")
help: Flag
help: Flag,
@arg(name = "analysis-results", doc = "Log analysis results in files at specified path.")
analysisResults: Option[String],
@arg(name = "analysis-results-dot", doc = "Log analysis results in .dot form at specified path.")
analysisResultsDot: Option[String]
)

def main(args: Array[String]): Unit = {
Expand All @@ -42,30 +48,29 @@ object Main {

val conf = parsed match {
case Right(r) => r
case Left(l) => {
case Left(l) =>
println(l)
return
}
}

if (conf.help.value) {
println(parser.helpText(sorted = false));
println(parser.helpText(sorted = false))
}

Logger.setLevel(LogLevel.INFO)
if (conf.verbose.value) {
Logger.setLevel(LogLevel.DEBUG)
}

val program: BProgram = RunUtils.loadAndTranslate(
conf.adtFileName,
conf.relfFileName,
conf.specFileName,
conf.analyse.value,
conf.interpret.value,
conf.dumpIL.value
val q = BASILConfig(
loading = ILLoadingConfig(conf.adtFileName, conf.relfFileName, conf.specFileName, conf.dumpIL),
runInterpret = conf.interpret.value,
staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot)) else None,
boogieTranslation = BoogieGeneratorConfig(if conf.lambdaStores.value then BoogieMemoryAccessMode.LambdaStoreSelect else BoogieMemoryAccessMode.SuccessiveStoreSelect),
outputPrefix = conf.outFileName,
)
RunUtils.writeToFile(program, conf.outFileName)

RunUtils.run(q)
}

}
123 changes: 58 additions & 65 deletions src/main/scala/analysis/Analysis.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,59 +147,49 @@ object Fresh {
}
}

trait MemoryRegion

/** Represents a stack region. The region is defined by a region Identifier identifying the assignment location. There
* can exist two regions with the same size (offset) but have a different base pointer. As such the base pointer is
* tracked but not printed in the toString method.
* @param start
* 0x1234 in case of mem[R1 + 0x1234] <- ...
* @param regionType
* The type of the region. This is used to distinguish between stack, heap, data and code regions.
* @param extent
* the start and end of the region
*/
case class StackRegion(regionIdentifier: String, start: Expr, var extent: Option[RangeKey]) extends MemoryRegion:
override def toString: String = s"Stack(${regionIdentifier}, ${start})"
override def hashCode(): Int = regionIdentifier.hashCode()
trait MemoryRegion {
val regionIdentifier: String
var extent: Option[RangeKey] = None
}

class StackRegion(override val regionIdentifier: String, val start: BitVecLiteral) extends MemoryRegion {
override def toString: String = s"Stack($regionIdentifier, $start)"
override def hashCode(): Int = regionIdentifier.hashCode() * start.hashCode()
override def equals(obj: Any): Boolean = obj match {
case StackRegion(ri, st, _) => st == start
case _ => false
case s: StackRegion => s.start == start && s.regionIdentifier == regionIdentifier
case _ => false
}
}

/** Represents a Heap region. The region is defined by its identifier which is defined by the allocation site.
* @param regionIdentifier
* region id identifying the call-site
* @param start
* the start address
* @param extent
* the start and end of the region
*/
case class HeapRegion(regionIdentifier: String, start: Expr, var extent: Option[RangeKey]) extends MemoryRegion:
override def toString: String = s"Heap(${regionIdentifier}, ${start})"
class HeapRegion(override val regionIdentifier: String, val allocatedSize: BitVecLiteral) extends MemoryRegion {
override def toString: String = s"Heap($regionIdentifier, $allocatedSize)"
override def hashCode(): Int = regionIdentifier.hashCode()
override def equals(obj: Any): Boolean = obj match {
case r: HeapRegion => regionIdentifier.equals(r.regionIdentifier)
case _ => false
case h: HeapRegion => h.regionIdentifier == regionIdentifier
case _ => false
}
}

case class DataRegion(regionIdentifier: String, start: Expr, var extent: Option[RangeKey]) extends MemoryRegion:
override def toString: String = s"Data(${regionIdentifier}, ${start})"

case class RegionAccess(regionBase: String, start: Expr) extends MemoryRegion:
override def toString: String = s"RegionAccess(${regionBase}, ${start})"
class DataRegion(override val regionIdentifier: String, val start: BitVecLiteral) extends MemoryRegion {
override def toString: String = s"Data($regionIdentifier, $start)"
override def hashCode(): Int = regionIdentifier.hashCode() * start.hashCode()
override def equals(obj: Any): Boolean = obj match {
case d: DataRegion => d.start == start && d.regionIdentifier == regionIdentifier
case _ => false
}
}

trait MemoryRegionAnalysisMisc:

var mallocCount: Int = 0
var stackCount: Int = 0
val stackMap: mutable.Map[CfgFunctionEntryNode, mutable.Map[Expr, StackRegion]] = mutable.HashMap()
private def getNextMallocCount(): String = {
private def nextMallocCount() = {
mallocCount += 1
s"malloc_$mallocCount"
}

private def getNextStackCount(): String = {
private def nextStackCount() = {
stackCount += 1
s"stack_$stackCount"
}
Expand All @@ -211,12 +201,12 @@ trait MemoryRegionAnalysisMisc:
* @param parent: the function entry node
* @return the stack region corresponding to the offset
*/
def poolMaster(expr: Expr, parent: CfgFunctionEntryNode): StackRegion = {
def poolMaster(expr: BitVecLiteral, parent: CfgFunctionEntryNode): StackRegion = {
val stackPool = stackMap.getOrElseUpdate(parent, mutable.HashMap())
if (stackPool.contains(expr)) {
stackPool(expr)
} else {
val newRegion = StackRegion(getNextStackCount(), expr, None)
val newRegion = StackRegion(nextStackCount(), expr)
stackPool += (expr -> newRegion)
newRegion
}
Expand Down Expand Up @@ -263,59 +253,58 @@ trait MemoryRegionAnalysisMisc:

private val mallocVariable = Register("R0", BitVecType(64))

/** Default implementation of eval.
*/
def eval(exp: Expr, env: stateLattice.Element, n: CfgNode): regionLattice.Element = {
def eval(exp: Expr, env: stateLattice.Element, n: CfgCommandNode): regionLattice.Element = {
import regionLattice._
Logger.debug(s"evaluating $exp")
Logger.debug(s"env: $env")
Logger.debug(s"n: $n")
exp match {
case binOp: BinaryExpr =>
if (binOp.arg1 == stackPointer) {
val rhs: Expr = evaluateExpression(binOp.arg2, n, constantProp(n))
Set(poolMaster(rhs, n.asInstanceOf[CfgStatementNode].parent))
evaluateExpression(binOp.arg2, constantProp(n)) match {
case Some(b: BitVecLiteral) => Set(poolMaster(b, n.parent))
case None => Set()
}
} else {
val evaluation: Expr = evaluateExpression(binOp, n, constantProp(n))
if (evaluation.equals(binOp)) {
return Set()
evaluateExpression(binOp, constantProp(n)) match {
case Some(b: BitVecLiteral) => eval(b, env, n)
case None => Set()
}
eval(evaluation, env, n)
}
case bitVecLiteral: BitVecLiteral =>
if (globals.contains(bitVecLiteral.value)) {
val globalName = globals(bitVecLiteral.value)
Set(DataRegion(globalName, bitVecLiteral, None))
Set(DataRegion(globalName, bitVecLiteral))
} else if (subroutines.contains(bitVecLiteral.value)) {
val subroutineName = subroutines(bitVecLiteral.value)
Set(DataRegion(subroutineName, bitVecLiteral, None))
Set(DataRegion(subroutineName, bitVecLiteral))
} else if (globalOffsets.contains(bitVecLiteral.value)) {
val val1 = globalOffsets(bitVecLiteral.value)
if (subroutines.contains(val1)) {
val globalName = subroutines(val1)
Set(DataRegion(globalName, bitVecLiteral, None))
Set(DataRegion(globalName, bitVecLiteral))
} else {
Set(DataRegion(s"Unknown_${bitVecLiteral}", bitVecLiteral, None))
Set(DataRegion(s"Unknown_$bitVecLiteral", bitVecLiteral))
}
} else {
//throw new Exception(s"Unknown type for $bitVecLiteral")
// unknown region here
Set(DataRegion(s"Unknown_${bitVecLiteral}", bitVecLiteral, None))
Set(DataRegion(s"Unknown_$bitVecLiteral", bitVecLiteral))
}
case variable: Variable =>
variable match {
case _: LocalVar =>
return Set()
Set()
case reg: Register if reg == stackPointer =>
return Set()
Set()
case _ =>
evaluateExpression(variable, constantProp(n)) match {
case Some(b: BitVecLiteral) =>
eval(b, env, n)
case _ =>
Set() // we cannot evaluate this to a concrete value, we need VSA for this
}
}

val evaluation: Expr = evaluateExpression(variable, n, constantProp(n))
evaluation match
case bitVecLiteral: BitVecLiteral =>
eval(bitVecLiteral, env, n)
case _ => Set() // we cannot evaluate this to a concrete value, we need VSA for this
case _ =>
Logger.debug(s"type: ${exp.getClass} $exp\n")
throw new Exception("Unknown type")
Expand All @@ -330,15 +319,19 @@ trait MemoryRegionAnalysisMisc:
cmd.data match {
case directCall: DirectCall =>
if (directCall.target.name == "malloc") {
return s ++ Set((n, Set(HeapRegion(getNextMallocCount(), evaluateExpression(mallocVariable, n, constantProp(n)), None))))

evaluateExpression(mallocVariable, constantProp(n)) match {
case Some(b: BitVecLiteral) =>
s ++ Set((s, Set(HeapRegion(nextMallocCount(), b))))
case None => s
}
} else {
s
}
s
case memAssign: MemoryAssign =>
if (ignoreRegions.contains(memAssign.rhs.value)) {
return s
}
val result = eval(memAssign.rhs.index, s, n)
val result = eval(memAssign.rhs.index, s, cmd)
/*
don't modify the IR in the middle of the analysis like this, also this produces a lot of incorrect results
result.collectFirst({
Expand Down Expand Up @@ -367,7 +360,7 @@ trait MemoryRegionAnalysisMisc:
val m = s
unwrapExpr(localAssign.rhs).foreach {
case memoryLoad: MemoryLoad =>
val result = eval(memoryLoad.index, s, n)
val result = eval(memoryLoad.index, s, cmd)
/*
don't modify the IR in the middle of the analysis like this, this also produces incorrect results
result.collectFirst({
Expand Down
Loading

0 comments on commit de5b348

Please sign in to comment.