[Caml-list] Developper position: designing a C front-end in OCaml

[Caml-list] Developper position: designing a C front-end in OCaml

[Xavier Rival]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 3348 bytes --]


We are looking for an experienced OCaml developper in order to design 
front-end components for a static analyzer developped as part of the 
MemCAD ERC project (http://www.di.ens.fr/~rival/memcad.html). The position 
is offered at INRIA Paris Rocquencourt center, in the Abstraction Research 
Team (located in Ecole Normale Supérieure, Paris, 5th Arrondissement). It 
will be funded on the MemCAD project, for a one or two years duration (if 
the candidate opts for a one year contact, an extension to two years will 
be possible). Hiring could be done as soon as December 2013 (later 
starting dates are feasible).

The task that will be undertaken consists in developping front-end 
components for the MemCAD static analyzer, including a C front-end, syntax 
tree simplification, and possibly pre-analyses to be used in the MemCAD 
tool (the goal of this tool is to infer program invariants for codes 
manipulating complex memory data-structures). The components that shall be 
designed as part of this effort have the potential to be used by other 
research groups in the static analysis area.

The candidate should be familiar with functional programming (expertise in 
OCaml is very appreciated) and should preferably have some knowledge in 
compilation (lexers, parsers, representation and transformation of 
abstract syntax trees). The ability to design interfaces with external 
libraries in C/C++ will also be useful. No knowledge in static analysis is 
required. This position requires a Master Degree (or equivalent).

For additional details, please contact Xavier Rival (rival@di.ens.fr).

---------------------------------------------------------------------------

Nous recherchons un expert en programmation OCaml pour concevoir et 
implémenter des composants d'un front-end d'analyseur statique, au sein du 
projet ERC MemCAD (http://www.di.ens.fr/~rival/memcad.html). Le poste sera 
rattaché au Centre de Recherche INRIA Paris Rocquencourt et sera situé à 
l'Ecole Normale Supérieure (Paris, 5ème Arrondissement). Il sera financé 
sur le projet MemCAD, pour une durée de un ou deux ans (dans le cas d'un 
contrat initial pour un an, une extension à deux ans sera possible). Le 
contrat pourra commencer à partir de Décembre 2013 (une date d'embauche 
ultérieure pourra aussi être fixée).

La tâche consistera en la réalisation d'un front-end pour l'analyseur 
statique MemCAD incluant un front-end C, des phases de simplifications 
syntaxiques et éventuellement des pré-analyses qui pourront être utilisées 
dans l'analyseur MemCAD (le but de cet analyseur est d'inférer des 
invariants de programmes pour des logiciels manipulant des structures de 
données complexes). Ces composants pourront également être utilisés 
ultérieurement dans d'autres équipes en analyse statique.

Une solide connaissance de la programmation fonctionnelle est attendue 
(est une expertise en OCaml sera très appréciée), ainsi que, de 
préférence, de bonnes connaissances en compilation (lexeurs, parseurs, 
représentations et transformations d'arbres syntaxiques abstraits). Une 
expérience en mise au point d'interfaces entre code OCaml et code C/C++ 
sera également utile. Aucune connaissance en analyse statique n'est 
exigée. Un niveau Master ou équivalent est attendu.

Pour plus de détails, veuillez contacter Xavier Rival (rival@di.ens.fr).

Re: [Caml-list] Developper position: designing a C front-end in OCaml

[Gabriel Kerneis]

On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote:
> The task that will be undertaken consists in developping front-end
> components for the MemCAD static analyzer, including a C front-end,
> syntax tree simplification, and possibly pre-analyses to be used in
> the MemCAD tool (the goal of this tool is to infer program
> invariants for codes manipulating complex memory data-structures).
> The components that shall be designed as part of this effort have
> the potential to be used by other research groups in the static
> analysis area.

Out of curiosity, why don't CIL or Frama-C suit your needs?

Best regards,
-- 
Gabriel

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Xavier Rival]

On Tue, 15 Oct 2013, Gabriel Kerneis wrote:

> On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote:
>> The task that will be undertaken consists in developping front-end
>> components for the MemCAD static analyzer, including a C front-end,
>> syntax tree simplification, and possibly pre-analyses to be used in
>> the MemCAD tool (the goal of this tool is to infer program
>> invariants for codes manipulating complex memory data-structures).
>> The components that shall be designed as part of this effort have
>> the potential to be used by other research groups in the static
>> analysis area.
>
> Out of curiosity, why don't CIL or Frama-C suit your needs?

I have used CIL in another project in the past. My experience is that it 
is a great front-end for program transformation. It is less adapted to 
static analysis though, as it does a lot of syntactic transformations, 
causing part of the structure of the code to be lost. For instance, it 
transforms loops into a while(1) form, with break statements. This design 
choice does not help static analyzers, and may require recalculating 
information that was lost in the early phases.

Best Regards,

Xavier.

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Julia Lawall]

On Tue, 15 Oct 2013, Xavier Rival wrote:

> On Tue, 15 Oct 2013, Gabriel Kerneis wrote:
>
> > On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote:
> > > The task that will be undertaken consists in developping front-end
> > > components for the MemCAD static analyzer, including a C front-end,
> > > syntax tree simplification, and possibly pre-analyses to be used in
> > > the MemCAD tool (the goal of this tool is to infer program
> > > invariants for codes manipulating complex memory data-structures).
> > > The components that shall be designed as part of this effort have
> > > the potential to be used by other research groups in the static
> > > analysis area.
> >
> > Out of curiosity, why don't CIL or Frama-C suit your needs?
>
> I have used CIL in another project in the past. My experience is that it is a
> great front-end for program transformation. It is less adapted to static
> analysis though, as it does a lot of syntactic transformations, causing part
> of the structure of the code to be lost. For instance, it transforms loops
> into a while(1) form, with break statements. This design choice does not help
> static analyzers, and may require recalculating information that was lost in
> the early phases.

I would have thought that all of those would be the same things that make
it not good for program transformation.  At least not if you want to look
at the transformed code.  It could be OK for something like weaving
aspects, where you just want to execute the code, and want to advise the
parts that are not broken by the simplifications.

I have the impression that Frama-C does similar reorganizations.

julia

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[David MENTRE]

Hello,

2013/10/15 Xavier Rival <Xavier.Rival@ens.fr>:
> I have used CIL in another project in the past. My experience is that it is
> a great front-end for program transformation. It is less adapted to static
> analysis though, as it does a lot of syntactic transformations, causing part
> of the structure of the code to be lost. For instance, it transforms loops
> into a while(1) form, with break statements. This design choice does not
> help static analyzers, and may require recalculating information that was
> lost in the early phases.

In that case, why don't you extend CIL to fix its deficiencies? It
would help other projects using CIL like Frama-C.

In the same way, why do you implement your own C parsing
infrastructure and do not build a Frama-C plug-in for your analysis?
Frama-C has already a user base (industrial and academic), if you can
improve it it would help a lot. And it would allow to combine your
analysis with other Frama-C plug-ins.

Last but not least, you say "We plan to release source code of the
analyzer along the course of the project." Which kind of licence do
you plan to use?[1]

Sincerely yours,
david

[1] I am maintaining this directory:
    http://gulliver.eu.org/free_software_for_formal_verification

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Gabriel Kerneis]

On Tue, Oct 15, 2013 at 03:02:23PM +0200, David MENTRE wrote:
> In that case, why don't you extend CIL to fix its deficiencies? It

We are talking about changing the AST used to manipulate the programs.
Changing it (in either CIL or Frama-C) would mean breaking every
existing code around the world based on it.  While it might be
acceptable in some cases, it is definitely a major change, with the risk
of alienating the user base.  And if breaking changes are required
anyway, restarting from scratch might be cleaner.

> would help other projects using CIL like Frama-C.

It would not help Frama-C, because they forked CIL and changed it too
deeply to port anything but trivial patches between them.

> In the same way, why do you implement your own C parsing
> infrastructure and do not build a Frama-C plug-in for your analysis?

