`--object-bits` and `--unwind` flag missing at checking safety properties and coverage step

[QinyuanWu]

I have an issue with the make pipeline for running a single proof: although I've specified CBMC_OBJECT_BITS in the makefile but it did not get translated into the --object-bits flag during the pipeline and the checking safety properties step fails due to insufficient object bits. The --unwind flag is also missing when I turn on --dfcc and --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.

[14/16] SymCryptMd2: checking safety properties                                                                                                                    FAILED: /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/result.xml /tmp/litani/runs/b68774f7-53d7-40d9-a60e-2ebbde6cc678/status/3bc78467-10f9-4ad0-8fe4-e60b42f060dc.json 

/usr/libexec/litani/litani exec --command 'cbmc  --flush --unwinding-assertions  --bounds-check           --trace --xml-ui /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto' --pipeline-name SymCryptMd2 --ci-stage test --job-id 3bc78467-10f9-4ad0-8fe4-e60b42f060dc --stdout-file /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/result.xml --stderr-file /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/result-err-log.txt --description 'SymCryptMd2: checking safety properties' --timeout 21600 --status-file /tmp/litani/runs/b68774f7-53d7-40d9-a60e-2ebbde6cc678/status/3bc78467-10f9-4ad0-8fe4-e60b42f060dc.json --profile-memory-interval 10 --inputs /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto --outputs /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/result.xml --ignore-returns 10 --tags 'stats-group:safety checks'

[15/16] SymCryptMd2: calculating coverage                                                                                                                                                                                                                                                      FAILED: /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/coverage.xml /tmp/litani/runs/e72e57eb-8aa7-4fbd-af07-2c66148fab37/status/47a40d29-4740-432d-94d1-b134df518d55.json 

/usr/libexec/litani/litani exec --command 'cbmc  --flush  --cover location --xml-ui /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto' --pipeline-name SymCryptMd2 --ci-stage test --job-id 47a40d29-4740-432d-94d1-b134df518d55 --stdout-file /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/coverage.xml --stderr-file /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/coverage-err-log.txt --description 'SymCryptMd2: calculating coverage' --timeout 21600 --status-file /tmp/litani/runs/e72e57eb-8aa7-4fbd-af07-2c66148fab37/status/47a40d29-4740-432d-94d1-b134df518d55.json --profile-memory-interval 10 --inputs /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto --outputs /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/coverage.xml --ignore-returns 10 --tags 'stats-group:coverage computation'

Makefile for SymCryptMd2, Makefile-project-define
CBMC version: 6.0.1
Running platform: WSL ubuntu

[QinyuanWu]

I saw the following comment in the Makefile:

# The default unwind should only be used in DFCC mode without loop contracts.
# When loop contracts are applied, we only unwind specified loops.
# If any loops remain after loop contracts have been applied, CBMC might try
# to unwind the program indefinetly, because we do not pass default unwind
# (i.e., --unwind 1) to CBMC when in DFCC mode.
# We must not use a default unwind command in DFCC mode, because contract instrumentation
# introduces loops encoding write set inclusion checks that must be dynamically unwound during
# symex.
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
  UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
else
  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
  UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
endif
endif

@qinheping since we are using both --dfcc and--apply-loop-contractand we also want to have --unwind 50, is there a way we can resolve this conflict?

[qinheping]

@qinheping since we are using both --dfcc and--apply-loop-contractand we also want to have --unwind 50, is there a way we can resolve this conflict?

Could you try to identify loops beside those in the dfcc built-in function with the CBMC flag --show-loops and set loop bounds for them with CBMC_UNWINDSET.

[tautschnig]

I suspect that your use of ?= in all the variable assignments causes some of the variables to be left empty instead. I suggest that your Makefile use = instead.

[QinyuanWu]

@qinheping currently there's no non-built-in loops left, the only one not related to dfcc is memcpy but I suppose the CBMC version of it one should be unbounded already?

[QinyuanWu]

@tautschnig for the --object-bits I realized Makefile.common by default had commented out CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) so uncomment that line resolved the issue. I also observe that using = instead of ?= in the individual proof Makefile will not be able to overwrite the flag for some reason so ?= is necessary.

@qinheping I ended up modifying the analysis command in Makefile.common to add the --unwind flag and the pipeline was able to generate the report:

# 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
endif

Is 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 --unwind 50 but without it the program will not stop.

[qinheping]

@qinheping currently there's no non-built-in loops left, the only one not related to dfcc is memcpy but I suppose the CBMC version of it one should be unbounded already?

