apl-cornell / fabric

Distributed persistent programming language with secure information flow types
http://www.cs.cornell.edu/projects/fabric/
Other
28 stars 4 forks source link

Label checking fails if `this` is not explicitly dereferenced #9

Open K33TY opened 7 years ago

K33TY commented 7 years ago
    public String{L} toString{L}()
    {
        return toLongString(); 
    }

Results in the following error:

[apply] /Users/Elizabeth/Desktop/MEng_Project/Calendar-Fabric/prototype/fabric/util/Date.fab:606: [apply] Unsatisfiable constraint [apply] general constraint: [apply] pc ⊑ callee_PC_bound [apply] in this context: [apply] {caller_pc} ⊑ L [apply] cannot satisfy equation: [apply] {caller_pc} ⊑ L [apply] in environment: [apply] {this} ⊑ {L ⊔ ⊥→⊥; ⊥←⊥} [apply] L ⊑ {⊤→this.store$} [apply] L ⊑ {⊤→this.store$} [apply] {⊤←this.store$} ⊑ L [apply] {this} ⊑ {caller_pc} [apply] [] [apply] [apply] Label Descriptions [apply] ------------------ [apply] - pc = label of the program counter at this call site [apply] - pc = {caller_pc} [apply] - callee_PC_bound = lower bound on the side effects of the method public [apply] java.lang.String toLongString() [apply] - callee_PC_bound = L [apply] - caller_pc = pc label [apply] - L = label parameter L of class prototype.fabric.util.Date [apply] - this = label of the special variable "this" in [apply] prototype.fabric.util.Date[label L, principal p] [apply] [apply] Calling the method at this program point may reveal too much information [apply] to the receiver of the method call. public java.lang.String [apply] toLongString() can only be invoked if the invocation will reveal no more [apply] information than the callee's begin label, callee_PC_bound. However, [apply] execution reaching this program point may depend on information up to the [apply] PC at this program point: pc. [apply] return toLongString(); [apply] ^------------^ [apply] [apply] 1 error. [apply] null

However, putting "this" in front allows it to compile:

    public String{L} toString{L}()
    {
        return this.toLongString(); 
    }

Shouldn't it know that the previous invocation is referencing "this" already?