There might be insufficient permission to access marked_execution_tree.children[0].function_name

[RCoeurjoly]

nagini complaints about insufficient permissions, although I have given permissions to the marked_execution_tree.children list and also to all function_name with a Forall.

from typing import Optional, List, Tuple
from nagini_contracts.contracts import *

class Node:
    def __init__(self, function_name: str, children:List['Node']) -> None:
        self.function_name = function_name # type: str
        self.children = children # type: List['Node']
        Ensures(Acc(self.function_name) and self.function_name is function_name and
                Acc(self.children) and self.children is children)

@Pure
def can_node_be_compressed(marked_execution_tree: 'Node') -> Tuple[bool, int]:
    """Searches for the longest compression possible. Returns:
    - bool: True if can be compressed. False otherwise
    - int: If it can be compressed, number of nodes to compress"""
    Requires(Acc(marked_execution_tree.children))
    Requires(Acc(list_pred(marked_execution_tree.children)))
    Requires(Forall(marked_execution_tree.children, lambda node: Acc(node.function_name)))
    Requires(Acc(marked_execution_tree.function_name))
    Ensures(Implies(Result()[1] > 0, Result()[0] is True))
    if len(marked_execution_tree.children) != 1:
        return False, 0
    if marked_execution_tree.children[0].function_name != marked_execution_tree.function_name:
        return False, 0
    # _, downstream_length = can_node_be_compressed(marked_execution_tree.children[0])
    # return True, downstream_length + 1

nagini output:

WARNING: Found non-basic heap chunk type; quantified chunks are currently not supported and will not be shown in counterexamples. WARNING: Found non-basic heap chunk type; quantified chunks are currently not supported and will not be shown in counterexamples. Verification failed Errors: Function can_node_be_compressed might not be well-formed. There might be insufficient permission to access marked_execution_tree.children[0].function_name. (nagini.py@12.0). Store: marked_executiontree -> Node0 Heap: list0 -> { len(list0) -> 1, list0[] -> Node1 }, Node0 -> { children -> list0 }

Verification took 8.70 seconds.

[marcoeilers]

This is a triggering problem on the SMT level. The problem is that the quantifier that contains the permission (Forall(marked_execution_tree.children, lambda node: Acc(node.function_name))) is not triggered by the expression that needs it; it will be triggered for any node.function_name if the fact that node in marked_execution_tree.children is directly mentioned somewhere.

If you rewrite the quantifier to Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children), Acc(marked_execution_tree.children[i].function_name))), which is semantically equivalent, it will get triggered whenever you have an expression of the form marked_execution_tree.children[i].function_name, so the function will verify.

[marcoeilers]

I should add: While this is not obvious and requires some understanding of what's going on on the SMT level, this kind of behavior of quantifiers is expected and not a bug, and can be worked around by rewriting the quantifier as described above. I'm happy to answer any questions of course, but I'll close the issue for now.

[RCoeurjoly]

Thanks!