goto-instrument --interpreter appears to be broken

[hannes-steffenhagen-diffblue]

CBMC version: 5.10 (cbmc-5.10-970-g7905492ff-dirty) (although I've checked, and this already happened in 4.9)
Operating system: Linux
Exact command line resulting in the issue:

cat <<EOF > test.c
int main(void) { return 0; }
EOF
goto-cc test.c -o test.goto
goto-instrument --interpreter test.goto
r

What behaviour did you expect: Should interpret the program with no error
What happened instead: Hit an invariant in the interpreter

Invariant check failed
File: /home/hannes/Documents/Diffblue/cbmc/src/util/sparse_vector.h:55 function: resize
Condition: new_size>=_size
Reason: sparse vector can't be shrunk (yet)
Backtrace:
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(print_backtrace(std::ostream&)+0x4d) [0x560560f4bce4]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(get_backtrace[abi:cxx11]()+0x45) [0x560560f4beeb]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(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&)+0x4c) [0x56056098ad81]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(std::_Rb_tree_node_base::_S_minimum(std::_Rb_tree_node_base*)+0) [0x560560984be8]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(sparse_vectort<interpretert::memory_cellt>::resize(unsigned long)+0x187) [0x560560cfb111]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(interpretert::build_memory_map()+0x33) [0x560560cf6c15]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(interpretert::initialize(bool)+0x2d) [0x560560cf187f]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(interpretert::command()+0x47d) [0x560560cf2163]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(interpretert::operator()()+0xa7) [0x560560cf1753]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(interpreter(goto_modelt const&, message_handlert&)+0x6d) [0x560560cf8421]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(goto_instrument_parse_optionst::doit()+0x1c7d) [0x56056097e3ab]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(parse_options_baset::main()+0xe8) [0x560560f75f00]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(main+0x55) [0x560560979bef]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f12c07ccb97]
/home/hannes/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument(_start+0x2a) [0x560560979aba]


--- end invariant violation report ---
[1]    9701 abort (core dumped)  ~/Documents/Diffblue/cbmc/cmake-build-debug/bin/goto-instrument --interpreter

[NlightNFotis]

Oh wow, this looks scary 😱

[martin-cs]

I would suggest some unit tests for sparse vector and a review of how the interpreter is using it.

[tautschnig]

Can people with insight into TG maybe comment on this? I thought the interpreter was in use quite a bit.

[xbauch]

If the reason for the invariant is that some elements in the vector may end up out of range then we could simply erase them:

    for (auto it = underlying.begin(); it != underlying.end();)
    {
      if (it->first >= new_size)
        it = underlying.erase(it);
      else
        it++;
    }

We use the sparse vector to simulate a memory map, resizing it to 1 when initializing the interpreter. Erasing the out-of-scope elements shouldn't cause any problem in this case. In the other (two) uses we indeed only resize up and the invariant is valid. Maybe resizing to 1 should be handled as a special case (a different method) in which the whole vector is erased. The resizing could then retain the invariant.

[tautschnig]

This was fixed in #2289.