opprop / immutability

The Practical Immutability for Classes and Objects (PICO) type system enforces transitive class and object immutability
Other
3 stars 5 forks source link

Add some examples #48

Open wmdietl opened 2 months ago

wmdietl commented 2 months ago

@txiang61 @Ao-senXiong I've split off the recent pushes to master into this PR. Please modify #45 to fix this example before we merge it.

Ao-senXiong commented 2 months ago

Thanks!

Ao-senXiong commented 2 months ago

@wmdietl @txiang61 Let's use this PR for discussion then.

I have run this example use current PICO checker in #43 with the following errors issued.

JavaExamples.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable Set<String> new_s1 = s; // ERROR, type incompatible
                                      ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:11: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set</*RAW*/>
  required: @Mutable Set</*RAW*/>
JavaExamples.java:18: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set</*RAW*/>
  required: @Mutable Set</*RAW*/>
JavaExamples.java:30: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable List<String> v2 = s.get(l); // ERROR
                                        ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:31: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        v.add("x"); // ERROR
             ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:36: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        p.family.add("Jenny"); // ERROR, can not mutate immut list
                    ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:54: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        this.family.add("Mom"); // ERROR
                       ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:62: error: [return.type.incompatible] incompatible types in return.
        return family; // ERROR, type incompatible
               ^
  type of expression: @Immutable List<@Immutable String>
  method return type: @Mutable List<@Immutable String>
JavaExamples.java:87: error: [type.argument.type.incompatible] incompatible type argument for type parameter T of MutList.
    void foo1 (ImmutSet<MutList<T>> s) {  // ERROR
                                ^
  found   : T extends @Readonly Object
  required: [extends @Readonly Object super @Mutable NullType]
9 errors
Ao-senXiong commented 3 weeks ago

After this PR on CF https://github.com/eisop/checker-framework/pull/793,

the error message are expected:

JavaExamples.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable Set<String> new_s1 = s; // ERROR, type incompatible
                                      ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:11: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:18: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:30: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable List<String> v2 = s.get(l); // ERROR
                                        ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:31: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        v.add("x"); // ERROR
             ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:36: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        p.family.add("Jenny"); // ERROR, can not mutate immut list
                    ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:54: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        this.family.add("Mom"); // ERROR
                       ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:62: error: [return.type.incompatible] incompatible types in return.
        return family; // ERROR, type incompatible
               ^
  type of expression: @Immutable List<@Immutable String>
  method return type: @Mutable List<@Immutable String>
JavaExamples.java:87: error: [type.argument.type.incompatible] incompatible type argument for type parameter T of MutList.
    void foo1 (ImmutSet<MutList<T>> s) {  // ERROR
                                ^
  found   : T extends @Readonly Object
  required: [extends @Readonly Object super @Mutable NullType]