Skip to content

Commit

Permalink
A new cross-workspace visibility flag
Browse files Browse the repository at this point in the history
msprotz committed Sep 20, 2024
1 parent a9206a0 commit 37a11a9
Showing 6 changed files with 68 additions and 11 deletions.
11 changes: 10 additions & 1 deletion lib/AstToMiniRust.ml
Original file line number Diff line number Diff line change
@@ -1218,6 +1218,15 @@ let bind_decl env (d: Ast.decl): env =
let translate_meta flags =
let comments = List.filter_map (function Common.Comment c -> Some c | _ -> None) flags in
let comments = List.filter ((<>) "") comments in
let comments = comments @
(* There is no notion of workspace visibility. *)
if List.mem Common.Workspace flags then
[ "ATTENTION: this function is public, but is intended for internal use \
within this workspace; callers should not rely on the availability of this \
function, or its behavior!" ]
else
[]
in
let visibility =
if List.mem Common.Private flags then
None
@@ -1271,12 +1280,12 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option =
None

| DType (lid, flags, _, _, decl) ->
(* creative naming for the lifetime *)
let name = lookup_type env lid in
let meta = translate_meta flags in
match decl with
| Flat _ ->
let lifetime =
(* creative naming for the lifetime *)
if Idents.LidSet.mem lid env.pointer_holding_structs then
Some (MiniRust.Label "a")
else
2 changes: 2 additions & 0 deletions lib/Common.ml
Original file line number Diff line number Diff line change
@@ -64,4 +64,6 @@ type flag =
| Target of string
(** Inserts target attribute. *)
| MustInline
| Workspace
(** Rust specific, not generated by F* *)
[@@deriving yojson,show]
56 changes: 47 additions & 9 deletions lib/Inlining.ml
Original file line number Diff line number Diff line change
@@ -192,6 +192,21 @@ let inline_analysis files =
in
must_inline, must_disappear

module StringMap = Map.Make(String)

(* After bundling, map filenames to crates *)
let mk_crate_of files =
List.fold_left (fun map (file, _) ->
StringMap.add file (List.find_map (fun (crate, members, _) ->
let crate = KList.one (KList.one crate) in
if List.exists (fun p -> Bundle.pattern_matches_file p file) members then begin
KPrint.bprintf "File %s goes into crate %s\n" file crate;
Some crate
end else
None
) (List.rev !Options.crates)) map
) StringMap.empty files

(** This phase is concerned with three whole-program, cross-compilation-unit
analyses, performed ina single pass:
- assign correct visibility to declarations in the presence of bundling,
@@ -204,9 +219,10 @@ let inline_analysis files =
let cross_call_analysis files =

let file_of = Bundle.mk_file_of files in
let crate_of = mk_crate_of files in

let module T = struct
type visibility = Private | Internal | Public
type visibility = Private | Internal | Workspace | Public
type inlining = Nope | Inline | StaticInline
type info = {
visibility: visibility;
@@ -272,17 +288,11 @@ let cross_call_analysis files =
| 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 v v' =
match v, v' with
| Private, _ -> v'
| _, Private -> v
| Internal, _ -> v'
| _, Internal -> v
| _ -> Public
in
let lub: visibility -> visibility -> visibility = max in

(* Set a lower a bound on the visibility of `lid`. *)
let raise lid v =
@@ -304,6 +314,24 @@ let cross_call_analysis files =
()
in

(* Is this a call across crate within the same workspace? *)
let cross_crate name1 name2 =
let file1 = file_of name1 in
let file2 = file_of name2 in
let crate1 = Option.bind file1 (fun file1 -> StringMap.find file1 crate_of) in
let crate2 = Option.bind file2 (fun file2 -> StringMap.find file2 crate_of) in
let should_drop = function
| Some f -> Drop.file f
| None -> false
in
let r = crate1 <> None && crate2 <> None && crate1 <> crate2 && not (should_drop file1 || should_drop file2) in
if r && Options.debug "visibility-fixpoint" then
KPrint.bprintf "[visibility-fixpoint] cross-crate from %a (%s) to %a (%s)\n"
plid name1 (Option.value ~default:"<none>" crate1)
plid name2 (Option.value ~default:"<none>" crate2);
r
in

(* Is this a call across compilation units? *)
let cross_call name1 name2 =
let file1 = file_of name1 in
@@ -365,6 +393,11 @@ let cross_call_analysis files =
scope for this definition to compile. *)
if cross_call lid name then
raise name Internal;
(* Using the multiple-crate, workspace feature of Rust code-gen. This
is a call across crates belonging to the same workspace -- the
definition needs to be visible across the whole workspace. *)
if cross_crate lid name && !Options.crates <> [] then
raise name Workspace;
(* Types that appear in prototypes (i.e., `not in_body`) must be
raised to the level of visibility of the current definition.
Types that appear in static inline function definitions (lhs of the
@@ -427,6 +460,9 @@ let cross_call_analysis files =
least through an internal header. *)
if cross_call lid name then
raise name Internal;
(* See above *)
if cross_crate lid name then
raise name Workspace;
(* Mutually recursive calls require the prototype to be in scope, at
least through the internal header. *)
if not (LidSet.mem name !seen) then
@@ -506,6 +542,8 @@ let cross_call_analysis files =
let flags = add_if (info.visibility = Private) Common.Private flags in
let flags = remove_if (info.visibility <> Internal) Common.Internal flags in
let flags = add_if (info.visibility = Internal) Common.Internal flags in
let flags = remove_if (info.visibility <> Workspace) Common.Workspace flags in
let flags = add_if (info.visibility = Workspace) Common.Workspace flags in
if Options.wasm () then
(* We override the previous logic in the case of WASM *)
let flags = remove_if info.wasm_mutable Common.Internal flags in
1 change: 1 addition & 0 deletions lib/Options.ml
Original file line number Diff line number Diff line change
@@ -35,6 +35,7 @@ let ldopts: string list ref = ref []
(* Note: do not populate this field directly but rather do it in Karamel.ml
* behind the "Options.minimal" test. *)
let bundle: Bundle.t list ref = ref []
let crates: Bundle.t list ref = ref []
let library: Bundle.pat list ref = ref []
let hand_written: Bundle.pat list ref = ref []
let debug_modules: string list ref = ref []
2 changes: 2 additions & 0 deletions lib/PrintAst.ml
Original file line number Diff line number Diff line change
@@ -155,6 +155,8 @@ and print_flag = function
string "__attribute__((unused))"
| Target s ->
string ("__attribute__((target = "^s^"))")
| Workspace ->
string "workspace"

and print_binder { typ; node = { name; mut; meta; mark; _ }} =
let o, u = !mark in
7 changes: 6 additions & 1 deletion src/Karamel.ml
Original file line number Diff line number Diff line change
@@ -248,7 +248,12 @@ Supported options:|}
" don't prepend the module name to declarations from module matching this \
pattern";
"-bundle", Arg.String (fun s -> prepend Options.bundle (Parsers.bundle s)), " \
group modules into a single C translation unit (see above)";
group F* modules into a single C translation unit or Rust file (see above)";
"-crate", Arg.String (fun s -> prepend Options.crates (Parsers.bundle s)), " \
adopt a Cargo workspace and group Rust files into a single sub-crate of \
that workspace (see above) -- no empty left-hand side allowed, and note \
that the right-hand side matches Rust file names (which may be the product \
of bundling), NOT F* module sources";
"-drop", Arg.String (fun s ->
used_drop := true;
List.iter (prepend Options.drop) (Parsers.drop s)),

0 comments on commit 37a11a9

Please sign in to comment.