Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incompleteness with the closure encoding #723

Open
jcp19 opened this issue Feb 4, 2024 · 4 comments
Open

Incompleteness with the closure encoding #723

jcp19 opened this issue Feb 4, 2024 · 4 comments

Comments

@jcp19
Copy link
Contributor

jcp19 commented Feb 4, 2024

In Scion, I have a program of the following form:

func (d *DataPlane) Run() {
    read /*@@@*/ :=
		// spec hidden
		func /*@ rc @*/ (ingressID uint16, rd BatchConn) {
                    // ...
                }
    cl := 
        // @ requires acc(&read, _) && read implements rc
        func /*@ closure1 @*/ (c BatchConn) {
                // @ assert read implements rc
		read(0, c) //@ as rc // (*)
	}
   go cl(d.internal) // @ as rc
}

Unfortunately, the call to read in (*) fails with the following perplexing error

Error at: </Users/joao/code/VerifiedSCION/router/dataplane.go:1046:5> Precondition of call read(0, c) as rc might not hold. 
read might not implement rc.

Note that this precondition is asserted immediately before the call. Looking at the generated Viper code reveals the failing precondition (marked in blue):
image

image

The problem is that, at the source program level, there is no way to write a term that encodes to closureGet$rc_Run_80c2a36d_F0(d_V0_RN3), except for the allocation of a closure.

@jcp19
Copy link
Contributor Author

jcp19 commented Feb 14, 2024

This could be addressed in tandem with #713

@jcp19
Copy link
Contributor Author

jcp19 commented Feb 14, 2024

Minimal example:

package closure_err

func f() {
	i@ := 0
	x@ :=
		preserves acc(&i) 
		func x1() {
			i += 1
		}
	g :=
		requires acc(&x, _)
		requires x implements x1
		preserves acc(&i)  
		func g1() {
			x() as x1
		}
}

@Felalolf
Copy link
Contributor

From my perspective, this is a design problem and not a problem of the encoding. Function literal names are not full specifications because the captured variables are missing. As a consequence, you cannot call a closure with the function literal contract outside of the immediate context. To call the closure inside of another closure, you have to give the called closure a proper specification:

ghost
preserves acc(i)
decreases _
func xSpec(ghost i *int)

func f() {
	i@ := 0
	x@ :=
		preserves acc(&i)
		decreases _
		func x1() {
			i += 1
		}

   ghost pi := &i // for some reason, typechecker complains about &i in the next line

	proof x implements xSpec{pi} {
	    x() as x1
	}

	g :=
		requires acc(&x, _)
		requires x implements xSpec{&i}
		preserves acc(&i)
		func g1() {
			x() as xSpec{&i}
		}

    assert g != nil
}

Admittedly, doing it as shown above is more verbose than referring to the x1 directly.

I see two points:

  1. Currently, x implements x1 should be rejected to avoid misunderstandings. Its current encoding is not incorrect, but also not useful.
  2. As an improvement, we could make function literal names a full specification within the scope of the captured variables (by statically inferring the captured variables). That means that x implements x1 is ok within the scope of the literal definition. x implements x1 could then be encoded to the getClosure expression or an implements expression with an additional argument. In both cases, the captured variables are inferred statically.

@Felalolf
Copy link
Contributor

I though about is bit more. I am not completely sure whether the following approach works, but I wanted to document it for now:

Currently, captured variables are encoded via uninterpreted getters. If captured variables are only encoded in implements expressions and calls for function literals, then instead of using uninterpreted getters, we might be able to just use the captured variable dircectly. The reasoning is that implements expressions and call for function literals can only happen in the scope of the function literal, which should be the same scope of the captured variables.

This requires (1) a careful naming scheme in the desugared representation such that captured variable parameters always have the same name for the same captured variable and (2) that x implements x1 is encoded to something with the captured variable as a parameter.

One challenge of the encoding is that how captured variables are replaced in different within a closure and outside a closure. Inside a closure, the captured variable is some paramter. Outside a closure, the captured variable is a reference to some parameter. At the Viper level, both are encoded to the same, namely just the variable. One solution might be to always use an exclusive variable with the pointer type, even outside of closures. Unless I am missing something, an exclusive variable with a pointer type should be translated correctly outside of the closure because the encoding does not check whether a variable with the same type was actually defined (which does not hold because the actual variable has the element type of the pointer type).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants