VR: use fixed and refactored version

[GiraffeReversed]

Known issues:

• release build has problems, since when building llvm-vr-dump, it is being linked with Release-built libraries dgvra and dgllvmvra, which therefore do not contain necessary dump methods; the build therefore fails (and I am not sure how to fix that)
• the CMakeLists.txt both in dg were changed because the source files were split between .h and .cpp files; the linking during build of llvm-vr-dump has been changed accordingly, but the solution probably has some issues
• the augmentation adds no incorrect answers, as tested on benchmarks from SV-COMP 2020 (the 2021 test in under way)
• the sleep-1 benchmark from busybox has been found faulty by the unaugmented version but timeouts with the new one, nevertheless I was not able to reproduce the success with the unaugmented version after that; when comparing the sliced ll files (i think), I have found no difference

I would prefer to go over the issues in person as to learn more from them :)

Related PR to sbt-instrumentation: https://github.com/staticafi/sbt-instrumentation/pull/65

[lzaoral]

@GiraffeReversed If you haven't looked into the linking issues yet, you can apply this commit https://github.com/lzaoral/dg/commit/971dff3832cc26f1f1d6ff63f73371329da459e0. The macOS and Ubuntu 20.04 jobs now compile successfully but the the value-releations-tests fails as ASAN found some use after free. Just pass -DUSE_SANITIZERS=ON to CMake to check it locally.

EDIT: Of course, if you'd like some explanation what the changes in my patch do, do not hesitate to ask.

[lzaoral]

Please, ignore the broken Ubuntu 16.04 jobs. #404 fixes the issue so don't forget to rebase after it's merged.

[lzaoral]

GitHub's macOS VMs have been just switched to LLVM 13, so that failure should be fixed by #404 as well.

[lzaoral]

@GiraffeReversed #404 has been just merged!

[lzaoral]

Sorry for the CI issues. they are caused by https://github.com/mchalupa/dg/pull/404#issuecomment-944402769. #406 should fix them for real.

[lzaoral]

Hopefully, #411 is the last PR that should fix the issues...

[lzaoral]

@GiraffeReversed Everything that was blocking this PR is merged now so feel free to rebase at your earliest convenience! Note, that there may be some additional build failures due to #408 and #375.

[GiraffeReversed]

I rebased on master here and in staticafi/sbt-instrumentation#65.

[mchalupa]

When I compile instrumentation with sanitizers and run symbiotic on this code:

struct ldv_list_head {
  struct ldv_list_head *next, *prev;
};

 struct ldv_list_head global_list_13 = { &(global_list_13), &(global_list_13) };
 struct A13 {
  int data;
  struct ldv_list_head list;
};
 void main(void) {
    struct A13 *p = (struct A13 *)malloc(sizeof(struct A13));
    global_list_13.next->prev = &p->list;
    p->list.next = global_list_13.next;
    p->list.prev = &global_list_13;
    global_list_13.next = &p->list;

    global_list_13.next = &global_list_13;
    global_list_13.prev = &global_list_13;
}

(with this command)

scripts/symbiotic --sv-comp --prp ../sv-benchmarks/c/properties/valid-memsafety.prp --32 --save-files ml.i

I get this error:

==30985==ERROR: AddressSanitizer: heap-use-after-free on address 0x60f0000a3b48 at pc 0x7fb7a3893ec6 bp 0x7ffc1565f9f0 sp 0x7ffc1565f9e0
READ of size 8 at 0x60f0000a3b48 thread T0
    #0 0x7fb7a3893ec5 in std::vector<llvm::Value const*, std::allocator<llvm::Value const*> >::size() const /usr/include/c++/11.1.0/bits/stl_vector.h:919
    #1 0x7fb7a3838500 in dg::vr::ValueRelations::hasComparativeRelations(dg::vr::EqualityBucket*) const /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:649
    #2 0x7fb7a3838eea in dg::vr::ValueRelations::hasComparativeRelationsOrLoads(dg::vr::EqualityBucket*) const /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:656
    #3 0x7fb7a384e4c5 in dg::vr::ValueRelations::unsetAllLoadsByPtr(llvm::Value const*) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:1410
    #4 0x7fb7a3873667 in dg::vr::RelationsAnalyzer::forgetInvalidated(dg::vr::ValueRelations&, llvm::Instruction const*) const /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:68
    #5 0x7fb7a3873055 in dg::vr::RelationsAnalyzer::processOperation(dg::vr::VRLocation*, dg::vr::VRLocation*, dg::vr::VROp*) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:52
    #6 0x7fb7a388a324 in dg::vr::RelationsAnalyzer::analysisPass() /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1205
    #7 0x7fb7a388abd3 in dg::vr::RelationsAnalyzer::analyze(unsigned int) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1226
    #8 0x7fb7a38124d8 in ValueRelationsPlugin::ValueRelationsPlugin(llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:22
    #9 0x7fb7a38164d6 in create_object /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:190
    #10 0x55955ece3312 in Analyzer::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/src/instr_analyzer.cpp:38
    #11 0x55955ec762a5 in loadPlugins(LLVMInstrumentation&) /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1315
    #12 0x55955ec796ba in main /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1409
    #13 0x7fb7a70b5b24 in __libc_start_main (/usr/lib/libc.so.6+0x27b24)
    #14 0x55955ec5cded in _start (/home/marek/src/symbiotic/sbt-instrumentation/build-10.0.1/src/sbt-instr+0x3c5ded)

