Invariant check failed in `goto-analyzer`

[feliperodri]

CBMC version: develop branch
Operating system: 18.04.1-Ubuntu

First, clone the s2n-tls repository.

$ cd s2n-tls
$ git submodule update --initi --recursive
$ cd tests/cbmc/proofs/s2n_hash_free
$ make goto
$ goto-analyzer gotos/s2n_hash_free_harness.c.goto

What behaviour did you expect: No errors.

What happened instead:

Storage not specified, defaulting to --one-domain-per-history
GOTO-ANALYSER version 5.28.0 (cbmc-5.28.1-14-gafd8a6095) 64-bit x86_64 linux
Reading GOTO program from file
Reading: gotos/s2n_hash_free_harness.c.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
--- begin invariant violation report ---
Invariant check failed
File: goto_inline_class.cpp:459 function: goto_inline
Condition: check_inline_map(inline_map)
Reason: Precondition
Backtrace:
goto-analyzer(+0x4aec4e) [0x55cbaec14c4e]
goto-analyzer(+0x4afbda) [0x55cbaec15bda]
goto-analyzer(+0x3f9ff) [0x55cbae7a59ff]
goto-analyzer(+0x353514) [0x55cbaeab9514]
goto-analyzer(+0x2f2b3d) [0x55cbaea58b3d]
goto-analyzer(+0x2f3360) [0x55cbaea59360]
goto-analyzer(+0x288ca9) [0x55cbae9eeca9]
goto-analyzer(+0x40ec9) [0x55cbae7a6ec9]
goto-analyzer(+0x45207) [0x55cbae7ab207]
goto-analyzer(+0x3da48) [0x55cbae7a3a48]
goto-analyzer(+0x332e4) [0x55cbae7992e4]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7feea193bbf7]
goto-analyzer(+0x3f63a) [0x55cbae7a563a]


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

[martin-cs]

Sorry to hear about this and thanks for the great bug report. That is definitely a bug. Does it affect CBMC as well? Since I harmonised the preprocessing steps between them I would expect it would turn up there too.

Can you try rebuilding with LINKFLAGS=-rdynamic and running to get a more detailed backtrace?

[feliperodri]

AFAIK, it doesn't affect CBMC. I'll post here a more detailed report using LINKFLAGS=-rdynamic.

[martin-cs]

Hmmm... that is interesting. There really should be very little that is different between these two at this stage of processing.

[feliperodri]

@martin-cs is this useful now?

Storage not specified, defaulting to --one-domain-per-history
GOTO-ANALYSER version 5.28.0 (cbmc-5.28.1-14-gafd8a6095) 64-bit x86_64 linux
Reading GOTO program from file
Reading: gotos/s2n_hash_free_harness.c.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
--- begin invariant violation report ---
Invariant check failed
File: goto_inline_class.cpp:459 function: goto_inline
Condition: check_inline_map(inline_map)
Reason: Precondition
Backtrace:
goto-analyzer(print_backtrace(std::ostream&)+0x4e) [0x5622ba2fd2ce]
goto-analyzer(get_backtrace[abi:cxx11]()+0x16a) [0x5622ba2fe25a]
goto-analyzer(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&)+0x4f) [0x5622b9e8e07f]
goto-analyzer(goto_inlinet::goto_inline(std::map<dstringt, std::__cxx11::list<std::pair<std::_List_iterator<goto_programt::instructiont>, bool>, std::allocator<std::pair<std::_List_iterator<goto_programt::instructiont>, bool> > >, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::__cxx11::list<std::pair<std::_List_iterator<goto_programt::instructiont>, bool>, std::allocator<std::pair<std::_List_iterator<goto_programt::instructiont>, bool> > > > > > const&, bool)+0x224) [0x5622ba1a1b94]
goto-analyzer(goto_partial_inline(goto_functionst&, namespacet const&, message_handlert&, unsigned int, bool)+0x5ed) [0x5622ba1411bd]
goto-analyzer(goto_partial_inline(goto_modelt&, message_handlert&, unsigned int, bool)+0x50) [0x5622ba1419e0]
goto-analyzer(process_goto_program(goto_modelt&, optionst const&, messaget&)+0xcd9) [0x5622ba0d7329]
goto-analyzer(goto_analyzer_parse_optionst::process_goto_program(optionst const&)+0x139) [0x5622b9e8f549]
goto-analyzer(goto_analyzer_parse_optionst::doit()+0x647) [0x5622b9e93887]
goto-analyzer(parse_options_baset::main()+0xa8) [0x5622b9e8c0c8]
goto-analyzer(main+0x34) [0x5622b9e81964]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f6ed32a0bf7]
goto-analyzer(_start+0x2a) [0x5622b9e8dcba]


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

[tautschnig]

@martin-cs You've obviously taken care to preserve existing behaviour when cleaning things up - from goto_analyzer_parse_options.cpp:

  // Preserve backwards compatibility in processing
  options.set_option("partial-inline", true);

[TGWDB]

Some notes on where we are (in no special order).

• The partial inlining is included in the code for cbmc and goto-diff but not possible to invoke, so this cannot cause a problem for these executions.
• The commit that introduced the bug is 6fdf17e
• The actual problem is the locations not increasing in the goto model.

Further updates to come.

[TGWDB]

Fix now merged.