File tree Expand file tree Collapse file tree 4 files changed +68
-0
lines changed Expand file tree Collapse file tree 4 files changed +68
-0
lines changed Original file line number Diff line number Diff line change @@ -1101,6 +1101,29 @@ fn run(tcx: TyCtxt) {
1101
1101
) ;
1102
1102
}
1103
1103
1104
+ // For testing, putting #[c2rust_analyze_test::force_non_null_args] on a function marks its
1105
+ // arguments as `NON_NULL` and also adds `NON_NULL` to the `updates_forbidden` mask.
1106
+ for & ldid in & all_fn_ldids {
1107
+ if !util:: has_test_attr ( tcx, ldid, TestAttr :: ForceNonNullArgs ) {
1108
+ continue ;
1109
+ }
1110
+
1111
+ let info = func_info. get_mut ( & ldid) . unwrap ( ) ;
1112
+ let mut asn = gasn. and ( & mut info. lasn ) ;
1113
+ let mut updates_forbidden = g_updates_forbidden. and_mut ( & mut info. l_updates_forbidden ) ;
1114
+
1115
+ let lsig = & gacx. fn_sigs [ & ldid. to_def_id ( ) ] ;
1116
+ for arg_lty in lsig. inputs . iter ( ) . copied ( ) {
1117
+ for lty in arg_lty. iter ( ) {
1118
+ let ptr = lty. label ;
1119
+ if !ptr. is_none ( ) {
1120
+ asn. perms_mut ( ) [ ptr] . insert ( PermissionSet :: NON_NULL ) ;
1121
+ updates_forbidden[ ptr] . insert ( PermissionSet :: NON_NULL ) ;
1122
+ }
1123
+ }
1124
+ }
1125
+ }
1126
+
1104
1127
eprintln ! ( "=== ADT Metadata ===" ) ;
1105
1128
eprintln ! ( "{:?}" , gacx. adt_metadata) ;
1106
1129
Original file line number Diff line number Diff line change @@ -530,6 +530,9 @@ pub enum TestAttr {
530
530
FailBeforeRewriting ,
531
531
/// `#[c2rust_analyze_test::skip_rewrite]`: Skip generating rewrites for the function.
532
532
SkipRewrite ,
533
+ /// `#[c2rust_analyze_test::force_non_null_args]`: Mark arguments as `NON_NULL` and don't allow
534
+ /// that flag to be changed during dataflow analysis.
535
+ ForceNonNullArgs ,
533
536
}
534
537
535
538
impl TestAttr {
@@ -539,6 +542,7 @@ impl TestAttr {
539
542
TestAttr :: FailBeforeAnalysis => "fail_before_analysis" ,
540
543
TestAttr :: FailBeforeRewriting => "fail_before_rewriting" ,
541
544
TestAttr :: SkipRewrite => "skip_rewrite" ,
545
+ TestAttr :: ForceNonNullArgs => "force_non_null_args" ,
542
546
}
543
547
}
544
548
}
Original file line number Diff line number Diff line change @@ -56,6 +56,7 @@ define_tests! {
56
56
insertion_sort_rewrites,
57
57
known_fn,
58
58
non_null,
59
+ non_null_force,
59
60
offset1,
60
61
offset2,
61
62
pointee,
Original file line number Diff line number Diff line change
1
+ #![ feature( register_tool) ]
2
+ #![ register_tool( c2rust_analyze_test) ]
3
+
4
+ // TODO: All the pointers here are currently inferred to be non-`UNIQUE`, even though the access
5
+ // patterns look fine.
6
+
7
+ use std:: ptr;
8
+
9
+ // CHECK-LABEL: final labeling for "f"
10
+ fn f ( cond : bool ) {
11
+ let x = 1_i32 ;
12
+ // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = (empty)#
13
+ let mut y = ptr:: addr_of!( x) ;
14
+ if cond {
15
+ y = 0 as * const _ ;
16
+ }
17
+ // The expression `y` is considered nullable even though it's passed for argument `p` of `g`,
18
+ // which is forced to be `NON_NULL`.
19
+ // CHECK: ([[@LINE+1]]: y): {{.*}}, type = (empty)#
20
+ g ( cond, y) ;
21
+ }
22
+
23
+ // CHECK-LABEL: final labeling for "g"
24
+ // `p` should be non-null, as it's forced to be by the attribute. This emulates the "unsound" PDG
25
+ // case, where a variable is forced to stay `NON_NULL` even though a null possibly flows into it.
26
+ // CHECK: ([[@LINE+2]]: p): {{.*}}, type = NON_NULL#
27
+ #[ c2rust_analyze_test:: force_non_null_args]
28
+ fn g ( cond : bool , p : * const i32 ) {
29
+ // `q` is not forced to be `NON_NULL`, so it should be inferred nullable due to the null
30
+ // assignment below.
31
+ // CHECK: ([[@LINE+1]]: mut q): {{.*}}, type = (empty)#
32
+ let mut q = p;
33
+ if cond {
34
+ q = 0 as * const _ ;
35
+ }
36
+ // `r` is derived from `q` (and is not forced), so it should also be nullable.
37
+ // CHECK: ([[@LINE+1]]: r): {{.*}}, type = (empty)#
38
+ let r = q;
39
+ }
40
+
You can’t perform that action at this time.
0 commit comments