summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Contexts.ml3
-rw-r--r--src/Interpreter.ml93
-rw-r--r--src/Synthesis.ml13
3 files changed, 86 insertions, 23 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 521ea0ed..4d924a9d 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -68,7 +68,8 @@ type eval_ctx = {
type_vars : type_var list;
env : env;
symbolic_counter : SymbolicValueId.generator;
- borrow_counter : BorrowId.generator;
+ (* TODO: make this global? *)
+ borrow_counter : BorrowId.generator; (* TODO: make this global? *)
}
[@@deriving show]
(** Evaluation context *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d1a34e19..2fa1bea2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2522,7 +2522,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
ctx
in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion original_sv see;
+ S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
@@ -2554,19 +2554,21 @@ let expand_symbolic_value_borrow (config : C.config)
see ctx
in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion original_sv see;
+ S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
| T.Shared ->
expand_symbolic_value_shared_borrow config original_sv ended_regions
ref_ty ctx
-(** Expand a symbolic value which is not an enumeration with several variants.
+(** Expand a symbolic value which is not an enumeration with several variants
+ (i.e., in a situation where it doesn't lead to branching).
- This function is used when exploring a path.
+ This function is used when exploring paths.
*)
-let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
- (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : C.eval_ctx =
+let expand_symbolic_value_no_branching (config : C.config)
+ (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) :
+ C.eval_ctx =
(* Compute the expanded value - note that when doing so, we may introduce
* fresh symbolic values in the context (which thus gets updated) *)
let original_sv = sp.V.svalue in
@@ -2591,7 +2593,7 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion original_sv see;
+ S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
| _ -> failwith "Unexpected")
@@ -2607,7 +2609,7 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion original_sv see;
+ S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
(* Boxes *)
@@ -2620,7 +2622,7 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
apply_symbolic_expansion_non_borrow config original_sv see ctx
in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion original_sv see;
+ S.synthesize_symbolic_expansion_no_branching original_sv see;
(* Return *)
ctx
(* Borrows *)
@@ -2636,6 +2638,45 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
(* Return *)
ctx
+(** Expand a symbolic enumeration value.
+
+ This might lead to branching.
+ *)
+let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
+ (ctx : C.eval_ctx) : C.eval_ctx list =
+ (* Compute the expanded value - note that when doing so, we may introduce
+ * fresh symbolic values in the context (which thus gets updated) *)
+ let original_sv = sp.V.svalue in
+ let rty = original_sv.V.sv_ty in
+ let ended_regions = sp.V.rset_ended in
+ match rty with
+ (* The value should be a "regular" ADTs *)
+ | T.Adt (T.AdtId def_id, regions, types) -> (
+ (* Compute the expanded value - there should be exactly one because we
+ * don't allow to expand enumerations with strictly more than one variant *)
+ let expand_enumerations = true in
+ match
+ compute_expanded_symbolic_adt_value expand_enumerations ended_regions
+ def_id regions types ctx
+ with
+ | res ->
+ (* Update the synthesized program *)
+ let seel = List.map (fun (_, x) -> x) res in
+ S.synthesize_symbolic_expansion_branching original_sv seel;
+ (* Apply in the context *)
+ let apply (ctx, see) : C.eval_ctx =
+ let ctx =
+ apply_symbolic_expansion_non_borrow config original_sv see ctx
+ in
+ (* Sanity check: the symbolic value has disappeared *)
+ assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
+ (* Return *)
+ ctx
+ in
+ List.map apply res
+ | _ -> failwith "Unexpected")
+ | _ -> failwith "Unexpected"
+
(** Update the environment to be able to read a place.
When reading a place, we may be stuck along the way because some value
@@ -2658,7 +2699,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
activate_inactivated_mut_borrow config Outer bid ctx
| FailSymbolic (pe, sp) ->
(* Expand the symbolic value *)
- expand_symbolic_value_non_enum config pe sp ctx
+ expand_symbolic_value_no_branching config pe sp ctx
| FailBottom (_, _, _) ->
(* We can't expand [Bottom] values while reading them *)
failwith "Found [Bottom] while reading a place"
@@ -2685,7 +2726,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
activate_inactivated_mut_borrow config Outer bid ctx
| FailSymbolic (pe, sp) ->
(* Expand the symbolic value *)
- expand_symbolic_value_non_enum config pe sp ctx
+ expand_symbolic_value_no_branching config pe sp ctx
| FailBottom (remaining_pes, pe, ty) ->
(* Expand the [Bottom] value *)
expand_bottom_value_from_projection config access p remaining_pes pe
@@ -3246,9 +3287,9 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
| C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
| C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
-let eval_rvalue_discriminant (config : C.config) (ctx : C.eval_ctx)
- (p : E.place) : (C.eval_ctx * V.typed_value) list =
- S.synthesize_eval_rvalue_discriminant p;
+(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *)
+let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
+ (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
@@ -3265,12 +3306,24 @@ let eval_rvalue_discriminant (config : C.config) (ctx : C.eval_ctx)
failwith "Disciminant id out of range"
(* Should really never happen *)
| Ok sv ->
- [
- (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize });
- ]))
+ (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
+ )
+ | _ -> failwith "Invalid input for `discriminant`"
+
+let eval_rvalue_discriminant (config : C.config) (p : E.place)
+ (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list =
+ S.synthesize_eval_rvalue_discriminant p;
+ (* Note that discriminant values have type `isize` *)
+ (* Access the value *)
+ let access = Read in
+ let ctx, v = prepare_rplace config access p ctx in
+ match v.V.value with
+ | Adt av -> [ eval_rvalue_discriminant_concrete config p ctx ]
| Symbolic sv ->
- (* We need to perform a symbolic expansion *)
- raise Unimplemented
+ (* Expand the symbolic value - may lead to branching *)
+ let ctxl = expand_symbolic_enum_value config sv ctx in
+ (* This time the value is concrete: reevaluate *)
+ List.map (eval_rvalue_discriminant_concrete config p) ctxl
| _ -> failwith "Invalid input for `discriminant`"
let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
@@ -3384,7 +3437,7 @@ let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
(C.eval_ctx * V.typed_value) list eval_result =
match rvalue with
- | E.Discriminant p -> Ok (eval_rvalue_discriminant config ctx p)
+ | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx)
| _ -> (
match eval_rvalue_non_discriminant config ctx rvalue with
| Error e -> Error e
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index f3cc5f91..9ce6c8da 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -26,11 +26,20 @@ open InterpreterUtils
* `s := op1 + op2`
* *)
-(** TODO: rename to synthesize_symbolic_expansion_{non_enum,one_variant}? *)
-let synthesize_symbolic_expansion (sv : V.symbolic_value)
+(** Synthesize code for a symbolic expansion which doesn't lead to branching
+ (i.e., applied on a value which is not an enumeration with several variants).
+ *)
+let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
(see : symbolic_expansion) : unit =
()
+(** Synthesize code for a symbolic expansion which leads to branching
+ (for instance when evaluating the discriminant of a symbolic value).
+ *)
+let synthesize_symbolic_expansion_branching (sv : V.symbolic_value)
+ (seel : symbolic_expansion list) : unit =
+ ()
+
let synthesize_unary_op (unop : E.unop) (op : V.typed_value)
(dest : V.symbolic_value) : unit =
()