Skip to content

Commit 76058cd

Browse files
CatarinaGamboaCatarinaGamboa
committed
improve debug info
1 parent 40e105f commit 76058cd

6 files changed

Lines changed: 186 additions & 19 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,13 @@
22

33
// ANSI color codes
44
public class Colors {
5-
public static final String RESET = "\u001B[0m";
6-
public static final String GREY = "\u001B[90m";
7-
public static final String BOLD_RED = "\u001B[1;31m";
8-
public static final String BOLD_YELLOW = "\u001B[1;33m";
9-
}
5+
public static final String RESET = "";
6+
public static final String GREY = "";
7+
public static final String RED = "";
8+
public static final String GREEN = "";
9+
public static final String YELLOW = "";
10+
public static final String BLUE = "";
11+
public static final String CYAN = "";
12+
public static final String BOLD_RED = "";
13+
public static final String BOLD_YELLOW = "";
14+
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
package liquidjava.diagnostics;
2+
3+
import java.util.ArrayList;
4+
import java.util.LinkedHashMap;
5+
import java.util.LinkedHashSet;
6+
import java.util.List;
7+
import java.util.Map;
8+
import java.util.Set;
9+
10+
import liquidjava.api.CommandLineLauncher;
11+
import liquidjava.rj_language.Predicate;
12+
import liquidjava.rj_language.ast.BinaryExpression;
13+
import liquidjava.rj_language.ast.Expression;
14+
import liquidjava.rj_language.ast.GroupExpression;
15+
import liquidjava.utils.Utils;
16+
import spoon.reflect.cu.SourcePosition;
17+
18+
/**
19+
* Centralised debug-mode logging for verification activity. Output is gated on the global {@code --debug} / {@code -d}
20+
* flag and is purely informational.
21+
*
22+
* <p>
23+
* Layers of output, from outermost to innermost:
24+
* <ul>
25+
* <li>{@link #info} — verification context (caller-level predicates, source position).</li>
26+
* <li>{@link #smtStart} — premises and conclusion as fed to Z3.</li>
27+
* <li>{@link #smtUnsat} / {@link #smtSat} / {@link #smtUnknown} — solver outcome.</li>
28+
* </ul>
29+
*/
30+
public final class DebugLog {
31+
32+
private static final String INFO_TAG = Colors.YELLOW + "[INFO]" + Colors.RESET;
33+
private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
34+
35+
private DebugLog() {
36+
}
37+
38+
public static boolean enabled() {
39+
return CommandLineLauncher.cmdArgs.debugMode;
40+
}
41+
42+
public static void info(String verb, Object expected, Object found, SourcePosition position) {
43+
if (!enabled()) {
44+
return;
45+
}
46+
String exp = Utils.getExpressionFromPosition(position);
47+
String where = position.getFile().getName() + ":" + position.getLine();
48+
System.out.println(INFO_TAG + " " + verb + ": " + found + " <: " + expected);
49+
System.out.println(INFO_TAG + " at " + where + (exp != null ? " on '" + exp + "'" : ""));
50+
}
51+
52+
public static void smtStart(Predicate premises, Predicate conclusion) {
53+
if (!enabled()) {
54+
return;
55+
}
56+
printPremisesByVariable(premises);
57+
System.out.println(SMT_TAG + " conclusion: " + conclusion);
58+
}
59+
60+
/**
61+
* Splits the premise conjunction into top-level conjuncts and groups them by the variable they constrain. Conjuncts
62+
* mentioning a single variable are printed under that variable; conjuncts mentioning zero or several variables are
63+
* printed under a {@code <shared>} bucket.
64+
*/
65+
private static void printPremisesByVariable(Predicate premises) {
66+
Expression root = premises.getExpression();
67+
List<Expression> conjuncts = new ArrayList<>();
68+
flattenConjunction(root, conjuncts);
69+
70+
Map<String, List<String>> grouped = new LinkedHashMap<>();
71+
for (Expression c : conjuncts) {
72+
List<String> names = new ArrayList<>();
73+
c.getVariableNames(names);
74+
Set<String> unique = new LinkedHashSet<>(names);
75+
String key;
76+
if (unique.isEmpty()) {
77+
key = "";
78+
} else if (unique.size() == 1) {
79+
key = unique.iterator().next();
80+
} else {
81+
key = "<shared>";
82+
}
83+
grouped.computeIfAbsent(key, k -> new ArrayList<>()).add(c.toString());
84+
}
85+
86+
System.out.println(SMT_TAG + " premises:");
87+
for (Map.Entry<String, List<String>> entry : grouped.entrySet()) {
88+
String prefix = entry.getKey().isEmpty() ? "" : entry.getKey() + ": ";
89+
for (String c : entry.getValue()) {
90+
System.out.println(SMT_TAG + " " + prefix + c);
91+
}
92+
}
93+
}
94+
95+
private static void flattenConjunction(Expression e, List<Expression> out) {
96+
if (e instanceof GroupExpression g) {
97+
flattenConjunction(g.getExpression(), out);
98+
return;
99+
}
100+
if (e instanceof BinaryExpression b && "&&".equals(b.getOperator())) {
101+
flattenConjunction(b.getFirstOperand(), out);
102+
flattenConjunction(b.getSecondOperand(), out);
103+
return;
104+
}
105+
out.add(e);
106+
}
107+
108+
public static void smtUnsat() {
109+
if (!enabled()) {
110+
return;
111+
}
112+
System.out.println(SMT_TAG + " result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET);
113+
}
114+
115+
public static void smtSat(Object counterexample) {
116+
if (!enabled()) {
117+
return;
118+
}
119+
System.out.println(SMT_TAG + " result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET
120+
+ "; counterexample: " + counterexample);
121+
}
122+
123+
public static void smtUnknown() {
124+
if (!enabled()) {
125+
return;
126+
}
127+
System.out.println(SMT_TAG + " result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
128+
}
129+
}

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

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -324,8 +324,13 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen
324324
}
325325

326326
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
327+
return checkStateSMT(prevState, expectedState, p, false);
328+
}
329+
330+
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent)
331+
throws LJError {
327332
SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p,
328-
factory);
333+
factory, silent);
329334
return result.isOk();
330335
}
331336

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

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
import java.util.stream.Collectors;
1111

