diff options
Diffstat (limited to 'src/SymbolicToPure.ml')
| -rw-r--r-- | src/SymbolicToPure.ml | 42 |
1 files changed, 17 insertions, 25 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 87e86e69..163ddde8 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -736,7 +736,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (_, _, _) -> + | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None | AEndedIgnoredMutBorrow _ -> @@ -804,9 +804,6 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. - - TODO: - *) let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_lvalue option = @@ -878,13 +875,10 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (consumed_mv, msv, _) -> - (* We use the originally consumed value (which is stored as a meta-value) - * to help with propagating naming constraints. *) - let consumed = typed_value_to_rvalue ctx consumed_mv in + | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp (Some consumed))) + (ctx, Some (mk_typed_lvalue_from_var var mp)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -903,15 +897,10 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs); (ctx, None) - | AEndedProjBorrows { original; given_back = mv } -> - (* We use the original symbolic value to help propagate the naming constraints *) - let original = - InterpreterUtils.mk_typed_value_from_symbolic_value original - in - let original = typed_value_to_rvalue ctx original in + | AEndedProjBorrows mv -> (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp (Some original))) + (ctx, Some (mk_typed_lvalue_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> failwith "Unreachable" @@ -1050,7 +1039,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (fun (arg, mp) -> mk_value_expression arg mp) (List.combine args args_mplaces) in - let dest_v = mk_typed_lvalue_from_var dest dest_mplace None in + let dest_v = mk_typed_lvalue_from_var dest dest_mplace in let call = { func; type_params; args } in let call = Call call in let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in @@ -1115,7 +1104,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) List.fold_right (fun (var, value) (e : texpression) -> mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression value None) e) variables_values next_e @@ -1287,7 +1276,7 @@ and translate_expansion (config : config) (p : S.mplace option) let next_e = translate_expression config e ctx in let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression scrutinee scrutinee_mplace) next_e | SeAdt _ -> @@ -1311,7 +1300,7 @@ and translate_expansion (config : config) (p : S.mplace option) (* This is an enumeration: introduce an [ExpandEnum] let-binding *) let variant_id = Option.get variant_id in let lvars = - List.map (fun v -> mk_typed_lvalue_from_var v None None) vars + List.map (fun v -> mk_typed_lvalue_from_var v None) vars in let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in let monadic = false in @@ -1340,13 +1329,13 @@ and translate_expansion (config : config) (p : S.mplace option) (fun (fid, var) e -> let field_proj = gen_field_proj fid var in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression field_proj None) e) id_var_pairs branch | T.Tuple -> let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None) vars in let monadic = false in mk_let monadic @@ -1362,7 +1351,7 @@ and translate_expansion (config : config) (p : S.mplace option) * identity when extracted (`box a == a`) *) let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None None) + (mk_typed_lvalue_from_var var None) (mk_value_expression scrutinee scrutinee_mplace) branch | T.Assumed T.Vec -> @@ -1383,7 +1372,7 @@ and translate_expansion (config : config) (p : S.mplace option) let variant_id = Option.get variant_id in let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_lvalue pat_ty variant_id vars in @@ -1456,6 +1445,9 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression option) : fun_decl = + (* Reset the counters *) + reset_pure_counters (); + (* Translate *) let def = ctx.fun_decl in let bid = ctx.bid in log#ldebug @@ -1492,7 +1484,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) in let inputs = List.append ctx.forward_inputs backward_inputs in let inputs_lvs = - List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs + List.map (fun v -> mk_typed_lvalue_from_var v None) inputs in (* Sanity check *) assert ( |