Read-only memory sections maintained throughout program

readme.md

@@ -197,16 +197,15 @@ The binary (i.e `*.out`) can then be generated from a C source file using:
 See [src/test/correct/liftone.sh](https://github.com/UQ-PAC/bil-to-boogie-translator/blob/main/src/test/correct/liftone.sh) for more examples
 for flag combinations that work. 
 
-## Verifying the generated boogie (the programming language), by running boogie (the progam) on the boogie (the program)
+## Verifying the generated Boogie file
 
 [Boogie](https://github.com/boogie-org/boogie#installation) can be installed by following the instructions in the given link.
 
-Boogie can be run on the output `*.bpl` file with the command `boogie *.bpl`. 
+Boogie can be run on the output `*.bpl` file with the command `boogie \useArrayAxioms *.bpl`. 
 
-A recent boogie version is needed, for example `Boogie program verifier version 2.4.1.10503, Copyright (c) 2003-2014, Microsoft.`. 
+It is recommended to use Boogie version 3.0.4 and Z3 version 4.8.8 (which is recommended by Boogie). Other versions and combinations may not have been tested.
 
-With older versions and recent versions of z3 (e.g. `Z3 version 4.8.12 - 64 bit`), Z3 emits warnings about `model_compress`, since the 
-parameter name was changed. This does not prevent it from working however. 
+The `\useArrayAxioms` flag is necessary for Boogie versions 2.16.8 and greater; for earlier versions it can be removed.
 
 Boogie can be installed through dotnet and requires dotnet 6.
 

src/main/scala/ir/Program.scala

@@ -2,13 +2,10 @@ package ir
 
 import scala.collection.mutable.ArrayBuffer
 import scala.collection.mutable
-import boogie._
+import boogie.*
+import analysis.BitVectorEval
 
-class Program(
-    var procedures: ArrayBuffer[Procedure],
-    var initialMemory: ArrayBuffer[MemorySection],
-    var mainProcedure: Procedure
-) {
+class Program(var procedures: ArrayBuffer[Procedure], var mainProcedure: Procedure, var initialMemory: ArrayBuffer[MemorySection], var readOnlyMemory: ArrayBuffer[MemorySection]) {
 
   // This shouldn't be run before indirect calls are resolved?
   def stripUnreachableFunctions(): Unit = {
@@ -33,7 +30,6 @@ class Program(
   }
 
   def setModifies(specModifies: Map[String, List[String]]): Unit = {
-
     val procToCalls: mutable.Map[Procedure, Set[Procedure]] = mutable.Map()
     for (p <- procedures) {
       p.modifies.addAll(p.blocks.flatMap(_.modifies))
@@ -83,6 +79,36 @@ class Program(
     }
   }
 
+  /**
+    * Takes all the memory sections we get from the ADT (previously in initialMemory) and restricts initialMemory to
+    * just the .data section (which contains things such as global variables which are mutable) and puts the .rodata
+    * section in readOnlyMemory. It also takes the .rela.dyn entries taken from the readelf output and adds them to the
+    * .rodata section, as they are the global offset table entries that we can assume are constant.
+    */
+  def determineRelevantMemory(rela_dyn: Map[BigInt, BigInt]): Unit = {
+    val initialMemoryNew = ArrayBuffer[MemorySection]()
+
+    val rodata = initialMemory.collect { case s if s.name == ".rodata" => s }
+    readOnlyMemory.addAll(rodata)
+
+    val data = initialMemory.collect { case s if s.name == ".data" => s }
+    initialMemoryNew.addAll(data)
+
+    // assuming little endian, adding the rela_dyn offset/address pairs like this is crude but is simplest for now
+    for ((offset, address) <- rela_dyn) {
+      val addressBV = BitVecLiteral(address, 64)
+      val bytes = for (i <- 0 to 7) yield {
+        val low = i * 8
+        val high = low + 8
+        BitVectorEval.boogie_extract(high, low, addressBV)
+      }
+      readOnlyMemory.append(MemorySection(s".got_$offset", offset.intValue, 8, bytes))
+    }
+
+    initialMemory = initialMemoryNew
+  }
+
+
 }
 
 class Procedure(
@@ -186,4 +212,10 @@ class Parameter(var name: String, var size: Int, var value: Register) {
   def toGamma: BVariable = BParam(s"Gamma_$name", BoolBType)
 }
 
-case class MemorySection(name: String, address: Int, size: Int, bytes: Seq[Literal])
+/**
+  * @param name name
+  * @param address initial offset of memory section
+  * @param size number of bytes
+  * @param bytes sequence of bytes represented by BitVecLiterals of size 8
+  */
+case class MemorySection(name: String, address: Int, size: Int, bytes: Seq[BitVecLiteral])

src/main/scala/translating/BAPToIR.scala

@@ -56,7 +56,7 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
       memorySections.append(MemorySection(m.name, m.address, m.size, bytes))
     }
 
-    Program(procedures, memorySections, mainProcedure.get)
+    Program(procedures, mainProcedure.get, memorySections, ArrayBuffer())
   }
 
   private def translate(s: BAPStatement) = s match {

src/main/scala/translating/IRToBoogie.scala

@@ -33,7 +33,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
   )
 
   def translate: BProgram = {
-    val procedures = program.procedures.map(f => translateProcedure(f))
+    val readOnlyMemory = memoryToCondition(program.readOnlyMemory)
+    val procedures = program.procedures.map(f => translateProcedure(f, readOnlyMemory))
     val defaultGlobals = List(BVarDecl(mem), BVarDecl(Gamma_mem))
     val globalVars = procedures.flatMap(p => p.globals ++ p.freeRequires.flatMap(_.globals) ++ p.freeEnsures.flatMap(_.globals) ++ p.ensures.flatMap(_.globals) ++ p.requires.flatMap(_.globals))
     val globalDecls = (globalVars.map(b => BVarDecl(b)) ++ defaultGlobals).distinct.sorted.toList
@@ -55,7 +56,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       guaranteesReflexive.map(g => BAssert(g))
     )
 
-    val rgProcs = genRely(relies) :+ guaranteeReflexive
+    val rgProcs = genRely(relies, readOnlyMemory) :+ guaranteeReflexive
 
     val functionsUsed1 =
       procedures.flatMap(p => p.functionOps).toSet ++ rgProcs.flatMap(p => p.functionOps).toSet ++ directFunctions
@@ -67,65 +68,23 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     BProgram(declarations)
   }
 
-  def genRely(relies: List[BExpr]): List[BProcedure] = {
+  def genRely(relies: List[BExpr], readOnlyMemory: List[BExpr]): List[BProcedure] = {
     val reliesUsed = if (relies.nonEmpty) {
       relies
     } else {
       // default case where no rely is given - rely on no external changes
       List(BinaryBExpr(BVEQ, mem, Old(mem)), BinaryBExpr(BVEQ, Gamma_mem, Old(Gamma_mem)))
     }
-    val i = BVariable("i", BitVecBType(64), Scope.Local)
-    val rely2 = ForAll(
-      List(i),
-      BinaryBExpr(
-        BoolIMPLIES,
-        BinaryBExpr(BVEQ, MapAccess(mem, i), Old(MapAccess(mem, i))),
-        BinaryBExpr(BVEQ, MapAccess(Gamma_mem, i), Old(MapAccess(Gamma_mem, i)))
-      )
-    )
-    val relyEnsures = List(rely2) ++ reliesUsed
-    val relyProc = BProcedure(
-      "rely",
-      List(),
-      List(),
-      relyEnsures,
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      Seq(mem, Gamma_mem),
-      List()
-    )
-    val relyTransitive = BProcedure(
-      "rely_transitive",
-      List(),
-      List(),
-      reliesUsed,
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      Seq(mem, Gamma_mem),
-      List(
-        ProcedureCall("rely", List(), List(), List(mem, Gamma_mem)),
-        ProcedureCall("rely", List(), List(), List(mem, Gamma_mem))
-      )
-    )
-    val relyReflexive = BProcedure(
-      "rely_reflexive",
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      List(),
-      Seq(),
-      reliesReflexive.map(r => BAssert(r))
-    )
+    val relyEnsures = if (relies.nonEmpty) {
+      val i = BVariable("i", BitVecBType(64), Scope.Local)
+      val rely2 = ForAll(List(i), BinaryBExpr(BoolIMPLIES, BinaryBExpr(BVEQ, MapAccess(mem, i), Old(MapAccess(mem, i))), BinaryBExpr(BVEQ, MapAccess(Gamma_mem, i), Old(MapAccess(Gamma_mem, i)))))
+      List(rely2) ++ reliesUsed
+    } else {
+      reliesUsed
+    }
+    val relyProc = BProcedure("rely", List(), List(), relyEnsures, List(), List(), List(), readOnlyMemory, List(), Seq(mem, Gamma_mem), List())
+    val relyTransitive = BProcedure("rely_transitive", List(), List(), reliesUsed, List(), List(), List(), List(), List(), Seq(mem, Gamma_mem), List(ProcedureCall("rely", List(), List(), List(mem, Gamma_mem)), ProcedureCall("rely", List(), List(), List(mem, Gamma_mem))))
+    val relyReflexive = BProcedure("rely_reflexive", List(), List(), List(), List(), List(), List(), List(), List(), Seq(), reliesReflexive.map(r => BAssert(r)))
     List(relyProc, relyTransitive, relyReflexive)
   }
 
@@ -258,39 +217,12 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     }
   }
 
-  def translateProcedure(p: Procedure): BProcedure = {
-    val in = p.in.flatMap(i => List(i.toBoogie, i.toGamma))
-
-    var outRegisters: Set[Variable] = Set()
-
-    val out = (for (o <- p.out) yield {
-      if (outRegisters.contains(o.value)) {
-        List()
-      } else {
-        outRegisters = outRegisters + o.value
-        List(o.toBoogie, o.toGamma)
-      }
-    }).flatten
-
-    outRegisters = Set()
-    val returns = (for (o <- p.out) yield {
-      if (outRegisters.contains(o.value)) {
-        List()
-      } else {
-        outRegisters = outRegisters + o.value
-        List(outParamToAssign(o))
-      }
-    }).flatten.toList
-
+  def translateProcedure(p: Procedure, readOnlyMemory: List[BExpr]): BProcedure = {
     val body = p.blocks.map(b => translateBlock(b))
-    val modifies: Seq[BVar] = p.modifies
-      .flatMap {
-        case m: Memory   => Seq(m.toBoogie, m.toGamma)
-        case r: Register => Seq(r.toBoogie, r.toGamma)
-      }
-      .toSeq
-      .sorted
-    //val modifies = Seq(mem, Gamma_mem, stack, Gamma_stack) // TODO placeholder until proper modifies analysis
+    val modifies: Seq[BVar] = p.modifies.flatMap {
+      case m: Memory => Seq(m.toBoogie, m.toGamma)
+      case r: Register => Seq(r.toBoogie, r.toGamma)
+    }.toSeq.sorted
 
     val modifiedPreserve = modifies.collect { case m: BVar if modifiedCheck.contains(m) => m }
     val modifiedPreserveEnsures: List[BExpr] = modifiedPreserve.map(m => BinaryBExpr(BoolEQ, m, Old(m))).toList
@@ -302,18 +234,12 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     val procEnsuresDirect: List[String] = ensuresDirect.getOrElse(p.name, List())
 
     val freeRequires: List[BExpr] = if (p == program.mainProcedure) {
-      initialiseMemory
+      memoryToCondition(program.initialMemory) ++ readOnlyMemory
     } else {
-      List()
+      readOnlyMemory
     }
 
-    val freeEnsures = modifiedPreserveEnsures
-
-    val inInits = if (body.isEmpty) {
-      List()
-    } else {
-      p.in.map(i => inParamToAssign(i)).toList
-    }
+    val freeEnsures = modifiedPreserveEnsures ++ readOnlyMemory
 
     BProcedure(
       p.name,
@@ -330,11 +256,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     )
   }
 
-  private def initialiseMemory: List[BExpr] = {
-    val dataSections = program.initialMemory.collect {
-      case s if s.name == ".data" || s.name == ".rodata" || s.name == ".got" => s
-    }
-    val sections = dataSections.flatMap { s =>
+  private def memoryToCondition(memory: ArrayBuffer[MemorySection]): List[BExpr] = {
+    val sections = memory.flatMap { s =>
       for (b <- s.bytes.indices) yield {
         BinaryBExpr(
           BVEQ,
@@ -346,36 +269,6 @@ class IRToBoogie(var program: Program, var spec: Specification) {
     sections.toList
   }
 
-  private def outParamToAssign(p: Parameter): AssignCmd = {
-    val param = BParam(p.name, BitVecBType(p.size))
-    val register = p.value.toBoogie
-    val paramGamma = BParam(s"Gamma_${p.name}", BoolBType)
-    val registerGamma = p.value.toGamma
-    val assigned = if (p.size > p.value.size) {
-      BVZeroExtend(p.size - p.value.size, register)
-    } else if (p.size < p.value.size) {
-      BVExtract(p.size, 0, register)
-    } else {
-      register
-    }
-    AssignCmd(List(param, paramGamma), List(assigned, registerGamma))
-  }
-
-  private def inParamToAssign(p: Parameter): AssignCmd = {
-    val param = BParam(p.name, BitVecBType(p.size))
-    val register = p.value.toBoogie
-    val paramGamma = BParam(s"Gamma_${p.name}", BoolBType)
-    val registerGamma = p.value.toGamma
-    val assigned = if (p.size > p.value.size) {
-      BVExtract(p.value.size, 0, param)
-    } else if (p.size < p.value.size) {
-      BVZeroExtend(p.value.size - p.size, param)
-    } else {
-      param
-    }
-    AssignCmd(List(register, registerGamma), List(assigned, paramGamma))
-  }
-
   def translateBlock(b: Block): BBlock = {
     val cmds = b.statements.flatMap(s => translate(s)) ++ b.jumps.flatMap(j => translate(j))
     BBlock(b.label, cmds.toList)
@@ -401,7 +294,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       val call: List[BCmd] = if (i.target.name == "R30") {
         List(ReturnCmd)
       } else {
-        val unresolved: List[BCmd] = List(Comment(s"UNRESOLVED: call ${i.target.name}"), BAssume(FalseBLiteral))
+        val unresolved: List[BCmd] = List(Comment(s"UNRESOLVED: call ${i.target.name}"), BAssert(FalseBLiteral))
         i.returnTarget match {
           case Some(r) => unresolved :+ GoToCmd(r.label)
           case None    => unresolved ++ List(Comment("no return target"), BAssume(FalseBLiteral))
@@ -477,67 +370,4 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       val body = a.body.toBoogie
       List(BAssert(body, a.comment))
   }
-
-  def coerceProcedureCall(target: Procedure): List[BCmd] = {
-    val params = for (i <- target.in) yield {
-      val register = i.value.toBoogie
-      val registerGamma = i.value.toGamma
-      if (i.value.size > i.size) {
-        List(BVExtract(i.size, 0, register), registerGamma)
-      } else if (i.value.size < i.size) {
-        List(BVZeroExtend(i.size - i.value.size, register), registerGamma)
-      } else {
-        List(register, registerGamma)
-      }
-    }
-    var outUsedRegisters: Set[Variable] = Set()
-    var outIndices: Set[Int] = Set()
-    for (o <- target.out.indices) {
-      if (!outUsedRegisters.contains(target.out(o).value)) {
-        outIndices = outIndices + o
-        outUsedRegisters = outUsedRegisters + target.out(o).value
-      }
-    }
-
-    val outTemp = for (o <- target.out.indices) yield {
-      BVariable(s"#temp$o", BitVecBType(target.out(o).size), Scope.Local)
-    }
-    val outTempGamma = for (o <- target.out.indices) yield {
-      BVariable(s"Gamma_#temp$o", BoolBType, Scope.Local)
-    }
-    val outRegisters = target.out.map(o => o.value.toBoogie)
-    val outRegisterGammas = target.out.map(o => o.value.toGamma)
-    val outAssigned = for (
-      o <- target.out.indices if target.out(o).value.size != target.out(o).size && outIndices.contains(o)
-    ) yield {
-      val regSize = target.out(o).value.size
-      val paramSize = target.out(o).size
-      if (regSize > paramSize) {
-        AssignCmd(
-          List(outRegisters(o), outRegisterGammas(o)),
-          List(BVZeroExtend(regSize - paramSize, outTemp(o)), outTempGamma(o))
-        )
-      } else {
-        AssignCmd(List(outRegisters(o), outRegisterGammas(o)), List(BVExtract(regSize, 0, outTemp(o)), outTempGamma(o)))
-      }
-    }
-
-    val returned = for (o <- target.out.indices if outIndices.contains(o)) yield {
-      if (target.out(o).value.size == target.out(o).size) {
-        List(outRegisters(o), outRegisterGammas(o))
-      } else {
-        List(outTemp(o), outTempGamma(o))
-      }
-    }
-    List(ProcedureCall(target.name, returned.flatten.toList, params.flatten.toList, List())) ++ outAssigned
-  }
-
-  /*
-  private val reserved = Set("free")
-
-  def avoidReserved(program: BProgram): BProgram = {
-    program.replaceReserved(reserved)
-  }
-   */
-
 }