mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
ca7cfbe3d0
rust/src/comp/middle/tstate/states.rs

790 lines
28 KiB
Rust
Raw Normal View History

Copy first batch of material from libstd to libcore.
2011-12-13 18:25:51 -06:00
import core::{vec, option};
import option::{none, some};
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
import ann::*;
Propagate constraints through copy, move, and swap Assignments and moves with a simple local variable reference on the RHS now propagate any typestate constraints the RHS was involved in to the LHS. Swaps where both sides are local variables exchange the constraints. This was a pain in the butt and I'm still not proud of the resulting code. Needs refactoring like whoa.
2011-07-09 00:05:30 -05:00
import aux::*;
Factor imports mindlessly.
2011-09-12 18:13:28 -05:00
import tritv::{tritv_clone, tritv_set, ttrue};
Restructure the "checking" pass in typestate 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.
2011-06-17 21:07:23 -05:00
Instantiate function preconditions inside the function body so that if we have a function like: f(...) : p(x) { ... } p(x) is true inside the body of f. Closes #694.
2011-07-21 18:03:30 -05:00
import bitvectors::*;
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
import pat_util::*;
Move everything syntax-related to syntax/, break deps on rest of compiler 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.
2011-07-05 04:48:19 -05:00
import syntax::ast::*;
Move functions from syntax::ast to syntax::ast_util This leaves syntax::ast just defining the AST, which strikes me as somewhat nicer
2011-08-21 23:44:41 -05:00
import syntax::ast_util::*;
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
import syntax::codemap::span;
Cleanup unused imports
2011-11-10 10:41:42 -06:00
import middle::ty::{expr_ty, type_is_bot};
import util::common::{field_exprs, has_nonlocal_exits};
Make driver::session::session no longer an object Rather, it is now a struct where properties like opts are accessed directly, and the error-reporting methods are part of a static impl (with the same name as the type).
2012-01-12 10:59:49 -06:00
import driver::session::session;
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn forbid_upvar(fcx: fn_ctxt, rhs_id: node_id, sp: span, t: oper_type) {
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
alt t {
oper_move. {
alt local_node_id_to_def(fcx, rhs_id) {
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
some(def_upvar(_, _, _)) {
fcx.ccx.tcx.sess.span_err(sp,
"Tried to deinitialize a variable \
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
declared in a different scope");
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
}
_ { }
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
}
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
_ {/* do nothing */ }
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
}
}
Box ast::path values It seems inefficient to copy them around. Let's measure whether that's actually > the case
2011-11-30 06:38:38 -06:00
fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
rhs_id: node_id, instlhs: inst, init_op: init_op) {
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
forbid_upvar(fcx, rhs_id, rhs_path.span, op_to_oper_ty(init_op));
let rhs_d_id = local_node_id_to_def_id(fcx, rhs_id);
alt rhs_d_id {
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
some(rhsid) {
// RHS is a local var
let instrhs =
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
{ident: path_to_ident(rhs_path), node: rhsid.node};
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
copy_in_poststate(fcx, post, instlhs, instrhs,
op_to_oper_ty(init_op));
}
_ {
// not a local -- do nothing
}
}
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) ->
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
{changed: bool, post: poststate} {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed = false;
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
let post = tritv_clone(pres);
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
for b: binding in bindings {
alt b.rhs {
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
some(an_init) {
// an expression, with or without a destination
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
changed |=
find_pre_post_state_expr(fcx, post, an_init.expr) || changed;
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
post = tritv_clone(expr_poststate(fcx.ccx, an_init.expr));
Partially implement destructuring locals You can now say let {bcx, val} = some_result_returner(); Similar for loop variables. Assigning to such variables is not safe yet. Function arguments also remain a TODO.
2011-07-28 05:01:45 -05:00
for i: inst in b.lhs {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
alt an_init.expr.node {
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
expr_path(p) {
handle_move_or_copy(fcx, post, p, an_init.expr.id, i,
an_init.op);
}
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
_ { }
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
}
set_in_poststate_ident(fcx, i.node, i.ident, post);
}
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
// Forget the RHS if we just moved it.
if an_init.op == init_move {
forget_in_poststate(fcx, post, an_init.expr.id);
}
Partially implement destructuring locals You can now say let {bcx, val} = some_result_returner(); Similar for loop variables. Assigning to such variables is not safe yet. Function arguments also remain a TODO.
2011-07-28 05:01:45 -05:00
}
none {
for i: inst in b.lhs {
// variables w/o an initializer
clear_in_poststate_ident_(fcx, i.node, i.ident, post);
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
}
}
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret {changed: changed, post: post};
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr,
Port the compiler to the typaram foo<T> syntax.
2011-08-12 09:15:18 -05:00
parent: node_id, c: option::t<tsconstr>) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed = find_pre_post_state_expr(fcx, pres, e);
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let post = tritv_clone(expr_poststate(fcx.ccx, e));
alt c {
none. { }
some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
rhs: @expr, parent: node_id, ty: oper_type) ->
Reformat for new syntax
2011-07-27 07:19:39 -05:00
bool {
let changed = set_prestate_ann(fcx.ccx, parent, pres);
Propagate constraints through copy, move, and swap Assignments and moves with a simple local variable reference on the RHS now propagate any typestate constraints the RHS was involved in to the LHS. Swaps where both sides are local variables exchange the constraints. This was a pain in the butt and I'm still not proud of the resulting code. Needs refactoring like whoa.
2011-07-09 00:05:30 -05:00
changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
Reformat for new syntax
2011-07-27 07:19:39 -05:00
changed =
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs), rhs) ||
changed;
Forbid blocks from deinitializing upvars Move expressions where the RHS is an upvar are now forbidden within block expressions.
2011-09-06 17:26:57 -05:00
forbid_upvar(fcx, rhs.id, rhs.span, ty);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let post = tritv_clone(expr_poststate(fcx.ccx, rhs));
alt lhs.node {
expr_path(p) {
// for termination, need to make sure intermediate changes don't set
// changed flag
// tmp remembers "old" constraints we'd otherwise forget,
// for substitution purposes
let tmp = tritv_clone(post);
alt ty {
oper_move. {
if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
forget_in_poststate_still_init(fcx, post, lhs.id);
}
oper_swap. {
forget_in_poststate_still_init(fcx, post, lhs.id);
forget_in_poststate_still_init(fcx, post, rhs.id);
}
_ { forget_in_poststate_still_init(fcx, post, lhs.id); }
}
gen_if_local(fcx, post, lhs);
alt rhs.node {
expr_path(p1) {
let d = local_node_id_to_local_def_id(fcx, lhs.id);
let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
alt d {
some(id) {
alt d1 {
some(id1) {
let instlhs =
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
{ident: path_to_ident(p), node: id};
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let instrhs =
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
{ident: path_to_ident(p1), node: id1};
Reformat for new syntax
2011-07-27 07:19:39 -05:00
copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
ty);
}
_ { }
Propagate constraints through copy, move, and swap Assignments and moves with a simple local variable reference on the RHS now propagate any typestate constraints the RHS was involved in to the LHS. Swaps where both sides are local variables exchange the constraints. This was a pain in the butt and I'm still not proud of the resulting code. Needs refactoring like whoa.
2011-07-09 00:05:30 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ { }
Propagate constraints through copy, move, and swap Assignments and moves with a simple local variable reference on the RHS now propagate any typestate constraints the RHS was involved in to the LHS. Swaps where both sides are local variables exchange the constraints. This was a pain in the butt and I'm still not proud of the resulting code. Needs refactoring like whoa.
2011-07-09 00:05:30 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ {/* do nothing */ }
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ { }
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_call(fcx: fn_ctxt, pres: prestate, a: @expr,
id: node_id, ops: [init_op], bs: [@expr],
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
cf: ret_style) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed = find_pre_post_state_expr(fcx, pres, a);
Track arguments in typestate Add the infrastructure for arguments -- as well as local vars -- to be deinitialized with move-mode calls. Address Issue #819
2011-08-17 18:58:00 -05:00
// FIXME: This could be a typestate constraint
Rename std::ivec to std::vec
2011-08-15 18:38:23 -05:00
if vec::len(bs) != vec::len(ops) {
Convert uses of #fmt to #ifmt. Issue #855
2011-08-28 02:24:28 -05:00
fcx.ccx.tcx.sess.span_bug(a.span,
Convert all uses of #ifmt to #fmt. Issue #855
2011-09-01 20:49:10 -05:00
#fmt["mismatched arg lengths: \
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
%u exprs vs. %u ops",
Convert uses of #fmt to #ifmt. Issue #855
2011-08-28 02:24:28 -05:00
vec::len(bs), vec::len(ops)]);
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
}
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
ret find_pre_post_state_exprs(fcx, expr_poststate(fcx.ccx, a), id, ops,
bs, cf) || changed;
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id,
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
ops: [init_op], es: [@expr], cf: ret_style) ->
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
bool {
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
let rs = seq_states(fcx, pres, anon_bindings(ops, es));
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed = rs.changed | set_prestate_ann(fcx.ccx, id, pres);
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
/* if this is a failing call, it sets everything as initialized */
Reformat for new syntax
2011-07-27 07:19:39 -05:00
alt cf {
noreturn. {
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
let post = false_postcond(num_constraints(fcx.enclosing));
changed |= set_poststate_ann(fcx.ccx, id, post);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
}
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
ret changed;
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local,
index: @expr, body: blk, id: node_id) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let loop_pres = intersect_states(pres, block_poststate(fcx.ccx, body));
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed =
set_prestate_ann(fcx.ccx, id, loop_pres) |
find_pre_post_state_expr(fcx, pres, index);
Add missing files git add didn't, so this actually has the changes that should have been in the previous commit
2011-07-12 13:26:14 -05:00
Partially implement destructuring locals You can now say let {bcx, val} = some_result_returner(); Similar for loop variables. Assigning to such variables is not safe yet. Function arguments also remain a TODO.
2011-07-28 05:01:45 -05:00
// Make sure the index vars are considered initialized
Add missing files git add didn't, so this actually has the changes that should have been in the previous commit
2011-07-12 13:26:14 -05:00
// in the body
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let index_post = tritv_clone(expr_poststate(fcx.ccx, index));
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
pat_bindings(pat_util::normalize_pat(fcx.ccx.tcx, l.node.pat)) {|p|
let ident = alt p.node
{ pat_ident(name, _) { path_to_ident(name) } };
Partially implement destructuring locals You can now say let {bcx, val} = some_result_returner(); Similar for loop variables. Assigning to such variables is not safe yet. Function arguments also remain a TODO.
2011-07-28 05:01:45 -05:00
set_in_poststate_ident(fcx, p.id, ident, index_post);
Move ast_util::pat_bindings over to new iter system. Issue #1056
2011-10-21 05:41:42 -05:00
};
Add missing files git add didn't, so this actually has the changes that should have been in the previous commit
2011-07-12 13:26:14 -05:00
changed |= find_pre_post_state_block(fcx, index_post, body);
Restructure the "checking" pass in typestate 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.
2011-06-17 21:07:23 -05:00
Reformat for new syntax
2011-07-27 07:19:39 -05:00
if has_nonlocal_exits(body) {
Tests for while loops that may invalidate constraints 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.
2011-06-27 20:12:37 -05:00
// See [Break-unsound]
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret changed | set_poststate_ann(fcx.ccx, id, pres);
} else {
let res_p =
intersect_states(expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body));
Tests for while loops that may invalidate constraints 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.
2011-06-27 20:12:37 -05:00
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
}
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn gen_if_local(fcx: fn_ctxt, p: poststate, e: @expr) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
alt e.node {
expr_path(pth) {
Make resolve recognize upvars Upvars are now marked with def_upvar throughout, not just when going through freevars::lookup_def. This makes things less error-prone. One thing to watch out for is that def_upvar is used in `for each` bodies too, when they refer to a local outside the body.
2011-09-01 07:35:00 -05:00
alt fcx.ccx.tcx.def_map.find(e.id) {
Forbid assignment to by-reference bindings Issue #918
2011-09-15 07:08:54 -05:00
some(def_local(loc, _)) {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret set_in_poststate_ident(fcx, loc.node,
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
path_to_ident(pth), p);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ { ret false; }
}
}
_ { ret false; }
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
maybe_alt: option::t<@expr>, id: node_id, chk: if_ty,
pres: prestate) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed =
set_prestate_ann(fcx.ccx, id, pres) |
find_pre_post_state_expr(fcx, pres, antec);
Prohibit trailing whitespace under 'tidy' script. Clean up all caught cases.
2011-07-13 17:44:09 -05:00
Restructure the "checking" pass in typestate 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.
2011-06-17 21:07:23 -05:00
/*
log_err("join_then_else:");
log_expr_err(*antec);
log_bitv_err(fcx, expr_prestate(fcx.ccx, antec));
log_bitv_err(fcx, expr_poststate(fcx.ccx, antec));
log_block_err(conseq);
log_bitv_err(fcx, block_prestate(fcx.ccx, conseq));
log_bitv_err(fcx, block_poststate(fcx.ccx, conseq));
log_err("****");
log_bitv_err(fcx, expr_precond(fcx.ccx, antec));
log_bitv_err(fcx, expr_postcond(fcx.ccx, antec));
log_bitv_err(fcx, block_precond(fcx.ccx, conseq));
log_bitv_err(fcx, block_postcond(fcx.ccx, conseq));
*/
Reformat for new syntax
2011-07-27 07:19:39 -05:00
alt maybe_alt {
none. {
Handle if-check with no else correctly in typestate Propagate the if-check constraint into the consequent even when there's no else branch. (Oops!)
2011-09-02 20:43:50 -05:00
alt chk {
if_check. {
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
let conseq_prestate = tritv_clone(expr_poststate(fcx.ccx, antec));
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
changed |=
find_pre_post_state_block(fcx, conseq_prestate, conseq) |
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
set_poststate_ann(fcx.ccx, id,
expr_poststate(fcx.ccx, antec));
Handle if-check with no else correctly in typestate Propagate the if-check constraint into the consequent even when there's no else branch. (Oops!)
2011-09-02 20:43:50 -05:00
}
_ {
changed |=
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
conseq) |
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
set_poststate_ann(fcx.ccx, id,
expr_poststate(fcx.ccx, antec));
Handle if-check with no else correctly in typestate Propagate the if-check constraint into the consequent even when there's no else branch. (Oops!)
2011-09-02 20:43:50 -05:00
}
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
some(altern) {
changed |=
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, antec),
altern);
let conseq_prestate = expr_poststate(fcx.ccx, antec);
alt chk {
if_check. {
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
conseq_prestate = tritv_clone(conseq_prestate);
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
}
_ { }
}
changed |= find_pre_post_state_block(fcx, conseq_prestate, conseq);
let poststate_res =
intersect_states(block_poststate(fcx.ccx, conseq),
expr_poststate(fcx.ccx, altern));
/*
fcx.ccx.tcx.sess.span_note(antec.span,
"poststate_res = " + aux::tritv_to_str(fcx, poststate_res));
fcx.ccx.tcx.sess.span_note(antec.span,
"altern poststate = " +
aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
fcx.ccx.tcx.sess.span_note(antec.span,
"conseq poststate = " + aux::tritv_to_str(fcx,
block_poststate(fcx.ccx, conseq)));
*/
changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
}
Bring back if-check Add "if check" (expr_if_check), a variation on check that executes an "else" clause rather than failing if the check doesn't hold.
2011-06-16 13:56:34 -05:00
}
ret changed;
}
integrate cap clause into type state, but not trans
2011-12-18 22:45:30 -06:00
fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
pres: prestate, cap_clause: capture_clause)
-> bool
{
let ccx = fcx.ccx;
let pres_changed = set_prestate_ann(ccx, e_id, pres);
let post = tritv_clone(pres);
vec::iter(cap_clause.moves) { |cap_item|
forget_in_poststate(fcx, post, cap_item.id);
}
ret set_poststate_ann(ccx, e_id, post) || pres_changed;
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let num_constrs = num_constraints(fcx.enclosing);
alt e.node {
Remove seq_kind from ast::expr_vec
2011-08-18 13:37:19 -05:00
expr_vec(elts, _) {
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
ret find_pre_post_state_exprs(fcx, pres, e.id,
Rename std::ivec to std::vec
2011-08-15 18:38:23 -05:00
vec::init_elt(init_assign,
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
vec::len(elts)), elts,
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
return_val);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
Change the way block calls are parsed, mark them as block-calls. This makes it possible to omit the semicolon after the block, and will cause the pretty-printer to properly print such calls (if pretty-printing of blocks wasn't so broken). Block calls (with the block outside of the parentheses) can now only occur at statement level, and their value can not be used. When calling a block-style function that returns a useful value, the block must be put insde the parentheses. Issue #1054
2011-10-21 07:11:24 -05:00
expr_call(operator, operands, _) {
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
ret find_pre_post_state_call(fcx, pres, operator, e.id,
callee_arg_init_ops(fcx, operator.id),
operands,
Reformat for new syntax
2011-07-27 07:19:39 -05:00
controlflow_expr(fcx.ccx, operator));
}
expr_bind(operator, maybe_args) {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
let args = [];
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
let callee_ops = callee_arg_init_ops(fcx, operator.id);
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
let ops = [];
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
let i = 0;
Port the compiler to the typaram foo<T> syntax.
2011-08-12 09:15:18 -05:00
for a_opt: option::t<@expr> in maybe_args {
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
alt a_opt {
none. {/* no-op */ }
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
some(a) { ops += [callee_ops[i]]; args += [a]; }
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
}
i += 1;
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
ret find_pre_post_state_call(fcx, pres, operator, e.id, ops, args,
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
return_val);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
expr_path(_) { ret pure_exp(fcx.ccx, e.id, pres); }
Switch log_expr to carrying a full expr:u32 for level. Add log_full variant that parses that expr, prepare for snapshot.
2011-12-21 16:31:31 -06:00
expr_log(_, lvl, ex) {
ret find_pre_post_state_two(fcx, pres, lvl, ex, e.id, oper_pure);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
Reformat. Issue #855
2011-09-02 17:34:58 -05:00
expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
Reformat for new syntax
2011-07-27 07:19:39 -05:00
expr_lit(l) { ret pure_exp(fcx.ccx, e.id, pres); }
split proto from fn_decl, as not all fn_decls know the proto. this will address the (crashing) new test added.
2011-12-29 22:07:55 -06:00
expr_fn(_, _, _, cap_clause) {
integrate cap clause into type state, but not trans
2011-12-18 22:45:30 -06:00
ret find_pre_post_state_cap_clause(fcx, e.id, pres, *cap_clause);
}
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
expr_fn_block(_, _) { ret pure_exp(fcx.ccx, e.id, pres); }
Reformat for new syntax
2011-07-27 07:19:39 -05:00
expr_block(b) {
ret find_pre_post_state_block(fcx, pres, b) |
Use single-bar or to make tstate/states.rs prettier Sorry. This is the kind of thing I do when I'm on a plane and too tired to manage anything that requires thinking.
2011-06-25 10:29:50 -05:00
set_prestate_ann(fcx.ccx, e.id, pres) |
set_poststate_ann(fcx.ccx, e.id, block_poststate(fcx.ccx, b));
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
expr_rec(fields, maybe_base) {
let changed =
Implement typestate checking for move-mode args. Un-XFAIL compile-fail/move-arg.rs.
2011-08-08 21:38:19 -05:00
find_pre_post_state_exprs(fcx, pres, e.id,
Rename std::ivec to std::vec
2011-08-15 18:38:23 -05:00
vec::init_elt(init_assign,
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
vec::len(fields)),
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
field_exprs(fields), return_val);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
alt maybe_base {
none. {/* do nothing */ }
some(base) {
changed |=
find_pre_post_state_expr(fcx, pres, base) |
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, base));
}
}
ret changed;
}
Tuple types back, not constructable yet
2011-08-15 04:40:26 -05:00
expr_tup(elts) {
ret find_pre_post_state_exprs(fcx, pres, e.id,
Rename std::ivec to std::vec
2011-08-15 18:38:23 -05:00
vec::init_elt(init_assign,
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
vec::len(elts)), elts,
Rename ast::controlflow to ast::ret_style It will include information about returning by alias.
2011-09-14 03:38:23 -05:00
return_val);
Add operator 'copy', translates as fall-through.
2011-08-15 17:35:40 -05:00
}
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
expr_copy(a) { ret find_pre_post_state_sub(fcx, pres, a, e.id, none); }
Reformat for new syntax
2011-07-27 07:19:39 -05:00
expr_move(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_move);
}
expr_assign(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_assign);
}
expr_swap(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_swap);
// Could be more precise and actually swap the role of
// lhs and rhs in constraints
}
expr_ret(maybe_ret_val) {
let changed = set_prestate_ann(fcx.ccx, e.id, pres);
/* normally, everything is true if execution continues after
a ret expression (since execution never continues locally
after a ret expression */
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
// FIXME should factor this out
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
let post = false_postcond(num_constrs);
// except for the "diverges" bit...
kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
set_poststate_ann(fcx.ccx, e.id, post);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
alt maybe_ret_val {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
none. {/* do nothing */ }
some(ret_val) {
changed |= find_pre_post_state_expr(fcx, pres, ret_val);
}
}
ret changed;
}
expr_be(val) {
let changed = set_prestate_ann(fcx.ccx, e.id, pres);
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
let post = false_postcond(num_constrs);
// except for the "diverges" bit...
kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
set_poststate_ann(fcx.ccx, e.id, post);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret changed | find_pre_post_state_expr(fcx, pres, val);
}
expr_if(antec, conseq, maybe_alt) {
ret join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if,
pres);
}
expr_ternary(_, _, _) {
ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
}
expr_binary(bop, l, r) {
if lazy_binop(bop) {
let changed = find_pre_post_state_expr(fcx, pres, l);
changed |=
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r);
ret changed | set_prestate_ann(fcx.ccx, e.id, pres) |
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, l));
} else {
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
expr_assign_op(op, lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id,
oper_assign_op);
}
expr_while(test, body) {
/*
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("in a while loop:");
Reformat for new syntax
2011-07-27 07:19:39 -05:00
log_expr_err(*e);
aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body));
aux::log_tritv_err(fcx, pres);
*/
let loop_pres =
intersect_states(block_poststate(fcx.ccx, body), pres);
// aux::log_tritv_err(fcx, loop_pres);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
// #error("---------------");
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed =
set_prestate_ann(fcx.ccx, e.id, loop_pres) |
Tests for while loops that may invalidate constraints 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.
2011-06-27 20:12:37 -05:00
find_pre_post_state_expr(fcx, loop_pres, test) |
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
Use single-bar or to make tstate/states.rs prettier Sorry. This is the kind of thing I do when I'm on a plane and too tired to manage anything that requires thinking.
2011-06-25 10:29:50 -05:00
body);
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
Reformat for new syntax
2011-07-27 07:19:39 -05:00
/* conservative approximation: if a loop contains a break
or cont, we assume nothing about the poststate */
/* which is still unsound -- see [Break-unsound] */
if has_nonlocal_exits(body) {
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
} else {
let e_post = expr_poststate(fcx.ccx, test);
let b_post = block_poststate(fcx.ccx, body);
ret changed |
set_poststate_ann(fcx.ccx, e.id,
intersect_states(e_post, b_post));
}
}
expr_do_while(body, test) {
let loop_pres = intersect_states(expr_poststate(fcx.ccx, test), pres);
let changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
changed |= find_pre_post_state_block(fcx, loop_pres, body);
/* conservative approximination: if the body of the loop
could break or cont, we revert to the prestate
(TODO: could treat cont differently from break, since
if there's a cont, the test will execute) */
changed |=
find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body),
test);
let breaks = has_nonlocal_exits(body);
if breaks {
// this should probably be true_poststate and not pres,
// b/c the body could invalidate stuff
// FIXME [Break-unsound]
// This is unsound as it is -- consider
// while (true) {
// x <- y;
// break;
// }
// The poststate wouldn't take into account that
// y gets deinitialized
changed |= set_poststate_ann(fcx.ccx, e.id, pres);
} else {
changed |=
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, test));
}
ret changed;
}
expr_for(d, index, body) {
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
}
expr_index(val, sub) {
ret find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure);
}
expr_alt(val, alts) {
let changed =
set_prestate_ann(fcx.ccx, e.id, pres) |
find_pre_post_state_expr(fcx, pres, val);
let e_post = expr_poststate(fcx.ccx, val);
let a_post;
Rename std::ivec to std::vec
2011-08-15 18:38:23 -05:00
if vec::len(alts) > 0u {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
a_post = false_postcond(num_constrs);
The wonky for...in... whitespace was bothering me. Sorry!
2011-08-15 23:54:52 -05:00
for an_alt: arm in alts {
Make typestate properly descend pattern guards Closes #1265
2011-12-07 07:09:45 -06:00
alt an_alt.guard {
some(e) {
changed |= find_pre_post_state_expr(fcx, e_post, e);
}
_ {}
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
changed |=
Rename a field (so that macros can mention it).
2011-08-10 17:38:41 -05:00
find_pre_post_state_block(fcx, e_post, an_alt.body);
intersect(a_post, block_poststate(fcx.ccx, an_alt.body));
Reformat for new syntax
2011-07-27 07:19:39 -05:00
// We deliberately do *not* update changed here, because
// we'd go into an infinite loop that way, and the change
// gets made after the if expression.
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
} else {
// No alts; poststate is the poststate of the test
a_post = e_post;
}
ret changed | set_poststate_ann(fcx.ccx, e.id, a_post);
}
Add type argument field to expr_path This way, you can explicitly provide type parameters when calling a generic method. Issue #1227
2011-12-19 03:21:31 -06:00
expr_field(val, _, _) {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret find_pre_post_state_sub(fcx, pres, val, e.id, none);
}
expr_unary(_, operand) {
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
}
expr_cast(operand, _) {
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
}
expr_fail(maybe_fail_val) {
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
// FIXME Should factor out this code,
// which also appears in find_pre_post_state_exprs
/* if execution continues after fail, then everything is true!
woo! */
let post = false_postcond(num_constrs);
alt fcx.enclosing.cf {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
noreturn. { kill_poststate_(fcx, ninit(fcx.id, fcx.name), post); }
_ { }
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret set_prestate_ann(fcx.ccx, e.id, pres) |
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
set_poststate_ann(fcx.ccx, e.id, post) |
alt maybe_fail_val {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
none. { false }
some(fail_val) {
find_pre_post_state_expr(fcx, pres, fail_val)
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
expr_assert(p) {
ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
}
expr_check(_, p) {
/* predicate p holds after this expression executes */
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));
}
expr_if_check(p, conseq, maybe_alt) {
ret join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check, pres);
}
expr_break. { ret pure_exp(fcx.ccx, e.id, pres); }
expr_cont. { ret pure_exp(fcx.ccx, e.id, pres); }
More work on anonymous objects.
2011-05-20 19:41:36 -05:00
}
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let stmt_ann = stmt_to_ann(fcx.ccx, *s);
Track arguments in typestate Add the infrastructure for arguments -- as well as local vars -- to be deinitialized with move-mode calls. Address Issue #819
2011-08-17 18:58:00 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
/*
Register new snapshots, purge log_err and log_full in favour of log(...).
2011-12-22 19:53:53 -06:00
log(error, ("[" + fcx.name + "]"));
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("*At beginning: stmt = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_stmt_err(*s);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("*prestate = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, stmt_ann.states.prestate);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("*poststate =");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, stmt_ann.states.poststate);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("pres = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, pres);
*/
alt s.node {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
stmt_decl(adecl, id) {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
alt adecl.node {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
decl_local(alocals) {
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
set_prestate(stmt_ann, pres);
Allow omission of the '.' after nullary tag patterns This commit allows patterns like: alt x { some(_) { ... } none { } } without the '.' after none. The parser suspends judgment about whether a bare ident is a tag or a new bound variable; instead, the resolver disambiguates. This means that any code after resolution that pattern-matches on patterns needs to call pat_util::normalize_pat, which consults an environment to do this disambiguation. In addition, local variables are no longer allowed to shadow tag names, so this required changing some code (e.g. renaming variables named "mut", and renaming ast::sub to subtract). The parser currently accepts patterns with and without the '.'. Once the compiler and libraries are changed, it will no longer accept the '.'.
2012-01-14 18:05:07 -06:00
let c_and_p = seq_states(fcx, pres,
locals_to_bindings(fcx.ccx.tcx, alocals));
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
/* important to do this in one step to ensure
termination (don't want to set changed to true
for intermediate changes) */
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
let changed =
set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed;
Initialize all constraints to False 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
2011-08-05 17:23:44 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
/*
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("Summary: stmt = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_stmt_err(*s);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("prestate = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, stmt_ann.states.prestate);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("poststate =");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, stmt_ann.states.poststate);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("changed =");
Register new snapshots, purge log_err and log_full in favour of log(...).
2011-12-22 19:53:53 -06:00
log(error, changed);
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
*/
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
Reformat for new syntax
2011-07-27 07:19:39 -05:00
ret changed;
}
decl_item(an_item) {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
ret set_prestate(stmt_ann, pres) | set_poststate(stmt_ann, pres);
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
/* the outer visitor will recurse into the item */
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
}
}
require a non-semi expr acting as a stmt to have unit return type
2012-01-04 16:16:41 -06:00
stmt_expr(ex, _) | stmt_semi(ex, _) {
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
let changed =
find_pre_post_state_expr(fcx, pres, ex) |
Use single-bar or to make tstate/states.rs prettier Sorry. This is the kind of thing I do when I'm on a plane and too tired to manage anything that requires thinking.
2011-06-25 10:29:50 -05:00
set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) |
set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex));
Initialize all constraints to False 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
2011-08-05 17:23:44 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
/*
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("Finally:");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_stmt_err(*s);
log_err("prestate = ");
log_err(bitv::to_str(stmt_ann.states.prestate));
log_tritv_err(fcx, stmt_ann.states.prestate);
log_err("poststate =");
log_err(bitv::to_str(stmt_ann.states.poststate));
log_tritv_err(fcx, stmt_ann.states.poststate);
log_err("changed =");
*/
Initialize all constraints to False 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
2011-08-05 17:23:44 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
ret changed;
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
_ { ret false; }
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
/* Updates the pre- and post-states of statements in the block,
returns a boolean flag saying whether any pre- or poststates changed */
Reformat for new mode syntax, step 1 Long lines were fixed in a very crude way, as I'll be following up with another reformat in a bit.
2011-09-12 04:27:30 -05:00
fn find_pre_post_state_block(fcx: fn_ctxt, pres0: prestate, b: blk) -> bool {
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* First, set the pre-states and post-states for every expression */
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let pres = pres0;
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* Iterate over each stmt. The new prestate is <pres>. The poststate
consist of improving <pres> with whatever variables this stmt
initializes. Then <pres> becomes the new poststate. */
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let changed = false;
The wonky for...in... whitespace was bothering me. Sorry!
2011-08-15 23:54:52 -05:00
for s: @stmt in b.node.stmts {
Use single-bar or to make tstate/states.rs prettier Sorry. This is the kind of thing I do when I'm on a plane and too tired to manage anything that requires thinking.
2011-06-25 10:29:50 -05:00
changed |= find_pre_post_state_stmt(fcx, pres, s);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
pres = stmt_poststate(fcx.ccx, *s);
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
let post = pres;
alt b.node.expr {
none. { }
some(e) {
changed |= find_pre_post_state_expr(fcx, pres, e);
post = expr_poststate(fcx.ccx, e);
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Restructure the "checking" pass in typestate 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.
2011-06-17 21:07:23 -05:00
Get rid of def_ids and anns in AST nodes, use single node_id 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.
2011-06-19 15:41:21 -05:00
set_prestate_ann(fcx.ccx, b.node.id, pres0);
set_poststate_ann(fcx.ccx, b.node.id, post);
Invalidate constraints correctly after an assignment expression 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.
2011-06-25 00:17:17 -05:00
Refactor typestate code involving stmt_decls 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.
2011-07-29 17:59:38 -05:00
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
/*
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("For block:");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_block_err(b);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("poststate = ");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_states_err(block_states(fcx.ccx, b));
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("pres0:");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, pres0);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("post:");
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
log_tritv_err(fcx, post);
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("changed = ");
Register new snapshots, purge log_err and log_full in favour of log(...).
2011-12-22 19:53:53 -06:00
log(error, changed);
Reformat This changes the indexing syntax from .() to [], the vector syntax from ~[] to [] and the extension syntax from #fmt() to #fmt[]
2011-08-19 17:16:48 -05:00
*/
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
ret changed;
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
fn find_pre_post_state_fn(fcx: fn_ctxt,
f_decl: fn_decl,
f_body: blk) -> bool {
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
let num_constrs = num_constraints(fcx.enclosing);
Initialize all constraints to False 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
2011-08-05 17:23:44 -05:00
// All constraints are considered false until proven otherwise.
// This ensures that intersect works correctly.
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
kill_all_prestate(fcx, f_body.node.id);
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
Track arguments in typestate Add the infrastructure for arguments -- as well as local vars -- to be deinitialized with move-mode calls. Address Issue #819
2011-08-17 18:58:00 -05:00
// Arguments start out initialized
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
let block_pre = block_prestate(fcx.ccx, f_body);
for a: arg in f_decl.inputs {
Track arguments in typestate Add the infrastructure for arguments -- as well as local vars -- to be deinitialized with move-mode calls. Address Issue #819
2011-08-17 18:58:00 -05:00
set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre);
}
// Instantiate any constraints on the arguments so we can use them
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
for c: @constr in f_decl.constraints {
let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c);
Instantiate function preconditions inside the function body so that if we have a function like: f(...) : p(x) { ... } p(x) is true inside the body of f. Closes #694.
2011-07-21 18:03:30 -05:00
set_in_prestate_constr(fcx, tsc, block_pre);
}
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
let changed = find_pre_post_state_block(fcx, block_pre, f_body);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
Get rid of the hack that ignores () typed things in fn tail position. Closes #868. Unfortunately, this causes certain invalid programs to fail type-checking instead of failing type-state when a type-state error message would probably be more intuitive. (Although, by any reasonable interpretation of the static semantics, it technically ought to be a type error.)
2011-08-30 14:45:12 -05:00
// Treat the tail expression as a return statement
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
alt f_body.node.expr {
Reformat for new syntax
2011-07-27 07:19:39 -05:00
some(tailexpr) {
Reformat. Issue #855
2011-09-02 17:34:58 -05:00
Get rid of the hack that ignores () typed things in fn tail position. Closes #868. Unfortunately, this causes certain invalid programs to fail type-checking instead of failing type-state when a type-state error message would probably be more intuitive. (Although, by any reasonable interpretation of the static semantics, it technically ought to be a type error.)
2011-08-30 14:45:12 -05:00
// We don't want to clear the diverges bit for bottom typed things,
// which really do diverge. I feel like there is a cleaner way
// to do this than checking the type.
if !type_is_bot(fcx.ccx.tcx, expr_ty(fcx.ccx.tcx, tailexpr)) {
Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779
2011-08-01 22:55:04 -05:00
let post = false_postcond(num_constrs);
// except for the "diverges" bit...
kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
set_poststate_ann(fcx.ccx, f_body.node.id, post);
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
}
Reformat for new syntax
2011-07-27 07:19:39 -05:00
}
none. {/* fallthrough */ }
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
}
Tests for while loops that may invalidate constraints 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.
2011-06-27 20:12:37 -05:00
Reformat for new syntax
2011-07-27 07:19:39 -05:00
/*
Register snapshots and switch logging over to use of log_full or #error / #debug.
2011-12-22 16:42:52 -06:00
#error("find_pre_post_state_fn");
Register new snapshots, purge log_err and log_full in favour of log(...).
2011-12-22 19:53:53 -06:00
log(error, changed);
Make { || ... } sugar for any type of closure, inferred
2011-12-20 13:03:21 -06:00
fcx.ccx.tcx.sess.span_note(f_body.span, fcx.name);
Reformat for new syntax
2011-07-27 07:19:39 -05:00
*/
Tests for while loops that may invalidate constraints 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.
2011-06-27 20:12:37 -05:00
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
ret changed;
Started adding support for return checking and non-returning function annotations * Reorganized typestate into several modules. * Made typestate check that any function with a non-nil return type returns a value. For now, the check is a warning and not an error (see next item). * Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and fail that don't locally return a value that can be inspected. "bot" is distinct from "nil". There is no concrete syntax for _|_, while the concrete syntax for the nil type is (). * Added support to the parser for a ! annotation on functions whose result type is _|_. Such a function is required to have either a fail or a call to another ! function that is reached in all control flow paths. The point of this annotation is to mark functions like unimpl() and span_err(), so that an alt with a call to err() in one case isn't a false positive for the return-value checker. I haven't actually annotated anything with it yet. * Random bugfixes: * * Fixed bug in trans::trans_binary that was throwing away the cleanups for nested subexpressions of an and or or (tests: box-inside-if and box-inside-if2). ** In typeck, unify the expected type arguments of a tag with the actual specified arguments.
2011-05-14 21:02:30 -05:00
}
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
//
// Local Variables:
// mode: rust
// fill-column: 78;
// indent-tabs-mode: nil
// c-basic-offset: 4
// buffer-file-coding-system: utf-8-unix
// End:
//
Reference in New Issue Copy Permalink