Skip to content

Vtable symbol mismatch causes unexpected success #160

@vecchiot-aws

Description

@vecchiot-aws

This issue should not be resolved until all tests in this PR pass when fixme is removed from the name.

When running rmc <filename> on any of the tests added in this PR, we expect a FAILURE, but get SUCCESS.

This seems to be caused by two things:

  1. When CBMC encounters a function which does not appear in the vtable, it (we believe) translates to assume(0).
  2. For dynamic traits, different naming conventions are used for insertion and lookup on the vtable.

When specifically running fixme_boxtrait_fail.rs, we receive the following log:

WARN rustc_codegen_llvm::gotoc::rvalue Unable to find vtable symbol for <Concrete as Trait>::increment. Using NULL instead

and when we view the symbol table using rmc --keep-temps fixme_boxtrait_fail.rs and opening fixme_boxtrait_fail.json, we find the following:

...
    "_ZN76_$LT$fixme_boxtrait_fail..Concrete$u20$as$u20$fixme_boxtrait_fail..Trait$GT$9increment17ha9f75436a1c6f32dE": {
      "baseName": "_ZN76_$LT$fixme_boxtrait_fail..Concrete$u20$as$u20$fixme_boxtrait_fail..Trait$GT$9increment17ha9f75436a1c6f32dE",
...
      "name": "_ZN76_$LT$fixme_boxtrait_fail..Concrete$u20$as$u20$fixme_boxtrait_fail..Trait$GT$9increment17ha9f75436a1c6f32dE",
      "prettyName": "fixme_boxtrait_fail::{impl#1}::increment",
...

Note the difference in names used: <Concrete as Trait>::increment vs fixme_boxtrait_fail::{impl#1}::increment.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] SoundnessKani failed to detect an issue

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions