summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 11:39:34 +0100
committerSon Ho2022-01-05 11:39:34 +0100
commit4245b2c5df7f9da6d9374abb5613a91ef6703975 (patch)
tree0110ba161c3ff323dafba21a9101ac5f4289622b
parentd376bd5633ed8bdd51861d5bede1888d0958d73c (diff)
Make eval_rvalue return a list of values because of possible branchings and propagate the changes
-rw-r--r--src/Interpreter.ml229
1 files changed, 143 insertions, 86 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c32e7d63..d1a34e19 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3247,7 +3247,7 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
| 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 =
+ (p : E.place) : (C.eval_ctx * V.typed_value) list =
S.synthesize_eval_rvalue_discriminant p;
(* Note that discriminant values have type `isize` *)
(* Access the value *)
@@ -3265,8 +3265,9 @@ 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 });
+ ]))
| Symbolic sv ->
(* We need to perform a symbolic expansion *)
raise Unimplemented
@@ -3355,19 +3356,39 @@ let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
let aty = T.Adt (T.AdtId def_id, regions, types) in
(ctx, { V.value = Adt av; ty = aty })
-(** Evaluate an rvalue in a given context: return the updated context and
- the computed value
-*)
-let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
- (C.eval_ctx * V.typed_value) eval_result =
+(** Evaluate an rvalue which is not a discriminant.
+
+ We define a function for this specific case, because evaluating
+ a discriminant might lead to branching (if we evaluate the discriminant
+ of a symbolic enumeration value), while it is not the case for the
+ other rvalues.
+ *)
+let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
+ (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result =
match rvalue with
| E.Use op -> Ok (eval_operand config ctx op)
| E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind)
| E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op
| E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
- | E.Discriminant p -> Ok (eval_rvalue_discriminant config ctx p)
| E.Aggregate (aggregate_kind, ops) ->
Ok (eval_rvalue_aggregate config ctx aggregate_kind ops)
+ | E.Discriminant _ -> failwith "Unreachable"
+
+(** Evaluate an rvalue in a given context: return the updated context and
+ the computed value.
+
+ Returns a list of pairs (new context, computed rvalue) because
+ `discriminant` might lead to a branching in case it is applied
+ on a symbolic enumeration value.
+*)
+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)
+ | _ -> (
+ match eval_rvalue_non_discriminant config ctx rvalue with
+ | Error e -> Error e
+ | Ok res -> Ok [ res ])
(** Result of evaluating a statement *)
type statement_eval_res = Unit | Break of int | Continue of int | Return
@@ -3428,8 +3449,7 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
For instance, something like: `Cons Bottom Bottom`.
*)
let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
- (variant_id : T.VariantId.id) :
- (C.eval_ctx * statement_eval_res) eval_result =
+ (variant_id : T.VariantId.id) : C.eval_ctx * statement_eval_res =
S.synthesize_set_discriminant p variant_id;
(* Access the value *)
let access = Write in
@@ -3449,7 +3469,7 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
| None -> failwith "Found a struct value while expected an enum"
| Some variant_id' ->
if variant_id' = variant_id then (* Nothing to do *)
- Ok (ctx, Unit)
+ (ctx, Unit)
else
(* Replace the value *)
let bottom_v =
@@ -3457,14 +3477,14 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
def_id (Some variant_id) regions types
in
let ctx = write_place_unwrap config access p bottom_v ctx in
- Ok (ctx, Unit))
+ (ctx, Unit))
| T.Adt (T.AdtId def_id, regions, types), V.Bottom ->
let bottom_v =
compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
(Some variant_id) regions types
in
let ctx = write_place_unwrap config access p bottom_v ctx in
- Ok (ctx, Unit)
+ (ctx, Unit)
| _, V.Symbolic _ ->
assert (config.mode = SymbolicMode);
(* TODO *) raise Unimplemented
@@ -3622,7 +3642,8 @@ let eval_box_deref_mut_or_shared (config : C.config)
in
let borrow_kind = if is_mut then E.Mut else E.Shared in
let rv = E.Ref (p, borrow_kind) in
- match eval_rvalue config ctx rv with
+ (* Note that the rvalue can't be a discriminant value *)
+ match eval_rvalue_non_discriminant config ctx rv with
| Error err -> Error err
| Ok (ctx, borrowed_value) ->
(* Move the borrowed value to its destination *)
@@ -3770,7 +3791,7 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
(** 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 =
+ : (C.eval_ctx * statement_eval_res) eval_result list =
(* Debugging *)
L.log#ldebug
(lazy
@@ -3783,42 +3804,52 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
| A.Assign (p, rvalue) -> (
(* Evaluate the rvalue *)
match eval_rvalue config ctx rvalue with
- | Error err -> Error err
- | Ok (ctx, rvalue) ->
+ | Error err -> [ Error err ]
+ | Ok res ->
(* Assign *)
- let ctx = assign_to_place config ctx rvalue p in
- Ok (ctx, Unit))
+ let assign (ctx, rvalue) =
+ let ctx = assign_to_place config ctx rvalue p in
+ Ok (ctx, Unit)
+ in
+ List.map assign res)
| A.FakeRead p ->
let ctx, _ = prepare_rplace config Read p ctx in
- Ok (ctx, Unit)
+ [ Ok (ctx, Unit) ]
| A.SetDiscriminant (p, variant_id) ->
- set_discriminant config ctx p variant_id
- | A.Drop p -> Ok (drop_value config ctx p, Unit)
+ [ Ok (set_discriminant config ctx p variant_id) ]
+ | A.Drop p -> [ Ok (drop_value config ctx p, Unit) ]
| A.Assert assertion -> (
let ctx, v = eval_operand config ctx assertion.cond in
assert (v.ty = T.Bool);
match v.value with
| Concrete (Bool b) ->
- if b = assertion.expected then Ok (ctx, Unit) else Error Panic
+ if b = assertion.expected then [ Ok (ctx, Unit) ] else [ Error Panic ]
| _ -> failwith "Expected a boolean")
| A.Call call -> eval_function_call config ctx call
- | A.Panic -> Error Panic
- | A.Return -> Ok (ctx, Return)
- | A.Break i -> Ok (ctx, Break i)
- | A.Continue i -> Ok (ctx, Continue i)
- | A.Nop -> Ok (ctx, Unit)
- | A.Sequence (st1, st2) -> (
+ | A.Panic -> [ Error Panic ]
+ | A.Return -> [ Ok (ctx, Return) ]
+ | A.Break i -> [ Ok (ctx, Break i) ]
+ | A.Continue i -> [ Ok (ctx, Continue i) ]
+ | A.Nop -> [ Ok (ctx, Unit) ]
+ | A.Sequence (st1, st2) ->
(* Evaluate the first statement *)
- match eval_statement config ctx st1 with
- | Error err -> Error err
- | Ok (ctx, Unit) ->
- (* Evaluate the second statement *)
- eval_statement config ctx st2
- (* Control-flow break: transmit. We enumerate the cases on purpose *)
- | Ok (ctx, Break i) -> Ok (ctx, Break i)
- | Ok (ctx, Continue i) -> Ok (ctx, Continue i)
- | Ok (ctx, Return) -> Ok (ctx, Return))
+ let res1 = eval_statement config ctx st1 in
+ (* Evaluate the sequence *)
+ let eval_seq res1 =
+ match res1 with
+ | Error err -> [ Error err ]
+ | Ok (ctx, Unit) ->
+ (* Evaluate the second statement *)
+ eval_statement config ctx st2
+ (* Control-flow break: transmit. We enumerate the cases on purpose *)
+ | Ok (ctx, Break i) -> [ Ok (ctx, Break i) ]
+ | Ok (ctx, Continue i) -> [ Ok (ctx, Continue i) ]
+ | Ok (ctx, Return) -> [ Ok (ctx, Return) ]
+ in
+ List.concat (List.map eval_seq res1)
| A.Loop loop_body ->
+ (* For now, we don't support loops in symbolic mode *)
+ assert (config.C.mode = C.ConcreteMode);
(* Evaluate a loop body
We need a specific function for the [Continue] case: in case we continue,
@@ -3826,28 +3857,34 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
(and repeat this an indefinite number of times).
*)
let rec eval_loop_body (ctx : C.eval_ctx) :
- (C.eval_ctx * statement_eval_res) eval_result =
+ (C.eval_ctx * statement_eval_res) eval_result list =
(* Evaluate the loop body *)
- match eval_statement config ctx loop_body with
- | Error err -> Error err
- | Ok (ctx, Unit) ->
- (* We finished evaluating the statement in a "normal" manner *)
- Ok (ctx, Unit)
- (* Control-flow breaks *)
- | Ok (ctx, Break i) ->
- (* Decrease the break index *)
- if i = 0 then Ok (ctx, Unit) else Ok (ctx, Break (i - 1))
- | Ok (ctx, Continue i) ->
- (* Decrease the continue index *)
- if i = 0 then
- (* We stop there. When we continue, we go back to the beginning
- of the loop: we must thus reevaluate the loop body (and
- recheck the result to know whether we must reevaluate again,
- etc. *)
- eval_loop_body ctx
- else (* We don't stop there: transmit *)
- Ok (ctx, Continue (i - 1))
- | Ok (ctx, Return) -> Ok (ctx, Return)
+ let body_res = eval_statement config ctx loop_body in
+ (* Evaluate the next steps *)
+ let eval res =
+ match res with
+ | Error err -> [ Error err ]
+ | Ok (ctx, Unit) ->
+ (* We finished evaluating the statement in a "normal" manner *)
+ [ Ok (ctx, Unit) ]
+ (* Control-flow breaks *)
+ | Ok (ctx, Break i) ->
+ (* Decrease the break index *)
+ if i = 0 then [ Ok (ctx, Unit) ] else [ Ok (ctx, Break (i - 1)) ]
+ | Ok (ctx, Continue i) ->
+ (* Decrease the continue index *)
+ if i = 0 then
+ (* We stop there. When we continue, we go back to the beginning
+ of the loop: we must thus reevaluate the loop body (and
+ recheck the result to know whether we must reevaluate again,
+ etc. *)
+ eval_loop_body ctx
+ else
+ (* We don't stop there: transmit *)
+ [ Ok (ctx, Continue (i - 1)) ]
+ | Ok (ctx, Return) -> [ Ok (ctx, Return) ]
+ in
+ List.concat (List.map eval body_res)
in
(* Apply *)
eval_loop_body ctx
@@ -3860,6 +3897,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
| 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
@@ -3868,11 +3906,12 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
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"))
(** Evaluate a function call (auxiliary helper for [eval_statement]) *)
and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :
- (C.eval_ctx * statement_eval_res) eval_result =
+ (C.eval_ctx * statement_eval_res) eval_result list =
(* There are two cases *
- this is a local function, in which case we execute its body
- this is a non-local function, in which case there is a special treatment
@@ -3883,22 +3922,27 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :
eval_local_function_call config ctx fid call.region_params
call.type_params call.args call.dest
| A.Assumed fid ->
- eval_non_local_function_call config ctx fid call.region_params
- call.type_params call.args call.dest
+ [
+ eval_non_local_function_call config ctx fid call.region_params
+ call.type_params call.args call.dest;
+ ]
in
- match res with Error err -> Error err | Ok ctx -> Ok (ctx, Unit)
+ List.map
+ (fun res ->
+ match res with Error err -> Error err | Ok ctx -> Ok (ctx, Unit))
+ res
(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
[eval_statement]) *)
and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
(fid : A.FunDefId.id) (region_params : T.erased_region list)
(type_params : T.ety list) (args : E.operand list) (dest : E.place) :
- C.eval_ctx eval_result =
+ C.eval_ctx eval_result list =
S.synthesize_local_function_call fid region_params type_params args dest;
(* Retrieve the (correctly instantiated) body *)
let def = C.ctx_lookup_fun_def ctx fid in
match config.mode with
- | ConcreteMode -> (
+ | ConcreteMode ->
let tsubst =
Subst.make_type_subst
(List.map (fun v -> v.T.index) def.A.signature.type_params)
@@ -3935,31 +3979,41 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
let ctx = C.ctx_push_uninitialized_vars ctx locals in
(* Execute the function body *)
- match eval_function_body config ctx body with
- | Error Panic -> Error Panic
- | Ok ctx ->
- (* Pop the stack frame and retrieve the return value *)
- let ctx, ret_value = ctx_pop_frame config ctx in
+ let res = eval_function_body config ctx body in
- (* Move the return value to its destination *)
- let ctx = assign_to_place config ctx ret_value dest in
+ (* Pop the stack frame and move the return value to its destination *)
+ let finish res =
+ match res with
+ | Error Panic -> Error Panic
+ | Ok ctx ->
+ (* Pop the stack frame and retrieve the return value *)
+ let ctx, ret_value = ctx_pop_frame config ctx in
- (* Return *)
- Ok ctx)
+ (* Move the return value to its destination *)
+ let ctx = assign_to_place config ctx ret_value dest in
+
+ (* Return *)
+ Ok ctx
+ in
+ List.map finish res
| SymbolicMode -> raise Unimplemented
(** Evaluate a statement seen as a function body (auxiliary helper for
[eval_statement]) *)
and eval_function_body (config : C.config) (ctx : C.eval_ctx)
- (body : A.statement) : (C.eval_ctx, eval_error) result =
- match eval_statement config ctx body with
- | Error err -> Error err
- | Ok (ctx, res) -> (
- (* Sanity check *)
- if config.C.check_invariants then Inv.check_invariants ctx;
- match res with
- | Unit | Break _ | Continue _ -> failwith "Inconsistent state"
- | Return -> Ok ctx)
+ (body : A.statement) : (C.eval_ctx, eval_error) result list =
+ let res = eval_statement config ctx body in
+ let finish res =
+ match res with
+ | Error err -> Error err
+ | Ok (ctx, res) -> (
+ (* Sanity check *)
+ if config.C.check_invariants then Inv.check_invariants ctx;
+ match res with
+ | Unit | Break _ | Continue _ -> failwith "Inconsistent state"
+ | Return -> Ok ctx)
+ in
+ List.map finish res
module Test = struct
(** Test a unit function (taking no arguments) by evaluating it in an empty
@@ -3997,8 +4051,11 @@ module Test = struct
(* Evaluate the function *)
let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in
match eval_function_body config ctx fdef.A.body with
- | Error err -> Error err
- | Ok _ -> Ok ()
+ | [ Ok _ ] -> Ok ()
+ | [ Error err ] -> Error err
+ | _ ->
+ (* We execute the concrete interpreter: there shouldn't be any branching *)
+ failwith "Unreachable"
(** Small helper: return true if the function is a unit function (no parameters,
no arguments) - TODO: move *)