similar to: [LLVMdev] Linearizability

Hi Andreas, Cloud9 is a project that has an extensive POSIX environment model which also lets you symbolically execute multithreaded programs. It is based on KLEE. http://dslab.epfl.ch/pubs/cloud9.pdf Portend builds on top of Cloud9 to perform race detection/classification: http://dslab.epfl.ch/pubs/portend.pdf Cloud9 code base is also public, it might be of interest to you:

On Fri, Apr 6, 2012 at 7:50 AM, John Criswell <criswell at illinois.edu> wrote: > On 4/6/12 12:50 AM, Kostya Serebryany wrote: > > I'd like some similar work to be done, although I view it a bit > differently. > This might be a separate analysis pass that knows nothing about ASAN or > SAFECode > and appends metadata nodes to memory access instructions saying things

What did you mean by "array access bounds expressions"? If you want to do something along the lines of constraint-based bounds check elimination, you can check out SAFECode. I don't think KLEE would be very useful for proving the safety of memory accesses, rather the lack thereof. Also, KLEE doesn't handle symbolic array sizes. If you can give more details about your project,

On 4/6/12 12:50 AM, Kostya Serebryany wrote: > I'd like some similar work to be done, although I view it a bit > differently. > This might be a separate analysis pass that knows nothing about ASAN > or SAFECode > and appends metadata nodes to memory access instructions saying things > like This is a good idea but is the wrong way to implement the idea. LLVM passes are

I'd like some similar work to be done, although I view it a bit differently. This might be a separate analysis pass that knows nothing about ASAN or SAFECode and appends metadata nodes to memory access instructions saying things like - this access can not go out of buffer bounds - this access can not touch free-ed memory - this access can not participate in a race - this read

This is a proposal to create memory safety instrumentation and optimization passes for LLVM. Abstract: The goal of this project is to modify SAFECode and AddressSanitizer (ASAN) to use a common set of memory safety instrumentation and optimization passes to increase code reuse. These tools and other similar ones use varying methods to detect whether memory accesses are safe, but are fundamentally

Dear Developers, I am a Master's student at the ECE department of the University of Florida, USA.​​ For my research project, supervised by Prof. Mark Tehranipoor<http://tehranipoor.ece.ufl.edu/> and Prof. Farimah Farahmandi<http://farimah.ece.ufl.edu/>, I need to use Clang LLVM DataflowSanitizer library in KLEE. However, I have faced some difficulties (explained below) while

Am 19.04.2011 um 16:44 schrieb John Criswell: > On 4/19/11 5:57 AM, Andreas Wilhelm wrote: >> >> Hello, >> >> I found some code within the pool allocation project to identify parallelizable function calls. >> Unfortunately the functionality isn't part of the current release of poolalloc (in release 14 it was). > > Can you tell me in what file(s) this

Hi, The klee library directory is determined at compile time and cannot be changed afterwards. Have a look at tools/klee/main.cpp to see how it is computed. I usually use Klee without any install step, right from the build directory. This has never given me the error you see. Hope this helps, Jonas On Wed, Jun 5, 2013 at 5:26 PM, Alexandru Ionut Diaconescu < alexandruionutdiaconescu at

Hi all, I'm new to llvm and klee. Now I'm trying to build up coreutil with klee. Following the steps online (http://klee.llvm.org/TestingCoreutils.html), I went to step 3 and stuck. When I try to run: klee --libc=uclibc --posix-runtime ./cat.bc -version Error occurred like: klee: error: Cannot find linker input '/lib/libc.a' klee: ModuleUtil.cpp:42: llvm::Module*

On 04/20/2011 08:05 AM, Andreas Wilhelm wrote: > Am 19.04.2011 um 16:44 schrieb John Criswell: > >> On 4/19/11 5:57 AM, Andreas Wilhelm wrote: >>> Hello, >>> >>> I found some code within the pool allocation project to identify >>> parallelizable function calls. >>> Unfortunately the functionality isn't part of the current release of

Hello everyone, I am a novice with KLEE under LLVM. I am trying to build a KLEE project (on a new LLVM environment) and I have the following problem: echo Testing... Testing... echo There should be no assertion fails! There should be no assertion fails! klee -taint=direct taint_direct.o KLEE: output directory = "klee-out-8" klee: error: Cannot find linker input

Hi, I'm currently trying to find and fix memory leaks (compiling with ``-fsanitize=address``) in the KLEE tool [1] an having found some leaks and I'm having trouble suppressing them. I'm trying to suppress them using the ``-fsanitize-blacklist=blacklist.txt`` option as documented at [2]. I'm using Clang 3.7 ( Arch Linux package 3.7.0-6). The sort of reported leaks I see are ```

On 4/19/11 5:57 AM, Andreas Wilhelm wrote: > Hello, > > I found some code within the pool allocation project to identify > parallelizable function calls. > Unfortunately the functionality isn't part of the current release of > poolalloc (in release 14 it was). Can you tell me in what file(s) this is implemented? I wasn't aware that the poolalloc project had such an

Hi all, Greetings. I'm a Ph.D. student in UIUC. Now I'm working on SAFECode, a research compiler based on LLVM which insert necessary runtime checks to guarantee memory-safety of programs. SAFECode needs to insert checks into the programs (say, please check this load instruction for me). Currently SAFECode inserts these checks as normal call instructions. It would be great that LLVM can

----- Original Message ----- > From: "Tobias Grosser" <tobias at grosser.es> > To: "Nadav Rotem" <nrotem at apple.com> > Cc: "llvmdev at cs.uiuc.edu Dev" <llvmdev at cs.uiuc.edu> > Sent: Monday, February 11, 2013 4:58:50 PM > Subject: Re: [LLVMdev] Parallel Loop Metadata > > On 02/11/2013 10:31 PM, Nadav Rotem wrote: > >

> Excuse me for the diversion but, is that interpreter of LLVM IR available > somewhere? Details on how it works, performance, etc? I'd be interested Yes it is available. The tool (KLEE [1]) is actually a lot more than an interpreter (although it can be used as one). KLEE allows you to mark certain variables (e.g. program inputs) as "symbolic". What this means is that the

Am 22.04.2011 um 18:03 schrieb Tobias Grosser: > On 04/20/2011 08:05 AM, Andreas Wilhelm wrote: >> Am 19.04.2011 um 16:44 schrieb John Criswell: >> >>> On 4/19/11 5:57 AM, Andreas Wilhelm wrote: >>>> Hello, >>>> >>>> I found some code within the pool allocation project to identify >>>> parallelizable function calls.

Hi, I am trying to evaluate how complex would be to modify KLEE ( http://klee.llvm.org/ ) so that it can run LLVM bitcode compiled from Java code obtained with vmjc (from the VMKIT project). Your feedback will be very appreciated. I am familiar with KLEE but I would like to know more about VMKIT, so please point me to the right docs/source code if appropriate. After a quick look over

Are there any "current" Linux distros that have installable packages for llvm, clang, nad klee? I am struggling to get klee built and need a working klee setup asap. Thanks in advance, Donald