0x60f0000a3b48 is located 152 bytes inside of 168-byte region [0x60f0000a3ab0,0x60f0000a3b58)
freed by thread T0 here:
    #0 0x7fb7a8fc8d69 in operator delete(void*, unsigned long) /build/gcc/src/gcc/libsanitizer/asan/asan_new_delete.cpp:172
    #1 0x7fb7a3995fa5 in std::default_delete<dg::vr::EqualityBucket>::operator()(dg::vr::EqualityBucket*) const /usr/include/c++/11.1.0/bits/unique_ptr.h:85
    #2 0x7fb7a39864ea in std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >::~unique_ptr() /usr/include/c++/11.1.0/bits/unique_ptr.h:361
    #3 0x7fb7a39667db in void __gnu_cxx::new_allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > >::destroy<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > >(std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >*) /usr/include/c++/11.1.0/ext/new_allocator.h:162
    #4 0x7fb7a39307ef in void std::allocator_traits<std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > > >::destroy<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > >(std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > >&, std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >*) /usr/include/c++/11.1.0/bits/alloc_traits.h:531
    #5 0x7fb7a38e25c8 in std::vector<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >, std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > > >::_M_erase(__gnu_cxx::__normal_iterator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >*, std::vector<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >, std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > > > >) /usr/include/c++/11.1.0/bits/vector.tcc:177
    #6 0x7fb7a38a102e in std::vector<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >, std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > > >::erase(__gnu_cxx::__normal_iterator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > const*, std::vector<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> >, std::allocator<std::unique_ptr<dg::vr::EqualityBucket, std::default_delete<dg::vr::EqualityBucket> > > > >) /usr/include/c++/11.1.0/bits/stl_vector.h:1431
    #7 0x7fb7a38178b4 in eraseUniquePtr<dg::vr::EqualityBucket> /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:42
    #8 0x7fb7a384e45a in dg::vr::ValueRelations::unsetAllLoadsByPtr(llvm::Value const*) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:1408
    #9 0x7fb7a3873667 in dg::vr::RelationsAnalyzer::forgetInvalidated(dg::vr::ValueRelations&, llvm::Instruction const*) const /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:68
    #10 0x7fb7a3873055 in dg::vr::RelationsAnalyzer::processOperation(dg::vr::VRLocation*, dg::vr::VRLocation*, dg::vr::VROp*) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:52
    #11 0x7fb7a388a324 in dg::vr::RelationsAnalyzer::analysisPass() /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1205
    #12 0x7fb7a388abd3 in dg::vr::RelationsAnalyzer::analyze(unsigned int) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1226
    #13 0x7fb7a38124d8 in ValueRelationsPlugin::ValueRelationsPlugin(llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:22
    #14 0x7fb7a38164d6 in create_object /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:190
    #15 0x55955ece3312 in Analyzer::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/src/instr_analyzer.cpp:38
    #16 0x55955ec762a5 in loadPlugins(LLVMInstrumentation&) /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1315
    #17 0x55955ec796ba in main /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1409
    #18 0x7fb7a70b5b24 in __libc_start_main (/usr/lib/libc.so.6+0x27b24)

previously allocated by thread T0 here:
    #0 0x7fb7a8fc7ca1 in operator new(unsigned long) /build/gcc/src/gcc/libsanitizer/asan/asan_new_delete.cpp:99
    #1 0x7fb7a3847cfa in dg::vr::ValueRelations::ValueRelations(dg::vr::ValueRelations const&) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/ValueRelations.h:1148
    #2 0x7fb7a3872f90 in dg::vr::RelationsAnalyzer::processOperation(dg::vr::VRLocation*, dg::vr::VRLocation*, dg::vr::VROp*) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:47
    #3 0x7fb7a388a324 in dg::vr::RelationsAnalyzer::analysisPass() /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1205
    #4 0x7fb7a388abd3 in dg::vr::RelationsAnalyzer::analyze(unsigned int) /home/marek/src/symbiotic/dg/include/dg/llvm/ValueRelations/RelationsAnalyzer.h:1226
    #5 0x7fb7a38124d8 in ValueRelationsPlugin::ValueRelationsPlugin(llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:22
    #6 0x7fb7a38164d6 in create_object /home/marek/src/symbiotic/sbt-instrumentation/analyses/value_relations_plugin.cpp:190
    #7 0x55955ece3312 in Analyzer::analyze(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, llvm::Module*) /home/marek/src/symbiotic/sbt-instrumentation/src/instr_analyzer.cpp:38
    #8 0x55955ec762a5 in loadPlugins(LLVMInstrumentation&) /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1315
    #9 0x55955ec796ba in main /home/marek/src/symbiotic/sbt-instrumentation/src/instr.cpp:1409
    #10 0x7fb7a70b5b24 in __libc_start_main (/usr/lib/libc.so.6+0x27b24)

