diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 56 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 15 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 26 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 105 | ||||
| -rw-r--r-- | src/Modules.ml | 20 | ||||
| -rw-r--r-- | src/PureUtils.ml | 2 |
6 files changed, 117 insertions, 107 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 06f82ac4..eb88b916 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -314,6 +314,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) String.concat "_" fname in let global_name (name : global_name) : string = + (* Converting to snake case also lowercases the letters (in Rust, global + * names are written in capital letters). *) let parts = List.map to_snake_case (get_name name) in String.concat "_" parts in @@ -326,7 +328,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ suffix in - let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string = + let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string + = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) let suffix = "_decreases" in @@ -795,8 +798,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) ctx (** Simply add the global name to the context. *) -let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) - : extraction_ctx = +let extract_global_decl_register_names (ctx : extraction_ctx) + (def : A.global_decl) : extraction_ctx = ctx_add_global_decl_body def ctx (** The following function factorizes the extraction of ADT values. @@ -851,7 +854,7 @@ let extract_adt_g_value (* Extract globals in the same way as variables *) let extract_global (ctx : extraction_ctx) (fmt : F.formatter) - (id : A.GlobalDeclId.id) : unit = + (id : A.GlobalDeclId.id) : unit = F.pp_print_string fmt (ctx_get_global id ctx) (** [inside]: see [extract_ty]. @@ -921,13 +924,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match qualif.id with | Func fun_id -> extract_function_call ctx fmt inside fun_id qualif.type_args args - | Global global_id -> - extract_global ctx fmt global_id + | Global global_id -> extract_global ctx fmt global_id | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> - extract_field_projector ctx fmt inside app proj qualif.type_args args - ) + extract_field_projector ctx fmt inside app proj qualif.type_args args) | _ -> (* "Regular" expression *) (* Open parentheses *) @@ -1493,9 +1494,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (name : string) (ty : ty) - (extract_body : (F.formatter -> unit) Option.t) - : unit = + (qualif : fun_decl_qualif) (name : string) (ty : ty) + (extract_body : (F.formatter -> unit) Option.t) : unit = let is_opaque = Option.is_none extract_body in (* Open the definition box (depth=0) *) @@ -1505,7 +1505,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; (* Print "QUALIF NAME " *) F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name); - F.pp_print_space fmt (); + F.pp_print_space fmt (); (* Open ": TYPE =" box (depth=2) *) F.pp_open_hvbox fmt 0; @@ -1523,8 +1523,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) if not is_opaque then ( (* Print " =" *) F.pp_print_space fmt (); - F.pp_print_string fmt "="; - ); + F.pp_print_string fmt "="); (* Close ": TYPE =" box (depth=2) *) F.pp_close_box fmt (); (* Close "QUALIF NAME : TYPE =" box (depth=1) *) @@ -1537,8 +1536,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (* Print "BODY" *) (Option.get extract_body) fmt; (* Close "BODY" box (depth=1) *) - F.pp_close_box fmt () - ); + F.pp_close_box fmt ()); (* Close the definition box (depth=0) *) F.pp_close_box fmt () @@ -1554,39 +1552,37 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = - assert (body.is_global_body); + assert body.is_global_body; assert (Option.is_none body.back_id); assert (List.length body.signature.inputs = 0); assert (List.length body.signature.doutputs = 1); assert (List.length body.signature.type_params = 0); (* Add a break then the name of the corresponding LLBC declaration *) - F.pp_print_break fmt 0 0; - F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); - F.pp_print_space fmt (); + F.pp_print_break fmt 0 0; + F.pp_print_string fmt + ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); + F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = ctx_get_function (Regular global.body_id) None ctx in let decl_ty, body_ty = let ty = body.signature.output in - if body.signature.info.effect_info.can_fail - then (unwrap_result_ty ty, ty) - else (ty, mk_result_ty ty) + if body.signature.info.effect_info.can_fail then (unwrap_result_ty ty, ty) + else (ty, mk_result_ty ty) in match body.body with | None -> let qualif = if interface then Val else AssumeVal in extract_global_decl_body ctx fmt qualif decl_name decl_ty None | Some body -> - extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt -> - extract_texpression ctx fmt false body.body - )); + extract_global_decl_body ctx fmt Let body_name body_ty + (Some (fun fmt -> extract_texpression ctx fmt false body.body)); F.pp_print_break fmt 0 0; - extract_global_decl_body ctx fmt Let decl_name decl_ty (Some (fun fmt -> - F.pp_print_string fmt ("eval_global " ^ body_name) - )); - F.pp_print_break fmt 0 0 + extract_global_decl_body ctx fmt Let decl_name decl_ty + (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name))); + F.pp_print_break fmt 0 0 (** Extract a unit test, if the function is a unit function (takes no parameters, returns unit). diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 4598895e..4a4f3353 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -110,14 +110,13 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) ctx (** Convert an operand constant operand value to a typed value *) -let constant_to_typed_value (ty : T.ety) - (cv : V.constant_value) : V.typed_value = +let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value + = (* Check the type while converting - we actually need some information - * contained in the type *) + * contained in the type *) log#ldebug (lazy - ("constant_to_typed_value:" ^ "\n- cv: " - ^ PV.constant_value_to_string cv)); + ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty } @@ -128,10 +127,8 @@ let constant_to_typed_value (ty : T.ety) assert (int_ty = v.int_ty); assert (check_scalar_value_in_range v); { V.value = V.Concrete (V.Scalar v); ty } - (* Remaining cases (invalid) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, _ -> - failwith "Improperly typed constant value" + (* Remaining cases (invalid) *) + | _, _ -> failwith "Improperly typed constant value" (** Reorganize the environment in preparation for the evaluation of an operand. diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 48620439..34310ea1 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -831,8 +831,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx - | A.AssignGlobal { dst; global } -> - eval_global config dst global cf ctx + | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare cf = @@ -910,20 +909,27 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.id) : st_cm_fun = +and eval_global (config : C.config) (dest : V.VarId.id) + (gid : LA.GlobalDeclId.id) : st_cm_fun = fun cf ctx -> let global = C.ctx_lookup_global_decl ctx gid in let place = { E.var_id = dest; projection = [] } in match config.mode with | ConcreteMode -> - (* Treat the global as a function without arguments to call *) - (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx + (* Treat the evaluation of the global as a call to the global body (without arguments) *) + (eval_local_function_call_concrete config global.body_id [] [] [] place) + cf ctx | SymbolicMode -> - (* Treat the global as a fresh symbolic value *) - let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in - let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in - let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid sval e + (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be + * defined as equal to the value of the global (see `S.synthesize_global_eval`). *) + let sval = + mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) + in + let cc = + assign_to_place config (mk_typed_value_from_symbolic_value sval) place + in + let e = cc (cf Unit) ctx in + S.synthesize_global_eval gid sval e (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index be43ff54..846d7232 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -394,7 +394,7 @@ let constant_value_of_json (js : json) : (V.constant_value, string) result = let* v = string_of_json v in Ok (V.String v) | _ -> Error "") - + let operand_of_json (js : json) : (E.operand, string) result = combine_error_msgs js "operand_of_json" (match js with @@ -599,10 +599,8 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result = | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = - list_of_json ( - pair_of_json - (list_of_json scalar_value_of_json) - statement_of_json) + list_of_json + (pair_of_json (list_of_json scalar_value_of_json) statement_of_json) tgts in let* otherwise = statement_of_json otherwise in @@ -633,47 +631,47 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result = let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in let* body = option_of_json fun_body_of_json body in - Ok { A.def_id; name; signature; body; is_global_body = false; } + Ok { A.def_id; name; signature; body; is_global_body = false } | _ -> Error "") (* Strict type for the number of function declarations (see [global_to_fun_id] below) *) -type global_id_converter = { fun_count : int } -[@@deriving show] +type global_id_converter = { fun_count : int } [@@deriving show] (** Converts a global id to its corresponding function id. To do so, it adds the global id to the number of function declarations : - We have the bijection `global_id <=> fun_id + fun_id_count`. + We have the bijection `global_fun_id <=> global_id + fun_id_count`. *) -let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id = - A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count) +let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : + A.FunDeclId.id = + A.FunDeclId.of_int (A.GlobalDeclId.to_int gid + conv.fun_count) (* Converts a global declaration to a function declaration. *) -let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result = +let global_decl_of_json (js : json) (gid_conv : global_id_converter) : + (A.global_decl * A.fun_decl, string) result = combine_error_msgs js "global_decl_of_json" (match js with - | `Assoc - [ - ("def_id", def_id); - ("name", name); - ("ty", ty); - ("body", body); - ] -> + | `Assoc [ ("def_id", def_id); ("name", name); ("ty", ty); ("body", body) ] + -> let* global_id = A.GlobalDeclId.id_of_json def_id in let fun_id = global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name in let* ty = ety_of_json ty in let* body = option_of_json fun_body_of_json body in - let signature : A.fun_sig = { - region_params = []; - num_early_bound_regions = 0; - regions_hierarchy = []; - type_params = []; - inputs = []; - output = TU.ety_no_regions_to_sty ty; - } in - Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; }, - { A.def_id = fun_id; name; signature; body; is_global_body = true; }) + let signature : A.fun_sig = + { + region_params = []; + num_early_bound_regions = 0; + regions_hierarchy = []; + type_params = []; + inputs = []; + output = TU.ety_no_regions_to_sty ty; + } + in + Ok + ( { A.def_id = global_id; body_id = fun_id; name; ty }, + { A.def_id = fun_id; name; signature; body; is_global_body = true } + ) | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) @@ -701,13 +699,12 @@ let fun_declaration_group_of_json (js : json) : let global_declaration_group_of_json (js : json) : (A.GlobalDeclId.id, string) result = combine_error_msgs js "global_declaration_group_of_json" - (match js with - | `Assoc [ ("NonRec", `List [ id ]) ] -> - let* id = A.GlobalDeclId.id_of_json id in - Ok (id) - | `Assoc [ ("Rec", `List [ _ ]) ] -> - Error "got mutually dependent globals" - | _ -> Error "") + (match js with + | `Assoc [ ("NonRec", `List [ id ]) ] -> + let* id = A.GlobalDeclId.id_of_json id in + Ok id + | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals" + | _ -> Error "") let declaration_group_of_json (js : json) : (M.declaration_group, string) result = @@ -724,11 +721,11 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result Ok (M.Global id) | _ -> Error "") -let length_of_json_list (js: json) : (int, string) result = +let length_of_json_list (js : json) : (int, string) result = combine_error_msgs js "get_json_list_len" (match js with - | `List jsl -> Ok (List.length jsl) - | _ -> Error ("not a list: " ^ show js)) + | `List jsl -> Ok (List.length jsl) + | _ -> Error ("not a list: " ^ show js)) let llbc_module_of_json (js : json) : (M.llbc_module, string) result = combine_error_msgs js "llbc_module_of_json" @@ -741,18 +738,30 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("functions", functions); ("globals", globals); ] -> + (* We first deserialize the declaration groups (which simply contain ids) + * and all the declarations *butù* the globals *) let* name = string_of_json name in - let* declarations = list_of_json declaration_group_of_json declarations in + let* declarations = + list_of_json declaration_group_of_json declarations + in let* types = list_of_json type_decl_of_json types in let* functions = list_of_json fun_decl_of_json functions in + (* When deserializing the globals, we split the global declarations + * between the globals themselves and their bodies, which are simply + * functions with no arguments. We add the global bodies to the list + * of function declarations: the (fresh) ids we use for those bodies + * are simply given by: `num_functions + global_id` *) let gid_conv = { fun_count = List.length functions } in - let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in + let* globals = + list_of_json (fun js -> global_decl_of_json js gid_conv) globals + in let globals, global_bodies = List.split globals in - Ok { - M.name; - declarations; - types; - functions = functions @ global_bodies; - globals; - } + Ok + { + M.name; + declarations; + types; + functions = functions @ global_bodies; + globals; + } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index 009e1ba6..7f372d09 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -7,10 +7,9 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list type type_declaration_group = TypeDeclId.id g_declaration_group [@@deriving show] -type fun_declaration_group = FunDeclId.id g_declaration_group -[@@deriving show] +type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] -(** Module declaration. Globals cannot be mutually dependent. *) +(** Module declaration. Globals cannot be mutually recursive. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group @@ -27,7 +26,9 @@ type llbc_module = { (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = + type_decl TypeDeclId.Map.t + * fun_decl FunDeclId.Map.t + * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -45,9 +46,11 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types, globals and functions *) +(** Split a module's declarations between types, functions and globals *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = + type_declaration_group list + * fun_declaration_group list + * GlobalDeclId.id list = let rec split decls = match decls with | [] -> ([], [], []) @@ -56,8 +59,7 @@ let split_declarations (decls : declaration_group list) : match d with | Type decl -> (decl :: types, funs, globals) | Fun decl -> (types, decl :: funs, globals) - | Global decl -> (types, funs, decl :: globals) - ) + | Global decl -> (types, funs, decl :: globals)) in split decls @@ -66,7 +68,7 @@ let split_declarations (decls : declaration_group list) : *) let split_declarations_to_group_maps (decls : declaration_group list) : type_declaration_group TypeDeclId.Map.t - * fun_declaration_group FunDeclId.Map.t + * fun_declaration_group FunDeclId.Map.t * GlobalDeclId.Set.t = let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 8a1c074d..e72ff9d7 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -402,7 +402,7 @@ let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) let unwrap_result_ty (ty : ty) : ty = match ty with | Adt (Assumed Result, [ ty ]) -> ty - | _ -> failwith "not a result" + | _ -> failwith "not a result type" let mk_result_fail_texpression (ty : ty) : texpression = let type_args = [ ty ] in |