refactor DebugExp to use Option types

viperproject · Oct 19, 2023 · 380000c · 380000c
1 parent 28d7b4a
commit 380000c
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 17 deletions.
diff --git a/src/main/scala/decider/DebugExp.scala b/src/main/scala/decider/DebugExp.scala
@@ -11,39 +11,38 @@ import viper.silicon.state.terms.Term
 import viper.silver.ast
 
 import scala.annotation.unused
-class DebugExp(str : String,
-               @unused exp : ast.Exp,
-               substitutedExp : ast.Exp,
+class DebugExp(str : Option[String],
+               @unused exp : Option[ast.Exp],
+               substitutedExp : Option[ast.Exp],
                terms : InsertionOrderedSet[Term],
                isInternal : Boolean,
                isImplicationLHS : Boolean,
                children : InsertionOrderedSet[DebugExp]) {
-// TODO ake: make str, exp, substitutedExp optional?
 
-  def this(str : String, @unused exp: ast.Exp, substitutedExp: ast.Exp, terms: InsertionOrderedSet[Term],
+  def this(str : Option[String], @unused exp: Option[ast.Exp], substitutedExp: Option[ast.Exp], terms: InsertionOrderedSet[Term],
            isInternal: Boolean, children: InsertionOrderedSet[DebugExp]) ={
     this(str, exp, substitutedExp, terms, isInternal, false, children)
   }
 
-  def this(str: String, @unused exp: ast.Exp, substitutedExp: ast.Exp,
+  def this(str: Option[String], @unused exp: Option[ast.Exp], substitutedExp: Option[ast.Exp],
             children: InsertionOrderedSet[DebugExp]) = {
     this(str, exp, substitutedExp, InsertionOrderedSet.empty, false, children)
   }
 
   def this(str : String, children : InsertionOrderedSet[DebugExp]) = {
-    this(str, null, null, children)
+    this(Some(str), None, None, children)
   }
 
   def this(str : String) = {
-    this(str, null, null, InsertionOrderedSet.empty)
+    this(Some(str), None, None, InsertionOrderedSet.empty)
   }
 
   def this(str: String, isInternal_ : Boolean) = {
-    this(str, null, null, InsertionOrderedSet.empty, isInternal_, InsertionOrderedSet.empty)
+    this(Some(str), None, None, InsertionOrderedSet.empty, isInternal_, InsertionOrderedSet.empty)
   }
 
   def this(exp : ast.Exp, substitutedExp : ast.Exp) = {
-    this(null, exp, substitutedExp, InsertionOrderedSet.empty)
+    this(None, Some(exp), Some(exp), InsertionOrderedSet.empty)
   }
 
   def withTerms(newTerms : InsertionOrderedSet[Term]): DebugExp = {
@@ -60,11 +59,11 @@ class DebugExp(str : String,
   }
 
   override def toString: String = {
-    if(str != null){
-      if(children.isEmpty) str
-      else str + ": " + children.mkString(" && ")
+    if(str.isDefined){
+      if(children.isEmpty) str.get
+      else str.get + ": " + children.mkString(" && ")
     }else{
-      substitutedExp.toString() + (if(isImplicationLHS && children.nonEmpty) " ==> (" + children.mkString(" && ") + ")" else "")
+      substitutedExp.get.toString() + (if(isImplicationLHS && children.nonEmpty) " ==> (" + children.mkString(" && ") + ")" else "")
     }
   }
 

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
@@ -205,7 +205,7 @@ private trait LayeredPathConditionStackLike {
       }
 
       if(layer.nonGlobalAssumptionDebugExps.nonEmpty && !implicationLHSExp.equals(TrueLit()())){
-        conditionalTerms :+= new decider.DebugExp(null, implicationLHSExp, implicationLHSExp, InsertionOrderedSet(implicationLHS),
+        conditionalTerms :+= new DebugExp(None, Some(implicationLHSExp), Some(implicationLHSExp), InsertionOrderedSet(implicationLHS),
           false, true, layer.nonGlobalAssumptionDebugExps)
       }else{
         conditionalTerms ++= layer.nonGlobalAssumptionDebugExps

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
@@ -540,7 +540,7 @@ object executor extends ExecutionRules {
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
               val eArgsStr = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-              val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($eArgsStr)", pa, s2.substituteVarsInExp(pa), InsertionOrderedSet.empty)
+              val debugExp = new DebugExp(Some(s"Predicate Trigger ${predicate.name}($eArgsStr)"), Some(pa), Some(s2.substituteVarsInExp(pa)), InsertionOrderedSet.empty)
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
               smCache1
             } else {

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
@@ -81,7 +81,7 @@ object joiner extends JoiningRules {
         })
         // Assume we are in a feasible branch
         val e = ast.BigOr(feasibleBranchesExp)
-        v.decider.assume(Or(feasibleBranches), new DebugExp("Feasible Branches", e, s.substituteVarsInExp(e), InsertionOrderedSet.empty))
+        v.decider.assume(Or(feasibleBranches), new DebugExp(Some("Feasible Branches"), Some(e), Some(s.substituteVarsInExp(e)), InsertionOrderedSet.empty))
         Q(sJoined, dataJoined, v)
       }
     }