Spurious failure with SMT2 backend

[zhassan-aws]

On this program:

#include <stdint.h>
#include <stdlib.h>
#include <string.h>

#define M 4

typedef struct {
  uint8_t val[M];
} s;

size_t nondet_size_t();

int main() {
    size_t n = nondet_size_t();
    __CPROVER_assume(0 < n && n <= 10);

    s *s1 = malloc(n * sizeof(s));
    uint8_t *buf = malloc(n * M);

    size_t i = nondet_size_t();
    if (i < n) {
        s *x = &s1[i];
        memcpy(&buf[0], x->val, M);
    }
}

Verification passes without --smt2 but fails with --smt2:

Without:

$ cbmc test.c
CBMC version 5.81.0 (cbmc-5.81.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00352765s
size of program expression: 127 steps
simple slicing removed 35 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 3.8991e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00141905s
Running propositional reduction
Post-processing
Runtime Post-process: 7.3871e-05s
Solving with MiniSAT 2.2.1 with simplifier
2178 variables, 3603 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.00748485s
Runtime decision procedure: 0.00895971s

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

test.c function main
[main.precondition_instance.1] line 23 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 23 memcpy source region readable: SUCCESS
[main.precondition_instance.3] line 23 memcpy destination region writeable: SUCCESS

** 0 of 5 failed (1 iterations)
VERIFICATION SUCCESSFUL

With:

$ cbmc test.c --smt2
CBMC version 5.81.0 (cbmc-5.81.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00352345s
size of program expression: 127 steps
simple slicing removed 35 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 1.2231e-05s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.000627752s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.031041s
Runtime decision procedure: 0.0317815s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 0.0198296s
Runtime decision procedure: 0.0198902s

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

test.c function main
[main.precondition_instance.1] line 23 memcpy src/dst overlap: SUCCESS
[main.precondition_instance.2] line 23 memcpy source region readable: FAILURE
[main.precondition_instance.3] line 23 memcpy destination region writeable: SUCCESS

** 1 of 5 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 5.81.0 Operating system: Ubuntu 20.04 Exact command line resulting in the issue: cbmc test.c --smt2 What behaviour did you expect: Verification successful What happened instead: Verification failed

[zhassan-aws]

Also running this with the new SMT solver interface results in a crash:

$ cbmc test.c --incremental-smt2-solver 'z3 -smt2 -in'
CBMC version 5.82.0 (cbmc-5.82.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00397233s
size of program expression: 127 steps
simple slicing removed 35 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 1.525e-05s
Passing problem to incremental SMT2 solving via "z3 -smt2 -in"
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2_incremental/convert_expr_to_smt.cpp:114 function: convert_type_to_smt_sort
Condition: false
Reason: Reached unimplemented Generation of SMT formula for type: struct_tag
  * #source_location: 
    * file: test.c
    * line: 7
    * function: 
    * working_directory: /home/ubuntu/examples/smack/serde/serde/orig/serde
  * identifier: tag-#anon#ST[ARR4{U8}'val']
  * #typedef: s
Backtrace:
cbmc(+0xb34870) [0x55aaa020f870]
cbmc(+0xb34e19) [0x55aaa020fe19]
cbmc(+0x1fd5b8) [0x55aa9f8d85b8]
cbmc(+0x933ef0) [0x55aaa000eef0]
cbmc(+0x933dfb) [0x55aaa000edfb]
cbmc(+0x8d4e91) [0x55aa9ffafe91]
cbmc(+0x8d6890) [0x55aa9ffb1890]
cbmc(+0x8d729b) [0x55aa9ffb229b]
cbmc(+0x55c141) [0x55aa9fc37141]
cbmc(+0x5648a6) [0x55aa9fc3f8a6]
cbmc(+0x565452) [0x55aa9fc40452]
cbmc(+0x34e334) [0x55aa9fa29334]
cbmc(+0x34e7b5) [0x55aa9fa297b5]
cbmc(+0x3606f5) [0x55aa9fa3b6f5]
cbmc(+0x207b19) [0x55aa9f8e2b19]
cbmc(+0x203f9e) [0x55aa9f8def9e]
cbmc(+0x1fb64f) [0x55aa9f8d664f]
cbmc(+0x1e7219) [0x55aa9f8c2219]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f89736f6083]
cbmc(+0x1fcfce) [0x55aa9f8d7fce]

--- end invariant violation report ---
Aborted (core dumped)

[thomasspriggs]

This should be retested on the old SMT back end. I would still expect support for this example to be unimplemented on the new backend. I am going to unassign myself, as I am not actively working on this retesting right now.