Unstable development branch (WIP)

.github/workflows/test.yml

@@ -87,9 +87,32 @@ jobs:
     - name: Run unit tests
       run: cargo test --doc
 
+  flowistry_tests:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout pcs repository
+      uses: actions/checkout@v4
+      with:
+        path: pcs
+
+    - name: Checkout flowistry repository
+      uses: actions/checkout@v4
+      with:
+        repository: zgrannan/flowistry
+        ref: zgrannan/pcg
+        path: flowistry
+
+    - uses: dtolnay/rust-toolchain@master
+      with:
+        toolchain: nightly-2024-09-15
+
+    - name: Run flowistry tests
+      working-directory: flowistry/crates/flowistry
+      run: cargo test
+
   build-docker-image:
     runs-on: ubuntu-latest
-    needs: [check_warnings, clippy, test_files, bench_test_files, test_crates, unit_tests, doc_tests]
+    needs: [check_warnings, clippy, test_files, bench_test_files, test_crates, unit_tests, doc_tests, flowistry_tests]
     permissions:
       contents: read
       packages: write

benchmark_results.txt

@@ -1,76 +1,89 @@
-01_basic.rs: 34968039
-02_list_zero.rs: 70053253
-03_unnest.rs: 43597929
-04_chunks.rs: 176964110
-05_is_xid_start.rs: 157608674
-06_cursor.rs: 82603109
-07_fmt.rs: 113893560
-08_parse_parens.rs: 53412847
-09_punct.rs: 230866236
-10_members.rs: 52154913
-11_display.rs: 66995244
-12_jasper.rs: 72964745
-13_heap_visitor.rs: 45534187
-14_serde_err.rs: 1177956222
-15_bernoulli.rs: 87360186
-16_lookahead.rs: 47786189
-17_entry.rs: 69264999
-18_slice.rs: 73555243
-19_lifetime_projection.rs: 44045847
-20_eager.rs: 40610549
-21_jasper2.rs: 56334749
-22_itoa_format.rs: 60404888
-23_lazy_poll.rs: 62278649
-24_style_render_reset.rs: 130708067
-25_parse_str.rs: 49090477
-26_ref_in_struct.rs: 49707914
-27_aurel.rs: 41897423
-28_ranged_slice.rs: 69415629
-29_prusti_issue_25.rs: 53350295
-30_prusti_issue_738-5.rs: 46353602
-31_prusti_timeout.rs: 89731326
-32_deflate64_inputbuffer_advance.rs: 72150609
-33_hashtable_shrink_to_fit.rs: 52780759
-34_pair_into_value.rs: 28661275
-35_miniz_oxide_new_output_buffer.rs: 172834003
-36_gimli_endian_slice.rs: 175436046
-37_demo_loop.rs: 100616823
-38_regex_autonoma_iter_pattern_match_ids.rs: 92853701
-39_cfi.rs: 94986175
-40_object_archive.rs: 214359685
-41_itertools_k_smallest.rs: 123396982
-42_dfa_dense.rs: 1831140835
-43_der_length.rs: 108278567
-44_rand_weighted_index.rs: 1484102108
-45_closure.rs: 42535919
-46_demo_cond_mut_borrow.rs: 47288702
-47_demo_choose.rs: 42442155
-48_flowistry_basic.rs: 47176136
-49_flowistry_recurse.rs: 29545326
-50_flowistry_pointer_deep.rs: 45827808
-51_flowistry_recurse_not_all_args.rs: 47886235
-52_flowistry_recurse_parent_privacy.rs: 47916918
-53_flowistry_time_calculation.rs: 60403002
-54_flowistry_struct_mut_ptr.rs: 47053017
-55_prusti_ownership2.rs: 62021458
-56_deep2.rs: 43843116
-57_slice_ptr_elem_write.rs: 44741017
-58_aurel_pledge.rs: 48160151
-59_struct_ptrs_deep.rs: 67423773
-60_pointer_reborrow_nested.rs: 45327225
-61_hashset_union.rs: 92624936
-62_tuple_ptr_write_field.rs: 46632674
-63_flowistry_function_lifetime_alias_mut.rs: 42616510
-64_flowistry_enum_write_branch_read_whole.rs: 52566418
-65_flowistry_recurse_project_dst.rs: 29401200
-66_polonius_borrow_cycle.rs: 68185242
-67_proc_macro2_trailing_backslash.rs: 195056034
-68_miniz_push_dict_out.rs: 146766404
-69_http_header_map.rs: 303860359
-70_tonic_decode_chunk.rs: 178031184
-71_serde_with_deserialize.rs: 73795834
-72_flowistry_enum_write_branch_read_branch.rs: 53696963
-73_flowistry_aliases_basic.rs: 47139640
-74_aliases_projection.rs: 66027574
-75_flowistry_recurse_simple.rs: 43665578
-76_slice_write.rs: 62143206
+01_basic.rs: 33592205
+02_list_zero.rs: 69597752
+03_unnest.rs: 42278965
+04_chunks.rs: 278769167
+05_is_xid_start.rs: 156335460
+06_cursor.rs: 84804190
+07_fmt.rs: 130456216
+08_parse_parens.rs: 52748098
+09_punct.rs: 315849070
+10_members.rs: 51212674
+11_display.rs: 65561249
+12_jasper.rs: 71560828
+13_heap_visitor.rs: 44142817
+14_serde_err.rs: 1382095214
+15_bernoulli.rs: 85770215
+16_lookahead.rs: 47002588
+17_entry.rs: 68801720
+18_slice.rs: 93160688
+19_lifetime_projection.rs: 42700710
+20_eager.rs: 39297543
+21_jasper2.rs: 54834147
+22_itoa_format.rs: 59049771
+23_lazy_poll.rs: 60992136
+24_style_render_reset.rs: 129773514
+25_parse_str.rs: 47781393
+26_ref_in_struct.rs: 48195606
+27_aurel.rs: 40614823
+28_ranged_slice.rs: 67820050
+29_prusti_issue_25.rs: 51702585
+30_prusti_issue_738-5.rs: 44922541
+31_prusti_timeout.rs: 88323218
+32_deflate64_inputbuffer_advance.rs: 71718403
+33_hashtable_shrink_to_fit.rs: 51452994
+34_pair_into_value.rs: 27341778
+35_miniz_oxide_new_output_buffer.rs: 183722867
+36_gimli_endian_slice.rs: 184775878
+37_demo_loop.rs: 101000408
+38_regex_autonoma_iter_pattern_match_ids.rs: 115099620
+39_cfi.rs: 97415290
+40_object_archive.rs: 210389480
+41_itertools_k_smallest.rs: 138570314
+42_dfa_dense.rs: 3237520682
+43_der_length.rs: 106437370
+44_rand_weighted_index.rs: 5821986260
+45_closure.rs: 41287801
+46_demo_cond_mut_borrow.rs: 45889648
+47_demo_choose.rs: 42798929
+48_flowistry_basic.rs: 46241722
+49_flowistry_recurse.rs: 28163412
+50_flowistry_pointer_deep.rs: 44441482
+51_flowistry_recurse_not_all_args.rs: 46452142
+52_flowistry_recurse_parent_privacy.rs: 46516496
+53_flowistry_time_calculation.rs: 70900133
+54_flowistry_struct_mut_ptr.rs: 45608046
+55_prusti_ownership2.rs: 60621580
+56_deep2.rs: 42460608
+57_slice_ptr_elem_write.rs: 43348943
+58_aurel_pledge.rs: 47029848
+59_struct_ptrs_deep.rs: 65808800
+60_pointer_reborrow_nested.rs: 43924419
+61_hashset_union.rs: 113164584
+62_tuple_ptr_write_field.rs: 45258768
+63_flowistry_function_lifetime_alias_mut.rs: 41314957
+64_flowistry_enum_write_branch_read_whole.rs: 50954487
+65_flowistry_recurse_project_dst.rs: 28017171
+66_polonius_borrow_cycle.rs: 66464337
+67_proc_macro2_trailing_backslash.rs: 282975580
+68_miniz_push_dict_out.rs: 157409974
+69_http_header_map.rs: 411277516
+70_tonic_decode_chunk.rs: 178938245
+71_serde_with_deserialize.rs: 76144256
+72_flowistry_enum_write_branch_read_branch.rs: 52160257
+73_flowistry_aliases_basic.rs: 46202084
+74_aliases_projection.rs: 66075982
+75_flowistry_recurse_simple.rs: 42256545
+76_slice_write.rs: 61342614
+77_flowistry_interior_mutability_not_observable.rs: 65683636
+78_interior_mutability_observable.rs: 46875188
+79_add_overflow.rs: 69546402
+80_crc_bytewise.rs: 211820594
+79_add_overflow.rs: 69144639
+80_crc_bytewise.rs: 221361585
+81_shared_ref.rs: 43520001
+82_shared_ref_2.rs: 58097901
+83_prusti_wand.rs: 44743154
+84_prusti_ownership.rs: 41035866
+85_prusti_rpe_example.rs: 40983383
+86_prusti_mut_borrows.rs: 52540071
+87_prusti_create_box.rs: 50621751