SUMMARY: AddressSanitizer: heap-use-after-free /usr/include/c++/11.1.0/bits/stl_vector.h:919 in std::vector<llvm::Value const*, std::allocator<llvm::Value const*> >::size() const
Shadow bytes around the buggy address:
  0x0c1e8000c710: 00 fa fa fa fa fa fa fa fa fa 00 00 00 00 00 00
  0x0c1e8000c720: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 fa
  0x0c1e8000c730: fa fa fa fa fa fa fa fa 00 00 00 00 00 00 00 00
  0x0c1e8000c740: 00 00 00 00 00 00 00 00 00 00 00 00 00 fa fa fa
  0x0c1e8000c750: fa fa fa fa fa fa fd fd fd fd fd fd fd fd fd fd
=>0x0c1e8000c760: fd fd fd fd fd fd fd fd fd[fd]fd fa fa fa fa fa
  0x0c1e8000c770: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c1e8000c780: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c1e8000c790: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c1e8000c7a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c1e8000c7b0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
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
  Shadow gap:              cc
==30985==ABORTING
timeout: the monitored command dumped core

// EDIT: fixed the used program

[GiraffeReversed]

I am having trouble reproducing this problem. When I compile dg configured with USE_SANITIZERS=On and analyze the code with llvm-vr-dump, I get no error.

I suspect there might be something wrong with the build, since when I compile symbiotic on dg with the option set, I get ASan runtime does not come first in initial library list; you should either link runtime to your application or manually preload it with LD_PRELOAD. as part of the error -- nevertheless, I have no clue as to what might be wrong.

EDIT: This is the output of cmake .. -DUSE_SANITIZERS=On, should it be of any help.

-- Build type: Debug
-- Found LLVM 10.0.1
-- Using LLVMConfig.cmake in: /home/anna/formela/symbiotic/llvm-10.0.1/build/lib/cmake/llvm
-- LLVM binaries: /home/anna/formela/symbiotic/llvm-10.0.1/build/./bin
-- Linker detection: unknown
-- LLVM include dir: /home/anna/formela/symbiotic/llvm-10.0.1/include;/home/anna/formela/symbiotic/llvm-10.0.1/build/include
-- LLVM libraries dir: /home/anna/formela/symbiotic/llvm-10.0.1/build/./lib
-- LLVM definitions: -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
-- Looking for headers in given: /home/anna/formela/symbiotic/llvm-10.0.1//include
-- Looking for libraries in given: /home/anna/formela/symbiotic/llvm-10.0.1/build//lib
-- LLVM linking: static
-- Using compiler: /usr/bin/clang++-10
-- Performing Test sanitizers_work
-- Performing Test sanitizers_work - Success
-- Using compilation flags: -g
-- Additional compilation flags:  -std=c++14 -fno-rtti -Wall -Wextra -fno-exceptions -fsanitize=undefined,address -g -fno-omit-frame-pointer -fno-sanitize-recover=all
-- CMAKE_INSTALL_LIBDIR: "lib"
-- CMAKE_INSTALL_INCLUDEDIR: "include"
-- clang: /usr/lib/llvm-10/bin/clang
-- llvm-link: /usr/lib/llvm-10/bin/llvm-link
-- lli: /usr/lib/llvm-10/bin/lli
-- opt: /usr/lib/llvm-10/bin/opt
-- Performing test sanitizers_work with /usr/lib/llvm-10/bin/clang
-- Performing test sanitizers_work with /usr/lib/llvm-10/bin/clang - Success
-- Configuring done
-- Generating done
-- Build files have been written to: /home/anna/formela/symbiotic/dg/build-10.0.1

[lzaoral]

@GiraffeReversed Try this: Compile dg and sbt-instrumentation with GCC and sanitizers and run the script with

$ LD_PRELOAD="$(gcc -print-file-name=libasan.so)" ASAN_OPTIONS=detect_leaks=0 scripts/symbiotic ...

EDIT: you need sbt-instrumentation as well

[GiraffeReversed]

@mchalupa Are you sure you tested the updated version? I renamed the EqualityBucket class as part of the refactoring, yet the error trace mentions it.

[GiraffeReversed]

The fix suggested by @lzaoral did fix the problem (in the sense that the error does no longer show). Nevertheless when I run symbiotic like this, I get INFO: Starting instrumentation followed by INFO: Instrumentation [FAILED] time: 0.00809025764465332, with no indication what the problem is in between.

[mchalupa]

@mchalupa Are you sure you tested the updated version? I renamed the EqualityBucket class as part of the refactoring, yet the error trace mentions it.

I'll re-check. It is possible that I did not recompile everything properly.

[mchalupa]

Ok, I have now tested this PR quite well and I do not have enough strength to go commit-by-commit, so I'll just believe the commits are nice and tidy :) Let's merge this.