From 1c1c5a37c50963661296393683b84cfba891a0c5 Mon Sep 17 00:00:00 2001 From: Leonid Vasilev Date: Tue, 4 Jun 2024 00:07:11 +0400 Subject: [PATCH] fixup! motoko-san: support labels, breaks, and continues --- src/viper/common.ml | 4 ++ src/viper/syntax.ml | 1 + src/viper/trans.ml | 46 +++++++++++------------ test/viper/ok/label-break-continue.vpr.ok | 36 +++++++++--------- 4 files changed, 45 insertions(+), 42 deletions(-) diff --git a/src/viper/common.ml b/src/viper/common.ml index b241fa8aaf1..699fda898a6 100644 --- a/src/viper/common.ml +++ b/src/viper/common.ml @@ -4,3 +4,7 @@ exception Unsupported of Source.region * string let unsupported at sexp = raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp))) +let rec map_last ~f = function + | [] -> [] + | [ x ] -> [ f x ] + | x :: xs -> x :: map_last ~f xs diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml index b4ec163f91c..8030a81d393 100644 --- a/src/viper/syntax.ml +++ b/src/viper/syntax.ml @@ -103,3 +103,4 @@ and typ' = | TupleT | OptionT of typ | ConT of id * typ list + diff --git a/src/viper/trans.ml b/src/viper/trans.ml index a3724334484..513ed25cbcc 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -7,7 +7,8 @@ module T = Mo_types.Type module M = Mo_def.Syntax module Arrange = Mo_def.Arrange -module Stamps = Env.Make(String) +module String_map = Env.Make(String) +module Stamps = String_map (* symbol generation *) @@ -100,8 +101,8 @@ module Env = T.Env type ctxt = { self : string option; ids : (sort * T.t) T.Env.t; - label_vars : (string, id) Hashtbl.t; (* Orig label var -> associated tmp variable. *) - mapped_labels : (string, string) Hashtbl.t; (* Orig label var -> label var in viper. *) + label_vars : id String_map.t; (* Orig label var -> associated tmp variable. *) + mapped_labels : string String_map.t; (* Orig label var -> label var in viper. *) ghost_items : (ctxt -> item) list ref; ghost_inits : (ctxt -> seqn') list ref; ghost_perms : (ctxt -> Source.region -> exp) list ref; @@ -190,8 +191,8 @@ and unit' (u : M.comp_unit) : prog = let ctxt = { self = None ; ids = Env.empty - ; label_vars = Hashtbl.create 32 - ; mapped_labels = Hashtbl.create 32 + ; label_vars = String_map.empty + ; mapped_labels = String_map.empty ; ghost_items = ref [] ; ghost_inits = ref [] ; ghost_perms = ref [] @@ -480,7 +481,7 @@ and compile_while let body = match label_id with | Some label_id -> - let label = loop_label ctxt label_id in + let label, ctxt = loop_label ctxt label_id in let stmts = stmt ctxt body in let decls, stmts = stmts.it in !!(decls, !!(LabelS label) :: stmts) @@ -597,14 +598,15 @@ and stmt ctxt (s : M.exp) : seqn = let stmt = !!(GotoS(!!! (Source.no_region) "$Ret")) in !!(ds, stmts @ [stmt]) | M.LabelE (label_id, typ, e) -> - let label = !!! Source.no_region (LabelS (loop_label ctxt label_id)) in + let label_id, ctxt = loop_label ctxt label_id in + let label = !!! Source.no_region (LabelS label_id) in let stmts = stmt ctxt e in let decls, stmts = stmts.it in let stmts = stmts @ [ label ] in !!(decls, stmts) | M.BreakE (label_id, ret) -> let stmts = - match Hashtbl.find_opt ctxt.label_vars label_id.it with + match String_map.find_opt label_id.it ctxt.label_vars with | None -> stmt ctxt ret | Some x -> let lvalue = LValueVar x in @@ -613,7 +615,7 @@ and stmt ctxt (s : M.exp) : seqn = in let decls, stmts = stmts.it in let label_name = - match Hashtbl.find_opt ctxt.mapped_labels label_id.it with + match String_map.find_opt label_id.it ctxt.mapped_labels with | Some name -> name | None -> failwith (Format.asprintf "can't find mapped name for label \"%s\"" label_id.it) in @@ -830,21 +832,21 @@ and rets t_opt = and id id = { it = id.it; at = id.at; note = NoInfo } -(* Make sure that you call it before translating inner expressions. - This thing mutates [ctxt] environment and we want to update it first. *) and loop_label ctxt loop_label = let label_name = loop_label.it |> String.map (fun ch -> (* Life without Core is hard... *) if Char.equal ch ' ' - then '_' + then '$' else ch) - |> Format.asprintf "$%s" + |> Format.asprintf "$lbl$%s" |> fresh_id in - Hashtbl.add ctxt.mapped_labels loop_label.it label_name; - id { loop_label with it = label_name } + let ctxt = + { ctxt with mapped_labels = String_map.add loop_label.it label_name ctxt.mapped_labels } + in + id { loop_label with it = label_name }, ctxt and tr_typ typ = { it = tr_typ' typ; @@ -940,10 +942,11 @@ and tuple_prj ctxt at e1 e2 t = prjE at (exp ctxt e1) (exp ctxt e2) (typed_field t) and label_alloc ~label_id ~label_type ~label_rhs ~label_note at ctxt lhs : seqn' = - (match label_type.it with - | M.TupT [] -> () - | _ -> Hashtbl.add ctxt.label_vars label_id.it lhs); - + let ctxt = + match label_type.it with + | M.TupT [] -> ctxt + | _ -> { ctxt with label_vars = String_map.add label_id.it lhs ctxt.label_vars } + in let wrap_break exp = match label_type.it, exp.it with | M.TupT [], _ | _, M.BreakE _ -> exp @@ -952,11 +955,6 @@ and label_alloc ~label_id ~label_type ~label_rhs ~label_note at ctxt lhs : seqn' let label_rhs = match label_rhs.it with | M.BlockE decs -> - let rec map_last ~f = function - | [] -> [] - | [ x ] -> [ f x ] - | x :: xs -> x :: map_last ~f xs - in let decs = map_last decs ~f:(fun dec -> match dec.it with | M.ExpD exp -> diff --git a/test/viper/ok/label-break-continue.vpr.ok b/test/viper/ok/label-break-continue.vpr.ok index 347cedd5e26..794888366d7 100644 --- a/test/viper/ok/label-break-continue.vpr.ok +++ b/test/viper/ok/label-break-continue.vpr.ok @@ -58,12 +58,12 @@ method label_expressions($Self: Ref) var mut_label: Tuple var mut_label_2: Tuple simple_label := 42; - goto $simple; - label $simple; + goto $lbl$simple; + label $lbl$simple; assume (simple_label == 42); implicit_leave := 42; - goto $implicit; - label $implicit; + goto $lbl$implicit; + label $lbl$implicit; assume (implicit_leave == 42); if (true) { var $t_block_label_early_expr: Tuple @@ -76,7 +76,7 @@ method label_expressions($Self: Ref) exhale acc(($prj($t_block_label_early_expr, 1)).$int,wildcard); inhale acc(($prj($t_block_label_early_expr, 1)).$int,wildcard); block_label_early_expr := $t_block_label_early_expr; - goto $block; + goto $lbl$block; }; inhale (acc(($prj($t_block_label_early_expr_2, 0)).$int,write) && acc(($prj($t_block_label_early_expr_2, 1)).$int,write)); @@ -87,8 +87,8 @@ method label_expressions($Self: Ref) exhale acc(($prj($t_block_label_early_expr_2, 1)).$int,wildcard); inhale acc(($prj($t_block_label_early_expr_2, 1)).$int,wildcard); block_label_early_expr := $t_block_label_early_expr_2; - goto $block; - label $block; + goto $lbl$block; + label $lbl$block; assume ((($prj(block_label_early_expr, 0)).$int == 42) && (($prj(block_label_early_expr, 1)).$int == 42)); if (false) @@ -102,7 +102,7 @@ method label_expressions($Self: Ref) exhale acc(($prj($t_block_label_expr, 1)).$int,wildcard); inhale acc(($prj($t_block_label_expr, 1)).$int,wildcard); block_label_expr := $t_block_label_expr; - goto $block_2; + goto $lbl$block_2; }; inhale (acc(($prj($t_block_label_expr_2, 0)).$int,write) && acc( ($prj($t_block_label_expr_2, @@ -114,27 +114,27 @@ method label_expressions($Self: Ref) exhale acc(($prj($t_block_label_expr_2, 1)).$int,wildcard); inhale acc(($prj($t_block_label_expr_2, 1)).$int,wildcard); block_label_expr := $t_block_label_expr_2; - goto $block_2; - label $block_2; + goto $lbl$block_2; + label $lbl$block_2; assume ((($prj(block_label_expr, 0)).$int == 24) && (($prj(block_label_expr, 1)).$int == 24)); v := 0; if (true) { v := 42; - goto $mutability; + goto $lbl$mutability; }; v := 100; - label $mutability; + label $lbl$mutability; assume (v == 42); v := 0; if (false) { v := 42; - goto $mutability_2; + goto $lbl$mutability_2; }; v := 100; - label $mutability_2; + label $lbl$mutability_2; assume (v == 100); label $Ret; } @@ -148,15 +148,15 @@ method loops($Self: Ref) invariant (i < 3) invariant ($Perm($Self) && $Inv($Self)) { - label $continue_while_loop; + label $lbl$continue$while_loop; i := (i + 1); if ((i == 3)) { - goto $while_loop; + goto $lbl$while_loop; }; - goto $continue_while_loop; + goto $lbl$continue$while_loop; i := 100; }; - label $while_loop; + label $lbl$while_loop; label $Ret; }