From 2b9b7f2d97aab18090c88d89527b3393f2a08397 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 23 Oct 2023 14:54:14 +0200
Subject: [PATCH] attach error information to failure context

---
 src/main/scala/decider/PathConditions.scala   |  2 +-
 src/main/scala/interfaces/Verification.scala  | 24 +++++++++++++++++--
 .../scala/rules/SymbolicExecutionRules.scala  |  9 ++++++-
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 2f3ae799d..537280fba 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -372,7 +372,7 @@ private[decider] class LayeredPathConditionStack
 
   def assumptions: InsertionOrderedSet[Term] = allAssumptions
 
-  def assumptionExps: InsertionOrderedSet[DebugExp] = InsertionOrderedSet.empty// TODo ake: layers.flatMap(_.assumptionExps) ?
+  def assumptionExps: InsertionOrderedSet[DebugExp] = InsertionOrderedSet(layers.flatMap(_.assumptionDebugExps))
 
   def declarations: InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala
index 7e6c8e320..a8979760b 100644
--- a/src/main/scala/interfaces/Verification.scala
+++ b/src/main/scala/interfaces/Verification.scala
@@ -6,6 +6,8 @@
 
 package viper.silicon.interfaces
 
+import viper.silicon.common.collections.immutable.InsertionOrderedSet
+import viper.silicon.decider.DebugExp
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.reporting.{Converter, DomainEntry, ExtractedFunction, ExtractedModel, ExtractedModelEntry, GenericDomainInterpreter, ModelInterpreter, NullRefEntry, RefEntry, UnprocessedModelEntry, VarEntry}
 import viper.silicon.state.{State, Store}
@@ -103,7 +105,9 @@ case class Failure/*[ST <: Store[ST],
 
 case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
                                  counterExample: Option[Counterexample],
-                                 reasonUnknown: Option[String]) extends FailureContext {
+                                 reasonUnknown: Option[String],
+                                 state: Option[State],
+                                 assumptions: InsertionOrderedSet[DebugExp]) extends FailureContext {
   lazy val branchConditionString: String = {
     if(branchConditions.nonEmpty) {
       val branchConditionsString =
@@ -129,7 +133,23 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
     }
   }
 
-  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString
+  lazy val stateString: String = {
+    if(state.isDefined){
+      s"\nStore:\n\t\t${state.get.g.values.mkString("\n\t\t")}\nHeap:\n\t\t${state.get.h.values.mkString("\n\t\t")}"
+    }else{
+      ""
+    }
+  }
+
+  lazy val assumptionsString: String = {
+    if(assumptions.nonEmpty){
+      s"\nassumptions: ${assumptions.mkString(" && ")}"
+    }else{
+      ""
+    }
+  }
+
+  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString + stateString + assumptionsString
 }
 
 trait SiliconCounterexample extends Counterexample {
diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala
index 243b44065..e3f385936 100644
--- a/src/main/scala/rules/SymbolicExecutionRules.scala
+++ b/src/main/scala/rules/SymbolicExecutionRules.scala
@@ -64,7 +64,14 @@ trait SymbolicExecutionRules {
           case _ => (-1, -1)
         })
     } else Seq()
-    res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown))
+
+    val state = s.copy()
+
+    val assumptions = v.decider.pcs.assumptionExps
+
+    // TODO ake: attach assertion that failed
+
+    res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown, Some(state), assumptions))
     Failure(res, v.reportFurtherErrors())
 
   }