Add SMTResult

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -1,8 +1,8 @@
 package liquidjava.diagnostics.errors;
 
-import liquidjava.diagnostics.Counterexample;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.smt.Counterexample;
 import spoon.reflect.cu.SourcePosition;
 
 /**

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -6,7 +6,6 @@
 import java.util.Map;
 import java.util.Optional;
 
-import liquidjava.diagnostics.Counterexample;
 import liquidjava.diagnostics.errors.*;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
@@ -17,6 +16,8 @@
 import liquidjava.processor.facade.GhostDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.smt.Counterexample;
+import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
@@ -314,9 +315,8 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen
     }
 
     public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
-        Counterexample counterexample = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(),
-                p, factory);
-        return counterexample == null;
+        SMTResult result = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
+        return result.isOk();
     }
 
     public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType,

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -8,13 +8,13 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.*;
-import liquidjava.diagnostics.Counterexample;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
+import liquidjava.smt.Counterexample;
 import liquidjava.smt.SMTEvaluator;
-import liquidjava.smt.TypeCheckError;
+import liquidjava.smt.SMTResult;
 import liquidjava.utils.constants.Keys;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -56,10 +56,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
             e.setPosition(element.getPosition());
             throw e;
         }
-        Counterexample counterexample = smtChecks(expected, premises, element.getPosition());
-        if (counterexample != null)
+        SMTResult result = smtChecks(expected, premises, element.getPosition());
+        if (result.isError()) {
             throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
-                    map, counterexample, customMessage);
+                    map, result.getCounterexample(), customMessage);
+        }
     }
 
     /**
@@ -75,9 +76,9 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
      */
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
             Factory f) throws LJError {
-        Counterexample counterexample = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
-        if (counterexample != null)
-            throwRefinementError(element.getPosition(), expectedType, type, counterexample, null);
+        SMTResult result = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
+        if (result.isError())
+            throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null);
     }
 
     /**
@@ -91,12 +92,9 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
      *
      * @throws LJError
      */
-    public Counterexample smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
+    public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
-            new SMTEvaluator().verifySubtype(found, expected, context);
-            return null;
-        } catch (TypeCheckError e) {
-            return e.getCounterexample();
+            return new SMTEvaluator().verifySubtype(found, expected, context);
         } catch (LJError e) {
             e.setPosition(position);
             throw e;
@@ -105,13 +103,13 @@ public Counterexample smtChecks(Predicate expected, Predicate found, SourcePosit
         }
     }
 
-    public Counterexample canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
+    public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
             SourcePosition position, Factory f) throws LJError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         gatherVariables(type, lrv, mainVars);
         if (expectedType.isBooleanTrue() && type.isBooleanTrue())
-            return null;
+            return SMTResult.ok();
 
         TranslationTable map = new TranslationTable();
         String[] s = { Keys.WILDCARD, Keys.THIS };

…quidjava/diagnostics/Counterexample.java …/java/liquidjava/smt/Counterexample.javaliquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java renamed to liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java renamed to liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java

@@ -1,4 +1,4 @@
-package liquidjava.diagnostics;
+package liquidjava.smt;
 
 import java.util.List;
 

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -7,14 +7,13 @@
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
 
-import liquidjava.diagnostics.Counterexample;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 
 public class SMTEvaluator {
 
-    public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception {
+    public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception {
         // Creates a parser for our SMT-ready refinement language
         // Discharges the verification to z3
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
@@ -28,7 +27,7 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws
                 if (result.equals(Status.SATISFIABLE)) {
                     Model model = solver.getModel();
                     Counterexample counterexample = tz3.getCounterexample(model);
-                    throw new TypeCheckError(counterexample);
+                    return SMTResult.error(counterexample);
                 }
             }
         } catch (SyntaxException e1) {
@@ -37,5 +36,6 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws
         } catch (Z3Exception e) {
             throw new Z3Exception(e.getLocalizedMessage());
         }
+        return SMTResult.ok();
     }
 }

liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java

@@ -0,0 +1,29 @@
+package liquidjava.smt;
+
+public class SMTResult {
+    private final Counterexample counterexample;
+
+    private SMTResult(Counterexample counterexample) {
+        this.counterexample = counterexample;
+    }
+
+    public static SMTResult ok() {
+        return new SMTResult(null);
+    }
+
+    public static SMTResult error(Counterexample counterexample) {
+        return new SMTResult(counterexample);
+    }
+
+    public boolean isOk() {
+        return counterexample == null;
+    }
+
+    public boolean isError() {
+        return !isOk();
+    }
+
+    public Counterexample getCounterexample() {
+        return counterexample;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -22,7 +22,6 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
-import liquidjava.diagnostics.Counterexample;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
 import liquidjava.processor.context.AliasWrapper;