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

@@ -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)
             }
           }
@@ -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

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
@@ -471,6 +474,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

@@ -21,8 +21,8 @@ case class BProcedure(
     freeRequires: List[BExpr],
     modifies: Set[BVar],
     body: List[BCmdOrBlock],
-    override val attributes: List[BAttribute]
-) extends BDeclaration()
+    override val attributes: List[BAttribute] = List()
+) extends BDeclaration
     with Ordered[BProcedure] {
   override def compare(that: BProcedure): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
@@ -43,7 +43,7 @@ case class BProcedure(
     val freeRequiresStrs = freeRequires.map(r => s"  free requires $r;")
     val freeEnsuresStrs = freeEnsures.map(e => s"  free ensures $e;")
     val locals = body.flatMap(l => l.locals).distinct.sorted
-    val localDefs = locals.map(l => "  " + BVarDecl(l, List.empty).toString)
+    val localDefs = locals.map(l => "  " + BVarDecl(l).toString)
     val bodyStr = if (body.nonEmpty) {
       List("{") ++ localDefs ++ body.flatMap(x => x.toBoogie).map(s => "  " + s) ++ List("}")
     } else {
@@ -62,15 +62,14 @@ case class BProcedure(
   def globals: Set[BVar] = body.flatMap(c => c.globals).toSet ++ modifies
 }
 
-case class BAxiom(body: BExpr, override val attributes: List[BAttribute]) extends BDeclaration() {
+case class BAxiom(body: BExpr, override val attributes: List[BAttribute] = List()) extends BDeclaration {
   override def toString: String = s"axiom $attrString$body;"
 }
 
 case class BFunction(name: String, in: List[BVar], out: BVar, body: Option[BExpr],
-                     override val attributes: List[BAttribute])
-    extends BDeclaration()
+                     override val attributes: List[BAttribute] = List())
+    extends BDeclaration
     with Ordered[BFunction] {
-
   override def compare(that: BFunction): Int = name.compare(that.name)
   override def toBoogie: List[String] = {
     val inString = in.map(_.withType).mkString(", ")
@@ -87,7 +86,7 @@ case class BFunction(name: String, in: List[BVar], out: BVar, body: Option[BExpr
   }
 }
 
-case class BVarDecl(variable: BVar, override val attributes: List[BAttribute]) extends BDeclaration() with Ordered[BVarDecl] {
+case class BVarDecl(variable: BVar, override val attributes: List[BAttribute] = List()) extends BDeclaration with Ordered[BVarDecl] {
   def compare(that: BVarDecl): Int = variable.compare(that.variable)
   override def toString: String = if (variable.scope == Scope.Const) {
     s"const $attrString$variable: ${variable.getType};"
@@ -96,7 +95,7 @@ case class BVarDecl(variable: BVar, override val attributes: List[BAttribute]) e
   }
 }
 
-case class BConstAxiomPair(const: BVarDecl, axiom: BAxiom) extends BDeclaration() with Ordered[BConstAxiomPair] {
+case class BConstAxiomPair(const: BVarDecl, axiom: BAxiom) extends BDeclaration with Ordered[BConstAxiomPair] {
   override def compare(that: BConstAxiomPair): Int = const.compare(that.const)
   override def toString: String = const.toString + "\n" + axiom.toString
 }