diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 68 | ||||
| -rw-r--r-- | src/Pure.ml | 3 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 26 | ||||
| -rw-r--r-- | src/StringUtils.ml | 9 | ||||
| -rw-r--r-- | src/Translate.ml | 2 |
5 files changed, 96 insertions, 12 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index fb781939..2f542922 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -65,7 +65,7 @@ let fstar_names_map_init = * In Rust: * ``` * enum List = { - * Cons(u32, Box<List>), + * Cons(u32, Box<List>),x * Nil, * } * ``` @@ -90,7 +90,7 @@ 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_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) = +let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) = let int_name (int_ty : integer_type) = match int_ty with | Isize -> "isize" @@ -194,6 +194,23 @@ let mk_name_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 + | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.V.value) + | Bool b -> + let b = if b then "true" else "false" in + F.pp_print_string fmt b + | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'") + | String s -> + (* We need to replace all the line breaks *) + let s = + StringUtils.map + (fun c -> if c = '\n' then "\n" else String.make 1 c) + s + in + F.pp_print_string fmt ("\"" ^ s ^ "\"") + in { bool_name = "bool"; char_name = "char"; @@ -207,6 +224,7 @@ let mk_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) = var_basename; type_var_basename; append_index; + extract_constant_value; } (** [inside] constrols whether we should add parentheses or not around type @@ -558,10 +576,52 @@ let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter) extract_adt_g_value extract_value fmt ctx inside av.variant_id av.field_values v.ty +let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit + = + let rec extract_projection (pl : projection) : unit = + match pl with + | [] -> + (* No projection element left: print the variable *) + let var_name = ctx_get_var p.var ctx in + F.pp_print_string fmt var_name + | pe :: pl -> + (* Extract the interior of the projection *) + extract_projection pl; + (* Match on the projection element *) + let def_id = + match pe.pkind with + | E.ProjAdt (def_id, None) -> def_id + | E.ProjAdt (_, Some _) | E.ProjTuple _ -> + (* We can't have field accesses on enumerations (variables for + * the fields are introduced upon the moment we match over the + * enumeration). We also forbid field access on tuples, because + * we don't have the syntax to translate that... We thus + * deconstruct the tuples whenever we need to have access: + * `let (x, y) = p in ...` *) + failwith "Unreachable" + in + let field_name = ctx_get_field (AdtId def_id) pe.field_id ctx in + (* We allow to break where the "." appears *) + F.pp_print_break fmt 0 0; + F.pp_print_string fmt "."; + F.pp_print_string fmt field_name + in + extract_projection p.projection + (** [inside]: see [extract_ty] *) let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (v : typed_rvalue) : unit = - raise Unimplemented + (inside : bool) (v : typed_rvalue) : extraction_ctx = + match v.value with + | RvConcrete cv -> + ctx.fmt.extract_constant_value fmt inside cv; + ctx + | RvPlace p -> + extract_place ctx fmt p; + ctx + | RvAdt av -> + let extract_value ctx inside v = extract_typed_rvalue ctx fmt inside v in + extract_adt_g_value extract_value fmt ctx inside av.variant_id + av.field_values v.ty (** [inside]: see [extract_ty] *) let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) diff --git a/src/Pure.ml b/src/Pure.ml index 32a1ca4c..fd3eb03f 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -134,6 +134,9 @@ type var = { itself. *) +(* TODO: we might want to redefine field_proj_kind here, to prevent field accesses + * on enumerations. + * Also: tuples... *) type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id } type projection = projection_elem list diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 02c507ef..8c8ab76a 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -9,6 +9,7 @@ open Pure open TranslateCore module C = Contexts module RegionVarId = T.RegionVarId +module F = Format (** The local logger *) let log = L.pure_to_extract_log @@ -30,7 +31,7 @@ module StringMap = Collections.MakeMap (Collections.OrderedString) type name = Identifiers.name -type name_formatter = { +type formatter = { bool_name : string; char_name : string; int_name : integer_type -> string; @@ -96,17 +97,28 @@ type name_formatter = { indices to names, the responsability of finding a proper index is delegated to helper functions. *) + extract_constant_value : F.formatter -> bool -> constant_value -> unit; + (** Format a constant value. + + Inputs: + - formatter + - [inside]: if `true`, the value should be wrapped in parentheses + if it is made of an application (ex.: `U32 3`) + *) } -(** A name formatter's role is to come up with name suggestions. +(** A formatter's role is twofold: + 1. Come up with name suggestions. For instance, provided some information about a function (its basename, information about the region group, etc.) it should come up with an appropriate name for the forward/backward function. It can of course apply many transformations, like changing to camel case/ snake case, adding prefixes/suffixes, etc. + + 2. Format some specific terms, like constants. *) -let compute_type_def_name (fmt : name_formatter) (def : type_def) : string = +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 @@ -145,14 +157,14 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) "_back" ^ RegionGroupId.to_string rg.id (** Extract information from a function, and give this information to a - [name_formatter] to generate a function's name. + [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 : name_formatter) - (fun_id : A.fun_id) (rg_id : RegionGroupId.id option) : string = +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 @@ -297,7 +309,7 @@ let basename_to_unique (names_set : StringSet.t) type extraction_ctx = { trans_ctx : trans_ctx; names_map : names_map; - fmt : name_formatter; + fmt : formatter; indent_incr : int; (** The indent increment we insert whenever we need to indent more *) } diff --git a/src/StringUtils.ml b/src/StringUtils.ml index 2e0e18f7..7c628184 100644 --- a/src/StringUtils.ml +++ b/src/StringUtils.ml @@ -86,6 +86,15 @@ let to_snake_case (s : string) : string = in string_of_chars (List.rev chars) +(** Applies a map operation. + + This is very inefficient, but shouldn't be used much. + *) +let map (f : char -> string) (s : string) : string = + let sl = List.map f (string_to_chars s) in + let sl = List.map string_to_chars sl in + string_of_chars (List.concat sl) + (** Unit tests *) let _ = assert (to_camel_case "hello_world" = "HelloWorld"); diff --git a/src/Translate.ml b/src/Translate.ml index efaa43d6..47426c81 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -271,7 +271,7 @@ let translate_module (filename : string) (config : C.partial_config) in let variant_concatenate_type_name = true in let fstar_fmt = - ExtractToFStar.mk_name_formatter trans_ctx variant_concatenate_type_name + ExtractToFStar.mk_formatter trans_ctx variant_concatenate_type_name in let extract_ctx = { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 } |