<div dir="ltr">Hi,<div><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div bgcolor="#FFFFFF" text="#000000" class="gmail_msg"><p lang="en-US" class="gmail_msg">I am not trying to achieve complete memory safety. I
wrote a pass that does some safety checks for every store
instruction. Now I want to optimize my pass by avoiding to
instrument
checks for store instructions that are somehow provable "memory
safe".
So, I am only looking for some easy and obvious cases where I can
optimize for performance.<br class="gmail_msg"></p></div></blockquote><div><br></div><div>The first thing I'd do is compile with -O3 before you run your pass. In this case, SROA will already take care of many of the easy cases, and convert the loads/stores into registers.</div><div><br></div><div>That said, SoftBound uses similar optimizations. See for example the code here: <a href="https://github.com/santoshn/softboundcets-3.8.0/blob/master/llvm-38/lib/Transforms/Instrumentation/SoftBoundCETS.cpp#L3244">https://github.com/santoshn/softboundcets-3.8.0/blob/master/llvm-38/lib/Transforms/Instrumentation/SoftBoundCETS.cpp#L3244</a></div><div><br></div><div>Another thing: in most cases the optimizations will not matter. In a typical program, there are only very few checks that cause most of the overhead. It's the checks that are in hot loops. Incidentally, those are loop-dependent, and thus hard to prove safe. You might be better off using a <a href="http://dslab.epfl.ch/proj/asap/">tool such as ASAP</a> that automatically recognizes and removes such checks.</div><div><br></div><div>Full disclaimer: I'm one of the authors of ASAP. If you want to try it out, I'm happy to help make it work for your use-case.</div><div><br></div><div>Best,</div><div>Jonas</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div bgcolor="#FFFFFF" text="#000000" class="gmail_msg"><p lang="en-US" class="gmail_msg">
</p></div><div bgcolor="#FFFFFF" text="#000000" class="gmail_msg">
<p style="margin-bottom:0in;line-height:100%" lang="en-US" class="gmail_msg"><br class="gmail_msg">
</p>
<div class="m_-3725457841275202486moz-cite-prefix gmail_msg">On 10/04/2016 09:54 AM, Jonas Wagner
wrote:<br class="gmail_msg">
</div>
<blockquote type="cite" class="gmail_msg">
<div dir="ltr" class="gmail_msg">Hi,
<div class="gmail_msg"><br class="gmail_msg">
</div>
<div class="gmail_msg">
<div class="gmail_quote gmail_msg">
<blockquote class="gmail_quote gmail_msg" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">My
current approach would be to declare every pointer as
unsafe that is computed somewhere by a GEP instruction
with non constant indices, as well as constant indices
that can be proven to be out of<br class="gmail_msg">
bounds (but that would be more a thing for the compiler to
complain).<br class="gmail_msg">
</blockquote>
<div class="gmail_msg"><br class="gmail_msg">
</div>
<div class="gmail_msg">Are you assuming that you see the entire program
(something like using LTO)? Otherwise one of the main
difficulties will be that the provenance of pointers are
unknown. For example, you might see a function that
receives a pointer argument, and have no idea where that
function is called from. Or some code might use a global,
and you don't know what the value of the global is. Or a
pointer is read from memory, and you don't know which
instruction modified it.</div>
<div class="gmail_msg"><br class="gmail_msg">
</div>
<div class="gmail_msg">There is definitely a lot of work already in this area.
For large real-world software, I believe the idea of
proving memory safety is not feasible yet; for those
people tend to use dynamic (run-time) checks instead,
e.g., <a href="http://clang.llvm.org/docs/AddressSanitizer.html" class="gmail_msg" target="_blank">AddressSanitizer</a>.</div>
<div class="gmail_msg"><br class="gmail_msg">
</div>
<div class="gmail_msg">For statically proving accesses, there are ideas such
as abstract interpretation, model checking, CEGAR,
separation logic... I think a good place to get an
overview of current tools is the <a href="https://sv-comp.sosy-lab.org/2016/" class="gmail_msg" target="_blank">software
verification competition</a>. Some of the participants
there are open-source and based on LLVM.</div>
<div class="gmail_msg"><br class="gmail_msg">
</div>
<div class="gmail_msg">Cheers,</div>
<div class="gmail_msg">Jonas</div>
<div class="gmail_msg"><br class="gmail_msg">
</div>
</div>
</div>
</div>
</blockquote>
<br class="gmail_msg">
</div></blockquote></div></div>