Fix a minor issue in expand_symbolic_value

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