track PC and assert at beginning of blocks (#387)

* feat: maintain program counter and assert at beginning of blocks

this makes a fairly significant change to the GTIRB loader by inserting
PC increment statements after instructions and checking the PC at the
entry of blocks. this is done by changing the loader to maintain PC and
branchtaken assignments, and inserting a default increment if there is
no branch.

* apportion TempIf statements into successor blocks, then remove TempIf

this fixes the problemetic cross pattern we saw, where there were extra
blocks inserted before the original successor blocks.

* add RemoveUnreachableBlocks pass to clean up padding blocks



* move RemovePCStatements into load()

this fixes the DifferentialAnalysisTest seeing program counters
in its loaded IR, but it is maybe undesirable to do a transformation
in the load() method.

regardless, the current approach (of keep PC, then remove if unwanted)
seems to necessitate this, as later parts of the runutils pipeline
make assumptions that PC wont be present and fail in unexpected ways
otherwise.

* add back RemoveUnreachableBlocks to loadAndTranslate

* update expected. some differences in memory sizes and function inlining?

* change --pc argument to an enum

* implement Assert feature, use requires/ensures instead of assume

* use "pc-tracking" label

* scalafmt

* add PCTrackingTest, using a test case which has a runtime-dependent branch

* inject requires/ensures through Specification logic

to hopefully make sure it's picked up by the parameter form transform.
despite this, it looks like it still is not working.

---------

Co-authored-by: am <[email protected]>

Author: katrinafyi

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()
+    }
+  }
+}