From 28b996132037a956df8bf8fcb6cf6cd89935d3f0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 13 Feb 2026 14:59:47 +0000 Subject: [PATCH] Add Boxed Types Support --- .../main/java/testSuite/CorrectBoxedTypes.java | 18 ++++++++++++++++++ .../main/java/testSuite/ErrorBoxedBoolean.java | 12 ++++++++++++ .../main/java/testSuite/ErrorBoxedDouble.java | 12 ++++++++++++ .../main/java/testSuite/ErrorBoxedInteger.java | 12 ++++++++++++ .../liquidjava/smt/TranslatorContextToZ3.java | 18 +++++++++--------- .../src/main/java/liquidjava/utils/Utils.java | 3 +-- 6 files changed, 64 insertions(+), 11 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java new file mode 100644 index 00000000..1a404775 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java @@ -0,0 +1,18 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class CorrectBoxedTypes { + public static void main(String[] args) { + @Refinement("_ == true") + Boolean b = true; + + @Refinement("_ > 0") + Integer i = 1; + + @Refinement("_ > 0") + Double d = 1.0; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java new file mode 100644 index 00000000..93c6a3c1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedBoolean { + public static void main(String[] args) { + @Refinement("_ == true") + Boolean b = false; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java new file mode 100644 index 00000000..643b509a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedDouble { + public static void main(String[] args) { + @Refinement("_ > 0") + Double d = -1.0; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java new file mode 100644 index 00000000..2d937e20 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedInteger { + public static void main(String[] args) { + @Refinement("_ > 0") + Integer j = -1; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index c3fb32dc..08749a07 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -42,10 +42,10 @@ public static void storeVariablesSubtypes(Context z3, List vari private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); return switch (typeName) { - case "int", "short" -> z3.mkIntConst(name); - case "boolean" -> z3.mkBoolConst(name); - case "long" -> z3.mkRealConst(name); - case "float", "double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); + case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.mkIntConst(name); + case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name); + case "long", "java.lang.Long" -> z3.mkRealConst(name); + case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; @@ -81,11 +81,11 @@ private static void addBuiltinFunctions(Context z3, Map> fun static Sort getSort(Context z3, String sort) { return switch (sort) { - case "int" -> z3.getIntSort(); - case "boolean" -> z3.getBoolSort(); - case "long" -> z3.getRealSort(); - case "float" -> z3.mkFPSort32(); - case "double" -> z3.mkFPSortDouble(); + case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.getIntSort(); + case "boolean", "java.lang.Boolean" -> z3.getBoolSort(); + case "long", "java.lang.Long" -> z3.getRealSort(); + case "float", "java.lang.Float" -> z3.mkFPSort32(); + case "double", "java.lang.Double" -> z3.mkFPSortDouble(); case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); case "String" -> z3.getStringSort(); case "void" -> z3.mkUninterpretedSort("void"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1cf45bc7..1e99e3f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { private static boolean hasRefinementValue(CtAnnotation annotation, String refinement) { Map values = annotation.getValues(); - return Stream.of("value", "to", "from") - .anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); + return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } }