Performance tests

.gitignore

@@ -18,6 +18,7 @@ samples/const_prop_tests/
 src/main/antlr4/.antlr
 *.bpl
 *.dot
+*.il
 result.txt
 examplesold/
 src/test/scala/dump/

build.sbt

@@ -45,21 +45,26 @@ updateExpected := {
         val name = e.getName
         val outPath = v / (name + ".bpl")
         val expectedPath = v / (name + ".expected")
+        val ILOutPath = v / (name + "-before-analysis.il")
+        val ILExpectedPath = v / (name + "-before-analysis.il.expected")
         val resultPath = v / (name + "_result.txt")
         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)
             }
+            if (ILOutPath.exists() && !(ILExpectedPath.exists() && filesContentEqual(ILExpectedPath, ILOutPath))) {
+              IO.copyFile(ILOutPath, ILExpectedPath)
+            }
           }
         }
       }
     }
   }
 
-  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

src/main/scala/Main.scala

@@ -23,15 +23,17 @@ 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
   )
@@ -57,15 +59,15 @@ object Main {
       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)) 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);
   }
 
 }

src/main/scala/boogie/BExpr.scala

@@ -403,12 +403,15 @@ trait QuantifierExpr(sort: Quantifier, bound: List[BVar], body: BExpr) extends B
 enum Quantifier {
   case forall
   case exists
+  case lambda
 }
 
 case class ForAll(bound: List[BVar], body: BExpr) extends QuantifierExpr(Quantifier.forall, bound, body)
 
 case class Exists(bound: List[BVar], body: BExpr) extends QuantifierExpr(Quantifier.exists, bound, body)
 
+case class Lambda(bound: List[BVar], body: BExpr) extends QuantifierExpr(Quantifier.lambda, bound, body)
+
 case class Old(body: BExpr) extends BExpr {
   override def toString: String = s"old($body)"
   override def getType: BType = body.getType
@@ -468,6 +471,68 @@ case class GammaStoreOp(addressSize: Int, bits: Int, accesses: Int) extends Func
 }
 case class LOp(memoryType: BType, indexType: BType) extends FunctionOp
 
