diff options
| -rw-r--r-- | src/Pure.ml | 13 | ||||
| -rw-r--r-- | 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 = |