CBMC 6.0.0-preview fails with mal-formed SMT

[rod-chapman]

CBMC version: 6.0.0-preview (built from source morning of 14th June)
Operating system: macOS
Exact command line resulting in the issue: make -f desktop.mk
What behaviour did you expect: Correct and complete proof
What happened instead:

CBMC returns some sort of error from the SMT prover - see below for details.

Source code: https://github.com/rod-chapman/mlkem-c-aarch64
Branch: poly_compress_contracts

To reproduce:

git clone https://github.com/rod-chapman/mlkem-c-aarch64.git
cd mlkem-c-aarch-64
git checkout poly_compress_contracts
cd cbmc/proofs/poly_compress
make -f desktop.mk

See the desktop.mk file for details of how the tools are being invoked.

This results in many ERROR lines in the output, but critically, an earlier error

Running SMT2 QF_AUFBV using Z3
SMT2 solver returned error message:
	"line 62616 column 354: unknown constant pqcrystals_kyber768_ref_poly_compress::tmp_cc$1!0@4#0"

which I assume is coming back from Z3 ?

[qinheping]

UPDATE:
If there are two expressions
forall x. e1 and forall x. e1 => e2, the first expression will be correctly converted to

(define-fun B1 () Bool (forall x. e1))

But the second expression will be converted to

(define-fun B2 () Bool (=> (and true B1)  e2))

where e2 is no more quantified.
The quantified scope is not correctly handled.

[rod-chapman]

Do you have a simple, reproducible test case? I hope so! Please add and commit that first, so reviewers can see what's going wrong, then see the subsequent commits that correct the behaviour.

[qinheping]

Yes, here is a small test case I reproduced the issue with:

#include <assert.h>
#include <stdbool.h>

#define N 16

void main()
{
  int a[N];
  a[10] = 0;
  bool flag = true;
  for(int j = 0; j < N; ++j)
    __CPROVER_loop_invariant(j <= N)
    {
      for(int i = 0; i < N; ++i)
        __CPROVER_assigns(i, __CPROVER_object_whole(a))
          __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
            int k;
            (0 <= k && k <= N) ==> (k<i ==> a[k] == 1)
          })
        {
          a[i] = 1;
        }
    }
  assert(a[10] == 1);
}

Running

goto-instrument --dfcc main --apply-loop-contracts a.out b.out
cbmc b.out --smt2

will get the error message

SMT2 solver returned error message:
        "line 10912 column 208: unknown constant main::tmp_cc$0!0@2#0"

[qinheping]

In the outfile produced with the --outfile flag, we can see that

(declare-fun B1526 () Bool)
(assert (= B1526 (and (bvsge |main::1::1::1::1::i!0@1#4| (_ bv0 32)) (not (bvsge |main::1::1::1::1::i!0@1#4| (_ bv17 32))) 
  (forall ((|main::tmp_cc$0!0@2#0| (_ BitVec 32))) (or (not (bvsge |main::tmp_cc$0!0@2#0| (_ bv0 32))) (bvsge |main::tmp_cc$0!0@2#0| (_ bv17 32)) (bvsge |main::tmp_cc$0!0@2#0| |main::1::1::1::1::i!0@1#4|) (= (select array.54 ((_ sign_extend 32) |main::tmp_cc$0!0@2#0|)) (_ bv1 32)))))))

...

; convert
; Converting var_no 1592 with expr ID of =>
(define-fun B1592 () Bool (=> (and true B1526 B1527 B1528) 
  (=> |goto_symex::&92;guard#10| 
    (or (not (bvsge |main::1::1::1::1::i!0@2#4| (_ bv0 32))) 
        (bvsge |main::1::1::1::1::i!0@2#4| (_ bv17 32)) 
        (not (bvsge |main::tmp_cc$0!0@2#0| (_ bv0 32))) (bvsge |main::tmp_cc$0!0@2#0| (_ bv17 32)) (bvsge |main::tmp_cc$0!0@2#0| |main::1::1::1::1::i!0@2#4|) (bvsge (bvmul ((_ sign_extend 32) |main::tmp_cc$0!0@2#0|) (_ bv4 64)) (_ bv0 64))))))

The variable main::tmp_cc$0!0@2#0 is correctly quantified in B1592 but not in B1526.

[rod-chapman]

I tried to reproduce that. I just copied the text above into a file called 8329.c, then:

rodchap@f4d4889dcf6d bugs % goto-cc -c -o a.goto 8329.c                                     
rodchap@f4d4889dcf6d bugs % goto-instrument --dfcc main --apply-loop-contracts a.goto b.goto
Reading GOTO program from 'a.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
No decrease clause provided for loop main.0 at file 8329.c line 14 function main. Termination will not be checked.
No assigns clause provided for loop main.1 at file 8329.c line 11 function main. The inferred set {side_effect statement="function_call"(__CPROVER_object_whole, arguments(address_of(main::1::a))), main::1::1::j} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.
No decrease clause provided for loop main.1 at file 8329.c line 11 function main. Termination will not be checked.
file 8329.c line 15 function main: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
file <built-in-additions> line 32: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 2 targets
Removing unused functions
Updating init function
--- begin invariant violation report ---
Invariant check failed
File: /Users/rodchap/Desktop/rod/tools/src/cbmc/src/goto-instrument/nondet_static.cpp:90 function: nondet_static
Condition: fct_entry != goto_model.goto_functions.function_map.end()
Reason: Check return value
Backtrace:
0   goto-instrument                     0x00000001028c4968 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1   goto-instrument                     0x00000001028c4df4 _Z13get_backtracev + 160
2   goto-instrument                     0x00000001023a90c8 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3   goto-instrument                     0x00000001023a9094 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 0
4   goto-instrument                     0x00000001024c6b80 _ZL13nondet_staticRK10namespacetR11goto_modeltRK8dstringt + 1064
5   goto-instrument                     0x00000001024c75a8 _Z13nondet_staticR11goto_modeltRKNSt3__13setINS1_12basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEENS1_4lessIS8_EENS6_IS8_EEEE + 2324
6   goto-instrument                     0x000000010240a228 _ZN5dfcct18reinitialize_modelEv + 180
7   goto-instrument                     0x0000000102407730 _ZN5dfcctC2ERK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalINS8_4pairIS5_S5_EEEEbRKNS8_3mapIS5_S5_NS8_4lessIS5_EENS8_9allocatorINSA_IS6_S5_EEEEEE24dfcc_loop_contract_modetR16message_handlertRKNS8_3setINS8_12basic_stringIcNS8_11char_traitsIcEENSI_IcEEEENSG_ISW_EENSI_ISW_EEEE + 552
8   goto-instrument                     0x0000000102406d70 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalIS4_EEbRKNS7_3setIS4_NS7_4lessIS4_EENS7_9allocatorIS4_EEEEbbRKNSC_INS7_12basic_stringIcNS7_11char_traitsIcEENSF_IcEEEENSD_ISO_EENSF_ISO_EEEER16message_handlert + 384
9   goto-instrument                     0x00000001024953b4 _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 8080
10  goto-instrument                     0x0000000102490b3c _ZN30goto_instrument_parse_optionst4doitEv + 660
11  goto-instrument                     0x00000001028ee6c0 _ZN19parse_options_baset4mainEv + 180
12  goto-instrument                     0x00000001023a8858 main + 40
13  dyld                                0x0000000187a8ff28 start + 2236


--- end invariant violation report ---

I'm running CBMC 6.0.0 on macOS...

[rod-chapman]

Anyway - please add that test case below https://github.com/diffblue/cbmc/tree/develop/regression
somewhere, so the difference in behaviour can be reviewed later as part of this Issue/PR.

[qinheping]

A test added in #8361.

[qinheping]

#8361 resolves this issue of unknown constant. But on your example, I encountered the issue of CBMC not terminating again, which is similar to #8326 and #8301 .

[rod-chapman]

Indeed... with your issue/8329 branch, version 6.0.1 no longer reports an SMT error, but does not terminate on the "poly_compress" function from the mlkem code:

rodchap@f4d4889dcf6d poly_compress % make -f desktop.mk
rm -f *.goto
cbmc --verbosity 6 --object-bits 10 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --smt2 ../../../mlkem/poly_contracts.goto
CBMC version 6.0.1 (cbmc-5.34.0-4388-g73ef5ef424) 64-bit arm64 macos
Reading GOTO program from file ../../../mlkem/poly_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
... and on on...

[rod-chapman]

OK... in my cbmc-examples/arrays/ar.c examples file, the "constant_time_equals_total()" function displays the same behaviour - with both cbmc 6.0.0 and your 6.0.1 branch it never terminates. For example

rodchap@f4d4889dcf6d arrays % make TARGET=constant_time_equals_total
rm -f *.goto
goto-cc --function constant_time_equals_total_harness -DCBMC -o ar.goto ar.c
goto-instrument --dfcc constant_time_equals_total_harness --apply-loop-contracts --enforce-contract constant_time_equals_total --replace-call-with-contract constant_time_equals_strict ar.goto ar_contracts.goto
Reading GOTO program from 'ar.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'constant_time_equals_total_harness'
Wrapping 'constant_time_equals_total' with contract 'constant_time_equals_total' in CHECK mode
Wrapping 'constant_time_equals_strict' with contract 'constant_time_equals_strict' in REPLACE mode
Instrumenting 'ctunpad'
No decrease clause provided for loop ctunpad.0 at file ar.c line 261 function ctunpad. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'arsum_bytes1'
No invariant provided for loop arsum_bytes1.0 at file ar.c line 100 function arsum_bytes1. Using 'true' as a sound default invariant. Please provide an invariant the default is too weak.
No decrease clause provided for loop arsum_bytes1.0 at file ar.c line 100 function arsum_bytes1. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'ctcc_harness'
Instrumenting 'arsum_bytes2_harness'
Instrumenting 'ctunpad_harness'
Instrumenting 'arsum_bytes1_harness'
Instrumenting 'zero_slice'
No decrease clause provided for loop zero_slice.0 at file ar.c line 184 function zero_slice. Termination will not be checked.
file ar.c line 185 function zero_slice: no body for function '__CPROVER_object_upto'
no body for function '__CPROVER_assignable'
Instrumenting 'arsum_bytes2'
No decrease clause provided for loop arsum_bytes2.0 at file ar.c line 118 function arsum_bytes2. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'f2'
Instrumenting 'arsum_blocks1'
No invariant provided for loop arsum_blocks1.0 at file ar.c line 49 function arsum_blocks1. Using 'true' as a sound default invariant. Please provide an invariant the default is too weak.
No decrease clause provided for loop arsum_blocks1.0 at file ar.c line 49 function arsum_blocks1. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'f1'
Instrumenting 'ctcc'
No decrease clause provided for loop ctcc.0 at file ar.c line 237 function ctcc. Termination will not be checked.
file ar.c line 238 function ctcc: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'init_st_harness'
Instrumenting 'f3'
Instrumenting 'zero_slice_harness'
Instrumenting 'arsum_blocks2'
No decrease clause provided for loop arsum_blocks2.0 at file ar.c line 75 function arsum_blocks2. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'constant_time_equals_strict_harness'
Instrumenting 'assign_st1'
Instrumenting 'assign_st2'
No decrease clause provided for loop assign_st2.0 at file ar.c line 150 function assign_st2. Termination will not be checked.
file ar.c line 151 function assign_st2: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'assign_st3'
Instrumenting 'init_st'
No decrease clause provided for loop init_st.0 at file ar.c line 172 function init_st. Termination will not be checked.
file ar.c line 173 function init_st: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'arsum_blocks2_harness'
Instrumenting '__builtin___memcpy_chk'
Instrumenting 'assign_st2_harness'
Instrumenting 'assign_st3_harness'
Instrumenting 'f1_harness'
Instrumenting 'f2_harness'
Instrumenting 'f3_harness'
Instrumenting 'arsum_blocks1_harness'
Instrumenting 'assign_st1_harness'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 3 targets
Removing unused functions
Updating init function
Setting entry point to constant_time_equals_total_harness
Writing GOTO program to 'ar_contracts.goto'
cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --smt2 ar_contracts.goto
CBMC version 6.0.1 (cbmc-5.34.0-4388-g73ef5ef424) 64-bit arm64 macos
Reading GOTO program from file ar_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
file <builtin-library-__builtin___memcpy_chk> line 2:  '__builtin___memcpy_chk'
old definition in module  file <builtin-architecture-strings> line 20
void * (void *__param$0, const void *__param$1, __CPROVER_size_t __param$2, __CPROVER_size_t __param$3, __CPROVER_contracts_write_set_ptr_t __write_set_to_check)
new definition in module <built-in-library> file <builtin-library-__builtin___memcpy_chk> line 2
void * (void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3
Running SMT2 QF_AUFBV using Z3

This needs to be fixed for me to make progress with either s2n-tls or mlkem, but I suggest you use this test case for now as it's easily available on GitHub and the result is reproducible without the use of cbmc-viewer or cbmc-starter-kit.

OK to close this Issue now as long as this gets picked up elsewhere.

[rod-chapman]

I have been trying to reproduce this with CBMC 6.0.0 and also using cbmc built from you branch. In doing that, I simplified the test case a bit to this:

#include <assert.h>
#include <stdbool.h>
#include <stddef.h>

#define N 16

void main()
{
  int a[N];
  a[10] = 0;
  bool flag = true;
  for(size_t j = 0; j < N; ++j)
  __CPROVER_assigns(j, __CPROVER_object_whole(a))
  __CPROVER_loop_invariant(j <= N)
  {
      for(size_t i = 0; i < N; ++i)
      __CPROVER_assigns(i, __CPROVER_object_whole(a))
      __CPROVER_loop_invariant(i <= N)
      __CPROVER_loop_invariant(__CPROVER_forall { int k; k < i ==> a[k] == 1 })
      {
          a[i] = 1;
      }
  }
  assert(a[10] == 1);
}

The main difference is that I use "size_t" for the loop index variables, and I have simplified inner loop invariant to avoid needed TWO ==> operators.

This still crashes CBMC with a similar error:

cbmc --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --verbosity 3 --smt2 8329_contracts.goto
SMT2 solver returned error message:
	"line 11014 column 98: unknown constant main::tmp_cc!0@3#0"

So something still not right.