rgrig / freeboogie Goto Github PK

I should skim thru the MSR implementation before writing mine. In any case,
it shouldn't be to different from the existing one, which already handles
generics.

I thought z3 interprets % as modulo but it seems to be uninterpreted. Check
and fix.

The ANTLR generated parser has methods for each rule but processes only
some "antlr streams". I should write an adapter between String and those
streams. Try to make the interface nice as it will be used in the Eclipse
editor.

At the moment a macro cycle like
  \def\A{\B}
  \def\B{\A}
  \A
leads to an infinite loop that eventually runs out of memory. (Note that
macro definitions are NOT expanded until macros are used.)

There should be some sort of check for that. The simplest to implement
without affecting performance in the common case is to put a fixed limit on
the depth of macro expansions.

A bit fancier is to not immediately report an error when the limit is
reached but rather check if there is indeed a cycle and, if not, increase
the limit. To check if there is indeed a cycle you go up the macro 'stack'
(which doesn't exist explicitly) and check for duplicates.

Instead of
--log-level=[info|warning|error]  (default: warning)
-ll=[info|warning|error]  (default: warning)
     Configure how much information should be logged.

--dump-intermediate-stages=<file>
-dis=<file>
     Specify  a directory where to dump the result  of each transformation.
     The  dump includes  a  Boogie  program,  its  symbol  table,  and  its
     flowgraphs.

It should be more like
--log-level|-ll=[info|warning|error]  default: warning
     how much information should be logged
--dump-intermediate-stages|-dis=<file>
     directory where intermediate results are dumped

The best place to implement this is probably one of
  FlowGraphMaker
  LabelsCollector

Make all tests active.

I believe there are a few places where FileLocation is not carried over
appropriately. There should be a debug switch that prints/logs all the
places from which the mk() methods are called without locations.

An easy way to implement type synonyms such as
  type Foo a b = [a]b;
is to expand them before doing typechecking. This may complicate a little
error reporting.

The FreeBoogie AST now uses singly linked lists. The rationale was that:
(1) we want immutable lists (in general, immutable AST), 
(2) there is no class for immutable lists in the Java API, and 
(3) implementing singly linked lists ourselves didn't require support from
AstGen.

However, there are disadvantages:
(1) David Cok complained that this leads to hard-to-maintain code. I
respectfully disagree but, even so, I expect others to feel the same.
(2) Performance: The JVM does not support tail calls and won't support them
for a while [http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=4726340].
This leads to slowness (not sure how much) and the _necessity_ of setting a
higher stack.
(3) Exceptions backtraces are hard to read.
(4) You can't loop over the list using the nice foreach syntax. The natural
recursive implementation is somewhat cumbersome in Java because defining a
new function requires typing lots of crap. In general, you can't use
Iterator and related facilities.

Since Google Collections have been recently added as an external dependency
we now have a nice ImmutableList class for free. Using it would allow us to
keep the AST immutable (thus avoiding ASTs that change from "under your
feet") and avoid the problems outlined above. The downside: This requires
changing pretty much every existing visitor.

The grammar is somewhat disorganized.

I should reorder the rules so that:
(1) they are laid out in BFS order, and alphabetically
(2) all the list rules are grouped together, and alphabetically

Move all issues from TODO files into the googlecode tracker.

Right now the best place that documents AstGen is in some FreeBoogie
javadoc. A wiki page is much better suited for that, given that people may
want to use AstGen independent of FreeBoogie.

if statements (commands) can always be desugarred using assume and goto

The current FreeBoogie plugin doesn't do anything useful. There should be
an editor and a way to run FreeBoogie on a Boogie file.

It can be tested with
 (1) the hand-written tests taken from krml178
 (2) the examples that come with Spec#
 (3) the automatically translated boogie benchmarks

At the moment the operator <: is parsed as in Boogie 1 and not interpreted
properly. It should be parsed as in Boogie 2, at least.

This should amount to making Main extend FbCliAntTaskBase and maybe a bit
more work to make it easy to use.

The code in MapRemover is horrible. There must be a better way to construct
the corresponding ASTs. Perhaps use the parser.

Triggers don't end up in the VC at the moment and that affects performance
a *lot*.

In Boogie a function must return *exactly* one value. Anything else should
fail parsing.

At the moment there is a @supresswarnings in Logger that can lead to ugly
trouble. This really needs more type-safety (since I already fall for it).
When you say:
  Logger<C,L> log = Logger.get("foo");
there is no guarantee that the name "foo" is attached to something of the
type Logger<C,L>. The problem, of course, is that generics aren't reified
in Java. I'm not sure what's a good solution.

It's convenient sometimes to have
  void see(
    VariableDecl vd,
    ImmutableList<Attribute> attr,
    String name,
    Type type,
    ImmutableList<AtomId> typeArgs,
    Expr where)
and then say
  name

instead of having
  void see(VariableDecl variableDecl)
and then say
  variabledecl.name()

BUT... the former is a *pain* to maintain when the abstract grammar
changes. Plus, the (necessary) vertical alignment of the arguments looks ugly.

This task is boring, takes time, but make further changes easier.

Add support for tagging members in AstGen. This way templates can do
something different for lists.

The AST for the body of functions should *be* a graph.

It is convenient (although not efficient) to redo name resolution instead
of forcing each transformer to work harder and update the symbol table too.
However, it is inconvenient (*and* inefficient) to recompute the graph of
commands from (possibly nested) blocks (which are lists of commands) and
goto-s. This is because I tend to think of the program as a graph anyway,
and keeping track of lowly things such as labels is a headache I'd rather
avoid.

Of course, if WhileCmd is not desugared and dealt with, we *have* to work
with blocks, labels, and goto-s.

Have a mechanism to make sure that all term names start with "term$$", and
make sure this prefix is not accidentally added to number literals.

It should be possible to include another file with a macro like:
  \include{file_path}
Make sure to check for cycles.

Make sure that tc2.ok/test00.in is processed without errors by MSR Boogie.

Make sure 'where' clauses are processed properly.

Implement an alpha renaming phase that makes sure each definition uses an
unique name throughout the program. Also, keep the correspondence to the
original name, for error reporting.

This will allow:
(1) processing the intermediate dumps (which use "forbidden names")
(2) hash-consing for ASTs, if deemed necessary

At the moment the split between general terms and smt terms seems to be an
overkill.

The code
  function f(args) returns (results) { expr }
is equivalent to
  function f(args) returns (results);
  axiom (forall args, results :: f(args) == expr);

Do the desugaring.

It should be possible to parse a string and know for each terminal and
non-terminal which substring it matched. This will be useful for
edit-and-verify reloaded.

If the template contains
  \file{a/b}
it should work on both Linux and Windows, even if the natural way to say it
on windows is
  \file{a\b}
This one would be confused with macros anyway.

With immutable data structures it is sometimes convenient to be able to
"change" one field:
  Command newCommand = oldCommand.changeLabels(emptyList);
To be able to generate code for changeLables one would need to write a
template like
  \members{
    public \ClassName change\MemberName(\MemberType newMember) {
      return new \ClassName(\members[,]
        {\if{\MemberName==\MemberName[1]}{newMember}{\memberName}});
    }
  }
or something similar.

There are two things that must be done to get the template above to work:
1. support references to outer loops, as in \MemberName[0], \MemberName[1]
2. evaluate conditions

At the moment you can only say
  \members[SEP]{foo}
if SEP doesn't contain any special character like [, *, |, etc. The
separator should be read as a string up to the matching ], so that one can say
  \members[&&]{\memberName}
for example.

It might even be worth processing the inside of [] using the current
context (including macros), save the result as a string, and use that string.

Make sure the Alterative* classes do all that * classes do and then keep
keep only the new ones. (PS: This should have been a branch.)

This issue was created by revision r566.

If there are more } than { the TemplateParser tries to rewind
when there is no mark. I believe this used to be a no-op, but
the proper fix would be to fix the TemplateParser to not try to
rewind the token stream when it didn't set a mark on it.

Basically, implement --dump-intermediate-stages.

This should create a directory with one subdirectory for each phase. In
each subdirectory there should be a boogie file, a symbol table file, and a
bunch of flow-graph files (one for each implementation). In short: a dump
of the AST and of the TypeChecker information in a readable form.

The first stage should be 'parsing', which isn't strictly speaking an AST
transformer.

It is easier to maintain svnignore if there is separate directory with all
the generated files. See also the comments for r575.

break statements are just convenient syntactic sugar for goto

In FreeBoogie templates I have the string
  "\if_primitive{\Membertype}{\MemberType}"
in so many places that I wish I'd be able to define
  \def\mt{\if_primitive{\Membertype}{\MemberType}}
and then use it simply as
  \mt

It's probably not worth it to support parameters. If a use-case arises then
I should consider parameters too.

Implement a desugarer for while commands.

That test is designed to check that 1MB is processed in less than 5
seconds. At the moment the 5 second limit is removed because at some point
AstGen became too slow.

It should be possible to say
  \def\terminals[1]{\classes{\if_terminal{#0}{}}}
The [1] is the number of parameters and #0 stands for the first parameter.
It is used as:
  \terminals{\ClassName}

Use logging with category/level everywhere, instead of the Java one.

There is a preliminary (?) coq implementation that dumps proof obligations
in a file, but no switch so that normal users can activate it.

Withe the Boogie 2 type system it is not safe to erase types. Instead they
need to be encoded, as explained here:
  http://research.microsoft.com/en-us/um/people/leino/papers/krml186.pdf

Change the cron script to check that
(1) the svn trunk in googlecode compiles
(2) the svn trunk in mobius passes tests

Also, put the script in the svn.

Make sure that 'where' on variable declarations is handled correctly. This
task is mainly about adding tests.