Remove exceptions for PICO

opprop · Jun 1, 2024 · f5a5ad7 · f5a5ad7
1 parent 5c5a016
commit f5a5ad7
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 50 deletions.
diff --git a/src/main/java/exceptions/ImmutabilityException.java b/src/main/java/exceptions/ImmutabilityException.java
diff --git a/src/main/java/exceptions/UnkownImmutabilityQualifierException.java b/src/main/java/exceptions/UnkownImmutabilityQualifierException.java
diff --git a/src/main/java/exceptions/solver/EncodingStuckException.java b/src/main/java/exceptions/solver/EncodingStuckException.java
diff --git a/src/main/java/exceptions/solver/SolverException.java b/src/main/java/exceptions/solver/SolverException.java
diff --git a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java
@@ -8,7 +8,6 @@
 import checkers.inference.solver.backend.maxsat.VectorUtils;
 import checkers.inference.solver.backend.maxsat.encoder.MaxSATAbstractConstraintEncoder;
 import checkers.inference.solver.frontend.Lattice;
-import exceptions.solver.EncodingStuckException;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.sat4j.core.VecInt;
 
@@ -38,7 +37,7 @@ private int id(AnnotationMirror am) {
         return typeToInt.get(am);
     }
 
-    private boolean isReceiverDependantMutable(ConstantSlot cSlot) {
+    private boolean isReceiverDependantMutable(ConstantSlot cSlot) throws Exception {
         if (AnnotationUtils.areSame(cSlot.getValue(), RECEIVER_DEPENDANT_MUTABLE)) {
             return true;
         } else if (AnnotationUtils.areSame(cSlot.getValue(), READONLY) ||
@@ -47,7 +46,7 @@ private boolean isReceiverDependantMutable(ConstantSlot cSlot) {
                 AnnotationUtils.areSame(cSlot.getValue(), BOTTOM)) {
             return false;
         } else {
-            throw new EncodingStuckException("Unknown qualifier: " + cSlot.getValue());
+            throw new Exception("Unknown qualifier: " + cSlot.getValue());
         }
     }
 
@@ -92,26 +91,30 @@ public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declar
     @Override
     public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, CombVariableSlot result) {
         List<VecInt> resultClauses = new ArrayList<VecInt>();
-        if (!isReceiverDependantMutable(declared)) {
-            resultClauses.add(VectorUtils.asVec(
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(declared.getValue()), lattice)));
-        } else {
-            resultClauses.add(VectorUtils.asVec(
-                    -MathUtils.mapIdToMatrixEntry(target.getId(), id(READONLY), lattice),
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(READONLY), lattice)));
-            resultClauses.add(VectorUtils.asVec(
-                    -MathUtils.mapIdToMatrixEntry(target.getId(), id(MUTABLE), lattice),
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(MUTABLE), lattice)));
-            resultClauses.add(VectorUtils.asVec(
-                    -MathUtils.mapIdToMatrixEntry(target.getId(), id(IMMUTABLE), lattice),
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(IMMUTABLE), lattice)));
-            resultClauses.add(VectorUtils.asVec(
-                    -MathUtils.mapIdToMatrixEntry(target.getId(), id(RECEIVER_DEPENDANT_MUTABLE), lattice),
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(RECEIVER_DEPENDANT_MUTABLE), lattice)));
-            resultClauses.add(VectorUtils.asVec(
-                    -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice),
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice)));
+        try {
+            if (!isReceiverDependantMutable(declared)) {
+                resultClauses.add(VectorUtils.asVec(
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(declared.getValue()), lattice)));
+            } else {
+                resultClauses.add(VectorUtils.asVec(
+                        -MathUtils.mapIdToMatrixEntry(target.getId(), id(READONLY), lattice),
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(READONLY), lattice)));
+                resultClauses.add(VectorUtils.asVec(
+                        -MathUtils.mapIdToMatrixEntry(target.getId(), id(MUTABLE), lattice),
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(MUTABLE), lattice)));
+                resultClauses.add(VectorUtils.asVec(
+                        -MathUtils.mapIdToMatrixEntry(target.getId(), id(IMMUTABLE), lattice),
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(IMMUTABLE), lattice)));
+                resultClauses.add(VectorUtils.asVec(
+                        -MathUtils.mapIdToMatrixEntry(target.getId(), id(RECEIVER_DEPENDANT_MUTABLE), lattice),
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(RECEIVER_DEPENDANT_MUTABLE), lattice)));
+                resultClauses.add(VectorUtils.asVec(
+                        -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice),
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice)));
 
+            }
+        } catch (Exception e) {
+            throw new RuntimeException(e);
         }
         return resultClauses.toArray(new VecInt[resultClauses.size()]);
     }
@@ -140,12 +143,16 @@ public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declar
     @Override
     public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, CombVariableSlot result) {
         List<VecInt> resultClauses = new ArrayList<VecInt>();
-        if (!isReceiverDependantMutable(declared)) {
-            resultClauses.add(VectorUtils.asVec(
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(declared.getValue()), lattice)));
-        } else {
-            resultClauses.add(VectorUtils.asVec(
-                    MathUtils.mapIdToMatrixEntry(result.getId(), id(target.getValue()), lattice)));
+        try {
+            if (!isReceiverDependantMutable(declared)) {
+                resultClauses.add(VectorUtils.asVec(
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(declared.getValue()), lattice)));
+            } else {
+                resultClauses.add(VectorUtils.asVec(
+                        MathUtils.mapIdToMatrixEntry(result.getId(), id(target.getValue()), lattice)));
+            }
+        } catch (Exception e) {
+            throw new RuntimeException(e);
         }
         return resultClauses.toArray(new VecInt[resultClauses.size()]);
     }

diff --git a/src/main/java/pico/typecheck/PICOViewpointAdapter.java b/src/main/java/pico/typecheck/PICOViewpointAdapter.java
@@ -17,7 +17,6 @@
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
 
-import exceptions.UnkownImmutabilityQualifierException;
 import pico.common.ExtendedViewpointAdapter;
 
 public class PICOViewpointAdapter extends AbstractViewpointAdapter implements ExtendedViewpointAdapter {
@@ -54,7 +53,7 @@ protected AnnotationMirror combineAnnotationWithAnnotation(AnnotationMirror rece
         } else if (AnnotationUtils.areSame(declaredAnnotation, RECEIVER_DEPENDANT_MUTABLE)) {
             return receiverAnnotation;
         } else {
-            throw new BugInCF("Unknown declared modifier: " + declaredAnnotation, new UnkownImmutabilityQualifierException());
+            throw new BugInCF("Unknown declared modifier: " + declaredAnnotation);
         }
     }