Invariant check failed: Condition: expr.operands().size() == 3

[ligurio]

CBMC version: 5.95.1 (cbmc-5.95.1)
Operating system: Ubuntu 22.10 amd64
Exact command line resulting in the issue:

goto-cc -I /home/sergeyb/sources/cache/lua -L /home/sergeyb/sources/cache/lua -llua -lm -o lua_close.goto lua_close.c
cbmc lua_close.goto --show-goto-functions --xml-ui > lua_close-property.xml

What behavior did you expect: successfully generated XML report
What happened instead: crash

--- begin invariant violation report ---
Invariant check failed
File: ../src/util/xml.cpp:110 function: escape           
Condition: static_cast<unsigned char>(ch) >= 32u
Reason: XML does not support escaping non-printable character 12
Backtrace:
cbmc(+0xaccd60) [0x566663572d60]
cbmc(+0xacda39) [0x566663573a39]
cbmc(+0x1c46d4) [0x566662c6a6d4]
cbmc(+0xb9cec1) [0x566663642ec1]
cbmc(+0xb9d654) [0x566663643654]
cbmc(+0xb9d564) [0x566663643564]
cbmc(+0xb9d564) [0x566663643564]
cbmc(+0xb9d564) [0x566663643564]
cbmc(+0xb9d564) [0x566663643564]
cbmc(+0xb915d7) [0x5666636375d7]
cbmc(+0x678a76) [0x56666311ea76]
cbmc(+0x678f3e) [0x56666311ef3e]
cbmc(+0x1c7b34) [0x566662c6db34]
cbmc(+0x1cab31) [0x566662c70b31]
cbmc(+0x1c206f) [0x566662c6806f]
cbmc(+0x1aebf9) [0x566662c54bf9]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x75fbffa29d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x75fbffa29e40]
cbmc(+0x1c3a05) [0x566662c69a05]


--- end invariant violation report ---

Source code:

#include <assert.h>

int main()
{
	return 0;
}

Without option --xml-ui:

$ cbmc lua_close.goto --show-goto-functions 
--- begin invariant violation report ---                  
Invariant check failed
File: ../src/util/std_expr.h:77 function: check           
Condition: expr.operands().size() == 3                                   
Reason: ternary expression must have three operands       
Backtrace:                         
cbmc(+0xaccd60) [0x578e84374d60]                                         
cbmc(+0xacda39) [0x578e84375a39]  
cbmc(+0x1c46d4) [0x578e83a6c6d4]                                         
cbmc(+0xab2437) [0x578e8435a437]                                                                                                                   
cbmc(+0x61b447) [0x578e83ec3447]                                         
cbmc(+0x61bcac) [0x578e83ec3cac]
cbmc(+0x678d21) [0x578e83f20d21]    
cbmc(+0x678f3e) [0x578e83f20f3e]                                         
cbmc(+0x1c7b34) [0x578e83a6fb34]    
cbmc(+0x1cab31) [0x578e83a72b31]
cbmc(+0x1c206f) [0x578e83a6a06f]                                         
cbmc(+0x1aebf9) [0x578e83a56bf9]                                                                                                                   
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x73c910829d90]         
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x73c910829e40]                                                                           
cbmc(+0x1c3a05) [0x578e83a6ba05]                                         
                                                                                                                                                   
                                                                         
--- end invariant violation report ---                                                                                                             
Aborted (core dumped)                                                    

GDB backtrace:

(gdb) bt
#0  __pthread_kill_implementation (no_tid=0, signo=6, threadid=140737352652608) at ./nptl/pthread_kill.c:44
#1  __pthread_kill_internal (signo=6, threadid=140737352652608) at ./nptl/pthread_kill.c:78
#2  __GI___pthread_kill (threadid=140737352652608, 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  0x00005555557187ac in std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) ()
#6  0x0000555556006437 in std::_Function_handler<std::ostream& (std::ostream&, exprt const&), format_expr_configt::setup()::{lambda(std::ostream&, exprt const&)#6}>::_M_invoke(std::_Any_data const&, std::ostream&, exprt const&) ()
#7  0x0000555555b6f447 in goto_programt::instructiont::output(std::ostream&) const ()
#8  0x0000555555b6fcac in goto_programt::output(std::ostream&) const ()
#9  0x0000555555bccd21 in show_goto_functions(namespacet const&, ui_message_handlert&, goto_functionst const&, bool) ()
#10 0x0000555555bccf3e in show_goto_functions(goto_modelt const&, ui_message_handlert&, bool) ()
#11 0x000055555571bb34 in cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&) ()
#12 0x000055555571eb31 in cbmc_parse_optionst::doit() ()
#13 0x000055555571606f in parse_options_baset::main() ()
#14 0x0000555555702bf9 in main ()
(gdb) 

[tautschnig]

The first problem (the XML report) is what we already know as #7073. Would you mind sharing the content of lua_close.c, or is that really just the main function that you posted above?

[ligurio]

is that really just the main function that you posted above?

Right.

[kroening]

It's a bummer that XML won't have arbitrary unicode -- I'll vote for doing C-style escaping.

[kroening]

@ligurio Would you consider JSON as a workaround?

[ligurio]

Would you consider JSON as a workaround?

--xml-ui is needed for building an HTML report with cbmc-viewer. It supports JSON as an input format too:

CBMC output:                                                             
  This is the output of CBMC that is summarized by cbmc-viewer. Output can be text, xml, or json, but xml is strongly preferred.                   
                                                                                                                                                   
  --result FILE [FILE ...]                                               
                        CBMC property checking the results. The output of "cbmc".                                                                  
  --coverage FILE [FILE ...]                                                                                                                       
                        CBMC coverage checking results. The output of "cbmc --cover locations".                                                    
  --property FILE [FILE ...]                                             
                        CBMC properties checked during property checking. The output of "cbmc --show-properties".                                  
                            

However, with enabled --show-goto-functions and using JSON output another bug is triggered:

--- begin invariant violation report ---
Invariant check failed
File: ../src/util/std_expr.h:77 function: check
Condition: expr.operands().size() == 3
Reason: ternary expression must have three operands
<snipped>
--- end invariant violation report ---

So removing option --show-goto-functions is a single workaround.

[tautschnig]

Could you please attach /home/sergeyb/sources/cache/lua/liblua.a to this issue? I an unable to reproduce your problem, which is not too surprising given the source code you shared had nothing that could require XML output of non-printable characters. So I suspect it will be part of the lua source code that, I am assuming, you have compiled using goto-cc? Will -lm also resolve to a libm.a that you compiled using goto-cc? If so, we'd need this as well. Thank you!

[ligurio]

@tautschnig, sorry for a broken reproducing steps in description.
See steps below:

$ git clone https://github.com/lua/lua
$ cd lua
$ make CC=goto-cc LD=goto-ld CFLAGS=-DLUA_USE_LINUX
$ cat << EOF > sample.c
> #include <assert.h>

int main()
{
        return 0;
}
> EOF
$ goto-cc -I . -L . -llua -lm -o sample.goto sample.c
$ cbmc sample.goto --show-goto-functions --xml-ui 

<snipped>

--- begin invariant violation report ---
Invariant check failed
File: ../src/util/std_expr.h:77 function: check
Condition: expr.operands().size() == 3
Reason: ternary expression must have three operands
Backtrace:

<snipped>

[tautschnig]

I believe this will be fixed once #7885 is complete: the problem is a bug in format_expr.cpp.