C: Generate C from sliced specifications

1 files changed, 48 insertions, 13 deletions

diff --git a/src/slice.ml b/src/slice.ml
index 036b80d3..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,20 +288,50 @@ let rec graph_of_ast (Defs defs) =
 
   | [] -> G.empty
 
-let rec filter_ast' g =
-  let module NM = Map.Make(Node) in
-  function
-  | 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
+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
+
 
-  | 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
+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 :: defs -> def :: 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
 
-let filter_ast g (Defs defs) = 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