summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CfimAstUtils.ml4
-rw-r--r--src/PrintPure.ml2
-rw-r--r--src/SymbolicToPure.ml17
-rw-r--r--src/Translate.ml30
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