Skip to content

Commit

Permalink
Merge pull request #403 from FStarLang/protz_cg
Browse files Browse the repository at this point in the history 
Adding support for const generics in order to support Rust-->C use-case
  • Loading branch information
@msprotz
msprotz authored Dec 22, 2023
2 parents 67b19d9 + 0eebaa9 commit 5c7ac22
Show file tree
Hide file tree
Showing 28 changed files with 728 additions and 414 deletions.
73 changes: 50 additions & 23 deletions lib/Ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,12 @@ and valuation = Mark.occurrence * Mark.usage [@ opaque]

let dummy_lid = [], ""

type cg =
| CgVar of int
| CgConst of constant

(* The visitor of types composes with the misc. visitor. *)
type typ =
and typ =
| TInt of width
| TBool
| TUnit
Expand All @@ -51,12 +55,16 @@ type typ =
| TArray of typ * constant
(** appears when we start hoisting buffer definitions to their enclosing
* push frame *)
| TCgArray of typ * int
(** for monomorphization of stuff coming from Rust (eurydice) *)
| TQualified of lident
(** a reference to a type that has been introduced via a DType *)
| TArrow of typ * typ
(** t1 -> t2 *)
| TApp of lident * typ list
(** disappears after monomorphization *)
| TCgApp of typ * cg
(** typ is either TCgApp, TApp, or TQualified *)
| TBound of int
(** appears in type definitions... also disappears after monorphization *)
| TTuple of typ list
Expand Down Expand Up @@ -189,7 +197,7 @@ type expr' =
| EIgnore of expr

| EApp of expr * expr list
| ETApp of expr * typ_wo list
| ETApp of expr * expr list * typ_wo list
| EPolyComp of poly_comp * typ_wo
| ELet of binder * expr * expr
| EFun of binder list * expr * typ_wo
Expand Down Expand Up @@ -344,8 +352,8 @@ class ['self] map_expr_adapter = object (self: 'self)
let node = f (env, typ) x.node in
{ node; typ }

method visit_expr_w =
self#lift_w self#visit_expr'
method visit_expr_w env e =
self#visit_expr (env, e.typ) e

method visit_binder_w =
self#lift_w self#visit_binder'
Expand Down Expand Up @@ -416,12 +424,12 @@ and files =
file list

and decl =
| DFunction of calling_convention option * flag list * int * typ * lident * binders_w * expr_w
| DFunction of calling_convention option * flag list * int * int * typ * lident * binders_w * expr_w
| DGlobal of flag list * lident * int * typ * expr_w
| DExternal of calling_convention option * flag list * int * lident * typ * string list
| DExternal of calling_convention option * flag list * int * int * lident * typ * string list
(** String list: only for pretty-printing purposes, names of the first few
* known arguments. *)
| DType of lident * flag list * int * type_def
| DType of lident * flag list * int * int * type_def

and binders_w = binder_w list

Expand Down Expand Up @@ -496,14 +504,14 @@ class ['self] map = object (self: 'self)
let e = self#visit_expr env e in
bs, p, e

method! visit_DType env lid flags n d =
method! visit_DType env lid flags n_cg n d =
let lid = self#visit_lident env lid in
let flags = self#visit_flags env flags in
let env = self#extend_tmany env n in
let d = self#visit_type_def env d in
DType (lid, flags, n, d)
DType (lid, flags, n_cg, n, d)

method! visit_DFunction env cc flags n t lid bs e =
method! visit_DFunction env cc flags n_cg n t lid bs e =
let cc = self#visit_calling_convention_option env cc in
let flags = self#visit_flags env flags in
let env = self#extend_tmany env n in
Expand All @@ -512,13 +520,14 @@ class ['self] map = object (self: 'self)
let bs = self#visit_binders_w env bs in
let env = self#extend_many env bs in
let e = self#visit_expr_w env e in
DFunction (cc, flags, n, t, lid, bs, e)
DFunction (cc, flags, n_cg, n, t, lid, bs, e)

