[Request] Allow function calls in quantifier bodies.

[JustusAdam]

Function calls are currently supported in function contracts, however they are not allowed in quantifiers. This is inconsistent and unintuitive, since the logical restrictions for function calls in contracts apply the same way in quantifiers.

Having the capability to call functions in quantifiers is important for the implementation of model-checking/kani#2546. This is for two reasons

1. The code generation in that implementation turns the body of Rust-level quantifiers into a function and then calls that function from the goto-C-level quantifier. This could be worked around but
2. Small functions (especially methods) are very common in Rust, e.g. the std::ops::Eq::eq function which overloads == or std::ops::Ord::cmp which overloads comparison. As a result these are likely to be used by users of kani's function contracts.

I would ask that CBMC should lift the arbitrary restriction on function calls in quantifiers and enforce side-effect freedom the same way it does in function contracts otherwise.

[feliperodri]

There are two major issues:

1. How can we ensure the functions inside quatifiers are side-effect free?
2. These function calls will be for GOTO functions. GOTO functions are sequential functions with statements and not pure mathematical function. How the SMT back-end would understand these calls? What if the function dereference pointer, for instance, how would you represent that in a way that the SMT back-end would understand?

[JustusAdam]

Well I think we can apply the same solution we do elsewhere:

1. Side effects are also an issue when using function calls in contracts period. Whatever detection/restriction mechanism is applied there should be good enough for quantifiers too.
2. Isn't it currently possible to dereference a pointer from the surrounding environment in the expression inside a quantifier or does CBMC somehow disallow that? For instance

   void set_0(int * i, int[] arr)
   __CPROVER_ensures(__CPROVER_forall(int j; *i != j || arr[*i] == 0))
   { arr[*i] = 0; }

Let me know if I'm begin naïve or wrong here.