GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
637 stars 42 forks source link

handling ostream llvm c++ #286

Open bond15 opened 5 years ago

bond15 commented 5 years ago

note: using llvm 6, Baggage Handler build (http://fryingpan.dev.galois.com/hydra/build/145296)

#include <string>
#include <iostream>
using namespace std;
int main()
{
  string str = "hello";
  cout << str << endl;
  return 0;
}
+FailureWithCounterExample: 262
Undefined behavior encountered: 
Addition of an offset to a pointer resulted in a pointer to an
address outside of the allocation.
Pointer: 0x0:[64]
Offset: 0xffffffffffffffe8:[64]
Reference: 
The C language standard, version C99
§6.5.6 Additive operators, ¶8
Document URL: http://www.iso-9899.info/n1570.html
in _ZNSt3__113basic_ostreamIcNS_11char_traitsIcEEE6sentryC2ERS3_ at :262:9
robdockins commented 5 years ago

Odd that the error message has the line/column number, but not the filename... at any rate, the method name demangles to: std::__1::basic_ostream<char, std::__1::char_traits<char> >::sentry::sentry(std::__1::basic_ostream<char, std::__1::char_traits<char> >&)

The corresponding code seems to come from the ostream header of libcxx, and the corresponding function code is:

template <class _CharT, class _Traits>
basic_ostream<_CharT, _Traits>::sentry::sentry(basic_ostream<_CharT, _Traits>& __os)
    : __ok_(false),
      __os_(__os)
{
    if (__os.good())
    {
        if (__os.tie())
            __os.tie()->flush();
        __ok_ = true;
    }
}

Line 262 is the first if statement. The error message indicates that the pointer value of __os is 0x0 (null). This is probably cout in this situation.

Most likely, there is some initialization magic that libcxx is doing somehow that we need to replicate/implement to get the standard output streams set up correctly.

travitch commented 5 years ago

I was looking at some similar failures recently and was wondering if we call static initializer functions at all. I saw the code for populating global variables in crucible-llvm, but didn't see anything obvious for calling global initializers. I'm a bit afraid to call them, since they might not symbolically terminate, but I believe they are what set up things like cout and cerr

robdockins commented 5 years ago

Indeed, in iostream.cpp the ios_base::Init::Init() constructor does a placed new which initialized cout. Moreover, a top-level declaration of ios_base::Init __start_std_streams; should cause this constructor to run according to what I remember of the C++ object initialization order.

I'm not sure what mechanism clang uses to accomplish this, but we should figure it out and implement the necessary hooks in crux.

robdockins commented 5 years ago

Well, I'd expect them to terminate... they shouldn't really have any access to symbolic data.

travitch commented 5 years ago

We'll have to try it soon then. I'm not so worried about symbolic data as I am about non-obvious loop bounds in locale initialization stuff.

robdockins commented 5 years ago

@siddharthist added some code awhile back to crucible-llvm (https://github.com/GaloisInc/crucible/blob/master/crucible-llvm/src/Lang/Crucible/LLVM/Ctors.hs) to generate code for running global constructors, but it isn't hooked up to anything that I see. I suspect it would be pretty easy to add this to crux.

langston-barrett commented 5 years ago

Yes, I think the reason we decided to put that down at the time was that it some of them were very poorly behaved, and so it wasn't clear that it was always a good idea to call them, even though it's more sound.

What we ended up doing IIRC was just writing a couple no-op overrides for a few of these functions and crossing our fingers, which is admittedly not great: https://github.com/GaloisInc/crucible/blob/master/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs

atomb commented 5 years ago

Regarding your comment at the beginning of this thread, @robdockins, LLVM has changed the way it encodes filenames in metadata over time. I recently made some changes to add support for an additional place to look for filenames (which especially seems to be used in C++?), but I'm not sure it's the only other place. See commit cd5905e2a for where to change it if more changes need to be made.

robdockins commented 5 years ago

I followed this trail down far enough to figure out where it lead. If we run the global_ctor associated with the iostream library, it runs the init code for cout etc, which assumes that stdout, stderr and stdin are already set up. Furthermore, output via cout turns into fwrite calls on stdout, etc.

To make this work, we'll need to implement enough of the C standard file I/O library to at least handle reads and writes to the console.