summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Collections.ml5
-rw-r--r--src/ExtractToFStar.ml1
-rw-r--r--src/Pure.ml89
-rw-r--r--src/PureMicroPasses.ml55
-rw-r--r--src/PureToExtract.ml25
5 files changed, 108 insertions, 67 deletions
diff --git a/src/Collections.ml b/src/Collections.ml
index 2bfdd18b..2d7a8787 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -72,6 +72,11 @@ module List = struct
fold acc (y :: ls)
in
fold init ls
+
+ let to_cons_nil (ls : 'a list) : 'a =
+ match ls with
+ | [ x ] -> x
+ | _ -> raise (Failure "The list should have length exactly one")
end
module type OrderedType = sig
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 2994d95f..a3972578 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -692,6 +692,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
let _ = extract_typed_rvalue ctx fmt inside rv in
()
| Call call -> (
+ log#ldebug (lazy ("ctx_get_function: " ^ show_fun_id call.func));
match (call.func, call.args) with
| Unop unop, [ arg ] ->
ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
diff --git a/src/Pure.ml b/src/Pure.ml
index c1dbaa13..428246dd 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -117,9 +117,9 @@ type type_def = {
}
[@@deriving show]
-type scalar_value = V.scalar_value
+type scalar_value = V.scalar_value [@@deriving show]
-type constant_value = V.constant_value
+type constant_value = V.constant_value [@@deriving show]
type var = {
id : VarId.id;
@@ -129,6 +129,7 @@ type var = {
*)
ty : ty;
}
+[@@deriving show]
(** Because we introduce a lot of temporary variables, the list of variables
is not fixed: we thus must carry all its information with the variable
itself.
@@ -138,10 +139,12 @@ type var = {
* on enumerations.
* Also: tuples... *)
type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
+[@@deriving show]
-type projection = projection_elem list
+type projection = projection_elem list [@@deriving show]
type mplace = { name : string option; projection : projection }
+[@@deriving show]
(** "Meta" place.
Meta-data retrieved from the symbolic execution, which gives provenance
@@ -149,7 +152,7 @@ type mplace = { name : string option; projection : projection }
we introduce.
*)
-type place = { var : VarId.id; projection : projection }
+type place = { var : VarId.id; projection : projection } [@@deriving show]
(** Ancestor for [iter_var_or_dummy] visitor *)
class ['self] iter_value_base =
@@ -224,15 +227,16 @@ type var_or_dummy =
| Var of var * mplace option
| Dummy (** Ignored value: `_`. *)
[@@deriving
- visitors
- {
- name = "iter_var_or_dummy";
- variety = "iter";
- ancestors = [ "iter_value_base" ];
- nude = true (* Don't inherit [VisitorsRuntime.iter] *);
- concrete = true;
- polymorphic = false;
- },
+ show,
+ visitors
+ {
+ name = "iter_var_or_dummy";
+ variety = "iter";
+ ancestors = [ "iter_value_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ polymorphic = false;
+ },
visitors
{
name = "map_var_or_dummy";
@@ -269,15 +273,16 @@ and adt_lvalue = {
and typed_lvalue = { value : lvalue; ty : ty }
[@@deriving
- visitors
- {
- name = "iter_typed_lvalue";
- variety = "iter";
- ancestors = [ "iter_var_or_dummy" ];
- nude = true (* Don't inherit [VisitorsRuntime.iter] *);
- concrete = true;
- polymorphic = false;
- },
+ show,
+ visitors
+ {
+ name = "iter_typed_lvalue";
+ variety = "iter";
+ ancestors = [ "iter_var_or_dummy" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ polymorphic = false;
+ },
visitors
{
name = "map_typed_lvalue";
@@ -316,15 +321,16 @@ and adt_rvalue = {
and typed_rvalue = { value : rvalue; ty : ty }
[@@deriving
- visitors
- {
- name = "iter_typed_rvalue";
- variety = "iter";
- ancestors = [ "iter_typed_lvalue" ];
- nude = true (* Don't inherit [VisitorsRuntime.iter] *);
- concrete = true;
- polymorphic = false;
- },
+ show,
+ visitors
+ {
+ name = "iter_typed_rvalue";
+ variety = "iter";
+ ancestors = [ "iter_typed_lvalue" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ polymorphic = false;
+ },
visitors
{
name = "map_typed_rvalue";
@@ -353,8 +359,6 @@ and typed_rvalue = { value : rvalue; ty : ty }
type unop = Not | Neg of integer_type [@@deriving show, ord]
-(* TODO: redefine assumed_fun_id (we need to get rid of box! *)
-
type fun_id =
| Regular of A.fun_id * T.RegionGroupId.id option
(** Backward id: `Some` if the function is a backward function, `None`
@@ -364,7 +368,7 @@ type fun_id =
[@@deriving show, ord]
(** Meta-information stored in the AST *)
-type meta = Assignment of mplace * typed_rvalue
+type meta = Assignment of mplace * typed_rvalue [@@deriving show]
(** Ancestor for [iter_expression] visitor *)
class ['self] iter_expression_base =
@@ -512,14 +516,15 @@ and match_branch = { pat : typed_lvalue; branch : texpression }
and texpression = { e : expression; ty : ty }
[@@deriving
- visitors
- {
- name = "iter_expression";
- variety = "iter";
- ancestors = [ "iter_expression_base" ];
- nude = true (* Don't inherit [VisitorsRuntime.iter] *);
- concrete = true;
- },
+ show,
+ visitors
+ {
+ name = "iter_expression";
+ variety = "iter";
+ ancestors = [ "iter_expression_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ },
visitors
{
name = "map_expression";
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 66442ec7..cbc2409d 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -677,6 +677,56 @@ let unit_vars_to_unit (def : fun_def) : fun_def =
(* Return *)
{ def with body; inputs_lvs }
+(** Eliminate the box functions like `Box::new`, `Box::deref`, etc. Most of them
+ are translated to identity, and `Box::free` is translated to `()`.
+
+ Note that the box types have already been eliminated during the translation
+ from symbolic to pure.
+ The reason why we don't eliminate the box functions at the same time is
+ that we would need to eliminate them in two different places: when translating
+ function calls, and when translating end abstractions. Here, we can do
+ something simpler, in one micro-pass.
+ *)
+let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def =
+ (* The map visitor *)
+ let obj =
+ object
+ inherit [_] map_expression as super
+
+ method! visit_Call env call =
+ match call.func with
+ | Regular (A.Assumed aid, rg_id) -> (
+ match (aid, rg_id) with
+ | A.BoxNew, _ ->
+ let arg = Collections.List.to_cons_nil call.args in
+ arg.e
+ | A.BoxDeref, None ->
+ (* `Box::deref` forward is the identity *)
+ let arg = Collections.List.to_cons_nil call.args in
+ arg.e
+ | A.BoxDeref, Some _ ->
+ (* `Box::deref` backward is `()` (doesn't give back anything) *)
+ (mk_value_expression unit_rvalue None).e
+ | A.BoxDerefMut, None ->
+ (* `Box::deref_mut` forward is the identity *)
+ let arg = Collections.List.to_cons_nil call.args in
+ arg.e
+ | A.BoxDerefMut, Some _ ->
+ (* `Box::deref_mut` back is the identity *)
+ let arg =
+ match call.args with
+ | [ _; given_back ] -> given_back
+ | _ -> failwith "Unreachable"
+ in
+ arg.e
+ | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e)
+ | _ -> super#visit_Call env call
+ end
+ in
+ (* Update the body *)
+ let body = obj#visit_texpression () def.body in
+ { def with body }
+
(** Unfold the monadic let-bindings to explicit matches. *)
let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def =
(* It is a very simple map *)
@@ -753,6 +803,11 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
(lazy
("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+ (* Eliminate the box functions *)
+ let def = eliminate_box_functions ctx def in
+ log#ldebug
+ (lazy ("eliminate_box_functions:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+
(* Filter the unused variables, assignments, function calls, etc. *)
let def = filter_unused config.filter_unused_monadic_calls ctx def in
log#ldebug (lazy ("filter_unused:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index bd69837a..6a1bcc2a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -240,31 +240,6 @@ let names_map_add_assumed_function (fid : A.assumed_fun_id)
names_map =
names_map_add (FunId (A.Assumed fid, rg_id)) name nm
-(* TODO: remove those functions? We use the ones of extraction_ctx *)
-let names_map_get (id : id) (nm : names_map) : string =
- IdMap.find id nm.id_to_name
-
-let names_map_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
- (nm : names_map) : string =
- names_map_get (FunId (id, rg)) nm
-
-let names_map_get_local_function (id : FunDefId.id)
- (rg : RegionGroupId.id option) (nm : names_map) : string =
- names_map_get_function (A.Local id) rg nm
-
-let names_map_get_type (id : type_id) (nm : names_map) : string =
- assert (id <> Tuple);
- names_map_get (TypeId id) nm
-
-let names_map_get_local_type (id : TypeDefId.id) (nm : names_map) : string =
- names_map_get_type (AdtId id) nm
-
-let names_map_get_var (id : VarId.id) (nm : names_map) : string =
- names_map_get (VarId id) nm
-
-let names_map_get_type_var (id : TypeVarId.id) (nm : names_map) : string =
- names_map_get (TypeVarId id) nm
-
(** Make a (variable) basename unique (by adding an index).
We do this in an inefficient manner (by testing all indices starting from
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 13:40:05 +0000