From ce4e764b08dc7436718e7377db7486b082ab84a8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 6 Nov 2025 11:33:02 +0000 Subject: [PATCH 1/2] Set `this` As Default Argument in Ghost Invocations --- .../classes/input_reader_correct/Test.java | 16 ++++------ .../InputStreamReaderRefs.java | 31 +++++++++++++++++++ .../Test.java | 12 +++++++ .../classes/input_reader_error/Test.java | 1 - .../liquidjava/rj_language/Predicate.java | 4 +-- .../visitors/CreateASTVisitor.java | 8 +++-- 6 files changed, 57 insertions(+), 15 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/Test.java index b0cff58d..3eb63372 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/Test.java @@ -1,16 +1,12 @@ package testSuite.classes.input_reader_correct; -@SuppressWarnings("unused") +import java.io.InputStreamReader; + public class Test { public static void main(String[] args) throws Exception { - // Arrays are not well supported in LiquidJava - - // InputStreamReader isr = new InputStreamReader(new FileInputStream("test1.txt")); - // @Refinement("_ > -9") - // int a = isr.read(); - // char[] arr = new char[20]; - // int b = isr.read(arr, 10, 5); - // System.out.println(arr); - // isr.close(); + InputStreamReader is = new InputStreamReader(System.in); + is.read(); + is.read(); + is.close(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java new file mode 100644 index 00000000..126da6ee --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java @@ -0,0 +1,31 @@ +package testSuite.classes.input_reader_correct_default_this; + +import java.io.InputStream; +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; + +// https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html +@ExternalRefinementsFor("java.io.InputStreamReader") +public interface InputStreamReaderRefs { + + @RefinementPredicate("boolean open(InputStreamReader i)") + @StateRefinement(to = "open()") + public void InputStreamReader(InputStream in); + + @StateRefinement(from = "open()", to = "open()") + @Refinement("(_ >= -1) && (_ <= 127)") + public int read(); + + @StateRefinement(from = "open()", to = "!open()") + public void close(); + + @StateRefinement(from = "open()", to = "open()") + @Refinement("_ >= -1") + public int read( + @Refinement("length(cbuf) > 0") char[] cbuf, + @Refinement("_ >= 0") int offset, + @Refinement("(_ >= 0) && (_ + offset) <= length(cbuf)") int length); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java new file mode 100644 index 00000000..c5eeafda --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java @@ -0,0 +1,12 @@ +package testSuite.classes.input_reader_correct_default_this; + +import java.io.InputStreamReader; + +public class Test { + public static void main(String[] args) throws Exception { + InputStreamReader is = new InputStreamReader(System.in); + is.read(); + is.read(); + is.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java index 85d7dc67..5a9f0aae 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java +++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java @@ -6,7 +6,6 @@ public class Test { public static void main(String[] args) throws IOException { - // java.io.InputStreamReader.InputStreamReader InputStreamReader is = new InputStreamReader(System.in); is.read(); is.read(); 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 1f476f15..8ffbbd9d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -261,9 +261,9 @@ public static Predicate createVar(String name) { return new Predicate(new Var(name)); } - public static Predicate createInvocation(String name, Predicate... Predicates) { + public static Predicate createInvocation(String name, Predicate... predicates) { List le = new ArrayList<>(); - for (Predicate c : Predicates) + for (Predicate c : predicates) le.add(c.getExpression()); return new Predicate(new FunctionInvocation(name, le)); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 102c9e58..9ddc2b35 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -161,9 +161,13 @@ else if (rc instanceof VarContext) { private Expression functionCallCreate(FunctionCallContext rc) { if (rc.ghostCall() != null) { GhostCallContext gc = rc.ghostCall(); - List le = getArgs(gc.args()); String name = Utils.qualifyName(prefix, gc.ID().getText()); - return new FunctionInvocation(name, le); + List args = getArgs(gc.args()); + if (args.isEmpty()) { + // if no args provided, add "this" as default + args.add(new Var("this")); + } + return new FunctionInvocation(name, args); } else { AliasCallContext gc = rc.aliasCall(); List le = getArgs(gc.args()); From 06c8e237830a4580349ebbc7520aef1f9a9b029d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 6 Nov 2025 11:40:22 +0000 Subject: [PATCH 2/2] Change Test --- .../ArrayListRefinements.java | 18 +++++++++++ .../Test.java | 11 +++++++ .../InputStreamReaderRefs.java | 31 ------------------- .../Test.java | 12 ------- 4 files changed, 29 insertions(+), 43 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/Test.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/ArrayListRefinements.java new file mode 100644 index 00000000..ac59869c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/ArrayListRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.index_out_of_bounds_default_this_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +@Ghost("int size") +public interface ArrayListRefinements { + + public void ArrayList(); + + @StateRefinement(to = "size() == size(old()) + 1") + public boolean add(E elem); + + public E get(@Refinement("_ < size()") int index); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/Test.java new file mode 100644 index 00000000..020544c3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_default_this_correct/Test.java @@ -0,0 +1,11 @@ +package testSuite.classes.index_out_of_bounds_default_this_correct; + +import java.util.ArrayList; + +public class Test { + public static void main(String[] args) { + ArrayList l = new ArrayList<>(); + l.add(1); + l.get(0); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java deleted file mode 100644 index 126da6ee..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java +++ /dev/null @@ -1,31 +0,0 @@ -package testSuite.classes.input_reader_correct_default_this; - -import java.io.InputStream; -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Ghost; -import liquidjava.specification.Refinement; -import liquidjava.specification.RefinementPredicate; -import liquidjava.specification.StateRefinement; - -// https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html -@ExternalRefinementsFor("java.io.InputStreamReader") -public interface InputStreamReaderRefs { - - @RefinementPredicate("boolean open(InputStreamReader i)") - @StateRefinement(to = "open()") - public void InputStreamReader(InputStream in); - - @StateRefinement(from = "open()", to = "open()") - @Refinement("(_ >= -1) && (_ <= 127)") - public int read(); - - @StateRefinement(from = "open()", to = "!open()") - public void close(); - - @StateRefinement(from = "open()", to = "open()") - @Refinement("_ >= -1") - public int read( - @Refinement("length(cbuf) > 0") char[] cbuf, - @Refinement("_ >= 0") int offset, - @Refinement("(_ >= 0) && (_ + offset) <= length(cbuf)") int length); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java b/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java deleted file mode 100644 index c5eeafda..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java +++ /dev/null @@ -1,12 +0,0 @@ -package testSuite.classes.input_reader_correct_default_this; - -import java.io.InputStreamReader; - -public class Test { - public static void main(String[] args) throws Exception { - InputStreamReader is = new InputStreamReader(System.in); - is.read(); - is.read(); - is.close(); - } -}