src/comp/syntax is currently just a sub-module of rustc, but it will,
in the near future, be its own crate. This includes:
- The AST data structure
- The parser
- The pretty-printer
- Visit, walk, and fold
- The syntax extension system
- Some utility stuff that should be in the stdlib*
*) Stdlib extensions currently require a snapshot before they can be
used, and the win build is very broken right now. This is temporary
and will be cleaned up when one of those problems goes away.
A lot of code was moved by this patch, mostly towards a more organized
layout. Some package paths did get longer, and I guess the new layout
will take some getting used to. Sorry about that!
Please try not to re-introduce any dependencies in syntax/ on any of
the other src/comp/ subdirs.
Implement "claim" (issue #14), which is a version of "check" that
doesn't really do the check at runtime. It's an unsafe feature.
The new flag --check-claims turns claims into checks automatically --
but it's off by default, so by default, the assertion in a claim
doesn't execute at runtime.
Wrote some small test cases that use while loops and moves, to
make sure the poststate for the loop body gets propagated into the
new prestate and deinitialization gets reflected.
Along with that, rewrite the code for intersecting states. I still
find it dodgy, but I guess I'll continue trying to add more tests.
Also, I'll probably feel better about it once I start formalizing
the algorithm.
This will probably need more work, as moving doesn't appear to do
quite the right thing yet in general, and we should also check
somewhere that we're not, for example, moving out the content out of
an immutable field (probably moving out of fields is not okay in
general).
Modified typestate to throw away any constraints mentioning a
variable on the LHS of an assignment, recv, assign_op, or on
either side of a swap.
Some code cleanup as well.
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
This reduces some redundancy in the AST data structures and cruft in
the code that works with them. To get a def_id from a node_id, apply
ast::local_def, which adds the local crate_num to the given node_id.
Most code only deals with crate-local node_ids, and won't have to
create def_ids at all.
With the changing of receive semantics the parser has been putting the rhs
expression in the first argument of expr_recv and the lhs in the second, and
all subsequent passes have been referring to them backwords (but still doing
the right thing because they were assuming that lhs was the port and rhs was
the receiver).
This makes all code agree on what lhs and rhs mean for receive expressions.
I noticed that typestate was being lazier than it should be,
because it was only checking typestate for statements and
top-level expression (that is, the expression in a stmt_expr, but
not any subexpressions). So I rewrote the checks in tstate/ck.rs
to use walk, which exposed a few bugs in typestate that I fixed.
Also added some more test cases for if-check.
Most of the fields in an AST item were present in all variants. Things
could be simplified considerably by putting them in the rec rather
than in the variant tags.
Since the decl in a for or for-each loop must always be a local
decl, I changed the AST to express this. Fewer potential match
failures and "the impossible happened" error messages = yay!
Generate appropriate constraints for calls to functions with
preconditions, and reject calls where those constraints don't
hold true in the prestate.
...by which I mean that it works for one test case :-)
* Non-returning calls should set all predicates to be true, not
just the "this function returns" predicate
* Fixed a bug in the expr_alt case in tstate.states that wasn't updating
the changed flag properly, then fixed *another* bug that was updating
it too enthusiastically, but was masked by the first bug.
