From ff3c466ee12014f659283551a7eb99f2ffabb57d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jan 2022 22:18:25 +0100
Subject: Start working on translate_typed_value_to_rvalue
---
src/Pure.ml | 13 +------------
src/SymbolicToPure.ml | 31 ++++++++++++++++++++++++++++---
2 files changed, 29 insertions(+), 15 deletions(-)
diff --git a/src/Pure.ml b/src/Pure.ml
index 45907610..1f66906d 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -54,17 +54,6 @@ type scalar_value = V.scalar_value
type constant_value = V.constant_value
-type symbolic_value = {
- sv_id : SymbolicValueId.id;
- sv_ty : ty;
- sv_rty : T.rty;
- sv_ended_regions : RegionId.Set.t;
- (** We need to remember what was the set of ended regions at the time the
- symbolic value was introduced.
- *)
-}
-(** TODO: remove *)
-
type value = Concrete of constant_value | Adt of adt_value
and adt_value = {
@@ -96,8 +85,8 @@ type projection = projection_elem list
type place = { var : VarId.id; projection : projection }
type rvalue =
- | RvPlace of place
| RvConcrete of constant_value
+ | RvPlace of place
| RvAdt of adt_rvalue
and adt_rvalue = {
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index acd40017..91f355ee 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -543,15 +543,40 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
contain ended regions.
TODO: we might want to remember in the symbolic AST the set of ended
- regions, at the points where we need it, for sanity checks.
+ regions, at the points where we need it, for sanity checks (though the
+ sanity checks in the symbolic interpreter should be enough).
The points where we need this set so far:
- function call
- end abstraction
- return
+
+ TODO: we need the evaluation context to lookup shared borrows!!!
*)
-let translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
+let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
typed_rvalue =
- raise Unimplemented
+ let translate = translate_typed_value_to_rvalue ctx in
+ let value =
+ match v.value with
+ | V.Concrete cv -> RvConcrete cv
+ | Adt av -> raise Unimplemented
+ | Bottom -> failwith "Unreachable"
+ | Loan lc -> (
+ match lc with
+ | SharedLoan (_, v) -> (translate v).value
+ | MutLoan _ -> failwith "Unreachable")
+ | Borrow bc -> (
+ match bc with
+ | V.SharedBorrow _ -> raise Unimplemented
+ | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+ | V.MutBorrow (_, v) ->
+ (* Borrows are the identity in the extraction *)
+ (translate v).value)
+ | Symbolic sv ->
+ (* TODO: add sanity checks *)
+ raise Unimplemented
+ in
+ let ty = translate_fwd_ty ctx v.ty in
+ { value; ty }
let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
typed_rvalue option =
--
cgit v1.2.3