Regression test failure: `goto-analyzer` fails with a segmentation fault in MacOS in `std::sort` of `std::vector<constant_interval_exprt>`

[NlightNFotis]

We (@NlightNFotis and @esteffin) recently found out that there's an issue with the regression tests on MacOS machines (we are running Apple Silicon machines, with latest osX Sonoma).

The following two tests are failing:

• regression/goto-analyzer/loop-termination-eq/test-value-sets.desc
• regression/goto-analyzer/loop-termination-ne/test-value-sets.desc

Zooming in on one of them (loop-termination-eq) and trying to inspect what went wrong, we get the following output on the command line:

$ goto-analyzer --variable-sensitivity --vsd-values set-of-constants --show main.c
GOTO-ANALYZER version 5.93.0 (cbmc-5.93.0-47-g0838c70e55) 64-bit arm64 macos
Parsing main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Selecting abstract domain
Computing abstract states
[2]    46413 segmentation fault  /Users/esteffin/git/cbmc/build-ninja/bin/goto-analyzer --variable-sensitivity

This is not terribly useful, so the next step is to run the command within the context of a debugger, which produces the same output but clarifies that the exact exception being thrown is of type EA_BAD_ACCESS, and that the exact location at the time of the crash is at src/analyses/variable-sensitivity/value_set_abstract_object.cpp:520, which looks like this:

