diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ExtractToFStar.ml | 64 | ||||
| -rw-r--r-- | src/FunsAnalysis.ml | 13 | ||||
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 7 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 37 | ||||
| -rw-r--r-- | src/Modules.ml | 27 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 32 | ||||
| -rw-r--r-- | src/PureTypeCheck.ml | 7 | ||||
| -rw-r--r-- | src/PureUtils.ml | 5 | ||||
| -rw-r--r-- | src/Translate.ml | 21 |
10 files changed, 134 insertions, 83 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2c53e45b..a2b15ece 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -313,11 +313,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* Concatenate the elements *) String.concat "_" fname in - let fun_name (_fid : A.fun_id) (fname : fun_name) (is_global : bool) (num_rgs : int) + let global_name (name : global_name) : string = + let parts = List.map to_snake_case (get_name name) in + String.concat "_" parts + in + let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) : string = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) - let suffix = default_fun_suffix is_global num_rgs rg filter_info in + let suffix = default_fun_suffix num_rgs rg filter_info in (* Concatenate *) fname ^ suffix in @@ -411,6 +415,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) variant_name; struct_constructor; type_name; + global_name; fun_name; decreases_clause_name; var_basename; @@ -839,6 +844,11 @@ let extract_adt_g_value ctx | _ -> raise (Failure "Inconsistent typed value") +(* Extract globals in the same way as variables *) +let extract_global (ctx : extraction_ctx) (fmt : F.formatter) + (id : A.GlobalDeclId.id) : unit = + F.pp_print_string fmt (ctx_get_global_decl id ctx) + (** [inside]: see [extract_ty]. As an pattern can introduce new variables, we return an extraction context @@ -907,12 +917,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Func fun_id -> extract_function_call ctx fmt inside fun_id qualif.type_args args | Global global_id -> - failwith "TODO ExtractToFStar.ml:911" - (* Previous code: - let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in - let fun_id = Regular (A.Regular fid, None) in - extract_function_call ctx fmt inside fun_id qualif.type_args args - *) + 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 -> @@ -1353,6 +1358,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) : unit = + assert (def.is_global_body); (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1551,40 +1557,40 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) `let x_c : int = eval_global x_body` *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (def : fun_decl) - : unit = - (* TODO Lookup LLBC decl *) - (* Sanity checks for globals *) - assert (def.is_global_body); - failwith "TODO ExtractToFStar.ml:1559" - (* Previous code: - assert (Option.is_none def.back_id); - assert (List.length def.signature.inputs = 0); - assert (List.length def.signature.doutputs = 1); - assert (List.length def.signature.type_params = 0); - assert (not def.signature.info.effect_info.can_fail); + (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = + 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.fun_name_to_string def.basename ^ "] *)"); + F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); F.pp_print_space fmt (); - let def_name = ctx_get_local_function def.def_id def.back_id ctx in - match def.body with + let decl_name = ctx_get_global_decl global.def_id ctx in + let body_name = ctx_get_global_body global.def_id 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) + in + match body.body with | None -> - extract_global_definition ctx fmt qualif def_name def.signature.output None + let qualif = if interface then Val else AssumeVal in + extract_global_definition ctx fmt qualif decl_name decl_ty None | Some body -> - let body_name = global_decl_to_body_name def_name in - let body_ty = mk_result_ty def.signature.output in - extract_global_definition ctx fmt qualif body_name body_ty (Some (fun fmt -> + extract_global_definition 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_definition ctx fmt qualif def_name def.signature.output (Some (fun fmt -> + extract_global_definition 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/FunsAnalysis.ml b/src/FunsAnalysis.ml index 3a6ad542..65a130c8 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -1,7 +1,7 @@ (** Compute various information, including: - can a function fail (by having `Fail` in its body, or transitively calling a function which can fail), false for globals - - can a function diverge (bu being recursive, containing a loop or + - can a function diverge (by being recursive, containing a loop or transitively calling a function which can diverge) - does a function perform stateful operations (i.e., do we need a state to translate it) @@ -26,7 +26,9 @@ type fun_info = { type modules_funs_info = fun_info FunDeclId.Map.t (** Various information about a module's functions *) -let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) +let analyze_module (m : llbc_module) + (funs_map : fun_decl FunDeclId.Map.t) + (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : modules_funs_info = let infos = ref FunDeclId.Map.empty in @@ -104,7 +106,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) * syntactically can't fail don't use an error monad. *) in List.iter visit_fun d; - (* Not-failing functions are not handled yet. *) + (* Non-failing functions are not handled yet. *) can_fail := true; { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } in @@ -126,6 +128,11 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) | Fun decl :: decls' -> analyze_fun_decl_group decl; analyze_decl_groups decls' + | Global id :: decls' -> + (* Analyze a global by analyzing its body function *) + let global = GlobalDeclId.Map.find id globals_map in + analyze_fun_decl_group (NonRec global.body_id); + analyze_decl_groups decls' in analyze_decl_groups m.declarations; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3610d486..51144ba2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -15,9 +15,9 @@ let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : C.type_context * C.fun_context * C.global_context = - let type_decls_list, _ = M.split_declarations m.declarations in + let type_decls_list, _, _ = M.split_declarations m.declarations in let type_decls, fun_decls, global_decls = M.compute_defs_maps m in - let type_decls_groups, _funs_defs_groups = + let type_decls_groups, _funs_defs_groups, _globals_defs_groups = M.split_declarations_to_group_maps m.declarations in let type_infos = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 3f6470b9..ffc47741 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,11 +919,16 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (* Treat the global as a function without arguments to call *) (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> + (* + let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in + (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx + *) + failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; (* Treat the global as a fresh symbolic value *) let rty = ety_no_regions_to_rty global.ty in let sval = mk_fresh_symbolic_value V.FunCallRet rty in let sval = mk_typed_value_from_symbolic_value sval in - assign_to_place config sval place (cf Unit) ctx + (assign_to_place config sval place) (cf Unit) ctx (** 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 f51c15be..be43ff54 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -698,18 +698,18 @@ let fun_declaration_group_of_json (js : json) : combine_error_msgs js "fun_declaration_group_of_json" (g_declaration_group_of_json A.FunDeclId.id_of_json js) -(* TODO Should a global declaration group be converted to its function bodies ? - It does not seems very clean. -*) -let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) : - (M.fun_declaration_group, string) result = +let global_declaration_group_of_json (js : json) : + (A.GlobalDeclId.id, string) result = combine_error_msgs js "global_declaration_group_of_json" - (g_declaration_group_of_json (fun js -> - let* id = A.GlobalDeclId.id_of_json js in - Ok (global_to_fun_id gid_conv id) - ) js) - -let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result + (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 = combine_error_msgs js "declaration_of_json" (match js with @@ -720,8 +720,8 @@ let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M. let* decl = fun_declaration_group_of_json decl in Ok (M.Fun decl) | `Assoc [ ("Global", `List [ decl ]) ] -> - let* decl = global_declaration_group_of_json decl gid_conv in - Ok (M.Fun decl) + let* id = global_declaration_group_of_json decl in + Ok (M.Global id) | _ -> Error "") let length_of_json_list (js: json) : (int, string) result = @@ -741,15 +741,12 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("functions", functions); ("globals", globals); ] -> - let* fun_count = length_of_json_list functions in - let gid_conv = { fun_count } in let* name = string_of_json name in - let* declarations = - list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations - in - let* types = list_of_json type_decl_of_json types 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 - let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in + 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, global_bodies = List.split globals in Ok { M.name; diff --git a/src/Modules.ml b/src/Modules.ml index 2f640636..009e1ba6 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -10,10 +10,11 @@ type type_declaration_group = TypeDeclId.id g_declaration_group type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] -(** Module declaration *) +(** Module declaration. Globals cannot be mutually dependent. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group + | Global of GlobalDeclId.id [@@deriving show] type llbc_module = { @@ -44,26 +45,29 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types and functions *) +(** Split a module's declarations between types, globals and functions *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list = + type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = let rec split decls = match decls with - | [] -> ([], []) + | [] -> ([], [], []) | d :: decls' -> ( - let types, funs = split decls' in + let types, funs, globals = split decls' in match d with - | Type decl -> (decl :: types, funs) - | Fun decl -> (types, decl :: funs)) + | Type decl -> (decl :: types, funs, globals) + | Fun decl -> (types, decl :: funs, globals) + | Global decl -> (types, funs, decl :: globals) + ) in split decls -(** Split a module's declarations into two maps from type/fun ids to +(** Split a module's declarations into three maps from type/fun/global ids to declaration groups. *) 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) (group : M.key g_declaration_group) : M.key g_declaration_group M.t = @@ -75,9 +79,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) : M.key g_declaration_group M.t = List.fold_left add_group M.empty groups end in - let types, funs = split_declarations decls in + let types, funs, globals = split_declarations decls in let module TG = G (TypeDeclId.Map) in let types = TG.create_map types in let module FG = G (FunDeclId.Map) in let funs = FG.create_map funs in - (types, funs) + let globals = GlobalDeclId.Set.of_list globals in + (types, funs, globals) diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 2d76f348..1dc7eae9 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -32,6 +32,8 @@ type name = Names.name type type_name = Names.type_name +type global_name = Names.global_name + type fun_name = Names.fun_name (* TODO: this should a module we give to a functor! *) @@ -71,10 +73,11 @@ type formatter = { *) type_name : type_name -> string; (** Provided a basename, compute a type name. *) + global_name : global_name -> string; + (** Provided a basename, compute a global name. *) fun_name : A.fun_id -> fun_name -> - bool -> int -> region_group_info option -> bool * int -> @@ -83,7 +86,6 @@ type formatter = { - function id: this is especially useful to identify whether the function is an assumed function or a local function - function basename - - flag indicating if the function is a global - number of region groups - region group information in case of a backward function (`None` if forward function) @@ -186,6 +188,7 @@ type formatter = { (** We use identifiers to look for name clashes *) type id = + | GlobalId of A.GlobalDeclId.id | FunId of A.fun_id * RegionGroupId.id option | DecreasesClauseId of A.fun_id (** The definition which provides the decreases/termination clause. @@ -342,6 +345,7 @@ type extraction_ctx = { (** Debugging function *) let id_to_string (id : id) (ctx : extraction_ctx) : string = + let global_decls = ctx.trans_ctx.global_context.global_decls in let fun_decls = ctx.trans_ctx.fun_context.fun_decls in let type_decls = ctx.trans_ctx.type_context.type_decls in (* TODO: factorize the pretty-printing with what is in PrintPure *) @@ -354,6 +358,9 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | Tuple -> failwith "Unreachable" in match id with + | GlobalId gid -> + let name = (A.GlobalDeclId.Map.find gid global_decls).name in + "global name: " ^ Print.global_name_to_string name | FunId (fid, rg_id) -> let fun_name = match fid with @@ -442,6 +449,12 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found +let ctx_get_global_decl (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx ^ "_c" + +let ctx_get_global_body (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx ^ "_body" + let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = @@ -572,6 +585,10 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx +let ctx_add_global_decl (def : A.global_decl) (ctx : extraction_ctx) : + extraction_ctx = + ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx + let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Lookup the LLBC def to compute the region group information *) @@ -600,11 +617,12 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in - (* Add the function name *) - let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in - ctx + (* Add the function name if it's not a global *) + if def.is_global_body + then ctx + else ctx_add (FunId (def_id, def.back_id)) name ctx type names_map_init = { keywords : string list; @@ -671,7 +689,6 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = TODO: move all those helpers. *) let default_fun_suffix - (is_global_body : bool) (num_region_groups : int) (rg : region_group_info option) ((keep_fwd, num_backs) : bool * int) @@ -691,7 +708,6 @@ let default_fun_suffix we could not add the "_fwd" suffix) to prevent name clashes between definitions (in particular between type and function definitions). *) - if is_global_body then "_body" else match rg with | None -> "_fwd" | Some rg -> diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml index c63814eb..39fb5073 100644 --- a/src/PureTypeCheck.ml +++ b/src/PureTypeCheck.ml @@ -112,11 +112,8 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = check_texpression ctx body | Qualif qualif -> ( match qualif.id with - | Func _ -> () (* TODO *) - | Global id -> - let global = A.GlobalDeclId.Map.find id ctx.global_decls in - (* TODO: something like assert (global.ty = e.ty) *) - failwith "PureTypeCheck.ml:118" + | Func _ -> () (* TODO *) + | Global _ -> () (* TODO *) | Proj { adt_id = proj_adt_id; field_id } -> (* Note we can only project fields of structures (not enumerations) *) (* Deconstruct the projector type *) diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 8d3b5258..8a1c074d 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -399,6 +399,11 @@ let type_decl_is_enum (def : T.type_decl) : bool = let mk_state_ty : ty = Adt (Assumed State, []) 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" + let mk_result_fail_texpression (ty : ty) : texpression = let type_args = [ ty ] in let ty = Adt (Assumed Result, type_args) in diff --git a/src/Translate.ml b/src/Translate.ml index a6477e7f..a936d626 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -298,7 +298,7 @@ let translate_module_to_pure (config : C.partial_config) (* Compute the type and function contexts *) let type_context, fun_context, global_context = compute_type_fun_contexts m in - let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in + let fun_infos = FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls use_state in let fun_context = { fun_decls = fun_context.fun_decls; fun_infos; @@ -498,9 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then if def.is_global_body - then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def - else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def + then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def ) fls); (* Insert unit tests if necessary *) @@ -512,6 +510,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) pure_ls in + (* TODO: Check correct behaviour with opaque globals *) + let export_global (id : A.GlobalDeclId.id) : unit = + let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in + let global = A.GlobalDeclId.Map.find id global_decls in + let (_, (body, body_backs)) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + assert (List.length body_backs = 0); + + let is_opaque = Option.is_none body.Pure.body in + if ((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque) + then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body config.interface + in + let export_state_type () : unit = let qualif = if config.interface then ExtractToFStar.TypeVal @@ -547,6 +558,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) in (* Translate *) export_functions true pure_funs + | Global id -> + export_global id in (* If we need to export the state type: we try to export it after we defined |