Proposal: Implement lexical block level scoping in Viper

Preamble

VIP: <to be assigned>
Title: Implement lexical block-level scoping in Viper
Author: @yzhang90 @daejunpark
Type: Standard Track
Status: Draft
Created: 2017-12-1

Simple Summary

Viper should correctly implement the block-level scoping semantics in order to avoid misleading and error-prone code.

Abstract

The semantics of variable scoping is very important for a programming language because the scoping semantics determines how a (variable) name binds to the actual object. Current Viper compiler mixes several things and makes it very hard to reason about programs. We propose to use lexical block-level scoping in Viper.

Motivation

The principle behind Viper is security, simplicity and audibility. However, current scoping semantics in Viper mixes several things and sometimes makes the code misleading and error-prone. For example, Viper differentiate index variables from other local variables. Viper accepts the following program and a is equal to 10 after the for loop. In this case, a is visible outside the for block and the annotated assignment a:num is only executed once in the loop.

@public
def foo():
    for i in range(10):
        a:num
        a += 1
    b = a

Viper rejects the following program because the index variable i only lives in the for block and is not visible outside.

@public
def foo():
    for i in range(10):
        pass
    i += 1

With the current scoping rules, a program which declares a variable inside if...then...else branch or for loop is almost equivalent to declaring the variable before if or for loop. For instance,

def foo(choice: bool) -> num:
     if choice:
         a: num
         a = 1
         return a
     else:
         b: num
         b = 2
         return a + b

is equivalent to

def foo(choice: bool) -> num:
     a: num
     b: num
     if choice:
         a = 1
         return a
     else:
         b = 2
         return a + b

The difference is that for the second program, one can negate the choice variable and swap the then branch and else branch, but you could not do the same thing for the first program (because a is not defined before expression a + b!).

In addition to the above examples, we believe it is easier to formally analyze/verify programs with block-scoped variables because you do not need to modify the program in order to analyze it compositionally (i.e., moving the variable declarations to the beginning of the method, in this case). Compositional verification is very important in practice, because it gives you the divide-and-conquer needed to do proofs in parallel.

Specification

Since global variables have their own namespace self.<variable name>, we only talk about the lexical block-level scoping rules for local variables inside a function declaration.

• Variable declaration: A variable can only be declared through function parameter declaration, annotated assignment (i.e., a:num) or assignment to a undeclared variable for the first time (i.e., a = 1 where a is not declared before)

• Block scope: Only function declaration, if and for can create a block scope.

  • function declaration: When you write def foo(a:num): stmt, you introduce a block scope, and the block scope is started with all the formal parameters(i.e, a) declared and followed by stmt. The block scope ends when the function declaration finishes.
  • if statement: if(exp) then stmts introduces 1 block scope and all the statements in the then branch is executed inside this block scope. if(exp) then stmts1 else stmts2 introduce 2 block scopes. stmts1 is executed in one block scope and stmts2 is executed in the other. The two block scopes are in parallel.
  • for loop: for i in exp: stmt introduces 2 nested block with the outer block declaring the index variable i and the inner block holding the loop body stmt.

• Variables must be lexically declared before being used. For example, the following program should be rejected:

def foo():
    a += 1

• Variables should only be declared once inside a block. For example, the following program should be rejected:

def foo():
    a:num
    a = 1
    a:num
    a = 2

• Variables declared in one block should be freed when the block ends. For example, the following examples should be valid:

def foo(choice: bool):
    if (choice):
        a:num
        a += 1
    else:
        a:num
        a += 2

a should be 1 or 2 depending on the value of choice.

def foo(choice: bool):
    if (choice):
        a:num
        a += 1
    a:num
    a += 2

a should always be 2.

• Nested Block: Block can be nested. i.e., you can declare if inside for loop and so on. Variables declared in the outer-block are visible to inner-block, but not the other way around. For example,

def foo(choice: bool):
    a = 10
    if (choice):
        a += 1

a is 11 if choice is true.

However, the following program is not allowed because a is declared in the if block and it is not visible to the outer-block.

def foo(choice: bool):
    if (choice):
        a = 1
    a += 1

Regarding the for loop, since index variable is declared in the outer loop, the index variable is visible to the inner block while the loop is executed.

• Shadowing: Block cannot be used for variable shadowing because it is error-prone. For example, the following program should be rejected:

def foo(choice:bool):
    a:num
    if (choice):
        a:bool

Backwards Compatibility

If a program do not declare a variable inside if or for loop through annotated assignment or first time assignment to a non-declared variable, the behavior of the program should be the same.

Copyright

Copyright and related rights waived via CC0