From 0d4e85006d06c51194db17a08055c00ee830124a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 20 Apr 2022 15:59:54 +0200 Subject: Introduce mdplace to link meta information about the given back values to the information about the input arguments --- src/SymbolicToPure.ml | 45 ++++++++++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 17 deletions(-) (limited to 'src/SymbolicToPure.ml') diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index fe500480..87e86e69 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -647,7 +647,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (mk_typed_rvalue_from_var var).value in let ty = ctx_translate_fwd_ty ctx v.ty in - let value = { value; ty } in + let value : typed_rvalue = { value; ty } in (* Debugging *) log#ldebug (lazy @@ -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,6 +804,9 @@ 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 = @@ -875,10 +878,13 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (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)) + | 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 + (* 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))) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -897,10 +903,15 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs); (ctx, None) - | AEndedProjBorrows mv -> + | 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 (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp)) + (ctx, Some (mk_typed_lvalue_from_var var mp (Some original))) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> failwith "Unreachable" @@ -1039,7 +1050,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 in + let dest_v = mk_typed_lvalue_from_var dest dest_mplace None 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 @@ -1104,7 +1115,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) + (mk_typed_lvalue_from_var var None None) (mk_value_expression value None) e) variables_values next_e @@ -1276,7 +1287,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) + (mk_typed_lvalue_from_var var None None) (mk_value_expression scrutinee scrutinee_mplace) next_e | SeAdt _ -> @@ -1300,7 +1311,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) vars + List.map (fun v -> mk_typed_lvalue_from_var v None None) vars in let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in let monadic = false in @@ -1329,13 +1340,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) + (mk_typed_lvalue_from_var var None 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) vars + List.map (fun x -> mk_typed_lvalue_from_var x None None) vars in let monadic = false in mk_let monadic @@ -1351,7 +1362,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) + (mk_typed_lvalue_from_var var None None) (mk_value_expression scrutinee scrutinee_mplace) branch | T.Assumed T.Vec -> @@ -1372,7 +1383,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) vars + List.map (fun x -> mk_typed_lvalue_from_var x None None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_lvalue pat_ty variant_id vars in @@ -1481,7 +1492,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) inputs + List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs in (* Sanity check *) assert ( -- cgit v1.2.3