diff options
| -rw-r--r-- | src/PrintPure.ml | 29 | ||||
| -rw-r--r-- | src/Pure.ml | 20 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 82 |
3 files changed, 99 insertions, 32 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml index b631f940..e5b58b9f 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -34,6 +34,9 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter = type_def_id_to_string = fmt.type_def_id_to_string; } +(* TODO: we need to store which variables we have encountered so far, and + remove [var_id_to_string]. +*) type ast_formatter = { type_var_id_to_string : TypeVarId.id -> string; type_def_id_to_string : TypeDefId.id -> string; @@ -101,8 +104,8 @@ let mk_ast_formatter (type_defs : T.type_def TypeDefId.Map.t) Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_defs in let var_id_to_string vid = - (* TODO: lookup in the context *) - VarId.to_string vid + (* TODO: somehow lookup in the context *) + "@" ^ VarId.to_string vid in let adt_field_names = Print.Contexts.type_ctx_to_adt_field_names_fun type_defs @@ -183,7 +186,12 @@ let type_def_to_string (fmt : type_formatter) (def : type_def) : string = "enum " ^ name ^ params ^ " =\n" ^ variants let var_to_string (fmt : type_formatter) (v : var) : string = - "(@" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")" + let varname = + match v.basename with + | Some name -> name ^ "^" ^ VarId.to_string v.id + | None -> "@" ^ VarId.to_string v.id + in + "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")" let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string = match v with @@ -218,6 +226,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string) "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name)) let place_to_string (fmt : ast_formatter) (p : place) : string = + (* TODO: improve that *) let var = "@" ^ fmt.var_id_to_string p.var in projection_to_string fmt var p.projection @@ -330,7 +339,7 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string) | Return v -> indent ^ "return " ^ typed_rvalue_to_string fmt v | Fail -> indent ^ "fail" | Let (lb, e) -> let_to_string fmt indent indent_incr lb e - | Switch (scrutinee, body) -> + | Switch (scrutinee, _, body) -> switch_to_string fmt indent indent_incr scrutinee body and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) @@ -339,7 +348,9 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) let val_fmt = ast_to_value_formatter fmt in match lb with | Call (lvs, call) -> - let lvs = List.map (typed_lvalue_to_string val_fmt) lvs in + let lvs = + List.map (fun (lv, _) -> typed_lvalue_to_string val_fmt lv) lvs + in let lvs = match lvs with | [] -> @@ -359,13 +370,15 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) else fun_id ^ " " ^ String.concat " " all_args in indent ^ "let " ^ lvs ^ " = " ^ call ^ " in\n" ^ e - | Assign (lv, rv) -> + | Assign (lv, _, rv, _) -> let lv = typed_lvalue_to_string val_fmt lv in let rv = typed_rvalue_to_string fmt rv in indent ^ "let " ^ lv ^ " = " ^ rv ^ " in\n" ^ e - | Deconstruct (lvs, opt_adt_id, rv) -> + | Deconstruct (lvs, opt_adt_id, rv, _) -> let rv = typed_rvalue_to_string fmt rv in - let lvs = List.map (var_or_dummy_to_string val_fmt) lvs in + let lvs = + List.map (fun (lv, _) -> var_or_dummy_to_string val_fmt lv) lvs + in let lvs = match opt_adt_id with | None -> "(" ^ String.concat ", " lvs ^ ")" diff --git a/src/Pure.ml b/src/Pure.ml index 02f6b1ba..ba0c9837 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -111,6 +111,14 @@ type projection = projection_elem list type place = { var : VarId.id; projection : projection } +type mplace = { name : string option; projection : projection } +(** "Meta" place. + + Meta-data retrieved from the symbolic execution, which gives provenance + information about the values. We use this to generate names for the variables + we introduce. + *) + type rvalue = | RvConcrete of constant_value | RvPlace of place @@ -148,15 +156,19 @@ type call = { In the extracted code, we add a unit argument. This is unit argument is added later, when going from the "pure" AST to the "extracted" AST. *) + args_mplaces : mplace option list; (** Meta data *) } type let_bindings = - | Call of typed_lvalue list * call + | Call of (typed_lvalue * mplace option) list * call (** The called function and the tuple of returned values. *) - | Assign of typed_lvalue * typed_rvalue + | Assign of typed_lvalue * mplace option * typed_rvalue * mplace option (** Variable assignment: the introduced pattern and the place we read *) | Deconstruct of - var_or_dummy list * (TypeDefId.id * VariantId.id) option * typed_rvalue + (var_or_dummy * mplace option) list + * (TypeDefId.id * VariantId.id) option + * typed_rvalue + * mplace option (** This is used in two cases. 1. When deconstructing a tuple: @@ -202,7 +214,7 @@ type expression = | Fail | Let of let_bindings * expression (** Let bindings include the let-bindings introduced because of function calls *) - | Switch of typed_rvalue * switch_body + | Switch of typed_rvalue * mplace option * switch_body and switch_body = | If of expression * expression diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 716b4e94..fb1bb029 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -768,6 +768,24 @@ let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list = log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs)); List.filter_map (typed_avalue_to_consumed ctx) abs.avalues +let translate_mprojection_elem (pe : E.projection_elem) : projection_elem option + = + match pe with + | Deref | DerefBox -> None + | Field (pkind, field_id) -> Some { pkind; field_id } + +let translate_mprojection (p : E.projection) : projection = + List.filter_map translate_mprojection_elem p + +(** Translate a "meta"-place *) +let translate_mplace (p : S.place) : mplace = + let name = p.bv.name in + let projection = translate_mprojection p.projection in + { name; projection } + +let translate_opt_mplace (p : S.place option) : mplace option = + match p with None -> None | Some p -> Some (translate_mplace p) + (** Explore an abstraction value and convert it to a given back value by collecting all the meta-values from the ended *borrows*. @@ -895,7 +913,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = | Panic -> Fail | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx - | Expansion (sv, exp) -> translate_expansion sv exp ctx + | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | Meta (_, e) -> (* We ignore the meta information *) translate_expression e ctx @@ -935,6 +953,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (* Translate the function call *) let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in let args = List.map (typed_value_to_rvalue ctx) call.args in + let args_mplaces = List.map translate_opt_mplace call.args_places in + let dest_mplace = translate_opt_mplace call.dest_place in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in (* Retrieve the function id, and register the function call in the context * if necessary. *) @@ -960,11 +980,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (ctx, Binop (binop, int_ty0)) | _ -> failwith "Unreachable") in - let call = { func; type_params; args } in + let call = { func; type_params; args; args_mplaces } in (* Translate the next expression *) let e = translate_expression e ctx in (* Put together *) - Let (Call ([ mk_typed_lvalue_from_var dest ], call), e) + Let (Call ([ (mk_typed_lvalue_from_var dest, dest_mplace) ], call), e) and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : expression = @@ -1019,7 +1039,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* Generate the assignemnts *) List.fold_right (fun (var, value) e -> - Let (Assign (mk_typed_lvalue_from_var var, value), e)) + Let (Assign (mk_typed_lvalue_from_var var, None, value, None), e)) variables_values e | V.FunCall -> let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in @@ -1072,7 +1092,9 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* Translate the next expression *) let e = translate_expression e ctx in (* Put everything together *) - let call = { func; type_params; args = inputs } in + let args_mplaces = List.map (fun _ -> None) inputs in + let call = { func; type_params; args = inputs; args_mplaces } in + let outputs = List.map (fun x -> (x, None)) outputs in Let (Call (outputs, call), e) | V.SynthRet -> (* If we end the abstraction which consumed the return value of the function @@ -1126,14 +1148,17 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* Generate the assignments *) List.fold_right (fun (given_back, input_var) e -> - Let (Assign (given_back, mk_typed_rvalue_from_var input_var), e)) + Let + ( Assign (given_back, None, mk_typed_rvalue_from_var input_var, None), + e )) given_back_inputs e -and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) - (ctx : bs_ctx) : expression = +and translate_expansion (p : S.place option) (sv : V.symbolic_value) + (exp : S.expansion) (ctx : bs_ctx) : expression = (* Translate the scrutinee *) let scrutinee_var = lookup_var_for_symbolic_value sv ctx in let scrutinee = mk_typed_rvalue_from_var scrutinee_var in + let scrutinee_mplace = translate_opt_mplace p in (* Translate the branches *) match exp with | ExpandNoBranch (sexp, e) -> ( @@ -1142,12 +1167,15 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) (* Actually, we don't *register* symbolic expansions to constant * values in the symbolic ADT *) failwith "Unreachable" - | SeMutRef (_, sv) | SeSharedRef (_, sv) -> + | SeMutRef (_, nsv) | SeSharedRef (_, nsv) -> (* The (mut/shared) borrow type is extracted to identity: we thus simply * introduce an reassignment *) - let ctx, var = fresh_var_for_symbolic_value sv ctx in + let ctx, var = fresh_var_for_symbolic_value nsv ctx in let e = translate_expression e ctx in - Let (Assign (mk_typed_lvalue_from_var var, scrutinee), e) + Let + ( Assign + (mk_typed_lvalue_from_var var, None, scrutinee, scrutinee_mplace), + e ) | SeAdt _ -> (* Should be in the [ExpandAdt] case *) failwith "Unreachable") @@ -1167,9 +1195,13 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) if is_enum then (* This is an enumeration: introduce an [ExpandEnum] let-binding *) let variant_id = Option.get variant_id in - let vars = List.map (fun x -> Var x) vars in + let vars = List.map (fun x -> (Var x, None)) vars in Let - ( Deconstruct (vars, Some (adt_id, variant_id), scrutinee), + ( Deconstruct + ( vars, + Some (adt_id, variant_id), + scrutinee, + scrutinee_mplace ), branch ) else (* This is not an enumeration: introduce let-bindings for every @@ -1190,11 +1222,14 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) List.fold_right (fun (fid, var) e -> let field_proj = gen_field_proj fid var in - Let (Assign (mk_typed_lvalue_from_var var, field_proj), e)) + Let + ( Assign + (mk_typed_lvalue_from_var var, None, field_proj, None), + e )) id_var_pairs branch | T.Tuple -> - let vars = List.map (fun x -> Var x) vars in - Let (Deconstruct (vars, None, scrutinee), branch) + let vars = List.map (fun x -> (Var x, None)) vars in + Let (Deconstruct (vars, None, scrutinee, scrutinee_mplace), branch) | T.Assumed T.Box -> (* There should be exactly one variable *) let var = @@ -1202,7 +1237,13 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) in (* We simply introduce an assignment - the box type is the * identity when extracted (`box a == a`) *) - Let (Assign (mk_typed_lvalue_from_var var, scrutinee), branch)) + Let + ( Assign + ( mk_typed_lvalue_from_var var, + None, + scrutinee, + scrutinee_mplace ), + branch )) | branches -> let translate_branch (variant_id : T.VariantId.id option) (svl : V.symbolic_value list) (branch : S.expression) : @@ -1217,13 +1258,13 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) let branches = List.map (fun (vid, svl, e) -> translate_branch vid svl e) branches in - Switch (scrutinee, Match branches)) + Switch (scrutinee, scrutinee_mplace, Match branches)) | ExpandBool (true_e, false_e) -> (* We don't need to update the context: we don't introduce any * new values/variables *) let true_e = translate_expression true_e ctx in let false_e = translate_expression false_e ctx in - Switch (scrutinee, If (true_e, false_e)) + Switch (scrutinee, scrutinee_mplace, If (true_e, false_e)) | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : scalar_value * expression = @@ -1234,7 +1275,8 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) in let branches = List.map translate_branch branches in let otherwise = translate_expression otherwise ctx in - Switch (scrutinee, SwitchInt (int_ty, branches, otherwise)) + Switch + (scrutinee, scrutinee_mplace, SwitchInt (int_ty, branches, otherwise)) let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def = let def = ctx.fun_def in |