summaryrefslogtreecommitdiff
path: root/src/slice.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/slice.ml')
-rw-r--r--src/slice.ml194
1 files changed, 168 insertions, 26 deletions
diff --git a/src/slice.ml b/src/slice.ml
index f50104c4..a38a207c 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -104,7 +104,7 @@ let builtins =
let rec constraint_ids' (NC_aux (aux, _)) =
match aux with
- | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_not_equal (n1, n2) ->
+ | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_lt (n1, n2) | NC_bounded_gt (n1, n2) | NC_not_equal (n1, n2) ->
IdSet.union (nexp_ids' n1) (nexp_ids' n2)
| NC_or (nc1, nc2) | NC_and (nc1, nc2) ->
IdSet.union (constraint_ids' nc1) (constraint_ids' nc2)
@@ -157,9 +157,9 @@ let add_def_to_graph graph def =
let env = env_of_annot annot in
begin match p_aux with
| P_app (id, _) ->
- graph := G.add_edge' self (Constructor id) !graph
+ graph := G.add_edge self (Constructor id) !graph
| P_typ (typ, _) ->
- IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
| _ -> ()
end;
P_aux (p_aux, annot)
@@ -169,10 +169,29 @@ let add_def_to_graph graph def =
let scan_lexp self lexp_aux annot =
let env = env_of_annot annot in
begin match lexp_aux with
- | LEXP_cast (typ, _) ->
- IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+ | LEXP_cast (typ, id) ->
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ);
+ begin match Env.lookup_id id env with
+ | Register _ ->
+ graph := G.add_edge self (Register id) !graph
+ | Enum _ -> graph := G.add_edge self (Constructor id) !graph
+ | _ ->
+ if IdSet.mem id (Env.get_toplevel_lets env) then
+ graph := G.add_edge self (Letbind id) !graph
+ else ()
+ end
| LEXP_memory (id, _) ->
- graph := G.add_edge' self (Function id) !graph
+ graph := G.add_edge self (Function id) !graph
+ | LEXP_id id ->
+ begin match Env.lookup_id id env with
+ | Register _ ->
+ graph := G.add_edge self (Register id) !graph
+ | Enum _ -> graph := G.add_edge self (Constructor id) !graph
+ | _ ->
+ if IdSet.mem id (Env.get_toplevel_lets env) then
+ graph := G.add_edge self (Letbind id) !graph
+ else ()
+ end
| _ -> ()
end;
LEXP_aux (lexp_aux, annot)
@@ -183,26 +202,28 @@ let add_def_to_graph graph def =
begin match e_aux with
| E_id id ->
begin match Env.lookup_id id env with
- | Register _ -> graph := G.add_edge' self (Register id) !graph
+ | Register _ -> graph := G.add_edge self (Register id) !graph
+ | Enum _ -> graph := G.add_edge self (Constructor id) !graph
| _ ->
if IdSet.mem id (Env.get_toplevel_lets env) then
- graph := G.add_edge' self (Letbind id) !graph
+ graph := G.add_edge self (Letbind id) !graph
else ()
end
| E_app (id, _) ->
if Env.is_union_constructor id env then
- graph := G.add_edge' self (Constructor id) !graph
+ graph := G.add_edge self (Constructor id) !graph
else
- graph := G.add_edge' self (Function id) !graph
+ graph := G.add_edge self (Function id) !graph
| E_ref id ->
- graph := G.add_edge' self (Register id) !graph
+ graph := G.add_edge self (Register id) !graph
| E_cast (typ, _) ->
- IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (typ_ids typ)
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
| _ -> ()
end;
E_aux (e_aux, annot)
in
let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot);
+ lEXP_aux = (fun (l_aux, annot) -> scan_lexp self l_aux annot);
pat_alg = rw_pat self } in
let rewriters self =
@@ -216,8 +237,9 @@ let add_def_to_graph graph def =
let scan_quant_item self (QI_aux (aux, _)) =
match aux with
| QI_id _ -> ()
- | QI_const nc ->
- IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc)
+ | QI_constraint nc ->
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (constraint_ids nc)
+ | QI_constant _ -> ()
in
let scan_typquant self (TypQ_aux (aux, _)) =
@@ -229,7 +251,7 @@ let add_def_to_graph graph def =
let add_type_def_to_graph (TD_aux (aux, (l, _))) =
match aux with
| TD_abbrev (id, typq, arg) ->
- graph := G.add_edges' (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_arg_ids arg))) !graph;
+ graph := G.add_edges (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_arg_ids arg))) !graph;
scan_typquant (Type id) typq
| TD_record (id, typq, fields, _) ->
let field_nodes =
@@ -238,40 +260,44 @@ let add_def_to_graph graph def =
|> IdSet.elements
|> List.map (fun id -> Type id)
in
- graph := G.add_edges' (Type id) field_nodes !graph;
+ graph := G.add_edges (Type id) field_nodes !graph;
scan_typquant (Type id) typq
| TD_variant (id, typq, ctors, _) ->
let ctor_nodes =
List.map (fun (Tu_aux (Tu_ty_id (typ, id), _)) -> (typ_ids typ, id)) ctors
|> List.fold_left (fun (ids, ctors) (ids', ctor) -> (IdSet.union ids ids', IdSet.add ctor ctors)) (IdSet.empty, IdSet.empty)
in
- IdSet.iter (fun ctor_id -> graph := G.add_edge' (Constructor ctor_id) (Type id) !graph) (snd ctor_nodes);
- IdSet.iter (fun typ_id -> graph := G.add_edge' (Type id) (Type typ_id) !graph) (fst ctor_nodes);
+ IdSet.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) (snd ctor_nodes);
+ IdSet.iter (fun typ_id -> graph := G.add_edge (Type id) (Type typ_id) !graph) (fst ctor_nodes);
scan_typquant (Type id) typq
- | TD_enum (id, _, _) ->
- graph := G.add_edges' (Type id) [] !graph
+ | TD_enum (id, ctors, _) ->
+ List.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) ctors
| TD_bitfield _ ->
Reporting.unreachable l __POS__ "Bitfield should be re-written"
in
begin match def with
| DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) ->
- graph := G.add_edges' (Function id) [] !graph;
- IdSet.iter (fun typ_id -> graph := G.add_edge' (Function id) (Type typ_id) !graph) (typ_ids typ)
+ graph := G.add_edges (Function id) [] !graph;
+ IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ)
| DEF_fundef fdef ->
let id = id_of_fundef fdef in
- graph := G.add_edges' (Function id) [] !graph;
+ graph := G.add_edges (Function id) [] !graph;
ignore (rewrite_fun (rewriters (Function id)) fdef)
| DEF_val (LB_aux (LB_val (pat, exp), _) as lb) ->
let ids = pat_ids pat in
- IdSet.iter (fun id -> graph := G.add_edges' (Letbind id) [] !graph) ids;
+ IdSet.iter (fun id -> graph := G.add_edges (Letbind id) [] !graph) ids;
IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids
| DEF_type tdef ->
add_type_def_to_graph tdef
- | DEF_pragma _ -> ()
+ | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
+ IdSet.iter (fun typ_id -> graph := G.add_edge (Register id) (Type typ_id) !graph) (typ_ids typ)
+ | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
+ ignore (rewrite_exp (rewriters (Register id)) exp);
+ IdSet.iter (fun typ_id -> graph := G.add_edge (Register id) (Type typ_id) !graph) (typ_ids typ)
| _ -> ()
end;
- G.fix_leaves !graph
+ !graph
let rec graph_of_ast (Defs defs) =
let module G = Graph.Make(Node) in
@@ -283,8 +309,124 @@ let rec graph_of_ast (Defs defs) =
| [] -> G.empty
+let id_of_typedef (TD_aux (aux, _)) =
+ match aux with
+ | TD_abbrev (id, _, _) -> id
+ | TD_record (id, _, _, _) -> id
+ | TD_variant (id, _, _, _) -> id
+ | TD_enum (id, _, _) -> id
+ | TD_bitfield (id, _, _) -> id
+
+let id_of_reg_dec (DEC_aux (aux, _)) =
+ match aux with
+ | DEC_reg (_, _, _, id) -> id
+ | DEC_config (id, _, _) -> id
+ | _ -> assert false
+
+
+let filter_ast cuts g (Defs defs) =
+ let rec filter_ast' g =
+ let module NS = Set.Make(Node) in
+ let module NM = Map.Make(Node) in
+ function
+ | DEF_fundef fdef :: defs when NS.mem (Function (id_of_fundef fdef)) cuts -> filter_ast' g defs
+ | DEF_fundef fdef :: defs when NM.mem (Function (id_of_fundef fdef)) g -> DEF_fundef fdef :: filter_ast' g defs
+ | DEF_fundef _ :: defs -> filter_ast' g defs
+
+ | DEF_reg_dec rdec :: defs when NM.mem (Register (id_of_reg_dec rdec)) g -> DEF_reg_dec rdec :: filter_ast' g defs
+ | DEF_reg_dec _ :: defs -> filter_ast' g defs
+
+ | DEF_spec vs :: defs when NM.mem (Function (id_of_val_spec vs)) g -> DEF_spec vs :: filter_ast' g defs
+ | DEF_spec _ :: defs -> filter_ast' g defs
+
+ | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) :: defs ->
+ let ids = pat_ids pat |> IdSet.elements in
+ if List.exists (fun id -> NM.mem (Letbind id) g) ids then
+ DEF_val lb :: filter_ast' g defs
+ else
+ filter_ast' g defs
+
+ | DEF_type tdef :: defs when NM.mem (Type (id_of_typedef tdef)) g -> DEF_type tdef :: filter_ast' g defs
+ | DEF_type _ :: defs -> filter_ast' g defs
+
+ | DEF_measure (id,_,_) :: defs when NS.mem (Function id) cuts -> filter_ast' g defs
+ | (DEF_measure (id,_,_) as def) :: defs when NM.mem (Function id) g -> def :: filter_ast' g defs
+ | DEF_measure _ :: defs -> filter_ast' g defs
+
+ | def :: defs -> def :: filter_ast' g defs
+
+ | [] -> []
+ in
+ Defs (filter_ast' g defs)
+
let dot_of_ast out_chan ast =
let module G = Graph.Make(Node) in
let module NodeSet = Set.Make(Node) in
let g = graph_of_ast ast in
G.make_dot (node_color NodeSet.empty) edge_color node_string out_chan g
+
+let () =
+ let open Printf in
+ let open Interactive in
+ let slice_roots = ref IdSet.empty in
+ let slice_cuts = ref IdSet.empty in
+
+ ArgString ("identifiers", fun arg -> Action (fun () ->
+ let args = Str.split (Str.regexp " +") arg in
+ let ids = List.map mk_id args |> IdSet.of_list in
+ Specialize.add_initial_calls ids;
+ slice_roots := IdSet.union ids !slice_roots
+ )) |> register_command ~name:"slice_roots" ~help:"Set the roots for :slice";
+
+ ArgString ("identifiers", fun arg -> Action (fun () ->
+ let args = Str.split (Str.regexp " +") arg in
+ let ids = List.map mk_id args |> IdSet.of_list in
+ slice_cuts := IdSet.union ids !slice_cuts
+ )) |> register_command ~name:"slice_cuts" ~help:"Set the cuts for :slice";
+
+ Action (fun () ->
+ let module NodeSet = Set.Make(Node) in
+ let module G = Graph.Make(Node) in
+ let g = graph_of_ast !ast in
+ let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let g = G.prune roots cuts g in
+ ast := filter_ast cuts g !ast
+ ) |> register_command
+ ~name:"slice"
+ ~help:"Slice AST to the definitions which the functions given \
+ by :slice_roots depend on, up to the functions given \
+ by :slice_cuts";
+
+ Action (fun () ->
+ let module NodeSet = Set.Make(Node) in
+ let module NodeMap = Map.Make(Node) in
+ let module G = Graph.Make(Node) in
+ let g = graph_of_ast !ast in
+ let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> NodeSet.of_list in
+ let keep = function
+ | (Function id,_) when IdSet.mem id (!slice_roots) -> None
+ | (Function id,_) -> Some (Function id)
+ | _ -> None
+ in
+ let cuts = NodeMap.bindings g |> Util.map_filter keep |> NodeSet.of_list in
+ let g = G.prune roots cuts g in
+ ast := filter_ast cuts g !ast
+ ) |> register_command
+ ~name:"thin_slice"
+ ~help:(sprintf ":thin_slice - Slice AST to the function definitions given with %s" (command "slice_roots"));
+
+ ArgString ("format", fun arg -> Action (fun () ->
+ let format = if arg = "" then "svg" else arg in
+ let dotfile, out_chan = Filename.open_temp_file "sail_graph_" ".gz" in
+ let image = Filename.temp_file "sail_graph_" ("." ^ format) in
+ dot_of_ast out_chan !ast;
+ close_out out_chan;
+ let _ = Unix.system (Printf.sprintf "dot -T%s %s -o %s" format dotfile image) in
+ let _ = Unix.system (Printf.sprintf "xdg-open %s" image) in
+ ()
+ )) |> register_command
+ ~name:"graph"
+ ~help:"Draw a callgraph using dot in :0 (e.g. svg), and open with xdg-open"
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 14:26:24 +0000