<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">On 4/3/13 8:21 AM, Marcelo Sousa wrote:<br>
</div>
<blockquote
cite="mid:CACu8kRReqEgmkUectqQEbUrSeXVatHMob=zBwRh-jvVNRorbHg@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html;
charset=ISO-8859-1">
<div dir="ltr">
<div>I am interested in type-based verification of LLVM IR in
the areas of certified compilation and software </div>
</div>
</blockquote>
<br>
Can you explain what you mean by type-based verification? Do you
mean that you want to use a set of typing rules to perform
verification, or do you mean something else?<br>
<br>
<blockquote
cite="mid:CACu8kRReqEgmkUectqQEbUrSeXVatHMob=zBwRh-jvVNRorbHg@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>verification. It seems to me that the LLVM IR type system
is rather informal in the sense that there is no paper with a
proper formalization of the type rules, and for example, a
proof of soundness for well-formedness of the code. <br>
</div>
</div>
</blockquote>
<br>
Another important feature of the LLVM type system is that it is not
a "safe" type system. It is possible to do all sorts of type unsafe
things, such as casting integers to pointers and dereferencing
them. One of the standard LLVM transforms (load widening) will
generate loads that access memory past the end of a memory object.
LLVM IR is capable of representing all the unsafe computations that
C can do.<br>
<br>
<blockquote
cite="mid:CACu8kRReqEgmkUectqQEbUrSeXVatHMob=zBwRh-jvVNRorbHg@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>I would like to know if you are aware of any work in this
direction for LLVM IR so that I can compare with my own
implementation.</div>
</div>
</blockquote>
<br>
The SAFECode/SVA work uses a points-to analysis called DSA which
infers the types of memory objects. A key result of the work is
that the points-to analysis/type inference results of DSA can be
made sound at run-time. The original version of DSA, working on
older versions of LLVM, was able to find a fairly decent number of
type-safe memory objects. The SAFECode/SVA work developed a simple
type checker that verified that the type-inference results returned
by DSA are consistent (i.e., if DSA says that a memory object is
used in a type-safe manner, then it is actually used in a type-safe
manner). There is also some work by Greg Morrisett's group at
Harvard at creating a verified type-checker for the SAFECode/SVA
system. SAFECode/SVA papers can be found at
<a class="moz-txt-link-freetext" href="http://sva.cs.illinois.edu/pubs.html">http://sva.cs.illinois.edu/pubs.html</a>.<br>
<br>
As far as formalisms for the LLVM IR, there is one from University
of Pennsylvania (Santosh Nagarakatte, now at Rutgers, was involved
with that work), the one used by Greg Morrisett's group for the
verified type checker, and there might be one from Grigore Rosu's
group here at the University of Illinois. There is also an LLVM
translation validator from Greg Morrisett's group
(<a class="moz-txt-link-freetext" href="http://llvm-md.org">http://llvm-md.org</a>).<br>
<br>
I think another person wrote asking about translation validation a
few months ago. You might want to search the llvmdev archives for
that conversation.<br>
<br>
<blockquote
cite="mid:CACu8kRReqEgmkUectqQEbUrSeXVatHMob=zBwRh-jvVNRorbHg@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>Moreover, it would be valuable to get some feedback on
suitable type-based analysis that the LLVM community would
like to have in the infrastructure.</div>
</div>
</blockquote>
<br>
LLVM already as a type-based alias analysis (called TBAA) which is
used for optimization. There's a proposal floating around on the
list to improve it; you might want to take a look at that.<br>
<br>
SAFECode can use type-safety to optimize away load/store checks
(provided that it uses garbage collection or automatic pool
allocation to make the optimization sound). Using TBAA instead of
DSA might generate better results. Address Sanitizer (ASan) might
benefit from that optimization as well.<br>
<br>
Automatic pool allocation could also benefit from something like
TBAA.<br>
<br>
I think you'll have to be more specific, though, on what you mean by
type-based analysis and provide details on how it could be applied.<br>
<br>
I apologize if my response is a bit of a ramble; I'm basically
providing a bit of information hoping that some of it is relevant to
what you are asking. I hope you find some of it useful.<br>
<br>
-- John T.<br>
<br>
<blockquote
cite="mid:CACu8kRReqEgmkUectqQEbUrSeXVatHMob=zBwRh-jvVNRorbHg@mail.gmail.com"
type="cite">
<div dir="ltr">
<div><br>
</div>
<div>Regards,</div>
<div>Marcelo</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
LLVM Developers mailing list
<a class="moz-txt-link-abbreviated" href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a> <a class="moz-txt-link-freetext" href="http://llvm.cs.uiuc.edu">http://llvm.cs.uiuc.edu</a>
<a class="moz-txt-link-freetext" href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a>
</pre>
</blockquote>
<br>
</body>
</html>