<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=utf-8">

<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>

</head>

<body dir="ltr">

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<span style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">Dear Jakub,<br>

</span><span style="font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255); display: inline !important"></span>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

<br>

</div>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

Thank you very much for your detail explanations and valuable suggestions. I will follow your suggestions.<br>

</div>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

<br>

</div>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

I completely agree with you that KLEE requires libraries with the .bca extension. In fact, I have already tried to generate the archived bit-code version of libclang_rt.dfsan-x86_64.a using WLLVM tool.

 But it could not generate the<span> </span><b>.bca</b><span> </span>file successfully (please, see the attached screenshot).<br>

</div>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

<br>

</div>

<div style="margin: 0px; font-family: Calibri, Arial, Helvetica, sans-serif; background-color: rgb(255, 255, 255)">

Would you please let me know how I can get the archived bit-code version of the LLVM DataFlowSanitizer library? Is there any repository that I may not be aware of? If there is none, could you please guide me on how I can generate it? I really appreciate any

 suggestion you may have. Thank you very much.</div>

<br>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

<br>

</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

Sincerely,</div>

<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">

-Monir</div>

<div id="appendonsend"></div>

<hr style="display:inline-block;width:98%" tabindex="-1">

<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Jakub (Kuba) Kuderski <kubakuderski@gmail.com><br>

<b>Sent:</b> Monday, July 8, 2019 12:22 PM<br>

<b>To:</b> Hossain,Muhammad Monir<br>

<b>Cc:</b> via llvm-dev; Rahman,Fahim; Tehranipoor, Mark; Farahmandi,Farimah<br>

<b>Subject:</b> Re: [llvm-dev] Seeking suggestions about interfacing of LLVM DataFlowSanitizer library with KLEE in C code.</font>

<div> </div>

</div>

<div>

<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="https://urldefense.proofpoint.com/v2/url?u=http-3A__klee.github.io_tutorials_testing-2Dcoreutils_&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=N7mBNCWumzZlQ2m9gF4uiAeH9ueQYRqBFRFR18VN-gU&e=">http://klee.github.io/tutorials/testing-coreutils/</a><br>

[2] <a href="https://urldefense.proofpoint.com/v2/url?u=https-3A__www.doc.ic.ac.uk_-7Ecristic_papers_klee-2Dosdi-2D08.pdf&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=22fD7F1PzwNQrvP15qZYJ-jSgwuzpH33BUShYRMDzyo&e=">https://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf</a><br>

[3] <a href="https://urldefense.proofpoint.com/v2/url?u=http-3A__seahorn.github.io_seahorn_memory-2520safety_2017_05_27_seahorn-2Dmemory-2Dsafety.html&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=vXBYnki_GXpMg2m3AjXhkSYWpqp0qbWQjlssKmtqz-k&e=">http://seahorn.github.io/seahorn/memory%20safety/2017/05/27/seahorn-memory-safety.html</a></div>

<br>

<div class="x_gmail_quote">

<div dir="ltr" class="x_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="x_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 <a href="http://tehranipoor.ece.ufl.edu/" rel="noopener noreferrer" title="http://tehranipoor.ece.ufl.edu/" target="_blank" style="margin:0px">Prof. Mark Tehranipoor</a><span style="margin:0px; background-color:white"> <span style="margin:0px; background-color:white">and<span style="margin:0px; background-color:white"> <a href="http://farimah.ece.ufl.edu/" rel="noopener noreferrer" title="http://farimah.ece.ufl.edu/" target="_blank" style="margin:0px">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%" data-outlook-trace="F:1|T:1" 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://urldefense.proofpoint.com/v2/url?u=https-3A__lists.llvm.org_cgi-2Dbin_mailman_listinfo_llvm-2Ddev&d=DwMFaQ&c=sJ6xIWYx-zLMB3EPkvcnVg&r=lDSmMGOiBAYgoioljve3DA&m=YCp0CzVKUdPTT1gYkqtYENRpDDmo-MoJUGhg9EfiY7Y&s=d5Palxb4z0zzQotZmk3mG7dVPeZUtiEDCvBg_iEpBVE&e=" 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="x_gmail_signature">

<div>Jakub Kuderski</div>

</div>

</div>

</body>

</html>