search

diffblue / cbmc

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

Invariant check failed: src/util/lower_byte_operators.cpp:73 function: adjust_width #8475

Open ligurio opened 2 months ago

ligurio commented 2 months ago

CBMC version: 6.3.1 (cbmc-6.3.1-6-gbcda5a9316) and 5.95.1 Operating system: Ubuntu 22.04 amd64 Exact command line resulting in the issue: cbmc --bounds-check --memory-leak-check --memory-cleanup-check --pointer-check --signed-overflow-check --unsigned-overflow-check --nan-check --float-overflow-check --object-bits 16 --unwind 5 --no-library proofs/heap_iterator.proof What behaviour did you expect: analysis finished successfully What happened instead: Invariant check failed: src/util/lower_byte_operators.cpp:73 function: adjust_width

CBMC version 6.3.1 (cbmc-6.3.1-6-gbcda5a9316) 64-bit x86_64 linux                     
Reading GOTO program from file proofs/heap_iterator.proof                  
Generating GOTO Program                                                               
Adding CPROVER library (x86_64)                                                       
Removal of function pointers and virtual functions                                    
Generic Property Instrumentation                                                      
Starting Bounded Model Checking                                                       
Passing problem to propositional reduction                                            
converting SSA                                                                        
--- begin invariant violation report ---                                              
Invariant check failed                                                                
File: /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:73 function: adjust_width                                                                           
Condition: false                                                                      
Reason: Precondition                       
Backtrace:

Backtrace (cbmc-6.3.1-6-gbcda5a9316):

#0  __pthread_kill_implementation (no_tid=0, signo=6, threadid=140737352644416) at ./nptl/pthread_kill.c:44
#1  __pthread_kill_internal (signo=6, threadid=140737352644416) at ./nptl/pthread_kill.c:78
#2  __GI___pthread_kill (threadid=140737352644416, signo=signo@entry=6) at ./nptl/pthread_kill.c:89
#3  0x00007ffff7842476 in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#4  0x00007ffff78287f3 in __GI_abort () at ./stdlib/abort.c:79
#5  0x000055555559c9e4 in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (
    file="/home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp", function="adjust_width", line=73, condition="false")
    at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:260
#6  0x000055555559be86 in invariant_violated_string (file="/home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp", function="adjust_width", line=73, 
    condition="false", reason="Precondition") at /home/sergeyb/sources/cache/cbmc/src/util/invariant.h:282
#7  0x000055555601c1af in adjust_width (src=..., new_width=64) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:73
#8  0x0000555556029051 in lower_byte_extract (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:1467
#9  0x000055555603753a in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2660
#10 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#11 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#12 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#13 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#14 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#15 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#16 0x00005555560373d4 in lower_byte_operators (src=..., ns=...) at /home/sergeyb/sources/cache/cbmc/src/util/lower_byte_operators.cpp:2647
#17 0x0000555555cfb5eb in boolbvt::convert_equality (this=0x5555568fd340, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv_equality.cpp:32
#18 0x0000555555ce2947 in boolbvt::convert_rest (this=0x5555568fd340, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:339
#19 0x0000555555d385e4 in bv_pointerst::convert_rest (this=0x5555568fd340, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/bv_pointers.cpp:224
#20 0x0000555555d77f80 in prop_conv_solvert::convert_bool (this=0x5555568fd340, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/prop/prop_conv_solver.cpp:310
#21 0x0000555555d76a8a in prop_conv_solvert::convert (this=0x5555568fd340, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/prop/prop_conv_solver.cpp:175
#22 0x0000555555d78d7c in prop_conv_solvert::add_constraints_to_prop (this=0x5555568fd340, expr=..., value=true)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/prop/prop_conv_solver.cpp:428
#23 0x0000555555d798b4 in prop_conv_solvert::set_to (this=0x5555568fd340, expr=..., value=true)
    at /home/sergeyb/sources/cache/cbmc/src/solvers/prop/prop_conv_solver.cpp:527
#24 0x0000555555ce4abf in boolbvt::set_to (this=0x5555568fd340, expr=..., value=true) at /home/sergeyb/sources/cache/cbmc/src/solvers/flattening/boolbv.cpp:528
#25 0x0000555555ccbe86 in decision_proceduret::set_to_true (this=0x5555568fd348, expr=...) at /home/sergeyb/sources/cache/cbmc/src/solvers/decision_procedure.cpp:33
#26 0x0000555555a0c562 in symex_target_equationt::convert_assignments (this=0x5555568fc400, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:374
#27 0x0000555555a0c24e in symex_target_equationt::convert_without_assertions (this=0x5555568fc400, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:338
#28 0x0000555555a0c33c in symex_target_equationt::convert (this=0x5555568fc400, decision_procedure=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-symex/symex_target_equation.cpp:351
#29 0x00005555557955b3 in convert_symex_target_equation (equation=..., decision_procedure=..., message_handler=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/bmc_util.cpp:158
#30 0x0000555555796ae3 in prepare_property_decider (properties=std::map with 342 elements = {...}, equation=..., property_decider=..., ui_message_handler=...)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/bmc_util.cpp:372
#31 0x00005555557aad61 in multi_path_symex_checkert::prepare_property_decider (this=0x5555568fc170, properties=std::map with 342 elements = {...})
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_checker.cpp:82
#32 0x00005555557aac16 in multi_path_symex_checkert::operator() (this=0x5555568fc170, properties=std::map with 342 elements = {...})
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/multi_path_symex_checker.cpp:69
#33 0x00005555555bcb19 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator() (this=0x5555568fbf80)
    at /home/sergeyb/sources/cache/cbmc/src/goto-checker/all_properties_verifier_with_trace_storage.h:45
#34 0x00005555555a7013 in cbmc_parse_optionst::doit (this=0x7fffffffd430) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_parse_options.cpp:776
#35 0x00005555560507e8 in parse_options_baset::main (this=0x7fffffffd430) at /home/sergeyb/sources/cache/cbmc/src/util/parse_options.cpp:97
#36 0x000055555559bb62 in main (argc=15, argv=0x7fffffffd8b8) at /home/sergeyb/sources/cache/cbmc/src/cbmc/cbmc_main.cpp:48
tautschnig commented 2 months ago

Would you be able to share the input that leads to this problem?

ligurio commented 2 months ago

How-to reproduce: