summaryrefslogtreecommitdiff
path: root/compiler/InterpreterExpressions.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterExpressions.ml94
1 files changed, 47 insertions, 47 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index afbf4605..51be904f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -23,7 +23,7 @@ let log = Logging.expressions_log
Note that the place should have been prepared so that there are no remaining
loans.
*)
-let expand_primitively_copyable_at_place (config : config)
+let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
(access : access_kind) (p : place) : cm_fun =
fun cf ctx ->
(* Small helper *)
@@ -36,7 +36,7 @@ let expand_primitively_copyable_at_place (config : config)
| None -> cf ctx
| Some sv ->
let cc =
- expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx))
+ expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx))
in
comp cc expand cf ctx
in
@@ -59,7 +59,7 @@ let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
(* Call the continuation *)
cf v ctx
-let access_rplace_reorganize_and_read (config : config)
+let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
(expand_prim_copy : bool) (access : access_kind) (p : place)
(cf : typed_value -> m_fun) : m_fun =
fun ctx ->
@@ -71,7 +71,7 @@ let access_rplace_reorganize_and_read (config : config)
* borrows) *)
let cc =
if expand_prim_copy then
- comp cc (expand_primitively_copyable_at_place config access p)
+ comp cc (expand_primitively_copyable_at_place meta config access p)
else cc
in
(* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -79,10 +79,10 @@ let access_rplace_reorganize_and_read (config : config)
(* Compose *)
comp cc read_place cf ctx
-let access_rplace_reorganize (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
(access : access_kind) (p : place) : cm_fun =
fun cf ctx ->
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
(fun _v -> cf)
ctx
@@ -224,7 +224,7 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
what we do in the formalization (because we don't enforce the same constraints
as MIR in the formalization).
*)
-let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
fun cf ctx ->
let prepare : cm_fun =
fun cf ctx ->
@@ -237,12 +237,12 @@ let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
let access = Read in
(* Expand the symbolic values, if necessary *)
let expand_prim_copy = true in
- access_rplace_reorganize config expand_prim_copy access p cf ctx
+ access_rplace_reorganize meta config expand_prim_copy access p cf ctx
| Move p ->
(* Access the value *)
let access = Move in
let expand_prim_copy = false in
- access_rplace_reorganize config expand_prim_copy access p cf ctx
+ access_rplace_reorganize meta config expand_prim_copy access p cf ctx
in
(* Apply *)
prepare cf ctx
@@ -358,7 +358,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
(* Compose and apply *)
comp cc move cf ctx
-let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (meta : Meta.meta) (config : config) (op : operand) (cf : typed_value -> m_fun) :
m_fun =
fun ctx ->
(* Debug *)
@@ -368,7 +368,7 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
^ eval_ctx_to_string ctx ^ "\n"));
(* We reorganize the context, then evaluate the operand *)
comp
- (prepare_eval_operand_reorganize config op)
+ (prepare_eval_operand_reorganize meta config op)
(eval_operand_no_reorganize config op)
cf ctx
@@ -376,16 +376,16 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
See [prepare_eval_operand_reorganize].
*)
-let prepare_eval_operands_reorganize (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
cm_fun =
- fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
+ fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
(** Evaluate several operands. *)
-let eval_operands (config : config) (ops : operand list)
+let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
(cf : typed_value list -> m_fun) : m_fun =
fun ctx ->
(* Prepare the operands *)
- let prepare = prepare_eval_operands_reorganize config ops in
+ let prepare = prepare_eval_operands_reorganize meta config ops in
(* Evaluate the operands *)
let eval =
fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
@@ -393,9 +393,9 @@ let eval_operands (config : config) (ops : operand list)
(* Compose and apply *)
comp prepare eval cf ctx
-let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
(cf : typed_value * typed_value -> m_fun) : m_fun =
- let eval_op = eval_operands config [ op1; op2 ] in
+ let eval_op = eval_operands meta config [ op1; op2 ] in
let use_res cf res =
match res with
| [ v1; v2 ] -> cf (v1, v2)
@@ -403,10 +403,10 @@ let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
in
comp eval_op use_res cf
-let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
(* Evaluate the operand *)
- let eval_op = eval_operand config op in
+ let eval_op = eval_operand meta config op in
(* Apply the unop *)
let apply cf (v : typed_value) : m_fun =
match (unop, v.value) with
@@ -451,11 +451,11 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
in
comp eval_op apply cf
-let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
(* Evaluate the operand *)
- let eval_op = eval_operand config op in
+ let eval_op = eval_operand meta config op in
(* Generate a fresh symbolic value to store the result *)
let apply cf (v : typed_value) : m_fun =
fun ctx ->
@@ -472,17 +472,17 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
(* Synthesize the symbolic AST *)
synthesize_unary_op ctx unop v
- (mk_opt_place_from_op op ctx)
+ (mk_opt_place_from_op meta op ctx)
res_sv None expr
in
(* Compose and apply *)
comp eval_op apply cf ctx
-let eval_unary_op (config : config) (unop : unop) (op : operand)
+let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
match config.mode with
- | ConcreteMode -> eval_unary_op_concrete config unop op cf
- | SymbolicMode -> eval_unary_op_symbolic config unop op cf
+ | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
+ | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
(** Small helper for [eval_binary_op_concrete]: computes the result of applying
the binop *after* the operands have been successfully evaluated
@@ -557,10 +557,10 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
| Ne | Eq -> raise (Failure "Unreachable"))
| _ -> raise (Failure "Invalid inputs for binop")
-let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
(* Evaluate the operands *)
- let eval_ops = eval_two_operands config op1 op2 in
+ let eval_ops = eval_two_operands meta config op1 op2 in
(* Compute the result of the binop *)
let compute cf (res : typed_value * typed_value) =
let v1, v2 = res in
@@ -569,11 +569,11 @@ let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
(* Compose and apply *)
comp eval_ops compute cf
-let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
(* Evaluate the operands *)
- let eval_ops = eval_two_operands config op1 op2 in
+ let eval_ops = eval_two_operands meta config op1 op2 in
(* Compute the result of applying the binop *)
let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
fun ctx ->
@@ -609,20 +609,20 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
let v = mk_typed_value_from_symbolic_value res_sv in
let expr = cf (Ok v) ctx in
(* Synthesize the symbolic AST *)
- let p1 = mk_opt_place_from_op op1 ctx in
- let p2 = mk_opt_place_from_op op2 ctx in
+ let p1 = mk_opt_place_from_op meta op1 ctx in
+ let p2 = mk_opt_place_from_op meta op2 ctx in
synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
in
(* Compose and apply *)
comp eval_ops compute cf ctx
-let eval_binary_op (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
match config.mode with
- | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
- | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
+ | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
+ | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
-let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
(cf : typed_value -> m_fun) : m_fun =
fun ctx ->
match bkind with
@@ -643,7 +643,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
let expand_prim_copy = false in
let prepare =
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
in
(* Evaluate the borrowing operation *)
let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -693,7 +693,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
let access = Write in
let expand_prim_copy = false in
let prepare =
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
in
(* Evaluate the borrowing operation *)
let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -714,10 +714,10 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
(* Compose and apply *)
comp prepare eval cf ctx
-let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
(ops : operand list) (cf : typed_value -> m_fun) : m_fun =
(* Evaluate the operands *)
- let eval_ops = eval_operands config ops in
+ let eval_ops = eval_operands meta config ops in
(* Compute the value *)
let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
fun ctx ->
@@ -781,7 +781,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
(* Compose and apply *)
comp eval_ops compute cf
-let eval_rvalue_not_global (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
log#ldebug (lazy "eval_rvalue");
@@ -793,12 +793,12 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
let comp_wrap f = comp f wrap_in_result cf in
(* Delegate to the proper auxiliary function *)
match rvalue with
- | Use op -> comp_wrap (eval_operand config op) ctx
- | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
- | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
- | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
+ | Use op -> comp_wrap (eval_operand meta config op) ctx
+ | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
+ | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
+ | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
| Aggregate (aggregate_kind, ops) ->
- comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
+ comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
| Discriminant _ ->
raise
(Failure
@@ -806,11 +806,11 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
the AST")
| Global _ -> raise (Failure "Unreachable")
-let eval_fake_read (config : config) (p : place) : cm_fun =
+let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
fun cf ctx ->
let expand_prim_copy = false in
let cf_prepare cf =
- access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+ access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
in
let cf_continue cf v : m_fun =
fun ctx ->
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:50:23 +0000