From d9c0b9a4110bb43384005897d1d02cc11c2183dc Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 19 Mar 2026 00:52:31 +0000 Subject: [PATCH 1/4] Modified CLI Added picocli to extend flag usage, with the implementation of --debug to presentraw expressions, counterexamples and all expressions sent to the SMT solver. Logging should be improved as it's not incredibly readable. --- liquidjava-verifier/pom.xml | 5 ++ .../liquidjava/api/CommandLineLauncher.java | 55 +++++++++++++------ .../liquidjava/diagnostics/Diagnostics.java | 10 ++++ .../rj_language/opt/ExpressionSimplifier.java | 9 ++- .../java/liquidjava/smt/SMTEvaluator.java | 10 ++++ 5 files changed, 72 insertions(+), 17 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 34ea18db..31d6d166 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -316,6 +316,11 @@ 2.10.1 + + info.picocli + picocli + 4.7.7 + diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index e473562c..644c1275 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -3,12 +3,17 @@ import java.io.File; import java.util.Arrays; import java.util.List; +import java.util.concurrent.Callable; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; import liquidjava.processor.context.ContextHistory; +import picocli.CommandLine; +import picocli.CommandLine.Command; +import picocli.CommandLine.Option; +import picocli.CommandLine.Parameters; import spoon.Launcher; import spoon.compiler.Environment; import spoon.processing.ProcessingManager; @@ -22,25 +27,43 @@ public class CommandLineLauncher { private static final ContextHistory contextHistory = ContextHistory.getInstance(); public static void main(String[] args) { - if (args.length == 0) { - System.out.println("No input paths provided"); - System.out.println("\nUsage: ./liquidjava <...paths>"); - System.out.println(" <...paths>: Paths to be verified by LiquidJava"); - System.out.println( - "\nExample: ./liquidjava liquidjava-example/src/main/java/test liquidjava-example/src/main/java/testingInProgress/Account.java"); - return; + CommandLine commandLine = new CommandLine(new CliArguments()); + int exitCode = commandLine.execute(args); + if (exitCode != 0) { + System.exit(exitCode); } - List paths = Arrays.asList(args); - launch(paths.toArray(new String[0])); + } + + @Command(name = "liquidjava", mixinStandardHelpOptions = true, customSynopsis = "./liquidjava <...paths> ") + private static class CliArguments implements Callable { + + @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output") + private boolean debugMode; + + @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava") + private List paths; + + @Override + public Integer call() { + if (debugMode) { + System.out.println("Debug mode enabled"); + System.out.println("Input paths: " + paths); + diagnostics.setDebugMode(); + } + + launch(paths.stream().toArray(String[]::new)); + + // print diagnostics + if (diagnostics.foundWarning()) { + System.out.println(diagnostics.getWarningOutput()); + } + if (diagnostics.foundError()) { + System.out.println(diagnostics.getErrorOutput()); + return 1; + } - // print diagnostics - if (diagnostics.foundWarning()) { - System.out.println(diagnostics.getWarningOutput()); - } - if (diagnostics.foundError()) { - System.out.println(diagnostics.getErrorOutput()); - } else { System.out.println("Correct! Passed Verification."); + return 0; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index f125f5fc..4a8f31fe 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -15,10 +15,12 @@ public class Diagnostics { private final LinkedHashSet errors; private final LinkedHashSet warnings; + private boolean debugMode; private Diagnostics() { this.errors = new LinkedHashSet<>(); this.warnings = new LinkedHashSet<>(); + this.debugMode = false; } public static Diagnostics getInstance() { @@ -33,6 +35,14 @@ public void add(LJWarning warning) { this.warnings.add(warning); } + public boolean isDebugMode() { + return this.debugMode; + } + + public void setDebugMode() { + this.debugMode = true; + } + public boolean foundError() { return !this.errors.isEmpty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 2e43e326..dcb46259 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -1,5 +1,6 @@ package liquidjava.rj_language.opt; +import liquidjava.diagnostics.Diagnostics; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; @@ -9,13 +10,19 @@ public class ExpressionSimplifier { + private static final Diagnostics diagnostics = Diagnostics.getInstance(); + /** * Simplifies an expression by applying constant propagation, constant folding and removing redundant conjuncts * Returns a derivation node representing the tree of simplifications applied */ public static ValDerivationNode simplify(Expression exp) { ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp); - return simplifyValDerivationNode(fixedPoint); + ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint); + if (diagnostics.isDebugMode()) { + System.out.println("Simplified expression: original: " + exp + " | simplified: " + simplified.getValue()); + } + return simplified; } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 096a9b95..cf416a61 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -9,12 +9,15 @@ import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; +import liquidjava.diagnostics.Diagnostics; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; public class SMTEvaluator { + private static final Diagnostics diagnostics = Diagnostics.getInstance(); + /** * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser * for our SMT-ready refinement language and discharges the verification to Z3 @@ -27,6 +30,9 @@ public class SMTEvaluator { */ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception { Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); + if (diagnostics.isDebugMode()) { + System.out.println("Verifying: " + toVerify); + } try { Expression exp = toVerify.getExpression(); try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) { @@ -39,6 +45,10 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); Counterexample counterexample = tz3.getCounterexample(model); + if (diagnostics.isDebugMode()) { + System.out.println("Verification failed. Counterexample:"); + System.out.println(counterexample); + } return SMTResult.error(counterexample); } } From 2f620af59d31004cba53ad443fdada4eb30c8e3f Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 19 Mar 2026 16:32:42 +0000 Subject: [PATCH 2/4] Split args into a separate file Arguments are now accessed via an object in the CommandLineLauncher class, so that it's easier in the future to implement new flags. --- .../java/liquidjava/api/CommandLineArgs.java | 20 +++++++ .../liquidjava/api/CommandLineLauncher.java | 56 ++++++------------- .../diagnostics/errors/RefinementError.java | 3 +- .../liquidjava/rj_language/Predicate.java | 4 ++ .../rj_language/opt/ExpressionSimplifier.java | 8 +-- .../java/liquidjava/smt/SMTEvaluator.java | 14 +---- 6 files changed, 47 insertions(+), 58 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java new file mode 100644 index 00000000..9fe7d6d0 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java @@ -0,0 +1,20 @@ +package liquidjava.api; + +import java.util.List; +import java.util.concurrent.Callable; + +import picocli.CommandLine.Command; +import picocli.CommandLine.Option; +import picocli.CommandLine.Parameters; + +@Command(name = "liquidjava", mixinStandardHelpOptions = false, customSynopsis = "./liquidjava <...paths> ") +public class CommandLineArgs { + @Option(names = {"-h", "--help"}, usageHelp = true, description = "Display this help message") + public boolean help; + + @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output") + public boolean debugMode; + + @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava") + public List paths; +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 644c1275..796928c8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -2,8 +2,6 @@ import java.io.File; import java.util.Arrays; -import java.util.List; -import java.util.concurrent.Callable; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.CustomError; @@ -11,9 +9,6 @@ import liquidjava.processor.RefinementProcessor; import liquidjava.processor.context.ContextHistory; import picocli.CommandLine; -import picocli.CommandLine.Command; -import picocli.CommandLine.Option; -import picocli.CommandLine.Parameters; import spoon.Launcher; import spoon.compiler.Environment; import spoon.processing.ProcessingManager; @@ -25,46 +20,29 @@ public class CommandLineLauncher { private static final Diagnostics diagnostics = Diagnostics.getInstance(); private static final ContextHistory contextHistory = ContextHistory.getInstance(); + public static final CommandLineArgs cmdArgs = new CommandLineArgs(); public static void main(String[] args) { - CommandLine commandLine = new CommandLine(new CliArguments()); - int exitCode = commandLine.execute(args); - if (exitCode != 0) { - System.exit(exitCode); - } - } - - @Command(name = "liquidjava", mixinStandardHelpOptions = true, customSynopsis = "./liquidjava <...paths> ") - private static class CliArguments implements Callable { - - @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output") - private boolean debugMode; - - @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava") - private List paths; - - @Override - public Integer call() { - if (debugMode) { - System.out.println("Debug mode enabled"); - System.out.println("Input paths: " + paths); - diagnostics.setDebugMode(); - } + CommandLine cmd = new CommandLine(cmdArgs); + cmd.parseArgs(args); - launch(paths.stream().toArray(String[]::new)); + if (cmd.isUsageHelpRequested()) { + cmd.usage(System.out); + return; + } - // print diagnostics - if (diagnostics.foundWarning()) { - System.out.println(diagnostics.getWarningOutput()); - } - if (diagnostics.foundError()) { - System.out.println(diagnostics.getErrorOutput()); - return 1; - } + launch(cmdArgs.paths.stream().toArray(String[]::new)); - System.out.println("Correct! Passed Verification."); - return 0; + // print diagnostics + if (diagnostics.foundWarning()) { + System.out.println(diagnostics.getWarningOutput()); + } + if (diagnostics.foundError()) { + System.out.println(diagnostics.getErrorOutput()); + return; } + + System.out.println("Correct! Passed Verification."); } public static void launch(String... paths) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 380edf9a..9ce59f68 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.stream.Collectors; +import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; @@ -45,7 +46,7 @@ public String getCounterExampleString() { found.getValue().getVariableNames(foundVarNames); String counterexampleString = counterexample.assignments().stream() // only include variables that appear in the found value - .filter(a -> foundVarNames.contains(a.first())) + .filter(a -> CommandLineLauncher.cmdArgs.debugMode || foundVarNames.contains(a.first())) // format as "var == value" .map(a -> a.first() + " == " + a.second()) // join with "&&" diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index c91380ee..6b6276df 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -6,6 +6,7 @@ import java.util.Map; import java.util.stream.Collectors; +import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -188,6 +189,9 @@ public Expression getExpression() { } public ValDerivationNode simplify() { + if (CommandLineLauncher.cmdArgs.debugMode) { + return new ValDerivationNode(exp.clone(), null); + } return ExpressionSimplifier.simplify(exp.clone()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index dcb46259..9d2143a9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -10,19 +10,13 @@ public class ExpressionSimplifier { - private static final Diagnostics diagnostics = Diagnostics.getInstance(); - /** * Simplifies an expression by applying constant propagation, constant folding and removing redundant conjuncts * Returns a derivation node representing the tree of simplifications applied */ public static ValDerivationNode simplify(Expression exp) { ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp); - ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint); - if (diagnostics.isDebugMode()) { - System.out.println("Simplified expression: original: " + exp + " | simplified: " + simplified.getValue()); - } - return simplified; + return simplifyValDerivationNode(fixedPoint); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index cf416a61..7ece2c15 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,7 +1,5 @@ package liquidjava.smt; -import java.util.Set; - import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.Expr; import com.microsoft.z3.Model; @@ -9,15 +7,13 @@ import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; -import liquidjava.diagnostics.Diagnostics; +import liquidjava.api.CommandLineLauncher; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; public class SMTEvaluator { - private static final Diagnostics diagnostics = Diagnostics.getInstance(); - /** * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser * for our SMT-ready refinement language and discharges the verification to Z3 @@ -30,8 +26,8 @@ public class SMTEvaluator { */ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception { Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); - if (diagnostics.isDebugMode()) { - System.out.println("Verifying: " + toVerify); + if (CommandLineLauncher.cmdArgs.debugMode) { + System.out.println("Verifying: " + subRef + " <: " + supRef); } try { Expression exp = toVerify.getExpression(); @@ -45,10 +41,6 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); Counterexample counterexample = tz3.getCounterexample(model); - if (diagnostics.isDebugMode()) { - System.out.println("Verification failed. Counterexample:"); - System.out.println(counterexample); - } return SMTResult.error(counterexample); } } From e09836c07a196f465a21902967b21d766bd81d7c Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 19 Mar 2026 16:37:43 +0000 Subject: [PATCH 3/4] Removed unused code in Diagnostics --- .../main/java/liquidjava/diagnostics/Diagnostics.java | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index 4a8f31fe..f125f5fc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -15,12 +15,10 @@ public class Diagnostics { private final LinkedHashSet errors; private final LinkedHashSet warnings; - private boolean debugMode; private Diagnostics() { this.errors = new LinkedHashSet<>(); this.warnings = new LinkedHashSet<>(); - this.debugMode = false; } public static Diagnostics getInstance() { @@ -35,14 +33,6 @@ public void add(LJWarning warning) { this.warnings.add(warning); } - public boolean isDebugMode() { - return this.debugMode; - } - - public void setDebugMode() { - this.debugMode = true; - } - public boolean foundError() { return !this.errors.isEmpty(); } From 6f0107d096fe216cf04f297d950371bcb9af055c Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 19 Mar 2026 17:03:52 +0000 Subject: [PATCH 4/4] Update SMTEvaluator Follows suggested print formatting Co-authored-by: Ricardo Costa --- .../src/main/java/liquidjava/smt/SMTEvaluator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 7ece2c15..4f7a7537 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -27,7 +27,7 @@ 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("Verifying: " + subRef + " <: " + supRef); + System.out.println(String.format("%s <: %s", subRef, supRef)); } try { Expression exp = toVerify.getExpression();