Audit Vtable generation for dynamic traits

[danielsn]

RMC handles dynamic traits by making a vtable for each trait, which maps virtual calls to the function pointer that implements the call. As of 2021-09-01, our implementation of dynamic traits has no known soundness issues.

Likelihood:

Due to the complexity of this feature, there may be currently-unknown soundness issues.

Mitigation:

• The default flags RMC passes to CBMC now include --pointer-check, so incorrect codegen of functions is now more likely to be found a verification time.
• We have added 40+ regression tests for dynamic traits.

[avanhatt]

Updated description to match current state.

[adpaco-aws]

RMC is now using --pointer-check by default (#263)

[avanhatt]

Updated to reflect that --pointer-check is used by default and that for closures we only fail for boxed closures.

[avanhatt]

Updated to reflect that all known cases of boxed closures now work.

[avanhatt]

As of 2021-09-01, all known soundness issues specific to dynamic traits objects and vtables have been resolved.

However, two issues to note:

• In certain cases of trait objects nested automatic reference counted objects, we generate invalid calls to the drop destructor. For now, we maintain soundness here by codegening an unimplemented block, which would cause code that relies on this behavior to fail at verification time: Fix drop type checking for nested Arc/Mutex objects #426
• We have some test cases with print statements that fail verification, which is likely due to unrelated issues with how we handle print: Incorrect verification success on print statement #194