Skip to content

Commit d760b63

Browse files
graydongraydon
committed
---
yaml --- r: 866 b: refs/heads/master c: 7db1158 h: refs/heads/master v: v3
1 parent 6f2bfa0 commit d760b63

File tree

17 files changed

+199
-144
lines changed

17 files changed

+199
-144
lines changed

‎[refs]

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
---
2-
refs/heads/master: da13c508d83032ca13679e1e122e96d25ac23283
2+
refs/heads/master: 7db115834f24eb9d9ccbd2468c9145fdf86be514

‎trunk/src/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,8 @@ BE_MLS := $(addprefix boot/be/, x86.ml ra.ml pe.ml elf.ml \
261261
macho.ml)
262262
IL_MLS := $(addprefix boot/be/, asm.ml il.ml abi.ml)
263263
ME_MLS := $(addprefix boot/me/, walk.ml semant.ml resolve.ml alias.ml \
264-
simplify.ml type.ml dead.ml effect.ml typestate.ml loop.ml \
265-
layout.ml transutil.ml trans.ml dwarf.ml)
264+
simplify.ml type.ml dead.ml stratum.ml effect.ml typestate.ml \
265+
loop.ml layout.ml transutil.ml trans.ml dwarf.ml)
266266
FE_MLS := $(addprefix boot/fe/, ast.ml token.ml lexer.ml parser.ml \
267267
extfmt.ml pexp.ml item.ml cexp.ml fuzz.ml)
268268
DRIVER_TOP_MLS := $(addprefix boot/driver/, lib.ml $(VARIANT)/glue.ml main.ml)

‎trunk/src/boot/driver/llvm/glue.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ let alt_pipeline sess sem_cx crate =
1818
Simplify.process_crate;
1919
Type.process_crate;
2020
Typestate.process_crate;
21+
Stratum.process_crate;
2122
Effect.process_crate;
2223
Loop.process_crate;
2324
Alias.process_crate;