+/**
+ * Utility to extract a particular byte from a bitvector.
+ */
+case class ByteExtract(valueSize: Int, offsetSize: Int) extends FunctionOp {
+  val fnName: String = s"byte_extract${valueSize}_${offsetSize}"
+}
+
+case class BByteExtract(value: BExpr, offset: BExpr) extends BExpr {
+  override def toString: String = s"$fnName($value, $offset)"
+
+  val valueSize: Int = value.getType match {
+    case b: BitVecBType => b.size
+    case _              => throw new Exception(s"ByteExtract does not have Bitvector type: $this")
+  }
+
+  val offsetSize: Int = offset.getType match {
+    case b: BitVecBType => b.size
+    case _              => throw new Exception(s"ByteExtract does not have Bitvector type: $this")
+  }
+
+  val fnName: String = s"byte_extract${valueSize}_${offsetSize}"
+
+  override val getType: BType = BitVecBType(8)
+  override def functionOps: Set[FunctionOp] =
+    value.functionOps ++ offset.functionOps + ByteExtract(valueSize, offsetSize)
+  override def locals: Set[BVar] = value.locals ++ offset.locals
+  override def globals: Set[BVar] = value.globals ++ offset.globals
+  override def loads: Set[BExpr] = value.loads ++ offset.loads
+}
+
+/**
+ * Utility to test if a particular value i is within the bounds of a base variable
+ * and some length. Factors in the problem of wrap around, given the base + length
+ * exceeds the bitvector size.
+ *
+ * Assumes all inputs are of the same bitvector width.
+ */
+case class InBounds(bits: Int, endian: Endian) extends FunctionOp {
+  val fnName: String = endian match {
+    case Endian.LittleEndian => s"in_bounds${bits}_le"
+    case Endian.BigEndian=> s"in_bounds${bits}_be"
+  }
+}
+
+case class BInBounds(base: BExpr, len: BExpr, endian: Endian, i: BExpr) extends BExpr {
+  override def toString: String = s"$fnName($base, $len, $i)"
+
+  val baseSize: Int = base.getType match {
+    case b: BitVecBType => b.size
+    case _              => throw new Exception(s"InBounds does not have Bitvector type: $this")
+  }
+
+  val fnName: String = s"in_bounds${baseSize}"
+
+  override val getType: BType = BoolBType
+  override def functionOps: Set[FunctionOp] =
+    base.functionOps ++ len.functionOps ++ i.functionOps + InBounds(baseSize, endian)
+  override def locals: Set[BVar]  = base.locals ++ len.locals ++ i.locals
+  override def globals: Set[BVar] = base.globals ++ len.globals ++ i.globals 
+  override def loads: Set[BExpr]  = base.loads ++ len.loads ++ i.loads 
+}
+
 case class BMemoryLoad(memory: BMapVar, index: BExpr, endian: Endian, bits: Int) extends BExpr {
   override def toString: String = s"$fnName($memory, $index)"
 

src/main/scala/boogie/BProgram.scala

@@ -64,7 +64,7 @@ case class BAxiom(body: BExpr) extends BDeclaration {
   override def toString: String = s"axiom $body;"
 }
 
-case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar, body: Option[BExpr])
+case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar, body: Option[BExpr], inline: Boolean =false)
     extends BDeclaration
     with Ordered[BFunction] {
   override def compare(that: BFunction): Int = name.compare(that.name)
@@ -74,8 +74,13 @@ case class BFunction(name: String, bvbuiltin: String, in: List[BVar], out: BVar,
     } else {
       s" {:bvbuiltin \"$bvbuiltin\"}"
     }
+    val inlineString = if (inline) {
+      s" {:inline}"
+    } else {
+      ""
+    }
     val inString = in.map(_.withType).mkString(", ")
-    val declString = s"function$bvbuiltinString $name($inString) returns (${out.withType})"
+    val declString = s"function$bvbuiltinString$inlineString $name($inString) returns (${out.withType})"
     body match {
       case Some(b) => List(declString + " {", "  " + b.toString, "}", "")
       case None    => List(declString + ";")

src/main/scala/translating/IRToBoogie.scala

@@ -1,7 +1,8 @@
 package translating
-import ir._
-import boogie._
-import specification._
+import ir.*
+import boogie.*
+import specification.*
+import util.{BoogieGeneratorConfig, BoogieMemoryAccessMode}
 
 import scala.collection.mutable.ArrayBuffer
 
@@ -25,14 +26,17 @@ class IRToBoogie(var program: Program, var spec: Specification) {
   private val Gamma_mem = BMapVar("Gamma_mem", MapBType(BitVecBType(64), BoolBType), Scope.Global)
   private val stack = BMapVar("stack", MapBType(BitVecBType(64), BitVecBType(8)), Scope.Global)
   private val Gamma_stack = BMapVar("Gamma_stack", MapBType(BitVecBType(64), BoolBType), Scope.Global)
+
+  private var config: BoogieGeneratorConfig = BoogieGeneratorConfig()
   private val modifiedCheck: Set[BVar] = (for (i <- 19 to 29) yield {
     Set(BVariable("R" + i, BitVecBType(64), Scope.Global), BVariable("Gamma_R" + i, BoolBType, Scope.Global))
   }).flatten.toSet ++ Set(
     BVariable("R" + 31, BitVecBType(64), Scope.Global),
     BVariable("Gamma_R" + 31, BoolBType, Scope.Global)
   )
 
-  def translate: BProgram = {
+  def translate(boogieGeneratorConfig: BoogieGeneratorConfig): BProgram = {
+    config = boogieGeneratorConfig
     val readOnlyMemory = memoryToCondition(program.readOnlyMemory)
     val procedures = program.procedures.map(f => translateProcedure(f, readOnlyMemory))
     val defaultGlobals = List(BVarDecl(mem), BVarDecl(Gamma_mem))
@@ -59,10 +63,13 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     val rgProcs = genRely(relies, readOnlyMemory) :+ guaranteeReflexive
 
     val functionsUsed1 =
-      procedures.flatMap(p => p.functionOps).toSet ++ rgProcs.flatMap(p => p.functionOps).toSet ++ directFunctions
+      procedures.flatMap(p => p.functionOps).toSet ++
+      rgProcs.flatMap(p => p.functionOps).toSet ++
+      directFunctions
     val functionsUsed2 = functionsUsed1.map(p => functionOpToDefinition(p))
     val functionsUsed3 = functionsUsed2.flatMap(p => p.functionOps).map(p => functionOpToDefinition(p))
-    val functionsUsed = (functionsUsed2 ++ functionsUsed3).toList.sorted
+    val functionsUsed4 = functionsUsed3.flatMap(p => p.functionOps).map(p => functionOpToDefinition(p))
+    val functionsUsed = (functionsUsed2 ++ functionsUsed3 ++ functionsUsed4).toList.sorted
 
     val declarations = globalDecls ++ globalConsts ++ functionsUsed ++ pushUpModifiesFixedPoint(rgProcs ++ procedures)
     BProgram(declarations)
@@ -138,26 +145,41 @@ class IRToBoogie(var program: Program, var spec: Specification) {
         val valueVar = BParam("value", BitVecBType(m.bits))
         val in = List(memVar, indexVar, valueVar)
         val out = BParam(memType)
-        val indices: Seq[BExpr] = for (i <- 0 until m.accesses) yield {
-          if (i == 0) {
-            indexVar
-          } else {
-            BinaryBExpr(BVADD, indexVar, BitVecBLiteral(i, m.addressSize))
-          }
-        }
-        val values: Seq[BExpr] = for (i <- 0 until m.accesses) yield {
-          BVExtract((i + 1) * m.valueSize, i * m.valueSize, valueVar)
-        }
-        val valuesEndian = m.endian match {
-          case Endian.BigEndian    => values.reverse
-          case Endian.LittleEndian => values
-        }
-        val indiceValues = for (i <- 0 until m.accesses) yield {
-          (indices(i), valuesEndian(i))
-        }
+        val body: BExpr = config.memoryFunctionType match {
+          case BoogieMemoryAccessMode.SuccessiveStoreSelect => {
+            val indices: Seq[BExpr] = for (i <- 0 until m.accesses) yield {
+              if (i == 0) {
+                indexVar
+              } else {
+                BinaryBExpr(BVADD, indexVar, BitVecBLiteral(i, m.addressSize))
+              }
+            }
+            val values: Seq[BExpr] = for (i <- 0 until m.accesses) yield {
+              BVExtract((i + 1) * m.valueSize, i * m.valueSize, valueVar)
+            }
+            val valuesEndian = m.endian match {
+              case Endian.BigEndian => values.reverse
+              case Endian.LittleEndian => values
+            }
+            val indiceValues = for (i <- 0 until m.accesses) yield {
+              (indices(i), valuesEndian(i))
+            }
 
-        val body: MapUpdate = indiceValues.tail.foldLeft(MapUpdate(memVar, indices.head, valuesEndian.head)) {
-          (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
+            indiceValues.tail.foldLeft(MapUpdate(memVar, indices.head, valuesEndian.head)) {
+              (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
+            }
+          }
+          case BoogieMemoryAccessMode.LambdaStoreSelect => {
+            if m.accesses == 1 then
+              MapUpdate(memVar, indexVar, valueVar)
+            else {
+              val i = BVariable("i", BitVecBType(m.addressSize), Scope.Local)
+              Lambda(List(i), IfThenElse(
+                BInBounds(indexVar, BitVecBLiteral(m.accesses, m.addressSize), m.endian, i),
+                BByteExtract(valueVar, BinaryBExpr(BVSUB, i, indexVar)),
+                MapAccess(memVar, i)))
+            }
+          }
         }
 
         BFunction(m.fnName, "", in, out, Some(body))
@@ -169,23 +191,38 @@ class IRToBoogie(var program: Program, var spec: Specification) {
         val in = List(gammaMapVar, indexVar, valueVar)
         val out = BParam(gammaMapType)
 
-        val indices: Seq[BExpr] = for (i <- 0 until g.accesses) yield {
-          if (i == 0) {
-            indexVar
-          } else {
-            BinaryBExpr(BVADD, indexVar, BitVecBLiteral(i, g.addressSize))
+        val body : BExpr = config.memoryFunctionType match {
+          case BoogieMemoryAccessMode.LambdaStoreSelect => {
+            if g.accesses == 1 then
+              MapUpdate(gammaMapVar, indexVar, valueVar)
+            else {
+              val i = BVariable("i", BitVecBType(g.addressSize), Scope.Local)
+              Lambda(List(i), IfThenElse(
+                BInBounds(indexVar, BitVecBLiteral(g.accesses, g.addressSize), Endian.LittleEndian, i),
+                valueVar,
+                MapAccess(gammaMapVar, i)))
+            }
+          }
+          case BoogieMemoryAccessMode.SuccessiveStoreSelect => {
+            val indices: Seq[BExpr] = for (i <- 0 until g.accesses) yield {
+              if (i == 0) {
+                indexVar
+              } else {
+                BinaryBExpr(BVADD, indexVar, BitVecBLiteral(i, g.addressSize))
+              }
+            }
+            val values: Seq[BExpr] = for (i <- 0 until g.accesses) yield {
+              valueVar
+            }
+            val indiceValues = for (i <- 0 until g.accesses) yield {
+              (indices(i), values(i))
+            }
+            indiceValues.tail.foldLeft(MapUpdate(gammaMapVar, indices.head, values.head)) {
+              (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
+            }
           }
-        }
-        val values: Seq[BExpr] = for (i <- 0 until g.accesses) yield {
-          valueVar
-        }
-        val indiceValues = for (i <- 0 until g.accesses) yield {
-          (indices(i), values(i))
         }
 
-        val body: MapUpdate = indiceValues.tail.foldLeft(MapUpdate(gammaMapVar, indices.head, values.head)) {
-          (update: MapUpdate, next: (BExpr, BExpr)) => MapUpdate(update, next._1, next._2)
-        }
 
         BFunction(g.fnName, "", in, out, Some(body))
       case l: LOp =>
@@ -214,6 +251,38 @@ class IRToBoogie(var program: Program, var spec: Specification) {
           }
         }
         BFunction("L", "", List(memoryVar, indexVar), BParam(BoolBType), Some(body))
+      case b: ByteExtract =>
+        val valueVar = BParam("value", BitVecBType(b.valueSize))
+        val offsetVar = BParam("offset", BitVecBType(b.offsetSize))
+        val in = List(valueVar, offsetVar)
+        val out = BParam(BitVecBType(8))
+        val shift = BinaryBExpr(BVMUL, offsetVar, BitVecBLiteral(8, b.offsetSize))
+        val eshift =
+          if (b.valueSize < b.offsetSize) BVExtract(b.valueSize, 0, shift)
+          else if (b.valueSize == b.offsetSize) shift
+          else BVZeroExtend(b.valueSize - b.offsetSize, shift)
+        val body = BVExtract(8, 0, BinaryBExpr(BVLSHR, valueVar, eshift))
+        BFunction(b.fnName, "", in, out, Some(body), true)
+      case b: InBounds =>
+        val baseVar = BParam("base", BitVecBType(b.bits))
+        val lenVar = BParam("len", BitVecBType(b.bits))
+        val iVar = BParam("i", BitVecBType(b.bits))
+        val in = List(baseVar, lenVar, iVar)
+        val out = BParam(BoolBType)
+        val begin = b.endian match {
+          case Endian.LittleEndian => baseVar
+          case Endian.BigEndian => BinaryBExpr(BVSUB, baseVar, lenVar)
+        }
+        val end = b.endian match {
+          case Endian.LittleEndian => BinaryBExpr(BVADD, baseVar, lenVar)
+          case Endian.BigEndian => baseVar
+        }
+
+        val above = BinaryBExpr(BVULE, begin, iVar)
+        val below = BinaryBExpr(BVULT, iVar, end)
+        val wrap = BinaryBExpr(BVULE, baseVar, end)
+        val body = IfThenElse(wrap, BinaryBExpr(BoolAND, above, below), BinaryBExpr(BoolOR, above, below))
+        BFunction(b.fnName, "", in, out, Some(body), true)
     }
   }