Update installation guide to include rmc crate build (rust-lang#604)

Update documentation after adding rmc crate

Author: celinval

rmc-docs/src/dev-documentation.md

@@ -12,6 +12,10 @@
 ```
 ([`--keep-stage` comes with caveats](https://rustc-dev-guide.rust-lang.org/building/suggested.html#incremental-builds-with---keep-stage). Know that it may cause spurious build failures.)
 ```bash
+# Build rmc crate
+./scripts/setup/rmc_build_lib.sh
+```
+```bash
 # Full regression suite
 ./scripts/rmc-regression.sh
 ```

rmc-docs/src/install-guide.md

@@ -54,10 +54,11 @@ Perform one-time build configuration:
 
 **NOTE: If you skip the above (`llvm.download-ci-llvm=true` specifically), builds may take a long time as all of LLVM would need to be built from scratch.**
 
-Then build RMC:
+Then build RMC and its library:
 
 ```
 ./x.py build -i --stage 1 library/std
+./scripts/setup/build_rmc_lib.sh
 ```
 
 Then, optionally, run the regression tests:

rmc-docs/src/tutorial-first-steps.md

@@ -71,7 +71,7 @@ The second command opens that report in your default browser (on mac, on linux d
 From this report, we can find the trace of the failure and filter through it to find the relevant line (at present time, an unfortunate amount of generated code is present in the trace):
 
 ```
-let x: u32 = __nondet();
+let x: u32 = rmc::nondet();
 x = 1023u
 ```
 

rmc-docs/src/tutorial-kinds-of-failure.md

@@ -101,26 +101,26 @@ Having run `rmc --visualize` and clicked on one of the failures to see a trace,
 
 To navigate this trace to find the information you need, we recommend searching for things you expect to be somewhere in the trace:
 
-1. Search the document for `__nondet` or `variable_of_interest =` such as `size =`.
+1. Search the document for `rmc::nondet` or `variable_of_interest =` such as `size =`.
 We can use this to find out what example values lead to a problem.
-In this case, where we just have a couple of `__nondet` values in our proof harness, we can learn a lot just by seeing what these are.
+In this case, where we just have a couple of `rmc::nondet` values in our proof harness, we can learn a lot just by seeing what these are.
 In this trace we find (and the values you get may be different):
 
 ```
 Step 23: Function main, File tests/bounds-check.rs, Line 43
-let size: usize = __nondet();
+let size: usize = rmc::nondet();
 size = 0ul
 
 Step 27: Function main, File tests/bounds-check.rs, Line 45
-let index: usize = __nondet();
+let index: usize = rmc::nondet();
 index = 0ul
 
 Step 36: Function main, File tests/bounds-check.rs, Line 43
-let size: usize = __nondet();
+let size: usize = rmc::nondet();
 size = 2464ul
 
 Step 39: Function main, File tests/bounds-check.rs, Line 45
-let index: usize = __nondet();
+let index: usize = rmc::nondet();
 index = 2463ul
 ```
 

rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs

@@ -29,20 +29,13 @@ mod tests {
     // ANCHOR_END: proptest
 }
 
-fn __nondet<T>() -> T {
-    unimplemented!()
-}
-fn __VERIFIER_assume(cond: bool) {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let size: usize = __nondet();
-    __VERIFIER_assume(size < 4096);
-    let index: usize = __nondet();
+    let size: usize = rmc::nondet();
+    rmc::assume(size < 4096);
+    let index: usize = rmc::nondet();
     let array: Vec<u32> = vec![0; size];
     get_wrapped(index, &array);
 }

rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs

@@ -7,19 +7,12 @@ fn find_midpoint(low: u32, high: u32) -> u32 {
 }
 // ANCHOR_END: code
 
-fn __nondet<T>() -> T {
-    unimplemented!()
-}
-fn __VERIFIER_assume(cond: bool) {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let a: u32 = __nondet();
-    let b: u32 = __nondet();
+    let a: u32 = rmc::nondet();
+    let b: u32 = rmc::nondet();
     find_midpoint(a, b);
 }
 // ANCHOR_END: rmc

rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs

@@ -22,19 +22,12 @@ mod tests {
     // ANCHOR_END: proptest
 }
 
-fn __nondet<T>() -> T {
-    unimplemented!()
-}
-fn __VERIFIER_assume(cond: bool) {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let a: u32 = __nondet();
-    let b: u32 = __nondet();
+    let a: u32 = rmc::nondet();
+    let b: u32 = rmc::nondet();
     simple_addition(a, b);
 }
 // ANCHOR_END: rmc

rmc-docs/src/tutorial/loops-unwinding/src/lib.rs

@@ -14,22 +14,15 @@ fn initialize_prefix(length: usize, buffer: &mut [u8]) {
 }
 // ANCHOR_END: code
 
-fn __nondet<T>() -> T {
-    unimplemented!()
-}
-fn __VERIFIER_assume(cond: bool) {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
     const LIMIT: usize = 10;
     let mut buffer: [u8; LIMIT] = [1; LIMIT];
 
-    let length = __nondet();
-    __VERIFIER_assume(length <= LIMIT);
+    let length = rmc::nondet();
+    rmc::assume(length <= LIMIT);
 
     initialize_prefix(length, &mut buffer);
 }

rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs

@@ -46,15 +46,11 @@ mod tests {
     // ANCHOR_END: proptest
 }
 
-fn __nondet() -> u32 {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let x: u32 = __nondet();
+    let x: u32 = rmc::nondet();
     estimate_size(x);
 }
 // ANCHOR_END: rmc

rmc-docs/src/tutorial/rmc-first-steps/tests/final-form.rs

@@ -48,19 +48,12 @@ mod tests {
     // ANCHOR_END: proptest
 }
 
-fn __nondet() -> u32 {
-    unimplemented!()
-}
-fn __VERIFIER_assume(cond: bool) {
-    unimplemented!()
-}
-
 // ANCHOR: rmc
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let x: u32 = __nondet();
-    __VERIFIER_assume(x < 4096);
+    let x: u32 = rmc::nondet();
+    rmc::assume(x < 4096);
     let y = estimate_size(x);
     assert!(y < 10);
 }
@@ -69,6 +62,6 @@ fn main() {
 #[cfg(rmc)]
 #[no_mangle]
 fn failing_main() {
-    let x: u32 = __nondet();
+    let x: u32 = rmc::nondet();
     let y = estimate_size(x);
 }