Correct name for an Instance

[zjp-CN]

• Context: Instance and DefId are different things #42

Since multiple closures are generated by macro, the span of which points to the callsite of the macro, we get less useful monomorphic function name lacking the order/index of closures to distinguish them.

Here are some attempts to obtain a mono fn name:

• Instance::name:
  verify::f::kani_register_contract::<(), {closure@tests/standard_proof_simple.rs:3:5: 3:27}>
• Instance::trimmed_name:
  kani_register_contract::<(), {closure@standard_proof_simple.rs:3:5}>

Unfortunately, Instance::name invokes rustc_middle::with_no_trimmed_paths under the hood, so it'd be not easy to fix.

A more reliable and simpler way to identify a mono fn is to call Instance::mangled_name. It'll give a unique name like _ZN21standard_proof_simple6verify1f22kani_register_contract17hc0e7d677161f3f51E. But not sure if the mangled name is stable.

{
  "def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
  "func": {
    "name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17h18a02e24ad3aea9fE",
    "kind": "Item",
    "file": "tests/proofs/gen_contracts_by_macros.rs",
    "src": "#[kani::requires($e)]",
    "before_expansion": "#[kani::requires($e)]"
  }
},
{
  "def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
  "func": {
    "name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17h9d0ccc93fbf12912E",
    "kind": "Item",
    "file": "tests/proofs/gen_contracts_by_macros.rs",
    "src": "#[kani::requires($e)]",
    "before_expansion": "#[kani::requires($e)]"
  }
},
{
  "def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
  "func": {
    "name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17hbf2da10a70b88b4fE",
    "kind": "Item",
    "file": "tests/proofs/gen_contracts_by_macros.rs",
    "src": "#[kani::requires($e)]",
    "before_expansion": "#[kani::requires($e)]"
  }
},
{
  "def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
  "func": {
    "name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17hc798f030eb131ab8E",
    "kind": "Item",
    "file": "tests/proofs/gen_contracts_by_macros.rs",
    "src": "#[kani::requires($e)]",
    "before_expansion": "#[kani::requires($e)]"
  }
},

[zjp-CN]

Alternatively, DefPath can act as a name, and use DefPathHash in hashing.

• cc mangled_name is unstable on platforms #75
• cc Request: expose stable hash value for DefId rust-lang/project-stable-mir#102