Added util to show code snippet, moved debug print

Added a util to get the expression from a SourcePosition.
Moved the print in the verifySubtype to verifySMTSubtype.

Author: cheestree

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

@@ -8,6 +8,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.*;
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
@@ -16,6 +17,7 @@
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.constants.Keys;
+import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.factory.Factory;
@@ -92,6 +94,11 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
      */
     public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
+            if (CommandLineLauncher.cmdArgs.debugMode) {
+                System.out.println(String.format("%s <: %s on expression '%s' at %s", expected, found,
+                        Utils.getExpressionFromPosition(position),
+                        position.getFile().getName() + ":" + position.getLine()));
+            }
             return new SMTEvaluator().verifySubtype(found, expected, context);
         } catch (LJError e) {
             e.setPosition(position);

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

@@ -7,7 +7,6 @@
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
 
-import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -26,9 +25,6 @@ public class SMTEvaluator {
      */
     public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
-        if (CommandLineLauncher.cmdArgs.debugMode) {
-            System.out.println(String.format("%s <: %s", subRef, supRef));
-        }
         try {
             Expression exp = toVerify.getExpression();
             try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -1,6 +1,7 @@
 package liquidjava.utils;
 
 import java.util.Map;
+import java.util.Scanner;
 import java.util.Set;
 import java.util.stream.Stream;
 
@@ -92,4 +93,22 @@ public static SourcePosition getRealPosition(CtElement element) {
         }
         return element.getPosition();
     }
+
+    public static String getExpressionFromPosition(SourcePosition position) {
+        if (position == null || position.getFile() == null)
+            return null;
+        try (Scanner scanner = new Scanner(position.getFile())) {
+            int currentLine = 1;
+            while (scanner.hasNextLine()) {
+                String line = scanner.nextLine();
+                if (currentLine == position.getLine()) {
+                    return line.substring(position.getColumn() - 1).trim();
+                }
+                currentLine++;
+            }
+        } catch (Exception e) {
+            // ignore
+        }
+        return null;
+    }
 }