<div dir="ltr">Hi Monir,<br><br>I'm not entirely familiar with KLEE nor with the dataflow sanitizer, but I think there are two issues with your approach.<br><br>First, I would expect KLEE to require for the whole program to be provided together with its bitcode (modulo known library functions) -- you can see how they achieve that in the tutorials section on their website (e.g., for coreutils [1]). From the high-level point of view, KLEE uses a technique called dynamic symbolic execution (DSE) that when interpreting LLVM bitcode maintains symbolic execution state alongside the (usual) concrete state [2], and while it's possible to use it on binaries, KLEE works on the level of LLVM IR. They have a custom libc implementation that KLEE can reason about (the files with .bca extension on your screenshot). I think that unless you link in whatever binaries you use (such that you end up with a single bitcode file), use on of the provided libraries like libc, KLEE won't be able to come up with a symbolic state for library code.<br><br>The second issue I see is that you want to use the dataflow sanitizer together with KLEE. Typically, the mainstream sanitizers provide cleaver encoding that makes checking some property of interest fast for runtime execution. For example, a sanitizer can maintain a mapping from normal program memory to shadow memory, and instrumentation that maintains this mapping and asserts some invariants over both the memory regions. This encoding/mapping use fast (runtime) operations like shifts, bit operations, hashing, that can be very difficult to reason about for an underlying constraint solver in a DSE tool. Software verification tools usually use custom encodings/instrumentation that is easier to reason about and can use tricks that don't work for runtime verification (e.g., use of nondeterminism in [3]). Things you want to avoid are complicated math function (hashing), large arrays and dependencies across them, etc.<br><br>My suggestion would be to try to first manually instrument your C/C++ source with an encoding friendly for DSE, and once you are happy with it create a custom transformation pass over LLVM IR that emits the instrumentation.<br><br>Best,<br>Jakub<br><br>[1] <a href="http://klee.github.io/tutorials/testing-coreutils/">http://klee.github.io/tutorials/testing-coreutils/</a><br>[2] <a href="https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf</a><br>[3] <a href="http://seahorn.github.io/seahorn/memory%20safety/2017/05/27/seahorn-memory-safety.html">http://seahorn.github.io/seahorn/memory%20safety/2017/05/27/seahorn-memory-safety.html</a></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 5, 2019 at 9:32 PM Hossain,Muhammad Monir via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org">llvm-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">




<div dir="ltr">
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
Dear Developers,<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<br>
</div>
<div style="margin:0px;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<span style="margin:0px;background-color:white">I am a Master's student at the <span style="margin:0px;background-color:white">ECE department of the University of Florida, USA.</span><span style="margin:0px;background-color:white">​</span>​ For my
 research project, supervised by </span><a href="http://tehranipoor.ece.ufl.edu/" rel="noopener noreferrer" title="http://tehranipoor.ece.ufl.edu/" style="margin:0px" target="_blank">Prof. Mark Tehranipoor</a><span style="margin:0px;background-color:white"> </span><span style="margin:0px;background-color:white">and</span><span style="margin:0px;background-color:white"> </span><a href="http://farimah.ece.ufl.edu/" rel="noopener noreferrer" title="http://farimah.ece.ufl.edu/" style="margin:0px" target="_blank">Prof.
 Farimah Farahmandi</a>, <span style="margin:0px;background-color:white"> I need to use Clang LLVM DataflowSanitizer library in KLEE. However, I have faced some difficulties (explained below) while interfacing this library with KLEE and I am seeking your
 help to solve it. </span><br>
<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
For our research purpose, we are using LLVM compiler and LLVM DataFlowSanitizer library. We instrumented a C code using LLVM DataFlowSanitizer library (from <strong>dfsan_interface.h</strong>) along with the insertion of some KLEE assertion (from <strong>klee.h</strong>)
 and converted it to LLVM Bit-code. Then we provided this LLVM Bit-code to KLEE (software verification tool) to run with the archive library of DataFlowSanitizer tool, <strong>libclang_rt.dfsan-x86_64.a</strong>. But, KLEE showed the following error.</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<img size="0" style="max-width: 100%;" src="cid:16bd2465d09b9bdfba41"><br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<span style="font-family:Calibri,Arial,Helvetica,sans-serif;background-color:rgb(255,255,255);display:inline">However, to figure out the problem, I have built a sample custom archive library from the object files generated by Clang/LLVM
 (using cmd </span><b style="font-family:Calibri,Arial,Helvetica,sans-serif">llvm-ar</b><span style="font-family:Calibri,Arial,Helvetica,sans-serif;background-color:rgb(255,255,255);display:inline">) and used this library in a C code
 along with KLEE. In this case, KLEE gave the same error as above. Then I generated the same sample custom archive library from the LLVM bit-code files</span><span style="font-family:Calibri,Arial,Helvetica,sans-serif;background-color:rgb(255,255,255);display:inline"> and
 this time KLEE executed successfully. Hence, I am afraid whether KLEE requires the bit-code version of </span><strong style="font-family:Calibri,Arial,Helvetica,sans-serif">libclang_rt.dfsan-x86_64.a</strong><span style="font-family:Calibri,Arial,Helvetica,sans-serif"> or
 there is any other solution.</span><br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<span style="margin:0px;font-family:Calibri,Arial,Helvetica,sans-serif"><br>
</span></div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
In this circumstance, it would be great if you could direct me to resolve this issue. Please let me know if you need any other information. </div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
Thank you,<br>
</div>
<div style="margin:0px;font-size:12pt;font-family:Calibri,Arial,Helvetica,sans-serif;background-color:white">
Monir</div>
<br>
</div>
</div>

_______________________________________________<br>
LLVM Developers mailing list<br>
<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div>Jakub Kuderski</div></div>