void collapse_overlapping_intervals(
  std::vector<constant_interval_exprt> &intervals)
{
  std::sort(
    intervals.begin(),
    intervals.end(),
    [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
      if(is_eq(lhs.get_lower(), rhs.get_lower()))
        return is_le(lhs.get_upper(), rhs.get_upper());
      return is_le(lhs.get_lower(), rhs.get_lower());
    });

[...]

Trying to work out what's going wrong by reading the code did point to potential errors across either the standard library implementation of std::sort, std::vector or our irep implementation and its sharing strategy, but didn't clarify the nature of the error beyond mere suspicions.

Our next bit of investigation led us to deploy the address sanitiser on the the binary, by building with clang supplied with an extra flag to it (the flag is -fsanitize=address, which we passed to clang through cmake) yielded a bit more fruit, in terms of the following output (minified a bit for increased legibility):

$ goto-analyzer --variable-sensitivity --vsd-values set-of-constants --show main.c
GOTO-ANALYZER version 5.93.0 (cbmc-5.93.0-47-g0838c70e55) 64-bit arm64 macos
Parsing main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Selecting abstract domain
Computing abstract states
=================================================================
==47565==ERROR: AddressSanitizer: container-overflow on address 0x000108b05630 at pc 0x0001022a0f50 bp 0x00016dc75ef0 sp 0x00016dc75ee8
READ of size 8 at 0x000108b05630 thread T0
    #0 0x1022a0f4c in sharing_treet<irept, forward_list_as_mapt<dstringt, irept>>::read() const irep.h:250
    #1 0x1022a0ef4 in irept::get_sub() const irep.h:457
    #2 0x1022a0ea4 in exprt::operands() const expr.h:98
    #3 0x10230425c in exprt::op0() const expr.h:138
    #4 0x103423034 in constant_interval_exprt::get_lower() const interval.cpp:29
    #5 0x10305f6e4 in collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8::operator()(constant_interval_exprt const&, constant_interval_exprt const&) const value_set_abstract_object.cpp:527
    #6 0x10305ebf4 in void std::__1::__introsort<std::__1::_ClassicAlgPolicy, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8&, constant_interval_exprt*>(constant_interval_exprt*, constant_interval_exprt*, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8&, std::__1::iterator_traits<constant_interval_exprt*>::difference_type) sort.h:549
    #7 0x10305d5bc in void std::__1::__sort<collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8&, constant_interval_exprt*>(constant_interval_exprt*, constant_interval_exprt*, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8&) sort.h:627
    #8 0x10305d234 in void std::__1::__sort_impl[abi:v15007]<std::__1::_ClassicAlgPolicy, std::__1::__wrap_iter<constant_interval_exprt*>, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8>(std::__1::__wrap_iter<constant_interval_exprt*>, std::__1::__wrap_iter<constant_interval_exprt*>, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8&) sort.h:687
    #9 0x10305c338 in void std::__1::sort[abi:v15007]<std::__1::__wrap_iter<constant_interval_exprt*>, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8>(std::__1::__wrap_iter<constant_interval_exprt*>, std::__1::__wrap_iter<constant_interval_exprt*>, collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&)::$_8) sort.h:694
    #10 0x10305b4dc in collapse_overlapping_intervals(std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>&) value_set_abstract_object.cpp:523
    #11 0x10305a734 in collect_intervals(abstract_object_sett const&) value_set_abstract_object.cpp:515
    #12 0x103032634 in non_destructive_compact(abstract_object_sett const&) value_set_abstract_object.cpp:555
    #13 0x10302b470 in compact_values(abstract_object_sett const&) value_set_abstract_object.cpp:484
    #14 0x10302a9c0 in value_set_abstract_objectt::make_value_set(abstract_object_sett const&) value_set_abstract_object.cpp:158
    #15 0x102f2f59c in value_set_evaluator::transform() const abstract_value_object.cpp:579
    #16 0x102f2ed48 in value_set_evaluator::operator()() const abstract_value_object.cpp:566
    #17 0x102f2e714 in value_set_expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) abstract_value_object.cpp:694
    #18 0x102f2d798 in transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) abstract_value_object.cpp:167
    #19 0x102f2d740 in abstract_value_objectt::expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) const abstract_value_object.cpp:179
    #20 0x102f7607c in context_abstract_objectt::expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) const context_abstract_object.cpp:103
    #21 0x102e88144 in abstract_environmentt::eval_expression(exprt const&, namespacet const&) const abstract_environment.cpp:475
    #22 0x102e7c1e8 in abstract_environmentt::eval(exprt const&, namespacet const&) const abstract_environment.cpp:131
    #23 0x1030c70cc in variable_sensitivity_domaint::transform(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, dstringt const&, std::__1::shared_ptr<ai_history_baset const>, ai_baset&, namespacet const&) variable_sensitivity_domain.cpp:65
    #24 0x102cd8b98 in ai_baset::visit_edge(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, dstringt const&, std::__1::__list_const_iterator<goto_programt::instructiont, void*>, std::__1::shared_ptr<ai_history_baset const>, namespacet const&, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&) ai.cpp:368
    #25 0x102cd6824 in ai_baset::visit(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:314
    #26 0x102cd4a60 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, dstringt const&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:248
    #27 0x102cdc0bc in ai_recursive_interproceduralt::visit_edge_function_call(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::__list_const_iterator<goto_programt::instructiont, void*>, dstringt const&, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:576
    #28 0x102cdab8c in ai_baset::visit_function_call(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:483
    #29 0x102cd60e0 in ai_baset::visit(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:293
    #30 0x102cd4a60 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, dstringt const&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:248
    #31 0x102cd5220 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, goto_functionst const&, namespacet const&) ai.cpp:264
    #32 0x10221fbbc in ai_baset::operator()(abstract_goto_modelt const&) ai.h:173
    #33 0x10221da90 in goto_analyzer_parse_optionst::perform_analysis(optionst const&) goto_analyzer_parse_options.cpp:596
    #34 0x10221b2d8 in goto_analyzer_parse_optionst::doit() goto_analyzer_parse_options.cpp:425
    #35 0x103515c18 in parse_options_baset::main() parse_options.cpp:97
    #36 0x1021849a8 in main goto_analyzer_main.cpp:28
    #37 0x18bfbd054  (<unknown module>)
    #38 0x7109fffffffffffc  (<unknown module>)
0x000108b05630 is located 112 bytes inside of 128-byte region [0x000108b055c0,0x000108b05640)
allocated by thread T0 here:
    #0 0x105dce6ac in wrap__Znwm+0x68 (libclang_rt.asan_osx_dynamic.dylib:arm64+0x4e6ac) (BuildId: 7e0582579c4b3c3d83923244415f64e732000000200000000100000000000b00)
    #1 0x102193658 in void* std::__1::__libcpp_operator_new[abi:v15007]<unsigned long>(unsigned long) new:246
    #2 0x102193614 in std::__1::__libcpp_allocate[abi:v15007](unsigned long, unsigned long) new:272
    #3 0x102f462dc in std::__1::allocator<constant_interval_exprt>::allocate[abi:v15007](unsigned long) allocator.h:112
    #4 0x102f46020 in std::__1::__allocation_result<std::__1::allocator_traits<std::__1::allocator<constant_interval_exprt>>::pointer> std::__1::__allocate_at_least[abi:v15007]<std::__1::allocator<constant_interval_exprt>>(std::__1::allocator<constant_interval_exprt>&, unsigned long) allocate_at_least.h:54
    #5 0x102f45bb8 in std::__1::__split_buffer<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>&>::__split_buffer(unsigned long, unsigned long, std::__1::allocator<constant_interval_exprt>&) __split_buffer:316
    #6 0x102f45050 in std::__1::__split_buffer<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>&>::__split_buffer(unsigned long, unsigned long, std::__1::allocator<constant_interval_exprt>&) __split_buffer:312
    #7 0x10305be70 in void std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>::__push_back_slow_path<constant_interval_exprt const&>(constant_interval_exprt const&) vector:1569
    #8 0x10305b20c in std::__1::vector<constant_interval_exprt, std::__1::allocator<constant_interval_exprt>>::push_back[abi:v15007](constant_interval_exprt const&) vector:1587
    #9 0x10305a658 in collect_intervals(abstract_object_sett const&) value_set_abstract_object.cpp:512
    #10 0x103032634 in non_destructive_compact(abstract_object_sett const&) value_set_abstract_object.cpp:555
    #11 0x10302b470 in compact_values(abstract_object_sett const&) value_set_abstract_object.cpp:484
    #12 0x10302a9c0 in value_set_abstract_objectt::make_value_set(abstract_object_sett const&) value_set_abstract_object.cpp:158
    #13 0x102f2f59c in value_set_evaluator::transform() const abstract_value_object.cpp:579
    #14 0x102f2ed48 in value_set_evaluator::operator()() const abstract_value_object.cpp:566
    #15 0x102f2e714 in value_set_expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) abstract_value_object.cpp:694
    #16 0x102f2d798 in transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) abstract_value_object.cpp:167
    #17 0x102f2d740 in abstract_value_objectt::expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) const abstract_value_object.cpp:179
    #18 0x102f7607c in context_abstract_objectt::expression_transform(exprt const&, std::__1::vector<std::__1::shared_ptr<abstract_objectt const>, std::__1::allocator<std::__1::shared_ptr<abstract_objectt const>>> const&, abstract_environmentt const&, namespacet const&) const context_abstract_object.cpp:103
    #19 0x102e88144 in abstract_environmentt::eval_expression(exprt const&, namespacet const&) const abstract_environment.cpp:475
    #20 0x102e7c1e8 in abstract_environmentt::eval(exprt const&, namespacet const&) const abstract_environment.cpp:131
    #21 0x1030c70cc in variable_sensitivity_domaint::transform(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, dstringt const&, std::__1::shared_ptr<ai_history_baset const>, ai_baset&, namespacet const&) variable_sensitivity_domain.cpp:65
    #22 0x102cd8b98 in ai_baset::visit_edge(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, dstringt const&, std::__1::__list_const_iterator<goto_programt::instructiont, void*>, std::__1::shared_ptr<ai_history_baset const>, namespacet const&, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&) ai.cpp:368
    #23 0x102cd6824 in ai_baset::visit(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:314
    #24 0x102cd4a60 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, dstringt const&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:248
    #25 0x102cdc0bc in ai_recursive_interproceduralt::visit_edge_function_call(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::__list_const_iterator<goto_programt::instructiont, void*>, dstringt const&, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:576
    #26 0x102cdab8c in ai_baset::visit_function_call(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:483
    #27 0x102cd60e0 in ai_baset::visit(dstringt const&, std::__1::shared_ptr<ai_history_baset const>, std::__1::set<std::__1::shared_ptr<ai_history_baset const>, ai_history_baset::compare_historyt, std::__1::allocator<std::__1::shared_ptr<ai_history_baset const>>>&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:293
    #28 0x102cd4a60 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, dstringt const&, goto_programt const&, goto_functionst const&, namespacet const&) ai.cpp:248
    #29 0x102cd5220 in ai_baset::fixedpoint(std::__1::shared_ptr<ai_history_baset const>, goto_functionst const&, namespacet const&) ai.cpp:264
HINT: if you don't care about these errors you may set ASAN_OPTIONS=detect_container_overflow=0.
If you suspect a false positive see also: https://github.com/google/sanitizers/wiki/AddressSanitizerContainerOverflow.
SUMMARY: AddressSanitizer: container-overflow irep.h:250 in sharing_treet<irept, forward_list_as_mapt<dstringt, irept>>::read() const
Shadow bytes around the buggy address:
  0x007021180a70: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x007021180a80: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x007021180a90: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x007021180aa0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x007021180ab0: fa fa fa fa fa fa fa fa 00 00 00 00 00 00 00 00
=>0x007021180ac0: 00 00 00 00 00 00[fc]fc fa fa fa fa fa fa fa fa
  0x007021180ad0: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x007021180ae0: fa fa fa fa fa fa fa fa fd fd fd fd fd fd fd fd
  0x007021180af0: fd fd fd fd fd fd fd fd fa fa fa fa fa fa fa fa
  0x007021180b00: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x007021180b10: fa fa fa fa fa fa fa fa fd fd fd fd fd fd fd fd
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
==47565==ABORTING

The exact error message produced is hinting at a memory management issue within the aforementioned components (or at least, that's what we gathered from the container-overflow error and the documentation at 1 and 2).

This investigation didn't introduce more clarity, so next up we tried to reshape the data in the crashing program into a minimal reproducing unit test, which did manage to trigger the issue with:

/*******************************************************************\

Module: Unit tests for interval_constraint in
        util/interval_constraint.cpp

Author: Diffblue Ltd.

\*******************************************************************/

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/interval.h>
#include <util/interval_constraint.h>

#include <testing-utils/use_catch.h>

#include <functional>

static bool is_eq(const exprt &lhs, const exprt &rhs)
{
  return constant_interval_exprt::equal(lhs, rhs);
}

static bool is_le(const exprt &lhs, const exprt &rhs)
{
  return constant_interval_exprt::less_than_or_equal(lhs, rhs);
}

template <typename T>
bool check_sorted(
  const std::vector<T> &intervals,
  const std::function<bool(const T &, const T &)> &comp)
{
  if(intervals.size())
  {
    return true;
  }

  auto wrap_iter = intervals.begin();

  for(++wrap_iter; wrap_iter != intervals.end(); ++wrap_iter)
  {
    if(!comp(*(wrap_iter - 1), *wrap_iter))
      return false;
  }
  return true;
}

TEST_CASE(
  "std::sort",
  "[core][analysis][variable-sensitivity][value_set_abstract_object][std::"
  "sort]")
{
  std::vector<constant_interval_exprt> intervals;
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0xC, signedbv_typet{32}),
    from_integer(0x10, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0x13, signedbv_typet{32}),
    from_integer(0x17, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0x9, signedbv_typet{32}),
    from_integer(0xD, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0x18, signedbv_typet{32}),
    from_integer(0x20, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0xD, signedbv_typet{32}),
    from_integer(0x11, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0xA, signedbv_typet{32}),
    from_integer(0xE, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0x14, signedbv_typet{32}),
    from_integer(0x18, signedbv_typet{32})});
  intervals.emplace_back(constant_interval_exprt{
    from_integer(0x17, signedbv_typet{32}),
    from_integer(0x1B, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0x15, signedbv_typet{32}),
  //    from_integer(0x19, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0x3, signedbv_typet{32}),
  //    from_integer(0x7, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0xB, signedbv_typet{32}),
  //    from_integer(0xF, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0xE, signedbv_typet{32}),
  //    from_integer(0x16, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0x16, signedbv_typet{32}),
  //    from_integer(0x1A, signedbv_typet{32})});
  //  intervals.emplace_back(constant_interval_exprt{
  //    from_integer(0x4, signedbv_typet{32}),
  //    from_integer(0xC, signedbv_typet{32})});

  const std::function<bool(
    const constant_interval_exprt &, const constant_interval_exprt &)>
    comparison =
      [](const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
  {
    if(is_eq(lhs.get_lower(), rhs.get_lower()))
      return is_le(lhs.get_upper(), rhs.get_upper());
    return is_le(lhs.get_lower(), rhs.get_lower());
  };

  std::sort(intervals.begin(), intervals.end(), comparison);

  REQUIRE(check_sorted(intervals, comparison));
}

This also results to the segmentation fault we were observing with the regression test, so it acts as a reproducer but in the form of a unit-test instead of a regression-test.

---

CBMC version: 5.93.0 and older at least until 5.75.0, but probably predates them all
Operating system: MacOS 14 Sonoma on Apple Silicon architecture
Exact command line resulting in the issue: goto-analyzer --variable-sensitivity --vsd-values set-of-constants --show main.c - but if the unit-test supplied is used, just building with cmake and running the unit-test binary is enough to observe the failure.
What behaviour did you expect: A run of goto-analyser that proceeds without an issue
What happened instead: A SEGMENTATION FAULT

[esteffin]

Replacing constant_interval_exprt with a minus_exprt and changing the comparison function to be:

      [](const minus_exprt &lhs, const minus_exprt &rhs)
  {
    if(is_eq(lhs.lhs(), rhs.lhs()))
      return is_le(lhs.rhs(), rhs.rhs());
    return is_le(lhs.lhs(), rhs.lhs());
  }

in the unit test also causes SEGMENTATION FAULT, so it is possible it is coming from binary_exprt?

Using constant_exprt instead seem to pass with no issue.

[tautschnig]

I was able to reproduce the problem on Ubuntu 20.04 when using libc++ instead of libstdc++ with clang 7 as well as clang 10. Debugging a bit more it is the case that the iterator used within the library runs beyond bounds. The bug, however, is still ours: It seems that LLVM's libc++ just relies a bit more on the requirements that the comparison function must satisfy: it has to be a strict weak ordering, meaning we need to use constant_interval_exprt::less_than instead of constant_interval_exprt::less_than_or_equal. With that change the test appears to run just fine. Will issue a PR.

[tautschnig]

@NlightNFotis Thank you for the excellent unit test!

[NlightNFotis]

@tautschnig Thanks for fighting this menace and coming out victorious. Was the stuff of nightmares for us.

The unit test was crafted by Enrico in particular, so kudos for that should go to him :)