Feat memory locations referrers

[MikaelMayer]

Fixes #6363

What was changed?

• Added support for the built-in unary expression referrers(o): set<(object, field)> where o is an object.
  • Support for parsing, resolving and printing
  • Support for rules that describe how referrers changes from before an assignment to afterwards
  • Support for $ReferrersHeap and update/read referrers heap in the Dafny prelude.
  • Support for methods to declare they modify the entire referrers heap by default until we have referrers modifies clauses.
  • Support for declaring that any unsupported assignment will havoc all referrers, for soundness.
  • New BoogieGenerator.Referrers.cs file to gather all rules related to referrers, including
    • Rules when pre-assigning local variables and object members
    • Rules when post-assigning local variables and object members
    • Rules for initializing objects
    • Rules for initializing arrays with a lambda expression (the most complex so far)
• Added support for declaring this as a special local field per non-static method, so that we can use locals`this as a referrer - and added special support to parse this as a field name.
• Added support for f.IsGhost if f is a field. Since the only way to write a field currently is to write something like o`f, one can detect in Dafny if a field is ghost by writing o`f.1.IsGhost, which was not possible before.
• Fixed so that special fields from local variables inherit the same ghostness
• Added IndexIField_Inverse(f) in the DafnyPrelude.bpl so that IndexField is proved injective, and it makes it possible to write the axiom of referrers for array assignments without existential quantifier in positive position.

Semantic differences

• Since unassigned variables should not try to remove themselves from the referrers of their previous values, I had no other choice than assuming that unassigned variables are really unassigned, meaning their assignment tracker is now set to "false" at declaration.
• This makes using an unassign variable generate a contradiction for any further statements. I think this is acceptable. I modified tests to reflect that

Other add-ons and refactorings

• make prelude compiles the prelude now and works without C++ preprocessors
• Added ExprHeapUsage as a way to differentiate the booleans that indicate which heap an expression is using: The current one, the old one and the referrers heap. That helped clarify a few booleans. This differs from HeapReadingStatus which is affected for functions.
• Added HeapExpressions to expression translators so that all heaps are under the same object, it will be easier to maintain and generalize to more heaps.
• Ensure the name "constructor" can be recognized s the name of a method for memory location's sake, by mapping it to the internal name "_ctor"

How has this been tested?

• Added 4 tests: One referrers.dfy that now passes, another one referrers-resolutionerrors.dfy that does not pass and will never, another one referrers-unsupported.dfy that contain code supposed to work in the future but does not yet. finally, another one referrers-errors.dfy that captures verification errors, including absence of detectable soundness issue.

TODO

• Extract Fix Opaque blocks prove variable previously assigned #6363 (?)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.