attach error information to failure context

viperproject · Oct 23, 2023 · 2b9b7f2 · 2b9b7f2
1 parent aaf96c3
commit 2b9b7f2
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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())
 
   }