From 3c906b905e3ba957d193c168a6c84ece06136a1e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Feb 2022 10:22:35 +0100 Subject: Merge the switches over integers and the matches over enumerations in the pure AST --- src/ExtractToFStar.ml | 53 +++----------------------------------------------- src/PrintPure.ml | 15 +------------- src/Pure.ml | 14 ++++++------- src/PureMicroPasses.ml | 19 ------------------ src/PureUtils.ml | 11 +++++++++++ src/SymbolicToPure.ml | 21 +++++++++++++------- 6 files changed, 36 insertions(+), 97 deletions(-) diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 8746b8af..919a5b05 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -665,6 +665,9 @@ let extract_adt_g_value let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (v : typed_lvalue) : extraction_ctx = match v.value with + | LvConcrete cv -> + ctx.fmt.extract_constant_value fmt inside cv; + ctx | LvVar (Var (v, _)) -> let vname = ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty @@ -832,56 +835,6 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) extract_branch false e_else; (* Close the box for the whole `if ... then ... else ...` *) F.pp_close_box fmt () - | SwitchInt (_, branches, otherwise) -> - (* Open a box for the whole match *) - F.pp_open_hvbox fmt 0; - (* Open a box for the `match ... with` *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the `match ... with` *) - F.pp_print_string fmt "begin match"; - F.pp_print_space fmt (); - extract_texpression ctx fmt false scrut; - F.pp_print_space fmt (); - F.pp_print_string fmt "with"; - (* Close the box for the `match ... with` *) - F.pp_close_box fmt (); - - (* Extract the branches *) - let extract_branch (sv : scalar_value option) (e_branch : texpression) - : unit = - F.pp_print_space fmt (); - (* Open a box for the pattern+branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "|"; - (* Print the pattern *) - F.pp_print_space fmt (); - (match sv with - | Some sv -> ctx.fmt.extract_constant_value fmt false (V.Scalar sv) - | None -> F.pp_print_string fmt "_"); - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - F.pp_print_space fmt (); - (* Open a box for the branch *) - F.pp_open_hvbox fmt 0; - (* Print the branch itself *) - extract_texpression ctx fmt false e_branch; - (* Close the box for the branch *) - F.pp_close_box fmt (); - (* Close the box for the pattern+branch *) - F.pp_close_box fmt () - in - - let all_branches = - List.map (fun (sv, br) -> (Some sv, br)) branches - in - let all_branches = List.append all_branches [ (None, otherwise) ] in - List.iter (fun (sv, br) -> extract_branch sv br) all_branches; - - (* End the match *) - F.pp_print_space fmt (); - F.pp_print_string fmt "end"; - (* Close the box for the whole match *) - F.pp_close_box fmt () | Match branches -> (* Open a box for the whole match *) F.pp_open_hvbox fmt 0; diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 0325e60c..81ebcc7e 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -267,6 +267,7 @@ let adt_g_value_to_string (fmt : value_formatter) let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) : string = match v.value with + | LvConcrete cv -> Print.Values.constant_value_to_string cv | LvVar var -> var_or_dummy_to_string fmt var | LvAdt av -> adt_g_value_to_string fmt @@ -415,20 +416,6 @@ and switch_to_string (fmt : ast_formatter) (indent : string) let e_false = texpression_to_string fmt indent1 indent_incr e_false in "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent ^ "else\n" ^ indent ^ e_false - | SwitchInt (_, branches, otherwise) -> - let branches = - List.map - (fun (v, be) -> - indent ^ "| " ^ scalar_value_to_string v ^ " ->\n" ^ indent1 - ^ texpression_to_string fmt indent1 indent_incr be) - branches - in - let otherwise = - indent ^ "| _ ->\n" ^ indent1 - ^ texpression_to_string fmt indent1 indent_incr otherwise - in - let all_branches = List.append branches [ otherwise ] in - "switch " ^ scrut ^ " with\n" ^ String.concat "\n" all_branches | Match branches -> let val_fmt = ast_to_value_formatter fmt in let branch_to_string (b : match_branch) : string = diff --git a/src/Pure.ml b/src/Pure.ml index 428246dd..c773d613 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -264,7 +264,12 @@ type var_or_dummy = }] (** A left value (which appears on the left of assignments *) -type lvalue = LvVar of var_or_dummy | LvAdt of adt_lvalue +type lvalue = + | LvConcrete of constant_value + (** [LvConcrete] is necessary because we merge the switches over integer + values and the matches over enumerations *) + | LvVar of var_or_dummy + | LvAdt of adt_lvalue and adt_lvalue = { variant_id : (VariantId.id option[@opaque]); @@ -505,12 +510,7 @@ and call = { *) } -and switch_body = - | If of texpression * texpression - | SwitchInt of integer_type * (scalar_value * texpression) list * texpression - | Match of match_branch list -(* TODO: merge SwitchInt and Match. In order to do that, - * we need to add constants to lvalues. *) +and switch_body = If of texpression * texpression | Match of match_branch list and match_branch = { pat : typed_lvalue; branch : texpression } diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 6b42e328..d8bfe4cd 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -240,19 +240,6 @@ let compute_pretty_names (def : fun_def) : fun_def = let ctx2, e_false = update_texpression e_false ctx in let ctx = merge_ctxs ctx1 ctx2 in (ctx, If (e_true, e_false)) - | SwitchInt (int_ty, branches, otherwise) -> - let ctx_branches_ls = - List.map - (fun (v, br) -> - let ctx, br = update_texpression br ctx in - (ctx, (v, br))) - branches - in - let ctx, otherwise = update_texpression otherwise ctx in - let ctxs, branches = List.split ctx_branches_ls in - let ctxs = merge_ctxs_ls ctxs in - let ctx = merge_ctxs ctx ctxs in - (ctx, SwitchInt (int_ty, branches, otherwise)) | Match branches -> let ctx_branches_ls = List.map @@ -478,12 +465,6 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call) fun () -> self#visit_texpression env e1 () && self#visit_texpression env e2 () - | SwitchInt (_, branches, otherwise) -> - fun () -> - List.for_all - (fun (_, br) -> self#visit_texpression env br ()) - branches - && self#visit_texpression env otherwise () | Match branches -> fun () -> List.for_all diff --git a/src/PureUtils.ml b/src/PureUtils.ml index c19d7914..f12ed87b 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -127,6 +127,17 @@ let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue = let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) +let compute_constant_value_ty (cv : constant_value) : ty = + match cv with + | V.Scalar sv -> Integer sv.V.int_ty + | Bool _ -> Bool + | Char _ -> Char + | String _ -> Str + +let mk_typed_lvalue_from_constant_value (cv : constant_value) : typed_lvalue = + let ty = compute_constant_value_ty cv in + { value = LvConcrete cv; ty } + let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression = let e = Value (v, mp) in let ty = v.ty in diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 9a611899..a1208f92 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1305,21 +1305,28 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : - scalar_value * texpression = + match_branch = (* We don't need to update the context: we don't introduce any * new values/variables *) - let branch_e = translate_expression branch_e ctx in - (v, branch_e) + let branch = translate_expression branch_e ctx in + let pat = mk_typed_lvalue_from_constant_value (V.Scalar v) in + { pat; branch } in let branches = List.map translate_branch branches in let otherwise = translate_expression otherwise ctx in + let pat_ty = Integer int_ty in + let otherwise_pat : typed_lvalue = { value = LvVar Dummy; ty = pat_ty } in + let otherwise : match_branch = + { pat = otherwise_pat; branch = otherwise } + in + let all_branches = List.append branches [ otherwise ] in let e = Switch - ( mk_value_expression scrutinee scrutinee_mplace, - SwitchInt (int_ty, branches, otherwise) ) + (mk_value_expression scrutinee scrutinee_mplace, Match all_branches) in - let ty = otherwise.ty in - assert (List.for_all (fun (_, br) -> br.ty = ty) branches); + let ty = otherwise.branch.ty in + assert ( + List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches); { e; ty } and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) : -- cgit v1.2.3