1212
import liquidjava.diagnostics.errors.*;
13-
import liquidjava.api.CommandLineLauncher;
13+
import liquidjava.diagnostics.DebugLog;
1414
import liquidjava.diagnostics.TranslationTable;
1515
import liquidjava.processor.VCImplication;
1616
import liquidjava.processor.context.*;
@@ -103,14 +103,14 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
103103
* @return the result of the verification, containing a counterexample if the verification fails
104104
*/
105105
public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError {
106+
DebugLog.info("discharging to SMT", expected, found, position);
107+
return dischargeToSMT(expected, found, position, false);
108+
}
109+
110+
private SMTResult dischargeToSMT(Predicate expected, Predicate found, SourcePosition position, boolean silent)
111+
throws LJError {
106112
try {
107-
if (CommandLineLauncher.cmdArgs.debugMode) {
108-
String exp = Utils.getExpressionFromPosition(position);
109-
System.out.println(String.format("%s <: %s %s at %s", expected, found,
110-
exp != null ? String.format("on expression '%s'", exp) : "",
111-
position.getFile().getName() + ":" + position.getLine()));
112-
}
113-
return new SMTEvaluator().verifySubtype(found, expected, context);
113+
return new SMTEvaluator().verifySubtype(found, expected, context, silent);
114114
} catch (LJError e) {
115115
if (e.getPosition() == null) {
116116
e.setPosition(position);
@@ -134,6 +134,14 @@ public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePos
134134
*/
135135
public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List<GhostState> states,
136136
SourcePosition position, Factory factory) throws LJError {
137+
return verifySMTSubtypeStates(type, expectedType, states, position, factory, false);
138+
}
139+
140+
public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List<GhostState> states,
141+
SourcePosition position, Factory factory, boolean silent) throws LJError {
142+
if (!silent) {
143+
DebugLog.info("checking subtyping (states)", expectedType, type, position);
144+
}
137145
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
138146
gatherVariables(expectedType, lrv, mainVars);
139147
gatherVariables(type, lrv, mainVars);
@@ -149,8 +157,8 @@ public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType,
149157
Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context,
150158
factory);
151159

152-
// check subtyping
153-
return verifySMTSubtype(expected, premises, position);
160+
// check subtyping (skip the inner INFO line — outer states-level INFO above is enough)
161+
return dischargeToSMT(expected, premises, position, silent);
154162
}
155163

156164
/**
@@ -350,4 +358,5 @@ private TranslationTable createMap(Predicate expectedType) {
350358
joinPredicates(expectedType, mainVars, lrv, map);
351359
return map;
352360
}
361+
353362
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
220220
Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
221221
Predicate c = c1.substituteVariable(Keys.THIS, name);
222222
c = c.changeOldMentions(nameOld, name);
223-
boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition());
223+
boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition(), true);
224224
if (ok) {
225225
SourcePosition pos = Utils.getLJAnnotationPosition(e, value);
226226
tc.throwStateConflictError(pos, p);

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

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import com.microsoft.z3.Status;
88
import com.microsoft.z3.Z3Exception;
99

10+
import liquidjava.diagnostics.DebugLog;
1011
import liquidjava.processor.context.Context;
1112
import liquidjava.rj_language.Predicate;
1213
import liquidjava.rj_language.ast.Expression;
@@ -16,14 +17,22 @@ public class SMTEvaluator {
1617
/**
1718
* Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser
1819
* for our SMT-ready refinement language and discharges the verification to Z3
19-
*
20+
*
2021
* @param subRef
2122
* @param supRef
2223
* @param context
23-
*
24+
*
2425
* @return the result of the verification, containing a counterexample if the verification fails
2526
*/
2627
public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
28+
return verifySubtype(subRef, supRef, context, false);
29+
}
30+
31+
public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context, boolean silent)
32+
throws Exception {
33+
if (!silent) {
34+
DebugLog.smtStart(subRef, supRef);
35+
}
2736
Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
2837
try {
2938
Expression exp = toVerify.getExpression();
@@ -37,8 +46,18 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
3746
if (result.equals(Status.SATISFIABLE)) {
3847
Model model = solver.getModel();
3948
Counterexample counterexample = tz3.getCounterexample(model);
49+
if (!silent) {
50+
DebugLog.smtSat(counterexample);
51+
}
4052
return SMTResult.error(counterexample);
4153
}
54+
if (!silent) {
55+
if (result.equals(Status.UNKNOWN)) {
56+
DebugLog.smtUnknown();
57+
} else {
58+
DebugLog.smtUnsat();
59+
}
60+
}
4261
}
4362
} catch (SyntaxException e) {
4463
System.out.println("Could not parse: " + toVerify);

0 commit comments

Comments
 (0)