summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/SymbolicAstUtils.ml2
-rw-r--r--src/SymbolicToPure.ml50
2 files changed, 35 insertions, 17 deletions
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml
index f781ed65..264f9cad 100644
--- a/src/SymbolicAstUtils.ml
+++ b/src/SymbolicAstUtils.ml
@@ -21,6 +21,8 @@ type ended_loan_or_borrow =
loans/borrows of an abstraction
We expect an abstraction where all the loans/borrows have ended.
+
+ TODO: remove
*)
let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
=
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 7cae951b..acd40017 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -105,6 +105,7 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
let ty = v.ty in
{ value; ty }
+(* TODO: move *)
let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
let value = LvVar (Var v) in
let ty = v.ty in
@@ -114,12 +115,6 @@ let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
let type_def_is_enum (def : T.type_def) : bool =
match def.kind with T.Struct _ -> false | Enum _ -> true
-(* TODO: move *)
-let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
- let value = LvVar (Var v) in
- let ty = v.ty in
- { value; ty }
-
type type_context = {
types_infos : TA.type_infos;
cfim_type_defs : T.type_def TypeDefId.Map.t;
@@ -155,6 +150,12 @@ type bs_ctx = {
fun_context : fun_context;
fun_def : A.fun_def;
bid : T.RegionGroupId.id option;
+ sv_to_var : var V.SymbolicValueId.Map.t;
+ (** Whenever we encounter a new symbolic value (introduced because of
+ a symbolic expansion or upon ending an abstraction, for instance)
+ we introduce a new variable (with a let-binding).
+ *)
+ var_counter : VarId.generator;
forward_inputs : var list;
(** The input parameters for the forward function *)
backward_inputs : var list T.RegionGroupId.Map.t;
@@ -192,11 +193,15 @@ let fs_ctx_to_bs_ctx (fs_ctx : fs_ctx) : bs_ctx =
} =
fs_ctx
in
+ let sv_to_var = V.SymbolicValueId.Map.empty in
+ let var_counter = VarId.generator_zero in
let calls = V.FunCallId.Map.empty in
let abstractions = V.AbstractionId.Map.empty in
{
fun_def;
bid;
+ sv_to_var;
+ var_counter;
type_context;
fun_context;
forward_inputs;
@@ -509,8 +514,30 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def)
(* Return *)
{ type_params; inputs; outputs }
+let fresh_var_for_symbolic_value (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 = translate_fwd_ty ctx sv.sv_ty in
+ let var = { id; 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 *)
+ let ctx = { ctx with var_counter; sv_to_var } in
+ (* Return *)
+ (ctx, var)
+
+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 get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
+ V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
+
(** Translate a typed value.
+ It is used, for instance, on values used as inputs for function calls.
+
**IMPORTANT**: this function makes the assumption that the typed value
doesn't contain ⊥. This means in particular that symbolic values don't
contain ended regions.
@@ -526,17 +553,6 @@ let translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
typed_rvalue =
raise Unimplemented
-let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) :
- bs_ctx * var =
- raise Unimplemented
-
-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 get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
- raise Unimplemented
-
let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
typed_rvalue option =
raise Unimplemented