diff options
| -rw-r--r-- | src/CfimAstUtils.ml | 4 | ||||
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 17 | ||||
| -rw-r--r-- | src/Translate.ml | 30 |
4 files changed, 34 insertions, 19 deletions
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml index 8ef74bef..770184b0 100644 --- a/src/CfimAstUtils.ml +++ b/src/CfimAstUtils.ml @@ -51,3 +51,7 @@ let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) in let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in parents + +let fun_def_get_input_vars (fdef : fun_def) : var list = + let locals = List.tl fdef.locals in + Collections.List.prefix fdef.arg_count locals diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 532278ea..6f56c379 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -105,7 +105,7 @@ let mk_ast_formatter (type_defs : T.type_def TypeDefId.Map.t) in let var_id_to_string vid = (* TODO: somehow lookup in the context *) - "@" ^ VarId.to_string vid + "^" ^ VarId.to_string vid in let adt_field_names = Print.Contexts.type_ctx_to_adt_field_names_fun type_defs diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 14bbc63f..5a3b3e96 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -518,12 +518,12 @@ let translate_fun_sig (types_infos : TA.type_infos) (sg : A.fun_sig) let sg = { type_params; inputs; outputs } in { sg; output_names } -let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : - bs_ctx * var = +let fresh_named_var_for_symbolic_value (basename : string option) + (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh ctx.var_counter in let ty = ctx_translate_fwd_ty ctx sv.sv_ty in - let var = { id; basename = None; ty } in + let var = { id; basename; ty } in (* Insert in the map *) let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in (* Update the context *) @@ -531,10 +531,21 @@ let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : (* Return *) (ctx, var) +let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : + bs_ctx * var = + fresh_named_var_for_symbolic_value None sv ctx + let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl +let fresh_named_vars_for_symbolic_values + (svl : (string option * V.symbolic_value) list) (ctx : bs_ctx) : + bs_ctx * var list = + List.fold_left_map + (fun ctx (name, sv) -> fresh_named_var_for_symbolic_value name sv ctx) + ctx svl + (** This generates a fresh variable **which is not to be linked to any symbolic value** *) let fresh_var (basename : string option) (ty : ty) (ctx : bs_ctx) : bs_ctx * var = diff --git a/src/Translate.ml b/src/Translate.ml index e3f7bbb2..f8634225 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -134,24 +134,25 @@ let translate_function_to_pure (config : C.partial_config) (* We need to initialize the input/output variables *) let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in + let forward_input_vars = CfimAstUtils.fun_def_get_input_vars fdef in + let forward_input_varnames = + List.map (fun (v : A.var) -> v.name) forward_input_vars + in + let num_forward_inputs = fdef.arg_count in let add_forward_inputs input_svs ctx = + let input_svs = List.combine forward_input_varnames input_svs in let ctx, forward_inputs = - SymbolicToPure.fresh_vars_for_symbolic_values input_svs ctx + SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } in - let forward_input_vars, _ = - Collections.List.split_at fdef.locals fdef.arg_count - in - let forward_input_varnames = - List.map (fun (v : A.var) -> v.name) forward_input_vars - in - let forward_inputs = - List.combine forward_input_varnames forward_sg.sg.inputs - in - let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_inputs ctx in - let ctx = { ctx with forward_inputs } in + (* let forward_inputs = + List.combine forward_input_varnames forward_sg.sg.inputs + in + let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_inputs ctx in + + let ctx = { ctx with forward_inputs } in*) (* Translate the forward function *) let pure_forward = @@ -174,8 +175,7 @@ let translate_function_to_pure (config : C.partial_config) RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs in let _, backward_inputs = - Collections.List.split_at backward_sg.sg.inputs - (List.length forward_inputs) + Collections.List.split_at backward_sg.sg.inputs num_forward_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: @@ -239,7 +239,7 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : ( A.Local fdef.def_id, List.map (fun (v : A.var) -> v.name) - (Collections.List.prefix fdef.arg_count fdef.locals), + (CfimAstUtils.fun_def_get_input_vars fdef), fdef.signature )) m.functions in |