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
|
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 util::ppaux::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 syntax::print::pprust::expr_to_str;
import driver::session::session;
import std::map::hashmap;
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);
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: |a,b,c,d,e,f,g| {
do_nothing::<fn_ctxt>(a, b, c, d, e, f, g)
}
with *visit::default_visitor::<fn_ctxt>()});
visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor);
}
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);
// We may not care about typestate for this function if it contains
// no constrained calls
if !ccx.fm.get(id).ignore {
/* Look up the var-to-bit-num map for this function */
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:
//
|
