1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
import syntax::ast;
import ast::{stmt, fn_ident, node_id, crate, return_val, noreturn, expr};
import syntax::{visit, print};
import syntax::codemap::span;
import middle::ty;
import tstate::ann::{precond, prestate,
implies, ann_precond, ann_prestate};
import aux::*;
import syntax::print::pprust::ty_to_str;
import bitvectors::*;
import annotate::annotate_crate;
import collect_locals::mk_f_to_fn_info;
import pre_post_conditions::fn_pre_post;
import states::find_pre_post_state_fn;
import driver::session::session;
import std::map::hashmap;
fn check_unused_vars(fcx: fn_ctxt) {
// FIXME: could be more efficient
for c: norm_constraint in constraints(fcx) {
alt c.c.node {
ninit(id, v) {
if !vec_contains(fcx.enclosing.used_vars, id) && v[0] != '_' as u8
{
fcx.ccx.tcx.sess.span_warn(c.c.span, "unused variable " + v);
}
}
_ {/* ignore pred constraints */ }
}
}
}
fn check_states_expr(e: @expr, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
visit::visit_expr(e, fcx, v);
let prec: precond = expr_precond(fcx.ccx, e);
let pres: prestate = expr_prestate(fcx.ccx, e);
/*
log_err("check_states_expr:");
util::common::log_expr_err(*e);
log_err("prec = ");
log_tritv_err(fcx, prec);
log_err("pres = ");
log_tritv_err(fcx, pres);
*/
if !implies(pres, prec) {
let mut s = "";
let diff = first_difference_string(fcx, prec, pres);
s +=
"unsatisfied precondition constraint (for example, " + diff +
") for expression:\n";
s += syntax::print::pprust::expr_to_str(e);
s += "\nprecondition:\n";
s += tritv_to_str(fcx, prec);
s += "\nprestate:\n";
s += tritv_to_str(fcx, pres);
fcx.ccx.tcx.sess.span_fatal(e.span, s);
}
}
fn check_states_stmt(s: @stmt, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
visit::visit_stmt(s, fcx, v);
let a = stmt_to_ann(fcx.ccx, *s);
let prec: precond = ann_precond(a);
let pres: prestate = ann_prestate(a);
#debug("check_states_stmt:");
log(debug, print::pprust::stmt_to_str(*s));
#debug("prec = ");
log_tritv(fcx, prec);
#debug("pres = ");
log_tritv(fcx, pres);
if !implies(pres, prec) {
let mut ss = "";
let diff = first_difference_string(fcx, prec, pres);
ss +=
"unsatisfied precondition constraint (for example, " + diff +
") for statement:\n";
ss += syntax::print::pprust::stmt_to_str(*s);
ss += "\nprecondition:\n";
ss += tritv_to_str(fcx, prec);
ss += "\nprestate: \n";
ss += tritv_to_str(fcx, pres);
fcx.ccx.tcx.sess.span_fatal(s.span, ss);
}
}
fn check_states_against_conditions(fcx: fn_ctxt,
fk: visit::fn_kind,
f_decl: ast::fn_decl,
f_body: ast::blk,
sp: span,
id: node_id) {
/* Postorder traversal instead of pre is important
because we want the smallest possible erroneous statement
or expression. */
let visitor = visit::mk_vt(
@{visit_stmt: check_states_stmt,
visit_expr: check_states_expr,
visit_fn: bind do_nothing::<fn_ctxt>(_, _, _, _, _, _, _)
with *visit::default_visitor::<fn_ctxt>()});
visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor);
/* Check that the return value is initialized */
let post = aux::block_poststate(fcx.ccx, f_body);
let is_ctor = alt fk { visit::fk_ctor(_,_) { true } _ { false } };
if !is_ctor && !promises(fcx, post, fcx.enclosing.i_return) &&
!ty::type_is_nil(ty::ty_fn_ret(ty::node_id_to_type(
fcx.ccx.tcx, id))) &&
f_decl.cf == return_val {
fcx.ccx.tcx.sess.span_err(f_body.span,
"in function " + fcx.name +
", not all control paths \
return a value");
fcx.ccx.tcx.sess.span_fatal(f_decl.output.span,
"see declared return type of '" +
ty_to_str(f_decl.output) + "'");
} else if f_decl.cf == noreturn {
// check that this really always fails
// Note that it's ok for i_diverge and i_return to both be true.
// In fact, i_diverge implies i_return. (But not vice versa!)
if !promises(fcx, post, fcx.enclosing.i_diverge) {
fcx.ccx.tcx.sess.span_fatal(f_body.span,
"in non-returning function " +
fcx.name +
", some control paths may \
return to the caller");
}
}
/* Finally, check for unused variables */
check_unused_vars(fcx);
}
fn check_fn_states(fcx: fn_ctxt,
fk: visit::fn_kind,
f_decl: ast::fn_decl,
f_body: ast::blk,
sp: span,
id: node_id) {
/* Compute the pre- and post-states for this function */
// Fixpoint iteration
while find_pre_post_state_fn(fcx, f_decl, f_body) { }
/* Now compare each expr's pre-state to its precondition
and post-state to its postcondition */
check_states_against_conditions(fcx, fk, f_decl, f_body, sp, id);
}
fn fn_states(fk: visit::fn_kind, f_decl: ast::fn_decl, f_body: ast::blk,
sp: span, id: node_id,
ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
visit::visit_fn(fk, f_decl, f_body, sp, id, ccx, v);
/* Look up the var-to-bit-num map for this function */
assert (ccx.fm.contains_key(id));
let f_info = ccx.fm.get(id);
let name = visit::name_of_fn(fk);
let fcx = {enclosing: f_info, id: id, name: name, ccx: ccx};
check_fn_states(fcx, fk, f_decl, f_body, sp, id)
}
fn check_crate(cx: ty::ctxt, crate: @crate) {
let ccx: crate_ctxt = new_crate_ctxt(cx);
/* Build the global map from function id to var-to-bit-num-map */
mk_f_to_fn_info(ccx, crate);
/* Add a blank ts_ann for every statement (and expression) */
annotate_crate(ccx, *crate);
/* Compute the pre and postcondition for every subexpression */
let vtor = visit::default_visitor::<crate_ctxt>();
let vtor = @{visit_fn: fn_pre_post with *vtor};
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
/* Check the pre- and postcondition against the pre- and poststate
for every expression */
let vtor = visit::default_visitor::<crate_ctxt>();
let vtor = @{visit_fn: fn_states with *vtor};
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
}
//
// Local Variables:
// mode: rust
// fill-column: 78;
// indent-tabs-mode: nil
// c-basic-offset: 4
// buffer-file-coding-system: utf-8-unix
// End:
//
|
