add bigendian support for lambda stores

UQ-PAC · Oct 24, 2023 · 55b1911 · 55b1911
1 parent ff0049a
commit 55b1911
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 14 deletions.
diff --git a/src/main/scala/boogie/BExpr.scala b/src/main/scala/boogie/BExpr.scala
@@ -508,11 +508,14 @@ case class BByteExtract(value: BExpr, offset: BExpr) extends BExpr {
  *
  * Assumes all inputs are of the same bitvector width.
  */
-case class InBounds(bits: Int) extends FunctionOp {
-  val fnName: String = s"in_bounds$bits"
+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, i: BExpr) extends BExpr {
+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 {
@@ -524,7 +527,7 @@ case class BInBounds(base: BExpr, len: BExpr, i: BExpr) extends BExpr {
 
   override val getType: BType = BoolBType
   override def functionOps: Set[FunctionOp] =
-    base.functionOps ++ len.functionOps ++ i.functionOps + InBounds(baseSize)
+    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 

diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala
@@ -62,7 +62,6 @@ class IRToBoogie(var program: Program, var spec: Specification) {
 
     val rgProcs = genRely(relies, readOnlyMemory) :+ guaranteeReflexive
 
-    // TODO: Fixed point
     val functionsUsed1 =
       procedures.flatMap(p => p.functionOps).toSet ++
       rgProcs.flatMap(p => p.functionOps).toSet ++
@@ -176,7 +175,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
             else {
               val i = BVariable("i", BitVecBType(m.addressSize), Scope.Local)
               Lambda(List(i), IfThenElse(
-                BInBounds(indexVar, BitVecBLiteral(m.accesses, m.addressSize), i),
+                BInBounds(indexVar, BitVecBLiteral(m.accesses, m.addressSize), m.endian, i),
                 BByteExtract(valueVar, BinaryBExpr(BVSUB, i, indexVar)),
                 MapAccess(memVar, i)))
             }
@@ -199,7 +198,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
             else {
               val i = BVariable("i", BitVecBType(g.addressSize), Scope.Local)
               Lambda(List(i), IfThenElse(
-                BInBounds(indexVar, BitVecBLiteral(g.accesses, g.addressSize), i),
+                BInBounds(indexVar, BitVecBLiteral(g.accesses, g.addressSize), Endian.LittleEndian, i),
                 valueVar,
                 MapAccess(gammaMapVar, i)))
             }
@@ -270,8 +269,16 @@ class IRToBoogie(var program: Program, var spec: Specification) {
         val iVar = BParam("i", BitVecBType(b.bits))
         val in = List(baseVar, lenVar, iVar)
         val out = BParam(BoolBType)
-        val end = BinaryBExpr(BVADD, baseVar, lenVar)
-        val above = BinaryBExpr(BVULE, baseVar, iVar)
+        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))

diff --git a/src/main/scala/util/BASILConfig.scala b/src/main/scala/util/BASILConfig.scala
@@ -1,10 +1,5 @@
 package util
 
-/**
- * We use 'quirks' to manage the operation mode of the tool e.g. for a-b testing or compiler options.
- */
-
-
 case class ILLoadingConfig(adtFile: String, relfFile: String, specFile: Option[String], dumpIL: Option[String])
 case class BoogieGeneratorConfig(memoryFunctionType: BoogieMemoryAccessMode = BoogieMemoryAccessMode.SuccessiveStoreSelect)
 case class StaticAnalysisConfig(dumpILToPath: Option[String] = None)