diff options
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
-rw-r--r-- | compiler/InterpreterExpressions.ml | 94 |
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 -> |