search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
847 stars 262 forks source link

Invariant violation on 5.23.0 #5811

Closed danielsn closed 3 years ago

danielsn commented 3 years ago

CBMC version: 5.23.0 Operating system: Exact command line resulting in the issue: What behaviour did you expect: What happened instead:

You can see the logs at this link https://ds4auz7vny70f.cloudfront.net/c1881680-283a-42a3-a3a1-1ba9c7d074ff/pipelines/aws_byte_buf_write_be16/index.html

On this proof aws_byte_buf_write_be16 from aws-c-common, with this commandline

cbmc --unwind 1 --unwindset memcpy_impl.0:11 --flush --object-bits 8 --pointer-primitive-check --external-sat-solver run_sat_solver.py --malloc-may-fail --malloc-fail-null --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace /codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/proofs/aws_byte_buf_write_be16/gotos//codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/proofs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c.goto

we got stdout: 

END TIME: 2021-02-10T13:04:14Z

COMMAND SUCCESSFUL: NO

stdout:

CBMC version 5.23.0 (cbmc-5.23.0) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/proofs/aws_byte_buf_write_be16/gotos//codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/proofs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c.goto
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 (user-specified)
Starting Bounded Model Checking
Unwinding loop memcpy_impl.0 iteration 1 file /codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/stubs/memcpy_override.c line 31 function memcpy_impl thread 0
Unwinding loop memcpy_impl.0 iteration 2 file /codebuild/output/src027378174/src/e98b1671-cd48-43ae-bb52-5a4b10764ccf/verification/cbmc/stubs/memcpy_override.c line 31 function memcpy_impl thread 0
Runtime Symex: 0.401534s
size of program expression: 897 steps
simple slicing removed 8 assignments
Generated 1276 VCC(s), 213 remaining after simplification
Runtime Postprocess Equation: 0.000164867s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0184793s
Running propositional reduction
Post-processing

and stderr

stderr:

--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv_typecast.cpp:504 function: type_conversion
Condition: src_width == dest_width
Reason: source bitvector width shall equal the destination bitvector width
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x3a) [0xa7e96a]
cbmc(get_backtrace[abi:cxx11]()+0x20) [0xa7eef0]
cbmc(_Z29invariant_violated_structuredI17invariant_failedtJRKNSt7__cxx1112basic_stringIcSt11char_traitsIcESaIcEEEEENSt9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES8_S8_iS8_DpOT0_+0x2d) [0x510b1d]
cbmc() [0x510ae6]
cbmc(boolbvt::type_conversion(typet const&, std::vector<literalt, std::allocator<literalt> > const&, typet const&, std::vector<literalt, std::allocator<literalt> >&)+0xde0) [0x8bddf0]
cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0x7a) [0x8bcf8a]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x312) [0x88f3a2]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x4eb) [0x8ce05b]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x85) [0x88eb55]
cbmc(boolbvt::convert_extractbits(extractbits_exprt const&)+0x65) [0x8a61f5]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x564) [0x88f5f4]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x4eb) [0x8ce05b]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x85) [0x88eb55]
cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0x36) [0x8bcf46]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x312) [0x88f3a2]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x4eb) [0x8ce05b]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x85) [0x88eb55]
cbmc(boolbvt::convert_bv_typecast(typecast_exprt const&)+0x36) [0x8bcf46]
cbmc(boolbvt::convert_bitvector(exprt const&)+0x312) [0x88f3a2]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0x4eb) [0x8ce05b]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x85) [0x88eb55]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0x113) [0x8a46e3]
cbmc(bv_pointerst::convert_rest(exprt const&)+0x3d1) [0x8c94c1]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0xdfd) [0x91066d]
cbmc(prop_conv_solvert::convert(exprt const&)+0x73) [0x90f7e3]
cbmc(arrayst::add_array_constraints_with(std::set<exprt, std::less<exprt>, std::allocator<exprt> > const&, with_exprt const&)+0x231) [0x888751]
cbmc(arrayst::add_array_constraints()+0x30a) [0x88613a]
cbmc(boolbvt::post_process()+0x2d) [0x89468d]
cbmc(bv_pointerst::post_process()+0xd) [0x8d156d]
cbmc(prop_conv_solvert::dec_solve()+0x5d) [0x9127bd]
cbmc(run_property_decider(incremental_goto_checkert::resultt&, std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, goto_symex_property_decidert&, ui_message_handlert&, std::chrono::duration<double, std::ratio<1l, 1l> >, bool)+0x181) [0x528c31]
cbmc(multi_path_symex_checkert::operator()(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x149) [0x52fb79]
cbmc(all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()()+0x30) [0x51fb00]
cbmc(cbmc_parse_optionst::doit()+0x11c9) [0x516619]
cbmc(parse_options_baset::main()+0x7f) [0xa96c2f]
cbmc(main+0x22) [0x510302]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7ffa835460b3]
cbmc(_start+0x2e) [0x51021e]

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

aws_byte_buf_write_be16: calculating coverage
tautschnig commented 3 years ago

To me, this looks like a duplicate of https://github.com/diffblue/cbmc/issues/5797?

hannes-steffenhagen-diffblue commented 3 years ago

@danielsn This is indeed probably a duplicate of #5797. It'd be helpful if you could check if this can still be reproduced with a recent from-source build (it should be fixed, this looks exactly the same as the error I saw), if the fix does work for you we can create an "emergency" release so you don't have to wait until next thursday.

hannes-steffenhagen-diffblue commented 3 years ago

Duplicate of #5797

Let me know if you think this is in error.