track PC and assert at beginning of blocks

src/main/scala/Main.scala

@@ -153,6 +153,11 @@ object Main {
     generateRelyGuarantees: Flag,
     @arg(name = "simplify", doc = "Partial evaluate / simplify BASIL IR before output (implies --parameter-form)")
     simplify: Flag,
+    @arg(
+      name = "pc",
+      doc = "Program counter mode, supports GTIRB only. (options: none | keep | assert) (default: none)"
+    )
+    pcTracking: Option[String],
     @arg(
       name = "validate-simplify",
       doc = "Emit SMT2 check for validation of simplification expression rewrites 'rewrites.smt2'"
@@ -253,7 +258,8 @@ object Main {
         case Some("prereq") => Some(Prereq)
         case Some("checks") => Some(Checks)
         case Some("standard") => Some(Standard)
-        case None => Some(Standard)
+        case Some("none") => None
+        case None => None
         case Some(_) =>
           throw new IllegalArgumentException("Illegal option to dsa, allowed are: (prereq|standard|checks)")
     } else {
@@ -289,7 +295,8 @@ object Main {
         mainProcedureName = conf.mainProcedureName,
         procedureTrimDepth = conf.procedureDepth,
         parameterForm = conf.parameterForm.value,
-        trimEarly = conf.trimEarly.value
+        trimEarly = conf.trimEarly.value,
+        pcTracking = PCTrackingOption.valueOf(conf.pcTracking.getOrElse("none").capitalize)
       ),
       runInterpret = conf.interpret.value,
       simplify = conf.simplify.value,
@@ -308,18 +315,11 @@ object Main {
       assert(result.boogie.nonEmpty)
       var failed = false
       for (b <- result.boogie) {
-        val fname = b.filename
-        val timer = PerformanceTimer("Verify", LogLevel.INFO)
-        val cmd = Seq("boogie", "/useArrayAxioms", fname)
-        Logger.info(s"Running: ${cmd.mkString(" ")}")
-        val output = cmd.!!
-        val result = util.boogie_interaction.parseOutput(output)
+        val result = b.verifyBoogie(b.filename)
         result.kind match {
           case BoogieResultKind.Verified(c, _) if c > 0 => ()
           case _ => failed = true
         }
-        Logger.info(result.toString)
-        timer.checkPoint("Finish")
       }
       if (failed) {
         throw Exception("Verification failed")

src/main/scala/boogie/BProgram.scala

@@ -1,12 +1,47 @@
 package boogie
-import java.io.{StringWriter, Writer}
+
+import util.{PerformanceTimer, Logger, LogLevel}
+
+import scala.sys.process.*
+import scala.collection.immutable.Seq
+
+import java.io.{StringWriter, Writer, BufferedWriter, FileWriter}
+import java.nio.file.{Files, Paths}
 
 case class BProgram(declarations: List[BDeclaration], filename: String) {
   override def toString: String = declarations.flatMap(x => x.toBoogie).mkString(System.lineSeparator())
 
   def writeToString(w: Writer): Unit = {
     declarations.foreach(x => x.writeToString(w))
   }
+
+  /**
+   * Invokes Boogie to verify the current BProgram.
+   */
+  def verifyBoogie(fname: String = "") = {
+    val temp =
+      if !fname.isEmpty then Paths.get(fname)
+      else Files.createTempFile("basil-boogie-temp", ".bpl")
+
+    val wr = BufferedWriter(FileWriter(temp.toFile))
+    try {
+      writeToString(wr)
+    } finally {
+      wr.close()
+    }
+
+    val timer = PerformanceTimer("Verify", LogLevel.INFO)
+    val cmd = Seq("boogie", "/useArrayAxioms", temp.toString)
+    Logger.info(s"Running: ${cmd.mkString(" ")}")
+
+    val output = cmd.!!
+    val result = util.boogie_interaction.parseOutput(output)
+
+    Logger.info(result.toString)
+    timer.checkPoint("Finish")
+
+    result
+  }
 }
 
 trait BDeclaration extends HasAttributes {

src/main/scala/ir/transforms/PCTracking.scala

@@ -0,0 +1,50 @@
+package ir.transforms
+
+import util.{Logger, PCTrackingOption}
+import ir.*
+
+object PCTracking {
+
+  def applyPCTracking(mode: PCTrackingOption, program: Program): Unit = {
+
+    // convenience variable to hold all procedures with defined program counters.
+    val proceduresWithPCs = program.procedures.collect {
+      case p if p.address.isDefined => (p, p.address.get)
+    }
+
+    mode match {
+      case PCTrackingOption.None =>
+        program.collect {
+          case x: Statement if x.label == Some("pc-tracking") =>
+            x.parent.statements.remove(x)
+
+          // note: direct jumps are from aslp and so do not have the pc-tracking tag
+          case x @ LocalAssign(Register("_PC", 64), _, _) =>
+            x.parent.statements.remove(x)
+        }
+        Logger.info(s"[!] Removed all PC-related statements")
+
+      case PCTrackingOption.Keep =>
+        Logger.info(s"[!] Removing PC-tracking assertion statements, keeping PC assignments")
+        program.collect { case x @ Assert(_, _, Some("pc-tracking")) =>
+          x.parent.statements.remove(x)
+        }
+      case PCTrackingOption.Assert =>
+        Logger.info(s"[!] Inserting PC-tracking requires/ensures")
+
+        // extra requires/ensures clauses for maintaining PC
+        proceduresWithPCs.foreach((proc, addr) => {
+          val pcVar = Register("_PC", 64)
+          val r30Var = Register("R30", 64)
+          val addrVar = BitVecLiteral(addr, 64)
+
+          val pcRequires = BinaryExpr(ir.EQ, pcVar, addrVar)
+          val pcEnsures = BinaryExpr(ir.EQ, pcVar, OldExpr(r30Var))
+
+          proc.requiresExpr = pcRequires +: proc.requiresExpr
+          proc.ensuresExpr = pcEnsures +: proc.ensuresExpr
+        })
+    }
+  }
+
+}

src/main/scala/ir/transforms/ProcedureParameters.scala

@@ -160,7 +160,10 @@ def liftProcedureCallAbstraction(ctx: util.IRContext): util.IRContext = {
 
   while (removeDeadInParams(ctx.program)) {}
 
-  ctx.copy(specification = specToProcForm(ctx.specification, formalParams.mappingInparam, formalParams.mappingOutparam))
+  ctx.program.procedures.foreach(SpecFixer.updateInlineSpec(formalParams.mappingInparam, formalParams.mappingOutparam))
+  ctx.copy(specification =
+    SpecFixer.specToProcForm(ctx.specification, formalParams.mappingInparam, formalParams.mappingOutparam)
+  )
 }
 
 def clearParams(p: Program) = {
@@ -395,22 +398,24 @@ def inOutParams(
 
   val alwaysReturnParams = (0 to 7).map(i => Register(s"R$i", 64))
 
+  val pc = Register("_PC", 64)
+
   val inout = readWrites.collect {
     case (proc, rws) if p.mainProcedure == proc => {
       // no callers of main procedure so keep the whole read/write set
       // of registers
 
       val outParams = (overapprox.intersect(DefinedOnAllPaths.proc(proc)))
       val inParams = lives(proc)._1
-      proc -> (inParams, outParams)
+      proc -> (inParams + pc, outParams + pc)
     }
     case (proc, rws) => {
       val liveStart = lives(proc)._1
       val liveEnd = lives(proc)._2 ++ alwaysReturnParams
 
       val outParams = liveEnd.intersect(rws.writes)
       val inParams = liveStart
-      proc -> (inParams, outParams)
+      proc -> (inParams + pc, outParams + pc)
     }
   }.toMap
 
@@ -540,18 +545,51 @@ class SetActualParams(
 
 }
 
-def specToProcForm(
-  spec: Specification,
-  mappingInparam: Map[Procedure, Map[LocalVar, Variable]],
-  mappingOutparam: Map[Procedure, Map[LocalVar, Variable]]
-): Specification = {
+object SpecFixer {
   import boogie.*
 
-  def toNameMapping(v: Map[LocalVar, Variable]): Map[String, String] = {
-    v.map(v => (v._2.name, v._1.name)) ++ v.map(v => ("Gamma_" + v._2.name, "Gamma_" + v._1.name))
+  class ExprToOld(varInPre: Map[String, Variable], varInPost: Map[String, Variable], initIsPost: Boolean = false)
+      extends CILVisitor {
+
+    var isPost = initIsPost
+
+    override def vexpr(e: Expr) = e match {
+      case OldExpr(inner) if !isPost => {
+        throw Exception("nested Old or Old in single-state context")
+      }
+      case OldExpr(inner) if isPost => {
+        isPost = false
+        ChangeDoChildrenPost(
+          inner,
+          e => {
+            isPost = true
+            e
+          }
+        )
+      }
+      case _ => DoChildren()
+    }
+
+    def changeVar(v: Variable) = {
+      val repl = v match {
+        case l: Variable if isPost && varInPost.contains(l.name) => varInPost(l.name)
+        case l: Variable if varInPre.contains(l.name) => varInPre(l.name)
+        case o => o
+      }
+      ChangeTo(repl)
+    }
+
+    override def vlvar(v: Variable) = changeVar(v)
+    override def vrvar(v: Variable) = changeVar(v)
+
+  }
+
+  def convVarToOldExpr(varInPre: Map[String, Variable], varInPost: Map[String, Variable], isPost: Boolean = false)(
+    b: Expr
+  ): Expr = {
+    val visitor = ExprToOld(varInPre, varInPost, isPost)
+    visit_expr(visitor, b)
   }
-  val varToInVar: Map[String, Map[String, String]] = mappingInparam.map(p => (p._1.procName -> toNameMapping(p._2)))
-  val varToOutVar: Map[String, Map[String, String]] = mappingOutparam.map(p => (p._1.procName -> toNameMapping(p._2)))
 
   def convVarToOld(varInPre: Map[String, String], varInPost: Map[String, String], isPost: Boolean = false)(
     b: BExpr
@@ -560,7 +598,7 @@ def specToProcForm(
     b match {
       case b: BVariable if isPost && varInPost.contains(b.name) => BVariable(varInPost(b.name), b.getType, b.scope)
       case b: BVariable if !isPost && varInPre.contains(b.name) => BVariable(varInPre(b.name), b.getType, b.scope)
-      case b: BVar => b
+      case b: BVariable if !isPost => b
       // case b : _ => varToOld(b)
       case b: BLiteral => b
       case b: BVExtract => b.copy(body = varToOld(b.body))
@@ -590,20 +628,61 @@ def specToProcForm(
       case b: GammaStore => b.copy(index = varToOld(b.index), value = varToOld(b.value))
       case b: L => b.copy(index = varToOld(b.index))
       case b: SpecVar => b
+      case b: BVar =>
+        ???
     }
   }
 
-  val ns = spec.copy(subroutines = spec.subroutines.map(s => {
-    if (s.requires.nonEmpty || s.ensures.nonEmpty) {
-      val in = varToInVar(s.name)
-      val out = varToOutVar(s.name)
-      s.copy(
-        requires = s.requires.map(convVarToOld(in, out, false)),
-        ensures = s.ensures.map(convVarToOld(in, out, true))
-      )
-    } else {
-      s
+  def updateInlineSpec(
+    mappingInparam: Map[Procedure, Map[LocalVar, Variable]],
+    mappingOutparam: Map[Procedure, Map[LocalVar, Variable]]
+  )(p: Procedure) = {
+
+    def toNameMapping(v: Map[LocalVar, Variable]): Map[String, String] = {
+      v.map(v => (v._2.name, v._1.name)) ++ v.map(v => ("Gamma_" + v._2.name, "Gamma_" + v._1.name))
     }
-  }))
-  ns
+
+    val varToInVar = mappingInparam.map(p => (p._1 -> toNameMapping(p._2)))
+    val varToOutVar = mappingOutparam.map(p => (p._1 -> toNameMapping(p._2)))
+
+    p.requires = p.requires.map(convVarToOld(varToInVar(p), varToOutVar(p), false))
+    p.ensures = p.ensures.map(convVarToOld(varToInVar(p), varToOutVar(p), true))
+
+    def toVarMapping(v: Map[LocalVar, Variable]): Map[String, Variable] = {
+      v.map(v => (v._2.name, v._1))
+    }
+
+    p.requiresExpr =
+      p.requiresExpr.map(convVarToOldExpr(toVarMapping(mappingInparam(p)), toVarMapping(mappingOutparam(p)), false))
+    p.ensuresExpr =
+      p.ensuresExpr.map(convVarToOldExpr(toVarMapping(mappingInparam(p)), toVarMapping(mappingOutparam(p)), true))
+
+  }
+
+  def specToProcForm(
+    spec: Specification,
+    mappingInparam: Map[Procedure, Map[LocalVar, Variable]],
+    mappingOutparam: Map[Procedure, Map[LocalVar, Variable]]
+  ): Specification = {
+
+    def toNameMapping(v: Map[LocalVar, Variable]): Map[String, String] = {
+      v.map(v => (v._2.name, v._1.name)) ++ v.map(v => ("Gamma_" + v._2.name, "Gamma_" + v._1.name))
+    }
+    val varToInVar: Map[String, Map[String, String]] = mappingInparam.map(p => (p._1.procName -> toNameMapping(p._2)))
+    val varToOutVar: Map[String, Map[String, String]] = mappingOutparam.map(p => (p._1.procName -> toNameMapping(p._2)))
+
+    val ns = spec.copy(subroutines = spec.subroutines.map(s => {
+      if (s.requires.nonEmpty || s.ensures.nonEmpty) {
+        val in = varToInVar(s.name)
+        val out = varToOutVar(s.name)
+        s.copy(
+          requires = s.requires.map(convVarToOld(in, out, false)),
+          ensures = s.ensures.map(convVarToOld(in, out, true))
+        )
+      } else {
+        s
+      }
+    }))
+    ns
+  }
 }

src/main/scala/ir/transforms/RemovePCStatements.scala

@@ -0,0 +1,15 @@
+package ir.transforms
+
+import ir.*
+import ir.cilvisitor.*
+
+class RemovePCStatements extends CILVisitor {
+  override def vstmt(s: Statement) = {
+    val vars = allVarsPos(s)
+    if (vars.contains(Register("_PC", 64))) {
+      ChangeTo(List())
+    } else {
+      SkipChildren()
+    }
+  }
+}