GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — Check calls on a constructor call whose constructor has refined param… · liquid-java/liquidjava@9c51147

File tree

Expand file treeCollapse file tree
Open diff view settings
Filter options
  • liquidjava-example/src/main/java/testSuite
    • CorrectConstructorReceiverRefinedArgument.java
    • ErrorConstructorReceiverRefinedArgument.java
  • liquidjava-verifier/src/main/java/liquidjava
    • processor/refinement_checker/object_checkers
      • AuxStateHandler.java
    • utils/constants
      • Keys.java
Expand file treeCollapse file tree
Open diff view settings
Collapse file

‎liquidjava-example/src/main/java/testSuite/CorrectConstructorReceiverRefinedArgument.java‎

Copy file name to clipboard
+23Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@StateSet({"unbound", "bound"})
8+
class CorrectRefinedArgListener {
9+
@StateRefinement(to = "unbound(this)")
10+
public CorrectRefinedArgListener() {}
11+
12+
@StateRefinement(to = "bound(this)")
13+
public CorrectRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
14+
15+
@StateRefinement(from = "bound(this)")
16+
public void accept() {}
17+
}
18+
19+
public class CorrectConstructorReceiverRefinedArgument {
20+
static void chained() {
21+
new CorrectRefinedArgListener(8080).accept();
22+
}
23+
}
Collapse file

‎liquidjava-example/src/main/java/testSuite/ErrorConstructorReceiverRefinedArgument.java‎

Copy file name to clipboard
+23Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@StateSet({"unbound", "bound"})
8+
class ErrorRefinedArgListener {
9+
@StateRefinement(to = "unbound(this)")
10+
public ErrorRefinedArgListener() {}
11+
12+
@StateRefinement(to = "bound(this)")
13+
public ErrorRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
14+
15+
@StateRefinement(from = "unbound(this)", to = "bound(this)")
16+
public void bind() {}
17+
}
18+
19+
public class ErrorConstructorReceiverRefinedArgument {
20+
static void chained() {
21+
new ErrorRefinedArgListener(8080).bind(); // Expect: State Refinement Error
22+
}
23+
}
Collapse file

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

Copy file name to clipboardExpand all lines: liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
+13-8Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -744,24 +744,29 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
744744
}
745745

746746
return name;
747-
} else if (target2.getMetadata(Keys.TARGET) != null) {
748-
// invocation is in
749-
// who did put the metadata here then?
750-
VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
751-
Optional<Variable> v = target2Vi.getParent();
752-
invocation.putMetadata(Keys.TARGET, target2Vi);
753-
return v.map(Refined::getName).orElse(target2Vi.getName());
747+
} else if (target2 instanceof CtConstructorCall<?> newCall
748+
&& newCall.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) {
749+
// `new T(args).method()` already prepared: reuse its receiver instead of creating another one
750+
invocation.putMetadata(Keys.TARGET, receiver);
751+
return receiver.getName();
754752
} else if (target2 instanceof CtConstructorCall<?> newCall
755753
&& newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) {
756-
// `new T(args).method()`: the receiver is a fresh object in the state the constructor gives
754+
// `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Must come
755+
// before the TARGET case: a constructor with refined parameters puts its (void) return value in TARGET
757756
String name = String.format(Formats.FRESH, tc.getContext().getCounter());
758757
CtTypeReference<?> type = newCall.getType();
759758
RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type,
760759
state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
761760
receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
762761
newCall.putMetadata(Keys.TARGET, receiver);
762+
newCall.putMetadata(Keys.RECEIVER, receiver);
763763
invocation.putMetadata(Keys.TARGET, receiver);
764764
return name;
765+
} else if (target2.getMetadata(Keys.TARGET) != null) {
766+
VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
767+
Optional<Variable> v = target2Vi.getParent();
768+
invocation.putMetadata(Keys.TARGET, target2Vi);
769+
return v.map(Refined::getName).orElse(target2Vi.getName());
765770
}
766771
return null;
767772
}
Collapse file

‎liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java‎

Copy file name to clipboardExpand all lines: liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java
+1Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ public final class Keys {
44
public static final String REFINEMENT = "refinement";
55
public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
66
public static final String TARGET = "target";
7+
public static final String RECEIVER = "receiver";
78
public static final String RETURN_VAR_NAME = "return_var_name";
89
public static final String THIS = "this";
910
public static final String WILDCARD = "_";

0 commit comments

Comments
0 (0)
You are visitor 01402520 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.