aws / aws/aws-encryption-sdk-c
CBMC proof stubs do not replace included functions
- Dominant language
- C
- Stars
- 63
- Forks
- 59
- PR merge metrics
- No merged PRs in 30d
Description
In the `aws_cryptosdk_keyring_release` CBMC proof, a few stubs coming from `stubs/` are added to proof sources but not able to replace the corresponding functions coming from `INCLUDES`. Below is the Makefile code.
```
# aws_atomic_fetch_sub_explicit receives a volatile input, which is always model
# as non-deterministic in CBMC; thus, we need a deterministic stub for it
PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_fetch_sub_explicit.c
REMOVE_FUNCTION_BODY += aws_atomic_fetch_sub_explicit
PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_load_int.c
REMOVE_FUNCTION_BODY += aws_atomic_load_int
PROOF_SOURCES += $(PROOF_STUB)/aws_atomic_priv_xlate_order.c
REMOVE_FUNCTION_BODY += aws_atomic_priv_xlate_order
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
HARNESS_ENTRY = aws_cryptosdk_keyring_release_harness
HARNESS_FILE = $(HARNESS_ENTRY).c
PROOF_SOURCES += $(HARNESS_FILE)
REMOVE_FUNCTION_BODY += hash_proof_destroy_noop
REMOVE_FUNCTION_BODY += aws_raise_error_private
```
We have tried to force removal by adding
```
REMOVE_FUNCTION_BODY += __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_sub_explicit$link5
```
which is the name given to the function already included. We have also tried with similar names with different escape sequences.
This could be related to #625
Contributor guide
Research direction
Start with the aws_cryptosdk_keyring_release CBMC proof Makefile entries, the stubs under stubs/, and the functions listed in REMOVE_FUNCTION_BODY. Compare how functions from INCLUDES are selected and removed, including the __CPROVER_file_local_atomics_gnu_inl_aws_atomic_fetch_sub_explicit$link5 name, and review related issue #625. Done means the intended stubs replace the included functions in this proof.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- c
- Domain
- build-system, testing
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100