scribble icon indicating copy to clipboard operation
scribble copied to clipboard

Warn users when annotations may add inifinte loops

Open cd1m0 opened this issue 4 years ago • 1 comments

Instrumentation turns the following terminating code into non-terminating code:

contract Foo {
        function double1(uint x) public view returns (uint) {
                return double2(x);
        }

        /// if_succeeds $result == double1(x);
        function double2(uint x) public view returns (uint) {
                return x + x;
        }
}

We can use the callgraph of the original code to detect when function calls in the annotations may create cycles and issue warnings for users that the annotations may introduce infinite recursion. For example this check shouldn't flag anything in the following sample:

contract Foo {
        /// if_succeeds $result == double2(x);
        function double1(uint x) public view returns (uint) {
                return x * 2;
        }       

        /// if_succeeds $result == double1(x);
        function double2(uint x) public view returns (uint) {
                return x + x;
        }       
}

cd1m0 avatar Apr 23 '21 09:04 cd1m0

This is not straightforward, as sometimes we can encounder conditional constructs in annotations and in functions. Therefore, in case of naive implementation some produced warnings might be misleading.

blitz-1306 avatar Jun 05 '23 05:06 blitz-1306