Safeguard type builders

RipplB · Mar 13, 2024 · a755b6c · a755b6c
1 parent 4d16f15
commit a755b6c
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/.../xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/.../xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java
@@ -375,6 +375,9 @@ public class ExplStrategy extends BuilderStrategy<ExplState, ExplPrec> {
 
 		public ExplStrategy(XSTS xsts) {
 			super(xsts);
+			if (domain != Domain.EXPL) {
+				throw new UnsupportedOperationException(domain + " does not support EXPL builder strategy");
+			}
 		}
 
 		@Override
@@ -418,6 +421,9 @@ public ExplPrec getInitPrec() {
 	public class PredStrategy extends BuilderStrategy<PredState, PredPrec> {
 		public PredStrategy(XSTS xsts) {
 			super(xsts);
+			if (domain != Domain.PRED_BOOL && domain != Domain.PRED_SPLIT && domain != Domain.PRED_CART) {
+				throw new UnsupportedOperationException(domain + " does not support PRED builder strategy");
+			}
 		}
 
 		@Override
@@ -453,6 +459,10 @@ public class ProdStrategy extends BuilderStrategy<Prod2State<ExplState, PredStat
 
 		public ProdStrategy(XSTS xsts) {
 			super(xsts);
+			if (domain != Domain.EXPL_PRED_BOOL && domain != Domain.EXPL_PRED_SPLIT
+					&& domain != Domain.EXPL_PRED_CART && domain != Domain.EXPL_PRED_COMBINED) {
+				throw new UnsupportedOperationException(domain + " does not support PROD builder strategy");
+			}
 		}
 
 		@Override

diff --git a/...cts/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsInUnWrappers.kt b/...cts/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsInUnWrappers.kt
@@ -34,6 +34,4 @@ fun <S : ExprState> xstsExtractFromState(xstsState: XstsState<S>): S {
 
 val xstsStripPrec: (Prec) -> Prec = { it }
 
-fun <P: Prec> xstsStripPrecFun(p: P): P {
-    return p
-}
+fun <P: Prec> xstsStripPrecFun(p: P) = p