‎trunk/src/boot/driver/main.ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,7 @@ let (sess:Session.sess) =
3737
Session.sess_log_resolve = false;
3838
Session.sess_log_type = false;
3939
Session.sess_log_simplify = false;
40+
Session.sess_log_stratum = false;
4041
Session.sess_log_effect = false;
4142
Session.sess_log_typestate = false;
4243
Session.sess_log_loop = false;
@@ -175,6 +176,8 @@ let argspecs =
175176
"-ltype" "log type checking");
176177
(flag (fun _ -> sess.Session.sess_log_simplify <- true)
177178
"-lsimplify" "log simplification");
179+
(flag (fun _ -> sess.Session.sess_log_stratum <- true)
180+
"-lstratum" "log stratum checking");
178181
(flag (fun _ -> sess.Session.sess_log_effect <- true)
179182
"-leffect" "log effect checking");
180183
(flag (fun _ -> sess.Session.sess_log_typestate <- true)
@@ -378,6 +381,7 @@ let main_pipeline _ =
378381
Simplify.process_crate;
379382
Type.process_crate;
380383
Typestate.process_crate;
384+
Stratum.process_crate;
381385
Effect.process_crate;
382386
Loop.process_crate;
383387
Alias.process_crate;

‎trunk/src/boot/driver/session.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ type sess =
2323
mutable sess_log_resolve: bool;
2424
mutable sess_log_type: bool;
2525
mutable sess_log_simplify: bool;
26+
mutable sess_log_stratum: bool;
2627
mutable sess_log_effect: bool;
2728
mutable sess_log_typestate: bool;
2829
mutable sess_log_dead: bool;

‎trunk/src/boot/me/effect.ml

Lines changed: 34 additions & 93 deletions
Original file line numberDiff line numberDiff line change
@@ -12,78 +12,7 @@ let iflog cx thunk =
1212
else ()
1313
;;
1414

15-
let mutability_checking_visitor
16-
(cx:ctxt)
17-
(inner:Walk.visitor)
18-
: Walk.visitor =
19-
(*
20-
* This visitor enforces the following rules:
21-
*
22-
* - A channel type carrying a mutable type is illegal.
23-
*
24-
* - Writing to an immutable slot is illegal.
25-
*
26-
* - Forming a mutable alias to an immutable slot is illegal.
27-
*
28-
*)
29-
let visit_ty_pre t =
30-
match t with
31-
Ast.TY_chan t' when type_has_state cx t' ->
32-
err None "channel of mutable type: %a " Ast.sprintf_ty t'
33-
| _ -> ()
34-
in
35-
36-
let check_write s dst =
37-
let is_init = Hashtbl.mem cx.ctxt_stmt_is_init s.id in
38-
let dst_ty = lval_ty cx dst in
39-
let is_mutable =
40-
match dst_ty with
41-
Ast.TY_mutable _ -> true
42-
| _ -> false
43-
in
44-
iflog cx
45-
(fun _ -> log cx "checking %swrite to %slval #%d = %a of type %a"
46-
(if is_init then "initializing " else "")
47-
(if is_mutable then "mutable " else "")
48-
(int_of_node (lval_base_id dst))
49-
Ast.sprintf_lval dst
50-
Ast.sprintf_ty dst_ty);
51-
if (is_mutable or is_init)
52-
then ()
53-
else err (Some s.id)
54-
"writing to immutable type %a in statement %a"
55-
Ast.sprintf_ty dst_ty Ast.sprintf_stmt s
56-
in
57-
(* FIXME (issue #75): enforce the no-write-alias-to-immutable-slot
58-
* rule.
59-
*)
60-
let visit_stmt_pre s =
61-
begin
62-
match s.node with
63-
Ast.STMT_copy (lv_dst, _)
64-
| Ast.STMT_call (lv_dst, _, _)
65-
| Ast.STMT_spawn (lv_dst, _, _, _, _)
66-
| Ast.STMT_recv (lv_dst, _)
67-
| Ast.STMT_bind (lv_dst, _, _)
68-
| Ast.STMT_new_rec (lv_dst, _, _)
69-
| Ast.STMT_new_tup (lv_dst, _)
70-
| Ast.STMT_new_vec (lv_dst, _, _)
71-
| Ast.STMT_new_str (lv_dst, _)
72-
| Ast.STMT_new_port lv_dst
73-
| Ast.STMT_new_chan (lv_dst, _)
74-
| Ast.STMT_new_box (lv_dst, _, _) ->
75-
check_write s lv_dst
76-
| _ -> ()
77-
end;
78-
inner.Walk.visit_stmt_pre s
79-
in
80-
81-
{ inner with
82-
Walk.visit_ty_pre = visit_ty_pre;
83-
Walk.visit_stmt_pre = visit_stmt_pre }
84-
;;
85-
86-
let function_effect_propagation_visitor
15+
let effect_calculating_visitor
8716
(item_effect:(node_id, Ast.effect) Hashtbl.t)
8817
(cx:ctxt)
8918
(inner:Walk.visitor)
@@ -93,6 +22,7 @@ let function_effect_propagation_visitor
9322
* its statements:
9423
*
9524
* - Communication statements lower to 'impure'
25+
* - Writing to anything other than a local slot lowers to 'impure'
9626
* - Native calls lower to 'unsafe'
9727
* - Calling a function with effect e lowers to e.
9828
*)
@@ -159,13 +89,27 @@ let function_effect_propagation_visitor
15989
end;
16090
in
16191

92+
let note_write s dst =
93+
(* FIXME (issue #182): this is too aggressive; won't permit writes to
94+
* interior components of records or tuples. It should at least do that,
95+
* possibly handle escape analysis on the pointee for things like vecs as
96+
* well. *)
97+
if lval_base_is_slot cx dst
98+
then
99+
let base_slot = lval_base_slot cx dst in
100+
match dst, base_slot.Ast.slot_mode with
101+
(Ast.LVAL_base _, Ast.MODE_local) -> ()
102+
| _ -> lower_to s Ast.EFF_impure
103+
in
104+
162105
let visit_stmt_pre s =
163106
begin
164107
match s.node with
165108
Ast.STMT_send _
166109
| Ast.STMT_recv _ -> lower_to s Ast.EFF_impure
167110

168-
| Ast.STMT_call (_, fn, _) ->
111+
| Ast.STMT_call (lv_dst, fn, _) ->
112+
note_write s lv_dst;
169113
let lower_to_callee_ty t =
170114
match simplified_ty t with
171115
Ast.TY_fn (_, taux) ->
@@ -185,6 +129,19 @@ let function_effect_propagation_visitor
185129
| Some (REQUIRED_LIB_rust _, _) -> ()
186130
| Some _ -> lower_to s Ast.EFF_unsafe
187131
end
132+
133+
| Ast.STMT_copy (lv_dst, _)
134+
| Ast.STMT_spawn (lv_dst, _, _, _, _)
135+
| Ast.STMT_bind (lv_dst, _, _)
136+
| Ast.STMT_new_rec (lv_dst, _, _)
137+
| Ast.STMT_new_tup (lv_dst, _)
138+
| Ast.STMT_new_vec (lv_dst, _, _)
139+
| Ast.STMT_new_str (lv_dst, _)
140+
| Ast.STMT_new_port lv_dst
141+
| Ast.STMT_new_chan (lv_dst, _)
142+
| Ast.STMT_new_box (lv_dst, _, _) ->
143+
note_write s lv_dst
144+
188145
| _ -> ()
189146
end;
190147
inner.Walk.visit_stmt_pre s
@@ -200,19 +157,6 @@ let function_effect_propagation_visitor
200157
Walk.visit_stmt_pre = visit_stmt_pre }
201158
;;
202159

203-
let binding_effect_propagation_visitor
204-
((*cx*)_:ctxt)
205-
(inner:Walk.visitor)
206-
: Walk.visitor =
207-
(* This visitor lowers the effect of an object or binding according
208-
* to its slots: holding a 'state' slot lowers any obj item, or
209-
* bind-stmt LHS, to 'state'.
210-
*
211-
* Binding (or implicitly just making a native 1st-class) makes the LHS
212-
* unsafe.
213-
*)
214-
inner
215-
;;
216160

217161
let effect_checking_visitor
218162
(item_auth:(node_id, Ast.effect) Hashtbl.t)
@@ -221,7 +165,7 @@ let effect_checking_visitor
221165
(inner:Walk.visitor)
222166
: Walk.visitor =
223167
(*
224-
* This visitor checks that each type, item and obj declares
168+
* This visitor checks that each fn declares
225169
* effects consistent with what we calculated.
226170
*)
227171
let auth_stack = Stack.create () in
@@ -250,7 +194,8 @@ let effect_checking_visitor
250194
end;
251195
begin
252196
match i.node.Ast.decl_item with
253-
Ast.MOD_ITEM_fn f ->
197+
Ast.MOD_ITEM_fn f
198+
when htab_search cx.ctxt_required_items i.id = None ->
254199
let e =
255200
match htab_search item_effect i.id with
256201
None -> Ast.EFF_pure
@@ -319,11 +264,7 @@ let process_crate
319264
let item_effect = Hashtbl.create 0 in
320265
let passes =
321266
[|
322-
(mutability_checking_visitor cx
323-
Walk.empty_visitor);
324-
(function_effect_propagation_visitor item_effect cx
325-
Walk.empty_visitor);
326-
(binding_effect_propagation_visitor cx
267+
(effect_calculating_visitor item_effect cx
327268
Walk.empty_visitor);
328269
(effect_checking_visitor item_auth item_effect cx
329270
Walk.empty_visitor);

‎trunk/src/boot/me/stratum.ml

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
open Semant;;
2+
open Common;;
3+
4+
let log cx = Session.log "stratum"
5+
(should_log cx cx.ctxt_sess.Session.sess_log_stratum)
6+
cx.ctxt_sess.Session.sess_log_out
7+
;;
8+
9+
let iflog cx thunk =
10+
if (should_log cx cx.ctxt_sess.Session.sess_log_stratum)
11+
then thunk ()
12+
else ()
13+
;;
14+
15+
16+
let state_stratum_checking_visitor
17+
(cx:ctxt)
18+
(inner:Walk.visitor)
19+
: Walk.visitor =
20+
(*
21+
* This visitor enforces the following rules:
22+
*
23+
* - A channel type carrying a state type is illegal.
24+
*
25+
* - Writing to an immutable slot is illegal.
26+
*
27+
* - Forming a mutable alias to an immutable slot is illegal.
28+
*
29+
*)
30+
let visit_ty_pre t =
31+
match t with
32+
Ast.TY_chan t' when type_has_state cx t' ->
33+
err None "channel of state type: %a " Ast.sprintf_ty t'
34+
| _ -> ()
35+
in
36+
37+
let check_write s dst =
38+
let is_init = Hashtbl.mem cx.ctxt_stmt_is_init s.id in
39+
let dst_ty = lval_ty cx dst in
40+
let is_mutable =
41+
match dst_ty with
42+
Ast.TY_mutable _ -> true
43+
| _ -> false
44+
in
45+
iflog cx
46+
(fun _ -> log cx "checking %swrite to %slval #%d = %a of type %a"
47+
(if is_init then "initializing " else "")
48+
(if is_mutable then "mutable " else "")
49+
(int_of_node (lval_base_id dst))
50+
Ast.sprintf_lval dst
51+
Ast.sprintf_ty dst_ty);
52+
if (is_mutable or is_init)
53+
then ()
54+
else err (Some s.id)
55+
"writing to immutable type %a in statement %a"
56+
Ast.sprintf_ty dst_ty Ast.sprintf_stmt s
57+
in
58+
(* FIXME (issue #75): enforce the no-write-alias-to-immutable-slot
59+
* rule.
60+
*)
61+
let visit_stmt_pre s =
62+
begin
63+
match s.node with
64+
Ast.STMT_copy (lv_dst, _)
65+
| Ast.STMT_call (lv_dst, _, _)
66+
| Ast.STMT_spawn (lv_dst, _, _, _, _)
67+
| Ast.STMT_recv (lv_dst, _)
68+
| Ast.STMT_bind (lv_dst, _, _)
69+
| Ast.STMT_new_rec (lv_dst, _, _)
70+
| Ast.STMT_new_tup (lv_dst, _)
71+
| Ast.STMT_new_vec (lv_dst, _, _)
72+
| Ast.STMT_new_str (lv_dst, _)
73+
| Ast.STMT_new_port lv_dst
74+
| Ast.STMT_new_chan (lv_dst, _)
75+
| Ast.STMT_new_box (lv_dst, _, _) ->
76+
check_write s lv_dst
77+
| _ -> ()
78+
end;
79+
inner.Walk.visit_stmt_pre s
80+
in
81+
82+
{ inner with
83+
Walk.visit_ty_pre = visit_ty_pre;
84+
Walk.visit_stmt_pre = visit_stmt_pre }
85+
;;
86+
87+
let process_crate
88+
(cx:ctxt)
89+
(crate:Ast.crate)
90+
: unit =
91+
let passes =
92+
[|
93+
(state_stratum_checking_visitor cx
94+
Walk.empty_visitor);
95+
|]
96+
in
97+
run_passes cx "stratum" passes
98+
cx.ctxt_sess.Session.sess_log_stratum log crate
99+
;;
100+
101+
(*
102+
* Local Variables:
103+
* fill-column: 78;
104+
* indent-tabs-mode: nil
105+
* buffer-file-coding-system: utf-8-unix
106+
* compile-command: "make -k -C ../.. 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
107+
* End:
108+
*)

0 commit comments

Comments
 (0)