summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Expressions.ml20
-rw-r--r--src/ExtractToFStar.ml136
-rw-r--r--src/PureToExtract.ml190
-rw-r--r--src/Types.ml3
4 files changed, 263 insertions, 86 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6e2b20d0..816870cd 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -47,6 +47,26 @@ type binop =
| Shr
[@@deriving show, ord]
+let all_binops =
+ [
+ BitXor;
+ BitAnd;
+ BitOr;
+ Eq;
+ Lt;
+ Le;
+ Ne;
+ Ge;
+ Gt;
+ Div;
+ Rem;
+ Add;
+ Sub;
+ Mul;
+ Shl;
+ Shr;
+ ]
+
(** Constant value for an operand
It is a bit annoying, but rustc treats some ADT and tuple instances as
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a4440071..100b5ecb 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -39,6 +39,21 @@ let fstar_keywords =
"Type0";
]
+let fstar_int_name (int_ty : integer_type) =
+ match int_ty with
+ | Isize -> "isize"
+ | I8 -> "i8"
+ | I16 -> "i16"
+ | I32 -> "i32"
+ | I64 -> "i64"
+ | I128 -> "i128"
+ | Usize -> "usize"
+ | U8 -> "u8"
+ | U16 -> "u16"
+ | U32 -> "u32"
+ | U64 -> "u64"
+ | U128 -> "u128"
+
let fstar_assumed_adts : (assumed_ty * string) list = [ (Result, "result") ]
let fstar_assumed_structs : (assumed_ty * string) list = []
@@ -46,14 +61,76 @@ let fstar_assumed_structs : (assumed_ty * string) list = []
let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
[ (Result, result_return_id, "Return"); (Result, result_fail_id, "Fail") ]
+let fstar_assumed_functions :
+ (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+ []
+
let fstar_names_map_init =
{
keywords = fstar_keywords;
assumed_adts = fstar_assumed_adts;
assumed_structs = fstar_assumed_structs;
assumed_variants = fstar_assumed_variants;
+ assumed_functions = fstar_assumed_functions;
}
+let fstar_extract_unop (ctx : extraction_ctx) (fmt : F.formatter)
+ (extract_expr :
+ extraction_ctx -> F.formatter -> bool -> texpression -> extraction_ctx)
+ (inside : bool) (unop : unop) (arg : texpression) : extraction_ctx =
+ let unop =
+ match unop with
+ | Not -> "not"
+ | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
+ in
+ if inside then F.pp_print_string fmt "(";
+ F.pp_print_string fmt unop;
+ F.pp_print_space fmt ();
+ let ctx = extract_expr ctx fmt true arg in
+ if inside then F.pp_print_string fmt ")";
+ ctx
+
+let fstar_extract_binop (ctx : extraction_ctx) (fmt : F.formatter)
+ (extract_expr :
+ extraction_ctx -> F.formatter -> bool -> texpression -> extraction_ctx)
+ (inside : bool) (binop : E.binop) (int_ty : integer_type)
+ (arg0 : texpression) (arg1 : texpression) : extraction_ctx =
+ if inside then F.pp_print_string fmt "(";
+ let ctx =
+ match binop with
+ | Eq ->
+ let ctx = extract_expr ctx fmt false arg0 in
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "=";
+ F.pp_print_space fmt ();
+ let ctx = extract_expr ctx fmt false arg1 in
+ ctx
+ | _ ->
+ let binop =
+ match binop with
+ | Eq -> failwith "Unreachable"
+ | Lt -> "lt"
+ | Le -> "le"
+ | Ne -> "ne"
+ | Ge -> "ge"
+ | Gt -> "gt"
+ | Div -> "div"
+ | Rem -> "rem"
+ | Add -> "add"
+ | Sub -> "sub"
+ | Mul -> "mul"
+ | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented
+ in
+ F.pp_print_string fmt (fstar_int_name int_ty ^ "_" ^ binop);
+ F.pp_print_space fmt ();
+ let ctx = extract_expr ctx fmt false arg0 in
+ F.pp_print_space fmt ();
+ let ctx = extract_expr ctx fmt false arg1 in
+ ctx
+ in
+ if inside then F.pp_print_string fmt ")";
+ ctx
+
(**
* [ctx]: we use the context to lookup type definitions, to retrieve type names.
* This is used to compute variable names, when they have no basenames: in this
@@ -90,22 +167,10 @@ let fstar_names_map_init =
* up type checking. Note that some languages actually forbids the name clashes
* (it is the case of F* ).
*)
-let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
- let int_name (int_ty : integer_type) =
- match int_ty with
- | Isize -> "isize"
- | I8 -> "i8"
- | I16 -> "i16"
- | I32 -> "i32"
- | I64 -> "i64"
- | I128 -> "i128"
- | Usize -> "usize"
- | U8 -> "u8"
- | U16 -> "u16"
- | U32 -> "u32"
- | U64 -> "u64"
- | U128 -> "u128"
- in
+let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
+ formatter =
+ let int_name = fstar_int_name in
+
(* For now, we treat only the case where type names are of the
* form: `Module::Type`
*)
@@ -158,6 +223,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
(* Concatenate *)
fname ^ suffix
in
+
let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
: string =
(* If there is a basename, we use it *)
@@ -194,6 +260,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
let append_index (basename : string) (i : int) : string =
basename ^ string_of_int i
in
+
let extract_constant_value (fmt : F.formatter) (_inside : bool)
(cv : constant_value) : unit =
match cv with
@@ -225,6 +292,8 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
type_var_basename;
append_index;
extract_constant_value;
+ extract_unop = fstar_extract_unop;
+ extract_binop = fstar_extract_binop;
}
(** [inside] constrols whether we should add parentheses or not around type
@@ -628,7 +697,38 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
(inside : bool) (e : texpression) : extraction_ctx =
match e.e with
| Value (rv, _) -> extract_typed_rvalue ctx fmt inside rv
- | Call call -> raise Unimplemented
+ | Call call -> (
+ match (call.func, call.args) with
+ | Unop unop, [ arg ] ->
+ ctx.fmt.extract_unop ctx fmt extract_texpression inside unop arg
+ | Binop (binop, int_ty), [ arg0; arg1 ] ->
+ ctx.fmt.extract_binop ctx fmt extract_texpression inside binop int_ty
+ arg0 arg1
+ | Regular (fun_id, rg_id), _ ->
+ if inside then F.pp_print_string fmt "(";
+ (* Open a box for the function call *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+ (* Print the function name *)
+ let fun_name = ctx_get_function fun_id rg_id ctx in
+ F.pp_print_string fmt fun_name;
+ (* Print the type parameters *)
+ List.iter
+ (fun ty ->
+ F.pp_print_space fmt ();
+ extract_ty ctx fmt true ty)
+ call.type_params;
+ (* Print the input values *)
+ let ctx =
+ List.fold_left
+ (fun ctx ve -> extract_texpression ctx fmt true ve)
+ ctx call.args
+ in
+ (* Close the box for the function call *)
+ F.pp_close_box fmt ();
+ (* Return *)
+ if inside then F.pp_print_string fmt ")";
+ ctx
+ | _ -> failwith "Unreachable")
| Let (monadic, lv, re, next_e) ->
(* Open a box for the let-binding *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -729,8 +829,8 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hvbox fmt 0;
(* Extract the body *)
let _ = extract_texpression ctx fmt false def.body in
- F.pp_close_box fmt ();
(* Close the box for the body *)
+ F.pp_close_box fmt ();
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 8c8ab76a..54b59141 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -31,7 +31,7 @@ module StringMap = Collections.MakeMap (Collections.OrderedString)
type name = Identifiers.name
-type formatter = {
+type 'ctx g_formatter = {
bool_name : string;
char_name : string;
int_name : integer_type -> string;
@@ -105,6 +105,45 @@ type formatter = {
- [inside]: if `true`, the value should be wrapped in parentheses
if it is made of an application (ex.: `U32 3`)
*)
+ extract_unop :
+ 'ctx ->
+ F.formatter ->
+ ('ctx -> F.formatter -> bool -> texpression -> 'ctx) ->
+ bool ->
+ unop ->
+ texpression ->
+ 'ctx;
+ (** Format a unary operation
+
+ Inputs:
+ - extraction context (see below)
+ - formatter
+ - expression formatter
+ - [inside]
+ - unop
+ - argument
+ *)
+ extract_binop :
+ 'ctx ->
+ F.formatter ->
+ ('ctx -> F.formatter -> bool -> texpression -> 'ctx) ->
+ bool ->
+ E.binop ->
+ integer_type ->
+ texpression ->
+ texpression ->
+ 'ctx;
+ (** Format a binary operation
+
+ Inputs:
+ - extraction context (see below)
+ - formatter
+ - expression formatter
+ - [inside]
+ - binop
+ - argument 0
+ - argument 1
+ *)
}
(** A formatter's role is twofold:
1. Come up with name suggestions.
@@ -118,73 +157,6 @@ type formatter = {
2. Format some specific terms, like constants.
*)
-let compute_type_def_name (fmt : formatter) (def : type_def) : string =
- fmt.type_name def.name
-
-(** A helper function: generates a function suffix from a region group
- information.
- TODO: move all those helpers.
-*)
-let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
- : string =
- (* There are several cases:
- - [rg] is `Some`: this is a forward function:
- - we add "_fwd"
- - [rg] is `None`: this is a backward function:
- - this function has one region group: we add "_back"
- - this function has several backward function: we add "_back" and an
- additional suffix to identify the precise backward function
- Note that we always add a suffix (in case there are no region groups,
- we could not add the "_fwd" suffix) to prevent name clashes between
- definitions (in particular between type and function definitions).
- *)
- match rg with
- | None -> "_fwd"
- | Some rg ->
- assert (num_region_groups > 0);
- if num_region_groups = 1 then (* Exactly one backward function *)
- "_back"
- else if
- (* Several region groups/backward functions:
- - if all the regions in the group have names, we use those names
- - otherwise we use an index
- *)
- List.for_all Option.is_some rg.region_names
- then
- (* Concatenate the region names *)
- "_back" ^ String.concat "" (List.map Option.get rg.region_names)
- else (* Use the region index *)
- "_back" ^ RegionGroupId.to_string rg.id
-
-(** Extract information from a function, and give this information to a
- [formatter] to generate a function's name.
-
- Note that we need region information coming from CFIM (when generating
- the name for a backward function, we try to use the names of the regions
- to
- *)
-let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
- (rg_id : RegionGroupId.id option) : string =
- (* Lookup the function CFIM signature (we need the region information) *)
- let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
- let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
- (* Compute the regions information *)
- let num_region_groups = List.length sg.regions_hierarchy in
- let rg_info =
- match rg_id with
- | None -> None
- | Some rg_id ->
- let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
- let regions =
- List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
- in
- let region_names =
- List.map (fun (r : T.region_var) -> r.name) regions
- in
- Some { id = rg.id; region_names }
- in
- fmt.fun_name fun_id basename num_region_groups rg_info
-
(** We use identifiers to look for name clashes *)
type id =
| FunId of A.fun_id * RegionGroupId.id option
@@ -266,6 +238,11 @@ let names_map_add_assumed_variant (id : assumed_ty) (variant_id : VariantId.id)
(name : string) (nm : names_map) : names_map =
names_map_add (VariantId (Assumed id, variant_id)) name nm
+let names_map_add_assumed_function (fid : A.assumed_fun_id)
+ (rg_id : RegionGroupId.id option) (name : string) (nm : names_map) :
+ 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
@@ -321,6 +298,8 @@ type extraction_ctx = {
functions, etc.
*)
+and formatter = extraction_ctx g_formatter
+
let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
(* TODO : nice debugging message if collision *)
let names_map = names_map_add id name ctx.names_map in
@@ -472,6 +451,7 @@ type names_map_init = {
assumed_adts : (assumed_ty * string) list;
assumed_structs : (assumed_ty * string) list;
assumed_variants : (assumed_ty * VariantId.id * string) list;
+ assumed_functions : (A.assumed_fun_id * RegionGroupId.id option * string) list;
}
(** Initialize a names map with a proper set of keywords/names coming from the
@@ -490,6 +470,7 @@ let initialize_names_map (init : names_map_init) : names_map =
* - the assumed types
* - the assumed struct constructors
* - the assumed variants
+ * - the assumed functions
*)
let nm =
List.fold_left
@@ -507,5 +488,78 @@ let initialize_names_map (init : names_map_init) : names_map =
names_map_add_assumed_variant type_id variant_id name nm)
nm init.assumed_variants
in
+ let nm =
+ List.fold_left
+ (fun nm (fun_id, rg_id, name) ->
+ names_map_add_assumed_function fun_id rg_id name nm)
+ nm init.assumed_functions
+ in
(* Return *)
nm
+
+let compute_type_def_name (fmt : formatter) (def : type_def) : string =
+ fmt.type_name def.name
+
+(** A helper function: generates a function suffix from a region group
+ information.
+ TODO: move all those helpers.
+*)
+let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
+ : string =
+ (* There are several cases:
+ - [rg] is `Some`: this is a forward function:
+ - we add "_fwd"
+ - [rg] is `None`: this is a backward function:
+ - this function has one region group: we add "_back"
+ - this function has several backward function: we add "_back" and an
+ additional suffix to identify the precise backward function
+ Note that we always add a suffix (in case there are no region groups,
+ we could not add the "_fwd" suffix) to prevent name clashes between
+ definitions (in particular between type and function definitions).
+ *)
+ match rg with
+ | None -> "_fwd"
+ | Some rg ->
+ assert (num_region_groups > 0);
+ if num_region_groups = 1 then (* Exactly one backward function *)
+ "_back"
+ else if
+ (* Several region groups/backward functions:
+ - if all the regions in the group have names, we use those names
+ - otherwise we use an index
+ *)
+ List.for_all Option.is_some rg.region_names
+ then
+ (* Concatenate the region names *)
+ "_back" ^ String.concat "" (List.map Option.get rg.region_names)
+ else (* Use the region index *)
+ "_back" ^ RegionGroupId.to_string rg.id
+
+(** Extract information from a function, and give this information to a
+ [formatter] to generate a function's name.
+
+ Note that we need region information coming from CFIM (when generating
+ the name for a backward function, we try to use the names of the regions
+ to
+ *)
+let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
+ (rg_id : RegionGroupId.id option) : string =
+ (* Lookup the function CFIM signature (we need the region information) *)
+ let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
+ let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
+ (* Compute the regions information *)
+ let num_region_groups = List.length sg.regions_hierarchy in
+ let rg_info =
+ match rg_id with
+ | None -> None
+ | Some rg_id ->
+ let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
+ let regions =
+ List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
+ in
+ let region_names =
+ List.map (fun (r : T.region_var) -> r.name) regions
+ in
+ Some { id = rg.id; region_names }
+ in
+ fmt.fun_name fun_id basename num_region_groups rg_info
diff --git a/src/Types.ml b/src/Types.ml
index 70ab3978..44302f8a 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -80,6 +80,9 @@ type integer_type =
| U128
[@@deriving show, ord]
+let all_integer_types =
+ [ Isize; I8; I16; I32; I64; I128; Usize; U8; U16; U32; U64; U128 ]
+
type ref_kind = Mut | Shared [@@deriving show, ord]
type assumed_ty = Box [@@deriving show, ord]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:39:39 +0000