From 62907a102af929ec6fe20543e619db5db9715979 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 19 Feb 2025 15:04:40 -0500 Subject: [PATCH 1/3] Fix long-standing issue with C Abstract Structs --- krmllib/dist/generic/FStar_Issue.h | 2 ++ krmllib/dist/generic/FStar_Order.c | 2 ++ krmllib/dist/generic/FStar_Order.h | 1 - lib/Bundles.ml | 33 ++++++++++++++++++++----- lib/CStarToC11.ml | 15 ++++++------ lib/Inlining.ml | 5 ++-- lib/Options.ml | 3 ++- lib/Output.ml | 39 +++++++++++++++++------------- src/Karamel.ml | 7 +++++- 9 files changed, 71 insertions(+), 36 deletions(-) diff --git a/krmllib/dist/generic/FStar_Issue.h b/krmllib/dist/generic/FStar_Issue.h index c0e1bf70..6e0f8ae5 100644 --- a/krmllib/dist/generic/FStar_Issue.h +++ b/krmllib/dist/generic/FStar_Issue.h @@ -46,6 +46,8 @@ FStar_Issue_range_of_issue(FStar_Issue_issue i); extern Prims_list__Prims_string *FStar_Issue_context_of_issue(FStar_Issue_issue i); +extern FStar_Pprint_document FStar_Issue_issue_to_doc(FStar_Issue_issue i); + extern Prims_string FStar_Issue_render_issue(FStar_Issue_issue i); extern FStar_Issue_issue diff --git a/krmllib/dist/generic/FStar_Order.c b/krmllib/dist/generic/FStar_Order.c index 45d4fe3e..04862dff 100644 --- a/krmllib/dist/generic/FStar_Order.c +++ b/krmllib/dist/generic/FStar_Order.c @@ -6,6 +6,8 @@ #include "FStar_Order.h" +#include "Prims.h" + bool FStar_Order_uu___is_Lt(FStar_Order_order projectee) { switch (projectee) diff --git a/krmllib/dist/generic/FStar_Order.h b/krmllib/dist/generic/FStar_Order.h index 397f44ee..8ff40892 100644 --- a/krmllib/dist/generic/FStar_Order.h +++ b/krmllib/dist/generic/FStar_Order.h @@ -7,7 +7,6 @@ #ifndef __FStar_Order_H #define __FStar_Order_H -#include "Prims.h" #include #include "krmllib.h" #include "krml/internal/compat.h" diff --git a/lib/Bundles.ml b/lib/Bundles.ml index 23267b82..6606ab38 100644 --- a/lib/Bundles.ml +++ b/lib/Bundles.ml @@ -254,8 +254,8 @@ let empty_deps = { internal = StringSet.empty; public = StringSet.empty } let drop_dinstinction { internal; public } = List.of_seq (StringSet.to_seq (StringSet.union internal public)) -class record_everything gen_dep = object - inherit [_] reduce +class record_everything (gen_dep: ?constructor:unit -> lident -> _) = object(self) + inherit [_] reduce as super method plus { internal = i1; public = p1 } { internal = i2; public = p2 } = { internal = StringSet.union i1 i2; public = StringSet.union p1 p2 } method zero = empty_deps @@ -265,6 +265,14 @@ class record_everything gen_dep = object gen_dep lid method! visit_TApp () lid _ = gen_dep lid + method! visit_EFlat ((_, t) as env) fields = + match t with + | TQualified lid -> + self#plus + (gen_dep ~constructor:() lid) + (super#visit_EFlat env fields) + | _ -> + super#visit_EFlat env fields end let direct_dependencies_with_internal files file_of = @@ -278,15 +286,24 @@ let direct_dependencies_with_internal files file_of = ) set decls ) LidSet.empty files in + let c_abstract_struct = List.fold_left (fun set (_, decls) -> + List.fold_left (fun set decl -> + if List.mem Common.AbstractStruct (Ast.flags_of_decl decl) then + LidSet.add (Ast.lid_of_decl decl) set + else + set + ) set decls + ) LidSet.empty files in + List.fold_left (fun by_file file -> - let gen_dep (callee: lident) = + let gen_dep ?constructor (callee: lident) = match file_of callee with | Some f when f <> fst file && not (Helpers.is_primitive callee) -> let is_internal = LidSet.mem callee internal in if Options.debug "dependencies" then KPrint.bprintf "In file %s, reference to %a (in %sheader %s)\n" (fst file) PrintAst.plid callee (if is_internal then "internal " else "") f; - if is_internal then + if is_internal || constructor = Some () && LidSet.mem callee c_abstract_struct then { empty_deps with internal = StringSet.singleton f } else { empty_deps with public = StringSet.singleton f } @@ -318,11 +335,15 @@ let direct_dependencies_with_internal files file_of = method! visit_DType env name flags n_cgs n def = let is_c_abstract_struct = List.mem Common.AbstractStruct flags in - if self#concerns_us flags then - if is_c_abstract_struct then + if is_c_abstract_struct then + (* In `header_deps`, a C abstract struct always concerns us because it appears both in the + public (forward declaration, no body) and in the internal header (actual declaration). *) + if which = `Public then super#visit_DType env name flags n_cgs n (Abbrev TUnit) else super#visit_DType env name flags n_cgs n def + else if self#concerns_us flags then + super#visit_DType env name flags n_cgs n def else super#zero diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml index f4545166..76c37225 100644 --- a/lib/CStarToC11.ml +++ b/lib/CStarToC11.ml @@ -1391,9 +1391,9 @@ let either f1 f2 x = | [] -> f2 x | l -> l -let if_private_or_abstract_struct f d = +let if_private f d = let flags = flags_of_decl d in - if List.mem Private flags || List.mem AbstractStruct flags then + if List.mem Private flags then f d else [] @@ -1404,8 +1404,9 @@ let if_public f d = else [] -let if_internal f d = - if List.mem Internal (flags_of_decl d) then +let if_internal_or_abstract_struct f d = + let flags = flags_of_decl d in + if List.mem Internal flags || List.mem AbstractStruct flags then (* let _ = KPrint.bprintf "%a is internal\n" PrintAst.Ops.plid (lid_of_decl d) in *) f d else @@ -1448,7 +1449,7 @@ let mk_file m decls = none (either (mk_function_or_global_body m) - (if_private_or_abstract_struct (mk_type_or_external m C)))) + (if_private (mk_type_or_external m C)))) decls let mk_files (map: GlobalNames.mapping) files = @@ -1500,10 +1501,10 @@ let mk_public_header (m: GlobalNames.mapping) decls = (* Private part if not already a static header, empty otherwise. *) let mk_internal_header (m: GlobalNames.mapping) decls = List.concat_map - (if_internal ( + (if_internal_or_abstract_struct ( (if_header_inline_static m (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C))) - (either (mk_function_or_global_stub m) (mk_type_or_external m H))))) + (either (mk_function_or_global_stub m) (mk_type_or_external m C))))) decls let mk_headers (map: GlobalNames.mapping) diff --git a/lib/Inlining.ml b/lib/Inlining.ml index 15c919b9..47d9b3f7 100644 --- a/lib/Inlining.ml +++ b/lib/Inlining.ml @@ -492,9 +492,8 @@ let cross_call_analysis files = (visit true)#visit_expr_w () e | DExternal (_, _, _, _, _, t, _) -> (visit false)#visit_typ () t - | DType (_, flags, _, _, d) -> - if not (List.mem Common.AbstractStruct flags) then - (visit false)#visit_type_def () d + | DType (_, _, _, _, d) -> + (visit false)#visit_type_def () d end; seen := LidSet.add lid !seen ) decls diff --git a/lib/Options.ml b/lib/Options.ml index e9ea07ce..fb344505 100644 --- a/lib/Options.ml +++ b/lib/Options.ml @@ -1,10 +1,11 @@ (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *) (* Licensed under the Apache 2.0 and MIT Licenses. *) -type include_ = All | HeaderOnly of string | COnly of string +type include_ = All | InternalOnly of string | HeaderOnly of string | COnly of string let pinc b = function | All -> Buffer.add_string b "*" + | InternalOnly h | HeaderOnly h -> Buffer.add_string b h; Buffer.add_string b ".h" | COnly h -> Buffer.add_string b h; Buffer.add_string b ".c" diff --git a/lib/Output.ml b/lib/Output.ml index 991eaf0e..8b22f21a 100644 --- a/lib/Output.ml +++ b/lib/Output.ml @@ -6,19 +6,24 @@ open Utils open PPrint +type which = H | InternalH | C + let mk_includes = separate_map hardline (fun x -> string "#include " ^^ string x) -let filter_includes ~is_c file (includes: (Options.include_ * string) list) = +let filter_includes which file (includes: (Options.include_ * string) list) = (* KPrint.bprintf "-- filter_includes for %s (%d)\n" file (List.length includes); *) KList.filter_some (List.rev_map (function - | Options.HeaderOnly file', h when file = file' && not is_c -> + | Options.HeaderOnly file', h when file = file' && which = H -> + (* KPrint.bprintf "--- H Match %s: include %s\n" file h; *) + Some h + | InternalOnly file', h when file = file' && which = InternalH -> (* KPrint.bprintf "--- H Match %s: include %s\n" file h; *) Some h - | COnly file', h when file = file' && is_c -> + | COnly file', h when file = file' && which = C-> (* KPrint.bprintf "--- C Match %s: include %s\n" file h; *) Some h - | All, h when not is_c -> + | All, h when which = H -> (* KPrint.bprintf "--- All Match %s: include %s\n" file h; *) Some h | _i, _h -> @@ -37,8 +42,8 @@ let krmllib_include () = * - #include X for X in the dependencies of the file, followed by * - #include Y for each -add-include Y passed on the command-line *) -let includes_for ~is_c file files = - let extra_includes = filter_includes ~is_c file !Options.add_include in +let includes_for which file files = + let extra_includes = filter_includes which file !Options.add_include in let includes = List.rev_map (Printf.sprintf "\"%s.h\"") files in let includes = includes @ extra_includes in if includes = [] then @@ -46,8 +51,8 @@ let includes_for ~is_c file files = else mk_includes includes ^^ hardline ^^ hardline -let early_includes_for ~is_c file = - let includes = filter_includes ~is_c file !Options.add_early_include in +let early_includes_for which file = + let includes = filter_includes which file !Options.add_early_include in if includes = [] then empty else @@ -85,7 +90,7 @@ let header (): string = * and a footer, containing: * - the #endif *) -let prefix_suffix original_name name = +let prefix_suffix which original_name name = Driver.detect_fstar_if (); Driver.detect_karamel_if (); let if_cpp doc = @@ -101,7 +106,7 @@ let prefix_suffix original_name name = string (Printf.sprintf "#define __%s_H" macro_name) ^^ hardline ^^ (if !Options.extern_c then hardline ^^ if_cpp (string "extern \"C\" {") else empty) ^^ hardline ^^ - early_includes_for ~is_c:false original_name ^^ + early_includes_for which original_name ^^ krmllib_include () in let suffix = @@ -149,7 +154,7 @@ let write_c files internal_headers (deps: Bundles.all_deps Bundles.StringMap.t) let internal_deps = List.of_seq (Bundles.StringSet.to_seq all_deps.Bundles.c.Bundles.internal) in let public_deps = List.of_seq (Bundles.StringSet.to_seq all_deps.Bundles.c.Bundles.public) in let deps = List.map (fun f -> "internal/" ^ f) internal_deps @ public_deps in - let includes = includes_for ~is_c:true name deps in + let includes = includes_for C name deps in let header = string (header ()) ^^ hardline ^^ hardline in let internal = if Bundles.StringSet.mem name internal_headers then "internal/" else "" in (* If there is an internal header, we include that rather than the public @@ -157,7 +162,7 @@ let write_c files internal_headers (deps: Bundles.all_deps Bundles.StringMap.t) let my_h = string (Printf.sprintf "#include \"%s%s.h\"" internal name) in let prefix = header ^^ - early_includes_for ~is_c:true name ^^ + early_includes_for C name ^^ (if !Options.add_include_tmh then string "#ifdef WPP_CONTROL_GUIDS" ^^ hardline ^^ string (Printf.sprintf "#include <%s.tmh>" name) ^^ hardline ^^ @@ -182,7 +187,7 @@ let write_h files public_headers (deps: Bundles.all_deps Bundles.StringMap.t) = let public = List.of_seq (Bundles.StringSet.to_seq public) in let internal = List.of_seq (Bundles.StringSet.to_seq internal) in let original_name = name in - let name, program, deps = + let name, program, deps, which = match program with | C11.Internal h -> (* Internal header depends on public header + other internal headers. @@ -196,13 +201,13 @@ let write_h files public_headers (deps: Bundles.all_deps Bundles.StringMap.t) = else public @ internal_headers in - "internal/" ^ name, h, headers + "internal/" ^ name, h, headers, InternalH | C11.Public h -> - name, h, public + name, h, public, H in (* KPrint.bprintf "- write_h: %s\n" name; *) - let includes = includes_for ~is_c:false original_name deps in - let prefix, suffix = prefix_suffix original_name name in + let includes = includes_for which original_name deps in + let prefix, suffix = prefix_suffix which original_name name in write_one (name ^ ".h") (prefix ^^ includes) program suffix; name ) files diff --git a/src/Karamel.ml b/src/Karamel.ml index 18f6faac..44e6ef73 100644 --- a/src/Karamel.ml +++ b/src/Karamel.ml @@ -179,7 +179,12 @@ Supported options:|} | Some h -> COnly h, i | None -> - HeaderOnly h, i + begin match Filename.chop_suffix_opt ~suffix:".h" h with + | Some h -> + InternalOnly h, i + | None -> + HeaderOnly h, i + end end | [ i ] -> All, i | _ -> failwith ("Invalid -add-[early-|]include argument: " ^ s) From 43021128f00ff2b26435b656850a8741a630d190 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 20 Feb 2025 14:57:19 -0500 Subject: [PATCH 2/3] What would need to work to fix this --- test/AbstractStruct2.fst | 2 +- test/AbstractStructAbstract.fsti | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/test/AbstractStruct2.fst b/test/AbstractStruct2.fst index 70cd179c..921a69cb 100644 --- a/test/AbstractStruct2.fst +++ b/test/AbstractStruct2.fst @@ -4,7 +4,7 @@ module B = LowStar.Buffer open FStar.HyperStack.ST -[@@CAbstractStruct] +[@CAbstractStruct] noeq type handle = { something: bool; diff --git a/test/AbstractStructAbstract.fsti b/test/AbstractStructAbstract.fsti index 787cafe8..72424aec 100644 --- a/test/AbstractStructAbstract.fsti +++ b/test/AbstractStructAbstract.fsti @@ -1,5 +1,6 @@ module AbstractStructAbstract +[@CAbstractStruct] val t (a:Type0) : Type0 val make (#a:Type0) (x:a) : t a From 4036428f2909a4f795dbde2e80c936f01e103874 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 26 Feb 2025 17:23:44 -0800 Subject: [PATCH 3/3] More subtleties related to CAbstractStruct Notably, allow specifying flags for monomorphizations via type abbreviations --- lib/Inlining.ml | 54 +++++++++++++++++++++++++++++------------ lib/Monomorphization.ml | 21 ++++++++-------- 2 files changed, 50 insertions(+), 25 deletions(-) diff --git a/lib/Inlining.ml b/lib/Inlining.ml index 47d9b3f7..607c5be0 100644 --- a/lib/Inlining.ml +++ b/lib/Inlining.ml @@ -223,10 +223,18 @@ let cross_call_analysis files = inlining: inlining; wasm_mutable: bool; wasm_needs_getter: bool; + abstract_struct: bool; } end in let open T in + let pvis b = function + | Private -> Buffer.add_string b "Private" + | Internal -> Buffer.add_string b "Internal" + | Public -> Buffer.add_string b "Public" + | Workspace -> Buffer.add_string b "Workspace" + in + (* We associate to each declaration some initial information. Three fields may change after initially filling the map: - visibility may go upward along the visibility lattice (this is only a @@ -238,14 +246,19 @@ let cross_call_analysis files = let info_map = Helpers.build_map files (fun map d -> let f = flags_of_decl d in let name = lid_of_decl d in + let abstract_struct = List.mem Common.AbstractStruct f in let visibility = - if List.mem Common.Private f then - Private - else if List.mem Common.Internal f then + if List.mem Common.Internal f || abstract_struct then + (* C abstract structs start at internal, since their body is going to be in the internal + header. *) Internal + else if List.mem Common.Private f then + Private else Public in + if Options.debug "visibility-fixpoint" then + KPrint.bprintf "[initial visibility] %a: %a\n" plid name pvis visibility; let inlining = let is_static_inline = Helpers.is_static_header name in let is_inline = List.mem Common.Inline f || List.mem Common.MustInline f in @@ -269,7 +282,7 @@ let cross_call_analysis files = in let wasm_needs_getter = false in let callers = LidSet.empty in - Hashtbl.add map (lid_of_decl d) { visibility; inlining; wasm_mutable; wasm_needs_getter; callers } + Hashtbl.add map (lid_of_decl d) { visibility; inlining; wasm_mutable; wasm_needs_getter; callers; abstract_struct } ) in (* We keep track of the declarations we have seen so far. Since the @@ -277,13 +290,6 @@ let cross_call_analysis files = another function indicates that there is mutual recursion. *) let seen = ref LidSet.empty in - let pvis b = function - | Private -> Buffer.add_string b "Private" - | Internal -> Buffer.add_string b "Internal" - | Public -> Buffer.add_string b "Public" - | Workspace -> Buffer.add_string b "Workspace" - in - (* T.Visibility forms a trivial lattice where Private <= Internal <= Public *) let lub: visibility -> visibility -> visibility = max in @@ -301,6 +307,10 @@ let cross_call_analysis files = let record_call_from_to caller callee = try let info = Hashtbl.find info_map callee in + if Options.debug "visibility-fixpoint" then + KPrint.bprintf "[visibility-fixpoint] recording cross-call from %a (%s) to %a (%s)\n" + plid caller (Option.value ~default:"" (file_of caller)) + plid callee (Option.value ~default:"" (file_of callee)); Hashtbl.replace info_map callee { info with callers = LidSet.add caller info.callers } with Not_found -> (* External type currently modeled as an lid without a definition (sigh) *) @@ -492,7 +502,7 @@ let cross_call_analysis files = (visit true)#visit_expr_w () e | DExternal (_, _, _, _, _, t, _) -> (visit false)#visit_typ () t - | DType (_, _, _, _, d) -> + | DType (_, _flags, _, _, d) -> (visit false)#visit_type_def () d end; seen := LidSet.add lid !seen @@ -513,7 +523,13 @@ let cross_call_analysis files = if not (Hashtbl.mem info_map lid) then Warn.fatal_error "No equation for %a" plid lid; let info = Hashtbl.find info_map lid in - LidSet.fold (fun caller v -> lub v (valuation caller)) info.callers info.visibility + let adjust caller = + if (Hashtbl.find info_map caller).abstract_struct then + Internal + else + valuation caller + in + LidSet.fold (fun caller v -> lub v (adjust caller)) info.callers info.visibility ) in (* Adjust definitions based on `info_map` updated with fixpoint *) @@ -521,13 +537,21 @@ let cross_call_analysis files = f, List.map (fun d -> let lid = lid_of_decl d in let info = Hashtbl.find info_map lid in + let old_vis = info.visibility in + (* Fixpoint computation *) let info = { info with visibility = valuation (lid_of_decl d) } in + (* C abstract structs are treated as internal for the purposes of visibility computation, + but the convention is that they end up being marked as public for CStarToC11 to do the + right thing. (This may need fixing.) *) + let info = { info with visibility = if info.abstract_struct then Public else info.visibility } in if Options.debug "visibility-fixpoint" then - KPrint.bprintf "[adjustment]: %a: %a, wasm: mut %b getter %b\n" - plid lid pvis info.visibility info.wasm_mutable info.wasm_needs_getter; + KPrint.bprintf "[adjustment]: %a: %a --> %a, wasm: mut %b getter %b\n" + plid lid pvis old_vis pvis info.visibility info.wasm_mutable info.wasm_needs_getter; + let remove_if cond flag flags = if cond then List.filter ((<>) flag) flags else flags in let add_if cond flag flags = if cond && not (List.mem flag flags) then flag :: flags else flags in let adjust flags = + let flags = remove_if (info.inlining = Nope) Common.Inline flags in let flags = remove_if (info.inlining = Nope) Common.MustInline flags in let flags = remove_if (info.visibility <> Private) Common.Private flags in diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index cd124f9f..d4c8365c 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -248,7 +248,7 @@ let monomorphize_data_types map = object(self) (* Current file, for warning purposes. *) val mutable current_file = "" (* Possibly populated with something relevant *) - val mutable best_hint: node * lident = (dummy_lid, [], []), dummy_lid + val mutable best_hint: node * lident * flag list = (dummy_lid, [], []), dummy_lid, [] (* For forward references, a map from lid to its pending monomorphizations (type arguments) *) val pending_monomorphizations: (lident, (typ list * cg list)) Hashtbl.t = Hashtbl.create 41 @@ -314,15 +314,15 @@ let monomorphize_data_types map = object(self) let lid, ts, cgs = n in if ts = [] && cgs = [] then lid, [] - else if fst best_hint = n then - snd best_hint, [] + else if fst3 best_hint = n then + snd3 best_hint, [] else let name, flags = NameGen.gen_lid lid ts (Cg cgs) in if Options.debug "monomorphization" then KPrint.bprintf "No hint provided for %a\n current best hint: %a -> %a\n picking: %a\n" ptyp (fold_tapp (lid, ts, [])) - ptyp (fold_tapp (fst best_hint)) - plid (snd best_hint) + ptyp (fold_tapp (fst3 best_hint)) + plid (snd3 best_hint) plid name; name, flags @@ -345,6 +345,7 @@ let monomorphize_data_types map = object(self) if Options.debug "data-types-traversal" then KPrint.bprintf "visiting %a: Not_found\n" ptyp (fold_tapp n); let chosen_lid, flag = self#lid_of n in + let flag = if fst3 best_hint = n then thd3 best_hint @ flag else flag in if lid = tuple_lid then begin Hashtbl.add state n (Gray, chosen_lid, false); let args = List.map (self#visit_typ under_ref) args in @@ -450,16 +451,16 @@ let monomorphize_data_types map = object(self) if Options.debug "data-types-traversal" then KPrint.bprintf "decl %a\n" plid (lid_of_decl d); match d with - | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) -> + | DType (lid, flags, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) -> Hashtbl.remove map lid; if Options.debug "monomorphization" then KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args)); - best_hint <- (tuple_lid, args, []), lid; + best_hint <- (tuple_lid, args, []), lid, flags; ignore (self#visit_node false (tuple_lid, args, [])); Hashtbl.add seen_declarations lid (); self#clear () - | DType (lid, _, 0, 0, Abbrev ((TApp _ | TCgApp _) as t)) when not (Hashtbl.mem state (flatten_tapp t)) -> + | DType (lid, flags, 0, 0, Abbrev ((TApp _ | TCgApp _) as t)) when not (Hashtbl.mem state (flatten_tapp t)) -> (* We have not yet monomorphized this type, and conveniently, we have a type abbreviation that provides us with a name hint! We simply ditch the type abbreviation and replace it with a monomorphization @@ -478,9 +479,9 @@ let monomorphize_data_types map = object(self) let abbrev_for_gc_type = Hashtbl.mem map hd && List.mem Common.GcType (fst (Hashtbl.find map hd)) in if abbrev_for_gc_type then - best_hint <- (hd, args, cgs), (fst lid, snd lid ^ "_gc") + best_hint <- (hd, args, cgs), (fst lid, snd lid ^ "_gc"), flags else - best_hint <- (hd, args, cgs), lid; + best_hint <- (hd, args, cgs), lid, flags; ignore (self#visit_node false (hd, args, cgs));