diff options
Diffstat (limited to 'src/SymbolicToPure.ml')
-rw-r--r-- | src/SymbolicToPure.ml | 69 |
1 files changed, 41 insertions, 28 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index d46d8386..7fd72926 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -24,11 +24,22 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue = { value; ty } (* TODO: move *) -let mk_typed_lvalue_from_var (v : var) : typed_lvalue = - let value = LvVar (Var v) in +let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = + let value = LvVar (Var (v, mp)) in let ty = v.ty in { value; ty } +let mk_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue = + let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in + let ty = Adt (T.Tuple, tys) in + let value = LvAdt { variant_id = None; field_values = vl } in + { value; ty } + +let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id) + (vl : typed_lvalue list) : typed_lvalue = + let value = LvAdt { variant_id = Some variant_id; field_values = vl } in + { value; ty = adt_ty } + let ty_as_integer (t : ty) : T.integer_type = match t with Integer int_ty -> int_ty | _ -> failwith "Unreachable" @@ -786,7 +797,7 @@ let rec typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) : assert (variant_id = None); if field_values = [] then (ctx, None) else - let value = LvTuple field_values in + let value = LvAdt { variant_id = None; field_values } in let ty = ctx_translate_fwd_ty ctx av.ty in let lv : typed_lvalue = { value; ty } in (ctx, Some lv)) @@ -822,7 +833,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) : | 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)) + (ctx, Some (mk_typed_lvalue_from_var var None)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -844,7 +855,7 @@ and aproj_to_given_back (aproj : V.aproj) (ctx : bs_ctx) : | 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)) + (ctx, Some (mk_typed_lvalue_from_var var None)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> failwith "Unreachable" @@ -947,7 +958,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (* Translate the next expression *) let e = translate_expression e ctx in (* Put together *) - Let (Call ([ (mk_typed_lvalue_from_var dest, dest_mplace) ], 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 = @@ -1002,7 +1013,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, None, value, None), 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 @@ -1026,6 +1037,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* Retrieve the values given back by this function: those are the output * values *) let ctx, outputs = abs_to_given_back abs ctx in + let output = mk_tuple_lvalue outputs in (* Sanity check: the inputs and outputs have the proper number and the proper type *) let fun_id = match call.call_id with @@ -1057,8 +1069,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* Put everything together *) 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) + Let (Call (output, call), e) | V.SynthRet -> (* If we end the abstraction which consumed the return value of the function * we are synthesizing, we get back the borrows which were inside. Those borrows @@ -1111,9 +1122,7 @@ 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, None, mk_typed_rvalue_from_var input_var, None), - e )) + Let (Assign (given_back, mk_typed_rvalue_from_var input_var, None), e)) given_back_inputs e and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) @@ -1137,7 +1146,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) let e = translate_expression e ctx in Let ( Assign - (mk_typed_lvalue_from_var var, None, scrutinee, scrutinee_mplace), + (mk_typed_lvalue_from_var var None, scrutinee, scrutinee_mplace), e ) | SeAdt _ -> (* Should be in the [ExpandAdt] case *) @@ -1158,14 +1167,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) 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, None)) vars in - Let - ( Deconstruct - ( vars, - Some (adt_id, variant_id), - scrutinee, - scrutinee_mplace ), - branch ) + let lvars = + 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 (Assign (lv, scrutinee, scrutinee_mplace), branch) else (* This is not an enumeration: introduce let-bindings for every * field. @@ -1187,12 +1193,16 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) let field_proj = gen_field_proj fid var in Let ( Assign - (mk_typed_lvalue_from_var var, None, field_proj, None), + (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, None)) vars in - Let (Deconstruct (vars, None, scrutinee, scrutinee_mplace), branch) + let vars = + List.map (fun x -> mk_typed_lvalue_from_var x None) vars + in + Let + ( Assign (mk_tuple_lvalue vars, scrutinee, scrutinee_mplace), + branch ) | T.Assumed T.Box -> (* There should be exactly one variable *) let var = @@ -1202,8 +1212,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) * identity when extracted (`box a == a`) *) Let ( Assign - ( mk_typed_lvalue_from_var var, - None, + ( mk_typed_lvalue_from_var var None, scrutinee, scrutinee_mplace ), branch )) @@ -1214,9 +1223,13 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) (* There *must* be a variant id - otherwise there can't be several branches *) 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 -> Var x) vars in + let 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 let branch = translate_expression branch ctx in - { variant_id; vars; branch } + { pat; branch } in let branches = List.map (fun (vid, svl, e) -> translate_branch vid svl e) branches |