diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 27 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 11 |
2 files changed, 34 insertions, 4 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index cd433890..407f01bb 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -16,6 +16,33 @@ module M = Modules * different contexts * - also, it is a lot more convenient to not store those counters in contexts * objects + * + * ============= + * **WARNNING**: + * ============= + * Pay attention when playing with the function type abbreviations, + * as they may make you not always generate fresh identifiers. For + * instance, consider the following: + * ``` + * type fun_type = unit -> ... + * fn f x : fun_type = + * let id = fresh_id () in + * ... + * + * let g = f x in // <-- the fresh identifier gets generated here + * let x1 = g () in // <-- no fresh generation here + * let x2 = g () in + * ... + * ``` + * + * This is one, in such cases, we often introduce all the inputs, even + * when they are not used (which happens!). + * ``` + * fn f x : fun_type = + * fun .. -> + * let id = fresh_id () in + * ... + * ``` *) let symbolic_value_id_counter, fresh_symbolic_value_id = diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 80b06143..d3153110 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -271,6 +271,7 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand) let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + fun ctx -> (* Evaluate the operand *) let eval_op = eval_operand config op in (* Generate a fresh symbolic value to store the result *) @@ -291,7 +292,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) cf (Ok (mk_typed_value_from_symbolic_value res_sv)) in (* Compose and apply *) - comp eval_op apply cf + comp eval_op apply cf ctx let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = @@ -387,6 +388,7 @@ let eval_binary_op_concrete (config : C.config) (binop : E.binop) let eval_binary_op_symbolic (config : C.config) (binop : E.binop) (op1 : E.operand) (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun = + fun ctx -> (* Evaluate the operands *) let eval_ops = eval_two_operands config op1 op2 in (* Compute the result of applying the binop *) @@ -426,7 +428,7 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop) cf (Ok v) in (* Compose and apply *) - comp eval_ops compute cf + comp eval_ops compute cf ctx let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand) (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun @@ -491,6 +493,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place) let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> match bkind with | E.Shared | E.TwoPhaseMut -> (* Access the value *) @@ -531,7 +534,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) cf rv ctx in (* Compose and apply *) - comp prepare eval cf + comp prepare eval cf ctx | E.Mut -> (* Access the value *) let access = Write in @@ -554,7 +557,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) cf rv ctx in (* Compose and apply *) - comp prepare eval cf + comp prepare eval cf ctx let eval_rvalue_aggregate (config : C.config) (aggregate_kind : E.aggregate_kind) (ops : E.operand list) |