From f5a5ad7133717bbb3ea680baac49a2bc753617f7 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 1 Jun 2024 01:49:09 -0400 Subject: [PATCH] Remove exceptions for PICO --- .../exceptions/ImmutabilityException.java | 3 - .../UnkownImmutabilityQualifierException.java | 3 - .../solver/EncodingStuckException.java | 7 --- .../exceptions/solver/SolverException.java | 7 --- .../solver/PICOCombineConstraintEncoder.java | 63 ++++++++++--------- .../pico/typecheck/PICOViewpointAdapter.java | 3 +- 6 files changed, 36 insertions(+), 50 deletions(-) delete mode 100644 src/main/java/exceptions/ImmutabilityException.java delete mode 100644 src/main/java/exceptions/UnkownImmutabilityQualifierException.java delete mode 100644 src/main/java/exceptions/solver/EncodingStuckException.java delete mode 100644 src/main/java/exceptions/solver/SolverException.java diff --git a/src/main/java/exceptions/ImmutabilityException.java b/src/main/java/exceptions/ImmutabilityException.java deleted file mode 100644 index 4f94f29..0000000 --- a/src/main/java/exceptions/ImmutabilityException.java +++ /dev/null @@ -1,3 +0,0 @@ -package exceptions; - -public class ImmutabilityException extends RuntimeException {} diff --git a/src/main/java/exceptions/UnkownImmutabilityQualifierException.java b/src/main/java/exceptions/UnkownImmutabilityQualifierException.java deleted file mode 100644 index e4b76a7..0000000 --- a/src/main/java/exceptions/UnkownImmutabilityQualifierException.java +++ /dev/null @@ -1,3 +0,0 @@ -package exceptions; - -public class UnkownImmutabilityQualifierException extends ImmutabilityException {} diff --git a/src/main/java/exceptions/solver/EncodingStuckException.java b/src/main/java/exceptions/solver/EncodingStuckException.java deleted file mode 100644 index 58d5f61..0000000 --- a/src/main/java/exceptions/solver/EncodingStuckException.java +++ /dev/null @@ -1,7 +0,0 @@ -package exceptions.solver; - -public class EncodingStuckException extends SolverException { - public EncodingStuckException(String reason) { - super(reason); - } -} diff --git a/src/main/java/exceptions/solver/SolverException.java b/src/main/java/exceptions/solver/SolverException.java deleted file mode 100644 index 31277be..0000000 --- a/src/main/java/exceptions/solver/SolverException.java +++ /dev/null @@ -1,7 +0,0 @@ -package exceptions.solver; - -public class SolverException extends RuntimeException { - public SolverException(String reason) { - super(reason); - } -} diff --git a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java index a03ccae..d9d8e69 100644 --- 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 resultClauses = new ArrayList(); - 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 resultClauses = new ArrayList(); - 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 index 0eee7ec..a6b8bcf 100644 --- 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); } }