Skip to content

Commit

Permalink
fixup! motoko-san: support labels, breaks, and continues
Browse files Browse the repository at this point in the history
  • Loading branch information
@DK318
DK318 committed Jun 3, 2024
1 parent 5b7b1cd commit 1c1c5a3
Show file tree
Hide file tree
Showing 4 changed files with 45 additions and 42 deletions.
4 changes: 4 additions & 0 deletions src/viper/common.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions src/viper/syntax.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,3 +103,4 @@ and typ' =
| TupleT
| OptionT of typ
| ConT of id * typ list

46 changes: 22 additions & 24 deletions src/viper/trans.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 []
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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 ->
Expand Down
36 changes: 18 additions & 18 deletions test/viper/ok/label-break-continue.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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));
Expand All @@ -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)
Expand All @@ -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,
Expand All @@ -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;
}
Expand All @@ -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;
}

0 comments on commit 1c1c5a3

Please sign in to comment.