Force return statement check

[jacqueswww]

What's your issue about?

Currently you can have a return type set on a function, yet omit the return statement. Add a exception when this happens forcing the programming to add a return, if specified.

e.g.

@public
def foo() -> num:
        pass

How can it be fixed?

Off the top of my head, check parse_func.

Cute Animal Picture

[fubuloubu]

As I think @yzhang90 has noted, this is actually subtletly very hard (but I'd argue still necessary) because of blocks, for example the following would pass your check but still fail to return anything:

def Foo(a: bool) -> num:
    if a:
         return 1

[DavidKnott]

I think we could track each path and make sure each one has a return. That being said, a good first step would be to check for the existence of any return.

[fubuloubu]

Agreed. And I think currently viper programs will probably be simple enough that most if branches in methods would be nested only once or twice (e.g. if: if: ... else: ... else: if: ... else: ...), so the number of total branches to keep track of should be fairly managable. I think the right upper bound is 2^n branches where n is the amount of nesting. The gas limit should impose an economic upper bound on this I would think.

[jacqueswww]

Actually it's probably much simpler than that, we have a checker that check correct return statements by type. And we just then need to make sure each function has at minimum one return. All those in the ifs will be handled by the return type checker, ie. Not None. ;)

[jacqueswww]

I will tackle this one next, it's just building a map of functions that have return and erroring if any are missing (my gut feel says just populating a map in parse_return) , will show you :)

[fubuloubu]

@jacqueswww How does your proposal deal with this:

def foo(a: bool) -> num:
    if a:
        return 1

[jacqueswww]

Ah I see, now. I have a few ideas. Looking forward to challenge ;)

[fubuloubu]

or this (this should pass):

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

[fubuloubu]

It shouldn't be too hard, my point is it is a harder algorithm because you have to explore 2**n branches

[fubuloubu]

And also the result if no return is taken in some subset of branches (and deferred to the end)

[fubuloubu]

P.S. I think this is actually a formal verification problem lol

[jacqueswww]

Yes you are right, one will have to figure out a way for the branches to take the default else into account, hmmm let me research it some more. 😂

[fubuloubu]

Yeah, I think there are standard FV algorithms for doing this, I think it usually involves holding an additional bookkeping variables while you're parsing a given function, then testing those instead.

[jacqueswww]

@fubuloubu @DavidKnott consider this rule set:

1.) There must be at least one return statement in every function.
2.) If there is a nested return statement a default return must be set OR trace all other nested returns and ensure they exist.

The problem with a nested return comes in that all paths have to be considered as you mentioned, however if we force the rule of a default return statement. Are we perhaps gaining clarity in the program ? And thereby simplifying this check. I personally always read default returns better than nested ones:

def a() -> num:
    if ...:
        return 1
    else:
        return 2

Is more difficult for me to read than:

def a() -> num:
    if ...:
        return 1
    return 2

Maybe I am the exception ;) But the one thing we can agree on to implement so long, is the check for rule 1. I will proceed with the partial PR so long that does that check.

[fubuloubu]

1 is a good start and get's us halfway there, I think that is okay to add.

2 requires that much more advanced check, and since checking for a default return is a special case of the general problem of branched returns, I don't think we want to arbitrarily disallow a certain type of style as a first step, so I think we need to leave 2 to when both parts of the check can be performed. Which means really just the general case check of branched returns, since default return is simply a special case.

2 will override 1 when it is complete.