From aa4f012b1d9b22273e034547fe00c80369629682 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 23 Jan 2025 10:06:38 -0500 Subject: [PATCH] Add new optional flags for the cprover contracts library. - --dfcc-debug-lib activates debug asserts in cprover_contracts.c - --dfcc-simple-invalid-pointer-model removes offset nondeterminism for invalid pointers produced in failure paths of the __CPROVER_is_fresh predicate. Mitigates some proof performance issues, but is possibly unsound due to reduced nondeterminism. --- .../proofs/Makefile.common | 22 ++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common b/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common index 781cd20..7fd2302 100644 --- a/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common +++ b/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common @@ -407,9 +407,29 @@ ifdef STRING_ABSTRACTION endif endif +# User simpler invalid pointer model for contracts with DFCC. +# +# Removes offset nondeterminism for invalid pointers created in failure paths +# of the __CPROVER_is_fresh predicate. Improves performance for some proofs. +# Unsound because of reduced nondeterminism. +DFCC_SIMPLE_INVALID_POINTER_MODEL ?= +ifdef DFCC_SIMPLE_INVALID_POINTER_MODEL + ifneq ($(strip $(DFCC_SIMPLE_INVALID_POINTER_MODEL)),) + CBMC_DFCC_SIMPLE_INVALID_POINTER_MODEL := --dfcc-simple-invalid-pointer-model + endif +endif + +# Activate debug assertions in the DFCC contracts support library. +DFCC_DEBUG_LIB ?= +ifdef DFCC_DEBUG_LIB + ifneq ($(strip $(DFCC_DEBUG_LIB)),) + CBMC_DFCC_DEBUG_LIB := --dfcc-debug-lib + endif +endif + # Optional configuration library flags OPT_CONFIG_LIBRARY ?= -CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION) +CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION) $(DFCC_SIMPLE_INVALID_POINTER_MODEL) $(DFCC_DEBUG_LIB) # Proof writers could add function contracts in their source code. # These contracts are ignored by default, but may be enabled in two distinct