Fix numerous non-linearities and O(sizeof(crate)) issues in typestate system's dataflow algorithm. No longer substantial in profile.
This commit is contained in:
parent
4b97b4e79d
commit
3d69407b51
2 changed files with 341 additions and 127 deletions
|
@ -100,6 +100,7 @@ type ctxt =
|
||||||
ctxt_all_stmts: (node_id,Ast.stmt) Hashtbl.t;
|
ctxt_all_stmts: (node_id,Ast.stmt) Hashtbl.t;
|
||||||
ctxt_item_files: (node_id,filename) Hashtbl.t;
|
ctxt_item_files: (node_id,filename) Hashtbl.t;
|
||||||
ctxt_all_lvals: (node_id,Ast.lval) Hashtbl.t;
|
ctxt_all_lvals: (node_id,Ast.lval) Hashtbl.t;
|
||||||
|
ctxt_call_lval_params: (node_id,Ast.ty array) Hashtbl.t;
|
||||||
|
|
||||||
(* definition id --> definition *)
|
(* definition id --> definition *)
|
||||||
ctxt_all_defns: (node_id,defn) Hashtbl.t;
|
ctxt_all_defns: (node_id,defn) Hashtbl.t;
|
||||||
|
@ -110,6 +111,10 @@ type ctxt =
|
||||||
ctxt_required_items: (node_id, (required_lib * nabi_conv)) Hashtbl.t;
|
ctxt_required_items: (node_id, (required_lib * nabi_conv)) Hashtbl.t;
|
||||||
ctxt_required_syms: (node_id, string) Hashtbl.t;
|
ctxt_required_syms: (node_id, string) Hashtbl.t;
|
||||||
|
|
||||||
|
(* Typestate-y stuff. *)
|
||||||
|
ctxt_stmt_is_init: (node_id,unit) Hashtbl.t;
|
||||||
|
ctxt_post_stmt_slot_drops: (node_id,node_id list) Hashtbl.t;
|
||||||
|
|
||||||
(* Layout-y stuff. *)
|
(* Layout-y stuff. *)
|
||||||
ctxt_slot_aliased: (node_id,unit) Hashtbl.t;
|
ctxt_slot_aliased: (node_id,unit) Hashtbl.t;
|
||||||
ctxt_slot_is_obj_state: (node_id,unit) Hashtbl.t;
|
ctxt_slot_is_obj_state: (node_id,unit) Hashtbl.t;
|
||||||
|
@ -121,17 +126,6 @@ type ctxt =
|
||||||
ctxt_stmt_loop_depths: (node_id,int) Hashtbl.t;
|
ctxt_stmt_loop_depths: (node_id,int) Hashtbl.t;
|
||||||
ctxt_slot_loop_depths: (node_id,int) Hashtbl.t;
|
ctxt_slot_loop_depths: (node_id,int) Hashtbl.t;
|
||||||
|
|
||||||
(* Typestate-y stuff. *)
|
|
||||||
ctxt_constrs: (constr_id,constr_key) Hashtbl.t;
|
|
||||||
ctxt_constr_ids: (constr_key,constr_id) Hashtbl.t;
|
|
||||||
ctxt_preconditions: (node_id,Bits.t) Hashtbl.t;
|
|
||||||
ctxt_postconditions: (node_id,Bits.t) Hashtbl.t;
|
|
||||||
ctxt_prestates: (node_id,Bits.t) Hashtbl.t;
|
|
||||||
ctxt_poststates: (node_id,Bits.t) Hashtbl.t;
|
|
||||||
ctxt_call_lval_params: (node_id,Ast.ty array) Hashtbl.t;
|
|
||||||
ctxt_stmt_is_init: (node_id,unit) Hashtbl.t;
|
|
||||||
ctxt_post_stmt_slot_drops: (node_id,node_id list) Hashtbl.t;
|
|
||||||
|
|
||||||
(* Translation-y stuff. *)
|
(* Translation-y stuff. *)
|
||||||
ctxt_fn_fixups: (node_id,fixup) Hashtbl.t;
|
ctxt_fn_fixups: (node_id,fixup) Hashtbl.t;
|
||||||
ctxt_block_fixups: (node_id,fixup) Hashtbl.t;
|
ctxt_block_fixups: (node_id,fixup) Hashtbl.t;
|
||||||
|
@ -192,19 +186,13 @@ let new_ctxt sess abi crate =
|
||||||
ctxt_item_files = crate.Ast.crate_files;
|
ctxt_item_files = crate.Ast.crate_files;
|
||||||
ctxt_all_lvals = Hashtbl.create 0;
|
ctxt_all_lvals = Hashtbl.create 0;
|
||||||
ctxt_all_defns = Hashtbl.create 0;
|
ctxt_all_defns = Hashtbl.create 0;
|
||||||
|
ctxt_call_lval_params = Hashtbl.create 0;
|
||||||
ctxt_lval_to_referent = Hashtbl.create 0;
|
ctxt_lval_to_referent = Hashtbl.create 0;
|
||||||
ctxt_required_items = crate.Ast.crate_required;
|
ctxt_required_items = crate.Ast.crate_required;
|
||||||
ctxt_required_syms = crate.Ast.crate_required_syms;
|
ctxt_required_syms = crate.Ast.crate_required_syms;
|
||||||
|
|
||||||
ctxt_constrs = Hashtbl.create 0;
|
|
||||||
ctxt_constr_ids = Hashtbl.create 0;
|
|
||||||
ctxt_preconditions = Hashtbl.create 0;
|
|
||||||
ctxt_postconditions = Hashtbl.create 0;
|
|
||||||
ctxt_prestates = Hashtbl.create 0;
|
|
||||||
ctxt_poststates = Hashtbl.create 0;
|
|
||||||
ctxt_stmt_is_init = Hashtbl.create 0;
|
ctxt_stmt_is_init = Hashtbl.create 0;
|
||||||
ctxt_post_stmt_slot_drops = Hashtbl.create 0;
|
ctxt_post_stmt_slot_drops = Hashtbl.create 0;
|
||||||
ctxt_call_lval_params = Hashtbl.create 0;
|
|
||||||
|
|
||||||
ctxt_slot_aliased = Hashtbl.create 0;
|
ctxt_slot_aliased = Hashtbl.create 0;
|
||||||
ctxt_slot_is_obj_state = Hashtbl.create 0;
|
ctxt_slot_is_obj_state = Hashtbl.create 0;
|
||||||
|
|
|
@ -13,6 +13,96 @@ let iflog cx thunk =
|
||||||
else ()
|
else ()
|
||||||
;;
|
;;
|
||||||
|
|
||||||
|
type node_graph = (node_id, (node_id list)) Hashtbl.t;;
|
||||||
|
type sibling_map = (node_id, node_id) Hashtbl.t;;
|
||||||
|
|
||||||
|
type typestate_tables =
|
||||||
|
{ ts_constrs: (constr_id,constr_key) Hashtbl.t;
|
||||||
|
ts_constr_ids: (constr_key,constr_id) Hashtbl.t;
|
||||||
|
ts_preconditions: (node_id,Bits.t) Hashtbl.t;
|
||||||
|
ts_postconditions: (node_id,Bits.t) Hashtbl.t;
|
||||||
|
ts_prestates: (node_id,Bits.t) Hashtbl.t;
|
||||||
|
ts_poststates: (node_id,Bits.t) Hashtbl.t;
|
||||||
|
ts_graph: node_graph;
|
||||||
|
ts_siblings: sibling_map;
|
||||||
|
ts_stmts: Ast.stmt Stack.t;
|
||||||
|
ts_maxid: int ref;
|
||||||
|
}
|
||||||
|
;;
|
||||||
|
|
||||||
|
let new_tables _ =
|
||||||
|
{ ts_constrs = Hashtbl.create 0;
|
||||||
|
ts_constr_ids = Hashtbl.create 0;
|
||||||
|
ts_preconditions = Hashtbl.create 0;
|
||||||
|
ts_postconditions = Hashtbl.create 0;
|
||||||
|
ts_poststates = Hashtbl.create 0;
|
||||||
|
ts_prestates = Hashtbl.create 0;
|
||||||
|
ts_graph = Hashtbl.create 0;
|
||||||
|
ts_siblings = Hashtbl.create 0;
|
||||||
|
ts_stmts = Stack.create ();
|
||||||
|
ts_maxid = ref 0 }
|
||||||
|
;;
|
||||||
|
|
||||||
|
type item_tables = (node_id, typestate_tables) Hashtbl.t
|
||||||
|
;;
|
||||||
|
|
||||||
|
let get_tables (all_tables:item_tables) (n:node_id) : typestate_tables =
|
||||||
|
htab_search_or_add all_tables n new_tables
|
||||||
|
;;
|
||||||
|
|
||||||
|
let tables_managing_visitor
|
||||||
|
(all_tables:item_tables)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
|
(inner:Walk.visitor)
|
||||||
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let enter id =
|
||||||
|
Stack.push (get_tables all_tables id) tables_stack
|
||||||
|
in
|
||||||
|
|
||||||
|
let leave _ =
|
||||||
|
ignore (Stack.pop tables_stack)
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_mod_item_pre n p i =
|
||||||
|
enter i.id;
|
||||||
|
inner.Walk.visit_mod_item_pre n p i
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_mod_item_post n p i =
|
||||||
|
inner.Walk.visit_mod_item_post n p i;
|
||||||
|
leave()
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_fn_pre obj ident fn =
|
||||||
|
enter fn.id;
|
||||||
|
inner.Walk.visit_obj_fn_pre obj ident fn
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_fn_post obj ident fn =
|
||||||
|
inner.Walk.visit_obj_fn_post obj ident fn;
|
||||||
|
leave()
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_drop_pre obj b =
|
||||||
|
enter b.id;
|
||||||
|
inner.Walk.visit_obj_drop_pre obj b
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_drop_post obj b =
|
||||||
|
inner.Walk.visit_obj_drop_post obj b;
|
||||||
|
leave()
|
||||||
|
in
|
||||||
|
{ inner with
|
||||||
|
Walk.visit_mod_item_pre = visit_mod_item_pre;
|
||||||
|
Walk.visit_mod_item_post = visit_mod_item_post;
|
||||||
|
Walk.visit_obj_fn_pre = visit_obj_fn_pre;
|
||||||
|
Walk.visit_obj_fn_post = visit_obj_fn_post;
|
||||||
|
Walk.visit_obj_drop_pre = visit_obj_drop_pre;
|
||||||
|
Walk.visit_obj_drop_post = visit_obj_drop_post; }
|
||||||
|
;;
|
||||||
|
|
||||||
|
|
||||||
let name_base_to_slot_key (nb:Ast.name_base) : Ast.slot_key =
|
let name_base_to_slot_key (nb:Ast.name_base) : Ast.slot_key =
|
||||||
match nb with
|
match nb with
|
||||||
Ast.BASE_ident ident -> Ast.KEY_ident ident
|
Ast.BASE_ident ident -> Ast.KEY_ident ident
|
||||||
|
@ -153,11 +243,13 @@ let fn_keys fn resolver =
|
||||||
|
|
||||||
let constr_id_assigning_visitor
|
let constr_id_assigning_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(scopes:(scope list) ref)
|
(scopes:(scope list) ref)
|
||||||
(idref:int ref)
|
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let resolve_constr_to_key
|
let resolve_constr_to_key
|
||||||
(formal_base:node_id)
|
(formal_base:node_id)
|
||||||
(constr:Ast.constr)
|
(constr:Ast.constr)
|
||||||
|
@ -166,7 +258,9 @@ let constr_id_assigning_visitor
|
||||||
in
|
in
|
||||||
|
|
||||||
let note_constr_key key =
|
let note_constr_key key =
|
||||||
if not (Hashtbl.mem cx.ctxt_constr_ids key)
|
let ts = tables () in
|
||||||
|
let idref = ts.ts_maxid in
|
||||||
|
if not (Hashtbl.mem ts.ts_constr_ids key)
|
||||||
then
|
then
|
||||||
begin
|
begin
|
||||||
let cid = Constr (!idref) in
|
let cid = Constr (!idref) in
|
||||||
|
@ -174,8 +268,8 @@ let constr_id_assigning_visitor
|
||||||
(fun _ -> log cx "assigning constr id #%d to constr %s"
|
(fun _ -> log cx "assigning constr id #%d to constr %s"
|
||||||
(!idref) (fmt_constr_key cx key));
|
(!idref) (fmt_constr_key cx key));
|
||||||
incr idref;
|
incr idref;
|
||||||
htab_put cx.ctxt_constrs cid key;
|
htab_put ts.ts_constrs cid key;
|
||||||
htab_put cx.ctxt_constr_ids key cid;
|
htab_put ts.ts_constr_ids key cid;
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -198,6 +292,24 @@ let constr_id_assigning_visitor
|
||||||
inner.Walk.visit_mod_item_pre n p i
|
inner.Walk.visit_mod_item_pre n p i
|
||||||
in
|
in
|
||||||
|
|
||||||
|
let visit_obj_fn_pre obj ident fn =
|
||||||
|
let (obj_input_keys, obj_init_keys) =
|
||||||
|
obj_keys obj.node (resolve_constr_to_key obj.id)
|
||||||
|
in
|
||||||
|
note_keys obj_input_keys;
|
||||||
|
note_keys obj_init_keys;
|
||||||
|
inner.Walk.visit_obj_fn_pre obj ident fn
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_drop_pre obj b =
|
||||||
|
let (obj_input_keys, obj_init_keys) =
|
||||||
|
obj_keys obj.node (resolve_constr_to_key obj.id)
|
||||||
|
in
|
||||||
|
note_keys obj_input_keys;
|
||||||
|
note_keys obj_init_keys;
|
||||||
|
inner.Walk.visit_obj_drop_pre obj b
|
||||||
|
in
|
||||||
|
|
||||||
let visit_constr_pre formal_base c =
|
let visit_constr_pre formal_base c =
|
||||||
let key = determine_constr_key cx (!scopes) formal_base c in
|
let key = determine_constr_key cx (!scopes) formal_base c in
|
||||||
note_constr_key key;
|
note_constr_key key;
|
||||||
|
@ -242,6 +354,8 @@ let constr_id_assigning_visitor
|
||||||
in
|
in
|
||||||
{ inner with
|
{ inner with
|
||||||
Walk.visit_mod_item_pre = visit_mod_item_pre;
|
Walk.visit_mod_item_pre = visit_mod_item_pre;
|
||||||
|
Walk.visit_obj_fn_pre = visit_obj_fn_pre;
|
||||||
|
Walk.visit_obj_drop_pre = visit_obj_drop_pre;
|
||||||
Walk.visit_slot_identified_pre = visit_slot_identified_pre;
|
Walk.visit_slot_identified_pre = visit_slot_identified_pre;
|
||||||
Walk.visit_stmt_pre = visit_stmt_pre;
|
Walk.visit_stmt_pre = visit_stmt_pre;
|
||||||
Walk.visit_constr_pre = visit_constr_pre }
|
Walk.visit_constr_pre = visit_constr_pre }
|
||||||
|
@ -249,25 +363,32 @@ let constr_id_assigning_visitor
|
||||||
|
|
||||||
let bitmap_assigning_visitor
|
let bitmap_assigning_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
(idref:int ref)
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let visit_stmt_pre s =
|
let visit_stmt_pre s =
|
||||||
|
let ts = tables () in
|
||||||
|
let idref = ts.ts_maxid in
|
||||||
iflog cx (fun _ -> log cx "building %d-entry bitmap for node %d"
|
iflog cx (fun _ -> log cx "building %d-entry bitmap for node %d"
|
||||||
(!idref) (int_of_node s.id));
|
(!idref) (int_of_node s.id));
|
||||||
htab_put cx.ctxt_preconditions s.id (Bits.create (!idref) false);
|
htab_put ts.ts_preconditions s.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_postconditions s.id (Bits.create (!idref) false);
|
htab_put ts.ts_postconditions s.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_prestates s.id (Bits.create (!idref) false);
|
htab_put ts.ts_prestates s.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_poststates s.id (Bits.create (!idref) false);
|
htab_put ts.ts_poststates s.id (Bits.create (!idref) false);
|
||||||
inner.Walk.visit_stmt_pre s
|
inner.Walk.visit_stmt_pre s
|
||||||
in
|
in
|
||||||
let visit_block_pre b =
|
let visit_block_pre b =
|
||||||
|
let ts = tables () in
|
||||||
|
let idref = ts.ts_maxid in
|
||||||
iflog cx (fun _ -> log cx "building %d-entry bitmap for node %d"
|
iflog cx (fun _ -> log cx "building %d-entry bitmap for node %d"
|
||||||
(!idref) (int_of_node b.id));
|
(!idref) (int_of_node b.id));
|
||||||
htab_put cx.ctxt_preconditions b.id (Bits.create (!idref) false);
|
htab_put ts.ts_preconditions b.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_postconditions b.id (Bits.create (!idref) false);
|
htab_put ts.ts_postconditions b.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_prestates b.id (Bits.create (!idref) false);
|
htab_put ts.ts_prestates b.id (Bits.create (!idref) false);
|
||||||
htab_put cx.ctxt_poststates b.id (Bits.create (!idref) false);
|
htab_put ts.ts_poststates b.id (Bits.create (!idref) false);
|
||||||
inner.Walk.visit_block_pre b
|
inner.Walk.visit_block_pre b
|
||||||
in
|
in
|
||||||
{ inner with
|
{ inner with
|
||||||
|
@ -277,14 +398,18 @@ let bitmap_assigning_visitor
|
||||||
|
|
||||||
let condition_assigning_visitor
|
let condition_assigning_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(scopes:(scope list) ref)
|
(scopes:(scope list) ref)
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let raise_bits (bitv:Bits.t) (keys:constr_key array) : unit =
|
let raise_bits (bitv:Bits.t) (keys:constr_key array) : unit =
|
||||||
|
let ts = tables () in
|
||||||
Array.iter
|
Array.iter
|
||||||
(fun key ->
|
(fun key ->
|
||||||
let cid = Hashtbl.find cx.ctxt_constr_ids key in
|
let cid = Hashtbl.find ts.ts_constr_ids key in
|
||||||
let i = int_of_constr cid in
|
let i = int_of_constr cid in
|
||||||
iflog cx (fun _ -> log cx "setting bit %d, constraint %s"
|
iflog cx (fun _ -> log cx "setting bit %d, constraint %s"
|
||||||
i (fmt_constr_key cx key));
|
i (fmt_constr_key cx key));
|
||||||
|
@ -295,12 +420,14 @@ let condition_assigning_visitor
|
||||||
let slot_inits ss = Array.map (fun s -> Constr_init s) ss in
|
let slot_inits ss = Array.map (fun s -> Constr_init s) ss in
|
||||||
|
|
||||||
let raise_postcondition (id:node_id) (keys:constr_key array) : unit =
|
let raise_postcondition (id:node_id) (keys:constr_key array) : unit =
|
||||||
let bitv = Hashtbl.find cx.ctxt_postconditions id in
|
let ts = tables () in
|
||||||
|
let bitv = Hashtbl.find ts.ts_postconditions id in
|
||||||
raise_bits bitv keys
|
raise_bits bitv keys
|
||||||
in
|
in
|
||||||
|
|
||||||
let raise_precondition (id:node_id) (keys:constr_key array) : unit =
|
let raise_precondition (id:node_id) (keys:constr_key array) : unit =
|
||||||
let bitv = Hashtbl.find cx.ctxt_preconditions id in
|
let ts = tables () in
|
||||||
|
let bitv = Hashtbl.find ts.ts_preconditions id in
|
||||||
raise_bits bitv keys
|
raise_bits bitv keys
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -602,18 +729,19 @@ let show_node cx graph s i =
|
||||||
s (int_of_node i) (lset_fmt (Hashtbl.find graph i)))
|
s (int_of_node i) (lset_fmt (Hashtbl.find graph i)))
|
||||||
;;
|
;;
|
||||||
|
|
||||||
type node_graph = (node_id, (node_id list)) Hashtbl.t;;
|
|
||||||
type sibling_map = (node_id, node_id) Hashtbl.t;;
|
|
||||||
|
|
||||||
let graph_sequence_building_visitor
|
let graph_sequence_building_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
(graph:node_graph)
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(sibs:sibling_map)
|
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
(* Flow each stmt to its sequence-successor. *)
|
(* Flow each stmt to its sequence-successor. *)
|
||||||
let visit_stmts stmts =
|
let visit_stmts stmts =
|
||||||
|
let ts = tables () in
|
||||||
|
let graph = ts.ts_graph in
|
||||||
|
let sibs = ts.ts_siblings in
|
||||||
let len = Array.length stmts in
|
let len = Array.length stmts in
|
||||||
for i = 0 to len - 2
|
for i = 0 to len - 2
|
||||||
do
|
do
|
||||||
|
@ -680,27 +808,36 @@ let last_id_or_block_id (block:Ast.block) : node_id =
|
||||||
|
|
||||||
let graph_general_block_structure_building_visitor
|
let graph_general_block_structure_building_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
(graph:node_graph)
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(sibs:sibling_map)
|
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
let stmts = Stack.create () in
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let visit_stmt_pre s =
|
let visit_stmt_pre s =
|
||||||
|
let ts = tables () in
|
||||||
|
let stmts = ts.ts_stmts in
|
||||||
Stack.push s stmts;
|
Stack.push s stmts;
|
||||||
inner.Walk.visit_stmt_pre s
|
inner.Walk.visit_stmt_pre s
|
||||||
in
|
in
|
||||||
|
|
||||||
let visit_stmt_post s =
|
let visit_stmt_post s =
|
||||||
|
let ts = tables () in
|
||||||
|
let stmts = ts.ts_stmts in
|
||||||
inner.Walk.visit_stmt_post s;
|
inner.Walk.visit_stmt_post s;
|
||||||
ignore (Stack.pop stmts)
|
ignore (Stack.pop stmts)
|
||||||
in
|
in
|
||||||
|
|
||||||
let show_node = show_node cx graph in
|
let show_node =
|
||||||
|
fun n id -> show_node cx (tables()).ts_graph n id
|
||||||
|
in
|
||||||
|
|
||||||
let visit_block_pre b =
|
let visit_block_pre b =
|
||||||
begin
|
begin
|
||||||
|
let ts = tables () in
|
||||||
|
let graph = ts.ts_graph in
|
||||||
|
let sibs = ts.ts_siblings in
|
||||||
|
let stmts = ts.ts_stmts in
|
||||||
let len = Array.length b.node in
|
let len = Array.length b.node in
|
||||||
let _ = htab_put graph b.id
|
let _ = htab_put graph b.id
|
||||||
(if len > 0 then [b.node.(0).id] else [])
|
(if len > 0 then [b.node.(0).id] else [])
|
||||||
|
@ -748,15 +885,19 @@ let graph_general_block_structure_building_visitor
|
||||||
|
|
||||||
let graph_special_block_structure_building_visitor
|
let graph_special_block_structure_building_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
(graph:(node_id, (node_id list)) Hashtbl.t)
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let visit_stmt_pre s =
|
let visit_stmt_pre s =
|
||||||
begin
|
begin
|
||||||
match s.node with
|
match s.node with
|
||||||
|
|
||||||
| Ast.STMT_if sif ->
|
Ast.STMT_if sif ->
|
||||||
|
let ts = tables () in
|
||||||
|
let graph = ts.ts_graph in
|
||||||
let cond_id = s.id in
|
let cond_id = s.id in
|
||||||
let then_id = sif.Ast.if_then.id in
|
let then_id = sif.Ast.if_then.id in
|
||||||
let then_end_id = last_id_or_block_id sif.Ast.if_then in
|
let then_end_id = last_id_or_block_id sif.Ast.if_then in
|
||||||
|
@ -799,6 +940,8 @@ let graph_special_block_structure_building_visitor
|
||||||
(* There are a bunch of rewirings to do on 'while' nodes. *)
|
(* There are a bunch of rewirings to do on 'while' nodes. *)
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
let ts = tables () in
|
||||||
|
let graph = ts.ts_graph in
|
||||||
let dsts = Hashtbl.find graph s.id in
|
let dsts = Hashtbl.find graph s.id in
|
||||||
let body = sw.Ast.while_body in
|
let body = sw.Ast.while_body in
|
||||||
let succ_stmts =
|
let succ_stmts =
|
||||||
|
@ -837,6 +980,8 @@ let graph_special_block_structure_building_visitor
|
||||||
end
|
end
|
||||||
|
|
||||||
| Ast.STMT_alt_tag at ->
|
| Ast.STMT_alt_tag at ->
|
||||||
|
let ts = tables () in
|
||||||
|
let graph = ts.ts_graph in
|
||||||
let dsts = Hashtbl.find graph s.id in
|
let dsts = Hashtbl.find graph s.id in
|
||||||
let arm_blocks =
|
let arm_blocks =
|
||||||
let arm_block_id { node = (_, block) } = block.id in
|
let arm_block_id { node = (_, block) } = block.id in
|
||||||
|
@ -865,37 +1010,60 @@ let find_roots
|
||||||
roots
|
roots
|
||||||
;;
|
;;
|
||||||
|
|
||||||
let run_dataflow cx idref graph : unit =
|
let run_dataflow (cx:ctxt) (ts:typestate_tables) : unit =
|
||||||
|
let graph = ts.ts_graph in
|
||||||
|
let idref = ts.ts_maxid in
|
||||||
let roots = find_roots graph in
|
let roots = find_roots graph in
|
||||||
let nodes = Queue.create () in
|
let nodes = Queue.create () in
|
||||||
|
|
||||||
let progress = ref true in
|
let progress = ref true in
|
||||||
|
let iter = ref 0 in
|
||||||
|
let total = ref 0 in
|
||||||
|
let written = Hashtbl.create 0 in
|
||||||
|
let scheduled = Hashtbl.create 0 in
|
||||||
|
let next_nodes = Queue.create () in
|
||||||
|
let schedule n =
|
||||||
|
if Hashtbl.mem scheduled n
|
||||||
|
then ()
|
||||||
|
else
|
||||||
|
begin
|
||||||
|
Queue.push n next_nodes;
|
||||||
|
Hashtbl.add scheduled n ()
|
||||||
|
end
|
||||||
|
in
|
||||||
|
|
||||||
let fmt_constr_bitv bitv =
|
let fmt_constr_bitv bitv =
|
||||||
String.concat ", "
|
String.concat ", "
|
||||||
(List.map
|
(List.map
|
||||||
(fun i ->
|
(fun i ->
|
||||||
fmt_constr_key cx
|
fmt_constr_key cx
|
||||||
(Hashtbl.find cx.ctxt_constrs (Constr i)))
|
(Hashtbl.find ts.ts_constrs (Constr i)))
|
||||||
(Bits.to_list bitv))
|
(Bits.to_list bitv))
|
||||||
in
|
in
|
||||||
|
|
||||||
let set_bits dst src =
|
let set_bits dst src =
|
||||||
if Bits.copy dst src
|
if Bits.copy dst src
|
||||||
then (progress := true;
|
then (progress := true;
|
||||||
iflog cx (fun _ -> log cx "made progress setting bits"))
|
iflog cx (fun _ -> log cx "made progress setting bits"))
|
||||||
in
|
in
|
||||||
let intersect_bits dst src =
|
|
||||||
|
let intersect_bits node dst src =
|
||||||
if Bits.intersect dst src
|
if Bits.intersect dst src
|
||||||
then (progress := true;
|
then (progress := true;
|
||||||
|
schedule node;
|
||||||
iflog cx (fun _ -> log cx
|
iflog cx (fun _ -> log cx
|
||||||
"made progress intersecting bits"))
|
"made progress intersecting bits"))
|
||||||
in
|
in
|
||||||
let iter = ref 0 in
|
|
||||||
let written = Hashtbl.create 0 in
|
|
||||||
let tmp_diff = (Bits.create (!idref) false) in
|
let tmp_diff = (Bits.create (!idref) false) in
|
||||||
let tmp_poststate = (Bits.create (!idref) false) in
|
let tmp_poststate = (Bits.create (!idref) false) in
|
||||||
Hashtbl.iter (fun n _ -> Queue.push n nodes) roots;
|
Hashtbl.iter (fun n _ -> schedule n) roots;
|
||||||
while !progress do
|
while !progress do
|
||||||
incr iter;
|
incr iter;
|
||||||
progress := false;
|
progress := false;
|
||||||
|
Queue.clear nodes;
|
||||||
|
Queue.transfer next_nodes nodes;
|
||||||
|
Hashtbl.clear scheduled;
|
||||||
iflog cx (fun _ ->
|
iflog cx (fun _ ->
|
||||||
log cx "";
|
log cx "";
|
||||||
log cx "--------------------";
|
log cx "--------------------";
|
||||||
|
@ -903,11 +1071,12 @@ let run_dataflow cx idref graph : unit =
|
||||||
Queue.iter
|
Queue.iter
|
||||||
begin
|
begin
|
||||||
fun node ->
|
fun node ->
|
||||||
let prestate = Hashtbl.find cx.ctxt_prestates node in
|
let prestate = Hashtbl.find ts.ts_prestates node in
|
||||||
let precond = Hashtbl.find cx.ctxt_preconditions node in
|
let precond = Hashtbl.find ts.ts_preconditions node in
|
||||||
let postcond = Hashtbl.find cx.ctxt_postconditions node in
|
let postcond = Hashtbl.find ts.ts_postconditions node in
|
||||||
let poststate = Hashtbl.find cx.ctxt_poststates node in
|
let poststate = Hashtbl.find ts.ts_poststates node in
|
||||||
|
|
||||||
|
incr total;
|
||||||
Bits.clear tmp_poststate;
|
Bits.clear tmp_poststate;
|
||||||
ignore (Bits.union tmp_poststate prestate);
|
ignore (Bits.union tmp_poststate prestate);
|
||||||
ignore (Bits.union tmp_poststate precond);
|
ignore (Bits.union tmp_poststate precond);
|
||||||
|
@ -947,18 +1116,15 @@ let run_dataflow cx idref graph : unit =
|
||||||
begin
|
begin
|
||||||
fun succ ->
|
fun succ ->
|
||||||
let succ_prestates =
|
let succ_prestates =
|
||||||
Hashtbl.find cx.ctxt_prestates succ
|
Hashtbl.find ts.ts_prestates succ
|
||||||
in
|
in
|
||||||
if Hashtbl.mem written succ
|
if Hashtbl.mem written succ
|
||||||
then
|
then
|
||||||
begin
|
intersect_bits succ succ_prestates poststate
|
||||||
intersect_bits succ_prestates poststate;
|
|
||||||
Hashtbl.replace written succ ()
|
|
||||||
end
|
|
||||||
else
|
else
|
||||||
begin
|
begin
|
||||||
progress := true;
|
progress := true;
|
||||||
Queue.push succ nodes;
|
schedule succ;
|
||||||
set_bits succ_prestates poststate
|
set_bits succ_prestates poststate
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
@ -968,18 +1134,60 @@ let run_dataflow cx idref graph : unit =
|
||||||
done
|
done
|
||||||
;;
|
;;
|
||||||
|
|
||||||
let typestate_verify_visitor
|
let dataflow_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
|
let visit_mod_item_pre n p i =
|
||||||
|
run_dataflow cx (tables());
|
||||||
|
inner.Walk.visit_mod_item_pre n p i
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_fn_pre obj ident fn =
|
||||||
|
run_dataflow cx (tables());
|
||||||
|
inner.Walk.visit_obj_fn_pre obj ident fn
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_obj_drop_pre obj b =
|
||||||
|
run_dataflow cx (tables());
|
||||||
|
inner.Walk.visit_obj_drop_pre obj b
|
||||||
|
in
|
||||||
|
|
||||||
|
let visit_block_pre b =
|
||||||
|
if Hashtbl.mem cx.ctxt_block_is_loop_body b.id
|
||||||
|
then run_dataflow cx (tables());
|
||||||
|
inner.Walk.visit_block_pre b
|
||||||
|
in
|
||||||
|
|
||||||
|
{ inner with
|
||||||
|
Walk.visit_mod_item_pre = visit_mod_item_pre;
|
||||||
|
Walk.visit_obj_fn_pre = visit_obj_fn_pre;
|
||||||
|
Walk.visit_obj_drop_pre = visit_obj_drop_pre;
|
||||||
|
Walk.visit_block_pre = visit_block_pre }
|
||||||
|
;;
|
||||||
|
|
||||||
|
|
||||||
|
let typestate_verify_visitor
|
||||||
|
(cx:ctxt)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
|
(inner:Walk.visitor)
|
||||||
|
: Walk.visitor =
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let visit_stmt_pre s =
|
let visit_stmt_pre s =
|
||||||
let prestate = Hashtbl.find cx.ctxt_prestates s.id in
|
let ts = tables () in
|
||||||
let precond = Hashtbl.find cx.ctxt_preconditions s.id in
|
let prestate = Hashtbl.find ts.ts_prestates s.id in
|
||||||
|
let precond = Hashtbl.find ts.ts_preconditions s.id in
|
||||||
List.iter
|
List.iter
|
||||||
(fun i ->
|
(fun i ->
|
||||||
if not (Bits.get prestate i)
|
if not (Bits.get prestate i)
|
||||||
then
|
then
|
||||||
let ckey = Hashtbl.find cx.ctxt_constrs (Constr i) in
|
let ckey = Hashtbl.find ts.ts_constrs (Constr i) in
|
||||||
let constr_str = fmt_constr_key cx ckey in
|
let constr_str = fmt_constr_key cx ckey in
|
||||||
err (Some s.id)
|
err (Some s.id)
|
||||||
"Unsatisfied precondition constraint %s at stmt %d: %s"
|
"Unsatisfied precondition constraint %s at stmt %d: %s"
|
||||||
|
@ -996,6 +1204,7 @@ let typestate_verify_visitor
|
||||||
|
|
||||||
let lifecycle_visitor
|
let lifecycle_visitor
|
||||||
(cx:ctxt)
|
(cx:ctxt)
|
||||||
|
(tables_stack:typestate_tables Stack.t)
|
||||||
(inner:Walk.visitor)
|
(inner:Walk.visitor)
|
||||||
: Walk.visitor =
|
: Walk.visitor =
|
||||||
|
|
||||||
|
@ -1007,6 +1216,8 @@ let lifecycle_visitor
|
||||||
* used later on in translation.
|
* used later on in translation.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
let tables _ = Stack.top tables_stack in
|
||||||
|
|
||||||
let (live_block_slots:(node_id, unit) Hashtbl.t) = Hashtbl.create 0 in
|
let (live_block_slots:(node_id, unit) Hashtbl.t) = Hashtbl.create 0 in
|
||||||
let (block_slots:(node_id Stack.t) Stack.t) = Stack.create () in
|
let (block_slots:(node_id Stack.t) Stack.t) = Stack.create () in
|
||||||
|
|
||||||
|
@ -1101,12 +1312,13 @@ let lifecycle_visitor
|
||||||
| Ast.STMT_new_port lv_dst
|
| Ast.STMT_new_port lv_dst
|
||||||
| Ast.STMT_new_chan (lv_dst, _)
|
| Ast.STMT_new_chan (lv_dst, _)
|
||||||
| Ast.STMT_new_box (lv_dst, _, _) ->
|
| Ast.STMT_new_box (lv_dst, _, _) ->
|
||||||
let prestate = Hashtbl.find cx.ctxt_prestates s.id in
|
let ts = tables () in
|
||||||
let poststate = Hashtbl.find cx.ctxt_poststates s.id in
|
let prestate = Hashtbl.find ts.ts_prestates s.id in
|
||||||
|
let poststate = Hashtbl.find ts.ts_poststates s.id in
|
||||||
let dst_slots = lval_slots cx lv_dst in
|
let dst_slots = lval_slots cx lv_dst in
|
||||||
let is_initializing slot =
|
let is_initializing slot =
|
||||||
let cid =
|
let cid =
|
||||||
Hashtbl.find cx.ctxt_constr_ids (Constr_init slot)
|
Hashtbl.find ts.ts_constr_ids (Constr_init slot)
|
||||||
in
|
in
|
||||||
let i = int_of_constr cid in
|
let i = int_of_constr cid in
|
||||||
(not (Bits.get prestate i)) && (Bits.get poststate i)
|
(not (Bits.get prestate i)) && (Bits.get poststate i)
|
||||||
|
@ -1184,44 +1396,58 @@ let process_crate
|
||||||
: unit =
|
: unit =
|
||||||
let path = Stack.create () in
|
let path = Stack.create () in
|
||||||
let (scopes:(scope list) ref) = ref [] in
|
let (scopes:(scope list) ref) = ref [] in
|
||||||
let constr_id = ref 0 in
|
let (tables_stack:typestate_tables Stack.t) = Stack.create () in
|
||||||
let (graph:(node_id, (node_id list)) Hashtbl.t) = Hashtbl.create 0 in
|
let (all_tables:item_tables) = Hashtbl.create 0 in
|
||||||
let sibs = Hashtbl.create 0 in
|
let table_managed = tables_managing_visitor all_tables tables_stack in
|
||||||
let setup_passes =
|
let setup_passes =
|
||||||
[|
|
[|
|
||||||
|
(table_managed
|
||||||
(scope_stack_managing_visitor scopes
|
(scope_stack_managing_visitor scopes
|
||||||
(constr_id_assigning_visitor cx scopes constr_id
|
(constr_id_assigning_visitor cx tables_stack scopes
|
||||||
|
Walk.empty_visitor)));
|
||||||
|
(table_managed
|
||||||
|
(bitmap_assigning_visitor cx tables_stack
|
||||||
Walk.empty_visitor));
|
Walk.empty_visitor));
|
||||||
(bitmap_assigning_visitor cx constr_id
|
(table_managed
|
||||||
Walk.empty_visitor);
|
|
||||||
(scope_stack_managing_visitor scopes
|
(scope_stack_managing_visitor scopes
|
||||||
(condition_assigning_visitor cx scopes
|
(condition_assigning_visitor cx tables_stack scopes
|
||||||
|
Walk.empty_visitor)));
|
||||||
|
(table_managed
|
||||||
|
(graph_sequence_building_visitor cx tables_stack
|
||||||
Walk.empty_visitor));
|
Walk.empty_visitor));
|
||||||
(graph_sequence_building_visitor cx graph sibs
|
(table_managed
|
||||||
Walk.empty_visitor);
|
(graph_general_block_structure_building_visitor cx tables_stack
|
||||||
(graph_general_block_structure_building_visitor cx graph sibs
|
Walk.empty_visitor));
|
||||||
Walk.empty_visitor);
|
(table_managed
|
||||||
(graph_special_block_structure_building_visitor cx graph
|
(graph_special_block_structure_building_visitor cx tables_stack
|
||||||
Walk.empty_visitor);
|
Walk.empty_visitor));
|
||||||
|
|]
|
||||||
|
in
|
||||||
|
let dataflow_passes =
|
||||||
|
[|
|
||||||
|
(table_managed
|
||||||
|
(dataflow_visitor cx tables_stack
|
||||||
|
Walk.empty_visitor))
|
||||||
|]
|
|]
|
||||||
in
|
in
|
||||||
let verify_passes =
|
let verify_passes =
|
||||||
[|
|
[|
|
||||||
(scope_stack_managing_visitor scopes
|
(table_managed
|
||||||
(typestate_verify_visitor cx
|
(typestate_verify_visitor cx tables_stack
|
||||||
Walk.empty_visitor))
|
Walk.empty_visitor))
|
||||||
|]
|
|]
|
||||||
in
|
in
|
||||||
let aux_passes =
|
let aux_passes =
|
||||||
[|
|
[|
|
||||||
(lifecycle_visitor cx
|
(table_managed
|
||||||
Walk.empty_visitor)
|
(lifecycle_visitor cx tables_stack
|
||||||
|
Walk.empty_visitor))
|
||||||
|]
|
|]
|
||||||
in
|
in
|
||||||
let log_flag = cx.ctxt_sess.Session.sess_log_typestate in
|
let log_flag = cx.ctxt_sess.Session.sess_log_typestate in
|
||||||
run_passes cx "typestate setup" path setup_passes log_flag log crate;
|
run_passes cx "typestate setup" path setup_passes log_flag log crate;
|
||||||
Session.time_inner "typestate dataflow" cx.ctxt_sess
|
run_passes cx
|
||||||
(fun _ -> run_dataflow cx constr_id graph);
|
"typestate dataflow" path dataflow_passes log_flag log crate;
|
||||||
run_passes cx "typestate verify" path verify_passes log_flag log crate;
|
run_passes cx "typestate verify" path verify_passes log_flag log crate;
|
||||||
run_passes cx "typestate aux" path aux_passes log_flag log crate
|
run_passes cx "typestate aux" path aux_passes log_flag log crate
|
||||||
;;
|
;;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue