cleanup

UQ-PAC · Jan 31, 2024 · c0b3e5b · c0b3e5b
1 parent 7e2c123
commit c0b3e5b
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 7 deletions.
diff --git a/src/main/scala/ir/Program.scala b/src/main/scala/ir/Program.scala
@@ -329,6 +329,23 @@ class Block private (
 
   def jump: Jump = _jump
 
+
+  def jump_=(j: Call): Unit = {
+    if (j ne _jump) {
+      _jump.deParent()
+      _jump match {
+        case c: IndirectCall => c.returnTarget.filter(b=>b.kind.isInstanceOf[AfterCall]).map(b => parent.removeBlocks(b))
+        case c: DirectCall => c.returnTarget.filter(b=>b.kind.isInstanceOf[AfterCall]).map(b => parent.removeBlocks(b))
+      }
+      _jump = j
+      _jump.parent = this
+      j match {
+        case c: IndirectCall => c.returnTarget = Some(parent.addBlocks(Block.afterCall(c)))
+        case c: DirectCall => c.returnTarget = Some(parent.addBlocks(Block.afterCall(c)))
+      }
+    }
+  }
+
   def jump_=(j: Jump): Unit = {
     if (j ne _jump) {
       _jump.deParent()
@@ -347,9 +364,9 @@ class Block private (
     }
   }
 
+
   def replaceJump(j: Jump) = {
     jump = j
-    assert(jump.parent eq this)
     this
   }
 
@@ -460,10 +477,7 @@ object Block:
       case d: DirectCall => GoTo(d.returnTarget.toSet)
       case c: IndirectCall => GoTo(c.returnTarget.toSet)
 
-    jump.parent = from.parent
-    val ac = Block(AfterCall(from), from.parent.label + "_basil_aftercall", None, Seq(), jump)
-    ac.parent = from.parent.parent
-    ac
+    Block(AfterCall(from), from.parent.label + "_basil_aftercall", None, Seq(), jump)
   }
 
   def procedureReturn(from: Procedure): Block = {

diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
@@ -96,10 +96,10 @@ object RunUtils {
     val renamer = Renamer(reserved)
     val returnUnifier = ConvertToSingleProcedureReturn()
     val callReturner = AddCallReturnBlocks()
-    IRProgram = callReturner.visitProgram(IRProgram)
     IRProgram = externalRemover.visitProgram(IRProgram)
     IRProgram = renamer.visitProgram(IRProgram)
     IRProgram = returnUnifier.visitProgram(IRProgram)
+    IRProgram = callReturner.visitProgram(IRProgram)
 
 
     q.loading.dumpIL.foreach(s => writeToFile(serialiseIL(IRProgram), s"$s-before-analysis.il"))

diff --git a/src/test/scala/SystemTests.scala b/src/test/scala/SystemTests.scala
@@ -104,7 +104,7 @@ class SystemTests extends AnyFunSuite {
       (verified, shouldVerify, xor(verified, proveFailed)) match {
         case (true, true, true) =>   "Test passed"
         case (false , false, true) => "Test passed"
-        case (_, _, false) => "Prover error: unknown result"
+        case (_, _, false) => "Prover error: unknown result: " + boogieResult
         case (true, false, true) => "Expected verification failure, but got success."
         case (false, true, true) => "Expected verification success, but got failure."
     }