| Age | Commit message (Collapse) | Author | Lines |
|---|
|
|
|
|
|
|
|
|
|
Closes #913
|
|
Issue #918
|
|
|
|
Long lines were fixed in a very crude way, as I'll be following up
with another reformat in a bit.
|
|
|
|
|
|
This changes the indexing syntax from .() to [], the vector syntax from ~[] to
[] and the extension syntax from #fmt() to #fmt[]
|
|
This should make the compilation process a bit less noisy.
|
|
|
|
|
|
|
|
|
|
|
|
Previously, typestate was initializing the init constraint for
a declared-but-not-initialized variable (like x in "let x;") to False,
but other constraints to Don't-know. This led to over-lenient results
when a variable was used before declaration (see the included test
case). Now, everything gets initialized to False in the prestate/poststate-
finding phase, and Don't-know should only be used in pre/postconditions.
This aspect of the algorithm really needs formalization (just on paper),
but for now, this closes #700
|
|
|
|
To handle multiple-LHS declarations with initializers properly,
I changed seq_states to take a list of expressions paired with optional
names, not just a list of expressions. Then, the same logic that handles
ordered lists of subexpressions everywhere else can handle multi-
declarations.
|
|
|
|
|
|
|
|
|
|
so that if we have a function like:
f(...) : p(x) {
...
}
p(x) is true inside the body of f.
Closes #694.
|
|
Programs with constrained types now parse and typecheck, but
typestate doesn't check them specially, so the one relevant test
case so far is XFAILed.
Also rewrote all of the constraint-related data structures in the
process (again), for some reason. I got rid of a superfluous
data structure in the context that was mapping front-end constraints
to resolved constraints, instead handling constraints in the same
way in which everything else gets resolved.
|
|
|
|
|
|
|
|
|
|
middle::tstate::{bitvectors, ck}
|
|
interior vectors
|
|
vectors
|
|
|
|
|
|
middle::tstate::{bitvectors, ck}
|
|
interior vectors
|
|
vectors
|
|
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.
|
|
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.
|
|
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.
|
|
This in preparation of making 'res' a keyword for defining resources.
Please don't introduce too many new ones in the meantime...
|
|
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.
|
|
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.
|
|
|
|
|
|
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 :-)
|
|
|
|
Start writing the cases for expr_check and expr_call to take
predicates into account, but this isn't working yet.
|
