diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 17 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 23 |
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 |