[CN] CVC5 solver crash generated by memcpy spec

[septract]

CN crashes with a parser bug when using CVC5. The bug is triggered by the spec for memcpy used in the OpenSUT proofs. Looks like CVC5 is producing an output that CN can't interpret.

Replication instructions

CN version: git-140db7a8a [2024-12-26 17:38:30 +0000]

CVC version (installed via homebrew on a MB pro M2):

This is cvc5 version 1.2.0 [git tag 1.2.0 branch HEAD]
compiled with GCC version Apple LLVM 16.0.0 (clang-1600.0.26.4)
on Aug  8 2024 16:21:07

Crashing code cvc5-crash.c:

// Adapted from: VERSE-OpenSUT/components/include/cn_memory.h
void _memcpy(unsigned char *dest,
             const unsigned char *src, unsigned long n);
/*@
spec _memcpy(pointer dest, pointer src, u64 n);
requires
    take Src = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
    take Dest = each (u64 i; 0u64 <= i && i < n ) { Block<unsigned char>(array_shift(dest, i)) };
ensures
    take SrcR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
    take DestR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(dest, i)) };
    Src == SrcR;
    each (u64 i; 0u64 <= i && i < n ) { SrcR[i] == DestR[i] };
@*/

void cvc5_crash() 
{
    unsigned char challenge1[16] = "something"; 
    unsigned char challenge2[16] = "something else"; 
    _memcpy(challenge1, challenge2, 16);
}

Crash:

$ cn verify --solver-type=cvc5 cvc5-crash.c
cn: internal error, uncaught exception:
    UnexpectedSolverResponse((error
     "Parse Error: <stdin>:831.32: invalid argument 'default_uf_1' for 'val', expected a value"))
    Raised at Cn__Solver.debug_ack_command in file "backend/cn/lib/solver.ml", line 153, characters 4-42
    Called from Cn__Solver.ack_command in file "backend/cn/lib/solver.ml", line 186, characters 2-25
    Called from Cn__Typing.add_c_internal in file "backend/cn/lib/typing.ml", line 434, characters 11-51
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.sandbox in file "backend/cn/lib/typing.ml", line 86, characters 10-13
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 161, characters 6-442
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 180, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

SMT-lib output generated by cn verify --solver-type=cvc5 cvc5-crash.c --solver-logging=output: cvc5_send_0.txt.

For comparison, the result with Z3 (version Z3 version 4.13.0 - 64 bit).

$ cn verify --solver-type=z3 cvc5-crash.c
[1/1]: cvc5_crash -- pass

Context

• OpenSUT specs for memcpy and other memory operations are here.
• Origin code for the crash is the MKM state machine proof here.

[dc-mak]

I have come across this before and it's a CVC5 limitation, meaning that "cvc5 does currently not support reasoning about constant arrays where the base value is not an actual value. In this case, 'default_uf_1' is a symbol, not a value, hence the error message."

Obviously we can and should consider changing the SMT representation in CN to avoid this. I don't have a good intuition for how difficult this will be, I think not very?

[yav]

I've filed a bug upstream for this:
cvc5/cvc5#11485

I am not sure how to work around this in the meantime, especially since I am not 100% sure on what we assume about default. Specifically, we could translate a constant array where all elements are default as just default, but these are not exactly the same because in the first case all elements of the array are the same, while in the second one they can be different. Perhaps that's OK in the case of default, but I am not sure. Thoughts?