From 0c814c97dd8e5167f24b0dbb14186d674e4d097b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 13 Dec 2023 11:44:58 +0100 Subject: Update Pure.fun_sig_info --- compiler/Translate.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 221d4e73..54e24066 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -216,11 +216,15 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* We need to ignore the forward inputs, and the state input (if there is) *) let backward_inputs = let sg = backward_sg.sg in + (* TODO: *) + assert (not !Config.return_back_funs); (* We need to ignore the forward state and the backward state *) let num_forward_inputs = - sg.info.num_fwd_inputs_with_fuel_with_state + sg.info.fwd_info.num_inputs_with_fuel_with_state + in + let num_back_inputs = + (Option.get sg.info.back_info).num_inputs_no_fuel_no_state in - let num_back_inputs = Option.get sg.info.num_back_inputs_no_state in Collections.List.subslice sg.inputs num_forward_inputs (num_forward_inputs + num_back_inputs) in -- cgit v1.2.3 From f1f41818fb14a6c46442ca42a49a3aab0a5b1aaf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 14 Dec 2023 17:48:44 +0100 Subject: Make progress on generated merged fwd/back functions --- compiler/Translate.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 54e24066..06d4bd6d 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -223,7 +223,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) sg.info.fwd_info.num_inputs_with_fuel_with_state in let num_back_inputs = - (Option.get sg.info.back_info).num_inputs_no_fuel_no_state + match sg.info.back_info with + | SingleBack (Some info) -> info.num_inputs_no_fuel_no_state + | _ -> raise (Failure "Unexpected") in Collections.List.subslice sg.inputs num_forward_inputs (num_forward_inputs + num_back_inputs) -- cgit v1.2.3 From 884edaa3ee975626f184249d491f343fc02a66e2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 15 Dec 2023 18:54:06 +0100 Subject: Make progress on updating the code --- compiler/Translate.ml | 207 +++++++++++++++++++++++--------------------------- 1 file changed, 93 insertions(+), 114 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 06d4bd6d..8b221c93 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -6,7 +6,6 @@ open LlbcAst open Contexts module SA = SymbolicAst module Micro = PureMicroPasses -open PureUtils open TranslateCore (** The local logger *) @@ -43,7 +42,6 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : TODO: maybe we should introduce a record for this. *) let translate_function_to_pure (trans_ctx : trans_ctx) - (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = (* Debug *) @@ -58,13 +56,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Convert the symbolic ASTs to pure ASTs: *) (* Initialize the context *) - let forward_sig = - RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs - in let sv_to_var = SymbolicValueId.Map.empty in let var_counter = Pure.VarId.generator_zero in let state_var, var_counter = Pure.VarId.fresh var_counter in - let back_state_var, var_counter = Pure.VarId.fresh var_counter in let fuel0, var_counter = Pure.VarId.fresh var_counter in let fuel, var_counter = Pure.VarId.fresh var_counter in let calls = FunCallId.Map.empty in @@ -89,7 +83,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) let fun_context = { SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; - fun_sigs; fun_infos = trans_ctx.fun_ctx.fun_infos; regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies; } @@ -126,17 +119,45 @@ let translate_function_to_pure (trans_ctx : trans_ctx) !m in + let input_names = + match fdef.body with + | None -> List.map (fun _ -> None) fdef.signature.inputs + | Some body -> + List.map + (fun (v : var) -> v.name) + (LlbcAstUtils.fun_body_get_input_vars body) + in + + let sg = + SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx (FRegular def_id) + fdef.signature input_names + in + + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies + in + + let var_counter, back_state_vars = + if !Config.return_back_funs then (var_counter, []) + else + List.fold_left_map + (fun var_counter (region_vars : region_var_group) -> + let gid = region_vars.id in + let var, var_counter = Pure.VarId.fresh var_counter in + (var_counter, (gid, var))) + var_counter regions_hierarchy + in + let back_state_vars = RegionGroupId.Map.of_list back_state_vars in + let ctx = { SymbolicToPure.bid = None; - (* Dummy for now *) - sg = forward_sig.sg; - fwd_sg = forward_sig.sg; + sg; (* Will need to be updated for the backward functions *) sv_to_var; - var_counter; + var_counter = ref var_counter; state_var; - back_state_var; + back_state_vars; fuel0; fuel; type_context; @@ -146,9 +167,11 @@ let translate_function_to_pure (trans_ctx : trans_ctx) trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls; fun_decl = fdef; forward_inputs = []; - (* Empty for now *) - backward_inputs = RegionGroupId.Map.empty; - (* Empty for now *) + (* Initialized just below *) + backward_inputs_no_state = RegionGroupId.Map.empty; + (* Initialized just below *) + backward_inputs_with_state = RegionGroupId.Map.empty; + (* Initialized just below *) backward_outputs = RegionGroupId.Map.empty; loop_backward_outputs = None; (* Empty for now *) @@ -180,6 +203,51 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | _ -> raise (Failure "Unreachable") in + (* Add the backward inputs *) + let ctx, backward_inputs_no_state, backward_inputs_with_state = + if !Config.return_back_funs then (ctx, [], []) + else + let ctx, inputs_no_with_state = + List.fold_left_map + (fun ctx (region_vars : region_var_group) -> + let gid = region_vars.id in + let back_sg = RegionGroupId.Map.find gid sg.back_sg in + let ctx, no_state = + SymbolicToPure.fresh_vars back_sg.inputs_no_state ctx + in + let ctx, with_state = + SymbolicToPure.fresh_vars back_sg.inputs ctx + in + (ctx, ((gid, no_state), (gid, with_state)))) + ctx regions_hierarchy + in + let inputs_no_state, inputs_with_state = + List.split inputs_no_with_state + in + (ctx, inputs_no_state, inputs_with_state) + in + let backward_inputs_no_state = + RegionGroupId.Map.of_list backward_inputs_no_state + in + let backward_inputs_with_state = + RegionGroupId.Map.of_list backward_inputs_with_state + in + let ctx = { ctx with backward_inputs_no_state; backward_inputs_with_state } in + + (* Add the backward outputs *) + let ctx, backward_outputs = + List.fold_left_map + (fun ctx (region_vars : region_var_group) -> + let gid = region_vars.id in + let back_sg = RegionGroupId.Map.find gid sg.back_sg in + let outputs = List.combine back_sg.output_names back_sg.outputs in + let ctx, vars = SymbolicToPure.fresh_vars outputs ctx in + (ctx, (gid, vars))) + ctx regions_hierarchy + in + let backward_outputs = RegionGroupId.Map.of_list backward_outputs in + let ctx = { ctx with backward_outputs } in + (* Translate the forward function *) let pure_forward = match symbolic_trans with @@ -187,7 +255,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) in - (* Translate the backward functions *) + (* Translate the backward functions, if we split the forward and backward functions *) let translate_backward (rg : region_var_group) : Pure.fun_decl = (* For the backward inputs/outputs initialization: we use the fact that * there are no nested borrows for now, and so that the region groups @@ -197,83 +265,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx) match symbolic_trans with | None -> - (* Initialize the context - note that the ret_ty is not really - * useful as we don't translate a body *) - let backward_sg = - RegularFunIdNotLoopMap.find (FRegular def_id, Some back_id) fun_sigs - in - let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in - + (* Initialize the context *) + let ctx = { ctx with bid = Some back_id } in (* Translate *) SymbolicToPure.translate_fun_decl ctx None | Some (_, symbolic) -> - (* Finish initializing the context by adding the additional input - variables required by the backward function. - *) - let backward_sg = - RegularFunIdNotLoopMap.find (FRegular def_id, Some back_id) fun_sigs - in - (* We need to ignore the forward inputs, and the state input (if there is) *) - let backward_inputs = - let sg = backward_sg.sg in - (* TODO: *) - assert (not !Config.return_back_funs); - (* We need to ignore the forward state and the backward state *) - let num_forward_inputs = - sg.info.fwd_info.num_inputs_with_fuel_with_state - in - let num_back_inputs = - match sg.info.back_info with - | SingleBack (Some info) -> info.num_inputs_no_fuel_no_state - | _ -> raise (Failure "Unexpected") - in - Collections.List.subslice sg.inputs num_forward_inputs - (num_forward_inputs + num_back_inputs) - in - (* As we forbid nested borrows, the additional inputs for the backward - * functions come from the borrows in the return value of the rust function: - * we thus use the name "ret" for those inputs *) - let backward_inputs = - List.map (fun ty -> (Some "ret", ty)) backward_inputs - in - let ctx, backward_inputs = - SymbolicToPure.fresh_vars backward_inputs ctx - in - (* The outputs for the backward functions, however, come from borrows - * present in the input values of the rust function: for those we reuse - * the names of the input values. *) - let backward_outputs = - List.combine backward_sg.output_names backward_sg.sg.doutputs - in - let ctx, backward_outputs = - SymbolicToPure.fresh_vars backward_outputs ctx - in - let backward_inputs = - RegionGroupId.Map.singleton back_id backward_inputs - in - let backward_outputs = - RegionGroupId.Map.singleton back_id backward_outputs - in - - (* Put everything in the context *) - let ctx = - { - ctx with - bid = Some back_id; - sg = backward_sg.sg; - backward_inputs; - backward_outputs; - } - in - + (* Initialize the context *) + let ctx = { ctx with bid = Some back_id } in (* Translate *) SymbolicToPure.translate_fun_decl ctx (Some symbolic) in - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular fdef.def_id) - fun_context.regions_hierarchies + let pure_backwards = + if !Config.return_back_funs then [] + else List.map translate_backward regions_hierarchy in - let pure_backwards = List.map translate_backward regions_hierarchy in (* Return *) (pure_forward, pure_backwards) @@ -300,36 +305,10 @@ let translate_crate_to_pure (crate : crate) : (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls) in - (* Translate all the function *signatures* *) - let assumed_sigs = - List.map - (fun (info : Assumed.assumed_fun_info) -> - ( FAssumed info.fun_id, - List.map (fun _ -> None) info.fun_sig.inputs, - info.fun_sig )) - Assumed.assumed_fun_infos - in - let local_sigs = - List.map - (fun (fdef : fun_decl) -> - let input_names = - match fdef.body with - | None -> List.map (fun _ -> None) fdef.signature.inputs - | Some body -> - List.map - (fun (v : var) -> v.name) - (LlbcAstUtils.fun_body_get_input_vars body) - in - (FRegular fdef.def_id, input_names, fdef.signature)) - (FunDeclId.Map.values crate.fun_decls) - in - let sigs = List.append assumed_sigs local_sigs in - let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in - (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure trans_ctx fun_sigs type_decls_map) + (translate_function_to_pure trans_ctx type_decls_map) (FunDeclId.Map.values crate.fun_decls) in @@ -1036,7 +1015,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : List.map (fun { fwd; _ } -> let fwd_f = - if fwd.f.Pure.signature.info.effect_info.is_rec then + if fwd.f.Pure.signature.fwd_info.effect_info.is_rec then [ (fwd.f.def_id, None) ] else [] in -- cgit v1.2.3 From a49754a5b11e4de8793dc7e13c2962d139eb03b1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Dec 2023 10:21:08 +0100 Subject: Rename some definitions --- compiler/Translate.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 8b221c93..e153f4f4 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -72,7 +72,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | RecGroup _ -> Some tid) (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) in - let type_context = + let type_ctx = { SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos; llbc_type_decls = trans_ctx.type_ctx.type_decls; @@ -80,14 +80,14 @@ let translate_function_to_pure (trans_ctx : trans_ctx) recursive_decls = recursive_type_decls; } in - let fun_context = + let fun_ctx = { SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; fun_infos = trans_ctx.fun_ctx.fun_infos; regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies; } in - let global_context = + let global_ctx = { SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls } in @@ -134,7 +134,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies + LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_ctx.regions_hierarchies in let var_counter, back_state_vars = @@ -160,9 +160,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx) back_state_vars; fuel0; fuel; - type_context; - fun_context; - global_context; + type_ctx; + fun_ctx; + global_ctx; trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls; trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls; fun_decl = fdef; -- cgit v1.2.3 From 4f7bc41dcbc6187512111a81f968726452024d25 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Dec 2023 12:54:40 +0100 Subject: Simplify SymbolicToPure.bs_ctx.{backward_outputs, loop_backward_outputs} --- compiler/Translate.ml | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index e153f4f4..0fa0202b 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -171,8 +171,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) backward_inputs_no_state = RegionGroupId.Map.empty; (* Initialized just below *) backward_inputs_with_state = RegionGroupId.Map.empty; - (* Initialized just below *) - backward_outputs = RegionGroupId.Map.empty; + backward_outputs = None; loop_backward_outputs = None; (* Empty for now *) calls; @@ -234,20 +233,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in let ctx = { ctx with backward_inputs_no_state; backward_inputs_with_state } in - (* Add the backward outputs *) - let ctx, backward_outputs = - List.fold_left_map - (fun ctx (region_vars : region_var_group) -> - let gid = region_vars.id in - let back_sg = RegionGroupId.Map.find gid sg.back_sg in - let outputs = List.combine back_sg.output_names back_sg.outputs in - let ctx, vars = SymbolicToPure.fresh_vars outputs ctx in - (ctx, (gid, vars))) - ctx regions_hierarchy - in - let backward_outputs = RegionGroupId.Map.of_list backward_outputs in - let ctx = { ctx with backward_outputs } in - (* Translate the forward function *) let pure_forward = match symbolic_trans with -- cgit v1.2.3 From 014c0668abf0834342b2b7076cf2f0634460e519 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Dec 2023 13:24:53 +0100 Subject: Remove SymbolicToPure.bs_ctx.loop_backward_outputs --- compiler/Translate.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0fa0202b..631a5af9 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -172,7 +172,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialized just below *) backward_inputs_with_state = RegionGroupId.Map.empty; backward_outputs = None; - loop_backward_outputs = None; (* Empty for now *) calls; abstractions; -- cgit v1.2.3 From 8835d87df111d09122267fadc9a32f16b52d234a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 21 Dec 2023 14:37:43 +0100 Subject: Make good progress on merging the fwd/back functions --- compiler/Translate.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 631a5af9..5584fb9a 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -129,7 +129,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in let sg = - SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx (FRegular def_id) + SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx def_id fdef.signature input_names in @@ -151,6 +151,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) let ctx = { + decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; (* Will need to be updated for the backward functions *) -- cgit v1.2.3 From 266db04e97778911c93cfd1aac251de04bb25f53 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 21 Dec 2023 22:17:11 +0100 Subject: Fix several issues --- compiler/Translate.ml | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 5584fb9a..ccc46420 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -42,7 +42,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : TODO: maybe we should introduce a record for this. *) let translate_function_to_pure (trans_ctx : trans_ctx) - (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) : + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) + (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = (* Debug *) log#ldebug @@ -119,18 +120,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx) !m in - let input_names = - match fdef.body with - | None -> List.map (fun _ -> None) fdef.signature.inputs - | Some body -> - List.map - (fun (v : var) -> v.name) - (LlbcAstUtils.fun_body_get_input_vars body) - in - let sg = - SymbolicToPure.translate_fun_sig_to_decomposed trans_ctx def_id - fdef.signature input_names + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef in let regions_hierarchy = @@ -154,6 +145,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; + fun_dsigs; (* Will need to be updated for the backward functions *) sv_to_var; var_counter = ref var_counter; @@ -290,10 +282,21 @@ let translate_crate_to_pure (crate : crate) : (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls) in + (* Compute the decomposed fun sigs for the whole crate *) + let fun_dsigs = + FunDeclId.Map.of_list + (List.map + (fun (fdef : LlbcAst.fun_decl) -> + ( fdef.def_id, + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx + fdef )) + (FunDeclId.Map.values crate.fun_decls)) + in + (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure trans_ctx type_decls_map) + (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in -- cgit v1.2.3 From 455ba366f9c8d07a1f1848ec0960b1f2d161e7cf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 22 Dec 2023 18:47:50 +0100 Subject: Update the library for F* --- compiler/Translate.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index ccc46420..55a94302 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1171,7 +1171,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let exe_dir = Filename.dirname Sys.argv.(0) in let primitives_src_dest = match !Config.backend with - | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") + | FStar -> + let src = + if !Config.return_back_funs then + "/backends/fstar/merge/Primitives.fst" + else "/backends/fstar/split/Primitives.fst" + in + Some (src, "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None | HOL4 -> None -- cgit v1.2.3