blah procedure param big fix !!!

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

Author: katrinafyi

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

@@ -160,7 +160,8 @@ 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 +396,25 @@ 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 +544,49 @@ 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 +595,10 @@ 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  =>
+        println("sad")
+        println(b)
+        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 =>
+        println(b)
+        ???
     }
   }
 
-  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/Simp.scala

@@ -567,11 +567,11 @@ class GuardVisitor(validate: Boolean = false) extends CILVisitor {
 
   /**
    *
-   * This takes all variables in guards and substitutes them for their definitions IFF they have 
+   * This takes all variables in guards and substitutes them for their definitions IFF they have
    * exactly one definition (Assuming DSA form).
    *
    * Due to dsa form this heuristic alone should prevent any copies across loop iterations / clobbers etc
-   * because transitively all definitions should dominate the use (the assume statement) we are propagating to. 
+   * because transitively all definitions should dominate the use (the assume statement) we are propagating to.
    *
    * The [[validate]] parameter further checks this is the case by checking the dsa property is preserved
    * by the propagation, by checking the reaching-definitions set at the use site.
@@ -884,11 +884,13 @@ def removeInvariantOutParameters(
     val proc = ret.parent.parent
     val inParams = proc.formalInParam.toSet
 
+    val specDependencies : Set[Variable] = proc.ensuresExpr.flatMap(_.variables).toSet
+
     val doneAlready = alreadyInlined.getOrElse(proc, Set())
     var doneNow = Set[Variable]()
     var toRename = Map[Variable, LocalVar]()
 
-    val invariantParams = ret.outParams.collect {
+    val invariantParams = ret.outParams.filterNot(x => specDependencies.contains(x._1)).collect {
       // we are returning a constant and can inline
       case (formalOut, binding: Literal) => (formalOut, binding)
       // we are returning the input parameter with the same name as the output parameter so can inline at callsite
@@ -1461,7 +1463,7 @@ class ExprComplexity extends CILVisitor {
   * @param complexityThreshold
   *   Stop substituting after the AST node count has increased by this much
   *
-  *  TODO: The recursive substitution here is a broken when res produces substitution loops. 
+  *  TODO: The recursive substitution here is a broken when res produces substitution loops.
   *  I want a substituter that takes a set of replacements to a canonical
   *  closure under substitution, but is more subtle to implement than it initially appears.
   *  One possibility is a union find on the set of rewrites to partition cycles it into canonical representative

src/main/scala/translating/IRToBoogieNoVC.scala

@@ -113,8 +113,8 @@ object BoogieTranslator {
       e.name,
       inparams,
       outparams,
-      e.requires ++ e.requiresExpr.map(translateExpr),
       e.ensures ++ e.ensuresExpr.map(translateExpr),
+      e.requires ++ e.requiresExpr.map(translateExpr),
       List(),
       List(),
       freeEnsures.toList,
@@ -149,18 +149,21 @@ object BoogieTranslator {
     val vvis = FindVars()
     visit_prog(vvis, p)
 
-    val globalVarDecls = vvis.globals.map(translateGlobal).map(BVarDecl(_))
 
     val readOnlySections = p.usedMemory.values.filter(_.readOnly)
     val readOnlyMemory = memoryToConditionCoalesced(readOnlySections)
     val initialSections = p.usedMemory.values.filter(!_.readOnly)
     val initialMemory = memoryToConditionCoalesced(initialSections)
 
+    val memGlobals = (readOnlyMemory ++ initialMemory).flatMap(_.globals).map(BVarDecl(_))
+    val globalVarDecls = vvis.globals.map(translateGlobal).map(BVarDecl(_)) ++ memGlobals
+
     val procs = p.procedures.map {
       case proc if p.mainProcedure eq proc => translateProc(initialMemory ++ readOnlyMemory)(proc)
       case proc => translateProc(readOnlyMemory)(proc)
     }
 
+
     val functionOpDefinitions = functionOpToDecl(globalVarDecls ++ procs)
     val decls = globalVarDecls.toList ++ functionOpDefinitions ++ procs
 

src/main/scala/util/RunUtils.scala

@@ -1166,22 +1166,25 @@ object RunUtils {
     val pcSubSpecs = proceduresWithPCs
       .map((proc, addr) => {
         // XXX: this does NOT work with parameter form! because the variables are changed
-        val pcVar = BVariable("_PC", BitVecBType(64), Scope.Global)
-        val r30Var = BVariable("R30", BitVecBType(64), Scope.Global)
-        val addrVar = BitVecBLiteral(addr, 64)
-        val pcRequires = BinaryBExpr(ir.EQ, pcVar, addrVar)
-        val pcEnsures = BinaryBExpr(ir.EQ, pcVar, Old(r30Var))
+        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))
 
         val name = proc.procName
-        (name -> SubroutineSpec(name, requires = List(pcRequires), ensures = List(pcEnsures)))
+        proc.requiresExpr = pcRequires +: proc.requiresExpr
+        proc.ensuresExpr = pcEnsures +: proc.ensuresExpr
+        (name -> SubroutineSpec(name, requires = List(), ensures = List()))
       })
       .toMap
 
     val subSpecs = spec.subroutines.map(x => x.name -> x).toMap
 
     val newSubroutineSpecs = util.functional.unionWith(pcSubSpecs, subSpecs, _ merge _)
 
-    spec.copy(subroutines = newSubroutineSpecs.values.toList)
+    // spec.copy(subroutines = newSubroutineSpecs.values.toList)
+    spec
   }
 }