-
Notifications
You must be signed in to change notification settings - Fork 127
Description
Proposed change: Refactor path handling for contracts and stubs to check for resolution errors once at the start of codegen; then maintain state about resolved functions and paths.
Motivation:
#4249 has interpret_for_contract_attribute
and interpret_stub_verified_attribute
do the exact same path resolution logic that we already did in check_attributes
. But we abort if check_attributes
errors:
kani/kani-compiler/src/kani_middle/mod.rs
Line 62 in bd6c8cf
tcx.dcx().abort_if_errors(); |
I'm envisioning that we do the resolution once in check_attributes
, abort if there's an error, and then again in the beginning of codegen, this time leveraging the fact that we know there won't be errors to store the FnResolution
only. Then codegen could pass around these resolutions as state (perhaps in the CodegenUnit
), rather than redoing path resolution every time we want to refer to the path in the attribute.
i.e. parse, don't validate!