All loops except for memcmp in the image are loops introduced by dfcc loop contracts, so you don't need to set bounds for them. Unlike memcpy and memset, memcmp is not unbounded.

[QinyuanWu]

Is the unbounded version of memcmp something that's in development or is there any issue with applying loop contract to it?

[qinheping]

Is the unbounded version of memcmp something that's in development or is there any issue with applying loop contract to it?

We don't have any plan for unbounded version of memcmp currently. You can stub it out and apply loop contracts in the stubbed version. Here is an example of memcmp annotated with loop contracts for proving memory safety.

[QinyuanWu]

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 __CPROVER_same_object and the last loop invariant before but after adding these the verification passed.
Another thing I find is that __CPROVER_loop_invariant(res == 0) did not change the verification result and since loop invariant is also checked after the last iteration of the loop, would __CPROVER_loop_invariant(res == 0) potentially cause the invariant to not hold if the loop did not immediate return when res != 0? 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?

[qinheping]

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 break or return.

[QinyuanWu]

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:

[memcmp.loop_invariant_step.1] line 108 Check invariant after step for loop memcmp.0: FAILURE
[memcmp.pointer_dereference.41] line 118 dereference failure: pointer outside object bounds in *tmp_post_sc1: FAILURE
[memcmp.pointer_dereference.47] line 118 dereference failure: pointer outside object bounds in *tmp_post_sc2: FAILURE

I also tried to switch the last loop invariant to __CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(sc1) == __CPROVER_POINTER_OFFSET(sc2) && __CPROVER_POINTER_OFFSET(sc2) <= __CPROVER_loop_entry(n)) but it also fails with the same errors. What's the key piece that's missing here? I have a feeling that it has something to do with <= __CPROVER_loop_entry(n) but I can't reason why.

error trace:

Violated property:
  file playground.c function memcmp line 119 thread 0
  dereference failure: pointer outside object bounds in *tmp_post_sc1
  (unsigned __CPROVER_bitvector[65])__CPROVER_OBJECT_SIZE(tmp_post_sc1) >= (unsigned __CPROVER_bitvector[65])__CPROVER_POINTER_OFFSET(tmp_post_sc1) + 1


Violated property:
  file playground.c function memcmp line 119 thread 0
  dereference failure: pointer outside object bounds in *tmp_post_sc2
  (unsigned __CPROVER_bitvector[65])__CPROVER_OBJECT_SIZE(tmp_post_sc2) >= (unsigned __CPROVER_bitvector[65])__CPROVER_POINTER_OFFSET(tmp_post_sc2) + 1


State 773 file playground.c function memcmp line 108 thread 0
----------------------------------------------------
  set=&__write_set_loop_0!0@1 (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 774 file playground.c function memcmp line 108 thread 0
----------------------------------------------------
  ptr=(const void *)&n!0@1 (00010000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 775 file playground.c function memcmp line 108 thread 0
----------------------------------------------------
  size=8ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00001000)

Violated property:
  file playground.c function memcmp line 108 thread 0
  Check invariant after step for loop memcmp.0
  n >= (unsigned long int)0 && n <= tmp_cc$1 && __CPROVER_POINTER_OBJECT((const void *)sc1) == __CPROVER_POINTER_OBJECT((const void *)tmp_cc$2) && __CPROVER_POINTER_OBJECT((const void *)sc2) == __CPROVER_POINTER_OBJECT((const void *)tmp_cc$3) && __CPROVER_POINTER_OFFSET((const void *)sc1) == __CPROVER_POINTER_OFFSET((const void *)sc2) && __CPROVER_POINTER_OFFSET((const void *)sc2) <= tmp_cc$1

[QinyuanWu]

Okey after some brainstorming, I had the following thoughts:
In the case __CPROVER_POINTER_OFFSET(sc2) <= __CPROVER_loop_entry(n), sc2 may havoc to a value of __CPROVER_loop_entry(n) before the execution of the loop, in which after the execution it will become __CPROVER_POINTER_OFFSET(sc2) > __CPROVER_loop_entry(n) due to *sc2++ which fails the invariant. Same case for sc1.
If we then change this invariant clause to __CPROVER_POINTER_OFFSET(sc2) < __CPROVER_loop_entry(n), after the last iteration it should always be the case where __CPROVER_POINTER_OFFSET(sc2) == __CPROVER_loop_entry(n) which fails the invariant.

Could you please confirm if my reasoning is correct?

[qinheping]

Yes, you are correct. If you look at the trace, the last assignment to sc2 in the trace will confirm your thought.

[QinyuanWu]

Great thank you very much!