similar to: [LLVMdev] Publication: Verified LLVM

I am interested in type-based verification of LLVM IR in the areas of certified compilation and software 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. I would like to know if you are aware of any work in this

On Mon, Aug 22, 2011 at 3:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote: > On Mon, Aug 22, 2011 at 11:17 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> On Mon, Aug 22, 2011 at 1:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote: >>> On Mon, Aug 22, 2011 at 9:55 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >>>> In

On Thu, Nov 11, 2010 at 8:28 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Hi all, > > http://www.llvm.org/docs/ProgrammersManual.html#BuildRecType suggests > us to define recursive types via opaque and refine. Since LLVM has > structural types, %rt = type { %rt* } and %rt1 = type { %rt* } should > be same structurally. I tested the following code, > > %rt =

Another quick question. In ./bindings/ocaml/Makefile.ocaml, the configurations when ENABLE_OPTIMIZED<>1 are commented, which set -g flag to $(OCAMLC). Is that for back-compatibility to support OCaml < 3.10.0? On Sun, Feb 28, 2010 at 6:48 PM, Erick Tryzelaar <idadesub at users.sourceforge.net> wrote: > On Sun, Feb 28, 2010 at 8:38 AM, Jianzhou Zhao <jianzhou at

Dear all, I would like to share a paper I co-authored with Prof. Alper Sen. This paper describes an algorithm to generate testbenches from SystemC models represented with LLVM IR. It was accepted and presented at International Conference on Hardware/Software Codesign and System Synthesis (CODES/ISSS), 2012. A link to the paper is accessible from acm or Alper's website:

On Sun, Jul 31, 2011 at 12:49 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > I noticed the patch was already merged into the current LLVM language > reference manual with new memory instructions, fence, cmpxchg and > atomicrmw. Will the instructions be available in LLVM 3.0? Hopefully, yes; the implementation is in progress. -Eli

On Sun, Jul 31, 2011 at 7:12 PM, Eli Friedman <eli.friedman at gmail.com> wrote: > On Sun, Jul 31, 2011 at 12:49 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> I noticed the patch was already merged into the current LLVM language >> reference manual with new memory instructions, fence, cmpxchg and >> atomicrmw. Will the instructions be available in LLVM

On Mon, Aug 22, 2011 at 3:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote: > On Mon, Aug 22, 2011 at 11:17 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> On Mon, Aug 22, 2011 at 1:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote: >>> On Mon, Aug 22, 2011 at 9:55 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >>>> In

Hi, Chapter 4 in http://llvm.org/pubs/2005-05-04-LattnerPHDThesis.html compares the precision of alias analysis in LLVM at that time. Does the latest LLVM still follow the similar results? I was also wondering how the globalmodred-aa and scev-aa that were not discussed in the PhD thesis are compared with others? Thanks and Happy New Year! -- Jianzhou

On Jan 2, 2012, at 9:42 PM, Jianzhou Zhao wrote: > Hi, > > Chapter 4 in http://llvm.org/pubs/2005-05-04-LattnerPHDThesis.html > compares the precision of alias analysis in LLVM at that time. Does > the latest LLVM still follow the similar results? I was also wondering > how the globalmodred-aa and scev-aa that were not discussed in the PhD > thesis are compared with others?

Hello Jianzhou, On Sat, Aug 14, 2010 at 8:25 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Hi, > > Does 2.8 release plan to change anything in Ocaml bindings? > http://llvm.org/docs/ReleaseNotes.html#whatsnew does not list any > relevant features. I usually wait until around nowish before a release to sync llvm-c and the ocaml bindings. I'll start the process.

On Wed, Jan 4, 2012 at 12:10 PM, David Gardner <daveg at xmos.com> wrote: > Jianzhou Zhao <jianzhou <at> seas.upenn.edu> writes: >> The documents say that all the aa analysis are chained, and give an >> example like opt -basicaa -ds-aa -licm. In this case, does ds-aa >> automatically call basicaa for the case when ds-aa can only return >> MayAlias? This

On Tue, Mar 2, 2010 at 3:23 AM, Erick Tryzelaar <idadesub at users.sourceforge.net> wrote: > On Mon, Mar 1, 2010 at 7:34 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> Another quick question. >> In ./bindings/ocaml/Makefile.ocaml, the configurations when >> ENABLE_OPTIMIZED<>1 are commented, which set -g flag to $(OCAMLC). >> Is that for

On Sun, Feb 28, 2010 at 8:38 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Hi, > > At the code below from > ./bindings/ocaml/executionengine/executionengine_ocaml.c, > we create an OCaml Variant from C. It is from 2.6, the latest 2.7 has > the same code. > > Line 240 Option = alloc(1, 1) assigns tag1 to the 'some' constructor. > In term of

On Mon, Mar 1, 2010 at 7:34 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Another quick question. > In ./bindings/ocaml/Makefile.ocaml, the configurations when > ENABLE_OPTIMIZED<>1 are commented, which set -g flag to $(OCAMLC). > Is that for back-compatibility to support OCaml < 3.10.0? At the time, we were still supporting 3.09. It sounds like everyone's

On Wed, Jul 14, 2010 at 6:05 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Some instructions are not implemented in the interpreter. For example, > extractvalue, insertvalue, load/store aggregate pointers, bitcast > between vectors and ints. Is this only the limitation of the current > release? or is there any technical reason that the interpreter has to > omit these

On Fri, Aug 20, 2010 at 6:49 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Hello, > > How does LLVM release deal with users' changings, and consider them as > a patch? But it would be very appreciated if you can review my > bindings to see if they are well-designed. > > Thanks You can just attach it here. In the future you could either file a bug report or

Jianzhou Zhao <jianzhou at seas.upenn.edu> writes: [snip] > The other question is about > target datalayout = > "e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:32:64-v64:64:64-v128:128:128-a0:0:64-f80:32:32" > > If I use this string to creat a TargetData object directly, I got an > assertion error: > >

On Wed, Apr 20, 2011 at 2:54 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: > Hi all, > > I am trying to compile a high-level imperative OOP-like language to > the LLVM IR. Do we have any "generic" way of translating a non-SSA > form to the LLVM IR's SSA? There are lots of LLVM front-ends now. Do > they do such translation individually? or there is some

On Mon, Aug 22, 2011 at 7:35 PM, Jeffrey Yasskin <jyasskin at google.com> wrote: > On Mon, Aug 22, 2011 at 4:20 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> On Mon, Aug 22, 2011 at 6:49 PM, Eli Friedman <eli.friedman at gmail.com> wrote: >>> On Mon, Aug 22, 2011 at 3:40 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >>>> On