--object-bits and --unwind flag missing at checking safety properties and coverage step
#209
Comments
QinyuanWu
changed the title
--object-bits and --unwind flag missing at checking safety properties step--object-bits and --unwind flag missing at checking safety properties and coverage step
|
I saw the following comment in the Makefile: @qinheping since we are using both |
Could you try to identify loops beside those in the dfcc built-in function with the CBMC flag |
|
I suspect that your use of |
|
@qinheping currently there's no non-built-in loops left, the only one not related to dfcc is |
|
@tautschnig for the @qinheping I ended up modifying the analysis command in # Targets to run the analysis commands
ifdef CBMCFLAGS
ifeq ($(strip $(CODE_CONTRACTS)),)
CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY) $(CBMC_DEFAULT_UNWIND) #added $(CBMC_DEFAULT_UNWIND) here
endif
endifIs this okey practice or would you foresee any issue with adding this flag for other proofs that uses loop contract and dfcc? I still don't know why we need |
All loops except for |
|
Is the unbounded version of |
We don't have any plan for unbounded version of |
|
Thank you! I was attempting the loop contract myself and came up with this version: #ifndef __CPROVER_STRING_H_INCLUDED
#include <string.h>
#define __CPROVER_STRING_H_INCLUDED
#endif
#undef memcmp
inline int memcmp(const void *s1, const void *s2, size_t n)
{
__CPROVER_HIDE:;
int res=0;
#ifdef __CPROVER_STRING_ABSTRACTION
__CPROVER_precondition(__CPROVER_buffer_size(s1)>=n,
"memcmp buffer overflow of 1st argument");
__CPROVER_precondition(__CPROVER_buffer_size(s2)>=n,
"memcmp buffer overflow of 2nd argument");
#else
__CPROVER_precondition(__CPROVER_r_ok(s1, n),
"memcmp region 1 readable");
__CPROVER_precondition(__CPROVER_r_ok(s2, n),
"memcpy region 2 readable");
const unsigned char *sc1=s1, *sc2=s2;
for(; n!=0; n--)
__CPROVER_assigns(n, res, sc1, sc2)
__CPROVER_loop_invariant(n >= 0 && n <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
__CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(sc1) <= __CPROVER_loop_entry(n)
&& __CPROVER_POINTER_OFFSET(sc2) <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(sc1) == __CPROVER_POINTER_OFFSET(sc2)
&& __CPROVER_POINTER_OFFSET(sc1) == __CPROVER_loop_entry(n) - n)
__CPROVER_decreases(n)
{
res = (*sc1++) - (*sc2++);
if (res != 0)
return res;
}
#endif
return res;
}
int main() {
unsigned str1_len;
unsigned str2_len;
__CPROVER_assume(str1_len <= str2_len);
char str1[str1_len];
char str2[str2_len];
unsigned len;
__CPROVER_assume(len <= str1_len);
memset(str1, "a", str1_len);
memset(str2, "a", str2_len);
memcmp(str1, str2, len);
return 0;
}I was originally missing the |
|
In other words, if a loop returns or breaks in the middle of an iteration, does CBMC not check the invariant for this last iteration? No, CBMC doesn't check if the loop invariant hold after |
|
Got it. When I was experimenting with the loop contract, I found that if we switched the last invariant clause to the commented line then the loop would fail to be inductive. I'm curious to understand what makes the loop invariant fail with the commented one. const unsigned char *sc1=s1, *sc2=s2;
for(; n!=0; n--)
__CPROVER_assigns(n, res, sc1, sc2)
__CPROVER_loop_invariant(n >= 0 && n <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
//__CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(sc1) <= __CPROVER_loop_entry(n)
// && __CPROVER_POINTER_OFFSET(sc2) <= __CPROVER_loop_entry(n)) why is this not inductive?
__CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(sc1) == __CPROVER_POINTER_OFFSET(sc2)
&& __CPROVER_POINTER_OFFSET(sc1) == __CPROVER_loop_entry(n) - n) // this makes the loop inductive
__CPROVER_decreases(n)
{
res = (*sc1++) - (*sc2++);
if (res != 0)
return res;
}error message when using the commented out clause: I also tried to switch the last loop invariant to error trace: |
|
Okey after some brainstorming, I had the following thoughts: Could you please confirm if my reasoning is correct? |
|
Yes, you are correct. If you look at the trace, the last assignment to |
|
Great thank you very much! |
|
I realized an issue with using const unsigned char *sc1=s1, *sc2=s2;
for(; n!=0; n--)
__CPROVER_assigns(n, res, sc1, sc2)
__CPROVER_loop_invariant(n >= 0 && n <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
__CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n)) //pointer relation: pointer outside object bounds in sc1: FAILURE
__CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n)) //pointer relation: pointer outside object bounds in sc2: FAILURE
__CPROVER_loop_invariant(sc1 - (const unsigned char*)s1 == sc2 - (const unsigned char*)s2
&& sc1 -(const unsigned char*)s1 == __CPROVER_loop_entry(n) - n)
__CPROVER_decreases(n)
{
res = (*sc1++) - (*sc2++);
if (res != 0)
return res;
}
#endif
return res; |
|
If theses two failures are the only failures, I suppose the reason could be |
|
Full implementation and harness: #ifndef __CPROVER_STRING_H_INCLUDED
#include <string.h>
#define __CPROVER_STRING_H_INCLUDED
#endif
#undef memcmp
inline int memcmp(const char *s1, const char *s2, size_t n)
{
__CPROVER_HIDE:;
int res=0;
#ifdef __CPROVER_STRING_ABSTRACTION
__CPROVER_precondition(__CPROVER_buffer_size(s1)>=n,
"memcmp buffer overflow of 1st argument");
__CPROVER_precondition(__CPROVER_buffer_size(s2)>=n,
"memcmp buffer overflow of 2nd argument");
#else
__CPROVER_precondition(__CPROVER_r_ok(s1, n),
"memcmp region 1 readable");
__CPROVER_precondition(__CPROVER_r_ok(s2, n),
"memcpy region 2 readable");
const char *sc1=s1, *sc2=s2;
for(; n!=0; n--)
__CPROVER_assigns(n, res, sc1, sc2)
__CPROVER_loop_invariant(n >= 0 && n <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
__CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(sc1 - s1 == sc2 - s2 && sc1 - s1 == __CPROVER_loop_entry(n) - n)
__CPROVER_decreases(n)
{
res = (*sc1++) - (*sc2++);
if (res != 0)
return res;
}
#endif
return res;
}
int main() {
unsigned str1_len;
unsigned str2_len;
__CPROVER_assume(str1_len <= str2_len);
unsigned char *str1 = malloc(str1_len);
unsigned char *str2 = malloc(str2_len);
unsigned len;
__CPROVER_assume(len <= str1_len);
__CPROVER_assume(str1 != NULL);
__CPROVER_assume(str2 != NULL);
memset(str1, "a", str1_len);
memset(str2, "a", str2_len);
memcmp(str1, str2, len);
return 0;
} |
|
The issue here is that with will resolve the failures. The failures doesn't appear in the CBMC regression tests because we run CBMC with |
|
Thank you for the insight. To confirm my understanding, is it correct that |
|
The GOTO program after applying loop contracts will look like By default, CBMC will instrument the pointer checks to check if pointers can be out of the bound in pointer arithmetic (plus, minus, comparison between pointers). So after the instrumentation, the GOTO program will be Since the instrumented checks are before the assumption, Using |
I have an issue with the make pipeline for running a single proof: although I've specified
CBMC_OBJECT_BITSin the makefile but it did not get translated into the--object-bitsflag during the pipeline and the checking safety properties step fails due to insufficient object bits. The--unwindflag is also missing when I turn on--dfccand--apply-loop-contract. Is this a bug with the pipeline or am I missing something? The same issue happens at the calculating coverage step. Appreciate any guidance.Makefile for SymCryptMd2, Makefile-project-define
CBMC version: 6.0.1
Running platform: WSL ubuntu
The text was updated successfully, but these errors were encountered: