@@ -445,6 +445,15 @@ let bitmap_assigning_visitor
445
445
Walk. visit_block_pre = visit_block_pre }
446
446
;;
447
447
448
+ type slots_stack = node_id Stack .t ;;
449
+ type block_slots_stack = slots_stack Stack .t ;;
450
+ type frame_block_slots_stack = block_slots_stack Stack .t ;;
451
+ type loop_block_slots_stack = block_slots_stack option Stack .t ;;
452
+ (* like ret drops slots from all blocks in the frame
453
+ * break from a simple loo drops slots from all block in a loop *)
454
+ let (loop_blocks:loop_block_slots_stack ) =
455
+ let s = Stack. create() in Stack. push None s; s
456
+
448
457
let condition_assigning_visitor
449
458
(cx :ctxt )
450
459
(tables_stack :typestate_tables Stack.t )
@@ -574,7 +583,7 @@ let condition_assigning_visitor
574
583
let precond = slot_inits (lval_slots cx lval) in
575
584
raise_precondition sid precond;
576
585
in
577
-
586
+
578
587
let visit_stmt_pre s =
579
588
begin
580
589
match s.node with
@@ -694,7 +703,6 @@ let condition_assigning_visitor
694
703
| Ast. STMT_check_expr expr ->
695
704
let precond = slot_inits (expr_slots cx expr) in
696
705
raise_pre_post_cond s.id precond
697
-
698
706
| Ast. STMT_while sw ->
699
707
let (_, expr) = sw.Ast. while_lval in
700
708
let precond = slot_inits (expr_slots cx expr) in
@@ -1275,9 +1283,6 @@ let typestate_verify_visitor
1275
1283
Walk. visit_block_pre = visit_block_pre }
1276
1284
;;
1277
1285
1278
- type slots_stack = node_id Stack .t ;;
1279
- type block_slots_stack = slots_stack Stack .t ;;
1280
- type frame_block_slots_stack = block_slots_stack Stack .t ;;
1281
1286
1282
1287
let lifecycle_visitor
1283
1288
(cx :ctxt )
@@ -1312,18 +1317,24 @@ let lifecycle_visitor
1312
1317
1313
1318
1314
1319
let visit_block_pre b =
1315
- Stack. push (Stack. create() ) (Stack. top frame_blocks);
1316
- begin
1317
- match htab_search implicit_init_block_slots b.id with
1318
- None -> ()
1319
- | Some slots ->
1320
+
1321
+ let s = Stack. create() in
1322
+ begin
1323
+ match Stack. top loop_blocks with
1324
+ Some loop -> Stack. push s loop | None -> ()
1325
+ end ;
1326
+ Stack. push s (Stack. top frame_blocks);
1327
+ begin
1328
+ match htab_search implicit_init_block_slots b.id with
1329
+ None -> ()
1330
+ | Some slots ->
1320
1331
List. iter
1321
1332
(fun slot ->
1322
1333
push_slot slot;
1323
1334
mark_slot_live slot)
1324
1335
slots
1325
- end ;
1326
- inner.Walk. visit_block_pre b
1336
+ end ;
1337
+ inner.Walk. visit_block_pre b
1327
1338
in
1328
1339
1329
1340
let note_drops stmt slots =
@@ -1341,8 +1352,20 @@ let lifecycle_visitor
1341
1352
htab_put cx.ctxt_post_stmt_slot_drops stmt.id slots
1342
1353
in
1343
1354
1355
+ let filter_live_block_slots slots =
1356
+ List. filter (fun i -> Hashtbl. mem live_block_slots i) slots
1357
+ in
1358
+
1344
1359
let visit_block_post b =
1345
1360
inner.Walk. visit_block_post b;
1361
+ begin
1362
+ match Stack. top loop_blocks with
1363
+ Some loop ->
1364
+ ignore(Stack. pop loop);
1365
+ if Stack. is_empty loop then
1366
+ ignore(Stack. pop loop_blocks);
1367
+ | None -> ()
1368
+ end ;
1346
1369
let block_slots = Stack. pop (Stack. top frame_blocks) in
1347
1370
let stmts = b.node in
1348
1371
let len = Array. length stmts in
@@ -1352,7 +1375,8 @@ let lifecycle_visitor
1352
1375
let s = stmts.(len-1 ) in
1353
1376
match s.node with
1354
1377
Ast. STMT_ret _
1355
- | Ast. STMT_be _ ->
1378
+ | Ast. STMT_be _
1379
+ | Ast. STMT_break ->
1356
1380
() (* Taken care of in visit_stmt_post below. *)
1357
1381
| _ ->
1358
1382
(* The blk_slots stack we have has accumulated slots in
@@ -1364,11 +1388,7 @@ let lifecycle_visitor
1364
1388
* point in the block.
1365
1389
*)
1366
1390
let slots = stk_elts_from_top block_slots in
1367
- let live =
1368
- List. filter
1369
- (fun i -> Hashtbl. mem live_block_slots i)
1370
- slots
1371
- in
1391
+ let live = filter_live_block_slots slots in
1372
1392
note_drops s live
1373
1393
end ;
1374
1394
in
@@ -1440,6 +1460,10 @@ let lifecycle_visitor
1440
1460
f.Ast. for_each_body.id
1441
1461
[ (fst f.Ast. for_each_slot).id ]
1442
1462
1463
+ | Ast. STMT_while _ ->
1464
+ iflog cx (fun _ -> log cx " entering a loop" );
1465
+ Stack. push (Some (Stack. create () )) loop_blocks;
1466
+
1443
1467
| Ast. STMT_alt_tag { Ast. alt_tag_arms = arms } ->
1444
1468
let note_slot block slot_id =
1445
1469
log cx
@@ -1475,26 +1499,38 @@ let lifecycle_visitor
1475
1499
1476
1500
let visit_stmt_post s =
1477
1501
inner.Walk. visit_stmt_post s;
1502
+ let handle_ret_like_stmt block_stack =
1503
+ let blocks = stk_elts_from_top block_stack in
1504
+ let slots = List. concat (List. map stk_elts_from_top blocks) in
1505
+ let live = filter_live_block_slots slots in
1506
+ note_drops s live
1507
+ in
1478
1508
match s.node with
1479
1509
Ast. STMT_ret _
1480
1510
| Ast. STMT_be _ ->
1481
- let blocks = stk_elts_from_top (Stack. top frame_blocks) in
1482
- let slots = List. concat (List. map stk_elts_from_top blocks) in
1483
- let live =
1484
- List. filter
1485
- (fun i -> Hashtbl. mem live_block_slots i)
1486
- slots
1487
- in
1488
- note_drops s live
1511
+ handle_ret_like_stmt (Stack. top frame_blocks)
1512
+ | Ast. STMT_break ->
1513
+ begin
1514
+ match (Stack. top loop_blocks) with
1515
+ Some loop -> handle_ret_like_stmt loop
1516
+ | None ->
1517
+ iflog cx (fun _ ->
1518
+ log cx " break statement outside of a loop" );
1519
+ err (Some s.id) " break statement outside of a loop"
1520
+ end
1489
1521
| _ -> ()
1490
1522
in
1491
1523
1492
1524
let enter_frame _ =
1493
- Stack. push (Stack. create() ) frame_blocks
1525
+ Stack. push (Stack. create() ) frame_blocks;
1526
+ Stack. push None loop_blocks
1494
1527
in
1495
-
1528
+
1496
1529
let leave_frame _ =
1497
- ignore (Stack. pop frame_blocks)
1530
+ ignore (Stack. pop frame_blocks);
1531
+ match Stack. pop loop_blocks with
1532
+ Some _ -> bug () " leave_frame should not end a loop"
1533
+ | None -> ()
1498
1534
in
1499
1535
1500
1536
let visit_mod_item_pre n p i =
0 commit comments