diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 16 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 41 |
2 files changed, 28 insertions, 29 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 38447fd1..eea60833 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -952,9 +952,11 @@ and end_borrows (config : C.config) (chain : borrow_or_abs_ids) (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun = fun cf -> - V.BorrowId.Set.fold - (fun id cf -> end_borrow config chain allowed_abs id cf) - lset cf + (* This is not necessary, but we prefer to reorder the borrow ids, + * so that we actually end from the smallest id to the highest id - just + * a matter of taste, and may make debugging easier *) + let ids = V.BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in + List.fold_left (fun cf id -> end_borrow config chain allowed_abs id cf) cf ids and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) : cm_fun = @@ -1035,9 +1037,11 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) and end_abstractions (config : C.config) (chain : borrow_or_abs_ids) (abs_ids : V.AbstractionId.Set.t) : cm_fun = fun cf -> - V.AbstractionId.Set.fold - (fun id cf -> end_abstraction config chain id cf) - abs_ids cf + (* This is not necessary, but we prefer to reorder the abstraction ids, + * so that we actually end from the smallest id to the highest id - just + * a matter of taste, and may make debugging easier *) + let abs_ids = V.AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in + List.fold_left (fun cf id -> end_abstraction config chain id cf) cf abs_ids and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) : cm_fun = diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index b3a0e3f2..734160f9 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -428,34 +428,29 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) fun cf ctx -> match rty with (* "Regular" ADTs *) - | T.Adt (T.AdtId def_id, regions, types) -> ( + | 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 - match + let seel = compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind def_id regions types ctx - with - | seel -> - (* Check for branching *) - assert (List.length seel <= 1 || allow_branching); - (* Apply in the context *) - let ctxl = - List.map - (fun see -> - apply_symbolic_expansion_non_borrow config original_sv see ctx) - seel - in - (* Continue *) - let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in - (* Synthesize *) - let res = S.synthesize_symbolic_expansion original_sv resl in - (* Return *) - Some res - | _ -> - failwith - "expand_symbolic_value_no_branching: the expansion lead to \ - branching") + in + (* Check for branching *) + assert (List.length seel <= 1 || allow_branching); + (* Apply in the context *) + let ctxl = + List.map + (fun see -> + apply_symbolic_expansion_non_borrow config original_sv see ctx) + seel + in + (* Continue *) + let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in + (* Synthesize *) + let res = S.synthesize_symbolic_expansion original_sv resl in + (* Return *) + Some res (* Tuples *) | T.Adt (T.Tuple, [], tys) -> (* Generate the field values *) |