summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Contexts.ml2
-rw-r--r--src/InterpreterExpansion.ml17
-rw-r--r--src/InterpreterExpressions.ml23
3 files changed, 25 insertions, 17 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 70c7a399..39c6ab91 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -49,6 +49,8 @@ module M = Modules
* independentely of each other). Still, it is always a good idea to be
* defensive.
*
+ * However, the same problem arises with logging.
+ *
* Also, a more defensive way would be to not use global references, and
* store the counters in the evaluation context. This is actually what was
* originally done, before we updated the code to use global counters because
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 1a6e198c..ce48b611 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -460,6 +460,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
let expand_symbolic_value (config : C.config) (allow_branching : bool)
(sp : V.symbolic_value) : cm_fun =
fun cf ctx ->
+ (* Debug *)
+ log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
(* Remember the initial context for printing purposes *)
let ctx0 = ctx in
(* Compute the expanded value - note that when doing so, we may introduce
@@ -471,12 +473,10 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
match rty with
(* "Regular" ADTs *)
| T.Adt (T.AdtId def_id, regions, types) ->
- (* Compute the expanded value - there should be exactly one because we
- * don't allow to expand enumerations with strictly more than one variant *)
- let expand_enumerations = false in
+ (* Compute the expanded value *)
let seel =
- compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
- def_id regions types ctx
+ compute_expanded_symbolic_adt_value allow_branching sp.sv_kind def_id
+ regions types ctx
in
(* Check for branching *)
assert (List.length seel <= 1 || allow_branching);
@@ -530,7 +530,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
comp_unit cc (fun ctx ->
log#ldebug
(lazy
- ("expand_symbolic_value_no_branching: "
+ ("expand_symbolic_value: "
^ symbolic_value_to_string ctx0 sp
^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
@@ -669,6 +669,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
*)
let greedy_expand_symbolic_values (config : C.config) : cm_fun =
fun cf ctx ->
- if config.greedy_expand_symbolics_with_borrows then
- greedy_expand_symbolics_with_borrows config cf ctx
+ if config.greedy_expand_symbolics_with_borrows then (
+ log#ldebug (lazy "greedy_expand_symbolic_values");
+ greedy_expand_symbolics_with_borrows config cf ctx)
else cf ctx
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index d3153110..808ad8c9 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -471,6 +471,8 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
*)
let eval_rvalue_discriminant (config : C.config) (p : E.place)
(cf : V.typed_value -> m_fun) : m_fun =
+ fun ctx ->
+ log#ldebug (lazy "eval_rvalue_discriminant");
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
@@ -478,18 +480,19 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
let prepare = prepare_rplace config expand_prim_copy access p in
(* Read the value *)
let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+ fun ctx ->
match v.V.value with
- | Adt _ -> eval_rvalue_discriminant_concrete config p cf
+ | Adt _ -> eval_rvalue_discriminant_concrete config p cf ctx
| Symbolic sv ->
(* Expand the symbolic value - may lead to branching *)
let allow_branching = true in
let cc = expand_symbolic_value config allow_branching sv in
(* This time the value is concrete: reevaluate *)
- comp cc (eval_rvalue_discriminant_concrete config p) cf
+ comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
| _ -> failwith "Invalid input for `discriminant`"
in
(* Compose and apply *)
- comp prepare read cf
+ comp prepare read cf ctx
let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
(cf : V.typed_value -> m_fun) : m_fun =
@@ -603,6 +606,8 @@ let eval_rvalue_aggregate (config : C.config)
*)
let eval_rvalue (config : C.config) (rvalue : E.rvalue)
(cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+ fun ctx ->
+ log#ldebug (lazy "eval_rvalue");
(* Small helpers *)
let wrap_in_result (cf : (V.typed_value, eval_error) result -> m_fun)
(v : V.typed_value) : m_fun =
@@ -611,10 +616,10 @@ let eval_rvalue (config : C.config) (rvalue : E.rvalue)
let comp_wrap f = comp f wrap_in_result cf in
(* Delegate to the proper auxiliary function *)
match rvalue with
- | E.Use op -> comp_wrap (eval_operand config op)
- | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind)
- | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf
- | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf
+ | E.Use op -> comp_wrap (eval_operand config op) ctx
+ | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
+ | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
+ | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
| E.Aggregate (aggregate_kind, ops) ->
- comp_wrap (eval_rvalue_aggregate config aggregate_kind ops)
- | E.Discriminant p -> comp_wrap (eval_rvalue_discriminant config p)
+ comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
+ | E.Discriminant p -> comp_wrap (eval_rvalue_discriminant config p) ctx