summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--TODO.md4
-rw-r--r--src/Pure.ml3
-rw-r--r--src/SymbolicToPure.ml94
3 files changed, 94 insertions, 7 deletions
diff --git a/TODO.md b/TODO.md
index 71d28517..a70e4546 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,10 @@
0. update the end borrows internal to abstractions to not introduce a Bottom
+0. remove AConcrete from avalue
+
+0. remove ABottom from avalue
+
1. reorder the branches of matches
1. stateful maps/sets modules (hashtbl?)
diff --git a/src/Pure.ml b/src/Pure.ml
index 1f66906d..566ba46b 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -74,7 +74,8 @@ type var_or_dummy = Var of var | Dummy (** Ignored value: `_` *)
(** A left value (which appears on the left of assignments *)
type lvalue =
| LvVar of var_or_dummy
- | LvTuple of lvalue list (** Rk.: for now we don't support general ADTs *)
+ | LvTuple of typed_lvalue list
+ (** Rk.: for now we don't support general ADTs *)
and typed_lvalue = { value : lvalue; ty : ty }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 442ec18c..b121ae33 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -531,6 +531,7 @@ 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
+(* TODO: rename *)
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
@@ -629,7 +630,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (lc : V.aloan_content) :
* borrow is in practice immutable) *)
None
| AIgnoredMutLoan (_, _) ->
- (* There can be *inner* mutable loans, but not outer ones *)
+ (* There can be *inner* not ended mutable loans, but not outer ones *)
failwith "Unreachable"
| AEndedIgnoredMutLoan _ ->
(* This happens with nested borrows: we need to dive in *)
@@ -643,9 +644,9 @@ and aborrow_content_to_consumed (ctx : bs_ctx) (bc : V.aborrow_content) :
match bc with
| V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
failwith "Unreachable"
- | AEndedMutBorrow (mv, _) ->
- (* Return the meta-value *)
- Some (translate_typed_value_to_rvalue ctx mv)
+ | AEndedMutBorrow (_, _) ->
+ (* We collect consumed values: ignore *)
+ None
| AEndedIgnoredMutBorrow _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
@@ -676,9 +677,90 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
-let typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
+let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
bs_ctx * typed_lvalue option =
- raise Unimplemented
+ match av.value with
+ | AConcrete _ -> failwith "Unreachable"
+ | AAdt adt_v -> (
+ (* Translate the field values *)
+ let ctx, field_values =
+ List.fold_left_map
+ (fun ctx fv -> typed_avalue_to_given_back fv ctx)
+ ctx adt_v.field_values
+ in
+ let field_values = List.filter_map (fun x -> x) field_values in
+ (* For now, only tuples can contain borrows *)
+ let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
+ match adt_id with
+ | T.AdtId _ | T.Assumed T.Box ->
+ assert (field_values = []);
+ (ctx, None)
+ | T.Tuple ->
+ (* Return *)
+ let variant_id = adt_v.variant_id in
+ if field_values = [] then (ctx, None)
+ else
+ let value = LvTuple field_values in
+ let ty = translate_fwd_ty ctx av.ty in
+ let lv : typed_lvalue = { value; ty } in
+ (ctx, Some lv))
+ | ABottom -> failwith "Unreachable"
+ | ALoan lc -> aloan_content_to_given_back lc ctx
+ | ABorrow bc -> aborrow_content_to_given_back bc ctx
+ | ASymbolic aproj -> aproj_to_given_back aproj ctx
+ | AIgnored -> (ctx, None)
+
+and aloan_content_to_given_back (lc : V.aloan_content) (ctx : bs_ctx) :
+ bs_ctx * typed_lvalue option =
+ match lc with
+ | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
+ | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
+ | AEndedSharedLoan (_, _) ->
+ (* We consider given back values, and thus ignore those *)
+ (ctx, None)
+ | AIgnoredMutLoan (_, _) ->
+ (* There can be *inner* not ended mutable loans, but not outer ones *)
+ failwith "Unreachable"
+ | AEndedIgnoredMutLoan _ ->
+ (* This happens with nested borrows: we need to dive in *)
+ raise Unimplemented
+ | AIgnoredSharedLoan _ ->
+ (* Ignore *)
+ (ctx, None)
+
+and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) :
+ bs_ctx * typed_lvalue option =
+ match bc with
+ | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+ failwith "Unreachable"
+ | AEndedMutBorrow (mv, _) ->
+ (* Return the meta-value *)
+ let ctx, var = fresh_var_for_symbolic_value mv ctx in
+ (ctx, Some (mk_typed_lvalue_from_var var))
+ | AEndedIgnoredMutBorrow _ ->
+ (* This happens with nested borrows: we need to dive in *)
+ raise Unimplemented
+ | AProjSharedBorrow _ ->
+ (* Ignore *)
+ (ctx, None)
+
+and aproj_to_given_back (aproj : V.aproj) (ctx : bs_ctx) :
+ bs_ctx * typed_lvalue option =
+ match aproj with
+ | V.AEndedProjLoans (_, child_projs) ->
+ (* There may be children borrow projections in case of nested borrows,
+ * in which case we need to dive in - we disallow nested borrows for now *)
+ assert (
+ List.for_all
+ (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows)
+ child_projs);
+ (ctx, None)
+ | AEndedProjBorrows mv ->
+ (* Return the meta-value *)
+ let ctx, var = fresh_var_for_symbolic_value mv ctx in
+ (ctx, Some (mk_typed_lvalue_from_var var))
+ | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
+ failwith "Unreachable"
let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_lvalue list
=