search

DonggeLiu / Legion

A coverage-based software testing tool
MIT License
29 stars 4 forks source link

Other baselines #9

Closed DonggeLiu closed 4 years ago

DonggeLiu commented 5 years ago

Try out other baselines, e.g. the ones used in SV-COMP. But not too sure if the results are going to be pretty since we don't know how competitive AMGR is.

DonggeLiu commented 5 years ago

One example is KLEE, which works on my desktop but not on MUPPET:

/usr/bin/llvm-link: /tmp/tmp5ythserf/library.bc:1:1: error: expected top-level entity ELF>8*@@UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H���H�E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H���H�E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H���H�E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H����E�H�E�dH3%(t���UH��H���E��E�H�H�ƿ�H�E�H�E���UH��H��dH�%(H�E�1�H�E���H����E�H�E�dH3%(t���UH��H��dH�%(H�E�1�H�E���H����E������E���t���������E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H���H�E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E��H���H�E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H��dH�%(H�E�1�H�E���H����E�H�M�dH3 %(t���UH��H���}��}�u 0 libLLVM-3.8.so.1 0x00007fa1b8211d38 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56 1 libLLVM-3.8.so.1 0x00007fa1b820ffc6 llvm::sys::RunSignalHandlers() + 54 2 libLLVM-3.8.so.1 0x00007fa1b8210129 3 libc.so.6 0x00007fa1b75624b0 4 libLLVM-3.8.so.1 0x00007fa1b8369804 llvm::Module::materializeMetadata() + 4 5 llvm-link 0x0000000000405399 6 llvm-link 0x0000000000405c6f 7 llvm-link 0x0000000000403c61 8 libc.so.6 0x00007fa1b754d830 __libc_start_main + 240 9 llvm-link 0x0000000000404cd9 Stack dump:

  1. Program arguments: /usr/bin/llvm-link -o /tmp/tmp5ythserf/replace.c.bc /tmp/tmp5ythserf/library.bc /tmp/tmp5ythserf/replace.c.bc /home/donggel/Baselines/klee/bin/../klee_build/bin/klee: /usr/lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.22' not found (required by /home/donggel/Baselines/klee/bin/../libraries/libLLVM-6.0.so.1)
DonggeLiu commented 5 years ago

Now that we have a virtual machine, the new issue with KLEE is:

/usr/bin/llvm-link: /tmp/tmpz34mszii/library.bc:1:1: error: expected top-level entity
ELF>p*@@UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                          %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
 %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                  %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                                                                   %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                          %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                                                           %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                  %(t���UH��H��dH�%(H�E�1�H�E�H�H���H�E�H�M�dH3
                                                                                  %(t���UH��H��dH�%(H�E�1�H�E�H�H���H�E�H�M�dH3
                        %(t���UH��H��dH�%(H�E�1�H�E�H�H���H�E�H�M�dH3
                                                                        %(t���UH��H��dH�%(H�E�1�H�E�H�H����E�H�E�dH3%(t���UH��H���E��E�H�H�ƿ�H�E�H�E���UH��H��dH�%(H�E�1�H�E�H��H����E�H�E�dH3%(t���UH��H��dH�%(H�E�1�H�E�H��H����E������E���t�����������E�H�M�dH3
                                                                  %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
         %(t���UH��H��dH�%(H�E�1�H�E�H�H���H�E�H�M�dH3
                                                         %(t���UH��H��dH�%(H�E�1�H�E�H�H���H�E�H�M�dH3
                                                                                                         %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                %(t���UH��H��dH�%(H�E�1�H�E�H��H����E�H�M�dH3
                                                                                                 %(t���UH��H���}��}�u
/usr/bin/llvm-link: error loading file '/tmp/tmpz34mszii/library.bc'
KLEE: ERROR: error loading program '/tmp/tmpz34mszii/test_while.c.bc': Loading file /tmp/tmpz34mszii/test_while.c.bc Object file as input is currently not supported
DonggeLiu commented 4 years ago

Decided to run other baselines inside the BenchExec framework