src/borrow_pcg/action/actions.rs

@@ -1,10 +1,90 @@
 use crate::borrow_pcg::action::BorrowPCGAction;
-use crate::validity_checks_enabled;
+use crate::borrow_pcg::borrow_pcg_edge::BorrowPCGEdge;
+use crate::borrow_pcg::borrow_pcg_expansion::BorrowPCGExpansion;
+use crate::borrow_pcg::edge::block::BlockEdge;
+use crate::borrow_pcg::edge::kind::BorrowPCGEdgeKind;
+use crate::borrow_pcg::graph::Conditioned;
+use crate::borrow_pcg::unblock_graph::BorrowPCGUnblockAction;
+use crate::rustc_interface::data_structures::fx::FxHashSet;
+use crate::utils::json::ToJsonWithRepacker;
+use crate::utils::PlaceRepacker;
+use crate::{validity_checks_enabled, Weaken};
 
-#[derive(Clone, Debug)]
-#[derive(Default)]
-pub(crate) struct BorrowPCGActions<'tcx>(Vec<BorrowPCGAction<'tcx>>);
+use super::BorrowPCGActionKind;
 
+#[derive(Clone, Debug, Default)]
+pub struct BorrowPCGActions<'tcx>(pub(crate) Vec<BorrowPCGAction<'tcx>>);
+
+impl<'tcx> ToJsonWithRepacker<'tcx> for BorrowPCGActions<'tcx> {
+    fn to_json(&self, repacker: PlaceRepacker<'_, 'tcx>) -> serde_json::Value {
+        self.0
+            .iter()
+            .map(|a| a.to_json(repacker))
+            .collect::<Vec<_>>()
+            .into()
+    }
+}
+
+impl<'tcx> BorrowPCGActions<'tcx> {
+    /// Actions applied to the PCG, in the order they occurred.
+    pub fn actions(&self) -> &[BorrowPCGAction<'tcx>] {
+        &self.0
+    }
+
+    pub fn added_block_edges(&self) -> FxHashSet<Conditioned<BlockEdge<'tcx>>> {
+        self.0
+            .iter()
+            .filter_map(|action| match action.kind() {
+                BorrowPCGActionKind::AddEdge {
+                    edge:
+                        BorrowPCGEdge {
+                            kind: BorrowPCGEdgeKind::Block(edge),
+                            conditions,
+                            ..
+                        },
+                    ..
+                } => Some(Conditioned::new(edge.clone(), conditions.clone())),
+                _ => None,
+            })
+            .collect()
+    }
+
+    pub fn weakens(&self) -> FxHashSet<Weaken<'tcx>> {
+        self.0
+            .iter()
+            .filter_map(|action| match action.kind() {
+                BorrowPCGActionKind::Weaken(weaken) => Some(*weaken),
+                _ => None,
+            })
+            .collect()
+    }
+
+    pub fn unblock_actions(&self) -> Vec<BorrowPCGUnblockAction<'tcx>> {
+        self.0
+            .iter()
+            .filter_map(|action| match action.kind() {
+                BorrowPCGActionKind::RemoveEdge(edge) => Some(edge.clone().into()),
+                _ => None,
+            })
+            .collect()
+    }
+
+    pub fn expands(&self) -> FxHashSet<Conditioned<BorrowPCGExpansion<'tcx>>> {
+        self.0
+            .iter()
+            .filter_map(|action| match action.kind() {
+                BorrowPCGActionKind::AddEdge { edge, .. } => match edge.kind() {
+                    BorrowPCGEdgeKind::BorrowPCGExpansion(expansion) => Some(Conditioned::new(
+                        expansion.clone(),
+                        edge.conditions().clone(),
+                    )),
+                    _ => None,
+                },
+                _ => None,
+            })
+            .collect()
+    }
+}
 
 impl<'tcx> BorrowPCGActions<'tcx> {
     pub(crate) fn is_empty(&self) -> bool {
@@ -14,10 +94,6 @@ impl<'tcx> BorrowPCGActions<'tcx> {
         self.0.iter()
     }
 
-    pub(crate) fn into_vec(self) -> Vec<BorrowPCGAction<'tcx>> {
-        self.0
-    }
-
     pub(crate) fn new() -> Self {
         Self(vec![])
     }
@@ -36,11 +112,13 @@ impl<'tcx> BorrowPCGActions<'tcx> {
 
     pub(crate) fn extend(&mut self, actions: BorrowPCGActions<'tcx>) {
         if validity_checks_enabled() {
-            if let (Some(a), Some(b)) = (self.last(), actions.first()) { assert_ne!(
+            if let (Some(a), Some(b)) = (self.last(), actions.first()) {
+                assert_ne!(
                 a, b,
                 "The last action ({:#?}) is the same as the first action in the list to extend with.",
                 a,
-            ) }
+            )
+            }
         }
         self.0.extend(actions.0);
     }