1
- // --unwind 3 --unwinding-assertions
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
2
3
//
3
- // Example from Firecracker balloon device
4
- // We test the functional correctness of the compact function
5
- // Outstanding issues:
6
- // - Padstone-4988 (vector sort not supported)
7
- // - Padstone-4856 (vector tuple iteration)
4
+ // Try with: rmc ignore-main.rs -- --unwind 3 --unwinding-assertions --pointer-check --object-bits 11
5
+ // With kissat as the solver (--external-sat-solver /path/to/kissat) this takes ~5mins
8
6
9
- # [ allow ( dead_code ) ]
7
+ pub const MAX_PAGE_COMPACT_BUFFER : usize = 2048 ;
10
8
11
- pub const MAX_PAGES_IN_DESC : usize = 256 ;
12
-
13
- pub ( crate ) fn compact_page_frame_numbers ( v : & mut Vec < u32 > ) -> Vec < ( u32 , u32 ) > {
9
+ pub ( crate ) fn compact_page_frame_numbers ( v : & mut [ u32 ] ) -> Vec < ( u32 , u32 ) > {
14
10
if v. is_empty ( ) {
15
11
return vec ! [ ] ;
16
12
}
17
13
18
14
// Since the total number of pages that can be
19
- // received at once from a single descriptor is `MAX_PAGES_IN_DESC `,
15
+ // received at once is `MAX_PAGE_COMPACT_BUFFER `,
20
16
// this sort does not change the complexity of handling
21
17
// an inflation.
22
- // v.sort (); //< Padstone-4988 (vector sort not supported)
18
+ v . sort_unstable ( ) ;
23
19
24
- // Since there are at most `MAX_PAGES_IN_DESC ` pages, setting the
20
+ // Since there are at most `MAX_PAGE_COMPACT_BUFFER ` pages, setting the
25
21
// capacity of `result` to this makes sense.
26
- let mut result = Vec :: with_capacity ( MAX_PAGES_IN_DESC ) ;
22
+ let mut result = Vec :: with_capacity ( MAX_PAGE_COMPACT_BUFFER ) ;
27
23
28
24
// The most recent range of pages is [previous..previous + length).
29
25
let mut previous = v[ 0 ] ;
@@ -57,27 +53,14 @@ fn expand(ranges: Vec<(u32, u32)>) -> Vec<u32> {
57
53
return v;
58
54
}
59
55
60
- // Padstone-4856 this version of expand required instead of fn above
61
- fn rmc_expand ( ranges : Vec < ( u32 , u32 ) > ) -> Vec < u32 > {
62
- let mut i = 0 ;
63
- let mut v: Vec < u32 > = Vec :: new ( ) ;
64
- while i < ranges. len ( ) {
65
- let ( start, len) = ranges[ i] ;
66
- for j in start..=( start + len - 1 ) {
67
- v. push ( j)
68
- }
69
- i += 1 ;
70
- }
71
- return v;
72
- }
73
-
74
56
fn __nondet < T > ( ) -> T {
75
57
unimplemented ! ( )
76
58
}
77
59
78
60
fn main ( ) {
79
- let mut input = vec ! [ __nondet ( ) ; 2 ] ;
61
+ let mut input = vec ! [ 0 ; 2 ] ;
80
62
for i in 0 ..input. len ( ) {
63
+ input[ i] = __nondet ( ) ;
81
64
if input[ i] == u32:: MAX {
82
65
return ;
83
66
}
@@ -87,7 +70,7 @@ fn main() {
87
70
assert ! ( 1 <= * len) ;
88
71
}
89
72
assert ! ( output. len( ) <= input. len( ) ) ;
90
- let expanded_output = rmc_expand ( output) ;
73
+ let expanded_output = expand ( output) ;
91
74
let i: usize = __nondet ( ) ;
92
75
if i < expanded_output. len ( ) {
93
76
assert ! ( expanded_output[ i] == input[ i] ) ;
0 commit comments