similar to: [LLVMdev] LLVM is doing something a bit weird in this example (which messes up DSA)

Thanks for your help John... Yup, I looked at Local.cpp even before I fired off my question to the mailing list. Take a peek here at line 464: https://github.com/llvm-mirror/poolalloc/blob/master/lib/DSA/Local.cpp Based on my understanding of this line, if AtomicCmpXchgInst does not return a pointer type, nothing gets merged. And in the example I posted, a pointer value is indeed not returned

Thanks John! You would not believe this :), but literally just 5 minutes ago I saw the TypeSafety pass and it seems to be exactly what we need. So we'll try to leverage that... Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/ On Mon, Dec 15, 2014 at 10:28 AM, John Criswell <jtcriswel at gmail.com> wrote: > On 12/14/14, 4:33 PM, Zvonimir Rakamaric wrote: >>

Hi John, all, Thanks for your responses everybody. This is actually helpful and I think I now better understand what is going on here. Unless there is a pointer involved, DSA will not collapse nodes. That makes sense... What we would like to leverage DSA for is essentially type-unsafe memory accesses, such as the example where code write a byte into the 0th byte of an integer. Another example

Hi, So, SMACK is a software verifier based around LLVM, and you can find more info (PDF, title, abstract) about our recent publication here: http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ I would appreciate if you could add it to your list of LLVM-based publications. Thanks! Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/

Hi, Coming back to this, I would greatly appreciate if someone could add this publication (based on TSan) to the list. Thanks, -- Zvonimir On Tue, Jun 21, 2016 at 12:07 PM Zvonimir Rakamaric <zvonimir at cs.utah.edu> wrote: > Hi, > > We recently published a paper that leverages clang/LLVM (through > ThreadSanitizer) to dynamically detect data races in OpenMP programs: >

Thanks guys! I was looking into ModRef before, but I don't think that's exactly what I need. ModRef API call getModRefInfo requires a Value to be passed to it. However, some memory location M (which is a <DSNode, offset> pair) visible to the caller can be modified in the callee without any Value in the caller actually pointing to that location. I also need to capture those... I

Hi, We recently published another paper that leverages LLVM (through our SMACK software verifier and novel tool called Whoop), and this time we focus on detecting concurrency bugs in device drivers: http://soarlab.org/2015/08/ase2015-ddr/ You can find all the required info (PDF, title, abstract, etc.) at the above webpage. I would appreciate if you could add this paper to your list of

Hi, We just published our work that uses LLVM for software verification: Counterexample-Guided Bit-Precision Selection Shaobo He, Zvonimir Rakamaric Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS), November 2017. Link: http://soarlab.org/2017/09/aplas2017-hr/ I would appreciate if someone could add it to your publication list. Thanks! -- Zvonimir --

Andrew, there used to be some code to compute the ModRef behavior of functions using DS graphs. Does that code still exist in svn? What Zvonimir is asking is essentially that, although perhaps he needs it as DS nodes explicitly rather than via the generic queries in the AliasAnalysis interface. --Vikram http://www.cs.uiuc.edu/~vadve http://llvm.org/ On Apr 3, 2008, at 12:45 PM,

Hi all, I've been using LLVM in my software analysis projects for quite a few years now, and several years back I relied on results of DSA analysis in my SMACK tool for checking C programs. At some point that part of SMACK got deprecated, but now I would like to revisit it since it was working quite well. Therefore, I would like to learn what's the status of the poolalloc project, and

On 12/6/12 4:47 PM, Zvonimir Rakamaric wrote: > Hi all, > > I've been using LLVM in my software analysis projects for quite a few > years now, and several years back I relied on results of DSA analysis > in my SMACK tool for checking C programs. > > At some point that part of SMACK got deprecated, but now I would like > to revisit it since it was working quite well.

In particular, I would for example like to prevent that two fields of type i32 are packed into an i64 parameter. And so on... Thanks! -- Zvonimir

On 11/29/17 7:42 PM, Zvonimir Rakamaric via llvm-dev wrote: > Counterexample-Guided Bit-Precision Selection I've added this publication to the publication list. Please let me know if I need to make any corrections. Regards, John Criswell -- John Criswell Assistant Professor Department of Computer Science, University of Rochester http://www.cs.rochester.edu/u/criswell

On Thu, Apr 3, 2008 at 12:29 PM, Zvonimir Rakamaric <zrakamar at gmail.com> wrote: > Currently I am using DSGraph::computeNodeMapping to do the task, but I > am not sure if that's the way to go.... I believe that is the correct function to use. Andrew

On Thu, Apr 3, 2008 at 4:53 PM, Zvonimir Rakamaric <zrakamar at gmail.com> wrote: > Thanks guys! > > I was looking into ModRef before, but I don't think that's exactly > what I need. ModRef API call getModRefInfo requires a Value to be > passed to it. However, some memory location M (which is a <DSNode, > offset> pair) visible to the caller can be modified

Hi, I am using DSA in the project I am working on. Currently, I am working on automatic inference of function frame conditions to be used in the modular verification tool for C I am developing. Here is a part of my algorithm I am not exactly sure how to do: Let's say function foo calls function bar, and they have corresponding DSGraphs DSG_foo and DSG_bar. Function bar modifies some memory

Thanks Bill! So should I email you again in 5 months? -- http://www.zvonimir.info On Wed, Feb 6, 2013 at 1:10 AM, Bill Wendling <wendling at apple.com> wrote: > Hi Zvonimir, > > We normally list projects that use LLVM when we do a release. The next release will be 3.3, which will probably start up in 5 months or so. > > -bw > > On Feb 3, 2013, at 9:16 PM, Zvonimir

Dear All, We can add a link to the SMACK project on the LLVM User's page at http://llvm.org/Users.html at any time. Bill, does your comment refer to the release notes, or something else? In any event, if the SMACK project has a web site, I can add the URL to the User's page. Is the Github URL what you want to use, or is there a web page with more information that we should link to

On Feb 6, 2013, at 7:22 AM, "Criswell, John T" <criswell at illinois.edu> wrote: > Dear All, > > We can add a link to the SMACK project on the LLVM User's page at http://llvm.org/Users.html at any time. Bill, does your comment refer to the release notes, or something else? > Just to the release notes. At least, that's when we do blurbs. :) -bw > In any

Hi Zvonimir, We normally list projects that use LLVM when we do a release. The next release will be 3.3, which will probably start up in 5 months or so. -bw On Feb 3, 2013, at 9:16 PM, Zvonimir Rakamaric <zvonimir at cs.utah.edu> wrote: > Hi guys, > > So, I've been a long-term user of LLVM, and currently me and my > students are actively using LLVM in several projects of