aboutsummaryrefslogtreecommitdiff
path: root/src/boot
diff options
context:
space:
mode:
Diffstat (limited to 'src/boot')
-rw-r--r--src/boot/driver/llvm/glue.ml1
-rw-r--r--src/boot/driver/main.ml4
-rw-r--r--src/boot/driver/session.ml1
-rw-r--r--src/boot/me/effect.ml127
-rw-r--r--src/boot/me/stratum.ml108
5 files changed, 148 insertions, 93 deletions
diff --git a/src/boot/driver/llvm/glue.ml b/src/boot/driver/llvm/glue.ml
index 03baf04d..da5e5b9d 100644
--- a/src/boot/driver/llvm/glue.ml
+++ b/src/boot/driver/llvm/glue.ml
@@ -18,6 +18,7 @@ let alt_pipeline sess sem_cx crate =
Simplify.process_crate;
Type.process_crate;
Typestate.process_crate;
+ Stratum.process_crate;
Effect.process_crate;
Loop.process_crate;
Alias.process_crate;
diff --git a/src/boot/driver/main.ml b/src/boot/driver/main.ml
index b37f5d93..30310b10 100644
--- a/src/boot/driver/main.ml
+++ b/src/boot/driver/main.ml
@@ -37,6 +37,7 @@ let (sess:Session.sess) =
Session.sess_log_resolve = false;
Session.sess_log_type = false;
Session.sess_log_simplify = false;
+ Session.sess_log_stratum = false;
Session.sess_log_effect = false;
Session.sess_log_typestate = false;
Session.sess_log_loop = false;
@@ -175,6 +176,8 @@ let argspecs =
"-ltype" "log type checking");
(flag (fun _ -> sess.Session.sess_log_simplify <- true)
"-lsimplify" "log simplification");
+ (flag (fun _ -> sess.Session.sess_log_stratum <- true)
+ "-lstratum" "log stratum checking");
(flag (fun _ -> sess.Session.sess_log_effect <- true)
"-leffect" "log effect checking");
(flag (fun _ -> sess.Session.sess_log_typestate <- true)
@@ -378,6 +381,7 @@ let main_pipeline _ =
Simplify.process_crate;
Type.process_crate;
Typestate.process_crate;
+ Stratum.process_crate;
Effect.process_crate;
Loop.process_crate;
Alias.process_crate;
diff --git a/src/boot/driver/session.ml b/src/boot/driver/session.ml
index 39848982..49242ac6 100644
--- a/src/boot/driver/session.ml
+++ b/src/boot/driver/session.ml
@@ -23,6 +23,7 @@ type sess =
mutable sess_log_resolve: bool;
mutable sess_log_type: bool;
mutable sess_log_simplify: bool;
+ mutable sess_log_stratum: bool;
mutable sess_log_effect: bool;
mutable sess_log_typestate: bool;
mutable sess_log_dead: bool;
diff --git a/src/boot/me/effect.ml b/src/boot/me/effect.ml
index 3bb761ef..238e3e5b 100644
--- a/src/boot/me/effect.ml
+++ b/src/boot/me/effect.ml
@@ -12,78 +12,7 @@ let iflog cx thunk =
else ()
;;
-let mutability_checking_visitor
- (cx:ctxt)
- (inner:Walk.visitor)
- : Walk.visitor =
- (*
- * This visitor enforces the following rules:
- *
- * - A channel type carrying a mutable type is illegal.
- *
- * - Writing to an immutable slot is illegal.
- *
- * - Forming a mutable alias to an immutable slot is illegal.
- *
- *)
- let visit_ty_pre t =
- match t with
- Ast.TY_chan t' when type_has_state cx t' ->
- err None "channel of mutable type: %a " Ast.sprintf_ty t'
- | _ -> ()
- in
-
- let check_write s dst =
- let is_init = Hashtbl.mem cx.ctxt_stmt_is_init s.id in
- let dst_ty = lval_ty cx dst in
- let is_mutable =
- match dst_ty with
- Ast.TY_mutable _ -> true
- | _ -> false
- in
- iflog cx
- (fun _ -> log cx "checking %swrite to %slval #%d = %a of type %a"
- (if is_init then "initializing " else "")
- (if is_mutable then "mutable " else "")
- (int_of_node (lval_base_id dst))
- Ast.sprintf_lval dst
- Ast.sprintf_ty dst_ty);
- if (is_mutable or is_init)
- then ()
- else err (Some s.id)
- "writing to immutable type %a in statement %a"
- Ast.sprintf_ty dst_ty Ast.sprintf_stmt s
- in
- (* FIXME (issue #75): enforce the no-write-alias-to-immutable-slot
- * rule.
- *)
- let visit_stmt_pre s =
- begin
- match s.node with
- Ast.STMT_copy (lv_dst, _)
- | Ast.STMT_call (lv_dst, _, _)
- | Ast.STMT_spawn (lv_dst, _, _, _, _)
- | Ast.STMT_recv (lv_dst, _)
- | Ast.STMT_bind (lv_dst, _, _)
- | Ast.STMT_new_rec (lv_dst, _, _)
- | Ast.STMT_new_tup (lv_dst, _)
- | Ast.STMT_new_vec (lv_dst, _, _)
- | Ast.STMT_new_str (lv_dst, _)
- | Ast.STMT_new_port lv_dst
- | Ast.STMT_new_chan (lv_dst, _)
- | Ast.STMT_new_box (lv_dst, _, _) ->
- check_write s lv_dst
- | _ -> ()
- end;
- inner.Walk.visit_stmt_pre s
- in
-
- { inner with
- Walk.visit_ty_pre = visit_ty_pre;
- Walk.visit_stmt_pre = visit_stmt_pre }
-;;
-
-let function_effect_propagation_visitor
+let effect_calculating_visitor
(item_effect:(node_id, Ast.effect) Hashtbl.t)
(cx:ctxt)
(inner:Walk.visitor)
@@ -93,6 +22,7 @@ let function_effect_propagation_visitor
* its statements:
*
* - Communication statements lower to 'impure'
+ * - Writing to anything other than a local slot lowers to 'impure'
* - Native calls lower to 'unsafe'
* - Calling a function with effect e lowers to e.
*)
@@ -159,13 +89,27 @@ let function_effect_propagation_visitor
end;
in
+ let note_write s dst =
+ (* FIXME (issue #182): this is too aggressive; won't permit writes to
+ * interior components of records or tuples. It should at least do that,
+ * possibly handle escape analysis on the pointee for things like vecs as
+ * well. *)
+ if lval_base_is_slot cx dst
+ then
+ let base_slot = lval_base_slot cx dst in
+ match dst, base_slot.Ast.slot_mode with
+ (Ast.LVAL_base _, Ast.MODE_local) -> ()
+ | _ -> lower_to s Ast.EFF_impure
+ in
+
let visit_stmt_pre s =
begin
match s.node with
Ast.STMT_send _
| Ast.STMT_recv _ -> lower_to s Ast.EFF_impure
- | Ast.STMT_call (_, fn, _) ->
+ | Ast.STMT_call (lv_dst, fn, _) ->
+ note_write s lv_dst;
let lower_to_callee_ty t =
match simplified_ty t with
Ast.TY_fn (_, taux) ->
@@ -185,6 +129,19 @@ let function_effect_propagation_visitor
| Some (REQUIRED_LIB_rust _, _) -> ()
| Some _ -> lower_to s Ast.EFF_unsafe
end
+
+ | Ast.STMT_copy (lv_dst, _)
+ | Ast.STMT_spawn (lv_dst, _, _, _, _)
+ | Ast.STMT_bind (lv_dst, _, _)
+ | Ast.STMT_new_rec (lv_dst, _, _)
+ | Ast.STMT_new_tup (lv_dst, _)
+ | Ast.STMT_new_vec (lv_dst, _, _)
+ | Ast.STMT_new_str (lv_dst, _)
+ | Ast.STMT_new_port lv_dst
+ | Ast.STMT_new_chan (lv_dst, _)
+ | Ast.STMT_new_box (lv_dst, _, _) ->
+ note_write s lv_dst
+
| _ -> ()
end;
inner.Walk.visit_stmt_pre s
@@ -200,19 +157,6 @@ let function_effect_propagation_visitor
Walk.visit_stmt_pre = visit_stmt_pre }
;;
-let binding_effect_propagation_visitor
- ((*cx*)_:ctxt)
- (inner:Walk.visitor)
- : Walk.visitor =
- (* This visitor lowers the effect of an object or binding according
- * to its slots: holding a 'state' slot lowers any obj item, or
- * bind-stmt LHS, to 'state'.
- *
- * Binding (or implicitly just making a native 1st-class) makes the LHS
- * unsafe.
- *)
- inner
-;;
let effect_checking_visitor
(item_auth:(node_id, Ast.effect) Hashtbl.t)
@@ -221,7 +165,7 @@ let effect_checking_visitor
(inner:Walk.visitor)
: Walk.visitor =
(*
- * This visitor checks that each type, item and obj declares
+ * This visitor checks that each fn declares
* effects consistent with what we calculated.
*)
let auth_stack = Stack.create () in
@@ -250,7 +194,8 @@ let effect_checking_visitor
end;
begin
match i.node.Ast.decl_item with
- Ast.MOD_ITEM_fn f ->
+ Ast.MOD_ITEM_fn f
+ when htab_search cx.ctxt_required_items i.id = None ->
let e =
match htab_search item_effect i.id with
None -> Ast.EFF_pure
@@ -319,11 +264,7 @@ let process_crate
let item_effect = Hashtbl.create 0 in
let passes =
[|
- (mutability_checking_visitor cx
- Walk.empty_visitor);
- (function_effect_propagation_visitor item_effect cx
- Walk.empty_visitor);
- (binding_effect_propagation_visitor cx
+ (effect_calculating_visitor item_effect cx
Walk.empty_visitor);
(effect_checking_visitor item_auth item_effect cx
Walk.empty_visitor);
diff --git a/src/boot/me/stratum.ml b/src/boot/me/stratum.ml
new file mode 100644
index 00000000..21598d55
--- /dev/null
+++ b/src/boot/me/stratum.ml
@@ -0,0 +1,108 @@
+open Semant;;
+open Common;;
+
+let log cx = Session.log "stratum"
+ (should_log cx cx.ctxt_sess.Session.sess_log_stratum)
+ cx.ctxt_sess.Session.sess_log_out
+;;
+
+let iflog cx thunk =
+ if (should_log cx cx.ctxt_sess.Session.sess_log_stratum)
+ then thunk ()
+ else ()
+;;
+
+
+let state_stratum_checking_visitor
+ (cx:ctxt)
+ (inner:Walk.visitor)
+ : Walk.visitor =
+ (*
+ * This visitor enforces the following rules:
+ *
+ * - A channel type carrying a state type is illegal.
+ *
+ * - Writing to an immutable slot is illegal.
+ *
+ * - Forming a mutable alias to an immutable slot is illegal.
+ *
+ *)
+ let visit_ty_pre t =
+ match t with
+ Ast.TY_chan t' when type_has_state cx t' ->
+ err None "channel of state type: %a " Ast.sprintf_ty t'
+ | _ -> ()
+ in
+
+ let check_write s dst =
+ let is_init = Hashtbl.mem cx.ctxt_stmt_is_init s.id in
+ let dst_ty = lval_ty cx dst in
+ let is_mutable =
+ match dst_ty with
+ Ast.TY_mutable _ -> true
+ | _ -> false
+ in
+ iflog cx
+ (fun _ -> log cx "checking %swrite to %slval #%d = %a of type %a"
+ (if is_init then "initializing " else "")
+ (if is_mutable then "mutable " else "")
+ (int_of_node (lval_base_id dst))
+ Ast.sprintf_lval dst
+ Ast.sprintf_ty dst_ty);
+ if (is_mutable or is_init)
+ then ()
+ else err (Some s.id)
+ "writing to immutable type %a in statement %a"
+ Ast.sprintf_ty dst_ty Ast.sprintf_stmt s
+ in
+ (* FIXME (issue #75): enforce the no-write-alias-to-immutable-slot
+ * rule.
+ *)
+ let visit_stmt_pre s =
+ begin
+ match s.node with
+ Ast.STMT_copy (lv_dst, _)
+ | Ast.STMT_call (lv_dst, _, _)
+ | Ast.STMT_spawn (lv_dst, _, _, _, _)
+ | Ast.STMT_recv (lv_dst, _)
+ | Ast.STMT_bind (lv_dst, _, _)
+ | Ast.STMT_new_rec (lv_dst, _, _)
+ | Ast.STMT_new_tup (lv_dst, _)
+ | Ast.STMT_new_vec (lv_dst, _, _)
+ | Ast.STMT_new_str (lv_dst, _)
+ | Ast.STMT_new_port lv_dst
+ | Ast.STMT_new_chan (lv_dst, _)
+ | Ast.STMT_new_box (lv_dst, _, _) ->
+ check_write s lv_dst
+ | _ -> ()
+ end;
+ inner.Walk.visit_stmt_pre s
+ in
+
+ { inner with
+ Walk.visit_ty_pre = visit_ty_pre;
+ Walk.visit_stmt_pre = visit_stmt_pre }
+;;
+
+let process_crate
+ (cx:ctxt)
+ (crate:Ast.crate)
+ : unit =
+ let passes =
+ [|
+ (state_stratum_checking_visitor cx
+ Walk.empty_visitor);
+ |]
+ in
+ run_passes cx "stratum" passes
+ cx.ctxt_sess.Session.sess_log_stratum log crate
+;;
+
+(*
+ * Local Variables:
+ * fill-column: 78;
+ * indent-tabs-mode: nil
+ * buffer-file-coding-system: utf-8-unix
+ * compile-command: "make -k -C ../.. 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+ * End:
+ *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 08:56:08 +0000