jennalwise
commented
2 years ago Major Issue causing the above error:
//@unfold avlh(node->right->left, node->right->leftHeight); on line 194 has its predicate optimistically assumed and the verifier at this point does not know whether node->right->left is null (probably due to optimism) and so when the predicate body is produced it branches on whether node->right->left is null or not and that information is added to the path condition. Permission to node->right->left is saved in the optimistic heap as well at this point. Upon analyzing the next line: rllh = node->right->left->leftHeight; eval is used to evaluate the rhs which looks for permission to node->right->left->leftHeight in the symbolic heaps. It is not there, so the verifier optimistically assumes it has access to it (thanks to imprecision) and adds permission to it into the optimistic heap. This creates an invalid state as permission to node->right->left->leftHeight implies node->right->left != null and the path condition contains node->right->left == null. Instead, the verifier should fail execution down this path at the point where eval looks to assume permission to node->right->left->leftHeight as doing so contradicts currently known information by the verifier. Other places where eval/eval-pc are used should be reconsidered for correctness based on the aforementioned realization.
Viper does not need to worry about this functionality in eval, because they fail if an accessibility predicate for a field is not available in the symbolic heap and an accessibility predicate implies the field receiver is not null.
Certain permutations of AVL cause static verification to fail with the following exception:
The following three permutations recreate this issue: