<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<p lang="en-US">Thanks for your hints, they give me a good overview.</p>
<p lang="en-US">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>
</p>
<p style="margin-bottom: 0in; line-height: 100%" lang="en-US"><br>
</p>
<title></title>
<meta name="generator" content="LibreOffice 4.2.8.2 (Linux)">
<style type="text/css">
<!--
@page { margin: 0.79in }
p { margin-bottom: 0.1in; line-height: 120% }
-->
</style>
<div class="moz-cite-prefix">On 10/04/2016 09:54 AM, Jonas Wagner
wrote:<br>
</div>
<blockquote
cite="mid:CAMRJFf+VmX3h2aKS23wtKb2-dzJT1WN1uKqiFp=p5Ph3HC99jQ@mail.gmail.com"
type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>
<div class="gmail_quote">
<blockquote class="gmail_quote" 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><br>
</div>
<div>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><br>
</div>
<div>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 moz-do-not-send="true"
href="http://clang.llvm.org/docs/AddressSanitizer.html">AddressSanitizer</a>.</div>
<div><br>
</div>
<div>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
moz-do-not-send="true"
href="https://sv-comp.sosy-lab.org/2016/">software
verification competition</a>. Some of the participants
there are open-source and based on LLVM.</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Jonas</div>
<div><br>
</div>
</div>
</div>
</div>
</blockquote>
<br>
</body>
</html>