Eval option in debugger and better eval of field accesses for basic chunks

marcoeilers · marcoeilers · commit c23329600ee1 · 2024-12-09T17:17:44.000+01:00
diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala
@@ -280,8 +280,8 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     while (true) {
       println(s"\nEnter 'q' to quit, 'z' to zoom in on (i.e., show all children of) an assumption, " +
         s"'r' to reset the proof obligation, 'ra' to remove assumptions, 'af' to add free assumptions, " +
-        s"'ap' prove additional assumptions, 'p' to execute proof, 'c' to change print configuration, " +
-        s"'s' to change the SMT solver, 't' to change the timeout")
+        s"'ap' prove additional assumptions, 'e' to evaluate an expression, 'p' to execute proof, " +
+        s"'c' to change print configuration, 's' to change the SMT solver, 't' to change the timeout")
       try {
         val userInput = readLine()
         userInput.toLowerCase match {
@@ -306,6 +306,8 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
           //  obl = chooseAssertion(obl)
           //  println(s"Current obligation:\n$obl")
           //  assertProofObligation(obl)
+          case "e" | "eval" =>
+            obl = evalExpr(obl)
           case "p" | "prove" =>
             assertProofObligation(obl)
           case "c" | "config" =>
@@ -399,8 +401,8 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     if (userInput.isEmpty || userInput.equalsIgnoreCase("s") || userInput.equalsIgnoreCase("skip")) {
       obl
     } else {
-      val assumptionE = translateStringToExp(userInput, obl)
-      evalAssumption(assumptionE, obl, free, obl.v) match {
+      val assumptionE = translateStringToExp(userInput, obl, true)
+      evalAssumption(assumptionE, obl, true, free, obl.v) match {
         case Some((resS, resT, resE, evalAssumptions)) =>
           val allAssumptions = obl.assumptionsExp ++ evalAssumptions + DebugExp.createInstance(assumptionE, resE).withTerm(resT)
           obl.copy(s = resS, assumptionsExp = allAssumptions)
@@ -410,13 +412,32 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     }
   }
 
+  private def evalExpr(obl: ProofObligation): ProofObligation = {
+    println(s"Enter the expression you want to evaluate:")
+    val userInput = readLine()
+    if (userInput.isEmpty || userInput.equalsIgnoreCase("s") || userInput.equalsIgnoreCase("skip")) {
+      obl
+    } else {
+      val assumptionE = translateStringToExp(userInput, obl, false)
+      evalAssumption(assumptionE, obl, false, false, obl.v) match {
+        case Some((resS, resT, resE, evalAssumptions)) =>
+          println("Evaluation successful!")
+          println("Result: " + resE.toString)
+          println("Internal result term:" + resT.toString)
+          obl.copy(s = resS)
+        case None =>
+          obl
+      }
+    }
+  }
+
   private def chooseAssertion(obl: ProofObligation): ProofObligation = {
     println(s"Enter the assertion or s(skip) to assert the previous assertion again:")
     val userInput = readLine()
     if (userInput.equalsIgnoreCase("s") || userInput.equalsIgnoreCase("skip")) {
       obl
     } else {
-      val assertionE = translateStringToExp(userInput, obl)
+      val assertionE = translateStringToExp(userInput, obl, true)
       var resT: Term = null
       var resE: ast.Exp = null
       var resV: Verifier = null
@@ -436,7 +457,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     }
   }
 
-  private def translateStringToExp(str: String, obl: ProofObligation): ast.Exp ={
+  private def translateStringToExp(str: String, obl: ProofObligation, expectBool: Boolean): ast.Exp ={
     def parseToPExp(): PExp = {
       try {
         val fp = new DebugParser()
@@ -453,7 +474,10 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     def typecheckPExp(pexp: PExp): Unit = {
       try {
         obl.resolver.typechecker.names.check(pexp, None, obl.resolver.typechecker.curMember)
-        obl.resolver.typechecker.check(pexp, PPrimitiv(PReserved(PKw.Bool)((NoPosition, NoPosition)))())
+        if (expectBool)
+          obl.resolver.typechecker.check(pexp, PPrimitiv(PReserved(PKw.Bool)((NoPosition, NoPosition)))())
+        else
+          obl.resolver.typechecker.checkTopTyped(pexp, None)
       } catch {
         case e: Throwable => println(s"Error while typechecking $str: ${e.getMessage}")
           throw e
@@ -480,7 +504,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     translatePExp(pexp)
   }
 
-  private def evalAssumption(e: ast.Exp, obl: ProofObligation, isFree: Boolean, v: Verifier): Option[(State, Term, ast.Exp, InsertionOrderedSet[DebugExp])] = {
+  private def evalAssumption(e: ast.Exp, obl: ProofObligation, assume: Boolean, isFree: Boolean, v: Verifier): Option[(State, Term, ast.Exp, InsertionOrderedSet[DebugExp])] = {
     var resT: Term = null
     var resS: State = null
     var resE: ast.Exp = null
@@ -499,10 +523,12 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
 
     verificationResult match {
       case Success() =>
-        val proved = isFree || resV.decider.prover.assert(resT, None)
+        val proved = !assume || isFree || resV.decider.prover.assert(resT, None)
         if (proved) {
-          println("Assumption was added successfully!")
-          resV.asInstanceOf[WorkerVerifier].decider.debuggerAssume(Seq(resT), null)
+          if (assume) {
+            println("Assumption was added successfully!")
+            resV.asInstanceOf[WorkerVerifier].decider.debuggerAssume(Seq(resT), null)
+          }
           Some((resS, resT, resE, evalPcs.assumptionExps))
         } else {
           println("Fail! Could not prove assumption. Skipping")
diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala
@@ -29,6 +29,7 @@ trait NonQuantifiedChunk extends GeneralChunk {
   val args: Seq[Term]
   val argsExp: Option[Seq[ast.Exp]]
   val snap: Term
+  val snapExp: Option[ast.Exp]
   override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): NonQuantifiedChunk
   override def permMinus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk
   override def permPlus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk
diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala
@@ -47,7 +47,7 @@ trait ChunkSupportRules extends SymbolicExecutionRules {
              argsExp: Option[Seq[ast.Exp]],
              ve: VerificationError,
              v: Verifier)
-            (Q: (State, Heap, Term, Verifier) => VerificationResult)
+            (Q: (State, Heap, Term, Option[ast.Exp], Verifier) => VerificationResult)
             : VerificationResult
 
   def findChunk[CH <: NonQuantifiedChunk: ClassTag]
@@ -222,15 +222,15 @@ object chunkSupporter extends ChunkSupportRules {
              argsExp: Option[Seq[ast.Exp]],
              ve: VerificationError,
              v: Verifier)
-            (Q: (State, Heap, Term, Verifier) => VerificationResult)
+            (Q: (State, Heap, Term, Option[ast.Exp], Verifier) => VerificationResult)
             : VerificationResult = {
 
-    executionFlowController.tryOrFail2[Heap, Term](s.copy(h = h), v)((s1, v1, QS) => {
+    executionFlowController.tryOrFail3[Heap, Term, Option[ast.Exp]](s.copy(h = h), v)((s1, v1, QS) => {
       val lookupFunction =
         if (s1.moreCompleteExhale) moreCompleteExhaleSupporter.lookupComplete _
         else lookupGreedy _
-      lookupFunction(s1, s1.h, resource, args, argsExp, ve, v1)((s2, tSnap, v2) =>
-        QS(s2.copy(h = s.h), s2.h, tSnap, v2))
+      lookupFunction(s1, s1.h, resource, args, argsExp, ve, v1)((s2, tSnap, eSnap, v2) =>
+        QS(s2.copy(h = s.h), s2.h, tSnap, eSnap, v2))
     })(Q)
   }
 
@@ -241,14 +241,14 @@ object chunkSupporter extends ChunkSupportRules {
                            argsExp: Option[Seq[ast.Exp]],
                            ve: VerificationError,
                            v: Verifier)
-                          (Q: (State, Term, Verifier) => VerificationResult)
+                          (Q: (State, Term, Option[ast.Exp], Verifier) => VerificationResult)
                           : VerificationResult = {
 
     val id = ChunkIdentifier(resource, s.program)
     val findRes = findChunk[NonQuantifiedChunk](h.values, id, args, v)
     findRes match {
       case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>
-        Q(s, ch.snap, v)
+        Q(s, ch.snap, ch.snapExp, v)
       case _ if v.decider.checkSmoke(true) =>
         Success() // TODO: Mark branch as dead?
       case _ =>
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
@@ -314,15 +314,20 @@ object evaluator extends EvaluationRules {
         evalLocationAccess(s, fa, pve, v)((s1, _, tArgs, eArgs, v1) => {
           val ve = pve dueTo InsufficientPermission(fa)
           val resource = fa.res(s.program)
-          chunkSupporter.lookup(s1, s1.h, resource, tArgs, eArgs, ve, v1)((s2, h2, tSnap, v2) => {
+          chunkSupporter.lookup(s1, s1.h, resource, tArgs, eArgs, ve, v1)((s2, h2, tSnap, eSnap, v2) => {
             val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap)
             val s3 = s2.copy(h = h2, functionRecorder = fr)
-            val (debugHeapName, debugLabel) = v2.getDebugOldLabel(s3, fa.pos)
-            val newFa = Option.when(withExp)({
-              if (s3.isEvalInOld) ast.FieldAccess(eArgs.get.head, fa.field)(e.pos, e.info, e.errT)
-              else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugLabel)(e.pos, e.info, e.errT)
-            })
-            val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s3))) else s3
+            val (newFa, s4) = if (withExp && eSnap.isEmpty) {
+              val (debugHeapName, debugLabel) = v2.getDebugOldLabel(s3, fa.pos)
+              val newFa = Option.when(withExp)({
+                if (s3.isEvalInOld) ast.FieldAccess(eArgs.get.head, fa.field)(e.pos, e.info, e.errT)
+                else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugLabel)(e.pos, e.info, e.errT)
+              })
+              val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s3))) else s3
+              (newFa, s4)
+            } else {
+              (eSnap, s3)
+            }
             Q(s4, tSnap, newFa, v1)
           })
         })
diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala
@@ -172,4 +172,11 @@ object executionFlowController extends ExecutionFlowRules {
                         : VerificationResult =
 
       tryOrFailWithResult[(R1, R2)](s, v)((s1, v1, QS) => action(s1, v1, (s2, r21, r22, v2) => QS(s2, (r21, r22), v2)))((s2, r, v2) => Q(s2, r._1, r._2, v2))
+
+  def tryOrFail3[R1, R2, R3](s: State, v: Verifier)
+                            (action: (State, Verifier, (State, R1, R2, R3, Verifier) => VerificationResult) => VerificationResult)
+                            (Q: (State, R1, R2, R3, Verifier) => VerificationResult)
+  : VerificationResult =
+
+    tryOrFailWithResult[(R1, R2, R3)](s, v)((s1, v1, QS) => action(s1, v1, (s2, r21, r22, r23, v2) => QS(s2, (r21, r22, r23), v2)))((s2, r, v2) => Q(s2, r._1, r._2, r._3, v2))
 }
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -197,7 +197,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                      argsExp: Option[Seq[ast.Exp]],
                      ve: VerificationError,
                      v: Verifier)
-                    (Q: (State, Term, Verifier) => VerificationResult)
+                    (Q: (State, Term, Option[ast.Exp], Verifier) => VerificationResult)
                     : VerificationResult = {
 
     val id = ChunkIdentifier(resource, s.program)
@@ -213,7 +213,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, permSum, permSumExp, v1) =>
         v.decider.assert(IsPositive(permSum)) {
           case true =>
-            Q(s1, snap, v1)
+            Q(s1, snap, None, v1)
           case false =>
             createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)()))
         })
diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala
@@ -231,6 +231,7 @@ case class MagicWandChunk(id: MagicWandIdentifier,
   require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}")
 
   override val resourceID = MagicWandID
+  override val snapExp = None
 
   override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) =
     withPerm(Ite(newCond, perm, NoPerm), newCondExp.map(nce => ast.CondExp(nce, permExp.get, ast.NoPerm()())()))
