summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml94
1 files changed, 75 insertions, 19 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3d3d7129..5bcd4cac 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3080,6 +3080,26 @@ let prepare_rplace (config : C.config) (access : access_kind) (p : E.place)
let v = read_place_unwrap config access p ctx in
(ctx, v)
+(** Prepare the evaluation of an operand. *)
+let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
+ : C.eval_ctx * V.typed_value =
+ let ctx, v =
+ match op with
+ | Expressions.Constant (ty, cv) ->
+ let v = constant_value_to_typed_value ctx ty cv in
+ (ctx, v)
+ | Expressions.Copy p ->
+ (* Access the value *)
+ let access = Read in
+ prepare_rplace config access p ctx
+ | Expressions.Move p ->
+ (* Access the value *)
+ let access = Move in
+ prepare_rplace config access p ctx
+ in
+ assert (not (bottom_in_value v));
+ (ctx, v)
+
(** Evaluate an operand. *)
let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
C.eval_ctx * V.typed_value =
@@ -3847,6 +3867,15 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
(* Return *)
Ok ctx)
+(** Expand a symbolic value over which we perform a switch *)
+let expand_symbolic_switch_scrutinee (config : C.config) (ctx : C.eval_ctx)
+ (sv : V.symbolic_proj_comp) (tgts : A.switch_targets) : C.eval_ctx list =
+ (* (* Expand, depending on the switch kind *)
+ match tgts with
+ | A.If (_, _) ->
+ | A.SwitchInt (int_ty, tgts, otherwise) ->*)
+ raise Unimplemented
+
(** Evaluate a statement *)
let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
: (C.eval_ctx * statement_eval_res) eval_result list =
@@ -3947,25 +3976,52 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
(* Apply *)
eval_loop_body ctx
| A.Switch (op, tgts) -> (
- (* Evaluate the operand *)
- let ctx, op_v = eval_operand config ctx op in
- match tgts with
- | A.If (st1, st2) -> (
- match op_v.value with
- | V.Concrete (V.Bool b) ->
- if b then eval_statement config ctx st1
- else eval_statement config ctx st2
- | V.Symbolic _ -> raise Unimplemented
- | _ -> failwith "Inconsistent state")
- | A.SwitchInt (int_ty, tgts, otherwise) -> (
- match op_v.value with
- | V.Concrete (V.Scalar sv) -> (
- assert (sv.V.int_ty = int_ty);
- match List.find_opt (fun (sv', _) -> sv = sv') tgts with
- | None -> eval_statement config ctx otherwise
- | Some (_, tgt) -> eval_statement config ctx tgt)
- | V.Symbolic _ -> raise Unimplemented
- | _ -> failwith "Inconsistent state"))
+ (* We evaluate the operand in two steps:
+ * first we prepare it, then we check if its value is concrete or
+ * symbolic. If it is concrete, we can then evaluate the operand
+ * directly, otherwise we must first expand the value.
+ * Note that we can't fully evaluate the operand *then* expand the
+ * value if it is symbolic, because the value may have been move
+ * (and thus floating in thin air...)!
+ * *)
+ (* Prepare the operand *)
+ let ctx, op_v = eval_operand_prepare config ctx op in
+ (* Check if the operand is concrete or symbolic, expand it if necessary *)
+ match op_v.V.value with
+ | V.Symbolic sv ->
+ (* Expand the symbolic value *)
+ let ctxl = expand_symbolic_switch_scrutinee config ctx sv tgts in
+ (* The value under scrutinee is now concrete: we can evaluate the switch *)
+ List.concat (List.map (eval_switch_concrete config op tgts) ctxl)
+ | _ ->
+ (* Concrete *)
+ eval_switch_concrete config op tgts ctx)
+
+(** Evaluate a switch *over* a concrete value.
+
+ The caller must make sure to expand the value under scrutinee *before*
+ calling this function, if the value is symbolic.
+*)
+and eval_switch_concrete (config : C.config) (op : E.operand)
+ (tgts : A.switch_targets) (ctx : C.eval_ctx) :
+ (C.eval_ctx * statement_eval_res) eval_result list =
+ (* Evaluate the operand *)
+ let ctx, op_v = eval_operand config ctx op in
+ match tgts with
+ | A.If (st1, st2) -> (
+ match op_v.value with
+ | V.Concrete (V.Bool b) ->
+ if b then eval_statement config ctx st1
+ else eval_statement config ctx st2
+ | _ -> failwith "Inconsistent state")
+ | A.SwitchInt (int_ty, tgts, otherwise) -> (
+ match op_v.value with
+ | V.Concrete (V.Scalar sv) -> (
+ assert (sv.V.int_ty = int_ty);
+ match List.find_opt (fun (sv', _) -> sv = sv') tgts with
+ | None -> eval_statement config ctx otherwise
+ | Some (_, tgt) -> eval_statement config ctx tgt)
+ | _ -> failwith "Inconsistent state")
(** Evaluate a function call (auxiliary helper for [eval_statement]) *)
and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :