[Haskell-cafe] static analysis of a C-like language

[Paul Brauner]

If you're interested I have a draft implemetation of that paper
<https://github.com/polux/abstract-interpreters/blob/master/src/Main.hs> in
Haskell that uses monad transformers. There's another one
<https://github.com/josefs/AbstractingDefinitionalInterpreters> online that
uses effect handlers. The original scheme implementation
<https://github.com/plum-umd/abstracting-definitional-interpreters> is also
available.

A caveat: while playing with my implementation I found some issue with the
GC as described in the paper and was able to reproduce on the reference
implementation:
https://github.com/plum-umd/abstracting-definitional-interpreters/issues/82.
I'm not knowledgeable enough to understand whether this is a flaw of the
approach or something that can be easily fixed.

Paul

On Thu, Nov 29, 2018 at 3:31 PM Carter Schonwald <carter.schonwald at gmail.com>
wrote:

> Most parser libraries in Haskell provide facilities for including source
> information.
>
> And then you include in your syntax tree extra fields for those positions.
>
> Simple as that
>
>
> The paper :
>
> http://david.darais.com/assets/papers/abstracting-definitional-interpreters/adi.pdf
> Is a great reference for how to add a bunch of program analysis features
> after you have a working interpreter .  Also it’s citations show a bunch of
> ways you can Add different flavored of anayses
>
> On Mon, Nov 26, 2018 at 3:37 PM Olaf Klinke <olf at aatal-apotheke.de> wrote:
>
>> > Hello Olaf,
>> >
>> > to me that sounds as if you want to do an abstract interpretation with
>> a
>> > forward collecting semantics that employs non-relational abstract
>> > domains for the primitive data types and summarizes the dimensions of
>> > arrays.
>> ...
>> > I would start by writing a simple interpreter for the language to be
>> > analyzed. That way you fix messy details before they bite you, e.g. the
>> > order in which submodules are loaded and initialized.
>>
>> I was hoping not having to write an interpreter (because the language
>> author wrote a translation to C++ already), but if that is the way to go,
>> I'll do it. As I understand it, the Haskell semantics should contain just
>> enough substance so that the errors I am after will cause hiccups in the
>> Haskell compiler? That is indeed a compelling approach.
>> What this does not address is the question about error reporting:  How
>> could a translation to Haskell preserve information about scope, source
>> position and masking? Can I leverage the ghc API for that?
>>
>> Regards,
>> Olaf
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181204/9655fe84/attachment.html>