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

761 lines
28 KiB
Rust
Raw Normal View History

Finally rename std::_xxx to std::xxx Except for _task, which is still a keyword.
2011-05-17 13:41:41 -05:00
import std::vec;
import std::vec::plus_option;
import std::vec::cat_options;
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
import std::option;
import std::option::get;
import std::option::is_none;
import std::option::none;
import std::option::some;
import std::option::maybe;
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
import tstate::ann::set_in_poststate_;
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
import tstate::ann::pre_and_post;
import tstate::ann::get_post;
import tstate::ann::postcond;
import tstate::ann::empty_pre_post;
import tstate::ann::empty_poststate;
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
import tstate::ann::clear_in_poststate;
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
import tstate::ann::intersect;
import tstate::ann::empty_prestate;
import tstate::ann::prestate;
import tstate::ann::poststate;
import tstate::ann::false_postcond;
import tstate::ann::ts_ann;
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
import tstate::ann::set_prestate;
import tstate::ann::set_poststate;
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
import aux::crate_ctxt;
import aux::fn_ctxt;
Redo typestate-related data structures to support predicate constraints. No actual support yet, just infrastructure.
2011-06-01 20:10:10 -05:00
import aux::num_constraints;
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
import aux::expr_pp;
import aux::stmt_pp;
import aux::block_pp;
import aux::set_pre_and_post;
import aux::expr_prestate;
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
import aux::expr_precond;
import aux::expr_postcond;
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
import aux::stmt_poststate;
import aux::expr_poststate;
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
import aux::block_prestate;
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
import aux::block_poststate;
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
import aux::block_precond;
import aux::block_postcond;
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
import aux::fn_info;
import aux::log_pp;
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
import aux::log_pp_err;
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
import aux::extend_prestate_ann;
import aux::extend_poststate_ann;
import aux::set_prestate_ann;
import aux::set_poststate_ann;
import aux::pure_exp;
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
import aux::log_tritv;
import aux::log_tritv_err;
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
import aux::stmt_to_ann;
import aux::log_states;
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
import aux::log_states_err;
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
import aux::block_states;
import aux::controlflow_expr;
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
import aux::node_id_to_def;
Start to check expr_check and expr_call constraints in typestate Start writing the cases for expr_check and expr_call to take predicates into account, but this isn't working yet.
2011-06-09 11:56:35 -05:00
import aux::expr_to_constr;
Refactor some typestate-related data structures
2011-06-13 20:10:33 -05:00
import aux::ninit;
import aux::npred;
import aux::path_to_ident;
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
import aux::if_ty;
import aux::if_check;
import aux::plain_if;
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
import aux::forget_in_poststate;
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
import aux::forget_in_poststate_still_init;
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
import tritv::tritv_clone;
import tritv::tritv_set;
import tritv::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
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
import bitvectors::set_in_poststate_ident;
import bitvectors::clear_in_poststate_expr;
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
import bitvectors::clear_in_prestate_ident;
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
import bitvectors::bit_num;
import bitvectors::gen_poststate;
Correctly check that ! functions always diverge Also make _|_ unify with any type.
2011-05-20 21:50:29 -05:00
import bitvectors::kill_poststate;
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
import bitvectors::clear_in_poststate_ident;
import bitvectors::intersect_states;
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
import front::ast;
Now imports are not re-exported unless 'export' is explicitly used.
2011-05-31 20:24:06 -05:00
import front::ast::*;
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
import middle::ty::expr_ty;
import middle::ty::type_is_nil;
import middle::ty::type_is_bot;
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
import util::common::new_def_hash;
import util::common::uistr;
import util::common::log_expr;
import util::common::log_block;
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
import util::common::log_block_err;
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
import util::common::log_fn;
import util::common::elt_exprs;
import util::common::field_exprs;
import util::common::has_nonlocal_exits;
import util::common::log_stmt;
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
import util::common::log_stmt_err;
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
import util::common::log_expr_err;
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
// Used to communicate which operands should be invalidated
// to helper functions
tag oper_type {
oper_move;
oper_swap;
oper_assign;
oper_pure;
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs) ->
tup(bool, poststate) {
auto changed = false;
auto post = pres;
for (@expr e in exprs) {
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_expr(fcx, post, e) || 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
// log_err("Seq_states: changed =");
// log_err changed;
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
post = expr_poststate(fcx.ccx, e);
}
ret tup(changed, 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
}
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
fn find_pre_post_state_sub(&fn_ctxt fcx, &prestate pres, &@expr e,
node_id parent, option::t[aux::constr_] c)
-> bool {
auto changed = find_pre_post_state_expr(fcx, pres, e);
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
auto post = tritv_clone(expr_poststate(fcx.ccx, e));
alt (c) {
case (none) {}
case (some(?c1)) {
set_in_poststate_(bit_num(fcx, c1), post);
}
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
fn find_pre_post_state_two(&fn_ctxt fcx, &prestate pres, &@expr a, &@expr b,
node_id parent, oper_type op) -> bool {
auto changed = set_prestate_ann(fcx.ccx, parent, pres);
changed = find_pre_post_state_expr(fcx, pres, a) || changed;
changed = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, a), b)
|| changed;
// for termination, need to make sure intermediate changes don't set
// changed flag
auto post = tritv_clone(expr_poststate(fcx.ccx, b));
alt (op) {
case (oper_move) {
forget_in_poststate(fcx, post, b.id);
gen_if_local(fcx, post, a);
}
case (oper_swap) {
forget_in_poststate_still_init(fcx, post, a.id);
forget_in_poststate_still_init(fcx, post, b.id);
}
case (oper_assign) {
forget_in_poststate_still_init(fcx, post, a.id);
gen_if_local(fcx, post, a);
}
case (_) {}
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
fn find_pre_post_state_call(&fn_ctxt fcx, &prestate pres, &@expr a,
node_id id, &vec[@expr] bs,
controlflow cf) -> bool {
auto changed = find_pre_post_state_expr(fcx, pres, a);
ret find_pre_post_state_exprs(fcx,
expr_poststate(fcx.ccx, a), id, bs, cf) || changed;
}
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
fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, ast::node_id id,
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
&vec[@expr] es, controlflow cf) -> bool {
Remove variable name 'res' from test suite
2011-06-25 10:45:49 -05:00
auto rs = seq_states(fcx, pres, es);
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
auto changed = rs._0 | 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 */
alt (cf) {
case (noreturn) {
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 |= set_poststate_ann
(fcx.ccx, id, false_postcond(num_constraints(fcx.enclosing)));
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
}
case (_) {
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 |= set_poststate_ann(fcx.ccx, id, rs._1);
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;
}
Change decl to local in expr_for and expr_for_each Since the decl in a for or for-each loop must always be a local decl, I changed the AST to express this. Fewer potential match failures and "the impossible happened" error messages = yay!
2011-06-13 19:04:15 -05:00
fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
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
&@expr index, &block body, node_id id) -> bool {
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
auto 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
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
auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
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
find_pre_post_state_expr(fcx, pres, index);
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), 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
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]
ret (changed | set_poststate_ann(fcx.ccx, id, pres));
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
}
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
else {
auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body));
/*
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
auto res_p =
intersect_postconds([expr_poststate(fcx.ccx, index),
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
block_poststate(fcx.ccx, body)]); */
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
}
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
fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool {
alt (e.node) {
case (expr_path(?pth)) {
alt (node_id_to_def(fcx.ccx, e.id)) {
case (some(def_local(?loc))) {
ret set_in_poststate_ident(fcx, loc._1,
path_to_ident(fcx.ccx.tcx, pth), p);
}
case (_) { ret false; }
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -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
case (_) { 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
}
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
fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
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
&option::t[@expr] maybe_alt, ast::node_id id, &if_ty chk,
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
&prestate pres) -> bool {
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
auto changed = set_prestate_ann(fcx.ccx, id, pres) |
find_pre_post_state_expr(fcx, pres, antec);
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));
*/
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
alt (maybe_alt) {
case (none) {
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_block
(fcx, expr_poststate(fcx.ccx, antec), conseq) |
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
set_poststate_ann(fcx.ccx, id,
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
expr_poststate(fcx.ccx, antec));
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
}
case (some(?altern)) {
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_expr
(fcx, expr_poststate(fcx.ccx, antec), altern);
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
auto conseq_prestate = expr_poststate(fcx.ccx, antec);
alt (chk) {
case (if_check) {
let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
conseq_prestate = tritv_clone(conseq_prestate);
tritv_set(bit_num(fcx, c.node), conseq_prestate, 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
}
case (_) {}
}
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_block(fcx, conseq_prestate, conseq);
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
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
auto poststate_res =
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
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));
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
fcx.ccx.tcx.sess.span_note(antec.span,
"altern poststate = " +
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
aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
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
fcx.ccx.tcx.sess.span_note(antec.span,
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
"conseq poststate = " + aux::tritv_to_str(fcx,
block_poststate(fcx.ccx, conseq)));
*/
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
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 |= 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;
}
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
fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
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
auto num_constrs = num_constraints(fcx.enclosing);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
alt (e.node) {
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_vec(?elts, _, _)) {
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_exprs(fcx, pres, e.id, elts, return);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_tup(?elts)) {
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_exprs(fcx, pres, e.id,
elt_exprs(elts), return);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_call(?operator, ?operands)) {
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
ret find_pre_post_state_call
(fcx, pres, operator, e.id, operands,
controlflow_expr(fcx.ccx, operator));
Insert plumbing for move that behaves just like assign.
2011-05-27 19:38:52 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_spawn(_, _, ?operator, ?operands)) {
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_call(fcx, pres, operator, e.id, operands,
return);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_bind(?operator, ?maybe_args)) {
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_call(fcx, pres, operator, e.id,
cat_options(maybe_args), return);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_path(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
case (expr_log(_, ?ex)) {
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_sub(fcx, pres, ex, e.id, none);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_chan(?ex)) {
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_sub(fcx, pres, ex, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_ext(_, _, _, ?expanded)) {
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_sub(fcx, pres, expanded, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_put(?maybe_e)) {
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
alt (maybe_e) {
case (some(?arg)) {
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_sub(fcx, pres, arg, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (none) { ret pure_exp(fcx.ccx, e.id, pres); }
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_lit(?l)) { ret pure_exp(fcx.ccx, e.id, pres); }
case (expr_fn(?f)) { ret pure_exp(fcx.ccx, e.id, pres); }
case (expr_block(?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
ret find_pre_post_state_block(fcx, pres, b) |
set_prestate_ann(fcx.ccx, e.id, pres) |
set_poststate_ann(fcx.ccx, e.id, block_poststate(fcx.ccx, b));
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_rec(?fields, ?maybe_base)) {
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
auto changed = find_pre_post_state_exprs
(fcx, pres, e.id, field_exprs(fields), return);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
alt (maybe_base) {
case (none) {/* do nothing */ }
case (some(?base)) {
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_expr(fcx, pres, base) |
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, base));
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 source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
ret changed;
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_move(?lhs, ?rhs)) {
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, lhs, rhs,
e.id, oper_move);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_assign(?lhs, ?rhs)) {
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, lhs, rhs,
e.id, oper_assign);
Correctly check that ! functions always diverge Also make _|_ unify with any type.
2011-05-20 21:50:29 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_swap(?lhs, ?rhs)) {
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, lhs, rhs, e.id,
oper_swap);
// Could be more precise and actually swap the role of
// lhs and rhs in constraints
Reformat a bunch of recent churn.
2011-06-16 18:55:46 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_recv(?lhs, ?rhs)) {
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
// Opposite order as most other binary operations,
// so not using find_pre_post_state_two
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
auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
find_pre_post_state_expr(fcx, pres, lhs) |
find_pre_post_state_expr
(fcx, expr_poststate(fcx.ccx, lhs), rhs);
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
auto post = tritv_clone(expr_poststate(fcx.ccx, rhs));
forget_in_poststate_still_init(fcx, post, rhs.id);
gen_if_local(fcx, post, rhs);
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
ret changed | set_poststate_ann(fcx.ccx, e.id, 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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_ret(?maybe_ret_val)) {
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
auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* normally, everything is true if execution continues after
a ret expression (since execution never continues locally
after a ret expression */
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
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* return from an always-failing function clears the return bit */
alt (fcx.enclosing.cf) {
case (noreturn) {
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
kill_poststate(fcx, e.id, rec(id=fcx.id,
c=ninit(fcx.name)));
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
case (_) { }
}
alt (maybe_ret_val) {
case (none) {/* do nothing */ }
case (some(?ret_val)) {
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_expr(fcx, pres, ret_val);
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 source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
ret changed;
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_be(?val)) {
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
auto changed = set_prestate_ann(fcx.ccx, e.id, 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
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
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
ret changed | find_pre_post_state_expr(fcx, pres, val);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_if(?antec, ?conseq, ?maybe_alt)) {
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
ret join_then_else
(fcx, antec, conseq, maybe_alt, e.id, plain_if, pres);
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
}
rustc: Add ternary operator. Closes #565 The implementation is so simple it might be considered cheating: at almost every step the expr_ternary is just converted to expr_if.
2011-06-23 17:15:50 -05:00
case (expr_ternary(_, _, _)) {
ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_binary(?bop, ?l, ?r)) {
Handle lazy binops properly in typestate The typestate analysis now reflects that the second operand of a logical and or or may not be evaluated.
2011-06-28 15:07:05 -05:00
if (lazy_binop(bop)) {
auto 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 {
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_send(?l, ?r)) {
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_assign_op(?op, ?lhs, ?rhs)) {
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, lhs, rhs, e.id,
oper_assign);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_while(?test, ?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
/*
log_err "in a while loop:";
log_expr_err(*e);
aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body));
aux::log_tritv_err(fcx, pres);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -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
auto loop_pres = intersect_states
(block_poststate(fcx.ccx, body), pres);
// aux::log_tritv_err(fcx, loop_pres);
// log_err "---------------";
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres) |
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);
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
/* conservative approximation: if a loop contains a break
or cont, we assume nothing about the poststate */
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
/* which is still unsound -- see [Break-unsound] */
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
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
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
}
else {
auto e_post = expr_poststate(fcx.ccx, test);
auto b_post = block_poststate(fcx.ccx, body);
ret changed | set_poststate_ann
(fcx.ccx, e.id, intersect_states(e_post, b_post));
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
}
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_do_while(?body, ?test)) {
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
auto loop_pres = intersect_states(expr_poststate(fcx.ccx, test),
pres);
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
changed |= find_pre_post_state_block(fcx, loop_pres, body);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* 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) */
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_expr
(fcx, block_poststate(fcx.ccx, body), test);
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
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
auto breaks = has_nonlocal_exits(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
if (breaks) {
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
// 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);
}
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
else {
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 |= set_poststate_ann
(fcx.ccx, e.id, expr_poststate(fcx.ccx, test));
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
ret changed;
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_for(?d, ?index, ?body)) {
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_for_each(?d, ?index, ?body)) {
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_index(?val, ?sub)) {
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, val, sub, e.id, oper_pure);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_alt(?val, ?alts)) {
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
auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
find_pre_post_state_expr(fcx, pres, val);
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
auto e_post = expr_poststate(fcx.ccx, val);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
auto a_post;
Handle lazy binops properly in typestate The typestate analysis now reflects that the second operand of a logical and or or may not be evaluated.
2011-06-28 15:07:05 -05:00
if (vec::len(alts) > 0u) {
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
a_post = false_postcond(num_constrs);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
for (arm an_alt in alts) {
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_block
(fcx, e_post, an_alt.block);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
intersect(a_post, block_poststate(fcx.ccx, an_alt.block));
// 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.
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
}
} else {
// No alts; poststate is the poststate of the test
a_post = e_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
}
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
ret changed | set_poststate_ann(fcx.ccx, e.id, a_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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_field(?val, _)) {
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_sub(fcx, pres, val, e.id, none);
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_unary(_, ?operand)) {
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_sub(fcx, pres, operand, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_cast(?operand, _)) {
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_sub(fcx, pres, operand, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Allow any string expression to be used with fail.
2011-07-01 13:33:15 -05:00
case (expr_fail(?maybe_fail_val)) {
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
ret set_prestate_ann(fcx.ccx, e.id, pres) |
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* if execution continues after fail, then everything is true!
woo! */
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_poststate_ann(fcx.ccx, e.id,
Allow any string expression to be used with fail.
2011-07-01 13:33:15 -05:00
false_postcond(num_constrs)) |
alt(maybe_fail_val) {
case (none) { false }
case (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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_assert(?p)) {
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_sub(fcx, pres, p, e.id, none);
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
}
Implement "claim" Implement "claim" (issue #14), which is a version of "check" that doesn't really do the check at runtime. It's an unsafe feature. The new flag --check-claims turns claims into checks automatically -- but it's off by default, so by default, the assertion in a claim doesn't execute at runtime.
2011-06-28 18:29:37 -05:00
case (expr_check(_, ?p)) {
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
/* predicate p holds after this expression executes */
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
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
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));
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
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_if_check(?p, ?conseq, ?maybe_alt)) {
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
ret join_then_else
(fcx, p, conseq, maybe_alt, e.id, if_check, pres);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_break) { ret pure_exp(fcx.ccx, e.id, pres); }
case (expr_cont) { ret pure_exp(fcx.ccx, e.id, pres); }
Teach the parser and typechecker to understand port[int](). Closes #588
2011-06-28 17:54:16 -05:00
case (expr_port(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (expr_self_method(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
case (expr_anon_obj(?anon_obj, _, _)) {
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
alt (anon_obj.with_obj) {
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (some(?wt)) {
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_sub(fcx, pres, wt, e.id, none);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (none) { 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
}
fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
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
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
/*
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 "*At beginning: stmt = ";
log_stmt_err(*s);
log_err "*prestate = ";
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
log_err tritv::to_str(stmt_ann.states.prestate);
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 "*poststate =";
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
log_err tritv::to_str(stmt_ann.states.poststate);
log_err "pres = ";
log_err tritv::to_str(pres);
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
*/
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
alt (s.node) {
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
case (stmt_decl(?adecl, ?id)) {
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
alt (adecl.node) {
case (decl_local(?alocal)) {
Consistify ast::local.
2011-06-16 17:58:25 -05:00
alt (alocal.node.init) {
rustc: Remove unneeded type params from alt patterns
2011-05-30 23:39:19 -05:00
case (some(?an_init)) {
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
auto changed = set_prestate(stmt_ann, pres) |
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
find_pre_post_state_expr(fcx, pres,
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
an_init.expr);
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -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
auto post = tritv_clone(expr_poststate(fcx.ccx,
an_init.expr));
Allow moving out of temporary values This will probably need more work, as moving doesn't appear to do quite the right thing yet in general, and we should also check somewhere that we're not, for example, moving out the content out of an immutable field (probably moving out of fields is not okay in general).
2011-06-25 05:16:48 -05:00
if (an_init.op == init_move) {
clear_in_poststate_expr(fcx, an_init.expr,
post);
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -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
set_in_poststate_ident(fcx, alocal.node.id,
alocal.node.ident, post);
/* important to do this in one step to ensure
termination (don't want to set changed to true
for intermediate changes) */
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
ret changed | set_poststate(stmt_ann, 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
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
/*
log_err "Summary: stmt = ";
log_stmt_err(*s);
log_err "prestate = ";
log_tritv_err(fcx, stmt_ann.states.prestate);
log_err "poststate =";
log_tritv_err(fcx, stmt_ann.states.poststate);
log_err "changed =";
log_err changed;
*/
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
}
rustc: Remove unneeded type params from alt patterns
2011-05-30 23:39:19 -05:00
case (none) {
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
// let int = x; => x is uninit in poststate
set_poststate_ann(fcx.ccx, id, pres);
clear_in_poststate_ident(fcx, alocal.node.id,
Re-enable tidy (it was broken) and fix various non-tidy things.
2011-06-29 17:11:20 -05:00
alocal.node.ident, id);
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
set_prestate(stmt_ann, pres);
ret false;
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
}
}
}
case (decl_item(?an_item)) {
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
ret set_prestate(stmt_ann, pres) |
set_poststate(stmt_ann, pres);
Eliminate explicit recursion in tstate.states (walk does that now), and kill dead code.
2011-05-18 20:03:48 -05:00
/* the outer "walk" will recurse into the item */
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
}
}
Move expr ids into the expr record type This simplifies the tag variants a bit and makes expr_node_id obsolete.
2011-06-21 15:16:40 -05:00
case (stmt_expr(?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
ret find_pre_post_state_expr(fcx, pres, ex) |
set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) |
set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex));
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -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
log_err "Finally:";
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -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 =");
log_err(changed);
Rewrite tstate.annotate to use walk instead of fold and various other tidying in typestate
2011-05-18 17:43:05 -05:00
*/
}
case (_) { 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 */
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
fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
-> 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 */
auto pres = pres0;
/* 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. */
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
auto changed = false;
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
for (@stmt s 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 source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
auto post = pres;
alt (b.node.expr) {
case (none) { }
case (some(?e)) {
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_expr(fcx, pres, e);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
post = expr_poststate(fcx.ccx, e);
}
}
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
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
log_err "For block:";
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
log_block_err(b);
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 "poststate = ";
log_states_err(block_states(fcx.ccx, b));
log_err "pres0:";
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
log_tritv_err(fcx, pres0);
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 "post:";
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
log_tritv_err(fcx, post);
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
}
fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
Redo typestate-related data structures to support predicate constraints. No actual support yet, just infrastructure.
2011-06-01 20:10:10 -05:00
auto num_local_vars = num_constraints(fcx.enclosing);
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
// make sure the return bit starts out False
clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
auto changed =
Compute typestate properly for move typestate now drops constraints correctly in the post-state of a move expression or a declaration whose op is a move. It doesn't yet drop constraints mentioning variables that get updated. To do this, I had to change typestate to use trit-vectors instead of bit-vectors, because for every constraint, there are three possible values: known-to-be-false (e.g. after x <- y, init(y) is known-to-be-false), known-to-be-true, and unknown. Before, we conflated known-to-be-false with unknown. But move requires them to be treated differently. Consider: (program a) (a1) x = 1; (a2) y <- x; (a3) log x; (program b) (b1) x = 1; (b2) y <- z; (b3) log x; With only two values, the postcondition of statement a2 for constraint init(x) is the same as that of b2: 0. But in (a2)'s postcondition, init(x) *must* be false, but in (b2)'s condition, it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
f.body);
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
// Treat the tail expression as a return statement
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
alt (f.body.node.expr) {
case (some(?tailexpr)) {
auto tailty = expr_ty(fcx.ccx.tcx, tailexpr);
// Since blocks and alts and ifs that don't have results
// implicitly result in nil, we have to be careful to not
// interpret nil-typed block results as the result of a
// function with some other return type
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
if (!type_is_nil(fcx.ccx.tcx, tailty) &&
!type_is_bot(fcx.ccx.tcx, tailty)) {
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
auto p = false_postcond(num_local_vars);
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_poststate_ann(fcx.ccx, f.body.node.id, p);
rustc: Teach rustc to use block results as fn return values. Closes #372
2011-05-31 14:24:18 -05:00
}
}
Reformat source tree (minus a couple tests that are still grumpy).
2011-06-15 13:19:50 -05:00
case (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
/*
log_err "find_pre_post_state_fn";
log_err changed;
fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name);
*/
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
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
// End:
//
Reference in New Issue Copy Permalink