From 9564ad271a9d69ca58333ec33c778f3255ca1632 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 15 Jan 2022 21:31:57 +0100
Subject: Add sv_kind ("symbolic value kind") to track the origin of the
symbolic values
---
src/Interpreter.ml | 4 +++-
src/InterpreterBorrows.ml | 8 ++++----
src/InterpreterExpansion.ml | 35 ++++++++++++++++++-----------------
src/InterpreterExpressions.ml | 8 ++++++--
src/InterpreterStatements.ml | 2 +-
src/InterpreterUtils.ml | 10 ++++++----
src/Values.ml | 28 +++++++++++++++++++++++++++-
7 files changed, 65 insertions(+), 30 deletions(-)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2f0f52af..8cab8c47 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -67,7 +67,9 @@ module Test = struct
let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
(* Create fresh symbolic values for the inputs *)
let input_svs =
- List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
+ List.map
+ (fun ty -> mk_fresh_symbolic_value V.SynthInput ty)
+ inst_sg.inputs
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
let empty_absl =
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index faa63c0a..9d332543 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -746,8 +746,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
be expanded (because expanding this symbolic value would require expanding
a reference whose region has already ended).
*)
-let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value =
- mk_fresh_symbolic_typed_value av.V.ty
+let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value =
+ mk_fresh_symbolic_typed_value V.FunCallGivenBack av.V.ty
(** End a borrow identified by its borrow id in a context
@@ -1129,7 +1129,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
match bc with
| V.AMutBorrow (bid, av) ->
(* First, convert the avalue to a (fresh symbolic) value *)
- let v = convert_avalue_to_value av in
+ let v = convert_avalue_to_given_back_value av in
give_back_value config bid v ctx
| V.ASharedBorrow bid -> give_back_shared config bid ctx
| V.AProjSharedBorrow _ ->
@@ -1148,7 +1148,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
V.AEndedProjBorrows ctx
in
(* Give back a fresh symbolic value *)
- let nsv = mk_fresh_symbolic_value proj_ty in
+ let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
let ctx =
give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
in
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 8f560083..8b039510 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -217,8 +217,9 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
doesn't allow the expansion of enumerations *containing several variants*.
*)
let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
- (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list)
- (types : T.rty list) (ctx : C.eval_ctx) : symbolic_expansion list =
+ (kind : V.sv_kind) (def_id : T.TypeDefId.id)
+ (regions : T.RegionId.id T.region list) (types : T.rty list)
+ (ctx : C.eval_ctx) : symbolic_expansion list =
(* Lookup the definition and check if it is an enumeration with several
* variants *)
let def = C.ctx_lookup_type_def ctx def_id in
@@ -235,7 +236,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
((variant_id, field_types) : T.VariantId.id option * T.rty list) :
symbolic_expansion =
let field_values =
- List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value ty) field_types
+ List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types
in
let see = SeAdt (variant_id, field_values) in
see
@@ -243,20 +244,20 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
(* Initialize all the expanded values of all the variants *)
List.map initialize variants_fields_types
-let compute_expanded_symbolic_tuple_value (field_types : T.rty list) :
- symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
+ (field_types : T.rty list) : symbolic_expansion =
(* Generate the field values *)
let field_values =
- List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
+ List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
in
let variant_id = None in
let see = SeAdt (variant_id, field_values) in
see
-let compute_expanded_symbolic_box_value (boxed_ty : T.rty) : symbolic_expansion
- =
+let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
+ symbolic_expansion =
(* Introduce a fresh symbolic value *)
- let boxed_value = mk_fresh_symbolic_value boxed_ty in
+ let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
let see = SeAdt (None, [ boxed_value ]) in
see
@@ -360,7 +361,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
(* Finally, replace the projectors on loans *)
let bids = !borrows in
assert (not (V.BorrowId.Set.is_empty bids));
- let shared_sv = mk_fresh_symbolic_value ref_ty in
+ let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
let see = SeSharedRef (bids, shared_sv) in
let allow_reborrows = true in
let ctx =
@@ -382,7 +383,7 @@ let expand_symbolic_value_borrow (config : C.config)
| T.Mut ->
(* Simple case: simply create a fresh symbolic value and a fresh
* borrow id *)
- let sv = mk_fresh_symbolic_value ref_ty in
+ let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
let bid = C.fresh_borrow_id () in
let see = SeMutRef (bid, sv) in
(* Expand the symbolic values - we simply perform a substitution (and
@@ -424,8 +425,8 @@ let expand_symbolic_value_no_branching (config : C.config)
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = false in
match
- compute_expanded_symbolic_adt_value expand_enumerations def_id regions
- types ctx
+ compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
+ def_id regions types ctx
with
| [ see ] ->
(* Apply in the context *)
@@ -443,7 +444,7 @@ let expand_symbolic_value_no_branching (config : C.config)
(* Tuples *)
| T.Adt (T.Tuple, [], tys) ->
(* Generate the field values *)
- let see = compute_expanded_symbolic_tuple_value tys in
+ let see = compute_expanded_symbolic_tuple_value sp.sv_kind tys in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -454,7 +455,7 @@ let expand_symbolic_value_no_branching (config : C.config)
ctx
(* Boxes *)
| T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
- let see = compute_expanded_symbolic_box_value boxed_ty in
+ let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -500,8 +501,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = true in
let seel =
- compute_expanded_symbolic_adt_value expand_enumerations def_id regions
- types ctx
+ compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
+ def_id regions types ctx
in
(* Update the synthesized program *)
S.synthesize_symbolic_expansion_enum_branching original_sv seel;
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f577a190..2390aa48 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -242,7 +242,9 @@ let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
| E.Neg, T.Integer int_ty -> T.Integer int_ty
| _ -> failwith "Invalid input for unop"
in
- let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+ let res_sv =
+ { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+ in
(* Synthesize *)
S.synthesize_unary_op unop v res_sv;
(* Return *)
@@ -360,7 +362,9 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
| E.Ne | E.Eq -> failwith "Unreachable")
| _ -> failwith "Invalid inputs for binop"
in
- let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+ let res_sv =
+ { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+ in
(* Synthesize *)
S.synthesize_binary_op binop v1 v2 res_sv;
(* Return *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 8b29bac9..e92b1c0b 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -885,7 +885,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(args : E.operand list) (dest : E.place) : C.eval_ctx =
(* Generate a fresh symbolic value for the return value *)
let ret_sv_ty = inst_sg.A.output in
- let ret_spc = mk_fresh_symbolic_value ret_sv_ty in
+ let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
let ret_value = mk_typed_value_from_symbolic_value ret_spc in
let ret_av regions =
mk_aproj_loans_value_from_symbolic_value regions ret_spc
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 971dc801..e00e7dcf 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -53,16 +53,18 @@ let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
{ var_id; projection = [] }
(** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value =
+let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.rty) :
+ V.symbolic_value =
let sv_id = C.fresh_symbolic_value_id () in
- let svalue = { V.sv_id; V.sv_ty = ty } in
+ let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in
svalue
(** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (rty : T.rty) : V.typed_value =
+let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) :
+ V.typed_value =
let ty = Subst.erase_regions rty in
(* Generate the fresh a symbolic value *)
- let value = mk_fresh_symbolic_value rty in
+ let value = mk_fresh_symbolic_value sv_kind rty in
let value = V.Symbolic value in
{ V.value; V.ty }
diff --git a/src/Values.ml b/src/Values.ml
index 59cfbdca..856ccb6f 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -45,7 +45,33 @@ type constant_value =
| String of string
[@@deriving show]
-type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
+(** The kind of a symbolic value, which precises how the value was generated *)
+type sv_kind =
+ | FunCallRet (** The value is the return value of a function call *)
+ | FunCallGivenBack
+ (** The value is a borrowed value given back by an abstraction
+ (happens when giving a borrow to a function: when the abstraction
+ introduced to model the function call ends we reintroduce a symbolic
+ value in the context for the value modified by the abstraction through
+ the borrow).
+ *)
+ | SynthInput
+ (** The value is an input value of the function whose body we are
+ currently synthesizing.
+ *)
+ | SynthGivenBack
+ (** The value is a borrowed value that the function whose body we are
+ synthesizing returned, and which was given back because we ended
+ one of the lifetimes of this function (we do this to synthesize
+ the backward functions).
+ *)
+[@@deriving show]
+
+type symbolic_value = {
+ sv_kind : sv_kind;
+ sv_id : SymbolicValueId.id;
+ sv_ty : rty;
+}
[@@deriving show]
(** A symbolic value *)
--
cgit v1.2.3