diff options
Diffstat (limited to 'src/slice.ml')
| -rw-r--r-- | src/slice.ml | 56 |
1 files changed, 53 insertions, 3 deletions
diff --git a/src/slice.ml b/src/slice.ml index f50104c4..fa574b7f 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -184,6 +184,7 @@ let add_def_to_graph graph def = | E_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 @@ -248,8 +249,8 @@ let add_def_to_graph graph def = 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 @@ -268,7 +269,11 @@ let add_def_to_graph graph def = 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 @@ -283,6 +288,51 @@ 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 NM = Map.Make(Node) in + function + | DEF_fundef fdef :: defs when IdSet.mem (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 :: 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 |