Frama-C uses (almost) the same AST as CIL, with the same simplifying
assumptions that make CIL unsuitable for Xavier.

> [1] I am maintaining this directory:
>     http://gulliver.eu.org/free_software_for_formal_verification

Thanks for the link.  You should update the entry about CIL:
http://gulliver.eu.org/program_dev_check_environments#cil
to the new URL:
http://cil.sourceforge.net/

Best regards,
-- 
Gabriel Kerneis (CIL maintainer)

Re: [Caml-list] Developper position: designing a C front-end in OCaml

[Basile Starynkevitch]

On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote:
> 
> We are looking for an experienced OCaml developper in order to
> design front-end components for a static analyzer developped as part
> of the MemCAD ERC project (http://www.di.ens.fr/~rival/memcad.html).


If you want to develop in Ocaml CIL is definitely a possible way to go 
(and you could also code a Frama-C plugin, hence taking advantage of 
existing Frama-C infrastructure). If it does not fit all of 
your needs, please contribute your enhancements to it.

Alternatively, Did you consider working inside GCC, perhaps thru a plugin, 
perhaps using MELT, a domain specific language to extend GCC, see http://gcc-melt.org/ ?
you could take advantage of existing GCC infrastructure, in particular
add some analysis pass after some existing GCC optimizing passes which 
would have already done some transformations (And MELT is not Ocaml, 
but a Lisp-like language, notably enabling you to code in a 
functional style - more than if you did your GCC extension in C++03).

At last you could work with CompCert http://compcert.inria.fr/ 
which can be viewed as a C compiler coded in Ocaml (although it is much more 
than that).

Regards.
-- 
Basile STARYNKEVITCH         http://starynkevitch.net/Basile/
email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359
8, rue de la Faiencerie, 92340 Bourg La Reine, France
*** opinions {are only mines, sont seulement les miennes} ***

Re: [Caml-list] Developper position: designing a C front-end in OCaml

[Wojciech Meyer]

[-- Attachment #1: Type: text/plain, Size: 2099 bytes --]

Hello,

So there are at least:

- cfront [1]
- yacfe [2]
- CIL

do we need yet another frontend in the compiler community? Just a
digression.

Wojciech

[1] http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=61
[2] http://padator.org/software-yacfe.php





On Tue, Oct 15, 2013 at 3:06 PM, Basile Starynkevitch <
basile@starynkevitch.net> wrote:

> On Tue, Oct 15, 2013 at 02:31:17PM +0200, Xavier Rival wrote:
> >
> > We are looking for an experienced OCaml developper in order to
> > design front-end components for a static analyzer developped as part
> > of the MemCAD ERC project (http://www.di.ens.fr/~rival/memcad.html).
>
>
> If you want to develop in Ocaml CIL is definitely a possible way to go
> (and you could also code a Frama-C plugin, hence taking advantage of
> existing Frama-C infrastructure). If it does not fit all of
> your needs, please contribute your enhancements to it.
>
> Alternatively, Did you consider working inside GCC, perhaps thru a plugin,
> perhaps using MELT, a domain specific language to extend GCC, see
> http://gcc-melt.org/ ?
> you could take advantage of existing GCC infrastructure, in particular
> add some analysis pass after some existing GCC optimizing passes which
> would have already done some transformations (And MELT is not Ocaml,
> but a Lisp-like language, notably enabling you to code in a
> functional style - more than if you did your GCC extension in C++03).
>
> At last you could work with CompCert http://compcert.inria.fr/
> which can be viewed as a C compiler coded in Ocaml (although it is much
> more
> than that).
>
> Regards.
> --
> Basile STARYNKEVITCH         http://starynkevitch.net/Basile/
> email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359
> 8, rue de la Faiencerie, 92340 Bourg La Reine, France
> *** opinions {are only mines, sont seulement les miennes} ***
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 3457 bytes --]

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Florian Weimer]

* Xavier Rival:

> I have used CIL in another project in the past. My experience is that
> it is a great front-end for program transformation. It is less adapted
> to static analysis though, as it does a lot of syntactic
> transformations, causing part of the structure of the code to be
> lost. For instance, it transforms loops into a while(1) form, with
> break statements. This design choice does not help static analyzers,
> and may require recalculating information that was lost in the early
> phases.

Clang mirrors the source pretty closely in its AST, so a Zephyr ASDL
model and serializer for that might be the way to go.  The advantage
would be that you get not just C, but also many popular extensions,
broadening the set of potential inputs for your analysis tools.

GCC is another option (using a similar approach), but it's trees are a
little less close to the source code.

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Dmitry Grebeniuk]

Hello.

> We are talking about changing the AST used to manipulate the programs.
> Changing it (in either CIL or Frama-C) would mean breaking every
> existing code around the world based on it.

  I don't think so.  Imagine that "C source -> CIL representation
(available to code based on CIL)" could be enhanced to "C source ->
Very Concrete C AST -> CIL representation".  Old users are happy, new
users have access to Very Concrete C AST.

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Gabriel Kerneis]

Le 2013-10-15 19:29, Dmitry Grebeniuk a écrit :
>> We are talking about changing the AST used to manipulate the 
>> programs.
>> Changing it (in either CIL or Frama-C) would mean breaking every
>> existing code around the world based on it.
>
>   I don't think so.  Imagine that "C source -> CIL representation
> (available to code based on CIL)" could be enhanced to "C source ->
> Very Concrete C AST -> CIL representation".  Old users are happy, new
> users have access to Very Concrete C AST.

Oh, this is already the case.  "Very concrete AST" is the
"FrontC" project mentionned elsewhere in this thread.

-- 
Gabriel

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[Wojciech Meyer]

[-- Attachment #1: Type: text/plain, Size: 1894 bytes --]

[now to the list, apart from Gabriel]
Hello,

In general, the AST transformation should be gradual, like in logic
rewriting systems kind of Maude. So the AST definitions should be
lightweight as possible and passes declarative. In the end you have a
"final" OCaml AST, with types or without, with blank tokens and comments or
without, and it would be CIL or something else depending what you want.

I am not opposing inventing new frontend, but would rather think what kind
of goodness we can get from the existing solutions. I think sticking with
Clang (or gcc) as a frontend and exporting, maybe automatically the AST
looks like a sane solution, as a bonus we have a C++ frontend that passes
all the conformance testing.

hope that helps,
Wojciech


On Tue, Oct 15, 2013 at 10:36 PM, Gabriel Kerneis <gabriel@kerneis.info>wrote:

> Le 2013-10-15 19:29, Dmitry Grebeniuk a écrit :
>
>  We are talking about changing the AST used to manipulate the programs.
>>> Changing it (in either CIL or Frama-C) would mean breaking every
>>> existing code around the world based on it.
>>>
>>
>>   I don't think so.  Imagine that "C source -> CIL representation
>> (available to code based on CIL)" could be enhanced to "C source ->
>> Very Concrete C AST -> CIL representation".  Old users are happy, new
>> users have access to Very Concrete C AST.
>>
>
> Oh, this is already the case.  "Very concrete AST" is the
> "FrontC" project mentionned elsewhere in this thread.
>
> --
> Gabriel
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/**arc/caml-list<https://sympa.inria.fr/sympa/arc/caml-list>
> Beginner's list: http://groups.yahoo.com/group/**ocaml_beginners<http://groups.yahoo.com/group/ocaml_beginners>
> Bug reports: http://caml.inria.fr/bin/caml-**bugs<http://caml.inria.fr/bin/caml-bugs>
>

[-- Attachment #2: Type: text/html, Size: 3320 bytes --]

Re: [Caml-list] [ocaml-jobs] Developper position: designing a C front-end in OCaml

[David MENTRE]

Hello Gabriel,

2013/10/15 Gabriel Kerneis <gabriel@kerneis.info>:
> Thanks for the link.  You should update the entry about CIL:
> http://gulliver.eu.org/program_dev_check_environments#cil
> to the new URL:
> http://cil.sourceforge.net/
>

Updated, thanks!

david