summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-20 00:53:35 +0100
committerSon Ho2022-01-20 00:53:35 +0100
commite354dd6ba08aa3b09f732b5449fafde3f91b1638 (patch)
tree08dd0c6435167b14d77b1a545211898a5fe4213d
parentcd37e6292a573f351679bc124ca007d82a2e30f5 (diff)
Make more progress on InterpreterExpressions
-rw-r--r--src/InterpreterExpressions.ml70
1 files changed, 41 insertions, 29 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index e80232c2..c74e0fd2 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -440,48 +440,60 @@ let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
(** 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 =
+ (cf : V.typed_value -> m_fun) : m_fun =
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
let expand_prim_copy = false in
- let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
- match v.V.value with
- | Adt av -> (
- match av.variant_id with
- | None ->
- failwith "Invalid input for `discriminant`: structure instead of enum"
- | Some variant_id -> (
- let id = Z.of_int (T.VariantId.to_int variant_id) in
- match mk_scalar Isize id with
- | Error _ ->
- failwith "Disciminant id out of range"
- (* Should really never happen *)
- | Ok sv ->
- (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
- )
- | _ -> failwith "Invalid input for `discriminant`"
+ let prepare = prepare_rplace config expand_prim_copy access p in
+ (* Read the value *)
+ let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+ match v.V.value with
+ | Adt av -> (
+ match av.variant_id with
+ | None ->
+ failwith
+ "Invalid input for `discriminant`: structure instead of enum"
+ | Some variant_id -> (
+ let id = Z.of_int (T.VariantId.to_int variant_id) in
+ match mk_scalar Isize id with
+ | Error _ -> failwith "Disciminant id out of range"
+ (* Should really never happen *)
+ | Ok sv ->
+ cf { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
+ | _ -> failwith "Invalid input for `discriminant`"
+ in
+ (* Compose and apply *)
+ comp prepare read cf
+
+(** Evaluate the discriminant of an ADT value.
+ Might lead to branching, if the value is symbolic.
+ *)
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;
+ (cf : V.typed_value -> m_fun) : m_fun =
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
let expand_prim_copy = false in
- let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
- match v.V.value with
- | Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ]
- | Symbolic sv ->
- (* 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 prepare = prepare_rplace config expand_prim_copy access p in
+ (* Read the value *)
+ let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+ match v.V.value with
+ | Adt _ -> eval_rvalue_discriminant_concrete config p cf
+ | Symbolic sv ->
+ (* Expand the symbolic value - may lead to branching *)
+ let allow_branching = true in
+ let cc = expand_symbolic_value config allow_branching sv in
+ (* This time the value is concrete: reevaluate *)
+ comp cc (eval_rvalue_discriminant_concrete config p) cf
+ | _ -> failwith "Invalid input for `discriminant`"
+ in
+ (* Compose and apply *)
+ comp prepare read cf
let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
(bkind : E.borrow_kind) : C.eval_ctx * V.typed_value =
- S.synthesize_eval_rvalue_ref p bkind;
match bkind with
| E.Shared | E.TwoPhaseMut ->
(* Access the value *)