method! visit_ETApp env e ts =
method! visit_ETApp env e es ts =
let ts = List.map (self#visit_typ_wo env) ts in
let es = List.map (self#visit_expr env) es in
let env = self#extend_tmany (fst env) (List.length ts) in
let e = self#visit_expr_w env e in
ETApp (e, ts)
ETApp (e, es, ts)
end

class ['self] iter = object (self: 'self)
Expand Down Expand Up @@ -551,13 +560,13 @@ class ['self] iter = object (self: 'self)
self#visit_pattern env p;
self#visit_expr env e

method! visit_DType env lid flags n d =
method! visit_DType env lid flags _n_cg n d =
self#visit_lident env lid;
self#visit_flags env flags;
let env = self#extend_tmany env n in
self#visit_type_def env d

method! visit_DFunction env cc flags n t lid bs e =
method! visit_DFunction env cc flags _n_cg n t lid bs e =
self#visit_calling_convention_option env cc;
self#visit_flags env flags;
let env = self#extend_tmany env n in
Expand Down Expand Up @@ -602,14 +611,14 @@ class virtual ['self] reduce = object (self: 'self)
let e = self#visit_expr env e in
KList.reduce self#plus [ bs'; p; e ]

method! visit_DType env lid flags n d =
method! visit_DType env lid flags _n_cg n d =
let lid = self#visit_lident env lid in
let flags = self#visit_flags env flags in
let env = self#extend_tmany env n in
let d = self#visit_type_def env d in
KList.reduce self#plus [ lid; flags; d ]

method! visit_DFunction env cc flags n t lid bs e =
method! visit_DFunction env cc flags _n_cg n t lid bs e =
let cc = self#visit_calling_convention_option env cc in
let flags = self#visit_flags env flags in
let env = self#extend_tmany env n in
Expand All @@ -633,18 +642,36 @@ let map_decls f files =
let with_type typ node =
{ typ; node }

let flatten_tapp t =
let rec flatten_tapp cgs t =
match t with
| TApp (lid, ts) ->
lid, ts, List.rev cgs
| TCgApp (t, cg) ->
flatten_tapp (cg :: cgs) t
| TQualified lid ->
lid, [], List.rev cgs
| _ ->
invalid_arg "flatten_tapp"
in
flatten_tapp [] t

let fold_tapp (lid, ts, cgs) =
let t = if ts = [] then TQualified lid else TApp (lid, ts) in
List.fold_right (fun cg t -> TCgApp (t, cg)) cgs t

let lid_of_decl = function
| DFunction (_, _, _, _, lid, _, _)
| DFunction (_, _, _, _, _, lid, _, _)
| DGlobal (_, lid, _, _, _)
| DExternal (_, _, _, lid, _, _)
| DType (lid, _, _, _) ->
| DExternal (_, _, _, _, lid, _, _)
| DType (lid, _, _, _, _) ->
lid

let flags_of_decl = function
| DFunction (_, flags, _, _, _, _, _)
| DFunction (_, flags, _, _, _, _, _, _)
| DGlobal (flags, _, _, _, _)
| DType (_, flags, _, _)
| DExternal (_, flags, _, _, _, _) ->
| DType (_, flags, _, _, _)
| DExternal (_, flags, _, _, _, _, _) ->
flags

let tuple_lid = [ "K" ], ""
20 changes: 11 additions & 9 deletions lib/AstToCFlat.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -340,7 +340,7 @@ let name_flat_layouts = object (self)
List.concat_map (fun d ->
current_prefix <- fst (lid_of_decl d);
let d = self#visit_decl () d in
let ds: decl list = List.map (fun (name, fields) -> DType (name, [], 0, Flat fields)) new_decls in
let ds: decl list = List.map (fun (name, fields) -> DType (name, [], 0, 0, Flat fields)) new_decls in
new_decls <- [];
List.rev_append ds [ d ]
) decls
Expand All @@ -352,7 +352,7 @@ let populate env files =
let env = List.fold_left (fun env (_, decls) ->
List.fold_left (fun env decl ->
match decl with
| DType (_, _, _, Enum idents) ->
| DType (_, _, _, _, Enum idents) ->
KList.fold_lefti (fun i env ident ->
assert (i < 256);
{ env with enums = LidMap.add ident i env.enums }
Expand All @@ -369,9 +369,9 @@ let populate env files =
let env = List.fold_left (fun env (_, decls) ->
List.fold_left (fun env decl ->
match decl with
| DType (lid, _, _, Enum _) ->
| DType (lid, _, _, _, Enum _) ->
{ env with layouts = LidMap.add lid LEnum env.layouts }
| DType (lid, _, _, Flat fields) ->
| DType (lid, _, _, _, Flat fields) ->
(* Need to pass in the layout of previous structs *)
begin try
let l = flat_layout env (fields_of_struct fields) in
Expand Down Expand Up @@ -723,13 +723,15 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr =
| EOpen _ ->
invalid_arg "mk_expr (EOpen)"

| EApp ({ node = ETApp ({ node = EQualified (["LowStar"; "Ignore"],"ignore"); _ }, _); _ }, [ e ]) ->
| EApp ({ node = ETApp ({ node = EQualified (["LowStar"; "Ignore"],"ignore"); _ }, cgs, _); _ }, [ e ]) ->
assert (cgs = []);
let locals, e = mk_expr env locals e in
(* This is slightly ill-typed since everywhere else the result of
intermediary sequence bits is units, but that's fine *)
locals, CF.Sequence [ e; cflat_unit ]

| EApp ({ node = ETApp ({ node = EQualified (["Lib"; "Memzero0"],"memzero"); _ }, _); _ }, [ dst; len ]) ->
| EApp ({ node = ETApp ({ node = EQualified (["Lib"; "Memzero0"],"memzero"); _ }, cgs, _); _ }, [ dst; len ]) ->
assert (cgs = []);
(* TODO: now that the C backend is generic for type applications, do the
same here and have generic support for ETApp. Idea: reuse the JSON
representation of a type (used for layouts) and pass that to the JS
Expand Down Expand Up @@ -1026,8 +1028,8 @@ let mk_wrapper orig_name n_args locals =

let mk_decl env (d: decl): env * CF.decl list =
match d with
| DFunction (_, flags, n, ret, name, args, body) ->
assert (n = 0);
| DFunction (_, flags, n_cgs, n, ret, name, args, body) ->
assert (n = 0 && n_cgs = 0);
let public = not (List.mem Common.Private flags) in
let locals, env = List.fold_left (fun (locals, env) b ->
let locals, _, env = extend env b locals in
Expand Down Expand Up @@ -1076,7 +1078,7 @@ let mk_decl env (d: decl): env * CF.decl list =
CF.Global (name, size, body, post_init, public)
]

| DExternal (_, _, _, lid, t, _) ->
| DExternal (_, _, _, _, lid, t, _) ->
let name = GlobalNames.to_c_name env.names lid in
match t with
| TArrow _ ->
Expand Down
30 changes: 20 additions & 10 deletions lib/AstToCStar.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -358,11 +358,15 @@ and mk_expr env in_stmt e =
| EConstant c ->
CStar.Constant c

| EApp ({ node = ETApp (e, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e ->
unit_to_void env e es (List.map (fun t -> CStar.Type (mk_type env t)) ts)
| EApp ({ node = ETApp (e0, cgs, ts); _ }, es) when !Options.allow_tapps || whitelisted_tapp e0 ->
(* Return type is oftentimes very useful when having to build a return value using e.g. a
compound literal *)
let ret_t = CStar.Type (mk_type env (MonomorphizationState.resolve e.typ)) in
unit_to_void env e0 (cgs @ es) (List.map (fun t -> CStar.Type (mk_type env t)) ts @ [ ret_t ])

| ETApp (e, ts) when !Options.allow_tapps || whitelisted_tapp e ->
CStar.Call (mk_expr env e, List.map (fun t -> CStar.Type (mk_type env t)) ts)
| ETApp (e0, cgs, ts) when !Options.allow_tapps || whitelisted_tapp e0 ->
let ret_t = CStar.Type (mk_type env (MonomorphizationState.resolve e.typ)) in
unit_to_void env e0 cgs (List.map (fun t -> CStar.Type (mk_type env t)) ts @ [ ret_t ])

| EApp ({ node = EOp (op, w); _ }, [ _; _ ]) when is_arith op w ->
fst (mk_arith env e)
Expand Down Expand Up @@ -802,6 +806,10 @@ and mk_return_type env = function
fatal_error "Internal failure: TTuple not desugared here"
| TAnonymous t ->
mk_type_def env t
| TCgArray _ ->
CStar.Qualified (["Eurydice"], "error_t_cg_array")
| TCgApp _ ->
fatal_error "Internal failure: TCgApp not desugared here"


and mk_type env = function
Expand Down Expand Up @@ -876,8 +884,8 @@ and mk_declaration m env d: (CStar.decl * _) option =
in

match d with
| DFunction (cc, flags, n, t, name, binders, body) ->
assert (n = 0);
| DFunction (cc, flags, n_cgs, n, t, name, binders, body) ->
assert (n = 0 && n_cgs = 0);
let env = locate env (InTop name) in
Some (wrap_throw (string_of_lident name) (lazy begin
let t = mk_return_type env t in
Expand All @@ -899,7 +907,7 @@ and mk_declaration m env d: (CStar.decl * _) option =
mk_type env t,
mk_expr env false body), [])

| DExternal (cc, flags, n, name, t, pp) ->
| DExternal (cc, flags, _, n, name, t, pp) ->
if LidSet.mem name env.ifdefs || n > 0 then
None
else
Expand All @@ -909,10 +917,10 @@ and mk_declaration m env d: (CStar.decl * _) option =
in
Some (CStar.External (name, add_cc (mk_type env t), flags, pp), [])

| DType (name, flags, _, Forward k) ->
| DType (name, flags, _, _, Forward k) ->
Some (CStar.TypeForward (name, flags, k), [ GlobalNames.to_c_name m name ])

| DType (name, flags, 0, def) ->
| DType (name, flags, 0, 0, def) ->
Some (CStar.Type (name, mk_type_def env def, flags), [ GlobalNames.to_c_name m name ] )

| DType _ ->
Expand Down Expand Up @@ -950,6 +958,8 @@ and mk_program m name env decls =
let n = string_of_lident (Ast.lid_of_decl d) in
match mk_declaration m { env with type_names = names } d with
| exception (Error e) ->
if Options.debug "backtraces" then
Printexc.print_backtrace stdout;
Warn.maybe_fatal_error (fst e, Dropping (name ^ "/" ^ n, e));
decls, names
| exception e ->
Expand Down Expand Up @@ -1002,7 +1012,7 @@ let mk_ifdefs_set files: LidSet.t =
inherit [_] reduce as super
method private zero = LidSet.empty
method private plus = LidSet.union
method! visit_DExternal _env _cc (flags: flag list) _n (name: lident) _t _hints: LidSet.t =
method! visit_DExternal _env _cc (flags: flag list) _n_cg _n (name: lident) _t _hints: LidSet.t =
if List.mem Common.IfDef flags then
LidSet.singleton name
else
Expand Down
17 changes: 10 additions & 7 deletions lib/AstToMiniRust.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -398,6 +398,8 @@ let rec translate_type (env: env) (t: Ast.typ): MiniRust.typ =
| TBound i -> Bound i
| TTuple _ -> failwith "TODO: TTuple"
| TAnonymous _ -> failwith "unexpected: we don't compile data types going to Rust"
| TCgArray _ -> failwith "Impossible: TCgArray"
| TCgApp _ -> failwith "Impossible: TCgApp"


(* Expressions *)
Expand Down Expand Up @@ -557,7 +559,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min
| EApp ({ node = EQualified ([ "LowStar"; "BufferOps" ], s); _ }, e1 :: e2 :: _ ) when KString.starts_with s "op_Star_Equals__" ->
Assign (Deref (translate_expr env e1), translate_expr env e2)

| EApp ({ node = ETApp (e, ts); _ }, es) ->
| EApp ({ node = ETApp (e, cgs, ts); _ }, es) ->
assert (cgs = []);
let es =
match es with
| [ { typ = TUnit; node } ] -> assert (node = EUnit); []
Expand All @@ -571,7 +574,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): Min
| _ -> es
in
Call (translate_expr env e, [], List.map (translate_expr env) es)
| ETApp (_, _) ->
| ETApp (_, _, _) ->
failwith "TODO: ETApp"
| EPolyComp _ ->
failwith "unexpected: EPolyComp"
Expand Down Expand Up @@ -780,11 +783,11 @@ let translate_decl env (d: Ast.decl) =
false
in
match d with
| Ast.DFunction (_, _, _, _, lid, _, _) when is_handled_primitively lid ->
| Ast.DFunction (_, _, _, _, _, lid, _, _) when is_handled_primitively lid ->
env, None

| Ast.DFunction (_cc, flags, type_parameters, t, lid, args, body) ->
assert (type_parameters = 0);
| Ast.DFunction (_cc, flags, n_cgs, type_parameters, t, lid, args, body) ->
assert (type_parameters = 0 && n_cgs = 0);
if Options.debug "rs" then
KPrint.bprintf "Ast.DFunction (%a)\n" PrintAst.Ops.plid lid;
let args, body =
Expand Down Expand Up @@ -821,12 +824,12 @@ let translate_decl env (d: Ast.decl) =
let env = push_global env lid (name, typ) in
env, Some (MiniRust.Constant { name; typ; body; public })

| Ast.DExternal (_, _, type_parameters, lid, t, _param_names) ->
| Ast.DExternal (_, _, _, type_parameters, lid, t, _param_names) ->
let name = translate_unknown_lid lid in
let env = push_global env lid (name, make_poly (translate_type env t) type_parameters) in
env, None

| Ast.DType (name, _, _, _) ->
| Ast.DType (name, _, _, _, _) ->
Warn.failwith "TODO: Ast.DType (%a)\n" PrintAst.Ops.plid name

let identify_path_components_rev filename =
Expand Down
Loading

0 comments on commit 5c7ac22

Please sign in to comment.